walther@59960
|
1 |
(* Title: Specify/p-model.sml
|
wneuper@59316
|
2 |
Author: Walther Neuper 170207
|
wneuper@59316
|
3 |
(c) due to copyright terms
|
walther@59959
|
4 |
|
Walther@60686
|
5 |
This will mostly be dropped at switch to Isabelle/PIDE .
|
wneuper@59316
|
6 |
*)
|
wneuper@59316
|
7 |
|
walther@59959
|
8 |
signature PRESENTATION_MODEL =
|
wneuper@59316
|
9 |
sig
|
Walther@60605
|
10 |
(* for the OLD P_Model.T *)
|
walther@59969
|
11 |
type T
|
walther@59969
|
12 |
val empty: T
|
walther@59969
|
13 |
val to_string: T -> string
|
walther@59943
|
14 |
|
walther@59969
|
15 |
datatype item = (*shall be dropped with PIDE*)
|
walther@59969
|
16 |
Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string
|
walther@59969
|
17 |
| Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string
|
Walther@60586
|
18 |
type 'a model (*shall be dropped with PIDE*)
|
wneuper@59316
|
19 |
|
walther@59969
|
20 |
val from : theory -> I_Model.T -> Pre_Conds.T -> T
|
walther@59989
|
21 |
|
Walther@60586
|
22 |
val to_list: 'a model -> 'a list
|
walther@59989
|
23 |
val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
|
walther@59989
|
24 |
val mk_additem: string -> TermC.as_string -> Tactic.input
|
Walther@60578
|
25 |
|
Walther@60578
|
26 |
val item_from_feedback: theory -> I_Model.feedback -> item
|
Walther@60690
|
27 |
(*from isac_test for Minisubpbl*)
|
Walther@60705
|
28 |
val add_sel_ppc: theory -> string -> {Find: 'a list, Given: 'a list, Relate: 'a list, Where: 'a list, With: 'b} -> 'a -> {Find: 'a list, Given: 'a list, Relate: 'a list, Where: 'a list, With: 'b}
|
Walther@60705
|
29 |
|
Walther@60695
|
30 |
(**)
|
Walther@60578
|
31 |
|
wenzelm@60223
|
32 |
\<^isac_test>\<open>
|
Walther@60578
|
33 |
(**)
|
wenzelm@60223
|
34 |
\<close>
|
wneuper@59316
|
35 |
end
|
wneuper@59316
|
36 |
|
walther@59968
|
37 |
(**)
|
walther@59959
|
38 |
structure P_Model(**) : PRESENTATION_MODEL(**) =
|
wneuper@59316
|
39 |
struct
|
walther@59968
|
40 |
(**)
|
wneuper@59316
|
41 |
|
Walther@60690
|
42 |
datatype switch_pbl_met = For_Problem | For_Method
|
Walther@60605
|
43 |
|
Walther@60605
|
44 |
(** types for OLD presentation**)
|
wneuper@59316
|
45 |
|
Walther@60586
|
46 |
type 'a model =
|
walther@59969
|
47 |
{Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
|
wneuper@59316
|
48 |
datatype item =
|
walther@59865
|
49 |
Correct of TermC.as_string (* labels a correct formula (type cterm') *)
|
wneuper@59316
|
50 |
| SyntaxE of string (**)
|
wneuper@59316
|
51 |
| TypeE of string (**)
|
walther@59865
|
52 |
| False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
|
walther@59865
|
53 |
| Incompl of TermC.as_string (**)
|
wneuper@59316
|
54 |
| Superfl of string (**)
|
Walther@60431
|
55 |
| Missing of TermC.as_string; (*REVIEW: a "missing" item is not shown, thus cannot be marked*)
|
walther@59969
|
56 |
|
Walther@60586
|
57 |
type T = item model;
|
walther@59937
|
58 |
fun item2str (Correct s) = "Correct " ^ s
|
walther@59937
|
59 |
| item2str (SyntaxE s) = "SyntaxE " ^ s
|
walther@59937
|
60 |
| item2str (TypeE s) = "TypeE " ^ s
|
walther@59937
|
61 |
| item2str (False s) = "False " ^ s
|
walther@59937
|
62 |
| item2str (Incompl s) = "Incompl " ^ s
|
walther@59937
|
63 |
| item2str (Superfl s) = "Superfl " ^ s
|
walther@59937
|
64 |
| item2str (Missing s) = "Missing " ^ s;
|
walther@59937
|
65 |
|
walther@59969
|
66 |
fun to_string ({Given=Given,Where=Where,
|
Walther@60586
|
67 |
Find=Find,With=With,Relate=Relate}:item model)=
|
wneuper@59316
|
68 |
("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
|
wneuper@59316
|
69 |
",Where=" ^ ((strs2str' o (map item2str)) Where) ^
|
wneuper@59316
|
70 |
",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
|
wneuper@59316
|
71 |
",With =" ^ ((strs2str' o (map item2str)) With ) ^
|
wneuper@59316
|
72 |
",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
|
wneuper@59316
|
73 |
|
walther@59969
|
74 |
val empty = {Given = [], Where= [], Find = [], With = [], Relate= []};
|
wneuper@59316
|
75 |
|
walther@59968
|
76 |
|
walther@59969
|
77 |
(** build T **)
|
walther@59969
|
78 |
|
Walther@60745
|
79 |
(*T_TESTold*)
|
Walther@60578
|
80 |
fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
walther@59969
|
81 |
| item_from_feedback _ (I_Model.Syn c) = SyntaxE c
|
walther@59969
|
82 |
| item_from_feedback _ (I_Model.Typ c) = TypeE c
|
Walther@60578
|
83 |
| item_from_feedback thy (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60578
|
84 |
| item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60578
|
85 |
| item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
|
walther@59969
|
86 |
| item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
|
Walther@60745
|
87 |
(*T_TEST* )
|
Walther@60745
|
88 |
fun item_from_feedback_TEST thy (I_Model.Cor_TEST ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60745
|
89 |
| item_from_feedback_TEST _ (I_Model.Syn_TEST c) = SyntaxE c
|
Walther@60745
|
90 |
| item_from_feedback_TEST thy (I_Model.Inc_TEST ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60745
|
91 |
| item_from_feedback_TEST thy (I_Model.Sup_TEST (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60745
|
92 |
( *T_TESTnew*)
|
walther@59968
|
93 |
|
walther@59968
|
94 |
fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
|
walther@59968
|
95 |
case sel of
|
Walther@60578
|
96 |
"#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re}
|
walther@59968
|
97 |
| "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
|
walther@59968
|
98 |
| "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
|
walther@59968
|
99 |
| "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
|
walther@59968
|
100 |
| "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
|
walther@59968
|
101 |
| _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
|
walther@59968
|
102 |
fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
|
Walther@60576
|
103 |
{Given = gi, Where = wh, Find= fi , With = wi, Relate = re}
|
walther@59968
|
104 |
|
Walther@60675
|
105 |
fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term)
|
Walther@60675
|
106 |
| boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);
|
walther@59968
|
107 |
|
Walther@60586
|
108 |
fun from thy itms where_ =
|
walther@59968
|
109 |
let
|
Walther@60586
|
110 |
fun coll model [] = model
|
Walther@60586
|
111 |
| coll model ((_, _, _, field, itm_) :: itms) =
|
Walther@60586
|
112 |
coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
|
walther@59969
|
113 |
val gfr = coll empty itms;
|
Walther@60586
|
114 |
in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end;
|
walther@59968
|
115 |
|
walther@59989
|
116 |
fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
|
walther@59989
|
117 |
| mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
|
walther@59989
|
118 |
| mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
|
walther@59989
|
119 |
| mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
|
walther@59989
|
120 |
fun mk_additem "#Given" ct = Tactic.Add_Given ct
|
walther@59989
|
121 |
| mk_additem "#Find" ct = Tactic.Add_Find ct
|
walther@59989
|
122 |
| mk_additem "#Relate"ct = Tactic.Add_Relation ct
|
walther@59989
|
123 |
| mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
|
walther@59989
|
124 |
|
walther@59989
|
125 |
fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
|
walther@59989
|
126 |
gis @ whs @ fis @ wis @ res
|
walther@59989
|
127 |
|
Walther@60690
|
128 |
(**)end(*struct*);
|