1.1 --- a/src/Tools/isac/Specify/p-spec.sml Tue Dec 05 18:15:45 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/p-spec.sml Thu Dec 07 11:54:42 2023 +0100
1.3 @@ -10,29 +10,23 @@
1.4 sig
1.5 type record
1.6 (*/------- rename -------\*)
1.7 - datatype iitem =
1.8 + datatype p_model =
1.9 Find of TermC.as_string list
1.10 | Given of TermC.as_string list
1.11 | Relate of TermC.as_string list
1.12 - type imodel = iitem list
1.13 - type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
1.14 - val empty: icalhd
1.15 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
1.16 -(*/----- from isac_test for Minisubpbl*)
1.17 - val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.18 - string * TermC.as_string -> I_Model.single
1.19 - val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
1.20 - (Model_Def.m_field * TermC.as_string) list -> I_Model.T
1.21 +
1.22 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
1.23 + string * TermC.as_string -> I_Model.single_POS
1.24 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
1.25 + (Model_Def.m_field * TermC.as_string) list -> I_Model.T_POS
1.26 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
1.27 - val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
1.28 - int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
1.29 - val imodel2fstr: iitem list -> (string * TermC.as_string) list
1.30 + val fstr2itm_: theory -> Model_Pattern.T -> Model_Def.m_field * string ->
1.31 + int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
1.32 + val imodel2fstr: p_model list -> (string * TermC.as_string) list
1.33 val is_e_ts: term list -> bool
1.34 val itms2fstr: Proof.context -> I_Model.single -> string * string
1.35 val par2fstr: I_Model.single -> string * TermC.as_string
1.36 - val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T*)
1.37 - (''a * string) list ->
1.38 - (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T*)
1.39 + val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T_POS
1.40 (*\----- from isac_test for Minisubpbl*)
1.41
1.42 \<^isac_test>\<open>
1.43 @@ -55,45 +49,34 @@
1.44
1.45 (** handle an input P_Specific'action **)
1.46
1.47 -datatype iitem =
1.48 +datatype p_model =
1.49 Given of TermC.as_string list
1.50 (*Where is still not input*)
1.51 | Find of TermC.as_string list
1.52 | Relate of TermC.as_string list
1.53
1.54 -type imodel = iitem list
1.55 -
1.56 -type icalhd =
1.57 - Pos.pos' * (* the position in Ctree *)
1.58 - TermC.as_string * (* the headline shown on Calc.T *)
1.59 - imodel * (* the model *)
1.60 - Pos.pos_ * (* model belongs to Problem or MethodC *)
1.61 - References.T; (* into Know_Store *)
1.62 -val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
1.63 -
1.64 fun is_e_ts [] = true
1.65 | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
1.66 | is_e_ts _ = false;
1.67
1.68 -(* WN.9.11.03 copied from fun appl_add *)
1.69 -fun appl_add' dI oris model pbt (sel, ct) =
1.70 +fun appl_add' dI oris (model: I_Model.T_POS) pbt (sel, ct) =
1.71 let
1.72 val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
1.73 in
1.74 (*/------------ replace by ParseC.term_position ------------------\*)
1.75 case ParseC.term_opt ctxt ct of
1.76 (*\------------ replace by ParseC.term_position ------------------/*)
1.77 - NONE => (0, [], false, sel, I_Model.Syn ct)
1.78 + NONE => (0, [], false, sel, (I_Model.Syn_POS ct, Position.none))
1.79 | SOME t =>
1.80 (case O_Model.contains ctxt sel oris t of
1.81 ("", ori', all) =>
1.82 - (case I_Model.is_notyet_input ctxt (I_Model.OLD_to_POS model) all ori' pbt of
1.83 - ("", itm) => I_Model.TEST_to_OLD_single itm
1.84 - | (msg,_) => raise ERROR ("appl_add': " ^ msg))
1.85 + (case I_Model.is_notyet_input ctxt model all ori' pbt of
1.86 + ("", itm) => itm
1.87 + | (msg,_) => raise ERROR ("P_Spec.appl_add': " ^ msg))
1.88 | (_, (i, v, _, d, ts), _) =>
1.89 if is_e_ts ts
1.90 - then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
1.91 - else (i, v, false, sel, I_Model.Sup (d, ts)))
1.92 + then (i, v, false, sel, (I_Model.Inc_POS (d, ts), Position.none))
1.93 + else (i, v, false, sel, (I_Model.Sup_POS (d, ts), Position.none)))
1.94 end
1.95
1.96 (* generate preliminary itm_ from a string (with field "#Given" etc.) *)
1.97 @@ -105,15 +88,15 @@
1.98 (*\------------ replace by ParseC.term_position ? ------------/*)
1.99 in
1.100 case topt of
1.101 - NONE => ([], false, f, I_Model.Syn str)
1.102 + NONE => ([], false, f, (I_Model.Syn_POS str, Position.none))
1.103 | SOME ct =>
1.104 let
1.105 val (d, ts) = Input_Descript.split ct
1.106 val popt = find_first (eq7 (f, d)) pbt
1.107 in
1.108 case popt of
1.109 - NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
1.110 - | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
1.111 + NONE => ([1](*??*), true(*??*), f, (I_Model.Sup_POS (d, ts), Position.none))
1.112 + | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor_POS (d, ts), Position.none))
1.113 end
1.114 end
1.115
1.116 @@ -121,18 +104,17 @@
1.117 fun unknown_expl dI pbt selcts =
1.118 let
1.119 val thy = Know_Store.get_via_last_thy dI
1.120 - val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
1.121 + val its_ = map (fstr2itm_ thy pbt) selcts
1.122 val its = O_Model.add_enumerate its_
1.123 in map flattup2 its end
1.124
1.125 -fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) =
1.126 - (I_Model.descriptor itm_ = I_Model.descriptor iitm_)
1.127 -(* handles superfluous items carelessly *)
1.128 -fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.129 +fun eq_dsc ((_, _, _, _, (itm_, _)), (_, _, _, _, (iitm_, _))) =
1.130 + (I_Model.descriptor_POS itm_ = I_Model.descriptor_POS iitm_)
1.131 +fun add itm (itms: I_Model.T_POS) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.132 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
1.133 (*already present itms in model are being overwritten*)
1.134 - | appl_adds _ _ model _ [] = model
1.135 - | appl_adds dI oris model pbt (selct :: ss) =
1.136 + | appl_adds _ _ (model: I_Model.T_POS) _ [] = model
1.137 + | appl_adds dI oris (model: I_Model.T_POS) pbt (selct :: ss) =
1.138 let val itm = appl_add' dI oris model pbt selct;
1.139 in appl_adds dI oris (add itm model) pbt ss end
1.140
1.141 @@ -156,72 +138,5 @@
1.142 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
1.143 in xxx [] iitems end;
1.144
1.145 -(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
1.146 -fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
1.147 - let
1.148 - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
1.149 - Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.150 - spec = sspec as (sdI, spI, smI), probl, meth, ...}
1.151 - => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
1.152 - | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
1.153 - val thy = Know_Store.get_via_last_thy dI
1.154 - val ctxt = Proof_Context.init_global thy
1.155 - in if CAS_Cmd.is_from hdf fmz
1.156 - then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the))
1.157 - else
1.158 - let val (pos_, pits, mits) =
1.159 - if dI <> sdI
1.160 - then let (* eliminated for PIDE turn 11: take Position into I_Model
1.161 - val its = map (parsitm thy) probl;
1.162 - val (its, trms) = filter_sep is_Par its;*)
1.163 - val pbt = (#model o Problem.from_store ctxt)
1.164 - (#2 (References.select_input ospec sspec))
1.165 - in (Pos.Pbl, appl_adds dI oris [](*its*) pbt (map par2fstr [](*trms*)), meth) end
1.166 - else
1.167 - if pI <> spI
1.168 - then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
1.169 - else let
1.170 - val pbt = (#model o Problem.from_store ctxt) pI
1.171 - val dI' = #1 (References.select_input ospec spec)
1.172 - val oris =
1.173 - if pI = #2 ospec then oris
1.174 - else O_Model.init thy fmz_ pbt |> #1;
1.175 - in (Pos.Pbl, appl_adds dI' oris probl pbt
1.176 - (map (itms2fstr ctxt) probl), meth) end
1.177 - else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.178 - then let
1.179 - val (_, mits) = I_Model.s_make_complete ctxt oris
1.180 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)
1.181 - in if foldl and_ (true, map #3 mits)
1.182 - then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
1.183 - else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
1.184 - end
1.185 - else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
1.186 - ((#model o Problem.from_store ctxt)
1.187 - (#2 (References.select_input ospec spec)))
1.188 - (imodel2fstr imodel), meth)
1.189 - val pt = Ctree.update_spec pt p spec;
1.190 - in if pos_ = Pos.Pbl
1.191 - then
1.192 - let
1.193 - val {where_rls, where_, model, ...} = Problem.from_store ctxt
1.194 - (#2 (References.select_input ospec spec))
1.195 - val (_, where_) = Pre_Conds.check ctxt where_rls where_
1.196 - (model, I_Model.OLD_to_POS pits)
1.197 - in (Ctree.update_pbl pt p pits,
1.198 - (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec))
1.199 - end
1.200 - else
1.201 - let
1.202 - val {where_rls,where_, model, ...} = MethodC.from_store ctxt
1.203 - (#3 (References.select_input ospec spec))
1.204 - val (_, where_) = Pre_Conds.check ctxt where_rls where_
1.205 - (model, I_Model.OLD_to_POS mits)
1.206 - in (Ctree.update_met pt p mits,
1.207 - (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
1.208 - end
1.209 - end
1.210 - end
1.211 - | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
1.212
1.213 (**)end (**)