1 (* Title: Specify/p-model.sml
2 Author: Walther Neuper 170207
3 (c) due to copyright terms
5 This will be dropped at switch to Isabelle/PIDE .
8 signature PRESENTATION_MODEL =
10 datatype switch_pbl_met = Model_For_Problem_Ref | Model_For_Method_Ref
13 val template_args: switch_pbl_met -> References.input -> Ctree.ctree ->
14 (switch_pbl_met * model_out) * References.input
16 (* for the OLD P_Model.T *)
19 val to_string: T -> string
21 datatype item = (*shall be dropped with PIDE*)
22 Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string
23 | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string
24 type 'a model (*shall be dropped with PIDE*)
26 val from : theory -> I_Model.T -> Pre_Conds.T -> T
28 val to_list: 'a model -> 'a list
29 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
30 val mk_additem: string -> TermC.as_string -> Tactic.input
32 val item_from_feedback: theory -> I_Model.feedback -> item
40 structure P_Model(**) : PRESENTATION_MODEL(**) =
44 datatype switch_pbl_met = Model_For_Problem_Ref | Model_For_Method_Ref
47 (** for the NEW template for Specification**)
48 datatype feedback = Cor | Inc | Sup | True | False
51 Cor correct: the default representation
52 Inc incomplete list, (accessible) markup to be defined
53 Sup superfluous within the current variant from Formalise.model;
54 (accessible) markup to be defined
55 True the default representation
56 False (accessible) markup to be defined
58 type out_element = UnparseC.term_as_string * feedback
59 type field_out = Model_Pattern.m_field * out_element list
61 field_out (* "#Given", feedback: Cor | Inc | Sup *)
62 * field_out (* "#Where", feedback: True | False *)
63 * field_out (* "#Find", feedback: Cor | Inc | Sup *)
64 * field_out (* "#Relate",feedback: Cor | Inc | Sup *)
66 (*val item_to_out: Proof.context -> I_Model.single -> out_element*)
67 fun item_to_out ctxt (_, _, _, _, I_Model.Cor (dsc_ts, _)) =
68 (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Cor)
69 | item_to_out ctxt (_, _, _, _, I_Model.Inc (dsc_ts, _)) =
70 (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Inc)
71 | item_to_out ctxt ((_, _, _, _, I_Model.Sup dsc_ts): I_Model.single) =
72 (dsc_ts |> Term.list_comb |> UnparseC.term_in_ctxt ctxt, Sup)
73 | item_to_out ctxt im =
74 raise ERROR ("P_Model.item_to_out called with " ^ I_Model.single_to_string ctxt im)
76 (*val items_to_out: Proof.context -> Model_Pattern.m_field -> I_Model.T -> field_out*)
77 fun items_to_out ctxt m_field items =
79 filter (fn (_, _, _, f, _) => f = m_field) items |> map (item_to_out ctxt))
81 (*val where_to_out: Proof.context -> bool * term -> out_element*)
82 fun where_to_out ctxt (bool, t) =
83 (UnparseC.term_in_ctxt ctxt t, if bool then True else False)
85 (*val wheres_to_out: Proof.context -> (bool * term) list -> field_out*)
86 fun wheres_to_out ctxt wheres = ("#Where", map (where_to_out ctxt) wheres)
88 (*val model_to_out: Proof.context -> (bool * term) list -> I_Model.T -> field_out list*)
89 (* the sequence of the template is maitained *)
90 fun model_to_out ctxt where_ model =
92 val given = items_to_out ctxt "#Given" model
93 val where_ = wheres_to_out ctxt where_
94 val find = items_to_out ctxt "#Find" model
95 val relate = items_to_out ctxt "#Relate" model
96 in (given, where_, find, relate) end
98 fun template_args switch_pbl_met input_refs store =
99 if not (Ctree.is_pblnd store) then raise ERROR "update code w.r.t. to future design of Solution"
102 val Ctree.Nd (Ctree.PblObj {origin = (_, o_refs, _), probl, meth, spec, ctxt, ...}, []) = store
103 val (_, pbl_id, met_id) = References.select_input o_refs spec
105 case switch_pbl_met of
106 Model_For_Problem_Ref =>
107 let (* the sequence *)
108 val {where_rls, where_, ...} = Problem.from_store ctxt pbl_id
109 val (_, where_) = Pre_Conds.check ctxt where_rls where_ probl 0
110 in model_to_out ctxt where_ probl end
111 | Model_For_Method_Ref =>
113 val {where_rls, where_ = where_, ...} = MethodC.from_store ctxt met_id
114 val (_, where_) = Pre_Conds.check ctxt where_rls where_ meth 0
115 in model_to_out ctxt where_ meth end
117 ((switch_pbl_met, p_model), input_refs)
120 (** types for OLD presentation**)
123 {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list};
125 Correct of TermC.as_string (* labels a correct formula (type cterm') *)
126 | SyntaxE of string (**)
127 | TypeE of string (**)
128 | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
129 | Incompl of TermC.as_string (**)
130 | Superfl of string (**)
131 | Missing of TermC.as_string; (*REVIEW: a "missing" item is not shown, thus cannot be marked*)
134 fun item2str (Correct s) = "Correct " ^ s
135 | item2str (SyntaxE s) = "SyntaxE " ^ s
136 | item2str (TypeE s) = "TypeE " ^ s
137 | item2str (False s) = "False " ^ s
138 | item2str (Incompl s) = "Incompl " ^ s
139 | item2str (Superfl s) = "Superfl " ^ s
140 | item2str (Missing s) = "Missing " ^ s;
142 fun to_string ({Given=Given,Where=Where,
143 Find=Find,With=With,Relate=Relate}:item model)=
144 ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^
145 ",Where=" ^ ((strs2str' o (map item2str)) Where) ^
146 ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^
147 ",With =" ^ ((strs2str' o (map item2str)) With ) ^
148 ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}");
150 val empty = {Given = [], Where= [], Find = [], With = [], Relate= []};
155 fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
156 | item_from_feedback _ (I_Model.Syn c) = SyntaxE c
157 | item_from_feedback _ (I_Model.Typ c) = TypeE c
158 | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
159 | item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
160 | item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
161 | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
163 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
165 "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re}
166 | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
167 | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
168 | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
169 | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
170 | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
171 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
172 {Given = gi, Where = wh, Find= fi , With = wi, Relate = re}
174 fun boolterm2item ctxt (true, term) = Correct (UnparseC.term_in_ctxt ctxt term)
175 | boolterm2item ctxt(false, term) = False (UnparseC.term_in_ctxt ctxt term);
177 fun from thy itms where_ =
179 fun coll model [] = model
180 | coll model ((_, _, _, field, itm_) :: itms) =
181 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
182 val gfr = coll empty itms;
183 in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end;
185 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
186 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
187 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
188 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
189 fun mk_additem "#Given" ct = Tactic.Add_Given ct
190 | mk_additem "#Find" ct = Tactic.Add_Find ct
191 | mk_additem "#Relate"ct = Tactic.Add_Relation ct
192 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
194 fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
195 gis @ whs @ fis @ wis @ res