1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu May 07 11:04:02 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu May 07 11:42:19 2020 +0200
1.3 @@ -32,7 +32,7 @@
1.4 ML_file "store.sml"
1.5 ML_file "check-unique.sml"
1.6 ML_file "specification.sml"
1.7 -ML_file "celem-4.sml" (*pat*)
1.8 +ML_file "model-pattern.sml"
1.9 ML_file "problem-def.sml"
1.10 ML_file "method-def.sml"
1.11 ML_file "cas-def.sml"
2.1 --- a/src/Tools/isac/BaseDefinitions/celem-4.sml Thu May 07 11:04:02 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,36 +0,0 @@
2.4 -(* Title: BaseDefinitions/celem-4.sml
2.5 - Author: Walther Neuper
2.6 - (c) due to copyright terms
2.7 -
2.8 - *)
2.9 -signature CALCELEMENT_4 =
2.10 -sig
2.11 - type pat
2.12 - val pats2str: pat list -> string
2.13 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.14 - val pats2str' : pat list -> string
2.15 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.16 - (*NONE*)
2.17 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.18 - (*NONE*)
2.19 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.20 -end
2.21 -
2.22 -(**)
2.23 -structure Celem4(**): CALCELEMENT_4(**) =
2.24 -struct
2.25 -(**)
2.26 -
2.27 -(* the pattern for an item of a problems model or a methods guard *)
2.28 -type pat =
2.29 - (string * (* field *)
2.30 - (term * (* description *)
2.31 - term)) (* id | arbitrary term *);
2.32 -fun pat2str ((field, (dsc, id)) : pat) =
2.33 - pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id))
2.34 -fun pats2str pats = (strs2str o (map pat2str)) pats
2.35 -fun pat2str' ((field, (dsc, id)) : pat) =
2.36 - pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n"
2.37 -fun pats2str' pats = (strs2str o (map pat2str')) pats
2.38 -
2.39 -(**)end(**)
3.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Thu May 07 11:04:02 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Thu May 07 11:42:19 2020 +0200
3.3 @@ -55,7 +55,7 @@
3.4 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
3.5 (*TODO: abstract to ?pre_model?...*)
3.6 prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
3.7 - ppc : Celem4.pat list, (* items in given, find, relate;
3.8 + ppc : Model_Pattern.T, (* items in given, find, relate;
3.9 items (in "#Find") which need not occur in the arg-list of a SubProblem
3.10 are 'copy-named' with an identifier "*'.'".
3.11 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Thu May 07 11:42:19 2020 +0200
4.3 @@ -0,0 +1,40 @@
4.4 +(* Title: BaseDefinitions/model-pattern.sml
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +
4.8 +A pattern to be combined with a formalisation (Formalise.T) yielding an O_Model.T..
4.9 +*)
4.10 +signature MODEL_PATTERN =
4.11 +sig
4.12 + type T
4.13 +(*type pat*)
4.14 + type single
4.15 +(*val pats2str: single list -> string*)
4.16 + val to_string: single list -> string
4.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.18 +(*val pats2str': single list -> string*)
4.19 + val to_string': single list -> string
4.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.21 + (*NONE*)
4.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.23 +end
4.24 +
4.25 +(**)
4.26 +structure Model_Pattern(**): MODEL_PATTERN(**) =
4.27 +struct
4.28 +(**)
4.29 +
4.30 +(* the pattern for an item of a problems model or a methods guard *)
4.31 +type m_field = string;
4.32 +type single =
4.33 + (m_field * (* field *)
4.34 + (term * (* description *)
4.35 + term)) (* id | arbitrary term *);
4.36 +type T = single list;
4.37 +
4.38 +fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
4.39 +fun to_string pats = (strs2str o (map pat2str)) pats;
4.40 +fun pat2str' (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n";
4.41 +fun to_string' pats = (strs2str o (map pat2str')) pats;
4.42 +
4.43 +(**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Thu May 07 11:04:02 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Thu May 07 11:42:19 2020 +0200
5.3 @@ -52,7 +52,7 @@
5.4 (*TODO: abstract to ?pre_model?...*)
5.5 prls : Rule_Set.T, (* for preds in where_ *)
5.6 where_ : term list, (* where - predicates *)
5.7 - ppc : Celem4.pat list (* this is the model-pattern;
5.8 + ppc : Model_Pattern.T (* this is the model-pattern;
5.9 it contains "#Given","#Where","#Find","#Relate"-patterns
5.10 for constraints on identifiers see "fun cpy_nam" *)
5.11 }
5.12 @@ -62,7 +62,7 @@
5.13 prls = prls', thy = thy', where_ = w'} : T)
5.14 = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
5.15 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
5.16 - ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "
5.17 + ^ (strslist2strs met') ^ ", ppc = " ^ Model_Pattern.to_string ppc' ^ ", prls = "
5.18 ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
5.19 ^ (UnparseC.terms w') ^ "}" |> linefeed;
5.20 fun s_to_string pbts = map pbt2str pbts |> list2str;
6.1 --- a/src/Tools/isac/Specify/calchead.sml Thu May 07 11:04:02 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu May 07 11:42:19 2020 +0200
6.3 @@ -77,7 +77,7 @@
6.4 val ocalhd_complete : I_Model.T -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool
6.5 val all_modspec : Calc.T -> Calc.T
6.6
6.7 - val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Celem4.pat list -> I_Model.T
6.8 + val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
6.9 val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T
6.10
6.11 val complete_mod : Calc.T -> Calc.T
6.12 @@ -91,7 +91,7 @@
6.13 val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list
6.14 val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list
6.15
6.16 - val match_ags : theory -> Celem4.pat list -> term list -> O_Model.T
6.17 + val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T
6.18 val match_ags_msg : Problem.id -> term -> term list -> unit
6.19 val oris2fmz_vals : O_Model.T -> string list * term list
6.20 val vars_of_pbl_' : ('a * ('b * term)) list -> term list
6.21 @@ -117,10 +117,10 @@
6.22 val is_copy_named_generating_idstr : string -> bool
6.23 val is_copy_named_generating : 'a * ('b * term) -> bool
6.24 val is_copy_named : 'a * ('b * term) -> bool
6.25 - val ori2Coritm : Celem4.pat list -> O_Model.single -> I_Model.single
6.26 + val ori2Coritm : Model_Pattern.T -> O_Model.single -> I_Model.single
6.27 val matc : theory -> (string * (term * term)) list -> term list -> O_Model.preori list -> O_Model.preori list
6.28 - val mtc : theory -> Celem4.pat -> term -> O_Model.preori option
6.29 - val cpy_nam : Celem4.pat list -> O_Model.preori list -> Celem4.pat -> O_Model.preori
6.30 + val mtc : theory -> Model_Pattern.single -> term -> O_Model.preori option
6.31 + val cpy_nam : Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori
6.32 datatype additm = Add of I_Model.single | Err of string
6.33 val appl_add: Proof.context -> string -> O_Model.T ->
6.34 I_Model.T -> (string * (term * term)) list -> TermC.as_string -> additm
6.35 @@ -584,7 +584,7 @@
6.36 fun matc _ [] _ oris = oris
6.37 | matc _ pbt [] _ =
6.38 (tracing (dashs 70);
6.39 - error ("actual arg(s) missing for '" ^ Celem4.pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
6.40 + error ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
6.41 | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
6.42 (*del?..*)if (is_copy_named_idstr o TermC.free2str) t then oris
6.43 else(*..del?*)
6.44 @@ -633,7 +633,7 @@
6.45 val pats = (#ppc o Specify.get_pbt) pI
6.46 val msg = (dots 70 ^ "\n"
6.47 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
6.48 - ^ "*** model-pattern " ^ Celem4.pats2str pats ^ "\n"
6.49 + ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
6.50 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
6.51 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
6.52 ^ dashs 70)
7.1 --- a/src/Tools/isac/Specify/ptyps.sml Thu May 07 11:04:02 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/ptyps.sml Thu May 07 11:42:19 2020 +0200
7.3 @@ -66,7 +66,7 @@
7.4 val show_pblguhs : unit -> unit
7.5 val sort_pblguhs : unit -> unit
7.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.7 - val add_field : theory -> Celem4.pat list -> term * 'b -> string * term * 'b
7.8 + val add_field : theory -> Model_Pattern.T -> term * 'b -> string * term * 'b
7.9 val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
7.10 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
7.11 val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
8.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Thu May 07 11:04:02 2020 +0200
8.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Thu May 07 11:42:19 2020 +0200
8.3 @@ -244,13 +244,13 @@
8.4 (1, ["1"], #Given,Streckenlast, ["q_0"]),
8.5 (2, ["1"], #Given,FunktionsVariable, ["x"]),
8.6 (3, ["1"], #Find,Funktionen, ["funs'''"])]*)
8.7 -(*+*)writeln (pats2str' ppc);
8.8 +(*+*)writeln (Model_Pattern.to_string' ppc);
8.9 (*["(#Given, (Streckenlast, q__q))
8.10 ","(#Given, (FunktionsVariable, v_v))
8.11 ","(#Given, (Biegelinie, id_fun))
8.12 ","(#Given, (AbleitungBiegelinie, id_abl))
8.13 ","(#Find, (Funktionen, fun_s))"]*)
8.14 -(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
8.15 +(*+*)writeln (Model_Pattern.to_string' ((#ppc o Specify.get_pbt) pI));
8.16 (*["(#Given, (Streckenlast, q_q))
8.17 ","(#Given, (FunktionsVariable, v_v))
8.18 ","(#Find, (Funktionen, funs'''))"]*)
9.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Thu May 07 11:04:02 2020 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Thu May 07 11:42:19 2020 +0200
9.3 @@ -63,12 +63,12 @@
9.4 fun testi_vt v itm = (curry (op mem) v) (#2 (itm:I_Model.single));
9.5 fun test_id ids r = curry (op mem) (#1 (r:O_Model.single)) ids;
9.6 fun test_subset (itm:I_Model.single) ((_,_,_,d,ts):O_Model.single) =
9.7 - (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
9.8 - fun false_and_not_Sup((i,v,false,f,Sup _):I_Model.single) = false
9.9 + (I_Model.d_in (#5 itm)) = d andalso subset op = (I_Model.ts_in (#5 itm), ts);
9.10 + fun false_and_not_Sup((i,v,false,f,I_Model.Sup _):I_Model.single) = false
9.11 | false_and_not_Sup (i,v,false,f, _) = true
9.12 | false_and_not_Sup _ = false;
9.13 end
9.14 - val v = if itms = [] then 1 else max_vt itms;
9.15 + val v = if itms = [] then 1 else I_Model.max_vt itms;
9.16 val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
9.17 val vits = if v = 0 then itms (*because of dsc without dat*)
9.18 else filter (testi_vt v) itms; (*itms..vat*)
9.19 @@ -82,7 +82,7 @@
9.20 (thy, ori, (hd icl));
9.21 "~~~~~ to return val:"; val xxx =
9.22 ( fd,
9.23 - ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string
9.24 + ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts) : TermC.as_string
9.25 );
9.26 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
9.27
10.1 --- a/test/Tools/isac/Specify/calchead.sml Thu May 07 11:04:02 2020 +0200
10.2 +++ b/test/Tools/isac/Specify/calchead.sml Thu May 07 11:42:19 2020 +0200
10.3 @@ -377,7 +377,7 @@
10.4 ============ inhibit exn AK110726 ==============================================*)
10.5 "-c1-----------------------------------------------------";
10.6 "--------------------------step through code match_ags---";
10.7 -val (thy, pbt: Celem4.pat list, ags) = (@{theory "EqSystem"}, pats, ags);
10.8 +val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);
10.9 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
10.10 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
10.11 val cy = filter is_copy_named pbt; (*=solution*)
10.12 @@ -392,7 +392,7 @@
10.13 val opt - mtc thy p a;
10.14 ============ inhibit exn AK110726 ==============================================*)
10.15 "--------------------------------step through code mtc---";
10.16 -val (thy, (str, (dsc, _)): Celem4.pat, ty $ var) = (thy, p, a);
10.17 +val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
10.18 Thm.global_cterm_of;
10.19 val ttt = (dsc $ var);
10.20 (*============ inhibit exn AK110726 ==============================================
10.21 @@ -468,7 +468,7 @@
10.22 -------------------------------------------------------------------*)
10.23 "-c1-----------------------------------------------------";
10.24 "--------------------------step through code match_ags---";
10.25 -val (thy, pbt: Celem4.pat list, ags) = (@{theory "EqSystem"}, pats, ags);
10.26 +val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);
10.27 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
10.28 val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*)
10.29 val cy = filter is_copy_named pbt; (*=solution*)
10.30 @@ -483,7 +483,7 @@
10.31 val opt - mtc thy p a;
10.32 -------------------------------------------------------------------*)
10.33 "--------------------------------step through code mtc---";
10.34 -val (thy, (str, (dsc, _)): Celem4.pat, ty $ var) = (thy, p, a);
10.35 +val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
10.36 Thm.global_cterm_of;
10.37 val ttt = (dsc $ var);
10.38 (*============ inhibit exn AK110726 ==============================================
10.39 @@ -528,7 +528,7 @@
10.40 val PATS = (#ppc o get_pbt) pI;
10.41 "-d1-----------------------------------------------------";
10.42 "--------------------------step through code match_ags---";
10.43 -val (thy, pbt: Celem4.pat list, ags) = (@{theory "Test"}, PATS, AGS);
10.44 +val (thy, pbt: Model_Pattern.T, ags) = (@{theory "Test"}, PATS, AGS);
10.45 fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
10.46 val pbt' = filter_out is_copy_named pbt;
10.47 val cy = filter is_copy_named pbt;
10.48 @@ -539,7 +539,7 @@
10.49 "---if False:...";
10.50 val opt = mtc thy p a;
10.51 "--------------------------------step through code mtc---";
10.52 -val (thy, (str, (dsc, _)): Celem4.pat, ty $ var) = (thy, p, a);
10.53 +val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);
10.54 val ttt = (dsc $ var);
10.55 Thm.global_cterm_of thy (dsc $ var);
10.56 val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
10.57 @@ -552,7 +552,7 @@
10.58 "---if False:...";
10.59 val opt = mtc thy p a;
10.60 "--------------------------------step through code mtc---";
10.61 -val (thy, (str, (dsc, _)):Celem4.pat, ty $ var) = (thy, p, a);
10.62 +val (thy, (str, (dsc, _)):Model_Pattern.single, ty $ var) = (thy, p, a);
10.63 val ttt = (dsc $ var);
10.64 Thm.global_cterm_of thy (dsc $ var);
10.65 val ori = ((([1], str, dsc, (*[var]*) I_Model.split_dts' (dsc, var))): O_Model.preori);
10.66 @@ -561,7 +561,7 @@
10.67 "-----------------continue step through code match_ags---";
10.68 val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*)
10.69 "--------------------------------step through cpy_nam----";
10.70 -val (pbt, oris, p as (field, (dsc, t)):Celem4.pat) = (pbt', oris', hd cy);
10.71 +val (pbt, oris, p as (field, (dsc, t)):Model_Pattern.single) = (pbt', oris', hd cy);
10.72 (*t = "v_v'i'" : term OLD: t = "v_i_"*)
10.73 "--------------------------------------------------------";
10.74 fun is_copy_named_generating_idstr str =
10.75 @@ -575,7 +575,7 @@
10.76 (is_copy_named_generating_idstr o free2str) t;
10.77 "--------------------------------------------------------";
10.78 is_copy_named_generating p (*true*);
10.79 - fun sel (_,_,d,ts) = comp_ts (d, ts);
10.80 + fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts);
10.81 val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t;
10.82 (*"v_v" OLD: "v_"*)
10.83 val ext = (last_elem o drop_last o Symbol.explode o free2str) t;
11.1 --- a/test/Tools/isac/Specify/o-model.sml Thu May 07 11:04:02 2020 +0200
11.2 +++ b/test/Tools/isac/Specify/o-model.sml Thu May 07 11:42:19 2020 +0200
11.3 @@ -31,7 +31,7 @@
11.4 val (pI, (pors, pctxt), mI) = (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI);
11.5
11.6 (*+*)Specify.get_pbt pI: Problem.T;
11.7 -(*+*)(Specify.get_pbt pI |> #ppc): Celem4.pat list;
11.8 +(*+*)(Specify.get_pbt pI |> #ppc): Model_Pattern.T;
11.9 (*+*)val (o_model, _) = (Specify.get_pbt pI |> #ppc |>
11.10 Specify.prep_ori fmz thy): O_Model.T * Proof.context;
11.11 "~~~~~ fun prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, Specify.get_pbt pI |> #ppc);