1.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu May 07 12:15:37 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu May 07 14:11:03 2020 +0200
1.3 @@ -7,12 +7,9 @@
1.4 signature MODEL_PATTERN =
1.5 sig
1.6 type T
1.7 -(*type pat*)
1.8 type single
1.9 -(*val pats2str: single list -> string*)
1.10 val to_string: single list -> string
1.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.12 -(*val pats2str': single list -> string*)
1.13 val to_string': single list -> string
1.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.15 (*NONE*)
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 07 12:15:37 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 07 14:11:03 2020 +0200
2.3 @@ -345,16 +345,16 @@
2.4 in filt end;
2.5
2.6 fun xml_of_itm_ (I_Model.Cor (dts, _)) =
2.7 - XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (I_Model.comp_dts' dts)])
2.8 + XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (O_Model.comp_dts' dts)])
2.9 | xml_of_itm_ (I_Model.Syn c) =
2.10 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
2.11 | xml_of_itm_ (I_Model.Typ c) =
2.12 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
2.13 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
2.14 | xml_of_itm_ (I_Model.Inc (dts, _)) =
2.15 - XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (I_Model.comp_dts' dts)])
2.16 + XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (O_Model.comp_dts' dts)])
2.17 | xml_of_itm_ (I_Model.Sup dts) =
2.18 - XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (I_Model.comp_dts' dts)])
2.19 + XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (O_Model.comp_dts' dts)])
2.20 | xml_of_itm_ (I_Model.Mis (d, pid)) =
2.21 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
2.22 | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
3.1 --- a/src/Tools/isac/Specify/calchead.sml Thu May 07 12:15:37 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu May 07 14:11:03 2020 +0200
3.3 @@ -191,7 +191,7 @@
3.4 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
3.5 fun oris2fmz_vals oris =
3.6 let fun ori2fmz_vals (_, _, _, dsc, ts) =
3.7 - ((UnparseC.term o I_Model.comp_dts') (dsc, ts), last_elem ts)
3.8 + ((UnparseC.term o O_Model.comp_dts') (dsc, ts), last_elem ts)
3.9 handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)
3.10 in (split_list o (map ori2fmz_vals)) oris end
3.11
3.12 @@ -208,7 +208,7 @@
3.13 WN.11.03: + dont take first inter<>[] *)
3.14 fun seek_oridts ctxt sel (d, ts) [] =
3.15 ("seek_oridts: input ('" ^
3.16 - (UnparseC.term_in_ctxt ctxt (I_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
3.17 + (UnparseC.term_in_ctxt ctxt (O_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
3.18 (0, [], sel, d, ts),
3.19 [])
3.20 | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
3.21 @@ -279,13 +279,13 @@
3.22
3.23 (* get the first term in ts from ori *)
3.24 fun getr_ct thy (_, _, fd, d, ts) =
3.25 - (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d,[hd ts]))
3.26 + (fd, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d,[hd ts]))
3.27
3.28 (* get a term from ori, notyet input in itm.
3.29 the term from ori is thrown back to a string in order to reuse
3.30 machinery for immediate input by the user. *)
3.31 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
3.32 - (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts))
3.33 + (fd, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts))
3.34
3.35 (* in FE dsc, not dat: this is in itms ...*)
3.36 fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
3.37 @@ -306,7 +306,7 @@
3.38 case find_first (test_d d) itms of SOME _ => true | NONE => false
3.39 in
3.40 case filter_out (is_elem itms) pbt of
3.41 - (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, []))
3.42 + (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d, []))
3.43 | _ => NONE
3.44 end
3.45 | nxt_add thy oris _ itms =
3.46 @@ -451,7 +451,7 @@
3.47
3.48 fun test_types ctxt (d,ts) =
3.49 let
3.50 - val opt = (try I_Model.comp_dts) (d, ts)
3.51 + val opt = (try O_Model.comp_dts) (d, ts)
3.52 val msg = case opt of
3.53 SOME _ => ""
3.54 | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
3.55 @@ -465,7 +465,7 @@
3.56 let
3.57 val ots = (distinct o flat o (map #5)) ori
3.58 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
3.59 - val (d, ts) = I_Model.split_dts t
3.60 + val (d, ts) = O_Model.split_dts t
3.61 val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
3.62 in
3.63 if (subtract op = oids ids) <> []
3.64 @@ -504,7 +504,7 @@
3.65 case TermC.parseNEW ctxt ct of
3.66 NONE => Add (i, [], false, sel, I_Model.Syn ct)
3.67 | SOME t =>
3.68 - let val (d, ts) = I_Model.split_dts t
3.69 + let val (d, ts) = O_Model.split_dts t
3.70 in
3.71 if d = TermC.empty
3.72 then Add (i, [], false, sel, I_Model.Mis (Specify.dsc_unknown, hd ts))
3.73 @@ -563,7 +563,7 @@
3.74 fun mtc thy (str, (dsc, _)) (ty $ var) =
3.75 ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
3.76 SOME (([1], str, dsc, (*[var]*)
3.77 - I_Model.split_dts' (dsc, var))) (*:ori without leading #*))
3.78 + O_Model.split_dts' (dsc, var))) (*:ori without leading #*))
3.79 handle e as TYPE _ =>
3.80 (tracing (dashs 70 ^ "\n"
3.81 ^ "*** ERROR while creating the items for the model of the ->problem\n"
3.82 @@ -602,7 +602,7 @@
3.83 fun cpy_nam pbt oris (p as (field, (dsc, t))) =
3.84 (if is_copy_named_generating p
3.85 then (*WN051014 kept strange old code ...*)
3.86 - let fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts)
3.87 + let fun sel (_,_,d,ts) = O_Model.comp_ts (d, ts)
3.88 val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
3.89 val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
3.90 val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
3.91 @@ -624,7 +624,7 @@
3.92 val cy = filter is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
3.93 val oris' = matc thy pbt' ags []
3.94 val cy' = map (cpy_nam pbt' oris') cy
3.95 - val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
3.96 + val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
3.97 in (map flattup ors) end
3.98
3.99 (* report part of the error-msg which is not available in match_args *)
4.1 --- a/src/Tools/isac/Specify/i-model.sml Thu May 07 12:15:37 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Thu May 07 14:11:03 2020 +0200
4.3 @@ -29,14 +29,15 @@
4.4
4.5 val untouched : T -> bool
4.6 (*\------- to I_Model from Model 1 -------/*)
4.7 -(*/------- to I_Model from Model 1a -------\*)
4.8 +
4.9 +(*/------- to O_Model from I_Model 1 -------\* )
4.10 val comp_dts : term * term list -> term
4.11 val comp_dts' : term * term list -> term
4.12 val comp_dts'' : term * term list -> string
4.13 val comp_ts : term * term list -> term
4.14 val split_dts : term -> term * term list
4.15 val split_dts' : term * term -> term list
4.16 -(*\------- to I_Model from Model 1a -------/*)
4.17 +( *\------- to O_Model from I_Model 1 -------/*)
4.18
4.19 (*/------- to I_Model from Model 4 -------\*)
4.20 val d_in : feedback -> term
4.21 @@ -66,7 +67,7 @@
4.22 type single = Model_Def.i_model_single;
4.23 val empty = Model_Def.i_model_empty;
4.24
4.25 -(*/------- to I_Model from Model 1b -------\*)
4.26 +(*/------- to O_Model from I_Model 2 -------\* )
4.27 val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
4.28 val e_listReal = script_parse "[]::(real list)";
4.29 val e_listBool = script_parse "[]::(bool list)";
4.30 @@ -78,8 +79,9 @@
4.31 fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
4.32 let val elems = (flat o (map TermC.isalist2list)) ts;
4.33 in TermC.list2isalist (type_of (hd elems)) elems end;
4.34 -(*\------- to I_Model from Model 1b -------/*)
4.35 -(*/------- to I_Model from Model 1a -------\*)
4.36 +( *\------- to O_Model from I_Model 2 -------/*)
4.37 +
4.38 +(*/------- to O_Model from I_Model 3 -------\* )
4.39 fun is_var (Free _) = true
4.40 | is_var _ = false;
4.41
4.42 @@ -90,7 +92,9 @@
4.43 then TermC.isalist2list t
4.44 else [t]
4.45 in (flat o (map dest)) ts end;
4.46 +( *\------- to O_Model from I_Model 3 -------/*)
4.47
4.48 +(*/------- to O_Model from I_Model 1 -------\* )
4.49 (* revert split_dts only for ts; compare comp_dts *)
4.50 fun comp_ts (d, ts) =
4.51 if Input_Descript.is_list_dsc d
4.52 @@ -173,7 +177,7 @@
4.53 (d $ (comp_ts (d, ts)))
4.54 handle _ => error ("comp_dts: "^(term2str d)^
4.55 " $ "^(term2str (hd ts))));*)
4.56 -(*\------- to I_Model from Model 1a -------/*)
4.57 +( *\------- to O_Model from I_Model 1 -------/*)
4.58
4.59 (*/------- to I_Model from Model 1c -------\*)
4.60 (* 27.8.01: problem-environment
4.61 @@ -191,13 +195,13 @@
4.62 (*\------- to I_Model from Model 1c -------/*)
4.63 (*/------- to I_Model from Model 1 -------\*)
4.64 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
4.65 - "Cor " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
4.66 + "Cor " ^ UnparseC.term_in_ctxt ctxt (O_Model.comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
4.67 | feedback_to_string _ (Syn c) = "Syn " ^ c
4.68 | feedback_to_string _ (Typ c) = "Typ " ^ c
4.69 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
4.70 - "Inc " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
4.71 + "Inc " ^ UnparseC.term_in_ctxt ctxt (O_Model.comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
4.72 | feedback_to_string ctxt (Sup (d, ts)) =
4.73 - "Sup " ^ UnparseC.term_in_ctxt ctxt (comp_dts (d, ts))
4.74 + "Sup " ^ UnparseC.term_in_ctxt ctxt (O_Model.comp_dts (d, ts))
4.75 | feedback_to_string ctxt (Mis (d, pid)) =
4.76 "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
4.77 | feedback_to_string _ (Par s) = "Trm "^s;
4.78 @@ -275,7 +279,7 @@
4.79 | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
4.80
4.81 fun dts2str (d, ts) = pair2str (UnparseC.term d, UnparseC.terms ts);
4.82 -fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
4.83 +fun penvval_in (Cor ((d, _), (_, ts))) = [O_Model.comp_ts (d,ts)]
4.84 | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
4.85 | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
4.86 | penvval_in (Inc (_, (_, ts))) = ts
5.1 --- a/src/Tools/isac/Specify/input-calchead.sml Thu May 07 12:15:37 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Thu May 07 14:11:03 2020 +0200
5.3 @@ -51,7 +51,7 @@
5.4 val thy = ThyC.get_theory dI
5.5 val {ppc, ...} = Specify.get_pbt pI
5.6 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
5.7 - val its = Specify.add_id its_
5.8 + val its = O_Model.add_id its_
5.9 val pits = map flattup2 its
5.10 val (pI, mI) =
5.11 if mI <> ["no_met"]
5.12 @@ -62,7 +62,7 @@
5.13 | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
5.14 val {ppc, pre, prls, ...} = Specify.get_met mI
5.15 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
5.16 - val its = Specify.add_id its_
5.17 + val its = O_Model.add_id its_
5.18 val mits = map flattup2 its
5.19 val pre = Stool.check_preconds thy prls pre mits
5.20 val ctxt = Proof_Context.init_global thy
5.21 @@ -116,7 +116,7 @@
5.22
5.23 (* re-parse itms with a new thy and prepare for checking with ori list *)
5.24 fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
5.25 - (let val t = I_Model.comp_dts (d, ts)
5.26 + (let val t = O_Model.comp_dts (d, ts)
5.27 val _ = (UnparseC.term_in_thy dI t)
5.28 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
5.29 in itm end
5.30 @@ -130,13 +130,13 @@
5.31 in (i, v, b, f, I_Model.Par str) end
5.32 handle _ => (i, v, b, f, I_Model.Syn str))
5.33 | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
5.34 - (let val t = I_Model.comp_dts (d,ts);
5.35 + (let val t = O_Model.comp_dts (d,ts);
5.36 val _ = UnparseC.term_in_thy dI t;
5.37 (*this ^ should raise the exn on unability of re-parsing dts*)
5.38 in itm end
5.39 handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
5.40 | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
5.41 - (let val t = I_Model.comp_dts (d,ts);
5.42 + (let val t = O_Model.comp_dts (d,ts);
5.43 val _ = UnparseC.term_in_thy dI t;
5.44 (*this ^ should raise the exn on unability of re-parsing dts*)
5.45 in itm end
5.46 @@ -196,7 +196,7 @@
5.47 NONE => ([], false, f, I_Model.Syn str)
5.48 | SOME ct =>
5.49 let
5.50 - val (d, ts) = (I_Model.split_dts o Thm.term_of) ct
5.51 + val (d, ts) = (O_Model.split_dts o Thm.term_of) ct
5.52 val popt = find_first (eq7 (f, d)) pbt
5.53 in
5.54 case popt of
5.55 @@ -210,7 +210,7 @@
5.56 let
5.57 val thy = ThyC.get_theory dI
5.58 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
5.59 - val its = Specify.add_id its_
5.60 + val its = O_Model.add_id its_
5.61 in map flattup2 its end
5.62
5.63 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
5.64 @@ -233,11 +233,11 @@
5.65
5.66 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
5.67 | par2fstr itm = error ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
5.68 -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, I_Model.comp_dts'' (d, ts))
5.69 +fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, O_Model.comp_dts'' (d, ts))
5.70 | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
5.71 | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
5.72 - | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, I_Model.comp_dts'' (d,ts))
5.73 - | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, I_Model.comp_dts'' (d, ts))
5.74 + | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, O_Model.comp_dts'' (d,ts))
5.75 + | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, O_Model.comp_dts'' (d, ts))
5.76 | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
5.77 | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
5.78 error ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
5.79 @@ -273,7 +273,7 @@
5.80 let val pbt = (#ppc o Specify.get_pbt) pI
5.81 val dI' = #1 (Chead.some_spec ospec spec)
5.82 val oris = if pI = #2 ospec then oris
5.83 - else Specify.prep_ori fmz_(ThyC.get_theory"Isac_Knowledge") pbt |> #1;
5.84 + else O_Model.prep_ori fmz_(ThyC.get_theory"Isac_Knowledge") pbt |> #1;
5.85 in (Pos.Pbl, appl_adds dI' oris probl pbt
5.86 (map itms2fstr probl), meth) end
5.87 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
6.1 --- a/src/Tools/isac/Specify/model.sml Thu May 07 12:15:37 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/model.sml Thu May 07 14:11:03 2020 +0200
6.3 @@ -78,7 +78,7 @@
6.4 fun mkval' x = mkval TermC.empty x;
6.5
6.6 (* 9.5.03 penv postponed: pbl_ids' *)
6.7 -fun pbl_ids' d vs = [I_Model.comp_ts (d, vs)];
6.8 +fun pbl_ids' d vs = [O_Model.comp_ts (d, vs)];
6.9
6.10 (* for _output_ of the items of a Model *)
6.11 datatype item =
7.1 --- a/src/Tools/isac/Specify/o-model.sml Thu May 07 12:15:37 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/o-model.sml Thu May 07 14:11:03 2020 +0200
7.3 @@ -16,6 +16,27 @@
7.4 (* e_ori*)
7.5 val single_empty: single
7.6
7.7 +(*/------- to O_Model from Specify -------\*)
7.8 + type field
7.9 + val prep_ori : Formalise.model -> theory -> field list -> T * Proof.context
7.10 + val add_id : 'a list -> (int * 'a) list
7.11 + val add_field : theory -> Model_Pattern.T -> term * 'b -> string * term * 'b
7.12 + val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
7.13 + val max: int list -> int
7.14 + val coll_variants: ('a * ''b) list -> ('a list * ''b) list
7.15 + val replace_0: int -> int list -> int list
7.16 + val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
7.17 +(*\------- to O_Model from Specify -------/*)
7.18 +
7.19 +(*/------- to O_Model from I_Model 1 -------\*)
7.20 + val comp_dts : term * term list -> term
7.21 + val comp_dts' : term * term list -> term
7.22 + val comp_dts'' : term * term list -> string
7.23 + val comp_ts : term * term list -> term
7.24 + val split_dts : term -> term * term list
7.25 + val split_dts' : term * term -> term list
7.26 +(*\------- to O_Model from I_Model 1 -------/*)
7.27 +
7.28 (*/------- to O_Model from Model 1 -------\*)
7.29 type preori
7.30 (*\------- to O_Model from Model 1 -------/*)
7.31 @@ -46,5 +67,191 @@
7.32 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
7.33 (*\------- to O_Model from Model 1 -------/*)
7.34
7.35 +type field = string * (term * term)
7.36 +
7.37 +(*/------- to O_Model from I_Model 3 -------\*)
7.38 +(* special handling for lists. ?WN:14.5.03 ??!? *)
7.39 +fun is_var (Free _) = true
7.40 + | is_var _ = false;
7.41 +
7.42 +fun dest_list (d, ts) =
7.43 + let fun dest t =
7.44 + if Input_Descript.is_list_dsc d andalso not (Input_Descript.is_unl d) andalso not (is_var t) (*..for pbt*)
7.45 + then TermC.isalist2list t
7.46 + else [t]
7.47 + in (flat o (map dest)) ts end;
7.48 +(*\------- to O_Model from I_Model 3 -------/*)
7.49 +
7.50 +(*/------- to O_Model from I_Model 2 -------\*)
7.51 +val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
7.52 +val e_listReal = script_parse "[]::(real list)";
7.53 +val e_listBool = script_parse "[]::(bool list)";
7.54 +
7.55 +(* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
7.56 +fun take_apart t =
7.57 + let val elems = TermC.isalist2list t
7.58 + in map ((TermC.list2isalist (type_of (hd elems))) o single) elems end;
7.59 +fun take_apart_inv ts = (* t = (take_apart_inv o take_apart) t *)
7.60 + let val elems = (flat o (map TermC.isalist2list)) ts;
7.61 + in TermC.list2isalist (type_of (hd elems)) elems end;
7.62 +(*\------- to O_Model from I_Model 1 -------/*)
7.63 +(*/------- to O_Model from I_Model -------\*)
7.64 +(* revert split_dts only for ts; compare comp_dts *)
7.65 +fun comp_ts (d, ts) =
7.66 + if Input_Descript.is_list_dsc d
7.67 + then if TermC.is_list (hd ts)
7.68 + then if Input_Descript.is_unl d
7.69 + then (hd ts) (* e.g. someList [1,3,2] *)
7.70 + else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
7.71 + else (hd ts) (* a variable or metavariable for a list *)
7.72 + else (hd ts);
7.73 +fun comp_dts (d, []) =
7.74 + if Input_Descript.is_reall_dsc d
7.75 + then (d $ e_listReal)
7.76 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
7.77 + | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
7.78 + handle _ => raise ERROR ("comp_dts: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
7.79 +fun comp_dts' (d, []) =
7.80 + if Input_Descript.is_reall_dsc d
7.81 + then (d $ e_listReal)
7.82 + else if Input_Descript.is_booll_dsc d then (d $ e_listBool) else d
7.83 + | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
7.84 + handle _ => raise ERROR ("comp_dts': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
7.85 +fun comp_dts'' (d, []) =
7.86 + if Input_Descript.is_reall_dsc d
7.87 + then UnparseC.term (d $ e_listReal)
7.88 + else if Input_Descript.is_booll_dsc d
7.89 + then UnparseC.term (d $ e_listBool)
7.90 + else UnparseC.term d
7.91 + | comp_dts'' (d, ts) = UnparseC.term (d $ (comp_ts (d, ts)))
7.92 + handle _ => raise ERROR ("comp_dts'': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts));
7.93 +
7.94 +(* decompose an input into description, terms (ev. elems of lists),
7.95 + and the value for the problem-environment; inv to comp_dts *)
7.96 +fun split_dts (t as d $ arg) =
7.97 + if Input_Descript.is_dsc d
7.98 + then if Input_Descript.is_list_dsc d andalso TermC.is_list arg andalso Input_Descript.is_unl d |> not
7.99 + then (d, take_apart arg)
7.100 + else (d, [arg])
7.101 + else (TermC.empty, TermC.dest_list' t)
7.102 + | split_dts t =
7.103 + let val t' as (h, _) = strip_comb t;
7.104 + in
7.105 + if Input_Descript.is_dsc h
7.106 + then (h, dest_list t')
7.107 + else (TermC.empty, TermC.dest_list' t)
7.108 + end;
7.109 +(* version returning ts only *)
7.110 +fun split_dts' (d, arg) =
7.111 + if Input_Descript.is_dsc d
7.112 + then if Input_Descript.is_list_dsc d
7.113 + then if TermC.is_list arg
7.114 + then if Input_Descript.is_unl d
7.115 + then ([arg]) (* e.g. someList [1,3,2] *)
7.116 + else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
7.117 + else ([arg]) (* a variable or metavariable for a list *)
7.118 + else ([arg])
7.119 + else (TermC.dest_list' arg)
7.120 +(* WN170204: Warning "redundant"
7.121 + | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)
7.122 + let val (h,argl) = strip_comb t
7.123 + in
7.124 + if (not o is_dsc) h
7.125 + then (dest_list' t)
7.126 + else (dest_list (h,argl))
7.127 + end;*)
7.128 +(* revert split_:
7.129 + WN050903 we do NOT know which is from subtheory, description or term;
7.130 + typecheck thus may lead to TYPE-error 'unknown constant';
7.131 + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
7.132 +(*fun comp_dts thy (d,[]) =
7.133 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
7.134 + (Thy_Info_get_theory "Isac_Knowledge")
7.135 + (*comp_dts:FIXXME stay with term for efficiency !!!*)
7.136 + (if is_reall_dsc d then (d $ e_listReal)
7.137 + else if is_booll_dsc d then (d $ e_listBool)
7.138 + else d)
7.139 + | comp_dts (d,ts) =
7.140 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
7.141 + (Thy_Info_get_theory "Isac_Knowledge")
7.142 + (*comp_dts:FIXXME stay with term for efficiency !!*)
7.143 + (d $ (comp_ts (d, ts)))
7.144 + handle _ => error ("comp_dts: "^(term2str d)^
7.145 + " $ "^(term2str (hd ts))));*)
7.146 +(*\------- to O_Model from I_Model -------/*)
7.147 +
7.148 +
7.149 +
7.150 +(*/------- to O_Model from Specify -------\*)
7.151 +(* mark an element with the position within a plateau;
7.152 + a plateau with length 1 is marked with 0 *)
7.153 +fun mark _ [] = error "mark []"
7.154 + | mark eq xs =
7.155 + let
7.156 + fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)]
7.157 + | mar _ _ [] _ = error "mark []"
7.158 + | mar xx eq (x:: x' :: xs) n =
7.159 + if eq(x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1)
7.160 + else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
7.161 + in mar [] eq xs 1 end;
7.162 +
7.163 +(* compare d and dsc in pbt and transfer field to pre-ori *)
7.164 +fun add_field (_: theory) pbt (d,ts) =
7.165 + let fun eq d pt = (d = (fst o snd) pt);
7.166 + in case filter (eq d) pbt of
7.167 + [(fi, (_, _))] => (fi, d, ts)
7.168 + | [] => ("#undef", d, ts) (*may come with met.ppc*)
7.169 + | _ => error ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
7.170 + end;
7.171 +
7.172 +(* assumes equal descriptions to be in adjacent 'plateaus',
7.173 + items at a certain position within the plateaus form a variant;
7.174 + length = 1 ... marked with 0: covers all variants *)
7.175 +fun add_variants fdts =
7.176 + let
7.177 + fun eq (a, b) = curry op= (snd3 a) (snd3 b);
7.178 + in mark eq fdts end;
7.179 +
7.180 +fun max [] = error "max of []"
7.181 + | max (y :: ys) =
7.182 + let fun mx x [] = x
7.183 + | mx x (y :: ys) = if x < y then mx y ys else mx x ys;
7.184 +in mx y ys end;
7.185 +
7.186 +fun coll_variants (((v,x) :: vxs)) =
7.187 + let
7.188 + fun col xs (vs, x) [] = xs @ [(vs, x)]
7.189 + | col xs (vs, x) ((v', x') :: vxs') =
7.190 + if x = x' then col xs (vs @ [v'], x') vxs'
7.191 + else col (xs @ [(vs, x)]) ([v'], x') vxs';
7.192 + in col [] ([v], x) vxs end
7.193 + | coll_variants _ = error "coll_variants: called with []";
7.194 +
7.195 +fun replace_0 vm [0] = intsto vm
7.196 + | replace_0 _ vs = vs;
7.197 +
7.198 +fun add_id [] = error "add_id []"
7.199 + | add_id xs =
7.200 + let
7.201 + fun add _ [] = []
7.202 + | add n (x :: xs) = (n, x) :: add (n + 1) xs;
7.203 + in add 1 xs end;
7.204 +
7.205 +fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
7.206 +
7.207 +fun prep_ori [] _ _ = ([], ContextC.empty)
7.208 + | prep_ori fmz thy pbt =
7.209 + let
7.210 + val ctxt = ContextC.initialise' thy fmz;
7.211 + val ori = map (add_field thy pbt o split_dts o TermC.parseNEW' ctxt) fmz
7.212 + |> add_variants;
7.213 + val maxv = map fst ori |> max;
7.214 + val maxv = if maxv = 0 then 1 else maxv;
7.215 + val oris = coll_variants ori
7.216 + |> map (replace_0 maxv |> apfst)
7.217 + |> add_id
7.218 + |> map flattup;
7.219 + in (oris, ctxt) end;
7.220 +(*\------- to O_Model from Specify -------/*)
7.221
7.222 (**)end(**);
7.223 \ No newline at end of file
8.1 --- a/src/Tools/isac/Specify/ptyps.sml Thu May 07 12:15:37 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/ptyps.sml Thu May 07 14:11:03 2020 +0200
8.3 @@ -9,10 +9,17 @@
8.4 val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T
8.5
8.6 val get_fun_ids : theory -> (string * typ) list
8.7 - type field
8.8 - (* for calchead.sml, if below at left margin *)
8.9 + type field = O_Model.field
8.10 +(*/------- to O_Model from Specify -------\* )
8.11 val prep_ori : Formalise.model -> theory -> field list -> O_Model.T * Proof.context
8.12 val add_id : 'a list -> (int * 'a) list
8.13 + val add_field : theory -> Model_Pattern.T -> term * 'b -> string * term * 'b
8.14 + val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
8.15 + val max: int list -> int
8.16 + val coll_variants: ('a * ''b) list -> ('a list * ''b) list
8.17 + val replace_0: int -> int list -> int list
8.18 + val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
8.19 +( *\------- to O_Model from Specify -------/*)
8.20 val add_field' : theory -> field list -> O_Model.T -> O_Model.T
8.21 val match_itms_oris : theory -> I_Model.T -> field list * term list * Rule_Set.T ->
8.22 O_Model.T -> bool * (I_Model.T * (bool * term) list)
8.23 @@ -66,12 +73,6 @@
8.24 val show_pblguhs : unit -> unit
8.25 val sort_pblguhs : unit -> unit
8.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.27 - val add_field : theory -> Model_Pattern.T -> term * 'b -> string * term * 'b
8.28 - val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
8.29 - val coll_variants: ('a * ''b) list -> ('a list * ''b) list
8.30 - val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
8.31 - val max: int list -> int
8.32 - val replace_0: int -> int list -> int list
8.33 val split_did: term -> term * term
8.34 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.35
8.36 @@ -148,14 +149,15 @@
8.37 filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
8.38 end
8.39
8.40 -type field = string * (term * term)
8.41 +type field = O_Model.field
8.42 +
8.43 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
8.44
8.45 -fun itm_2item (_: theory) (I_Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (I_Model.comp_dts (d, ts)))
8.46 +fun itm_2item (_: theory) (I_Model.Cor ((d, ts), _)) = Model.Correct (UnparseC.term (O_Model.comp_dts (d, ts)))
8.47 | itm_2item _ (I_Model.Syn c) = Model.SyntaxE c
8.48 | itm_2item _ (I_Model.Typ c) = Model.TypeE c
8.49 - | itm_2item _ (I_Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (I_Model.comp_dts (d, ts)))
8.50 - | itm_2item _ (I_Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (I_Model.comp_dts (d, ts)))
8.51 + | itm_2item _ (I_Model.Inc ((d, ts), _)) = Model.Incompl (UnparseC.term (O_Model.comp_dts (d, ts)))
8.52 + | itm_2item _ (I_Model.Sup (d, ts)) = Model.Superfl (UnparseC.term (O_Model.comp_dts (d, ts)))
8.53 | itm_2item _ (I_Model.Mis (d, pid)) = Model.Missing (UnparseC.term d ^ " " ^ UnparseC.term pid)
8.54 | itm_2item _ _ = error "itm_2item: uncovered definition"
8.55
8.56 @@ -184,11 +186,11 @@
8.57 in (hd, arg) end
8.58
8.59 (*create output-string for itm_*)
8.60 -fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
8.61 +fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (O_Model.comp_dts (d, ts))
8.62 | itm_out _ (I_Model.Syn c) = c
8.63 | itm_out _ (I_Model.Typ c) = c
8.64 - | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (I_Model.comp_dts (d, ts))
8.65 - | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (I_Model.comp_dts (d, ts))
8.66 + | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (O_Model.comp_dts (d, ts))
8.67 + | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (O_Model.comp_dts (d, ts))
8.68 | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
8.69 | itm_out _ _ = error "itm_out: uncovered definition"
8.70
8.71 @@ -203,15 +205,6 @@
8.72 val gfr = coll Model.empty_ppc itms;
8.73 in add_where gfr (map boolterm2item pre) end;
8.74
8.75 -(* compare d and dsc in pbt and transfer field to pre-ori *)
8.76 -fun add_field (_: theory) pbt (d,ts) =
8.77 - let fun eq d pt = (d = (fst o snd) pt);
8.78 - in case filter (eq d) pbt of
8.79 - [(fi, (_, _))] => (fi, d, ts)
8.80 - | [] => ("#undef", d, ts) (*may come with met.ppc*)
8.81 - | _ => error ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
8.82 - end;
8.83 -
8.84 (* take over field from met.ppc at 'Specify_Method' into ori,
8.85 i.e. also removes "#undef" fields *)
8.86 fun add_field' (_: theory) mpc ori =
8.87 @@ -224,6 +217,7 @@
8.88 | _ => error ("add_field': " ^ UnparseC.term d ^ " more than once in met");
8.89 in flat ((map (repl mpc)) ori) end;
8.90
8.91 +(*/------- to O_Model from Specify -------\* )
8.92 (* mark an element with the position within a plateau;
8.93 a plateau with length 1 is marked with 0 *)
8.94 fun mark _ [] = error "mark []"
8.95 @@ -236,6 +230,15 @@
8.96 else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1;
8.97 in mar [] eq xs 1 end;
8.98
8.99 +(* compare d and dsc in pbt and transfer field to pre-ori *)
8.100 +fun add_field (_: theory) pbt (d,ts) =
8.101 + let fun eq d pt = (d = (fst o snd) pt);
8.102 + in case filter (eq d) pbt of
8.103 + [(fi, (_, _))] => (fi, d, ts)
8.104 + | [] => ("#undef", d, ts) (*may come with met.ppc*)
8.105 + | _ => error ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
8.106 + end;
8.107 +
8.108 (* assumes equal descriptions to be in adjacent 'plateaus',
8.109 items at a certain position within the plateaus form a variant;
8.110 length = 1 ... marked with 0: covers all variants *)
8.111 @@ -275,7 +278,7 @@
8.112 | prep_ori fmz thy pbt =
8.113 let
8.114 val ctxt = ContextC.initialise' thy fmz;
8.115 - val ori = map (add_field thy pbt o I_Model.split_dts o TermC.parseNEW' ctxt) fmz
8.116 + val ori = map (add_field thy pbt o O_Model.split_dts o TermC.parseNEW' ctxt) fmz
8.117 |> add_variants;
8.118 val maxv = map fst ori |> max;
8.119 val maxv = if maxv = 0 then 1 else maxv;
8.120 @@ -284,6 +287,7 @@
8.121 |> add_id
8.122 |> map flattup;
8.123 in (oris, ctxt) end;
8.124 +( *\------- to O_Model from Specify -------/*)
8.125
8.126 val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Pattern_Def.T
8.127 val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
8.128 @@ -596,7 +600,7 @@
8.129 (* match a formalization with a problem type, for tests *)
8.130 fun match_pbl fmz {thy = thy, where_ = pre, ppc, prls = er, ...} =
8.131 let
8.132 - val oris = prep_ori fmz thy ppc |> #1;
8.133 + val oris = O_Model.prep_ori fmz thy ppc |> #1;
8.134 val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
8.135 in
8.136 if bool
8.137 @@ -627,7 +631,7 @@
8.138 let
8.139 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
8.140 val {thy, ppc, where_, prls, ...} = py
8.141 - val oris = prep_ori fmz thy ppc |> #1;
8.142 + val oris = O_Model.prep_ori fmz thy ppc |> #1;
8.143 (* WN020803: itms!: oris might _not_ be complete here *)
8.144 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
8.145 in
8.146 @@ -639,7 +643,7 @@
8.147 let
8.148 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
8.149 val {thy, ppc, where_, prls, ...} = py
8.150 - val oris = prep_ori fmz thy ppc |> #1;
8.151 + val oris = O_Model.prep_ori fmz thy ppc |> #1;
8.152 (* WN020803: itms!: oris might _not_ be complete here *)
8.153 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
8.154 in
9.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu May 07 12:15:37 2020 +0200
9.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu May 07 14:11:03 2020 +0200
9.3 @@ -298,12 +298,12 @@
9.4 if mI = ["no_met"]
9.5 then
9.6 let
9.7 - val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
9.8 + val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> O_Model.prep_ori fmz thy;
9.9 val pI' = Specify.refine_ori' pors pI;
9.10 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
9.11 (hd o #met o Specify.get_pbt) pI')
9.12 end
9.13 - else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
9.14 + else (pI, Specify.get_pbt pI |> #ppc |> O_Model.prep_ori fmz thy, mI)
9.15 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
9.16 val dI = Context.theory_name (Stool.common_subthy (thy, thy'))
9.17 val hdl = case cas of
10.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu May 07 12:15:37 2020 +0200
10.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu May 07 14:11:03 2020 +0200
10.3 @@ -1228,7 +1228,7 @@
10.4 [Free ("x", _) $ _]
10.5 )
10.6 ],_
10.7 - ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
10.8 + ) = O_Model.prep_ori fmz thy ((#ppc o get_pbt) pI);
10.9
10.10 val Prog sc
10.11 = (#scr o get_met) ["SignalProcessing",
11.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu May 07 12:15:37 2020 +0200
11.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Thu May 07 14:11:03 2020 +0200
11.3 @@ -287,7 +287,7 @@
11.4 ((rev o tl) pblID, fmz, [(*match list*)],
11.5 ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node));
11.6 val {thy, ppc, where_, prls, ...} = py ;
11.7 -"~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
11.8 +"~~~~~ fun O_Model.prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
11.9 val ctxt = Proof_Context.init_global thy;
11.10 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
11.11 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
12.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Thu May 07 12:15:37 2020 +0200
12.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Thu May 07 14:11:03 2020 +0200
12.3 @@ -6,7 +6,7 @@
12.4 "table of contents -----------------------------------------------------------------------------";
12.5 "-----------------------------------------------------------------------------------------------";
12.6 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
12.7 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
12.8 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
12.9 "----------- type penv -------------------------------------------------------------------------";
12.10 "----------- fun untouched ---------------------------------------------------------------------";
12.11 "----------- fun pbl_ids -----------------------------------------------------------------------";
12.12 @@ -79,8 +79,8 @@
12.13 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
12.14 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T);
12.15 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
12.16 -val (d, ts) = I_Model.split_dts t;
12.17 -"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
12.18 +val (d, ts) = O_Model.split_dts t;
12.19 +"~~~~~ fun O_Model.split_dts, args:"; val (t as d $ arg) = t;
12.20 (*if is_dsc d then () else error "TODO";*)
12.21 if is_dsc d then () else error "TODO";
12.22 "----- these were the errors (call hierarchy from bottom up)";
12.23 @@ -96,60 +96,60 @@
12.24 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
12.25 ========== inhibit exn AK110725 ================================================*)
12.26
12.27 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
12.28 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
12.29 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
12.30 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
12.31 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
12.32 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
12.33 (*val t = str2term "maximum A";
12.34 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.35 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.36 val it = "maximum A" : cterm
12.37 > val t = str2term "fixedValues [r=Arbfix]";
12.38 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.39 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.40 "fixedValues [r = Arbfix]"
12.41 > val t = str2term "valuesFor [a]";
12.42 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.43 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.44 "valuesFor [a]"
12.45 > val t = str2term "valuesFor [a,b]";
12.46 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.47 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.48 "valuesFor [a, b]"
12.49 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
12.50 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.51 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.52 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
12.53 > val t = str2term "boundVariable a";
12.54 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.55 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.56 "boundVariable a"
12.57 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
12.58 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.59 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.60 "interval {x. 0 <= x & x <= 2 * r}"
12.61
12.62 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
12.63 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.64 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.65 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
12.66 > val t = str2term "solveFor x";
12.67 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.68 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.69 "solveFor x"
12.70 > val t = str2term "errorBound (eps=0)";
12.71 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.72 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.73 "errorBound (eps = 0)"
12.74 > val t = str2term "solutions L";
12.75 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
12.76 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
12.77 "solutions L"
12.78
12.79 before 6.5.03:
12.80 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
12.81 -> val (d,ts) = I_Model.split_dts t;
12.82 +> val (d,ts) = O_Model.split_dts t;
12.83 > comp_dts thy (d,ts);
12.84 val it = "testdscforlist [#1]" : cterm
12.85
12.86 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
12.87 -> val (d,ts) = I_Model.split_dts t;
12.88 +> val (d,ts) = O_Model.split_dts t;
12.89 val d = Const ("empty","empty") : term
12.90 val ts = [Free ("A","RealDef.real")] : term list
12.91 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
12.92 -> val (d,ts) = I_Model.split_dts t;
12.93 +> val (d,ts) = O_Model.split_dts t;
12.94 val d = Const ("empty","empty") : term
12.95 val ts = [Const # $ Free # $ Free (#,#)] : term list
12.96 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
12.97 -> val (d,ts) = I_Model.split_dts t;
12.98 +> val (d,ts) = O_Model.split_dts t;
12.99 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
12.100 *)
12.101 "----------- type penv -------------------------------------------------------------------------";
12.102 @@ -189,7 +189,7 @@
12.103
12.104 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
12.105 val (d,argl) = strip_comb t;
12.106 - is_dsc d; (*see I_Model.split_dts*)
12.107 + is_dsc d; (*see O_Model.split_dts*)
12.108 dest_list (d,argl);
12.109 val (_ $ v) = t;
12.110 is_list v;
12.111 @@ -197,7 +197,7 @@
12.112 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
12.113 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
12.114
12.115 - val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
12.116 + val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
12.117 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term
12.118 val vl = Free ("x","RealDef.real") : term
12.119
12.120 @@ -205,7 +205,7 @@
12.121 pbl_ids ctxt dsc vl;
12.122 val it = [Free ("x","RealDef.real")] : term list
12.123
12.124 - val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy))
12.125 + val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o(parse thy))
12.126 "errorBound (eps=#0)";
12.127 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
12.128 pbl_ids ctxt dsc vl;
13.1 --- a/test/Tools/isac/MathEngBasic/model.sml Thu May 07 12:15:37 2020 +0200
13.2 +++ b/test/Tools/isac/MathEngBasic/model.sml Thu May 07 14:11:03 2020 +0200
13.3 @@ -43,7 +43,7 @@
13.4
13.5
13.6 val env = []:envv;
13.7 - val (d,ts) = (I_Model.split_dts o Thm.term_of o the o (parse thy))
13.8 + val (d,ts) = (O_Model.split_dts o Thm.term_of o the o (parse thy))
13.9 "fixedValues [r=Arbfix]";
13.10 val (_,id) = (split_did o Thm.term_of o the o (parse thy))"fixedValues fix_";
13.11 val vats = [1,2,3];
14.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Thu May 07 12:15:37 2020 +0200
14.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Thu May 07 14:11:03 2020 +0200
14.3 @@ -6,7 +6,7 @@
14.4 "table of contents -----------------------------------------------------------------------------";
14.5 "-----------------------------------------------------------------------------------------------";
14.6 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
14.7 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
14.8 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
14.9 "----------- type penv -------------------------------------------------------------------------";
14.10 "----------- fun untouched ---------------------------------------------------------------------";
14.11 "----------- fun pbl_ids -----------------------------------------------------------------------";
14.12 @@ -79,8 +79,8 @@
14.13 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
14.14 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T);
14.15 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
14.16 -val (d, ts) = I_Model.split_dts t;
14.17 -"~~~~~ fun I_Model.split_dts, args:"; val (t as d $ arg) = t;
14.18 +val (d, ts) = O_Model.split_dts t;
14.19 +"~~~~~ fun O_Model.split_dts, args:"; val (t as d $ arg) = t;
14.20 (*if is_dsc d then () else error "TODO";*)
14.21 if is_dsc d then () else error "TODO";
14.22 "----- these were the errors (call hierarchy from bottom up)";
14.23 @@ -96,60 +96,60 @@
14.24 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
14.25 ========== inhibit exn AK110725 ================================================*)
14.26
14.27 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
14.28 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
14.29 -"----------- fun comp_dts -- fun I_Model.split_dts -----------------------------------------------------";
14.30 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
14.31 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
14.32 +"----------- fun comp_dts -- fun O_Model.split_dts -----------------------------------------------------";
14.33 (*val t = str2term "maximum A";
14.34 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.35 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.36 val it = "maximum A" : cterm
14.37 > val t = str2term "fixedValues [r=Arbfix]";
14.38 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.39 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.40 "fixedValues [r = Arbfix]"
14.41 > val t = str2term "valuesFor [a]";
14.42 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.43 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.44 "valuesFor [a]"
14.45 > val t = str2term "valuesFor [a,b]";
14.46 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.47 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.48 "valuesFor [a, b]"
14.49 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
14.50 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.51 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.52 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"
14.53 > val t = str2term "boundVariable a";
14.54 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.55 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.56 "boundVariable a"
14.57 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
14.58 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.59 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.60 "interval {x. 0 <= x & x <= 2 * r}"
14.61
14.62 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
14.63 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.64 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.65 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
14.66 > val t = str2term "solveFor x";
14.67 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.68 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.69 "solveFor x"
14.70 > val t = str2term "errorBound (eps=0)";
14.71 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.72 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.73 "errorBound (eps = 0)"
14.74 > val t = str2term "solutions L";
14.75 -> val (d,ts) = I_Model.split_dts thy t; comp_dts thy (d,ts);
14.76 +> val (d,ts) = O_Model.split_dts thy t; comp_dts thy (d,ts);
14.77 "solutions L"
14.78
14.79 before 6.5.03:
14.80 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
14.81 -> val (d,ts) = I_Model.split_dts t;
14.82 +> val (d,ts) = O_Model.split_dts t;
14.83 > comp_dts thy (d,ts);
14.84 val it = "testdscforlist [#1]" : cterm
14.85
14.86 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
14.87 -> val (d,ts) = I_Model.split_dts t;
14.88 +> val (d,ts) = O_Model.split_dts t;
14.89 val d = Const ("empty","empty") : term
14.90 val ts = [Free ("A","RealDef.real")] : term list
14.91 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
14.92 -> val (d,ts) = I_Model.split_dts t;
14.93 +> val (d,ts) = O_Model.split_dts t;
14.94 val d = Const ("empty","empty") : term
14.95 val ts = [Const # $ Free # $ Free (#,#)] : term list
14.96 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
14.97 -> val (d,ts) = I_Model.split_dts t;
14.98 +> val (d,ts) = O_Model.split_dts t;
14.99 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
14.100 *)
14.101 "----------- type penv -------------------------------------------------------------------------";
14.102 @@ -189,7 +189,7 @@
14.103
14.104 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
14.105 val (d,argl) = strip_comb t;
14.106 - is_dsc d; (*see I_Model.split_dts*)
14.107 + is_dsc d; (*see O_Model.split_dts*)
14.108 dest_list (d,argl);
14.109 val (_ $ v) = t;
14.110 is_list v;
14.111 @@ -197,7 +197,7 @@
14.112 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
14.113 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
14.114
14.115 - val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
14.116 + val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
14.117 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term
14.118 val vl = Free ("x","RealDef.real") : term
14.119
14.120 @@ -205,7 +205,7 @@
14.121 pbl_ids ctxt dsc vl;
14.122 val it = [Free ("x","RealDef.real")] : term list
14.123
14.124 - val (dsc,vl) = (I_Model.split_dts o Thm.term_of o the o(parse thy))
14.125 + val (dsc,vl) = (O_Model.split_dts o Thm.term_of o the o(parse thy))
14.126 "errorBound (eps=#0)";
14.127 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
14.128 pbl_ids ctxt dsc vl;
15.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 07 12:15:37 2020 +0200
15.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 07 14:11:03 2020 +0200
15.3 @@ -148,7 +148,7 @@
15.4 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
15.5 val thy = ThyC.get_theory dI;
15.6 mI = ["no_met"]; (*false*)
15.7 - val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
15.8 + val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> O_Model.prep_ori fmz thy, mI)
15.9 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
15.10 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
15.11 val dI = Context.theory_name (ThyC.parent_of thy thy');
16.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu May 07 12:15:37 2020 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu May 07 14:11:03 2020 +0200
16.3 @@ -14,7 +14,7 @@
16.4 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : Spec.T) = (fmz, sp);
16.5 val thy = ThyC.get_theory dI;
16.6 (*if*) mI = ["no_met"]; (*else*)
16.7 - val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
16.8 + val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> O_Model.prep_ori fmz thy, mI)
16.9 val {cas, ppc, thy=thy',...} = get_pbt pI
16.10 val dI = Context.theory_name (ThyC.parent_of thy thy');
16.11 val hdl =
16.12 @@ -44,7 +44,7 @@
16.13 (*if*) mI = ["no_met"] = false (*else*);
16.14 val xxx = Specify.get_pbt pI
16.15 val yyy = #ppc xxx
16.16 -val (oris, ctxt) = Specify.prep_ori fmz thy yyy
16.17 +val (oris, ctxt) = O_Model.prep_ori fmz thy yyy
16.18 ;
16.19 case oris of
16.20 ((1, [1], "#Given", Const ("Input_Descript.equality", _),
16.21 @@ -52,7 +52,7 @@
16.22 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
16.23 | _ => error ""
16.24
16.25 -"~~~~~ fun prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
16.26 +"~~~~~ fun O_Model.prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
16.27 val ctxt = ContextC.initialise' thy fmz;
16.28 (*ADD check*)
16.29 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
17.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Thu May 07 12:15:37 2020 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Thu May 07 14:11:03 2020 +0200
17.3 @@ -82,7 +82,7 @@
17.4 (thy, ori, (hd icl));
17.5 "~~~~~ to return val:"; val xxx =
17.6 ( fd,
17.7 - ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts) : TermC.as_string
17.8 + ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts) : TermC.as_string
17.9 );
17.10 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
17.11
18.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu May 07 12:15:37 2020 +0200
18.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Thu May 07 14:11:03 2020 +0200
18.3 @@ -257,7 +257,7 @@
18.4 val thy' = "Test";
18.5 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
18.6 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
18.7 -val oris = prep_ori ctl thy
18.8 +val oris = O_Model.prep_ori ctl thy
18.9 ((#ppc o get_pbt)
18.10 ["sqroot-test","univariate","equation","test"]);
18.11 val loc = Istate.empty;
19.1 --- a/test/Tools/isac/Specify/calchead.sml Thu May 07 12:15:37 2020 +0200
19.2 +++ b/test/Tools/isac/Specify/calchead.sml Thu May 07 14:11:03 2020 +0200
19.3 @@ -542,7 +542,7 @@
19.4 val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
19.5 val ttt = (dsc $ var);
19.6 Thm.global_cterm_of thy (dsc $ var);
19.7 -val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
19.8 +val ori = ((([1], str, dsc, (*[var]*) O_Model.split_dts' (dsc, var))): O_Model.preori);
19.9
19.10 "-d2-----------------------------------------------------";
19.11 pbt = []; (*false*)
19.12 @@ -555,7 +555,7 @@
19.13 val (thy, (str, (dsc, _)):Model_Pattern.single, ty $ var) = (thy, p, a);
19.14 val ttt = (dsc $ var);
19.15 Thm.global_cterm_of thy (dsc $ var);
19.16 -val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
19.17 +val ori = ((([1], str, dsc, (*[var]*) O_Model.split_dts' (dsc, var))): O_Model.preori);
19.18 "-d3-----------------------------------------------------";
19.19 pbt = []; (*true, base case*)
19.20 "-----------------continue step through code match_ags---";
19.21 @@ -575,7 +575,7 @@
19.22 (is_copy_named_generating_idstr o free2str) t;
19.23 "--------------------------------------------------------";
19.24 is_copy_named_generating p (*true*);
19.25 - fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts);
19.26 + fun sel (_,_,d,ts) = O_Model.comp_ts (d, ts);
19.27 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
19.28 (*"v_v" OLD: "v_"*)
19.29 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
19.30 @@ -814,7 +814,7 @@
19.31 (*#############################^^^^^^^^^ defined by Isabelle*)
19.32 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
19.33 [Free ("N", _ (*"Real.real"*))])],
19.34 - _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
19.35 + _ ) = O_Model.prep_ori fmz thy ((#ppc o get_pbt) pI);
19.36 "#undef means: the element with description TERM in fmz did not match ";
19.37 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
19.38 "defined in Simplify.thy";
19.39 @@ -842,7 +842,7 @@
19.40 (*########################^^^^^^^^^ defined in Simplify.thy*)
19.41 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
19.42 [Free ("N", _ )])],
19.43 - _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
19.44 + _ ) = O_Model.prep_ori fmz thy ((#ppc o get_pbt) pI);
19.45
19.46 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
19.47 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
20.1 --- a/test/Tools/isac/Specify/o-model.sml Thu May 07 12:15:37 2020 +0200
20.2 +++ b/test/Tools/isac/Specify/o-model.sml Thu May 07 14:11:03 2020 +0200
20.3 @@ -28,15 +28,15 @@
20.4 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
20.5 val thy = ThyC.get_theory dI;
20.6 (*if*) mI = ["no_met"] (*else*);
20.7 - val (pI, (pors, pctxt), mI) = (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI);
20.8 + val (pI, (pors, pctxt), mI) = (pI, Specify.get_pbt pI |> #ppc |> Specify.O_Model.prep_ori fmz thy, mI);
20.9
20.10 (*+*)Specify.get_pbt pI: Problem.T;
20.11 (*+*)(Specify.get_pbt pI |> #ppc): Model_Pattern.T;
20.12 (*+*)val (o_model, _) = (Specify.get_pbt pI |> #ppc |>
20.13 - Specify.prep_ori fmz thy): O_Model.T * Proof.context;
20.14 -"~~~~~ fun prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, Specify.get_pbt pI |> #ppc);
20.15 + Specify.O_Model.prep_ori fmz thy): O_Model.T * Proof.context;
20.16 +"~~~~~ fun O_Model.prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, Specify.get_pbt pI |> #ppc);
20.17 val ctxt = ContextC.initialise' thy fmz;
20.18 - val ori = map (add_field thy pbt o I_Model.split_dts o TermC.parseNEW' ctxt) fmz
20.19 + val ori = map (add_field thy pbt o O_Model.split_dts o TermC.parseNEW' ctxt) fmz
20.20 |> add_variants;
20.21 val maxv = map fst ori |> max;
20.22 val maxv = if maxv = 0 then 1 else maxv;
20.23 @@ -46,8 +46,8 @@
20.24 |> add_id
20.25 |> map flattup;
20.26
20.27 - (oris, ctxt) (*return from prep_ori*);
20.28 -"~~~~~ from fun prep_ori \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);
20.29 + (oris, ctxt) (*return from O_Model.prep_ori*);
20.30 +"~~~~~ from fun O_Model.prep_ori \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);
20.31
20.32 (* final test ...*)
20.33 (*+*)if O_Model.to_string pors = "[\n" ^
21.1 --- a/test/Tools/isac/Specify/ptyps.sml Thu May 07 12:15:37 2020 +0200
21.2 +++ b/test/Tools/isac/Specify/ptyps.sml Thu May 07 14:11:03 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) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
21.8 -val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
21.9 +val (d1,ts1) = O_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
21.10 +val (d2,ts2) = O_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)]: O_Model.T;
21.12
21.13 (*case 2: refined to pbt without children *)
21.14 -val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
21.15 +val (d2,ts2) = O_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)]:O_Model.T;
21.17
21.18 (*case 3: refined to pbt with children *)
21.19 -val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
21.20 +val (d2,ts2) = O_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)]:O_Model.T;
21.22
21.23 (*case 4: refined to children (without child)*)
21.24 -val (d3,ts3) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
21.25 +val (d3,ts3) = O_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)]:O_Model.T;
21.27
21.28 (*=================================================================