# HG changeset patch # User Walther Neuper # Date 1588678403 -7200 # Node ID d6261de56fb0494c9ddc87a5163e0c9f7921d230 # Parent 602bf61dc6df521574fd29a3e6f9b7889b141589 assign code struct.O_Model and I_Model, part 1 diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/BridgeLibisabelle/datatypes.sml --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 13:33:23 2020 +0200 @@ -345,16 +345,16 @@ in filt end; fun xml_of_itm_ (Model.Cor (dts, _)) = - XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Model.comp_dts' dts)]) + XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (I_Model.comp_dts' dts)]) | xml_of_itm_ (Model.Syn c) = XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c]) | xml_of_itm_ (Model.Typ c) = XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c]) (*type item also has 'False of cterm' set in preconds2xml WN 050618*) | xml_of_itm_ (Model.Inc (dts, _)) = - XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Model.comp_dts' dts)]) + XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (I_Model.comp_dts' dts)]) | xml_of_itm_ (Model.Sup dts) = - XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Model.comp_dts' dts)]) + XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (I_Model.comp_dts' dts)]) | xml_of_itm_ (Model.Mis (d, pid)) = XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)]) | xml_of_itm_ _ = error "xml_of_itm_: wrong argument" diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue May 05 13:33:23 2020 +0200 @@ -54,7 +54,7 @@ (* *) val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)." fun error_msg_2 d itms = ("arguments_from_model: '" ^ UnparseC.term d ^ "' not in itms:\n" ^ - "itms:\n" ^ Model.itms2str_ @{context} itms) + "itms:\n" ^ I_Model.to_string @{context} itms) (* turn model-items into arguments for a program *) fun arguments_from_model mI itms = let diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/MathEngBasic/model-def.sml --- a/src/Tools/isac/MathEngBasic/model-def.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Tue May 05 13:33:23 2020 +0200 @@ -33,7 +33,7 @@ | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string (* itm*) type i_model_single -(*\ form_T*) +(* itm list*) type i_model (* e_itm*) val i_model_empty : i_model_single diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/calchead.sml --- a/src/Tools/isac/Specify/calchead.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200 @@ -118,9 +118,9 @@ val is_copy_named_generating : 'a * ('b * term) -> bool val is_copy_named : 'a * ('b * term) -> bool val ori2Coritm : Celem4.pat list -> O_Model.single -> I_Model.single - val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list - val mtc : theory -> Celem4.pat -> term -> Model.preori option - val cpy_nam : Celem4.pat list -> Model.preori list -> Celem4.pat -> Model.preori + val matc : theory -> (string * (term * term)) list -> term list -> O_Model.preori list -> O_Model.preori list + val mtc : theory -> Celem4.pat -> term -> O_Model.preori option + val cpy_nam : Celem4.pat list -> O_Model.preori list -> Celem4.pat -> O_Model.preori datatype additm = Add of I_Model.single | Err of string val appl_add: Proof.context -> string -> O_Model.T -> I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm @@ -191,7 +191,7 @@ --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *) fun oris2fmz_vals oris = let fun ori2fmz_vals (_, _, _, dsc, ts) = - ((UnparseC.term o Model.comp_dts') (dsc, ts), last_elem ts) + ((UnparseC.term o I_Model.comp_dts') (dsc, ts), last_elem ts) handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts) in (split_list o (map ori2fmz_vals)) oris end @@ -208,7 +208,7 @@ WN.11.03: + dont take first inter<>[] *) fun seek_oridts ctxt sel (d, ts) [] = ("seek_oridts: input ('" ^ - (UnparseC.term_in_ctxt ctxt (Model.comp_dts (d, ts))) ^ "') not found in oris (typed)", + (UnparseC.term_in_ctxt ctxt (I_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)", (0, [], sel, d, ts), []) | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) = @@ -219,13 +219,13 @@ (* to an input (_,ts) find the according ori and insert the ts *) fun seek_orits ctxt _ ts [] = ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^ - "') not found in oris (typed)", Model.e_ori, []) + "') not found in oris (typed)", O_Model.single_empty, []) | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) = if sel = sel' andalso (inter op = ts ts') <> [] then if sel = sel' then ("", (id, vat, sel, d, inter op = ts ts'), ts') - else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, Model.e_ori, []) + else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, []) else seek_orits ctxt sel ts oris (* find_first item with #1 equal to id *) @@ -268,7 +268,7 @@ | d_in (Model.Inc ((d,_),_)) = [d] | d_in (Model.Sup (d,_)) = [d] | d_in (Model.Mis (d,_)) = [d] - | d_in i = error ("all_dsc_in: uncovered case with " ^ Model.itm_2str i) + | d_in i = error ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i) in (flat o (map d_in)) itm_s end; fun is_error (Model.Cor _) = false @@ -279,13 +279,13 @@ (* get the first term in ts from ori *) fun getr_ct thy (_, _, fd, d, ts) = - (fd, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d,[hd ts])) + (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d,[hd ts])) (* get a term from ori, notyet input in itm. the term from ori is thrown back to a string in order to reuse machinery for immediate input by the user. *) fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) = - (fd, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts)) + (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts)) (* in FE dsc, not dat: this is in itms ...*) fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true @@ -306,7 +306,7 @@ case find_first (test_d d) itms of SOME _ => true | NONE => false in case filter_out (is_elem itms) pbt of - (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d, [])) + (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, [])) | _ => NONE end | nxt_add thy oris _ itms = @@ -419,7 +419,7 @@ if complete then (id, vt, true, fd, Model.Cor ((d,ts'), (pid, pval))) else (id, vt, false, fd, Model.Inc ((d,ts'), (pid, pval))) - | i => error ("ori_2itm: uncovered case of "^ Model.itm_2str i) + | i => error ("ori_2itm: uncovered case of "^ I_Model.feedback_to_string' i) end fun eq1 d (_, (d', _)) = (d = d') @@ -443,7 +443,7 @@ let val ts' = inter op = (Model.ts_in itm_) ts in if subset op = (ts, ts') - then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", Model.e_itm) (*2*) + then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", I_Model.empty) (*2*) else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*) end | NONE => ("", ori_2itm (Model.Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*) @@ -451,7 +451,7 @@ fun test_types ctxt (d,ts) = let - val opt = (try Model.comp_dts) (d, ts) + val opt = (try I_Model.comp_dts) (d, ts) val msg = case opt of SOME _ => "" | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^ @@ -465,24 +465,24 @@ let val ots = (distinct o flat o (map #5)) ori val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots - val (d, ts) = Model.split_dts t + val (d, ts) = I_Model.split_dts t val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts) in if (subtract op = oids ids) <> [] - then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", Model.e_ori, []) + then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, []) else if d = TermC.empty then if not (subset op = (map typeless ts, map typeless ots)) then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^ - "' not in example (typeless)", Model.e_ori, []) + "' not in example (typeless)", O_Model.single_empty, []) else (case seek_orits ctxt sel ts ori of ("", ori_ as (_,_,_,d,ts), all) => (case test_types ctxt (d,ts) of "" => ("", ori_, all) - | msg => (msg, Model.e_ori, [])) - | (msg, _, _) => (msg, Model.e_ori, [])) + | msg => (msg, O_Model.single_empty, [])) + | (msg, _, _) => (msg, O_Model.single_empty, [])) else if member op = (map #4 ori) d then seek_oridts ctxt sel (d, ts) ori @@ -504,7 +504,7 @@ case TermC.parseNEW ctxt ct of NONE => Add (i, [], false, sel, Model.Syn ct) | SOME t => - let val (d, ts) = Model.split_dts t + let val (d, ts) = I_Model.split_dts t in if d = TermC.empty then Add (i, [], false, sel, Model.Mis (Specify.dsc_unknown, hd ts)) @@ -563,7 +563,7 @@ fun mtc thy (str, (dsc, _)) (ty $ var) = ((Thm.global_cterm_of thy (dsc $ var);(*type check*) SOME (([1], str, dsc, (*[var]*) - Model.split_dts' (dsc, var))) (*:ori without leading #*)) + I_Model.split_dts' (dsc, var))) (*:ori without leading #*)) handle e as TYPE _ => (tracing (dashs 70 ^ "\n" ^ "*** ERROR while creating the items for the model of the ->problem\n" @@ -602,7 +602,7 @@ fun cpy_nam pbt oris (p as (field, (dsc, t))) = (if is_copy_named_generating p then (*WN051014 kept strange old code ...*) - let fun sel (_,_,d,ts) = Model.comp_ts (d, ts) + let fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts) val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*) @@ -649,7 +649,7 @@ fun overwrite_ppc thy itm ppc = let fun repl _ (_, _, _, _, itm_) [] = - error ("overwrite_ppc: " ^ (Model.itm_2str_ (ThyC.to_ctxt thy) itm_) ^ " not found") + error ("overwrite_ppc: " ^ (I_Model.feedback_to_string (ThyC.to_ctxt thy) itm_) ^ " not found") | repl ppc' itm (p :: ppc) = if (#1 itm) = (#1 p) then ppc' @ [itm] @ ppc diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/i-model.sml --- a/src/Tools/isac/Specify/i-model.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/i-model.sml Tue May 05 13:33:23 2020 +0200 @@ -5,12 +5,38 @@ signature MODEL_FOR_INTERACTION = sig +(**) type variants = Model_Def.variants +(* itm list*) type T = Model_Def.i_model +(* itm*) type single = Model_Def.i_model_single +(* itm_ *) datatype feedback = datatype Model_Def.i_model_feedback +(* e_itm*) val empty : single + +(*/------- to I_Model from Model 1 -------\*) +(*val itm_2str: feedback -> string*) + val feedback_to_string': feedback -> string +(*val itm_2str_: Proof.context -> feedback -> string*) + val feedback_to_string: Proof.context -> feedback -> string +(*val itm2str_: Proof.context -> single -> string*) + val single_to_string: Proof.context -> single -> string +(*val itms2str: Proof.context -> T -> string*) + val to_string: Proof.context -> T -> string + + val untouched : T -> bool +(*\------- to I_Model from Model 1 -------/*) +(*/------- to I_Model from Model 1a -------\*) + val comp_dts : term * term list -> term + val comp_dts' : term * term list -> term + val comp_dts'' : term * term list -> string + val comp_ts : term * term list -> term + val split_dts : term -> term * term list + val split_dts' : term * term -> term list +(*\------- to I_Model from Model 1a -------/*) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (* NONE *) @@ -19,9 +45,10 @@ ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end +(**) structure I_Model(**) : MODEL_FOR_INTERACTION(**) = struct - +(**) type variants = Model_Def.variants; type T = Model_Def.i_model_single list; @@ -29,4 +56,151 @@ type single = Model_Def.i_model_single; val empty = Model_Def.i_model_empty; +(*/------- to I_Model from Model 1b -------\*) +val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW); +val e_listReal = script_parse "[]::(real list)"; +val e_listBool = script_parse "[]::(bool list)"; + +(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \ ["[a]","[b]"] *) +fun take_apart t = + let val elems = TermC.isalist2list t + in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end; +fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *) + let val elems = (flat o (map TermC.isalist2list)) ts; + in TermC.list2isalist (type_of (hd elems)) elems end; +(*\------- to I_Model from Model 1b -------/*) +(*/------- to I_Model from Model 1a -------\*) +fun is_var (Free _) = true + | is_var _ = false; + +(* special handling for lists. ?WN:14.5.03 ??!? *) +fun dest_list (d, ts) = + let fun dest t = + if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*) + then TermC.isalist2list t + else [t] + in (flat o (map dest)) ts end; + +(* revert split_dts only for ts; compare comp_dts *) +fun comp_ts (d, ts) = + if Input_Descript.is_list_dsc d + then if TermC.is_list (hd ts) + then if Input_Descript.is_unl d + then (hd ts) (* e.g. someList [1,3,2] *) + else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *) + else (hd ts) (* a variable or metavariable for a list *) + else (hd ts); +fun comp_dts (d, []) = + if Input_Descript.is_reall_dsc d + then (d $ e_listReal) + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d + | comp_dts (d, ts) = (d $ (comp_ts (d, ts))) + handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); +fun comp_dts' (d, []) = + if Input_Descript.is_reall_dsc d + then (d $ e_listReal) + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d + | comp_dts' (d, ts) = (d $ (comp_ts (d, ts))) + handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); +fun comp_dts'' (d, []) = + if Input_Descript.is_reall_dsc d + then UnparseC.term (d $ e_listReal) + else if Input_Descript.is_booll_dsc d + then UnparseC.term (d $ e_listBool) + else UnparseC.term d + | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts))) + handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); + +(* decompose an input into description, terms (ev. elems of lists), + and the value for the problem-environment; inv to comp_dts *) +fun split_dts (t as d $ arg) = + if Input_Descript.is_dsc d + then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not + then (d, take_apart arg) + else (d, [arg]) + else (TermC.empty, TermC.dest_list' t) + | split_dts t = + let val t' as (h, _) = strip_comb t; + in + if Input_Descript.is_dsc h + then (h, dest_list t') + else (TermC.empty, TermC.dest_list' t) + end; +(* version returning ts only *) +fun I_Model.split_dts' (d, arg) = + if Input_Descript.is_dsc d + then if Input_Descript.is_list_dsc d + then if TermC.is_list arg + then if Input_Descript.is_unl d + then ([arg]) (* e.g. someList [1,3,2] *) + else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *) + else ([arg]) (* a variable or metavariable for a list *) + else ([arg]) + else (TermC.dest_list' arg) +(* WN170204: Warning "redundant" + | I_Model.split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*) + let val (h,argl) = strip_comb t + in + if (not o is_dsc) h + then (dest_list' t) + else (dest_list (h,argl)) + end;*) +(* revert split_: + WN050903 we do NOT know which is from subtheory, description or term; + typecheck thus may lead to TYPE-error 'unknown constant'; + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*) +(*fun comp_dts thy (d,[]) = + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*) + (Thy_Info_get_theory "Isac_Knowledge") + (*comp_dts:FIXXME stay with term for efficiency !!!*) + (if is_reall_dsc d then (d $ e_listReal) + else if is_booll_dsc d then (d $ e_listBool) + else d) + | comp_dts (d,ts) = + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*) + (Thy_Info_get_theory "Isac_Knowledge") + (*comp_dts:FIXXME stay with term for efficiency !!*) + (d $ (comp_ts (d, ts))) + handle _ => error ("comp_dts: "^(term2str d)^ + " $ "^(term2str (hd ts))));*) +(*\------- to I_Model from Model 1a -------/*) + +(*/------- to I_Model from Model 1c -------\*) +(* 27.8.01: problem-environment +WN.6.5.03: FIXXME reconsider if penv is worth the effort -- + -- just rerun a whole expl with num/var may show the same ?! +WN.9.5.03: penv-concept stalled, immediately generate script env ! + but [#0, epsilon] only outcommented for eventual reconsideration *) +type penv = (* problem-environment *) + (term (* err_ *) + * (term list) (* [#0, epsilon] 9.5.03 outcommented *) + ) list; +fun pen2str ctxt (t, ts) = + pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts); +fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv; +(*\------- to I_Model from Model 1c -------/*) +(*/------- to I_Model from Model 1 -------\*) +fun feedback_to_string ctxt (Cor ((d, ts), penv)) = + "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv + | feedback_to_string _ (Syn c) = "Syn " ^ c + | feedback_to_string _ (Typ c) = "Typ " ^ c + | feedback_to_string ctxt (Inc ((d, ts), penv)) = + "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv + | feedback_to_string ctxt (Sup (d, ts)) = + "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) + | feedback_to_string ctxt (Mis (d, pid)) = + "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid + | feedback_to_string _ (Par s) = "Trm "^s; +fun feedback_to_string' t = feedback_to_string (ThyC.id_to_ctxt "Isac_Knowledge") t; + +fun single_to_string ctxt (i, is, b, s, itm_) = + "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^ + s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")"; +fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms); + +(* in CalcTree/Subproblem an 'untouched' model is created + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*) +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms); +(*\------- to I_Model from Model 1 -------/*) + (**)end(**); \ No newline at end of file diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/input-calchead.sml --- a/src/Tools/isac/Specify/input-calchead.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/input-calchead.sml Tue May 05 13:33:23 2020 +0200 @@ -116,7 +116,7 @@ (* re-parse itms with a new thy and prepare for checking with ori list *) fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) = - (let val t = Model.comp_dts (d, ts) + (let val t = I_Model.comp_dts (d, ts) val _ = (UnparseC.term_in_thy dI t) (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) in itm end @@ -130,13 +130,13 @@ in (i, v, b, f, Model.Par str) end handle _ => (i, v, b, f, Model.Syn str)) | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) = - (let val t = Model.comp_dts (d,ts); + (let val t = I_Model.comp_dts (d,ts); val _ = UnparseC.term_in_thy dI t; (*this ^ should raise the exn on unability of re-parsing dts*) in itm end handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) = - (let val t = Model.comp_dts (d,ts); + (let val t = I_Model.comp_dts (d,ts); val _ = UnparseC.term_in_thy dI t; (*this ^ should raise the exn on unability of re-parsing dts*) in itm end @@ -148,7 +148,7 @@ in itm end handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*)))) | parsitm dI (itm as (_, _, _, _, Model.Par _)) = - error ("parsitm (" ^ Model.itm2str_ (ThyC.to_ctxt dI) itm ^ "): Par should be internal"); + error ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal"); (*separate a list to a pair of elements that do NOT satisfy the predicate, and of elements that satisfy the predicate, i.e. (false, true)*) @@ -196,7 +196,7 @@ NONE => ([], false, f, Model.Syn str) | SOME ct => let - val (d, ts) = (Model.split_dts o Thm.term_of) ct + val (d, ts) = (I_Model.split_dts o Thm.term_of) ct val popt = find_first (eq7 (f, d)) pbt in case popt of @@ -232,15 +232,15 @@ else oris2itms pbt vat os fun par2fstr (_, _, _, f, Model.Par s) = (f, s) - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm) -fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts)) + | par2fstr itm = error ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm) +fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, I_Model.comp_dts'' (d, ts)) | itms2fstr (_, _, _, f, Model.Syn str) = (f, str) | itms2fstr (_, _, _, f, Model.Typ str) = (f, str) - | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts)) - | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts)) + | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, I_Model.comp_dts'' (d,ts)) + | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, I_Model.comp_dts'' (d, ts)) | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term (d $ t)) | itms2fstr (itm as (_, _, _, _, Model.Par _)) = - error ("parsitm (" ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal"); + error ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal"); fun imodel2fstr iitems = let diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/model.sml --- a/src/Tools/isac/Specify/model.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/model.sml Tue May 05 13:33:23 2020 +0200 @@ -8,60 +8,67 @@ signature MODEL = sig -(*/------- to O_Model+I_ from ModelModel -------\*) type vats = Model_Def.variants -(*\------- to O_Model+I_ from ModelModel -------/*) -(*/------- to O_Model from Model -------\*) + type ori = Model_Def.o_model_single +(*/------- to O_Model from Model -------\* ) val oris2str: ori list -> string val e_ori: ori -(*\------- to O_Model from Model -------/*) -(*/------- to I_Model from Model -------\*) +( *\------- to O_Model from Model DONE -------/*) datatype itm_ = datatype Model_Def.i_model_feedback type itm = I_Model.single +(*/------- to I_Model from Model DONE -------\* ) val e_itm : itm -(*\------- to I_Model from Model -------/*) +( *\------- to I_Model from Model DONE -------/*) datatype item = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string +(*/------- to I_Model from Model 1 -------\* ) val itm_2str : itm_ -> string val itm_2str_ : Proof.context -> itm_ -> string val itm2str_ : Proof.context -> itm -> string val itms2str_ : Proof.context -> itm list -> string + val untouched : itm list -> bool +( *\------- to I_Model from Model 1 -------/*) type 'a ppc val empty_ppc : item ppc val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list, With: string list} -> string val itemppc2str : item ppc -> string +(*/------- to I_Model from Model 1a -------\* ) val comp_dts : term * term list -> term val comp_dts' : term * term list -> term val comp_dts'' : term * term list -> string val comp_ts : term * term list -> term val split_dts : term -> term * term list val split_dts' : term * term -> term list +( *\------- to I_Model from Model 1a -------/*) val pbl_ids' : term -> term list -> term list val mkval' : term list -> term val d_in : itm_ -> term val ts_in : itm_ -> term list val penvval_in : itm_ -> term list - val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *) val vars_of : itm list -> term list val max_vt : itm list -> int + val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *) (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) +(*/------- to I_Model from Model 1c -------\* ) type penv val penv2str_ : Proof.context -> penv -> string (* NONE *) +( *\------- to I_Model from Model 1c -------/*) +(*/------- to O_Model from Model 1 -------\* ) type preori val preoris2str : preori list -> string +( *\------- to O_Model from Model 1 -------/*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) (* NONE *) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) (*----- unused code, kept as hints to design ideas ---------------------------------------------*) - val untouched : itm list -> bool type envv val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv val item_ppc : string ppc -> item ppc @@ -113,6 +120,7 @@ (b) ==========================================================================*) +(*/------- to I_Model from Model 1b -------\* ) val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW); val e_listReal = script_parse "[]::(real list)"; val e_listBool = script_parse "[]::(bool list)"; @@ -124,7 +132,9 @@ fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *) let val elems = (flat o (map TermC.isalist2list)) ts; in TermC.list2isalist (type_of (hd elems)) elems end; +( *\------- to I_Model from Model 1b -------/*) +(*/------- to I_Model from Model 1a -------\* ) fun is_var (Free _) = true | is_var _ = false; @@ -218,7 +228,9 @@ (d $ (comp_ts (d, ts))) handle _ => error ("comp_dts: "^(term2str d)^ " $ "^(term2str (hd ts))));*) +( *\------- to I_Model from Model 1a -------/*) +(*/------- to I_Model from Model 1c -------\*) (* 27.8.01: problem-environment WN.6.5.03: FIXXME reconsider if penv is worth the effort -- -- just rerun a whole expl with num/var may show the same ?! @@ -231,6 +243,7 @@ fun pen2str ctxt (t, ts) = pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts); fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv; +(*\------- to I_Model from Model 1c -------/*) (* get the constant value from a penv *) fun getval (id, values) = @@ -255,7 +268,7 @@ type vats = Model_Def.variants; (*\------- to O_Model+I_ from Model -------/*) -(*/------- to I_Model from Model -------\*) +(*/------- to I_Model from Model DONE -------\*) (* the internal representation of a models' item 4.9.01: not consistent: after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation @@ -273,11 +286,7 @@ string * (* #Given | #Find | #Relate *) itm_; (* *) val e_itm = (0, [], false, "e_itm", Syn "e_itm"); -(*\------- to I_Model from Model -------/*) - -(* in CalcTree/Subproblem an 'untouched' model is created - FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*) -fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms); +(*\------- to I_Model from Model DONE -------/*) (* find most frequent variant v in itms *) fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list); @@ -322,15 +331,17 @@ val oris2str = Model_Def.o_model_to_string; (*\------- to O_Model from Model -------/*) +(*/------- to O_Model from Model 1 -------\* ) (* an or without leading integer *) type preori = (vats * string * term * term list); fun preori2str (vs, fi, t, ts) = "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; val preoris2str = (strs2str' o (map (linefeed o preori2str))); +( *\------- to O_Model from Model 1 -------/*) (* 9.5.03 penv postponed: pbl_ids' *) -fun pbl_ids' d vs = [comp_ts (d, vs)]; +fun pbl_ids' d vs = [I_Model.comp_ts (d, vs)]; (* 14.9.01: not used after putting values for penv into itm_ WN.5.5.03: used in upd .. upd_envv *) @@ -382,6 +393,7 @@ | item2str (Superfl s) = "Superfl " ^ s | item2str (Missing s) = "Missing " ^ s; +(*/------- to I_Model from Model 1 -------\* ) fun itm_2str_ ctxt (Cor ((d, ts), penv)) = "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv | itm_2str_ _ (Syn c) = "Syn " ^ c @@ -399,6 +411,11 @@ "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^ s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")"; fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms); + +(* in CalcTree/Subproblem an 'untouched' model is created + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*) +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms); +( *\------- to I_Model from Model 1 -------/*) fun init_item str = SyntaxE str; type 'a ppc = @@ -439,7 +456,7 @@ | d_in _ = raise ERROR "d_in: uncovered case in fun.def."; fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts); -fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)] +fun penvval_in (Cor ((d, _), (_, ts))) = [I_Model.comp_ts (d,ts)] | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) []) | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) []) | penvval_in (Inc (_, (_, ts))) = ts diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/o-model.sml --- a/src/Tools/isac/Specify/o-model.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/o-model.sml Tue May 05 13:33:23 2020 +0200 @@ -5,14 +5,23 @@ signature ORIGINAL_MODEL = sig +(* vats*) type variants = Model_Def.variants +(* ori list*) type T = Model_Def.o_model +(* ori *) type single = Model_Def.o_model_single - +(* oris2str*) val to_string: T -> string +(* e_ori*) val single_empty: single +(*/------- to O_Model from Model 1 -------\*) + type preori +(*\------- to O_Model from Model 1 -------/*) + (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + val preoris2str : preori list -> string (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) (* NONE *) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) @@ -28,5 +37,14 @@ val single_empty = Model_Def.o_model_empty; val to_string = Model_Def.o_model_to_string; +(*/------- to O_Model from Model 1 -------\*) +(* an or without leading integer *) +type preori = (variants * string * term * term list); +fun preori2str (vs, fi, t, ts) = + "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ + UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; +val preoris2str = (strs2str' o (map (linefeed o preori2str))); +(*\------- to O_Model from Model 1 -------/*) + (**)end(**); \ No newline at end of file diff -r 602bf61dc6df -r d6261de56fb0 src/Tools/isac/Specify/ptyps.sml --- a/src/Tools/isac/Specify/ptyps.sml Tue May 05 09:07:36 2020 +0200 +++ b/src/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200 @@ -151,11 +151,11 @@ type field = string * (term * term) val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow"; -fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (Model.comp_dts (d, ts))) +fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts))) | itm_2item _ (Model.Syn c) = Model.SyntaxE c | itm_2item _ (Model.Typ c) = Model.TypeE c - | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (Model.comp_dts (d, ts))) - | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (Model.comp_dts (d, ts))) + | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts))) + | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts))) | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid) | itm_2item _ _ = error "itm_2item: uncovered definition" @@ -184,11 +184,11 @@ in (hd, arg) end (*create output-string for itm_*) -fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts)) +fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts)) | itm_out _ (Model.Syn c) = c | itm_out _ (Model.Typ c) = c - | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts)) - | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (Model.comp_dts (d, ts)) + | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts)) + | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts)) | itm_out _ (Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid | itm_out _ _ = error "itm_out: uncovered definition" @@ -275,7 +275,7 @@ | prep_ori fmz thy pbt = let val ctxt = ContextC.initialise' thy fmz; - val ori = map (add_field thy pbt o Model.split_dts o TermC.parseNEW' ctxt) fmz + val ori = map (add_field thy pbt o I_Model.split_dts o TermC.parseNEW' ctxt) fmz |> add_variants; val maxv = map fst ori |> max; val maxv = if maxv = 0 then 1 else maxv; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Interpret/error-pattern.sml --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 13:33:23 2020 +0200 @@ -399,11 +399,11 @@ (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*) val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)]; (*val nxt = ("Model_Problem", ...*) - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "fixedValues [r = Arbfix]"*) - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; (*[ (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])), (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])), @@ -412,7 +412,7 @@ (*the empty CalcHead is checked w.r.t the model and re-established as such*) val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, Spec.empty); - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1"; (*there is one input to the model (could be more)*) @@ -420,7 +420,7 @@ input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"], Find ["maximum", "valuesFor"], Relate ["relations"]], Pbl, Spec.empty); - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl; if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 2"; @@ -430,7 +430,7 @@ Find ["maximum A", "valuesFor [a,b]"], Relate ["relations [A=a*b, a/2=r*sin alpha, \ \b/2=r*cos alpha]"]], Pbl, Spec.empty); - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*) (*this input is complete in variant 1 (variant 3 does not work yet)*) @@ -440,7 +440,7 @@ Relate ["relations [A=a*b, \ \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl, Spec.empty); - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl; + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl; modifycalcheadOK2xml 111 (bool2str b) ocalhd; *) @@ -655,8 +655,8 @@ (*default_print_depth 5;*) writeln"-----------------------------------------------------------"; spec; -writeln (itms2str_ ctxt probl); -writeln (itms2str_ ctxt meth); +writeln (I_Model.to_string ctxt probl); +writeln (I_Model.to_string ctxt meth); writeln (Istate.string_of (fst istate)); refFormula 1 ([],Pbl) (*--> correct CalcHead*); @@ -677,12 +677,12 @@ (*("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) : spec*) -writeln (itms2str_ ctxt probl); +writeln (I_Model.to_string ctxt probl); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) -writeln (itms2str_ ctxt meth); +writeln (I_Model.to_string ctxt meth); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), @@ -720,12 +720,12 @@ (*("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) : spec*) -writeln (itms2str_ ctxt probl); +writeln (I_Model.to_string ctxt probl); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*) -writeln (itms2str_ ctxt meth); +writeln (I_Model.to_string ctxt meth); (*[ (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])), (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])), @@ -1253,7 +1253,7 @@ (#1 (some_spec ospec spec), oris, []:itm list, ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); val iii = appl_adds dI oris ppc pbt (selct::ss); - tracing(itms2str_ thy iii); + tracing(I_Model.to_string thy iii); val itm = appl_add' dI oris ppc pbt selct; val ppc = insert_ppc' itm ppc; @@ -1265,7 +1265,7 @@ val _::selct::ss = (selct::ss); val itm = appl_add' dI oris ppc pbt selct; val ppc = insert_ppc' itm ppc; - tracing(itms2str_ thy ppc); + tracing(I_Model.to_string thy ppc); val _::selct::ss = (selct::ss); val itm = appl_add' dI oris ppc pbt selct; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Knowledge/biegelinie-4.sml --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 05 13:33:23 2020 +0200 @@ -96,8 +96,8 @@ (5, ["1"], #undef,FunktionsVariable, ["x"]), (6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]), (7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*) -(*+*)itms2str_ @{context} probl = "[]"; -(*+*)itms2str_ @{context} meth = "[]"; +(*+*)I_Model.to_string @{context} probl = "[]"; +(*+*)I_Model.to_string @{context} meth = "[]"; (*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*) (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*) @@ -207,15 +207,15 @@ (1, ["1"], #Given,Streckenlast, ["q_0"]), (2, ["1"], #Given,FunktionsVariable, ["x"]), (3, ["1"], #Find,Funktionen, ["funs'''"])]*) -(*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]" +(*+*)if I_Model.to_string @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]" (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl"; -writeln (itms2str_ @{context} probl); (*[ +writeln (I_Model.to_string @{context} probl); (*[ (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*) -(*+*)if itms2str_ @{context} meth = "[]" +(*+*)if I_Model.to_string @{context} meth = "[]" (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth"; -writeln (itms2str_ @{context} meth); (*[]*) +writeln (I_Model.to_string @{context} meth); (*[]*) "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt'''''); (* val (pt, p) = *) @@ -258,7 +258,7 @@ val met = if met = [] then pbl else met val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris ; -(*+*)writeln (itms2str_ @{context} itms); (*[ +(*+*)writeln (I_Model.to_string @{context} itms); (*[ (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *) diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue May 05 13:33:23 2020 +0200 @@ -282,10 +282,10 @@ | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method"; val oris = fst3 (get_obj g_origin pt (fst p)); writeln(O_Model.to_string oris); -val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits); +val pits = get_obj g_pbl pt (fst p); writeln(I_Model.to_string ctxt pits); val (p,_,f,nxt,_,pt) = me nxt p c pt; -val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits); +val mits = get_obj g_met pt (fst p); writeln(I_Model.to_string ctxt mits); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -313,7 +313,7 @@ === inhibit exn 110722=============================================================*) val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits); (*=== inhibit exn 110722============================================================= val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -348,7 +348,7 @@ (*val nxt = Refine_Tacitly ["univariate","equation"])*) val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits); val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; @@ -383,11 +383,11 @@ val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris); -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); -val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits); +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits); +val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits); -val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits); -val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits); +val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string ctxt mits); +val mits = get_obj g_met pt [];writeln(I_Model.to_string ctxt mits); (*=== inhibit exn 110722============================================================= arguments_from_model ["DiffApp","max_by_calculus"] mits; @@ -434,14 +434,14 @@ fetchProposedTactic 1; val ((pt,p),_) = get_calc 1; val mits = get_obj g_met pt (fst p); - writeln (itms2str_ ctxt mits); + writeln (I_Model.to_string ctxt mits); (* - if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then () + if I_Model.to_string ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then () else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1"; *) (*FIXME: the environments contain identifers, and NOT values ?!?!?*) (* WN051209 while extending 'fun step' for initac, this became better ... - if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1"; *) diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue May 05 13:33:23 2020 +0200 @@ -460,7 +460,7 @@ =========================================================================/ -----fun refin' ff: -> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms; +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms; [ (1 ,[1] ,true ,#Given ,Cor equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, @@ -475,7 +475,7 @@ (true, length_ [c, c_2] = 2)] ----- fun match_oris': -> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms; +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms; > (writeln o pres2str) pre'; ..as in refin' @@ -542,7 +542,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val PblObj {probl,...} = get_obj I pt [5]; - (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl; + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl; (*[ (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])), @@ -610,7 +610,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val PblObj {probl,...} = get_obj I pt [5]; - (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl; + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl; (*[ (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])), diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Tue May 05 13:33:23 2020 +0200 @@ -615,7 +615,7 @@ (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n (3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1))"*) (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*) -(*+*)if itms2str_ ctxt (get_obj g_pbl pt (fst p)) = +(*+*)if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) = (*+*) "[\n(0 ,[] ,false ,#Find ,Inc normalform ,(??.empty, [])),\n(1 ,[1] ,true ,#Given ,Cor Term\n ((5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n (3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)) ,(t_t, [(5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n(3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)]))]" (*+*)then () else error "No.267b: itm list CHANGED"; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/MathEngBasic/ctree-navi.sml --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 13:33:23 2020 +0200 @@ -6,7 +6,7 @@ "table of contents -----------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; "----------- go through Model_Problem until nxt_tac --------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; "----------- type penv -------------------------------------------------------------------------"; "----------- fun untouched ---------------------------------------------------------------------"; "----------- fun pbl_ids -----------------------------------------------------------------------"; @@ -79,8 +79,8 @@ val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list); val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; -val (d, ts) = split_dts t; -"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t; +val (d, ts) = I_Model.split_dts t; +"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t; (*if is_dsc d then () else error "TODO";*) if is_dsc d then () else error "TODO"; "----- these were the errors (call hierarchy from bottom up)"; @@ -96,60 +96,60 @@ Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) ========== inhibit exn AK110725 ================================================*) -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; (*val t = str2term "maximum A"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); val it = "maximum A" : cterm > val t = str2term "fixedValues [r=Arbfix]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "fixedValues [r = Arbfix]" > val t = str2term "valuesFor [a]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "valuesFor [a]" > val t = str2term "valuesFor [a,b]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "valuesFor [a, b]" > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" > val t = str2term "boundVariable a"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "boundVariable a" > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "interval {x. 0 <= x & x <= 2 * r}" > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" > val t = str2term "solveFor x"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "solveFor x" > val t = str2term "errorBound (eps=0)"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "errorBound (eps = 0)" > val t = str2term "solutions L"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "solutions L" before 6.5.03: > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; > comp_dts thy (d,ts); val it = "testdscforlist [#1]" : cterm > val t = (Thm.term_of o the o (parse thy)) "(A::real)"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val d = Const ("empty","empty") : term val ts = [Free ("A","RealDef.real")] : term list > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val d = Const ("empty","empty") : term val ts = [Const # $ Free # $ Free (#,#)] : term list > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED *) "----------- type penv -------------------------------------------------------------------------"; @@ -189,7 +189,7 @@ val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; val (d,argl) = strip_comb t; - is_dsc d; (*see split_dts*) + is_dsc d; (*see I_Model.split_dts*) dest_list (d,argl); val (_ $ v) = t; is_list v; @@ -197,7 +197,7 @@ [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. - val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term val vl = Free ("x","RealDef.real") : term @@ -205,7 +205,7 @@ pbl_ids ctxt dsc vl; val it = [Free ("x","RealDef.real")] : term list - val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy)) + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy)) "errorBound (eps=#0)"; val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_"; pbl_ids ctxt dsc vl; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/MathEngBasic/ctree.sml --- a/test/Tools/isac/MathEngBasic/ctree.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Tue May 05 13:33:23 2020 +0200 @@ -66,7 +66,7 @@ handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj"; val pt = EmptyPtree; -val pt = append_problem [] (Istate.empty, ContextC.empty) Celem.Formalise.empty ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt; +val pt = append_problem [] (Istate.empty, ContextC.empty) Formalise.empty ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt; val ctxt = get_obj g_ctxt pt []; if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed"; @@ -81,13 +81,13 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = Add_Given "equality (x + 1 = 2)" - (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); + (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; @@ -453,13 +453,13 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* nxt = Add_Given "equality (x + 1 = 2)" - (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); + (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p)); +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p)); *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/MathEngBasic/model.sml --- a/test/Tools/isac/MathEngBasic/model.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/MathEngBasic/model.sml Tue May 05 13:33:23 2020 +0200 @@ -43,7 +43,7 @@ val env = []:envv; - val (d,ts) = (split_dts o Thm.term_of o the o (parse thy)) + val (d,ts) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; val (_,id) = (split_did o Thm.term_of o the o (parse thy))"fixedValues fix_"; val vats = [1,2,3]; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/MathEngBasic/mstools.sml --- a/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 13:33:23 2020 +0200 @@ -6,7 +6,7 @@ "table of contents -----------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; "----------- go through Model_Problem until nxt_tac --------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; "----------- type penv -------------------------------------------------------------------------"; "----------- fun untouched ---------------------------------------------------------------------"; "----------- fun pbl_ids -----------------------------------------------------------------------"; @@ -79,8 +79,8 @@ val _ = tracing ("RM is_known: t=" ^ UnparseC.term t); val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list); val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots; -val (d, ts) = split_dts t; -"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t; +val (d, ts) = I_Model.split_dts t; +"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t; (*if is_dsc d then () else error "TODO";*) if is_dsc d then () else error "TODO"; "----- these were the errors (call hierarchy from bottom up)"; @@ -96,60 +96,60 @@ Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) ========== inhibit exn AK110725 ================================================*) -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------"; (*val t = str2term "maximum A"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); val it = "maximum A" : cterm > val t = str2term "fixedValues [r=Arbfix]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "fixedValues [r = Arbfix]" > val t = str2term "valuesFor [a]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "valuesFor [a]" > val t = str2term "valuesFor [a,b]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "valuesFor [a, b]" > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" > val t = str2term "boundVariable a"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "boundVariable a" > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "interval {x. 0 <= x & x <= 2 * r}" > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" > val t = str2term "solveFor x"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "solveFor x" > val t = str2term "errorBound (eps=0)"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "errorBound (eps = 0)" > val t = str2term "solutions L"; -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts); +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts); "solutions L" before 6.5.03: > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; > comp_dts thy (d,ts); val it = "testdscforlist [#1]" : cterm > val t = (Thm.term_of o the o (parse thy)) "(A::real)"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val d = Const ("empty","empty") : term val ts = [Free ("A","RealDef.real")] : term list > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val d = Const ("empty","empty") : term val ts = [Const # $ Free # $ Free (#,#)] : term list > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]"; -> val (d,ts) = split_dts t; +> val (d,ts) = I_Model.split_dts t; val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED *) "----------- type penv -------------------------------------------------------------------------"; @@ -189,7 +189,7 @@ val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; val (d,argl) = strip_comb t; - is_dsc d; (*see split_dts*) + is_dsc d; (*see I_Model.split_dts*) dest_list (d,argl); val (_ $ v) = t; is_list v; @@ -197,7 +197,7 @@ [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. - val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term val vl = Free ("x","RealDef.real") : term @@ -205,7 +205,7 @@ pbl_ids ctxt dsc vl; val it = [Free ("x","RealDef.real")] : term list - val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy)) + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy)) "errorBound (eps=#0)"; val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_"; pbl_ids ctxt dsc vl; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Minisubpbl/150-add-given.sml --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 13:33:23 2020 +0200 @@ -82,7 +82,7 @@ (thy, ori, (hd icl)); "~~~~~ to return val:"; val xxx = ( fd, - ((UnparseC.term_in_thy thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string + ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string ); if xxx = ("#Given", "equality (x + 1 = 2)") then () else error ""; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Specify/calchead.sml --- a/test/Tools/isac/Specify/calchead.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200 @@ -97,7 +97,7 @@ val ("dummy", ([(Add_Relation "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]", _, _)], _, ptp)) = Step.specify_do_next ptp; val PblObj {probl, ...} = get_obj I (fst ptp) []; -if itms2str_ @{context} probl = +if I_Model.to_string @{context} probl = "[\n" ^ "(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n" ^ "(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n" @@ -191,7 +191,7 @@ (*val nxt = Specify_Theory "DiffApp" : tac*) -val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms); +val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms); val nxt = tac2tac_ pt p nxt; val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; @@ -542,7 +542,7 @@ val (thy, (str, (dsc, _)): Celem4.pat, ty $ var) = (thy, p, a); val ttt = (dsc $ var); Thm.global_cterm_of thy (dsc $ var); -val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); +val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori); "-d2-----------------------------------------------------"; pbt = []; (*false*) @@ -555,7 +555,7 @@ val (thy, (str, (dsc, _)):Celem4.pat, ty $ var) = (thy, p, a); val ttt = (dsc $ var); Thm.global_cterm_of thy (dsc $ var); -val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); +val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori); "-d3-----------------------------------------------------"; pbt = []; (*true, base case*) "-----------------continue step through code match_ags---"; diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Specify/ptyps.sml --- a/test/Tools/isac/Specify/ptyps.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200 @@ -34,20 +34,20 @@ val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}; (*case 1: no refinement *) -val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]"); -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)"); +val (d1,ts1) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]"); +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)"); val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list; (*case 2: refined to pbt without children *) -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]"); +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]"); val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list; (*case 3: refined to pbt with children *) -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]"); +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]"); val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list; (*case 4: refined to children (without child)*) -val (d3,ts3) = split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy"); +val (d3,ts3) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy"); val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list; (*================================================================= diff -r 602bf61dc6df -r d6261de56fb0 test/Tools/isac/Specify/specify.sml --- a/test/Tools/isac/Specify/specify.sml Tue May 05 09:07:36 2020 +0200 +++ b/test/Tools/isac/Specify/specify.sml Tue May 05 13:33:23 2020 +0200 @@ -37,7 +37,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*) val pits = get_obj g_pbl pt (fst p); - writeln (itms2str_ ctxt pits); + writeln (I_Model.to_string ctxt pits); (*[ (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])), (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])), @@ -45,9 +45,9 @@ (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) val (pt,p) = complete_mod (pt,p); val pits = get_obj g_pbl pt (fst p); - if itms2str_ ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" + if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" then () else error "completetest.sml: new behav. in complete_mod 3"; - writeln (itms2str_ ctxt pits); + writeln (I_Model.to_string ctxt pits); (*[ (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), @@ -55,9 +55,9 @@ (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*) val mits = get_obj g_met pt (fst p); - if itms2str_ ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () else error "completetest.sml: new behav. in complete_mod 3"; - writeln (itms2str_ ctxt mits); + writeln (I_Model.to_string ctxt mits); (*[ (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), @@ -112,7 +112,7 @@ (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]), (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*) val pits = get_obj g_pbl pt (fst p); - writeln (itms2str_ ctxt pits); + writeln (I_Model.to_string ctxt pits); (*[ (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])), @@ -122,7 +122,7 @@ val mits = get_obj g_met pt (fst p); val mits = complete_metitms oris pits [] ((#ppc o get_met) ["DiffApp","max_by_calculus"]); - writeln (itms2str_ ctxt mits); + writeln (I_Model.to_string ctxt mits); (*[ (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), @@ -133,7 +133,7 @@ (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. 0 <= x & x <= 2 * r}])), (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) -if itms2str_ ctxt mits +if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 \ x \ x \ 2 * r} ,(i_tv, [{x. 0 \ x \ x \ 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]" then () else error "completetest.sml: new behav. in complete_metitms 1";