1.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Dec 11 16:18:42 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/p-spec.sml Mon Dec 11 17:26:30 2023 +0100
1.3 @@ -3,7 +3,7 @@
1.4 (c) due to copyright terms
1.5
1.6 Major parts will be dropped at switch to Isabelle/PIDE.
1.7 -Thus the switch to I_Model.T_POS is prepared quick and dirty.
1.8 +Thus the switch to I_Model.T is prepared quick and dirty.
1.9 *)
1.10
1.11 signature PRESENTATION_SPECIFICATION =
1.12 @@ -15,18 +15,18 @@
1.13 | Given of TermC.as_string list
1.14 | Relate of TermC.as_string list
1.15
1.16 - val appl_add': ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
1.17 - string * TermC.as_string -> I_Model.single_POS
1.18 - val appl_adds: ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
1.19 - (Model_Def.m_field * TermC.as_string) list -> I_Model.T_POS
1.20 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.21 + string * TermC.as_string -> I_Model.single
1.22 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.23 + (Model_Def.m_field * TermC.as_string) list -> I_Model.T
1.24 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
1.25 val fstr2itm_: theory -> Model_Pattern.T -> Model_Def.m_field * string ->
1.26 - int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
1.27 + int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)
1.28 val imodel2fstr: p_model list -> (string * TermC.as_string) list
1.29 val is_e_ts: term list -> bool
1.30 - val itms2fstr: Proof.context -> I_Model.single_POS -> string * string
1.31 - val par2fstr: I_Model.single_POS -> string * TermC.as_string
1.32 - val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T_POS
1.33 + val itms2fstr: Proof.context -> I_Model.single -> string * string
1.34 + val par2fstr: I_Model.single -> string * TermC.as_string
1.35 + val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T
1.36 (*\----- from isac_test for Minisubpbl*)
1.37
1.38 \<^isac_test>\<open>
1.39 @@ -59,14 +59,14 @@
1.40 | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
1.41 | is_e_ts _ = false;
1.42
1.43 -fun appl_add' dI oris (model: I_Model.T_POS) pbt (sel, ct) =
1.44 +fun appl_add' dI oris (model: I_Model.T) pbt (sel, ct) =
1.45 let
1.46 val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
1.47 in
1.48 (*/------------ replace by ParseC.term_position ------------------\*)
1.49 case ParseC.term_opt ctxt ct of
1.50 (*\------------ replace by ParseC.term_position ------------------/*)
1.51 - NONE => (0, [], false, sel, (I_Model.Syn_POS ct, Position.none))
1.52 + NONE => (0, [], false, sel, (I_Model.Syn ct, Position.none))
1.53 | SOME t =>
1.54 (case O_Model.contains ctxt sel oris t of
1.55 ("", ori', all) =>
1.56 @@ -75,8 +75,8 @@
1.57 | (msg,_) => raise ERROR ("P_Spec.appl_add': " ^ msg))
1.58 | (_, (i, v, _, d, ts), _) =>
1.59 if is_e_ts ts
1.60 - then (i, v, false, sel, (I_Model.Inc_POS (d, ts), Position.none))
1.61 - else (i, v, false, sel, (I_Model.Sup_POS (d, ts), Position.none)))
1.62 + then (i, v, false, sel, (I_Model.Inc (d, ts), Position.none))
1.63 + else (i, v, false, sel, (I_Model.Sup (d, ts), Position.none)))
1.64 end
1.65
1.66 (* generate preliminary itm_ from a string (with field "#Given" etc.) *)
1.67 @@ -88,15 +88,15 @@
1.68 (*\------------ replace by ParseC.term_position ? ------------/*)
1.69 in
1.70 case topt of
1.71 - NONE => ([], false, f, (I_Model.Syn_POS str, Position.none))
1.72 + NONE => ([], false, f, (I_Model.Syn str, Position.none))
1.73 | SOME ct =>
1.74 let
1.75 val (d, ts) = Input_Descript.split ct
1.76 val popt = find_first (eq7 (f, d)) pbt
1.77 in
1.78 case popt of
1.79 - NONE => ([1](*??*), true(*??*), f, (I_Model.Sup_POS (d, ts), Position.none))
1.80 - | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor_POS (d, ts), Position.none))
1.81 + NONE => ([1](*??*), true(*??*), f, (I_Model.Sup (d, ts), Position.none))
1.82 + | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor (d, ts), Position.none))
1.83 end
1.84 end
1.85
1.86 @@ -109,23 +109,23 @@
1.87 in map flattup2 its end
1.88
1.89 fun eq_dsc ((_, _, _, _, (itm_, _)), (_, _, _, _, (iitm_, _))) =
1.90 - (I_Model.descriptor_POS itm_ = I_Model.descriptor_POS iitm_)
1.91 -fun add itm (itms: I_Model.T_POS) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.92 + (I_Model.descriptor itm_ = I_Model.descriptor iitm_)
1.93 +fun add itm (itms: I_Model.T) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.94 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
1.95 (*already present itms in model are being overwritten*)
1.96 - | appl_adds _ _ (model: I_Model.T_POS) _ [] = model
1.97 - | appl_adds dI oris (model: I_Model.T_POS) pbt (selct :: ss) =
1.98 + | appl_adds _ _ (model: I_Model.T) _ [] = model
1.99 + | appl_adds dI oris (model: I_Model.T) pbt (selct :: ss) =
1.100 let val itm = appl_add' dI oris model pbt selct;
1.101 in appl_adds dI oris (add itm model) pbt ss end
1.102
1.103 -fun par2fstr (_, _, _, f, (I_Model.Syn_POS s, _)) = (f, s)
1.104 +fun par2fstr (_, _, _, f, (I_Model.Syn s, _)) = (f, s)
1.105 | par2fstr itm = raise ERROR ("par2fstr: called with " ^
1.106 - I_Model.single_to_string_POS (ContextC.for_ERROR ()) itm)
1.107 + I_Model.single_to_string (ContextC.for_ERROR ()) itm)
1.108
1.109 -fun itms2fstr _ (_, _, _, f, (I_Model.Cor_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.110 - | itms2fstr _ (_, _, _, f, (I_Model.Syn_POS str, _)) = (f, str)
1.111 - | itms2fstr _ (_, _, _, f, (I_Model.Inc_POS (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
1.112 - | itms2fstr _ (_, _, _, f, (I_Model.Sup_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.113 +fun itms2fstr _ (_, _, _, f, (I_Model.Cor (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.114 + | itms2fstr _ (_, _, _, f, (I_Model.Syn str, _)) = (f, str)
1.115 + | itms2fstr _ (_, _, _, f, (I_Model.Inc (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
1.116 + | itms2fstr _ (_, _, _, f, (I_Model.Sup (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.117
1.118 fun imodel2fstr iitems =
1.119 let