1 (* Title: Specify/p-model.sml
2 Author: Walther Neuper 170207
3 (c) due to copyright terms
5 This will mostly be dropped at switch to Isabelle/PIDE .
8 signature PRESENTATION_MODEL =
10 (* for the OLD P_Model.T *)
13 val to_string: T -> string
15 datatype item = (*shall be dropped with PIDE*)
16 Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string
17 | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string
18 type 'a model (*shall be dropped with PIDE*)
20 val from: theory -> I_Model.T_POS -> Pre_Conds.T ->
21 {Find: item list, Given: item list, Relate: item list, Where: item list, With: item list}
23 val to_list: 'a model -> 'a list
24 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
25 val mk_additem: string -> TermC.as_string -> Tactic.input
27 val item_from_feedback: theory -> I_Model.feedback -> item
28 (*from isac_test for Minisubpbl*)
29 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}
39 structure P_Model(**) : PRESENTATION_MODEL(**) =
43 datatype switch_pbl_met = For_Problem | For_Method
45 (** types for OLD presentation**)
48 {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
50 Correct of TermC.as_string (* labels a correct formula (type cterm') *)
51 | SyntaxE of string (**)
52 | TypeE of string (**)
53 | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
54 | Incompl of TermC.as_string (**)
55 | Superfl of string (**)
56 | Missing of TermC.as_string; (*REVIEW: a "missing" item is not shown, thus cannot be marked*)
59 fun item2str (Correct s) = "Correct " ^ s
60 | item2str (SyntaxE s) = "SyntaxE " ^ s
61 | item2str (TypeE s) = "TypeE " ^ s
62 | item2str (False s) = "False " ^ s
63 | item2str (Incompl s) = "Incompl " ^ s
64 | item2str (Superfl s) = "Superfl " ^ s
65 | item2str (Missing s) = "Missing " ^ s;
67 fun to_string ({Given=Given,Where=Where,
68 Find=Find,With=With,Relate=Relate}:item model)=
69 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
70 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
71 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
72 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
73 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
75 val empty = {Given = [], Where= [], Find = [], With = [], Relate= []};
80 fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
81 | item_from_feedback _ (I_Model.Syn c) = SyntaxE c
82 | item_from_feedback _ (I_Model.Typ c) = TypeE c
83 | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
84 | item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
85 | item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
86 | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
87 fun item_from_feedback_POS thy (I_Model.Cor_POS ((d, ts))) =
88 Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
89 | item_from_feedback_POS _ (I_Model.Syn_POS c) = SyntaxE c
90 | item_from_feedback_POS thy (I_Model.Inc_POS ((d, ts))) =
91 Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
92 | item_from_feedback_POS thy (I_Model.Sup_POS (d, ts)) =
93 Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
95 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
97 "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re}
98 | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
99 | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
100 | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
101 | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
102 | "i_model_empty" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
103 | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
104 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
105 {Given = gi, Where = wh, Find= fi , With = wi, Relate = re}
107 fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term)
108 | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);
110 fun from thy i_model where_ =
112 fun coll model [] = model
113 | coll model ((_, _, _, field, (feedb, _)) :: itms) =
114 coll (add_sel_ppc thy field model (item_from_feedback_POS thy feedb)) itms;
115 val gfr = coll empty i_model;
116 in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end;
118 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
119 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
120 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
121 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
122 fun mk_additem "#Given" ct = Tactic.Add_Given ct
123 | mk_additem "#Find" ct = Tactic.Add_Find ct
124 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
125 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
127 fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
128 gis @ whs @ fis @ wis @ res