1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 09:07:36 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 05 13:33:23 2020 +0200
1.3 @@ -345,16 +345,16 @@
1.4 in filt end;
1.5
1.6 fun xml_of_itm_ (Model.Cor (dts, _)) =
1.7 - XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Model.comp_dts' dts)])
1.8 + XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (I_Model.comp_dts' dts)])
1.9 | xml_of_itm_ (Model.Syn c) =
1.10 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
1.11 | xml_of_itm_ (Model.Typ c) =
1.12 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
1.13 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
1.14 | xml_of_itm_ (Model.Inc (dts, _)) =
1.15 - XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Model.comp_dts' dts)])
1.16 + XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (I_Model.comp_dts' dts)])
1.17 | xml_of_itm_ (Model.Sup dts) =
1.18 - XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Model.comp_dts' dts)])
1.19 + XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (I_Model.comp_dts' dts)])
1.20 | xml_of_itm_ (Model.Mis (d, pid)) =
1.21 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
1.22 | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue May 05 09:07:36 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue May 05 13:33:23 2020 +0200
2.3 @@ -54,7 +54,7 @@
2.4 (* *)
2.5 val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
2.6 fun error_msg_2 d itms = ("arguments_from_model: '" ^ UnparseC.term d ^ "' not in itms:\n" ^
2.7 - "itms:\n" ^ Model.itms2str_ @{context} itms)
2.8 + "itms:\n" ^ I_Model.to_string @{context} itms)
2.9 (* turn model-items into arguments for a program *)
2.10 fun arguments_from_model mI itms =
2.11 let
3.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Tue May 05 09:07:36 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Tue May 05 13:33:23 2020 +0200
3.3 @@ -33,7 +33,7 @@
3.4 | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
3.5 (* itm*)
3.6 type i_model_single
3.7 -(*\<rightarrow> form_T*)
3.8 +(* itm list*)
3.9 type i_model
3.10 (* e_itm*)
3.11 val i_model_empty : i_model_single
4.1 --- a/src/Tools/isac/Specify/calchead.sml Tue May 05 09:07:36 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200
4.3 @@ -118,9 +118,9 @@
4.4 val is_copy_named_generating : 'a * ('b * term) -> bool
4.5 val is_copy_named : 'a * ('b * term) -> bool
4.6 val ori2Coritm : Celem4.pat list -> O_Model.single -> I_Model.single
4.7 - val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
4.8 - val mtc : theory -> Celem4.pat -> term -> Model.preori option
4.9 - val cpy_nam : Celem4.pat list -> Model.preori list -> Celem4.pat -> Model.preori
4.10 + val matc : theory -> (string * (term * term)) list -> term list -> O_Model.preori list -> O_Model.preori list
4.11 + val mtc : theory -> Celem4.pat -> term -> O_Model.preori option
4.12 + val cpy_nam : Celem4.pat list -> O_Model.preori list -> Celem4.pat -> O_Model.preori
4.13 datatype additm = Add of I_Model.single | Err of string
4.14 val appl_add: Proof.context -> string -> O_Model.T ->
4.15 I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm
4.16 @@ -191,7 +191,7 @@
4.17 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
4.18 fun oris2fmz_vals oris =
4.19 let fun ori2fmz_vals (_, _, _, dsc, ts) =
4.20 - ((UnparseC.term o Model.comp_dts') (dsc, ts), last_elem ts)
4.21 + ((UnparseC.term o I_Model.comp_dts') (dsc, ts), last_elem ts)
4.22 handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)
4.23 in (split_list o (map ori2fmz_vals)) oris end
4.24
4.25 @@ -208,7 +208,7 @@
4.26 WN.11.03: + dont take first inter<>[] *)
4.27 fun seek_oridts ctxt sel (d, ts) [] =
4.28 ("seek_oridts: input ('" ^
4.29 - (UnparseC.term_in_ctxt ctxt (Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
4.30 + (UnparseC.term_in_ctxt ctxt (I_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
4.31 (0, [], sel, d, ts),
4.32 [])
4.33 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
4.34 @@ -219,13 +219,13 @@
4.35 (* to an input (_,ts) find the according ori and insert the ts *)
4.36 fun seek_orits ctxt _ ts [] =
4.37 ("seek_orits: input (_, '" ^ strs2str (map (UnparseC.term_in_ctxt ctxt) ts) ^
4.38 - "') not found in oris (typed)", Model.e_ori, [])
4.39 + "') not found in oris (typed)", O_Model.single_empty, [])
4.40 | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: oris) =
4.41 if sel = sel' andalso (inter op = ts ts') <> []
4.42 then
4.43 if sel = sel'
4.44 then ("", (id, vat, sel, d, inter op = ts ts'), ts')
4.45 - else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, Model.e_ori, [])
4.46 + else (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts) ^ " not for " ^ sel, O_Model.single_empty, [])
4.47 else seek_orits ctxt sel ts oris
4.48
4.49 (* find_first item with #1 equal to id *)
4.50 @@ -268,7 +268,7 @@
4.51 | d_in (Model.Inc ((d,_),_)) = [d]
4.52 | d_in (Model.Sup (d,_)) = [d]
4.53 | d_in (Model.Mis (d,_)) = [d]
4.54 - | d_in i = error ("all_dsc_in: uncovered case with " ^ Model.itm_2str i)
4.55 + | d_in i = error ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
4.56 in (flat o (map d_in)) itm_s end;
4.57
4.58 fun is_error (Model.Cor _) = false
4.59 @@ -279,13 +279,13 @@
4.60
4.61 (* get the first term in ts from ori *)
4.62 fun getr_ct thy (_, _, fd, d, ts) =
4.63 - (fd, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d,[hd ts]))
4.64 + (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d,[hd ts]))
4.65
4.66 (* get a term from ori, notyet input in itm.
4.67 the term from ori is thrown back to a string in order to reuse
4.68 machinery for immediate input by the user. *)
4.69 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
4.70 - (fd, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts))
4.71 + (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts))
4.72
4.73 (* in FE dsc, not dat: this is in itms ...*)
4.74 fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true
4.75 @@ -306,7 +306,7 @@
4.76 case find_first (test_d d) itms of SOME _ => true | NONE => false
4.77 in
4.78 case filter_out (is_elem itms) pbt of
4.79 - (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Model.comp_dts) (d, []))
4.80 + (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, []))
4.81 | _ => NONE
4.82 end
4.83 | nxt_add thy oris _ itms =
4.84 @@ -419,7 +419,7 @@
4.85 if complete
4.86 then (id, vt, true, fd, Model.Cor ((d,ts'), (pid, pval)))
4.87 else (id, vt, false, fd, Model.Inc ((d,ts'), (pid, pval)))
4.88 - | i => error ("ori_2itm: uncovered case of "^ Model.itm_2str i)
4.89 + | i => error ("ori_2itm: uncovered case of "^ I_Model.feedback_to_string' i)
4.90 end
4.91
4.92 fun eq1 d (_, (d', _)) = (d = d')
4.93 @@ -443,7 +443,7 @@
4.94 let val ts' = inter op = (Model.ts_in itm_) ts
4.95 in
4.96 if subset op = (ts, ts')
4.97 - then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", Model.e_itm) (*2*)
4.98 + then (((strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts') ^ " already input", I_Model.empty) (*2*)
4.99 else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
4.100 end
4.101 | NONE => ("", ori_2itm (Model.Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
4.102 @@ -451,7 +451,7 @@
4.103
4.104 fun test_types ctxt (d,ts) =
4.105 let
4.106 - val opt = (try Model.comp_dts) (d, ts)
4.107 + val opt = (try I_Model.comp_dts) (d, ts)
4.108 val msg = case opt of
4.109 SOME _ => ""
4.110 | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
4.111 @@ -465,24 +465,24 @@
4.112 let
4.113 val ots = (distinct o flat o (map #5)) ori
4.114 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
4.115 - val (d, ts) = Model.split_dts t
4.116 + val (d, ts) = I_Model.split_dts t
4.117 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
4.118 in
4.119 if (subtract op = oids ids) <> []
4.120 - then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", Model.e_ori, [])
4.121 + then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", O_Model.single_empty, [])
4.122 else
4.123 if d = TermC.empty
4.124 then
4.125 if not (subset op = (map typeless ts, map typeless ots))
4.126 then ("terms '" ^ (strs2str' o (map (UnparseC.term_in_ctxt ctxt))) ts ^
4.127 - "' not in example (typeless)", Model.e_ori, [])
4.128 + "' not in example (typeless)", O_Model.single_empty, [])
4.129 else
4.130 (case seek_orits ctxt sel ts ori of
4.131 ("", ori_ as (_,_,_,d,ts), all) =>
4.132 (case test_types ctxt (d,ts) of
4.133 "" => ("", ori_, all)
4.134 - | msg => (msg, Model.e_ori, []))
4.135 - | (msg, _, _) => (msg, Model.e_ori, []))
4.136 + | msg => (msg, O_Model.single_empty, []))
4.137 + | (msg, _, _) => (msg, O_Model.single_empty, []))
4.138 else
4.139 if member op = (map #4 ori) d
4.140 then seek_oridts ctxt sel (d, ts) ori
4.141 @@ -504,7 +504,7 @@
4.142 case TermC.parseNEW ctxt ct of
4.143 NONE => Add (i, [], false, sel, Model.Syn ct)
4.144 | SOME t =>
4.145 - let val (d, ts) = Model.split_dts t
4.146 + let val (d, ts) = I_Model.split_dts t
4.147 in
4.148 if d = TermC.empty
4.149 then Add (i, [], false, sel, Model.Mis (Specify.dsc_unknown, hd ts))
4.150 @@ -563,7 +563,7 @@
4.151 fun mtc thy (str, (dsc, _)) (ty $ var) =
4.152 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
4.153 SOME (([1], str, dsc, (*[var]*)
4.154 - Model.split_dts' (dsc, var))) (*:ori without leading #*))
4.155 + I_Model.split_dts' (dsc, var))) (*:ori without leading #*))
4.156 handle e as TYPE _ =>
4.157 (tracing (dashs 70 ^ "\n"
4.158 ^ "*** ERROR while creating the items for the model of the ->problem\n"
4.159 @@ -602,7 +602,7 @@
4.160 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
4.161 (if is_copy_named_generating p
4.162 then (*WN051014 kept strange old code ...*)
4.163 - let fun sel (_,_,d,ts) = Model.comp_ts (d, ts)
4.164 + let fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts)
4.165 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
4.166 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
4.167 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
4.168 @@ -649,7 +649,7 @@
4.169 fun overwrite_ppc thy itm ppc =
4.170 let
4.171 fun repl _ (_, _, _, _, itm_) [] =
4.172 - error ("overwrite_ppc: " ^ (Model.itm_2str_ (ThyC.to_ctxt thy) itm_) ^ " not found")
4.173 + error ("overwrite_ppc: " ^ (I_Model.feedback_to_string (ThyC.to_ctxt thy) itm_) ^ " not found")
4.174 | repl ppc' itm (p :: ppc) =
4.175 if (#1 itm) = (#1 p)
4.176 then ppc' @ [itm] @ ppc
5.1 --- a/src/Tools/isac/Specify/i-model.sml Tue May 05 09:07:36 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue May 05 13:33:23 2020 +0200
5.3 @@ -5,12 +5,38 @@
5.4
5.5 signature MODEL_FOR_INTERACTION =
5.6 sig
5.7 +(**)
5.8 type variants = Model_Def.variants
5.9
5.10 +(* itm list*)
5.11 type T = Model_Def.i_model
5.12 +(* itm*)
5.13 type single = Model_Def.i_model_single
5.14 +(* itm_ *)
5.15 datatype feedback = datatype Model_Def.i_model_feedback
5.16 +(* e_itm*)
5.17 val empty : single
5.18 +
5.19 +(*/------- to I_Model from Model 1 -------\*)
5.20 +(*val itm_2str: feedback -> string*)
5.21 + val feedback_to_string': feedback -> string
5.22 +(*val itm_2str_: Proof.context -> feedback -> string*)
5.23 + val feedback_to_string: Proof.context -> feedback -> string
5.24 +(*val itm2str_: Proof.context -> single -> string*)
5.25 + val single_to_string: Proof.context -> single -> string
5.26 +(*val itms2str: Proof.context -> T -> string*)
5.27 + val to_string: Proof.context -> T -> string
5.28 +
5.29 + val untouched : T -> bool
5.30 +(*\------- to I_Model from Model 1 -------/*)
5.31 +(*/------- to I_Model from Model 1a -------\*)
5.32 + val comp_dts : term * term list -> term
5.33 + val comp_dts' : term * term list -> term
5.34 + val comp_dts'' : term * term list -> string
5.35 + val comp_ts : term * term list -> term
5.36 + val split_dts : term -> term * term list
5.37 + val split_dts' : term * term -> term list
5.38 +(*\------- to I_Model from Model 1a -------/*)
5.39
5.40 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.41 (* NONE *)
5.42 @@ -19,9 +45,10 @@
5.43 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.44 end
5.45
5.46 +(**)
5.47 structure I_Model(**) : MODEL_FOR_INTERACTION(**) =
5.48 struct
5.49 -
5.50 +(**)
5.51 type variants = Model_Def.variants;
5.52
5.53 type T = Model_Def.i_model_single list;
5.54 @@ -29,4 +56,151 @@
5.55 type single = Model_Def.i_model_single;
5.56 val empty = Model_Def.i_model_empty;
5.57
5.58 +(*/------- to I_Model from Model 1b -------\*)
5.59 +val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
5.60 +val e_listReal = script_parse "[]::(real list)";
5.61 +val e_listBool = script_parse "[]::(bool list)";
5.62 +
5.63 +(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
5.64 +fun take_apart t =
5.65 + let val elems = TermC.isalist2list t
5.66 + in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
5.67 +fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
5.68 + let val elems = (flat o (map TermC.isalist2list)) ts;
5.69 + in TermC.list2isalist (type_of (hd elems)) elems end;
5.70 +(*\------- to I_Model from Model 1b -------/*)
5.71 +(*/------- to I_Model from Model 1a -------\*)
5.72 +fun is_var (Free _) = true
5.73 + | is_var _ = false;
5.74 +
5.75 +(* special handling for lists. ?WN:14.5.03 ??!? *)
5.76 +fun dest_list (d, ts) =
5.77 + let fun dest t =
5.78 + if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
5.79 + then TermC.isalist2list t
5.80 + else [t]
5.81 + in (flat o (map dest)) ts end;
5.82 +
5.83 +(* revert split_dts only for ts; compare comp_dts *)
5.84 +fun comp_ts (d, ts) =
5.85 + if Input_Descript.is_list_dsc d
5.86 + then if TermC.is_list (hd ts)
5.87 + then if Input_Descript.is_unl d
5.88 + then (hd ts) (* e.g. someList [1,3,2] *)
5.89 + else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
5.90 + else (hd ts) (* a variable or metavariable for a list *)
5.91 + else (hd ts);
5.92 +fun comp_dts (d, []) =
5.93 + if Input_Descript.is_reall_dsc d
5.94 + then (d $ e_listReal)
5.95 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
5.96 + | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
5.97 + handle _ => error ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
5.98 +fun comp_dts' (d, []) =
5.99 + if Input_Descript.is_reall_dsc d
5.100 + then (d $ e_listReal)
5.101 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
5.102 + | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
5.103 + handle _ => error ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
5.104 +fun comp_dts'' (d, []) =
5.105 + if Input_Descript.is_reall_dsc d
5.106 + then UnparseC.term (d $ e_listReal)
5.107 + else if Input_Descript.is_booll_dsc d
5.108 + then UnparseC.term (d $ e_listBool)
5.109 + else UnparseC.term d
5.110 + | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
5.111 + handle _ => error ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
5.112 +
5.113 +(* decompose an input into description, terms (ev. elems of lists),
5.114 + and the value for the problem-environment; inv to comp_dts *)
5.115 +fun split_dts (t as d $ arg) =
5.116 + if Input_Descript.is_dsc d
5.117 + then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
5.118 + then (d, take_apart arg)
5.119 + else (d, [arg])
5.120 + else (TermC.empty, TermC.dest_list' t)
5.121 + | split_dts t =
5.122 + let val t' as (h, _) = strip_comb t;
5.123 + in
5.124 + if Input_Descript.is_dsc h
5.125 + then (h, dest_list t')
5.126 + else (TermC.empty, TermC.dest_list' t)
5.127 + end;
5.128 +(* version returning ts only *)
5.129 +fun I_Model.split_dts' (d, arg) =
5.130 + if Input_Descript.is_dsc d
5.131 + then if Input_Descript.is_list_dsc d
5.132 + then if TermC.is_list arg
5.133 + then if Input_Descript.is_unl d
5.134 + then ([arg]) (* e.g. someList [1,3,2] *)
5.135 + else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
5.136 + else ([arg]) (* a variable or metavariable for a list *)
5.137 + else ([arg])
5.138 + else (TermC.dest_list' arg)
5.139 +(* WN170204: Warning "redundant"
5.140 + | I_Model.split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
5.141 + let val (h,argl) = strip_comb t
5.142 + in
5.143 + if (not o is_dsc) h
5.144 + then (dest_list' t)
5.145 + else (dest_list (h,argl))
5.146 + end;*)
5.147 +(* revert split_:
5.148 + WN050903 we do NOT know which is from subtheory, description or term;
5.149 + typecheck thus may lead to TYPE-error 'unknown constant';
5.150 + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
5.151 +(*fun comp_dts thy (d,[]) =
5.152 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
5.153 + (Thy_Info_get_theory "Isac_Knowledge")
5.154 + (*comp_dts:FIXXME stay with term for efficiency !!!*)
5.155 + (if is_reall_dsc d then (d $ e_listReal)
5.156 + else if is_booll_dsc d then (d $ e_listBool)
5.157 + else d)
5.158 + | comp_dts (d,ts) =
5.159 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
5.160 + (Thy_Info_get_theory "Isac_Knowledge")
5.161 + (*comp_dts:FIXXME stay with term for efficiency !!*)
5.162 + (d $ (comp_ts (d, ts)))
5.163 + handle _ => error ("comp_dts: "^(term2str d)^
5.164 + " $ "^(term2str (hd ts))));*)
5.165 +(*\------- to I_Model from Model 1a -------/*)
5.166 +
5.167 +(*/------- to I_Model from Model 1c -------\*)
5.168 +(* 27.8.01: problem-environment
5.169 +WN.6.5.03: FIXXME reconsider if penv is worth the effort --
5.170 + -- just rerun a whole expl with num/var may show the same ?!
5.171 +WN.9.5.03: penv-concept stalled, immediately generate script env !
5.172 + but [#0, epsilon] only outcommented for eventual reconsideration *)
5.173 +type penv = (* problem-environment *)
5.174 + (term (* err_ *)
5.175 + * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
5.176 + ) list;
5.177 +fun pen2str ctxt (t, ts) =
5.178 + pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
5.179 +fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
5.180 +(*\------- to I_Model from Model 1c -------/*)
5.181 +(*/------- to I_Model from Model 1 -------\*)
5.182 +fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
5.183 + "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
5.184 + | feedback_to_string _ (Syn c) = "Syn " ^ c
5.185 + | feedback_to_string _ (Typ c) = "Typ " ^ c
5.186 + | feedback_to_string ctxt (Inc ((d, ts), penv)) =
5.187 + "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
5.188 + | feedback_to_string ctxt (Sup (d, ts)) =
5.189 + "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
5.190 + | feedback_to_string ctxt (Mis (d, pid)) =
5.191 + "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
5.192 + | feedback_to_string _ (Par s) = "Trm "^s;
5.193 +fun feedback_to_string' t = feedback_to_string (ThyC.id_to_ctxt "Isac_Knowledge") t;
5.194 +
5.195 +fun single_to_string ctxt (i, is, b, s, itm_) =
5.196 + "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
5.197 + s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
5.198 +fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
5.199 +
5.200 +(* in CalcTree/Subproblem an 'untouched' model is created
5.201 + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
5.202 +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : single -> int)) itms);
5.203 +(*\------- to I_Model from Model 1 -------/*)
5.204 +
5.205 (**)end(**);
5.206 \ No newline at end of file
6.1 --- a/src/Tools/isac/Specify/input-calchead.sml Tue May 05 09:07:36 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Tue May 05 13:33:23 2020 +0200
6.3 @@ -116,7 +116,7 @@
6.4
6.5 (* re-parse itms with a new thy and prepare for checking with ori list *)
6.6 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
6.7 - (let val t = Model.comp_dts (d, ts)
6.8 + (let val t = I_Model.comp_dts (d, ts)
6.9 val _ = (UnparseC.term_in_thy dI t)
6.10 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
6.11 in itm end
6.12 @@ -130,13 +130,13 @@
6.13 in (i, v, b, f, Model.Par str) end
6.14 handle _ => (i, v, b, f, Model.Syn str))
6.15 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
6.16 - (let val t = Model.comp_dts (d,ts);
6.17 + (let val t = I_Model.comp_dts (d,ts);
6.18 val _ = UnparseC.term_in_thy dI t;
6.19 (*this ^ should raise the exn on unability of re-parsing dts*)
6.20 in itm end
6.21 handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
6.22 | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
6.23 - (let val t = Model.comp_dts (d,ts);
6.24 + (let val t = I_Model.comp_dts (d,ts);
6.25 val _ = UnparseC.term_in_thy dI t;
6.26 (*this ^ should raise the exn on unability of re-parsing dts*)
6.27 in itm end
6.28 @@ -148,7 +148,7 @@
6.29 in itm end
6.30 handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
6.31 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
6.32 - error ("parsitm (" ^ Model.itm2str_ (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
6.33 + error ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
6.34
6.35 (*separate a list to a pair of elements that do NOT satisfy the predicate,
6.36 and of elements that satisfy the predicate, i.e. (false, true)*)
6.37 @@ -196,7 +196,7 @@
6.38 NONE => ([], false, f, Model.Syn str)
6.39 | SOME ct =>
6.40 let
6.41 - val (d, ts) = (Model.split_dts o Thm.term_of) ct
6.42 + val (d, ts) = (I_Model.split_dts o Thm.term_of) ct
6.43 val popt = find_first (eq7 (f, d)) pbt
6.44 in
6.45 case popt of
6.46 @@ -232,15 +232,15 @@
6.47 else oris2itms pbt vat os
6.48
6.49 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
6.50 - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm)
6.51 -fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
6.52 + | par2fstr itm = error ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
6.53 +fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, I_Model.comp_dts'' (d, ts))
6.54 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
6.55 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
6.56 - | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))
6.57 - | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
6.58 + | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, I_Model.comp_dts'' (d,ts))
6.59 + | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, I_Model.comp_dts'' (d, ts))
6.60 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
6.61 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
6.62 - error ("parsitm (" ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
6.63 + error ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
6.64
6.65 fun imodel2fstr iitems =
6.66 let
7.1 --- a/src/Tools/isac/Specify/model.sml Tue May 05 09:07:36 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/model.sml Tue May 05 13:33:23 2020 +0200
7.3 @@ -8,60 +8,67 @@
7.4
7.5 signature MODEL =
7.6 sig
7.7 -(*/------- to O_Model+I_ from ModelModel -------\*)
7.8 type vats = Model_Def.variants
7.9 -(*\------- to O_Model+I_ from ModelModel -------/*)
7.10 -(*/------- to O_Model from Model -------\*)
7.11 +
7.12 type ori = Model_Def.o_model_single
7.13 +(*/------- to O_Model from Model -------\* )
7.14 val oris2str: ori list -> string
7.15 val e_ori: ori
7.16 -(*\------- to O_Model from Model -------/*)
7.17 -(*/------- to I_Model from Model -------\*)
7.18 +( *\------- to O_Model from Model DONE -------/*)
7.19 datatype itm_ = datatype Model_Def.i_model_feedback
7.20 type itm = I_Model.single
7.21 +(*/------- to I_Model from Model DONE -------\* )
7.22 val e_itm : itm
7.23 -(*\------- to I_Model from Model -------/*)
7.24 +( *\------- to I_Model from Model DONE -------/*)
7.25
7.26 datatype item
7.27 = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
7.28 | SyntaxE of string | TypeE of string
7.29 +(*/------- to I_Model from Model 1 -------\* )
7.30 val itm_2str : itm_ -> string
7.31 val itm_2str_ : Proof.context -> itm_ -> string
7.32 val itm2str_ : Proof.context -> itm -> string
7.33 val itms2str_ : Proof.context -> itm list -> string
7.34 + val untouched : itm list -> bool
7.35 +( *\------- to I_Model from Model 1 -------/*)
7.36 type 'a ppc
7.37 val empty_ppc : item ppc
7.38 val ppc2str : {Find: string list, Given: string list, Relate: string list, Where: string list,
7.39 With: string list} -> string
7.40 val itemppc2str : item ppc -> string
7.41
7.42 +(*/------- to I_Model from Model 1a -------\* )
7.43 val comp_dts : term * term list -> term
7.44 val comp_dts' : term * term list -> term
7.45 val comp_dts'' : term * term list -> string
7.46 val comp_ts : term * term list -> term
7.47 val split_dts : term -> term * term list
7.48 val split_dts' : term * term -> term list
7.49 +( *\------- to I_Model from Model 1a -------/*)
7.50 val pbl_ids' : term -> term list -> term list
7.51 val mkval' : term list -> term
7.52
7.53 val d_in : itm_ -> term
7.54 val ts_in : itm_ -> term list
7.55 val penvval_in : itm_ -> term list
7.56 - val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
7.57 val vars_of : itm list -> term list
7.58 val max_vt : itm list -> int
7.59 + val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
7.60
7.61 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.62 +(*/------- to I_Model from Model 1c -------\* )
7.63 type penv
7.64 val penv2str_ : Proof.context -> penv -> string (* NONE *)
7.65 +( *\------- to I_Model from Model 1c -------/*)
7.66 +(*/------- to O_Model from Model 1 -------\* )
7.67 type preori
7.68 val preoris2str : preori list -> string
7.69 +( *\------- to O_Model from Model 1 -------/*)
7.70 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.71 (* NONE *)
7.72 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.73
7.74 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
7.75 - val untouched : itm list -> bool
7.76 type envv
7.77 val upds_envv : Proof.context -> envv -> (vats * term * term * term) list -> envv
7.78 val item_ppc : string ppc -> item ppc
7.79 @@ -113,6 +120,7 @@
7.80 (b)
7.81 ==========================================================================*)
7.82
7.83 +(*/------- to I_Model from Model 1b -------\* )
7.84 val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
7.85 val e_listReal = script_parse "[]::(real list)";
7.86 val e_listBool = script_parse "[]::(bool list)";
7.87 @@ -124,7 +132,9 @@
7.88 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
7.89 let val elems = (flat o (map TermC.isalist2list)) ts;
7.90 in TermC.list2isalist (type_of (hd elems)) elems end;
7.91 +( *\------- to I_Model from Model 1b -------/*)
7.92
7.93 +(*/------- to I_Model from Model 1a -------\* )
7.94 fun is_var (Free _) = true
7.95 | is_var _ = false;
7.96
7.97 @@ -218,7 +228,9 @@
7.98 (d $ (comp_ts (d, ts)))
7.99 handle _ => error ("comp_dts: "^(term2str d)^
7.100 " $ "^(term2str (hd ts))));*)
7.101 +( *\------- to I_Model from Model 1a -------/*)
7.102
7.103 +(*/------- to I_Model from Model 1c -------\*)
7.104 (* 27.8.01: problem-environment
7.105 WN.6.5.03: FIXXME reconsider if penv is worth the effort --
7.106 -- just rerun a whole expl with num/var may show the same ?!
7.107 @@ -231,6 +243,7 @@
7.108 fun pen2str ctxt (t, ts) =
7.109 pair2str (UnparseC.term_in_ctxt ctxt t, (strs2str' o map (UnparseC.term_in_ctxt ctxt)) ts);
7.110 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
7.111 +(*\------- to I_Model from Model 1c -------/*)
7.112
7.113 (* get the constant value from a penv *)
7.114 fun getval (id, values) =
7.115 @@ -255,7 +268,7 @@
7.116 type vats = Model_Def.variants;
7.117 (*\------- to O_Model+I_ from Model -------/*)
7.118
7.119 -(*/------- to I_Model from Model -------\*)
7.120 +(*/------- to I_Model from Model DONE -------\*)
7.121 (* the internal representation of a models' item
7.122 4.9.01: not consistent:
7.123 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
7.124 @@ -273,11 +286,7 @@
7.125 string * (* #Given | #Find | #Relate *)
7.126 itm_; (* *)
7.127 val e_itm = (0, [], false, "e_itm", Syn "e_itm");
7.128 -(*\------- to I_Model from Model -------/*)
7.129 -
7.130 -(* in CalcTree/Subproblem an 'untouched' model is created
7.131 - FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
7.132 -fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
7.133 +(*\------- to I_Model from Model DONE -------/*)
7.134
7.135 (* find most frequent variant v in itms *)
7.136 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);
7.137 @@ -322,15 +331,17 @@
7.138 val oris2str = Model_Def.o_model_to_string;
7.139 (*\------- to O_Model from Model -------/*)
7.140
7.141 +(*/------- to O_Model from Model 1 -------\* )
7.142 (* an or without leading integer *)
7.143 type preori = (vats * string * term * term list);
7.144 fun preori2str (vs, fi, t, ts) =
7.145 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
7.146 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
7.147 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
7.148 +( *\------- to O_Model from Model 1 -------/*)
7.149
7.150 (* 9.5.03 penv postponed: pbl_ids' *)
7.151 -fun pbl_ids' d vs = [comp_ts (d, vs)];
7.152 +fun pbl_ids' d vs = [I_Model.comp_ts (d, vs)];
7.153
7.154 (* 14.9.01: not used after putting values for penv into itm_
7.155 WN.5.5.03: used in upd .. upd_envv *)
7.156 @@ -382,6 +393,7 @@
7.157 | item2str (Superfl s) = "Superfl " ^ s
7.158 | item2str (Missing s) = "Missing " ^ s;
7.159
7.160 +(*/------- to I_Model from Model 1 -------\* )
7.161 fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
7.162 "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
7.163 | itm_2str_ _ (Syn c) = "Syn " ^ c
7.164 @@ -399,6 +411,11 @@
7.165 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
7.166 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
7.167 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
7.168 +
7.169 +(* in CalcTree/Subproblem an 'untouched' model is created
7.170 + FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)
7.171 +fun untouched itms = foldl and_ (true , map ((curry op = 0) o (#1 : itm -> int)) itms);
7.172 +( *\------- to I_Model from Model 1 -------/*)
7.173 fun init_item str = SyntaxE str;
7.174
7.175 type 'a ppc =
7.176 @@ -439,7 +456,7 @@
7.177 | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
7.178
7.179 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
7.180 -fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
7.181 +fun penvval_in (Cor ((d, _), (_, ts))) = [I_Model.comp_ts (d,ts)]
7.182 | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
7.183 | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
7.184 | penvval_in (Inc (_, (_, ts))) = ts
8.1 --- a/src/Tools/isac/Specify/o-model.sml Tue May 05 09:07:36 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/o-model.sml Tue May 05 13:33:23 2020 +0200
8.3 @@ -5,14 +5,23 @@
8.4
8.5 signature ORIGINAL_MODEL =
8.6 sig
8.7 +(* vats*)
8.8 type variants = Model_Def.variants
8.9 +(* ori list*)
8.10 type T = Model_Def.o_model
8.11 +(* ori *)
8.12 type single = Model_Def.o_model_single
8.13 -
8.14 +(* oris2str*)
8.15 val to_string: T -> string
8.16 +(* e_ori*)
8.17 val single_empty: single
8.18
8.19 +(*/------- to O_Model from Model 1 -------\*)
8.20 + type preori
8.21 +(*\------- to O_Model from Model 1 -------/*)
8.22 +
8.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.24 + val preoris2str : preori list -> string
8.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.26 (* NONE *)
8.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.28 @@ -28,5 +37,14 @@
8.29 val single_empty = Model_Def.o_model_empty;
8.30 val to_string = Model_Def.o_model_to_string;
8.31
8.32 +(*/------- to O_Model from Model 1 -------\*)
8.33 +(* an or without leading integer *)
8.34 +type preori = (variants * string * term * term list);
8.35 +fun preori2str (vs, fi, t, ts) =
8.36 + "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
8.37 + UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
8.38 +val preoris2str = (strs2str' o (map (linefeed o preori2str)));
8.39 +(*\------- to O_Model from Model 1 -------/*)
8.40 +
8.41
8.42 (**)end(**);
8.43 \ No newline at end of file
9.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue May 05 09:07:36 2020 +0200
9.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200
9.3 @@ -151,11 +151,11 @@
9.4 type field = string * (term * term)
9.5 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
9.6
9.7 -fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (Model.comp_dts (d, ts)))
9.8 +fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
9.9 | itm_2item _ (Model.Syn c) = Model.SyntaxE c
9.10 | itm_2item _ (Model.Typ c) = Model.TypeE c
9.11 - | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (Model.comp_dts (d, ts)))
9.12 - | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (Model.comp_dts (d, ts)))
9.13 + | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
9.14 + | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
9.15 | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
9.16 | itm_2item _ _ = error "itm_2item: uncovered definition"
9.17
9.18 @@ -184,11 +184,11 @@
9.19 in (hd, arg) end
9.20
9.21 (*create output-string for itm_*)
9.22 -fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts))
9.23 +fun itm_out _ (Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
9.24 | itm_out _ (Model.Syn c) = c
9.25 | itm_out _ (Model.Typ c) = c
9.26 - | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (Model.comp_dts (d, ts))
9.27 - | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (Model.comp_dts (d, ts))
9.28 + | itm_out _ (Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
9.29 + | itm_out _ (Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
9.30 | itm_out _ (Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
9.31 | itm_out _ _ = error "itm_out: uncovered definition"
9.32
9.33 @@ -275,7 +275,7 @@
9.34 | prep_ori fmz thy pbt =
9.35 let
9.36 val ctxt = ContextC.initialise' thy fmz;
9.37 - val ori = map (add_field thy pbt o Model.split_dts o TermC.parseNEW' ctxt) fmz
9.38 + val ori = map (add_field thy pbt o I_Model.split_dts o TermC.parseNEW' ctxt) fmz
9.39 |> add_variants;
9.40 val maxv = map fst ori |> max;
9.41 val maxv = if maxv = 0 then 1 else maxv;
10.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 09:07:36 2020 +0200
10.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue May 05 13:33:23 2020 +0200
10.3 @@ -399,11 +399,11 @@
10.4 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
10.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
10.6 (*val nxt = ("Model_Problem", ...*)
10.7 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.8 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.9
10.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.11 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
10.12 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.13 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.14 (*[
10.15 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
10.16 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
10.17 @@ -412,7 +412,7 @@
10.18
10.19 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
10.20 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, Spec.empty);
10.21 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.22 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.23 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";
10.24
10.25 (*there is one input to the model (could be more)*)
10.26 @@ -420,7 +420,7 @@
10.27 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
10.28 Find ["maximum", "valuesFor"],
10.29 Relate ["relations"]], Pbl, Spec.empty);
10.30 - val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.31 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.32 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 ()
10.33 else error "informtest.sml: diff.behav. max 2";
10.34
10.35 @@ -430,7 +430,7 @@
10.36 Find ["maximum A", "valuesFor [a,b]"],
10.37 Relate ["relations [A=a*b, a/2=r*sin alpha, \
10.38 \b/2=r*cos alpha]"]], Pbl, Spec.empty);
10.39 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.40 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.41 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
10.42
10.43 (*this input is complete in variant 1 (variant 3 does not work yet)*)
10.44 @@ -440,7 +440,7 @@
10.45 Relate ["relations [A=a*b, \
10.46 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
10.47 Pbl, Spec.empty);
10.48 - val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
10.49 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
10.50
10.51 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
10.52 *)
10.53 @@ -655,8 +655,8 @@
10.54 (*default_print_depth 5;*)
10.55 writeln"-----------------------------------------------------------";
10.56 spec;
10.57 -writeln (itms2str_ ctxt probl);
10.58 -writeln (itms2str_ ctxt meth);
10.59 +writeln (I_Model.to_string ctxt probl);
10.60 +writeln (I_Model.to_string ctxt meth);
10.61 writeln (Istate.string_of (fst istate));
10.62
10.63 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
10.64 @@ -677,12 +677,12 @@
10.65 (*("Isac_Knowledge",
10.66 ["derivative_of", "function"],
10.67 ["diff", "differentiate_on_R"]) : spec*)
10.68 -writeln (itms2str_ ctxt probl);
10.69 +writeln (I_Model.to_string ctxt probl);
10.70 (*[
10.71 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
10.72 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
10.73 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
10.74 -writeln (itms2str_ ctxt meth);
10.75 +writeln (I_Model.to_string ctxt meth);
10.76 (*[
10.77 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
10.78 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
10.79 @@ -720,12 +720,12 @@
10.80 (*("Isac_Knowledge",
10.81 ["derivative_of", "function"],
10.82 ["diff", "differentiate_on_R"]) : spec*)
10.83 -writeln (itms2str_ ctxt probl);
10.84 +writeln (I_Model.to_string ctxt probl);
10.85 (*[
10.86 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
10.87 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
10.88 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
10.89 -writeln (itms2str_ ctxt meth);
10.90 +writeln (I_Model.to_string ctxt meth);
10.91 (*[
10.92 (1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
10.93 (2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
10.94 @@ -1253,7 +1253,7 @@
10.95 (#1 (some_spec ospec spec), oris, []:itm list,
10.96 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
10.97 val iii = appl_adds dI oris ppc pbt (selct::ss);
10.98 - tracing(itms2str_ thy iii);
10.99 + tracing(I_Model.to_string thy iii);
10.100
10.101 val itm = appl_add' dI oris ppc pbt selct;
10.102 val ppc = insert_ppc' itm ppc;
10.103 @@ -1265,7 +1265,7 @@
10.104 val _::selct::ss = (selct::ss);
10.105 val itm = appl_add' dI oris ppc pbt selct;
10.106 val ppc = insert_ppc' itm ppc;
10.107 - tracing(itms2str_ thy ppc);
10.108 + tracing(I_Model.to_string thy ppc);
10.109
10.110 val _::selct::ss = (selct::ss);
10.111 val itm = appl_add' dI oris ppc pbt selct;
11.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 05 09:07:36 2020 +0200
11.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 05 13:33:23 2020 +0200
11.3 @@ -96,8 +96,8 @@
11.4 (5, ["1"], #undef,FunktionsVariable, ["x"]),
11.5 (6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
11.6 (7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
11.7 -(*+*)itms2str_ @{context} probl = "[]";
11.8 -(*+*)itms2str_ @{context} meth = "[]";
11.9 +(*+*)I_Model.to_string @{context} probl = "[]";
11.10 +(*+*)I_Model.to_string @{context} meth = "[]";
11.11 (*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
11.12
11.13 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
11.14 @@ -207,15 +207,15 @@
11.15 (1, ["1"], #Given,Streckenlast, ["q_0"]),
11.16 (2, ["1"], #Given,FunktionsVariable, ["x"]),
11.17 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
11.18 -(*+*)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''']))]"
11.19 +(*+*)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''']))]"
11.20 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
11.21 -writeln (itms2str_ @{context} probl); (*[
11.22 +writeln (I_Model.to_string @{context} probl); (*[
11.23 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
11.24 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
11.25 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
11.26 -(*+*)if itms2str_ @{context} meth = "[]"
11.27 +(*+*)if I_Model.to_string @{context} meth = "[]"
11.28 (*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
11.29 -writeln (itms2str_ @{context} meth); (*[]*)
11.30 +writeln (I_Model.to_string @{context} meth); (*[]*)
11.31
11.32 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
11.33 (* val (pt, p) = *)
11.34 @@ -258,7 +258,7 @@
11.35 val met = if met = [] then pbl else met
11.36 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
11.37 ;
11.38 -(*+*)writeln (itms2str_ @{context} itms); (*[
11.39 +(*+*)writeln (I_Model.to_string @{context} itms); (*[
11.40 (1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
11.41 (2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
11.42 (3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
12.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue May 05 09:07:36 2020 +0200
12.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue May 05 13:33:23 2020 +0200
12.3 @@ -282,10 +282,10 @@
12.4 | _ => error "diffapp.sml: max-exp me, nxt = Specify_Method";
12.5
12.6 val oris = fst3 (get_obj g_origin pt (fst p)); writeln(O_Model.to_string oris);
12.7 -val pits = get_obj g_pbl pt (fst p); writeln(itms2str_ ctxt pits);
12.8 +val pits = get_obj g_pbl pt (fst p); writeln(I_Model.to_string ctxt pits);
12.9
12.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.11 -val mits = get_obj g_met pt (fst p); writeln(itms2str_ ctxt mits);
12.12 +val mits = get_obj g_met pt (fst p); writeln(I_Model.to_string ctxt mits);
12.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.15 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.16 @@ -313,7 +313,7 @@
12.17 === inhibit exn 110722=============================================================*)
12.18
12.19 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
12.20 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.21 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
12.22
12.23 (*=== inhibit exn 110722=============================================================
12.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.25 @@ -348,7 +348,7 @@
12.26 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
12.27
12.28 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
12.29 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.30 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
12.31
12.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.34 @@ -383,11 +383,11 @@
12.35
12.36 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
12.37
12.38 -val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits);
12.39 -val pits = get_obj g_pbl pt [];writeln(itms2str_ ctxt pits);
12.40 +val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
12.41 +val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits);
12.42
12.43 -val mits = get_obj g_met pt (fst p);writeln(itms2str_ ctxt mits);
12.44 -val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
12.45 +val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string ctxt mits);
12.46 +val mits = get_obj g_met pt [];writeln(I_Model.to_string ctxt mits);
12.47
12.48 (*=== inhibit exn 110722=============================================================
12.49 arguments_from_model ["DiffApp","max_by_calculus"] mits;
12.50 @@ -434,14 +434,14 @@
12.51 fetchProposedTactic 1;
12.52 val ((pt,p),_) = get_calc 1;
12.53 val mits = get_obj g_met pt (fst p);
12.54 - writeln (itms2str_ ctxt mits);
12.55 + writeln (I_Model.to_string ctxt mits);
12.56 (*
12.57 - 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 ()
12.58 + 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 ()
12.59 else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
12.60 *)
12.61 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
12.62 (* WN051209 while extending 'fun step' for initac, this became better ...
12.63 - 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 ()
12.64 + 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 ()
12.65 else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
12.66 *)
12.67
13.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue May 05 09:07:36 2020 +0200
13.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue May 05 13:33:23 2020 +0200
13.3 @@ -460,7 +460,7 @@
13.4 =========================================================================/
13.5
13.6 -----fun refin' ff:
13.7 -> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
13.8 +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
13.9 [
13.10 (1 ,[1] ,true ,#Given ,Cor equalities
13.11 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
13.12 @@ -475,7 +475,7 @@
13.13 (true, length_ [c, c_2] = 2)]
13.14
13.15 ----- fun match_oris':
13.16 -> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
13.17 +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
13.18 > (writeln o pres2str) pre';
13.19 ..as in refin'
13.20
13.21 @@ -542,7 +542,7 @@
13.22
13.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.24 val PblObj {probl,...} = get_obj I pt [5];
13.25 - (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
13.26 + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
13.27 (*[
13.28 (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]])),
13.29 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
13.30 @@ -610,7 +610,7 @@
13.31
13.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.33 val PblObj {probl,...} = get_obj I pt [5];
13.34 - (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
13.35 + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
13.36 (*[
13.37 (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]])),
13.38 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
14.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue May 05 09:07:36 2020 +0200
14.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue May 05 13:33:23 2020 +0200
14.3 @@ -615,7 +615,7 @@
14.4 (*[], 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))"*)
14.5 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
14.6
14.7 -(*+*)if itms2str_ ctxt (get_obj g_pbl pt (fst p)) =
14.8 +(*+*)if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
14.9 (*+*) "[\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)]))]"
14.10 (*+*)then () else error "No.267b: itm list CHANGED";
14.11
15.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 09:07:36 2020 +0200
15.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue May 05 13:33:23 2020 +0200
15.3 @@ -6,7 +6,7 @@
15.4 "table of contents -----------------------------------------------------------------------------";
15.5 "-----------------------------------------------------------------------------------------------";
15.6 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
15.7 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
15.8 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
15.9 "----------- type penv -------------------------------------------------------------------------";
15.10 "----------- fun untouched ---------------------------------------------------------------------";
15.11 "----------- fun pbl_ids -----------------------------------------------------------------------";
15.12 @@ -79,8 +79,8 @@
15.13 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
15.14 val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
15.15 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
15.16 -val (d, ts) = split_dts t;
15.17 -"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
15.18 +val (d, ts) = I_Model.split_dts t;
15.19 +"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
15.20 (*if is_dsc d then () else error "TODO";*)
15.21 if is_dsc d then () else error "TODO";
15.22 "----- these were the errors (call hierarchy from bottom up)";
15.23 @@ -96,60 +96,60 @@
15.24 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
15.25 ========== inhibit exn AK110725 ================================================*)
15.26
15.27 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
15.28 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
15.29 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
15.30 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
15.31 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
15.32 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
15.33 (*val t = str2term "maximum A";
15.34 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.35 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.36 val it = "maximum A" : cterm
15.37 > val t = str2term "fixedValues [r=Arbfix]";
15.38 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.39 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.40 "fixedValues [r = Arbfix]"
15.41 > val t = str2term "valuesFor [a]";
15.42 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.43 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.44 "valuesFor [a]"
15.45 > val t = str2term "valuesFor [a,b]";
15.46 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.47 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.48 "valuesFor [a, b]"
15.49 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
15.50 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.51 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.52 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
15.53 > val t = str2term "boundVariable a";
15.54 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.55 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.56 "boundVariable a"
15.57 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
15.58 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.59 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.60 "interval {x. 0 <= x & x <= 2 * r}"
15.61
15.62 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
15.63 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.64 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.65 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
15.66 > val t = str2term "solveFor x";
15.67 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.68 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.69 "solveFor x"
15.70 > val t = str2term "errorBound (eps=0)";
15.71 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.72 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.73 "errorBound (eps = 0)"
15.74 > val t = str2term "solutions L";
15.75 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
15.76 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
15.77 "solutions L"
15.78
15.79 before 6.5.03:
15.80 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
15.81 -> val (d,ts) = split_dts t;
15.82 +> val (d,ts) = I_Model.split_dts t;
15.83 > comp_dts thy (d,ts);
15.84 val it = "testdscforlist [#1]" : cterm
15.85
15.86 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
15.87 -> val (d,ts) = split_dts t;
15.88 +> val (d,ts) = I_Model.split_dts t;
15.89 val d = Const ("empty","empty") : term
15.90 val ts = [Free ("A","RealDef.real")] : term list
15.91 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
15.92 -> val (d,ts) = split_dts t;
15.93 +> val (d,ts) = I_Model.split_dts t;
15.94 val d = Const ("empty","empty") : term
15.95 val ts = [Const # $ Free # $ Free (#,#)] : term list
15.96 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
15.97 -> val (d,ts) = split_dts t;
15.98 +> val (d,ts) = I_Model.split_dts t;
15.99 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
15.100 *)
15.101 "----------- type penv -------------------------------------------------------------------------";
15.102 @@ -189,7 +189,7 @@
15.103
15.104 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
15.105 val (d,argl) = strip_comb t;
15.106 - is_dsc d; (*see split_dts*)
15.107 + is_dsc d; (*see I_Model.split_dts*)
15.108 dest_list (d,argl);
15.109 val (_ $ v) = t;
15.110 is_list v;
15.111 @@ -197,7 +197,7 @@
15.112 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
15.113 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
15.114
15.115 - val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
15.116 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
15.117 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term
15.118 val vl = Free ("x","RealDef.real") : term
15.119
15.120 @@ -205,7 +205,7 @@
15.121 pbl_ids ctxt dsc vl;
15.122 val it = [Free ("x","RealDef.real")] : term list
15.123
15.124 - val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy))
15.125 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy))
15.126 "errorBound (eps=#0)";
15.127 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
15.128 pbl_ids ctxt dsc vl;
16.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Tue May 05 09:07:36 2020 +0200
16.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Tue May 05 13:33:23 2020 +0200
16.3 @@ -66,7 +66,7 @@
16.4 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
16.5
16.6 val pt = EmptyPtree;
16.7 -val pt = append_problem [] (Istate.empty, ContextC.empty) Celem.Formalise.empty ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt;
16.8 +val pt = append_problem [] (Istate.empty, ContextC.empty) Formalise.empty ([(*oris*)], Spec.empty, TermC.empty, ContextC.empty) pt;
16.9 val ctxt = get_obj g_ctxt pt [];
16.10 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
16.11
16.12 @@ -81,13 +81,13 @@
16.13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.15 (* nxt = Add_Given "equality (x + 1 = 2)"
16.16 - (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.17 + (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.18 *)
16.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.20 -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.21 +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.22 *)
16.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.24 -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.25 +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.26 *)
16.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.29 @@ -453,13 +453,13 @@
16.30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.32 (* nxt = Add_Given "equality (x + 1 = 2)"
16.33 - (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.34 + (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.35 *)
16.36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.37 -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.38 +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.39 *)
16.40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.41 -(* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
16.42 +(* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
16.43 *)
16.44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
16.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.1 --- a/test/Tools/isac/MathEngBasic/model.sml Tue May 05 09:07:36 2020 +0200
17.2 +++ b/test/Tools/isac/MathEngBasic/model.sml Tue May 05 13:33:23 2020 +0200
17.3 @@ -43,7 +43,7 @@
17.4
17.5
17.6 val env = []:envv;
17.7 - val (d,ts) = (split_dts o Thm.term_of o the o (parse thy))
17.8 + val (d,ts) = (I_Model.split_dts o Thm.term_of o the o (parse thy))
17.9 "fixedValues [r=Arbfix]";
17.10 val (_,id) = (split_did o Thm.term_of o the o (parse thy))"fixedValues fix_";
17.11 val vats = [1,2,3];
18.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 09:07:36 2020 +0200
18.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue May 05 13:33:23 2020 +0200
18.3 @@ -6,7 +6,7 @@
18.4 "table of contents -----------------------------------------------------------------------------";
18.5 "-----------------------------------------------------------------------------------------------";
18.6 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
18.7 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
18.8 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
18.9 "----------- type penv -------------------------------------------------------------------------";
18.10 "----------- fun untouched ---------------------------------------------------------------------";
18.11 "----------- fun pbl_ids -----------------------------------------------------------------------";
18.12 @@ -79,8 +79,8 @@
18.13 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
18.14 val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
18.15 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
18.16 -val (d, ts) = split_dts t;
18.17 -"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
18.18 +val (d, ts) = I_Model.split_dts t;
18.19 +"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
18.20 (*if is_dsc d then () else error "TODO";*)
18.21 if is_dsc d then () else error "TODO";
18.22 "----- these were the errors (call hierarchy from bottom up)";
18.23 @@ -96,60 +96,60 @@
18.24 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
18.25 ========== inhibit exn AK110725 ================================================*)
18.26
18.27 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
18.28 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
18.29 -"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
18.30 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
18.31 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
18.32 +"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
18.33 (*val t = str2term "maximum A";
18.34 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.35 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.36 val it = "maximum A" : cterm
18.37 > val t = str2term "fixedValues [r=Arbfix]";
18.38 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.39 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.40 "fixedValues [r = Arbfix]"
18.41 > val t = str2term "valuesFor [a]";
18.42 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.43 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.44 "valuesFor [a]"
18.45 > val t = str2term "valuesFor [a,b]";
18.46 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.47 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.48 "valuesFor [a, b]"
18.49 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
18.50 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.51 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.52 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
18.53 > val t = str2term "boundVariable a";
18.54 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.55 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.56 "boundVariable a"
18.57 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
18.58 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.59 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.60 "interval {x. 0 <= x & x <= 2 * r}"
18.61
18.62 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
18.63 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.64 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.65 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
18.66 > val t = str2term "solveFor x";
18.67 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.68 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.69 "solveFor x"
18.70 > val t = str2term "errorBound (eps=0)";
18.71 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.72 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.73 "errorBound (eps = 0)"
18.74 > val t = str2term "solutions L";
18.75 -> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);
18.76 +> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
18.77 "solutions L"
18.78
18.79 before 6.5.03:
18.80 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
18.81 -> val (d,ts) = split_dts t;
18.82 +> val (d,ts) = I_Model.split_dts t;
18.83 > comp_dts thy (d,ts);
18.84 val it = "testdscforlist [#1]" : cterm
18.85
18.86 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
18.87 -> val (d,ts) = split_dts t;
18.88 +> val (d,ts) = I_Model.split_dts t;
18.89 val d = Const ("empty","empty") : term
18.90 val ts = [Free ("A","RealDef.real")] : term list
18.91 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
18.92 -> val (d,ts) = split_dts t;
18.93 +> val (d,ts) = I_Model.split_dts t;
18.94 val d = Const ("empty","empty") : term
18.95 val ts = [Const # $ Free # $ Free (#,#)] : term list
18.96 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
18.97 -> val (d,ts) = split_dts t;
18.98 +> val (d,ts) = I_Model.split_dts t;
18.99 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
18.100 *)
18.101 "----------- type penv -------------------------------------------------------------------------";
18.102 @@ -189,7 +189,7 @@
18.103
18.104 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
18.105 val (d,argl) = strip_comb t;
18.106 - is_dsc d; (*see split_dts*)
18.107 + is_dsc d; (*see I_Model.split_dts*)
18.108 dest_list (d,argl);
18.109 val (_ $ v) = t;
18.110 is_list v;
18.111 @@ -197,7 +197,7 @@
18.112 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
18.113 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
18.114
18.115 - val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
18.116 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
18.117 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term
18.118 val vl = Free ("x","RealDef.real") : term
18.119
18.120 @@ -205,7 +205,7 @@
18.121 pbl_ids ctxt dsc vl;
18.122 val it = [Free ("x","RealDef.real")] : term list
18.123
18.124 - val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy))
18.125 + val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy))
18.126 "errorBound (eps=#0)";
18.127 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
18.128 pbl_ids ctxt dsc vl;
19.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 09:07:36 2020 +0200
19.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 05 13:33:23 2020 +0200
19.3 @@ -82,7 +82,7 @@
19.4 (thy, ori, (hd icl));
19.5 "~~~~~ to return val:"; val xxx =
19.6 ( fd,
19.7 - ((UnparseC.term_in_thy thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string
19.8 + ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string
19.9 );
19.10 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
19.11
20.1 --- a/test/Tools/isac/Specify/calchead.sml Tue May 05 09:07:36 2020 +0200
20.2 +++ b/test/Tools/isac/Specify/calchead.sml Tue May 05 13:33:23 2020 +0200
20.3 @@ -97,7 +97,7 @@
20.4 val ("dummy", ([(Add_Relation "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]", _, _)], _, ptp))
20.5 = Step.specify_do_next ptp;
20.6 val PblObj {probl, ...} = get_obj I (fst ptp) [];
20.7 -if itms2str_ @{context} probl =
20.8 +if I_Model.to_string @{context} probl =
20.9 "[\n"
20.10 ^ "(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n"
20.11 ^ "(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n"
20.12 @@ -191,7 +191,7 @@
20.13
20.14 (*val nxt = Specify_Theory "DiffApp" : tac*)
20.15
20.16 -val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
20.17 +val itms = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt itms);
20.18
20.19 val nxt = tac2tac_ pt p nxt;
20.20 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
20.21 @@ -542,7 +542,7 @@
20.22 val (thy, (str, (dsc, _)): Celem4.pat, ty $ var) = (thy, p, a);
20.23 val ttt = (dsc $ var);
20.24 Thm.global_cterm_of thy (dsc $ var);
20.25 -val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
20.26 +val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
20.27
20.28 "-d2-----------------------------------------------------";
20.29 pbt = []; (*false*)
20.30 @@ -555,7 +555,7 @@
20.31 val (thy, (str, (dsc, _)):Celem4.pat, ty $ var) = (thy, p, a);
20.32 val ttt = (dsc $ var);
20.33 Thm.global_cterm_of thy (dsc $ var);
20.34 -val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
20.35 +val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
20.36 "-d3-----------------------------------------------------";
20.37 pbt = []; (*true, base case*)
20.38 "-----------------continue step through code match_ags---";
21.1 --- a/test/Tools/isac/Specify/ptyps.sml Tue May 05 09:07:36 2020 +0200
21.2 +++ b/test/Tools/isac/Specify/ptyps.sml Tue May 05 13:33:23 2020 +0200
21.3 @@ -34,20 +34,20 @@
21.4 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
21.5
21.6 (*case 1: no refinement *)
21.7 -val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
21.8 -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
21.9 +val (d1,ts1) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
21.10 +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
21.11 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
21.12
21.13 (*case 2: refined to pbt without children *)
21.14 -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
21.15 +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
21.16 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
21.17
21.18 (*case 3: refined to pbt with children *)
21.19 -val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
21.20 +val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
21.21 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
21.22
21.23 (*case 4: refined to children (without child)*)
21.24 -val (d3,ts3) = split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
21.25 +val (d3,ts3) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
21.26 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
21.27
21.28 (*=================================================================
22.1 --- a/test/Tools/isac/Specify/specify.sml Tue May 05 09:07:36 2020 +0200
22.2 +++ b/test/Tools/isac/Specify/specify.sml Tue May 05 13:33:23 2020 +0200
22.3 @@ -37,7 +37,7 @@
22.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.5 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
22.6 val pits = get_obj g_pbl pt (fst p);
22.7 - writeln (itms2str_ ctxt pits);
22.8 + writeln (I_Model.to_string ctxt pits);
22.9 (*[
22.10 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
22.11 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
22.12 @@ -45,9 +45,9 @@
22.13 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
22.14 val (pt,p) = complete_mod (pt,p);
22.15 val pits = get_obj g_pbl pt (fst p);
22.16 - 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]]))]"
22.17 + 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]]))]"
22.18 then () else error "completetest.sml: new behav. in complete_mod 3";
22.19 - writeln (itms2str_ ctxt pits);
22.20 + writeln (I_Model.to_string ctxt pits);
22.21 (*[
22.22 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
22.23 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
22.24 @@ -55,9 +55,9 @@
22.25 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
22.26 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
22.27 val mits = get_obj g_met pt (fst p);
22.28 - 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]))]"
22.29 + 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]))]"
22.30 then () else error "completetest.sml: new behav. in complete_mod 3";
22.31 - writeln (itms2str_ ctxt mits);
22.32 + writeln (I_Model.to_string ctxt mits);
22.33 (*[
22.34 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
22.35 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
22.36 @@ -112,7 +112,7 @@
22.37 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
22.38 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
22.39 val pits = get_obj g_pbl pt (fst p);
22.40 - writeln (itms2str_ ctxt pits);
22.41 + writeln (I_Model.to_string ctxt pits);
22.42 (*[
22.43 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
22.44 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
22.45 @@ -122,7 +122,7 @@
22.46 val mits = get_obj g_met pt (fst p);
22.47 val mits = complete_metitms oris pits []
22.48 ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
22.49 - writeln (itms2str_ ctxt mits);
22.50 + writeln (I_Model.to_string ctxt mits);
22.51 (*[
22.52 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
22.53 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
22.54 @@ -133,7 +133,7 @@
22.55 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
22.56 0 <= x & x <= 2 * r}])),
22.57 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
22.58 -if itms2str_ ctxt mits
22.59 +if I_Model.to_string ctxt mits
22.60 = "[\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 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
22.61 then () else error "completetest.sml: new behav. in complete_metitms 1";
22.62