1.1 --- a/src/Tools/isac/Specify/calchead.sml Sat May 09 13:15:25 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/calchead.sml Sat May 09 15:31:15 2020 +0200
1.3 @@ -95,9 +95,7 @@
1.4 val match_ags_msg : Problem.id -> term -> term list -> unit
1.5 val oris2fmz_vals : O_Model.T -> string list * term list
1.6 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
1.7 - val is_known : Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list
1.8 - val is_notyet_input : Proof.context -> I_Model.T -> term list -> O_Model.single -> ('a * (term * term)) list
1.9 - -> string * I_Model.single
1.10 +
1.11 val ppc2list : 'a Model.ppc -> 'a list
1.12 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
1.13 val mk_additem: string -> TermC.as_string -> Tactic.input
1.14 @@ -121,10 +119,6 @@
1.15 val matc : theory -> (string * (term * term)) list -> term list -> O_Model.preori list -> O_Model.preori list
1.16 val mtc : theory -> Model_Pattern.single -> term -> O_Model.preori option
1.17 val cpy_nam : Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori
1.18 - datatype additm = Add of I_Model.single | Err of string
1.19 - val appl_add: Proof.context -> string -> O_Model.T ->
1.20 - I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm
1.21 - val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
1.22 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.23
1.24 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
1.25 @@ -195,39 +189,6 @@
1.26 handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)
1.27 in (split_list o (map ori2fmz_vals)) oris end
1.28
1.29 -(* make a term 'typeless' for comparing with another 'typeless' term;
1.30 - 'type-less' usually is illtyped *)
1.31 -fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
1.32 - | typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
1.33 - | typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
1.34 - | typeless (Bound i) = (Bound i)
1.35 - | typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)
1.36 - | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
1.37 -
1.38 -(* to an input (d,ts) find the according ori and insert the ts)
1.39 - WN.11.03: + dont take first inter<>[] *)
1.40 -fun seek_oridts ctxt sel (d, ts) [] =
1.41 - ("seek_oridts: input ('" ^
1.42 - (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
1.43 - (0, [], sel, d, ts),
1.44 - [])
1.45 - | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
1.46 - if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
1.47 - then ("", (id, vat, sel, d, inter op = ts ts'), ts')
1.48 - else seek_oridts ctxt sel (d, ts) oris
1.49 -
1.50 -(* to an input (_,ts) find the according ori and insert the ts *)
1.51 -fun seek_orits ctxt _ ts [] =
1.52 - ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^
1.53 - "') not found in oris (typed)", O_Model.single_empty, [])
1.54 - | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
1.55 - if sel = sel' andalso (inter op = ts ts') <> []
1.56 - then
1.57 - if sel = sel'
1.58 - then ("", (id, vat, sel, d, inter op = ts ts'), ts')
1.59 - else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, [])
1.60 - else seek_orits ctxt sel ts oris
1.61 -
1.62 (* find_first item with #1 equal to id *)
1.63 fun seek_ppc _ [] = NONE
1.64 | seek_ppc id (p :: ppc) = if id = #1 (p: I_Model.single) then SOME p else seek_ppc id ppc
1.65 @@ -393,151 +354,6 @@
1.66 else (Met, Tactic.Apply_Method mI)))
1.67 | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
1.68
1.69 -(* update the itm_ already input, all..from ori *)
1.70 -fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
1.71 - let
1.72 - val ts' = union op = (I_Model.ts_in itm_) ts;
1.73 - val pval = Model.pbl_ids' d ts'
1.74 - (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
1.75 - val complete = if eq_set op = (ts', all) then true else false
1.76 - in
1.77 - case itm_ of
1.78 - (I_Model.Cor _) =>
1.79 - (if fd = "#undef" then (id, vt, complete, fd, I_Model.Sup (d, ts'))
1.80 - else (id, vt, complete, fd, I_Model.Cor ((d, ts'), (pid, pval))))
1.81 - | (I_Model.Syn c) => error ("ori_2itm wants to overwrite " ^ c)
1.82 - | (I_Model.Typ c) => error ("ori_2itm wants to overwrite " ^ c)
1.83 - | (I_Model.Inc _) =>
1.84 - if complete
1.85 - then (id, vt, true, fd, I_Model.Cor ((d, ts'), (pid, pval)))
1.86 - else (id, vt, false, fd, I_Model.Inc ((d, ts'), (pid, pval)))
1.87 - | (I_Model.Sup (d,ts')) => (*4.9.01 lost env*)
1.88 - (*if fd = "#undef" then*) (id,vt,complete,fd,I_Model.Sup(d,ts'))
1.89 - (*else (id,vt,complete,fd,I_Model.Cor((d,ts'),e))*)
1.90 - (* 28.1.00: not completely clear ---^^^ etc.*)
1.91 - | (I_Model.Mis _) => (* 4.9.01: I_Model.Mis just copied *)
1.92 - if complete
1.93 - then (id, vt, true, fd, I_Model.Cor ((d,ts'), (pid, pval)))
1.94 - else (id, vt, false, fd, I_Model.Inc ((d,ts'), (pid, pval)))
1.95 - | i => error ("ori_2itm: uncovered case of "^ I_Model.feedback_to_string' i)
1.96 - end
1.97 -
1.98 -fun eq1 d (_, (d', _)) = (d = d')
1.99 -fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.d_in itm_)
1.100 -
1.101 -(* 'all' ts from ori; ts is the input; (ori carries rest of info)
1.102 - 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
1.103 - pval: value for problem-environment _NOT_ checked for 'inter' --
1.104 - -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
1.105 - (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
1.106 -(*. is_input ori itms <=>
1.107 - EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
1.108 - (2) ori(ts) subset itm(ts) --- Err "already input"
1.109 - (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
1.110 - (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.111 -fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
1.112 - case find_first (eq1 d) pbt of
1.113 - SOME (_, (_, pid)) =>
1.114 - (case find_first (eq3 f d) itms of
1.115 - SOME (_,_,_,_,itm_) =>
1.116 - let val ts' = inter op = (I_Model.ts_in itm_) ts
1.117 - in
1.118 - if subset op = (ts, ts')
1.119 - then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", I_Model.empty) (*2*)
1.120 - else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.121 - end
1.122 - | NONE => ("", ori_2itm (I_Model.Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
1.123 - | NONE => ("", ori_2itm (I_Model.Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
1.124 -
1.125 -fun test_types ctxt (d,ts) =
1.126 - let
1.127 - val opt = (try Input_Descript.join) (d, ts)
1.128 - val msg = case opt of
1.129 - SOME _ => ""
1.130 - | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
1.131 - (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")
1.132 - in msg end
1.133 -
1.134 -(* is the term t input (or taken from fmz) known in oris ?
1.135 - give feedback on all(?) strange input;
1.136 - return _all_ terms already input to this item (e.g. valuesFor a,b) *)
1.137 -fun is_known ctxt sel ori t =
1.138 - let
1.139 - val ots = (distinct o flat o (map #5)) ori
1.140 - val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
1.141 - val (d, ts) = Input_Descript.split t
1.142 - val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
1.143 - in
1.144 - if (subtract op = oids ids) <> []
1.145 - then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, [])
1.146 - else
1.147 - if d = TermC.empty
1.148 - then
1.149 - if not (subset op = (map typeless ts, map typeless ots))
1.150 - then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
1.151 - "' not in example (typeless)", O_Model.single_empty, [])
1.152 - else
1.153 - (case seek_orits ctxt sel ts ori of
1.154 - ("", ori_ as (_,_,_,d,ts), all) =>
1.155 - (case test_types ctxt (d,ts) of
1.156 - "" => ("", ori_, all)
1.157 - | msg => (msg, O_Model.single_empty, []))
1.158 - | (msg, _, _) => (msg, O_Model.single_empty, []))
1.159 - else
1.160 - if member op = (map #4 ori) d
1.161 - then seek_oridts ctxt sel (d, ts) ori
1.162 - else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.163 - end
1.164 -
1.165 -
1.166 -datatype additm =
1.167 - Add of I_Model.single (* return-value of appl_add *)
1.168 -| Err of string (* error-message *)
1.169 -
1.170 -(* add an item to the model; check wrt. oris and pbt.
1.171 - in contrary to oris<>[] below, this part handles user-input
1.172 - extremely acceptive, i.e. accept input instead error-msg *)
1.173 -fun appl_add ctxt sel [] ppc pbt ct =
1.174 - let
1.175 - val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
1.176 - in
1.177 - case TermC.parseNEW ctxt ct of
1.178 - NONE => Add (i, [], false, sel, I_Model.Syn ct)
1.179 - | SOME t =>
1.180 - let val (d, ts) = Input_Descript.split t
1.181 - in
1.182 - if d = TermC.empty
1.183 - then Add (i, [], false, sel, I_Model.Mis (Specify.dsc_unknown, hd ts))
1.184 - else
1.185 - (case find_first (eq1 d) pbt of
1.186 - NONE => Add (i, [], true, sel, I_Model.Sup (d,ts))
1.187 - | SOME (f, (_, id)) =>
1.188 - let fun eq2 d (i, _, _, _, itm_) = d = (I_Model.d_in itm_) andalso i <> 0
1.189 - in case find_first (eq2 d) ppc of
1.190 - NONE => Add (i, [], true, f,I_Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
1.191 - | SOME (i', _, _, _, itm_) =>
1.192 - if Input_Descript.for_list d
1.193 - then
1.194 - let
1.195 - val in_itm = I_Model.ts_in itm_
1.196 - val ts' = union op = ts in_itm
1.197 - val i'' = if in_itm = [] then i else i'
1.198 - in Add (i'', [], true, f, I_Model.Cor ((d, ts'), (id, Model.pbl_ids' d ts')))end
1.199 - else Add (i', [], true, f, I_Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
1.200 - end)
1.201 - end
1.202 - end
1.203 - | appl_add ctxt sel oris ppc pbt str =
1.204 - case TermC.parseNEW ctxt str of
1.205 - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.206 - | SOME t =>
1.207 - case is_known ctxt sel oris t of
1.208 - ("", ori', all) =>
1.209 - (case is_notyet_input ctxt ppc all ori' pbt of
1.210 - ("", itm) => Add itm
1.211 - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.212 - | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
1.213 -
1.214 (* make oris from args of the stac SubProblem and from pbt.
1.215 can this formal argument (of a model-pattern) be omitted in the arg-list
1.216 of a SubProblem ? see calcelems.sml 'type met ' *)
1.217 @@ -690,8 +506,8 @@
1.218 val cmI = if mI = Method.id_empty then mI' else mI
1.219 val {ppc, pre, prls, ...} = Specify.get_met cmI
1.220 in
1.221 - case appl_add ctxt sel oris met ppc ct of
1.222 - Add itm => (*..union old input *)
1.223 + case I_Model.add_single ctxt sel oris met ppc ct of
1.224 + I_Model.Add itm => (*..union old input *)
1.225 let
1.226 val met' = insert_ppc thy itm met
1.227 val arg = case sel of
1.228 @@ -710,7 +526,7 @@
1.229 in
1.230 ("ok", ([], [], (pt', (p, p_))))
1.231 end
1.232 - | Err msg =>
1.233 + | I_Model.Err msg =>
1.234 let
1.235 val pre' = Stool.check_preconds thy prls pre met
1.236 val pb = foldl and_ (true, map fst pre')
1.237 @@ -732,8 +548,8 @@
1.238 val cmI = if mI = Method.id_empty then mI' else mI
1.239 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
1.240 in
1.241 - case appl_add ctxt sel oris pbl ppc ct of
1.242 - Add itm => (*..union old input *)
1.243 + case I_Model.add_single ctxt sel oris pbl ppc ct of
1.244 + I_Model.Add itm => (*..union old input *)
1.245 let
1.246 val pbl' = insert_ppc thy itm pbl
1.247 val arg = case sel of
1.248 @@ -753,7 +569,7 @@
1.249 in
1.250 ("ok", ([], [], (pt', (p, p_))))
1.251 end
1.252 - | Err msg =>
1.253 + | I_Model.Err msg =>
1.254 let
1.255 val pre = Stool.check_preconds thy prls where_ pbl
1.256 val pb = foldl and_ (true, map fst pre)
1.257 @@ -776,8 +592,8 @@
1.258 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.259 val cpI = if pI = Problem.id_empty then pI' else pI;
1.260 in
1.261 - case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
1.262 - Add itm (*..union old input *) =>
1.263 + case I_Model.add_single ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
1.264 + I_Model.Add itm (*..union old input *) =>
1.265 let
1.266 val pbl' = insert_ppc thy itm pbl
1.267 val (tac, tac_) = case sel of
1.268 @@ -792,7 +608,7 @@
1.269 in
1.270 ([(tac, tac_, ((p, Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pbl)))
1.271 end
1.272 - | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.273 + | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.274 FIXME ..and dont abuse a tactic for that purpose*)
1.275 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
1.276 (e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
1.277 @@ -806,8 +622,8 @@
1.278 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.279 val cmI = if mI = Method.id_empty then mI' else mI;
1.280 in
1.281 - case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
1.282 - Add itm (*..union old input *) =>
1.283 + case I_Model.add_single ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
1.284 + I_Model.Add itm (*..union old input *) =>
1.285 let
1.286 val met' = insert_ppc thy itm met;
1.287 val (tac,tac_) = case sel of
1.288 @@ -822,12 +638,12 @@
1.289 in
1.290 ([(tac, tac_, ((p, Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Met)))
1.291 end
1.292 - | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
1.293 + | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
1.294 end
1.295 | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
1.296
1.297 fun ori2Coritm pbt (i, v, f, d, ts) =
1.298 - (i, v, true, f, I_Model.Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts)))
1.299 + (i, v, true, f, I_Model.Cor ((d,ts),((snd o snd o the o (find_first (I_Model.eq1 d))) pbt,ts)))
1.300 handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
1.301 (*dsc in oris, but not in pbl pat list: keep this dsc*)
1.302
2.1 --- a/src/Tools/isac/Specify/i-model.sml Sat May 09 13:15:25 2020 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Sat May 09 15:31:15 2020 +0200
2.3 @@ -19,21 +19,45 @@
2.4 val single_to_string: Proof.context -> single -> string
2.5 val to_string: Proof.context -> T -> string
2.6
2.7 - val untouched : T -> bool
2.8 +(*/------- to I_Model from Chead -------\*)
2.9 + datatype additm = Add of single | Err of string
2.10 +(*val appl_add: m_field -> Proof.context -> O_Model.T -> Model_Pattern.T -> TermC.as_string -> T
2.11 + -> additm*)
2.12 +(*val appl_add: Proof.context -> m_field -> O_Model.T ->
2.13 + T -> Model_Pattern.T -> TermC.as_string -> additm*)
2.14 + val add_single: Proof.context -> m_field -> O_Model.T ->
2.15 + T -> Model_Pattern.T -> TermC.as_string -> additm
2.16 +(*\------- to I_Model from Chead -------/*)
2.17
2.18 - val d_in : feedback -> term
2.19 - val ts_in : feedback -> term list
2.20 - val vars_of : T -> term list
2.21 - val max_vt : T -> int
2.22 - val all_ts_in : feedback list -> term list
2.23 + val untouched: T -> bool
2.24 +
2.25 + val d_in: feedback -> term
2.26 + val ts_in: feedback -> term list
2.27 + val vars_of: T -> term list
2.28 + val max_vt: T -> int
2.29 + val all_ts_in: feedback list -> term list
2.30 val vts_in: T -> int list
2.31
2.32 - val mk_env : T -> (term * term) list
2.33 - val penvval_in : feedback -> term list
2.34 + val mk_env: T -> (term * term) list
2.35 + val penvval_in: feedback -> term list
2.36 +
2.37 +(*/------- to I_Model from Model -------\*)
2.38 + val pbl_ids': term -> term list -> term list
2.39 +(*\------- to I_Model from Model -------/*)
2.40 +
2.41 +(*/------- to I_Model from Chead -------\*)
2.42 + val is_known: Proof.context -> string -> O_Model.T -> term -> string * O_Model.single * term list
2.43 + val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list
2.44 + -> string * single
2.45 + val dsc_unknown: term
2.46 +(*\------- to I_Model from Chead -------/*)
2.47 +
2.48 +
2.49 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.50 - (* NONE *)
2.51 + val dts2str: term * (term list) -> string
2.52 + val eq1: ''a -> 'b * (''a * 'c) -> bool
2.53 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.54 - (* NONE *)
2.55 + val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
2.56 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.57 end
2.58
2.59 @@ -87,7 +111,6 @@
2.60 FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
2.61 fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms);
2.62
2.63 -
2.64 (* find most frequent variant v in itms *)
2.65 fun vts_in itms = (distinct o flat o (map #2)) (itms: T);
2.66
2.67 @@ -141,25 +164,219 @@
2.68
2.69 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
2.70 fun d_in (Cor ((d ,_), _)) = d
2.71 - | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
2.72 - | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
2.73 + | d_in (Syn _) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
2.74 + | d_in (Typ _) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
2.75 | d_in (Inc ((d, _), _)) = d
2.76 | d_in (Sup (d, _)) = d
2.77 | d_in (Mis (d, _)) = d
2.78 | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
2.79
2.80 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
2.81 -(**)
2.82 -fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d,ts)]
2.83 - | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
2.84 - | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
2.85 +fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]
2.86 + | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
2.87 + | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
2.88 | penvval_in (Inc (_, (_, ts))) = ts
2.89 - | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
2.90 - | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
2.91 + | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
2.92 + | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
2.93 pair2str(UnparseC.term d, UnparseC.term t));*) [])
2.94 | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
2.95 -(**)
2.96
2.97 fun vars_of itms = itms |> mk_env |> map snd
2.98
2.99 +
2.100 +(*/------- to I_Model from Chead -------\*)
2.101 +(* to an input (d,ts) find the according ori and insert the ts)
2.102 + WN.11.03: + dont take first inter<>[] *)
2.103 +fun seek_oridts ctxt sel (d, ts) [] =
2.104 + ("seek_oridts: input ('" ^
2.105 + (UnparseC.term_in_ctxt ctxt (Input_Descript.join (d, ts))) ^ "') not found in oris (typed)",
2.106 + (0, [], sel, d, ts),
2.107 + [])
2.108 + | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
2.109 + if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
2.110 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
2.111 + else seek_oridts ctxt sel (d, ts) oris
2.112 +
2.113 +fun test_types ctxt (d,ts) =
2.114 + let
2.115 + val opt = (try Input_Descript.join) (d, ts)
2.116 + val msg = case opt of
2.117 + SOME _ => ""
2.118 + | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
2.119 + (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts ^ " is illtyped")
2.120 + in msg end
2.121 +
2.122 +(* to an input (_,ts) find the according ori and insert the ts *)
2.123 +fun seek_orits ctxt _ ts [] =
2.124 + ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^
2.125 + "') not found in oris (typed)", O_Model.single_empty, [])
2.126 + | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
2.127 + if sel = sel' andalso (inter op = ts ts') <> []
2.128 + then
2.129 + if sel = sel'
2.130 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
2.131 + else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, [])
2.132 + else seek_orits ctxt sel ts oris
2.133 +
2.134 +(* make a term 'typeless' for comparing with another 'typeless' term;
2.135 + 'type-less' usually is illtyped *)
2.136 +fun typeless (Const (s, _)) = (Const (s, TermC.typ_empty))
2.137 + | typeless (Free (s, _)) = (Free (s, TermC.typ_empty))
2.138 + | typeless (Var (n, _)) = (Var (n, TermC.typ_empty))
2.139 + | typeless (Bound i) = (Bound i)
2.140 + | typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, typeless t)
2.141 + | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
2.142 +
2.143 +(* is the term t input (or taken from fmz) known in oris ?
2.144 + give feedback on all(?) strange input;
2.145 + return _all_ terms already input to this item (e.g. valuesFor a,b) *)
2.146 +fun is_known ctxt sel ori t =
2.147 + let
2.148 + val ots = (distinct o flat o (map #5)) ori
2.149 + val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
2.150 + val (d, ts) = Input_Descript.split t
2.151 + val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
2.152 + in
2.153 + if (subtract op = oids ids) <> []
2.154 + then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, [])
2.155 + else
2.156 + if d = TermC.empty
2.157 + then
2.158 + if not (subset op = (map typeless ts, map typeless ots))
2.159 + then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
2.160 + "' not in example (typeless)", O_Model.single_empty, [])
2.161 + else
2.162 + (case seek_orits ctxt sel ts ori of
2.163 + ("", ori_ as (_,_,_,d,ts), all) =>
2.164 + (case test_types ctxt (d,ts) of
2.165 + "" => ("", ori_, all)
2.166 + | msg => (msg, O_Model.single_empty, []))
2.167 + | (msg, _, _) => (msg, O_Model.single_empty, []))
2.168 + else
2.169 + if member op = (map #4 ori) d
2.170 + then seek_oridts ctxt sel (d, ts) ori
2.171 + else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])
2.172 + end
2.173 +(*\------- to I_Model from Chead -------/*)
2.174 +
2.175 +(*/------- to I_Model from Specify -------\*)
2.176 +val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
2.177 +(*\------- to I_Model from Specify -------/*)
2.178 +
2.179 +(*/------- to I_Model from Model -------\*)
2.180 +(* 9.5.03 penv postponed: pbl_ids' *)
2.181 +fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
2.182 +(*\------- to I_Model from Model -------/*)
2.183 +
2.184 +(*/------- to I_Model from Chead -------\*)
2.185 +(* update the itm_ already input, all..from ori *)
2.186 +fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
2.187 + let
2.188 + val ts' = union op = (ts_in itm_) ts;
2.189 + val pval =pbl_ids' d ts'
2.190 + (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
2.191 + val complete = if eq_set op = (ts', all) then true else false
2.192 + in
2.193 + case itm_ of
2.194 + (Cor _) =>
2.195 + (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
2.196 + else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
2.197 + | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
2.198 + | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
2.199 + | (Inc _) =>
2.200 + if complete
2.201 + then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
2.202 + else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
2.203 + | (Sup (d,ts')) => (*4.9.01 lost env*)
2.204 + (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
2.205 + (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
2.206 + (* 28.1.00: not completely clear ---^^^ etc.*)
2.207 + | (Mis _) => (* 4.9.01: Mis just copied *)
2.208 + if complete
2.209 + then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
2.210 + else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
2.211 + | i => error ("ori_2itm: uncovered case of "^ feedback_to_string' i)
2.212 + end
2.213 +
2.214 +fun eq1 d (_, (d', _)) = (d = d')
2.215 +fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
2.216 +
2.217 +(* 'all' ts from ori; ts is the input; (ori carries rest of info)
2.218 + 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
2.219 + pval: value for problem-environment _NOT_ checked for 'inter' --
2.220 + -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
2.221 + (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
2.222 +(*. is_input ori itms <=>
2.223 + EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
2.224 + (2) ori(ts) subset itm(ts) --- Err "already input"
2.225 + (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
2.226 + (4) -"- <> empty --- new: ori(ts) \\ inter .*)
2.227 +fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
2.228 + case find_first (eq1 d) pbt of
2.229 + SOME (_, (_, pid)) =>
2.230 + (case find_first (eq3 f d) itms of
2.231 + SOME (_,_,_,_,itm_) =>
2.232 + let val ts' = inter op = (ts_in itm_) ts
2.233 + in
2.234 + if subset op = (ts, ts')
2.235 + then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", empty) (*2*)
2.236 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
2.237 + end
2.238 + | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
2.239 + | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
2.240 +
2.241 +datatype additm =
2.242 + Add of single (* return-value of add_single *)
2.243 +| Err of string (* error-message *)
2.244 +
2.245 +(*
2.246 + Create feedback for input of TermC.as_string to m_field;
2.247 + check w.r.t. O_Model.T and Model_Pattern.T.
2.248 + In case of O_Model.T = [] (i.e. no data for user-guidance from Formalise.T)
2.249 + add_single is extremely permissive.
2.250 +*)
2.251 +fun add_single ctxt m_field [] i_model m_patt ct =
2.252 + let
2.253 + val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
2.254 + in
2.255 + case TermC.parseNEW ctxt ct of
2.256 + NONE => Add (i, [], false, m_field, Syn ct)
2.257 + | SOME t =>
2.258 + let
2.259 + val (d, ts) = Input_Descript.split t
2.260 + in
2.261 + if d = TermC.empty then
2.262 + Add (i, [], false, m_field, Mis (dsc_unknown, hd ts))
2.263 + else
2.264 + (case find_first (eq1 d) m_patt of
2.265 + NONE => Add (i, [], true, m_field, Sup (d,ts))
2.266 + | SOME (f, (_, id)) =>
2.267 + let
2.268 + fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
2.269 + in
2.270 + case find_first (eq2 d) i_model of
2.271 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
2.272 + | SOME (i', _, _, _, itm_) =>
2.273 + if Input_Descript.for_list d then
2.274 + let
2.275 + val in_itm = ts_in itm_
2.276 + val ts' = union op = ts in_itm
2.277 + val i'' = if in_itm = [] then i else i'
2.278 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
2.279 + else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
2.280 + end)
2.281 + end
2.282 + end
2.283 + | add_single ctxt m_field o_model i_model m_patt str =
2.284 + case TermC.parseNEW ctxt str of
2.285 + NONE => Err ("add_single: syntax error in '" ^ str ^ "'")
2.286 + | SOME t =>
2.287 + case is_known ctxt m_field o_model t of
2.288 + ("", ori', all) =>
2.289 + (case is_notyet_input ctxt i_model all ori' m_patt of
2.290 + ("", itm) => Add itm
2.291 + | (msg, _) => Err ("[error] add_single: is_notyet_input: " ^ msg))
2.292 + | (msg, _, _) => Err ("[error] add_single: is_known: " ^ msg);
2.293 +(*\------- to I_Model from Chead -------/*)
2.294 +
2.295 (**)end(**);
2.296 \ No newline at end of file
3.1 --- a/src/Tools/isac/Specify/input-calchead.sml Sat May 09 13:15:25 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Sat May 09 15:31:15 2020 +0200
3.3 @@ -175,9 +175,9 @@
3.4 case TermC.parseNEW ctxt ct of
3.5 NONE => (0, [], false, sel, I_Model.Syn ct)
3.6 | SOME t =>
3.7 - (case Chead.is_known ctxt sel oris t of
3.8 + (case I_Model.is_known ctxt sel oris t of
3.9 ("", ori', all) =>
3.10 - (case Chead.is_notyet_input ctxt ppc all ori' pbt of
3.11 + (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
3.12 ("",itm) => itm
3.13 | (msg,_) => error ("appl_add': " ^ msg))
3.14 | (_, (i, v, _, d, ts), _) =>
4.1 --- a/src/Tools/isac/Specify/model.sml Sat May 09 13:15:25 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/model.sml Sat May 09 15:31:15 2020 +0200
4.3 @@ -18,7 +18,6 @@
4.4 With: string list} -> string
4.5 val itemppc2str : item ppc -> string
4.6
4.7 - val pbl_ids' : term -> term list -> term list
4.8 val mkval' : term list -> term
4.9
4.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.11 @@ -36,10 +35,10 @@
4.12 (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
4.13 =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
4.14 (1.2) Syn,Typ,Sup: not related to oris
4.15 - Syn, Typ (presently) should be accepted in appl_add (instead Error')
4.16 - Sup (presently) should be accepted in appl_add (instead Error')
4.17 + Syn, Typ (presently) should be accepted in I_Model.add_single (instead Error')
4.18 + Sup (presently) should be accepted in I_Model.add_single (instead Error')
4.19 _could_ be w.r.t current vat (and then _is_ related to vat
4.20 - Mis should _not_ be made Inc ((presently, by appl_add & match_itms)
4.21 + Mis should _not_ be made Inc ((presently, by I_Model.add_single & match_itms)
4.22 - dsc in I_Model.feedback is timeconsuming -- keep id for respective queries ?
4.23 - order of items in ppc should be stable w.r.t order of itms
4.24
4.25 @@ -77,9 +76,6 @@
4.26 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
4.27 fun mkval' x = mkval TermC.empty x;
4.28
4.29 -(* 9.5.03 penv postponed: pbl_ids' *)
4.30 -fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
4.31 -
4.32 (* for _output_ of the items of a Model *)
4.33 datatype item =
4.34 Correct of TermC.as_string (* labels a correct formula (type cterm') *)
5.1 --- a/src/Tools/isac/Specify/ptyps.sml Sat May 09 13:15:25 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/ptyps.sml Sat May 09 15:31:15 2020 +0200
5.3 @@ -33,8 +33,7 @@
5.4 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
5.5 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
5.6 val itm_out : theory -> I_Model.feedback -> string
5.7 - val dsc_unknown : term
5.8 -
5.9 +
5.10 datatype ketype = Exp_ | Met_ | Pbl_ | Thy_
5.11 val ketype2str: ketype -> string
5.12 val ketype2str': ketype -> string
5.13 @@ -142,8 +141,6 @@
5.14
5.15 type field = Model_Pattern.single;
5.16
5.17 -val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
5.18 -
5.19 fun itm_2item (_: theory) (I_Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (Input_Descript.join (d, ts)))
5.20 | itm_2item _ (I_Model.Syn c) = Model.SyntaxE c
5.21 | itm_2item _ (I_Model.Typ c) = Model.TypeE c
5.22 @@ -379,21 +376,21 @@
5.23 for matching a problemtype; returns true only for itms found in pbt *)
5.24 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
5.25 (case find_first (eq1 d) pbt of
5.26 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
5.27 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
5.28 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
5.29 | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
5.30 (case find_first (eq1 d) pbt of
5.31 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))
5.32 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
5.33 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
5.34 | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
5.35 | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
5.36 | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
5.37 (case find_first (eq1 d) pbt of
5.38 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))
5.39 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, I_Model.pbl_ids' d vs)))
5.40 | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
5.41 | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
5.42 (case find_first (eq1 d) pbt of
5.43 - SOME (_, _) => error "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"
5.44 + SOME (_, _) => error "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
5.45 | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
5.46 | chk_ _ _ _ = error "chk_: uncovered fun def.";
5.47
5.48 @@ -475,7 +472,7 @@
5.49 returns true only for itms found in pbt *)
5.50 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
5.51 case find_first (eq1 d) pbt of
5.52 - SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]
5.53 + SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
5.54 | NONE => [];
5.55
5.56 (* elem 'p' of pbt contained in itms ? *)
6.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sat May 09 13:15:25 2020 +0200
6.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat May 09 15:31:15 2020 +0200
6.3 @@ -1255,20 +1255,20 @@
6.4 val iii = appl_adds dI oris ppc pbt (selct::ss);
6.5 tracing(I_Model.to_string thy iii);
6.6
6.7 - val itm = appl_add' dI oris ppc pbt selct;
6.8 + val itm = add_single' dI oris ppc pbt selct;
6.9 val ppc = insert_ppc' itm ppc;
6.10
6.11 val _::selct::ss = (selct::ss);
6.12 - val itm = appl_add' dI oris ppc pbt selct;
6.13 + val itm = add_single' dI oris ppc pbt selct;
6.14 val ppc = insert_ppc' itm ppc;
6.15
6.16 val _::selct::ss = (selct::ss);
6.17 - val itm = appl_add' dI oris ppc pbt selct;
6.18 + val itm = add_single' dI oris ppc pbt selct;
6.19 val ppc = insert_ppc' itm ppc;
6.20 tracing(I_Model.to_string thy ppc);
6.21
6.22 val _::selct::ss = (selct::ss);
6.23 - val itm = appl_add' dI oris ppc pbt selct;
6.24 + val itm = add_single' dI oris ppc pbt selct;
6.25 val ppc = insert_ppc' itm ppc;
6.26 *)
6.27 "--------- fun concat_deriv --------------------------------------";
7.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Sat May 09 13:15:25 2020 +0200
7.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Sat May 09 15:31:15 2020 +0200
7.3 @@ -72,7 +72,7 @@
7.4 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
7.5 val cpI = if pI = Problem.id_empty then pI' else pI;
7.6 val ctxt = get_ctxt pt (p, Pbl);
7.7 -"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
7.8 +"~~~~~ fun add_single, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
7.9 val SOME t = parseNEW ctxt str;
7.10 is_known ctxt sel oris t;
7.11 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
7.12 @@ -84,16 +84,16 @@
7.13 (*if Input_Descript.is_a d then () else error "TODO";*)
7.14 if Input_Descript.is_a d then () else error "TODO";
7.15 "----- these were the errors (call hierarchy from bottom up)";
7.16 -appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
7.17 -Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
7.18 +I_Model.add_single ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
7.19 +Err "[error] add_single: is_known: identifiers [equality] not in example"*)
7.20 nxt_specif_additem "#Given" ct ptp;(*WAS
7.21 -Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
7.22 +Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
7.23 Step_Specify.by_tactic_input tac ptp;(*WAS
7.24 -Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
7.25 +Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
7.26 nxt_specify_ (pt,ip); (*WAS
7.27 -Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
7.28 +Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
7.29 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
7.30 -Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
7.31 +Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
7.32 ========== inhibit exn AK110725 ================================================*)
7.33
7.34 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";