walther@59960: (* Title: Specify/p-model.sml wneuper@59316: Author: Walther Neuper 170207 wneuper@59316: (c) due to copyright terms walther@59959: Walther@60686: This will mostly be dropped at switch to Isabelle/PIDE . wneuper@59316: *) wneuper@59316: walther@59959: signature PRESENTATION_MODEL = wneuper@59316: sig Walther@60605: (* for the OLD P_Model.T *) walther@59969: type T walther@59969: val empty: T walther@59969: val to_string: T -> string walther@59943: walther@59969: datatype item = (*shall be dropped with PIDE*) walther@59969: Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string walther@59969: | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string Walther@60586: type 'a model (*shall be dropped with PIDE*) wneuper@59316: walther@59969: val from : theory -> I_Model.T -> Pre_Conds.T -> T walther@59989: Walther@60586: val to_list: 'a model -> 'a list walther@59989: val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input walther@59989: val mk_additem: string -> TermC.as_string -> Tactic.input Walther@60578: Walther@60578: val item_from_feedback: theory -> I_Model.feedback -> item Walther@60690: (*from isac_test for Minisubpbl*) Walther@60705: 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: Walther@60695: (**) Walther@60578: wenzelm@60223: \<^isac_test>\ Walther@60578: (**) wenzelm@60223: \ wneuper@59316: end wneuper@59316: walther@59968: (**) walther@59959: structure P_Model(**) : PRESENTATION_MODEL(**) = wneuper@59316: struct walther@59968: (**) wneuper@59316: Walther@60690: datatype switch_pbl_met = For_Problem | For_Method Walther@60605: Walther@60605: (** types for OLD presentation**) wneuper@59316: Walther@60586: type 'a model = walther@59969: {Given : 'a list, Where: 'a list, Find : 'a list, With : 'a list, Relate: 'a list}; wneuper@59316: datatype item = walther@59865: Correct of TermC.as_string (* labels a correct formula (type cterm') *) wneuper@59316: | SyntaxE of string (**) wneuper@59316: | TypeE of string (**) walther@59865: | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *) walther@59865: | Incompl of TermC.as_string (**) wneuper@59316: | Superfl of string (**) Walther@60431: | Missing of TermC.as_string; (*REVIEW: a "missing" item is not shown, thus cannot be marked*) walther@59969: Walther@60586: type T = item model; walther@59937: fun item2str (Correct s) = "Correct " ^ s walther@59937: | item2str (SyntaxE s) = "SyntaxE " ^ s walther@59937: | item2str (TypeE s) = "TypeE " ^ s walther@59937: | item2str (False s) = "False " ^ s walther@59937: | item2str (Incompl s) = "Incompl " ^ s walther@59937: | item2str (Superfl s) = "Superfl " ^ s walther@59937: | item2str (Missing s) = "Missing " ^ s; walther@59937: walther@59969: fun to_string ({Given=Given,Where=Where, Walther@60586: Find=Find,With=With,Relate=Relate}:item model)= wneuper@59316: ("{Given =" ^ ((strs2str' o (map item2str)) Given ) ^ wneuper@59316: ",Where=" ^ ((strs2str' o (map item2str)) Where) ^ wneuper@59316: ",Find =" ^ ((strs2str' o (map item2str)) Find ) ^ wneuper@59316: ",With =" ^ ((strs2str' o (map item2str)) With ) ^ wneuper@59316: ",Relate=" ^ ((strs2str' o (map item2str)) Relate) ^ "}"); wneuper@59316: walther@59969: val empty = {Given = [], Where= [], Find = [], With = [], Relate= []}; wneuper@59316: walther@59968: walther@59969: (** build T **) walther@59969: Walther@60745: (*T_TESTold*) Walther@60578: fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) walther@59969: | item_from_feedback _ (I_Model.Syn c) = SyntaxE c walther@59969: | item_from_feedback _ (I_Model.Typ c) = TypeE c Walther@60578: | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) Walther@60578: | item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) Walther@60578: | item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid) walther@59969: | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition" Walther@60745: (*T_TEST* ) Walther@60745: 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: | item_from_feedback_TEST _ (I_Model.Syn_TEST c) = SyntaxE c Walther@60745: | item_from_feedback_TEST thy (I_Model.Inc_TEST ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) Walther@60745: | item_from_feedback_TEST thy (I_Model.Sup_TEST (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))) Walther@60745: ( *T_TESTnew*) walther@59968: walther@59968: fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x = walther@59968: case sel of Walther@60578: "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} walther@59968: | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re} walther@59968: | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re} walther@59968: | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]} Walther@60760: | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*) Walther@60760: | "i_model_empty" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*) walther@59968: | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"") walther@59968: fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh = Walther@60576: {Given = gi, Where = wh, Find= fi , With = wi, Relate = re} walther@59968: Walther@60675: fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term) Walther@60675: | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term); walther@59968: Walther@60586: fun from thy itms where_ = Walther@60757: let Walther@60586: fun coll model [] = model Walther@60586: | coll model ((_, _, _, field, itm_) :: itms) = Walther@60586: coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; walther@59969: val gfr = coll empty itms; Walther@60586: in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end; walther@59968: walther@59989: fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_) walther@59989: | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_) walther@59989: | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_) walther@59989: | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"") walther@59989: fun mk_additem "#Given" ct = Tactic.Add_Given ct walther@59989: | mk_additem "#Find" ct = Tactic.Add_Find ct walther@59989: | mk_additem "#Relate"ct = Tactic.Add_Relation ct walther@59989: | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"") walther@59989: walther@59989: fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} = walther@59989: gis @ whs @ fis @ wis @ res walther@59989: Walther@60690: (**)end(*struct*);