1.1 --- a/src/Tools/isac/Specify/p-spec.sml Sat Feb 04 11:21:56 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/p-spec.sml Sat Feb 04 16:20:45 2023 +0100
1.3 @@ -29,7 +29,7 @@
1.4 val imodel2fstr: iitem list -> (string * TermC.as_string) list
1.5 val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
1.6 val is_e_ts: term list -> bool
1.7 - val itms2fstr: I_Model.single -> string * string
1.8 + val itms2fstr: Proof.context -> I_Model.single -> string * string
1.9 val par2fstr: I_Model.single -> string * TermC.as_string
1.10 val parsitm: theory -> I_Model.single -> I_Model.single
1.11 val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
1.12 @@ -70,52 +70,52 @@
1.13 val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
1.14
1.15 (* re-parse itms with a new thy and prepare for checking with ori list *)
1.16 -fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
1.17 +fun parsitm thy (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
1.18 (case \<^try>\<open>
1.19 let val t = Input_Descript.join (d, ts)
1.20 - val _ = (UnparseC.term_in_thy dI t)
1.21 + val _ = (UnparseC.term_in_thy thy t)
1.22 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
1.23 in itm end\<close> of
1.24 SOME x => x
1.25 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
1.26 - | parsitm dI (i, v, b, f, I_Model.Syn str) =
1.27 + | parsitm _ (i, v, b, f, I_Model.Syn str) =
1.28 (case \<^try>\<open>
1.29 let val _ = Syntax.read_term\<^context> str
1.30 in (i, v, b ,f, I_Model.Par str) end\<close> of
1.31 SOME x => x
1.32 | NONE => (i, v, b, f, I_Model.Syn str))
1.33 - | parsitm dI (i, v, b, f, I_Model.Typ str) =
1.34 + | parsitm _ (i, v, b, f, I_Model.Typ str) =
1.35 (case \<^try>\<open>
1.36 let val _ = Syntax.read_term\<^context> str
1.37 in (i, v, b, f, I_Model.Par str) end\<close> of
1.38 SOME x => x
1.39 | NONE => (i, v, b, f, I_Model.Syn str))
1.40 - | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
1.41 + | parsitm thy (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
1.42 (case \<^try>\<open>
1.43 let val t = Input_Descript.join (d,ts);
1.44 - val _ = UnparseC.term_in_thy dI t;
1.45 + val _ = UnparseC.term_in_thy thy t;
1.46 (*this ^ should raise the exn on unability of re-parsing dts*)
1.47 in itm end\<close> of
1.48 SOME x => x
1.49 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
1.50 - | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
1.51 + | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
1.52 (case \<^try>\<open>
1.53 let val t = Input_Descript.join (d,ts);
1.54 - val _ = UnparseC.term_in_thy dI t;
1.55 + val _ = UnparseC.term_in_thy thy t;
1.56 (*this ^ should raise the exn on unability of re-parsing dts*)
1.57 in itm end\<close> of
1.58 SOME x => x
1.59 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
1.60 - | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
1.61 + | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
1.62 (case \<^try>\<open>
1.63 let val t = d $ t';
1.64 - val _ = UnparseC.term_in_thy dI t;
1.65 + val _ = UnparseC.term_in_thy thy t;
1.66 (*this ^ should raise the exn on unability of re-parsing dts*)
1.67 in itm end\<close> of
1.68 SOME x => x
1.69 | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
1.70 - | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
1.71 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global dI) itm ^
1.72 + | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) =
1.73 + raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^
1.74 "): Par should be internal");
1.75
1.76 (*separate a list to a pair of elements that do NOT satisfy the predicate,
1.77 @@ -199,14 +199,14 @@
1.78
1.79 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
1.80 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
1.81 -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.82 - | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
1.83 - | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
1.84 - | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
1.85 - | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
1.86 - | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
1.87 - | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
1.88 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
1.89 +fun itms2fstr _ (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
1.90 + | itms2fstr _ (_, _, _, f, I_Model.Syn str) = (f, str)
1.91 + | itms2fstr _ (_, _, _, f, I_Model.Typ str) = (f, str)
1.92 + | itms2fstr _ (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
1.93 + | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
1.94 + | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term_in_ctxt ctxt (d $ t))
1.95 + | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) =
1.96 + raise ERROR ("parsitm (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
1.97
1.98 fun imodel2fstr iitems =
1.99 let
1.100 @@ -221,57 +221,57 @@
1.101 let
1.102 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
1.103 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.104 - spec = sspec as (sdI, spI, smI), probl, meth, ...}
1.105 + spec = sspec as (sdI, spI, smI), probl, meth, ctxt, ...}
1.106 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
1.107 | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
1.108 val thy = Know_Store.get_via_last_thy dI
1.109 -(** ) val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)( **)
1.110 + val ctxt = Proof_Context.init_global thy
1.111 in if CAS_Cmd.is_from hdf fmz
1.112 - then the (CAS_Cmd.input (ParseC.term_opt (Proof_Context.init_global thy) hdf |> the))
1.113 + then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the))
1.114 else
1.115 let val (pos_, pits, mits) =
1.116 if dI <> sdI
1.117 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
1.118 val (its, trms) = filter_sep is_Par its;
1.119 - val pbt = (#model o Problem.from_store (Proof_Context.init_global thy))
1.120 + val pbt = (#model o Problem.from_store ctxt)
1.121 (#2 (References.select_input ospec sspec))
1.122 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.123 else
1.124 if pI <> spI
1.125 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
1.126 else
1.127 - let val pbt = (#model o Problem.from_store (Proof_Context.init_global thy)) pI
1.128 + let val pbt = (#model o Problem.from_store ctxt) pI
1.129 val dI' = #1 (References.select_input ospec spec)
1.130 val oris =
1.131 if pI = #2 ospec then oris
1.132 else O_Model.init thy fmz_ pbt |> #1;
1.133 in (Pos.Pbl, appl_adds dI' oris probl pbt
1.134 - (map itms2fstr probl), meth) end
1.135 + (map (itms2fstr ctxt) probl), meth) end
1.136 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.137 - then let val met = (#model o MethodC.from_store (Proof_Context.init_global thy)) mI
1.138 + then let val met = (#model o MethodC.from_store ctxt) mI
1.139 val mits = I_Model.complete oris probl meth met
1.140 in if foldl and_ (true, map #3 mits)
1.141 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
1.142 end
1.143 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
1.144 - ((#model o Problem.from_store (Proof_Context.init_global thy))
1.145 + ((#model o Problem.from_store ctxt)
1.146 (#2 (References.select_input ospec spec)))
1.147 (imodel2fstr imodel), meth)
1.148 val pt = Ctree.update_spec pt p spec;
1.149 in if pos_ = Pos.Pbl
1.150 then
1.151 let
1.152 - val {where_rls, where_,...} = Problem.from_store (Proof_Context.init_global thy)
1.153 + val {where_rls, where_,...} = Problem.from_store ctxt
1.154 (#2 (References.select_input ospec spec))
1.155 - val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ pits 0
1.156 + val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
1.157 in (Ctree.update_pbl pt p pits,
1.158 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec))
1.159 end
1.160 else
1.161 let
1.162 - val {where_rls,where_,...} = MethodC.from_store (Proof_Context.init_global thy)
1.163 + val {where_rls,where_,...} = MethodC.from_store ctxt
1.164 (#3 (References.select_input ospec spec))
1.165 - val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ mits 0
1.166 + val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
1.167 in (Ctree.update_met pt p mits,
1.168 (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
1.169 end