1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Feb 14 10:54:53 2018 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Feb 14 12:20:35 2018 +0100
1.3 @@ -73,7 +73,7 @@
1.4 ML {*
1.5 *} ML {*
1.6 *}
1.7 -ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.8 +ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.9 ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
1.10 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
1.11 ML {* print_exn_unit *}
2.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Feb 14 10:54:53 2018 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed Feb 14 12:20:35 2018 +0100
2.3 @@ -434,11 +434,11 @@
2.4 case get_obj g_env pt p of
2.5 SOME _ =>
2.6 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
2.7 - e_term, [], Selem.e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
2.8 + e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID))
2.9 | NONE => Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
2.10 else (*somewhere later in the script*)
2.11 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
2.12 - e_term, [], Selem.e_ctxt, subpbl domID pblID))
2.13 + e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID))
2.14 | applicable_in _ _ (Tac.End_Subproblem) =
2.15 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Subproblem)
2.16 | applicable_in _ _ (Tac.CAScmd ct') =
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Feb 14 10:54:53 2018 +0100
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Feb 14 12:20:35 2018 +0100
3.3 @@ -448,7 +448,7 @@
3.4 in case find_first (eq2 d) ppc of
3.5 NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))
3.6 | SOME (i', _, _, _, itm_) =>
3.7 - if is_list_dsc d
3.8 + if LTool.is_list_dsc d
3.9 then
3.10 let
3.11 val in_itm = Model.ts_in itm_
3.12 @@ -1090,7 +1090,7 @@
3.13 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
3.14 val dI = if dI = "" then theory2theory' thy else dI
3.15 val mI = if mI = [] then hd met else mI
3.16 - val hdl = case cas of NONE => pblterm dI pI | SOME t => t
3.17 + val hdl = case cas of NONE => LTool.pblterm dI pI | SOME t => t
3.18 val (pt,_) = cappend_problem e_ctree [] (Selem.Uistate, Selem.e_ctxt) ([], (dI, pI, mI))
3.19 ([], (dI,pI,mI), hdl)
3.20 val pt = update_spec pt [] (dI, pI, mI)
3.21 @@ -1130,7 +1130,7 @@
3.22 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
3.23 val dI = theory2theory' (maxthy thy thy')
3.24 val hdl = case cas of
3.25 - NONE => pblterm dI pI
3.26 + NONE => LTool.pblterm dI pI
3.27 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
3.28 val (pt, _) =
3.29 cappend_problem e_ctree [] (Selem.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
3.30 @@ -1291,7 +1291,7 @@
3.31 val (dI, pI, _) = get_somespec' spec spec'
3.32 val {cas, ...} = Specify.get_pbt pI
3.33 in case cas of
3.34 - NONE => Form (pblterm dI pI)
3.35 + NONE => Form (LTool.pblterm dI pI)
3.36 | SOME t => Form (subst_atomic (Model.mk_env probl) t)
3.37 end
3.38
4.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Feb 14 10:54:53 2018 +0100
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Wed Feb 14 12:20:35 2018 +0100
4.3 @@ -49,11 +49,11 @@
4.4 | Rls {scr = EmptyScr, ...} =>
4.5 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
4.6 "use prep_rls' for storing rule-sets !")
4.7 - | Rls {scr = Prog s, ...} => (Selem.ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
4.8 + | Rls {scr = Prog s, ...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
4.9 | Seq {scr=EmptyScr,...} =>
4.10 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
4.11 "use prep_rls' for storing rule-sets !")
4.12 - | Seq {scr = Prog s,...} => (Selem.ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
4.13 + | Seq {scr = Prog s,...} => (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, e_term, Selem.Sundef, true))
4.14 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
4.15 | init_istate (Tac.Rewrite_Set_Inst (subs, rls)) t =
4.16 let
4.17 @@ -66,14 +66,14 @@
4.18 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
4.19 "use prep_rls' for storing rule-sets !")
4.20 | Rls {scr = Prog s, ...} =>
4.21 - let val (form, bdv) = two_scr_arg s
4.22 + let val (form, bdv) = LTool.two_scr_arg s
4.23 in (Selem.ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Selem.Sundef,true))
4.24 end
4.25 | Seq {scr = EmptyScr, ...} =>
4.26 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
4.27 "use prep_rls' for storing rule-sets !")
4.28 | Seq {scr = Prog s,...} =>
4.29 - let val (form, bdv) = two_scr_arg s
4.30 + let val (form, bdv) = LTool.two_scr_arg s
4.31 in (Selem.ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Selem.Sundef,true))
4.32 end
4.33 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
4.34 @@ -261,7 +261,7 @@
4.35 val p' = lev_up p
4.36 val (pt, c) = append_result pt p' l tasm Complete
4.37 in
4.38 - ((p', Res), c, FormKF (term2str t), pt)
4.39 + ((p', Res), c, FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
4.40 end
4.41 | generate1 _ (Tac.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt =
4.42 let
4.43 @@ -294,7 +294,7 @@
4.44 val (pt, _) = cappend_form pt p (is, ctxt') f
4.45 val pt = update_branch pt p TransitiveB
4.46 val is = init_istate (Tac.Rewrite_Set_Inst (Selem.subst2subs subs, id_rls rls)) f
4.47 - val tac_ = Tac.Apply_Method' (e_metID, SOME t, is, ctxt')
4.48 + val tac_ = Tac.Apply_Method' (e_metID, SOME e_term (*t ..has not been declared*), is, ctxt')
4.49 val pos' = ((lev_on o lev_dn) p, Frm)
4.50 in
4.51 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
4.52 @@ -313,7 +313,7 @@
4.53 val (pt, _) = cappend_form pt p (is, ctxt') f
4.54 val pt = update_branch pt p TransitiveB
4.55 val is = init_istate (Tac.Rewrite_Set (id_rls rls)) f
4.56 - val tac_ = Tac.Apply_Method' (e_metID, SOME t, is, ctxt')
4.57 + val tac_ = Tac.Apply_Method' (e_metID, SOME e_term (*t ..has not been declared*), is, ctxt')
4.58 val pos' = ((lev_on o lev_dn) p, Frm)
4.59 in
4.60 generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*)
5.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Feb 14 10:54:53 2018 +0100
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Feb 14 12:20:35 2018 +0100
5.3 @@ -131,7 +131,7 @@
5.4 val _ = (term_to_string''' dI t)
5.5 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
5.6 in itm end
5.7 - handle _ => (i, v, false, f, Model.Syn (term2str t)))
5.8 + handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
5.9 | parsitm dI (i, v, b, f, Model.Syn str) =
5.10 (let val _ = (Thm.term_of o the o (parse dI)) str
5.11 in (i, v, b ,f, Model.Par str) end
5.12 @@ -145,19 +145,19 @@
5.13 val _ = term_to_string''' dI t;
5.14 (*this ^ should raise the exn on unability of re-parsing dts*)
5.15 in itm end
5.16 - handle _ => (i, v, false, f, Model.Syn (term2str t)))
5.17 + handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
5.18 | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
5.19 (let val t = Model.comp_dts (d,ts);
5.20 val _ = term_to_string''' dI t;
5.21 (*this ^ should raise the exn on unability of re-parsing dts*)
5.22 in itm end
5.23 - handle _ => (i, v, false, f, Model.Syn (term2str t)))
5.24 + handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
5.25 | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
5.26 (let val t = d $ t';
5.27 val _ = term_to_string''' dI t;
5.28 (*this ^ should raise the exn on unability of re-parsing dts*)
5.29 in itm end
5.30 - handle _ => (i, v, false, f, Model.Syn (term2str t)))
5.31 + handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
5.32 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
5.33 error ("parsitm (" ^ Model.itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
5.34
6.1 --- a/src/Tools/isac/Interpret/model.sml Wed Feb 14 10:54:53 2018 +0100
6.2 +++ b/src/Tools/isac/Interpret/model.sml Wed Feb 14 12:20:35 2018 +0100
6.3 @@ -130,36 +130,36 @@
6.4 (* special handling for lists. ?WN:14.5.03 ??!? *)
6.5 fun dest_list (d, ts) =
6.6 let fun dest t =
6.7 - if is_list_dsc d andalso not (is_unl d) andalso not (is_var t) (*..for pbt*)
6.8 + if LTool.is_list_dsc d andalso not (LTool.is_unl d) andalso not (is_var t) (*..for pbt*)
6.9 then isalist2list t
6.10 else [t]
6.11 in (flat o (map dest)) ts end;
6.12
6.13 (* revert split_dts only for ts; compare comp_dts *)
6.14 fun comp_ts (d, ts) =
6.15 - if is_list_dsc d
6.16 + if LTool.is_list_dsc d
6.17 then if is_list (hd ts)
6.18 - then if is_unl d
6.19 + then if LTool.is_unl d
6.20 then (hd ts) (* e.g. someList [1,3,2] *)
6.21 else (take_apart_inv ts) (* [ [a], [b] ] -> [a,b] *)
6.22 else (hd ts) (* a variable or metavariable for a list *)
6.23 else (hd ts);
6.24 fun comp_dts (d, []) =
6.25 - if is_reall_dsc d
6.26 + if LTool.is_reall_dsc d
6.27 then (d $ e_listReal)
6.28 - else if is_booll_dsc d then (d $ e_listBool) else d
6.29 + else if LTool.is_booll_dsc d then (d $ e_listBool) else d
6.30 | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
6.31 handle _ => error ("comp_dts: " ^ term2str d ^ " $ " ^ term2str (hd ts));
6.32 fun comp_dts' (d, []) =
6.33 - if is_reall_dsc d
6.34 + if LTool.is_reall_dsc d
6.35 then (d $ e_listReal)
6.36 - else if is_booll_dsc d then (d $ e_listBool) else d
6.37 + else if LTool.is_booll_dsc d then (d $ e_listBool) else d
6.38 | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
6.39 handle _ => error ("comp_dts': " ^ term2str d ^ " $ " ^ term2str (hd ts));
6.40 fun comp_dts'' (d, []) =
6.41 - if is_reall_dsc d
6.42 + if LTool.is_reall_dsc d
6.43 then term2str (d $ e_listReal)
6.44 - else if is_booll_dsc d
6.45 + else if LTool.is_booll_dsc d
6.46 then term2str (d $ e_listBool)
6.47 else term2str d
6.48 | comp_dts'' (d, ts) = term2str (d $ (comp_ts (d, ts)))
6.49 @@ -168,24 +168,24 @@
6.50 (* decompose an input into description, terms (ev. elems of lists),
6.51 and the value for the problem-environment; inv to comp_dts *)
6.52 fun split_dts (t as d $ arg) =
6.53 - if is_dsc d
6.54 - then if is_list_dsc d andalso is_list arg andalso is_unl d |> not
6.55 + if LTool.is_dsc d
6.56 + then if LTool.is_list_dsc d andalso is_list arg andalso LTool.is_unl d |> not
6.57 then (d, take_apart arg)
6.58 else (d, [arg])
6.59 else (e_term, dest_list' t)
6.60 | split_dts t =
6.61 let val t' as (h, _) = strip_comb t;
6.62 in
6.63 - if is_dsc h
6.64 + if LTool.is_dsc h
6.65 then (h, dest_list t')
6.66 else (e_term, dest_list' t)
6.67 end;
6.68 (* version returning ts only *)
6.69 fun split_dts' (d, arg) =
6.70 - if is_dsc d
6.71 - then if is_list_dsc d
6.72 + if LTool.is_dsc d
6.73 + then if LTool.is_list_dsc d
6.74 then if is_list arg
6.75 - then if is_unl d
6.76 + then if LTool.is_unl d
6.77 then ([arg]) (* e.g. someList [1,3,2] *)
6.78 else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *)
6.79 else ([arg]) (* a variable or metavariable for a list *)
7.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Feb 14 10:54:53 2018 +0100
7.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed Feb 14 12:20:35 2018 +0100
7.3 @@ -340,7 +340,7 @@
7.4 calc =
7.5 if scr = "empty_script"
7.6 then []
7.7 - else ((assoc_calc' thy |> map) o (map op_of_calc) o (filter is_calc) o stacpbls) sc,
7.8 + else ((assoc_calc' thy |> map) o (map LTool.op_of_calc) o (filter LTool.is_calc) o LTool.stacpbls) sc,
7.9 crls = cr, errpats = ep, nrls = nr, scr = Prog sc}: met, metID: metID)
7.10 end;
7.11
8.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Feb 14 10:54:53 2018 +0100
8.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Feb 14 12:20:35 2018 +0100
8.3 @@ -452,7 +452,7 @@
8.4 (* try if a rewrite-rule is applicable to a given formula;
8.5 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
8.6 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =
8.7 - if contains_bdv thm
8.8 + if LTool.contains_bdv thm
8.9 then case rewrite_inst_ thy ro erls false subst thm f of
8.10 SOME _ => [Tac.rule2tac thy subst thm']
8.11 | NONE => []
8.12 @@ -581,7 +581,7 @@
8.13 "Theorems" =>
8.14 let val thm = Global_Theory.get_thm (assoc_thy (thyID2theory' thyID)) xstr
8.15 in
8.16 - if contains_bdv thm
8.17 + if LTool.contains_bdv thm
8.18 then
8.19 let
8.20 val formal_arg = str2term "v_"
8.21 @@ -593,7 +593,7 @@
8.22 let
8.23 val rules = (get_rules o assoc_rls) xstr
8.24 in
8.25 - if contain_bdv rules
8.26 + if LTool.contain_bdv rules
8.27 then
8.28 let
8.29 val formal_arg = str2term "v_"
9.1 --- a/src/Tools/isac/Interpret/script.sml Wed Feb 14 10:54:53 2018 +0100
9.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Feb 14 12:20:35 2018 +0100
9.3 @@ -182,7 +182,7 @@
9.4 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
9.5 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
9.6 thus "NONE" must be set at the end of currying (ill designed anyway)*)
9.7 -fun upd_env_opt env (SOME a, v) = upd_env env (a, v)
9.8 +fun upd_env_opt env (SOME a, v) = LTool.upd_env env (a, v)
9.9 | upd_env_opt env (NONE, _) =
9.10 ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);
9.11
9.12 @@ -273,9 +273,9 @@
9.13 val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals
9.14 val hdl =
9.15 case cas of
9.16 - NONE => pblterm dI pI
9.17 + NONE => LTool.pblterm dI pI
9.18 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
9.19 - val f = subpbl (strip_thy dI) pI
9.20 + val f = LTool.subpbl (strip_thy dI) pI
9.21 in (Tac.Subproblem (dI, pI), Tac.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
9.22 end
9.23 | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
9.24 @@ -435,9 +435,9 @@
9.25 val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals
9.26 val hdl =
9.27 case cas of
9.28 - NONE => pblterm dI pI
9.29 + NONE => LTool.pblterm dI pI
9.30 | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
9.31 - val f = subpbl (strip_thy dI) pI
9.32 + val f = LTool.subpbl (strip_thy dI) pI
9.33 in
9.34 if domID = dI andalso pblID = pI
9.35 then Ass (Tac.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
9.36 @@ -537,24 +537,24 @@
9.37 *)
9.38 fun handle_leaf call thy srls E a v t =
9.39 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
9.40 - case subst_stacexpr E a v t of
9.41 - (a', STac stac) => (*script-tactic*)
9.42 + case LTool.subst_stacexpr E a v t of
9.43 + (a', LTool.STac stac) => (*script-tactic*)
9.44 let val stac' =
9.45 eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
9.46 in
9.47 (if (! trace_script)
9.48 then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac ^"'")
9.49 else ();
9.50 - (a', STac stac'))
9.51 + (a', LTool.STac stac'))
9.52 end
9.53 - | (a', Expr lexpr) => (*leaf-expression*)
9.54 + | (a', LTool.Expr lexpr) => (*leaf-expression*)
9.55 let val lexpr' =
9.56 eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
9.57 in
9.58 (if (! trace_script)
9.59 then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
9.60 else ();
9.61 - (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
9.62 + (a', LTool.Expr lexpr')) (*lexpr' is the value of the Expr*)
9.63 end;
9.64
9.65 (** locate an applicable stac in a script **)
9.66 @@ -570,7 +570,7 @@
9.67 | NasNap of (* stac not associated, not applicable, nothing generated;
9.68 for distinction in Or, for leaving iterations, leaving Seq,
9.69 evaluate scriptexpressions *)
9.70 - term * env;
9.71 + term * LTool.env;
9.72 fun assoc2str (Assoc _) = "Assoc"
9.73 | assoc2str (NasNap _) = "NasNap"
9.74 | assoc2str (NasApp _) = "NasApp";
9.75 @@ -598,16 +598,16 @@
9.76 NasApp ((E',l,a,v,S,_),ss) =>
9.77 let
9.78 val id' = mk_Free (id, T);
9.79 - val E' = upd_env E' (id', v);
9.80 + val E' = LTool.upd_env E' (id', v);
9.81 in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
9.82 | NasNap (v,E) =>
9.83 let
9.84 val id' = mk_Free (id, T);
9.85 - val E' = upd_env E (id', v);
9.86 + val E' = LTool.upd_env E (id', v);
9.87 in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
9.88 | ay => ay)
9.89 | assy (ya as (thy,_,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
9.90 - if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
9.91 + if eval_true_ thy srls (subst_atomic (LTool.upd_env E (a,v)) c)
9.92 then assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e
9.93 else NasNap (v, E)
9.94 | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
9.95 @@ -655,10 +655,10 @@
9.96 (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
9.97 | assy (thy',ctxt,sr,d,ap) ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss) t =
9.98 (case handle_leaf "locate" thy' sr E a v t of
9.99 - (a', Expr _) =>
9.100 + (a', LTool.Expr _) =>
9.101 (NasNap (eval_listexpr_ (assoc_thy thy') sr
9.102 (subst_atomic (upd_env_opt E (a',v)) t), E))
9.103 - | (a', STac stac) =>
9.104 + | (a', LTool.STac stac) =>
9.105 let
9.106 val p' =
9.107 case p_ of Frm => p
9.108 @@ -700,7 +700,7 @@
9.109 Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
9.110 | t => error ("ass_up..HOL.Let $ _ with " ^ term2str t))
9.111 val i = mk_Free (i, T);
9.112 - val E = upd_env E (i, v);
9.113 + val E = LTool.upd_env E (i, v);
9.114 in case assy (y,ctxt,s,d,Aundef) ((E, l @ [R, D], a,v,S,b),ss) body of
9.115 Assoc iss => Assoc iss
9.116 | NasApp iss => astep_up ys iss
9.117 @@ -731,7 +731,7 @@
9.118 | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
9.119 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
9.120 (t as Const ("Script.While",_) $ c $ e $ a) =
9.121 - if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
9.122 + if eval_true_ y s (subst_atomic (LTool.upd_env E (a,v)) c)
9.123 then case assy (y,ctxt,s,d,Aundef) ((E, l @ [L, R], SOME a,v,S,b),ss) e of
9.124 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
9.125 | NasApp ((E',l,a,v,S,b),ss) =>
9.126 @@ -864,11 +864,11 @@
9.127 Selem.scrstate (* after determination of stac WN.18.8.03 *)
9.128 | Napp of (* stac found was not applicable;
9.129 this mode may become Skip in Repeat, Try and Or *)
9.130 - env (*stack*) (* popped while nxt_up *)
9.131 + LTool.env (* popped while nxt_up *)
9.132 | Skip of (* for restart after Appy, for leaving iterations,
9.133 for passing the value of scriptexpressions,
9.134 and for finishing the script successfully *)
9.135 - term * env (*stack*);
9.136 + term * LTool.env (*a stack*);
9.137
9.138 datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
9.139 (*Appy is only (final) returnvalue, not argument during search *)
9.140 @@ -880,11 +880,11 @@
9.141 fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
9.142 (case appy thy ptp E (l @ [L, R]) e a v of
9.143 Skip (res, E) =>
9.144 - let val E' = upd_env E (Free (i,T), res);
9.145 + let val E' = LTool.upd_env E (Free (i,T), res);
9.146 in appy thy ptp E' (l @ [R, D]) b a v end
9.147 | ay => ay)
9.148 | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
9.149 - (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
9.150 + (if eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)
9.151 then appy thy ptp E (l @ [L, R]) e (SOME a) v
9.152 else Skip (v, E))
9.153 | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
9.154 @@ -925,8 +925,8 @@
9.155 (* a leaf has been found *)
9.156 | appy ((th,sr)) (pt, p) E l t a v =
9.157 case handle_leaf "next " th sr E a v t of
9.158 - (_, Expr s) => Skip (s, E)
9.159 - | (a', STac stac) =>
9.160 + (_, LTool.Expr s) => Skip (s, E)
9.161 + | (a', LTool.STac stac) =>
9.162 let val (m,m') = stac2tac_ pt (assoc_thy th) stac
9.163 in case m of
9.164 Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))
9.165 @@ -947,7 +947,7 @@
9.166 Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
9.167 | t => error ("nxt_up..HOL.Let $ _ with " ^ term2str t))
9.168 val i = mk_Free (i, T)
9.169 - val E = upd_env E (i, v)
9.170 + val E = LTool.upd_env E (i, v)
9.171 in
9.172 case appy thy ptp E (up @ [R,D]) body a v of
9.173 Appy lre => Appy lre
9.174 @@ -1180,8 +1180,8 @@
9.175 {scr = Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
9.176 val (env, a, v) = (case get_istate pt (p, p_) of
9.177 Selem.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
9.178 - in map ((stac2tac pt thy) o rep_stacexpr o #2 o
9.179 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
9.180 + in map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
9.181 + (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
9.182 end;
9.183
9.184 (* fetch tactics from script and filter _applicable_ tactics;
9.185 @@ -1207,8 +1207,8 @@
9.186 val (env, a, v) = (case get_istate pt (p, p_) of
9.187 Selem.ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
9.188 val alltacs = (*we expect at least 1 stac in a script*)
9.189 - map ((stac2tac pt thy) o rep_stacexpr o #2 o
9.190 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
9.191 + map ((stac2tac pt thy) o LTool.rep_stacexpr o #2 o
9.192 + (handle_leaf "selrul" thy' srls env a v)) (LTool.stacpbls sc)
9.193 val f =
9.194 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
9.195 | _ => error "")
10.1 --- a/src/Tools/isac/Interpret/specification-elems.sml Wed Feb 14 10:54:53 2018 +0100
10.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml Wed Feb 14 12:20:35 2018 +0100
10.3 @@ -70,7 +70,7 @@
10.4 | safe2str Helpless = "Helpless";
10.5
10.6 type scrstate = (* state for script interpreter *)
10.7 - env(*stack*) (* used to instantiate tac for checking assod
10.8 + LTool.env(*stack*) (* used to instantiate tac for checking assod
10.9 12.03.noticed: e_ not updated during execution ?!? *)
10.10 * loc_ (* location of tac in script *)
10.11 * term option (* argument of curried functions *)
11.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Feb 14 10:54:53 2018 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Feb 14 12:20:35 2018 +0100
11.3 @@ -46,7 +46,7 @@
11.4 [Calc ("Tools.matches",eval_matches "")];
11.5 *}
11.6 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
11.7 - (Context.theory_name @{theory}, prep_rls @{theory} univariate_equation_prls))] *}
11.8 + (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))] *}
11.9 setup {* KEStore_Elems.add_pbts
11.10 [(Specify.prep_pbt thy "pbl_equ" [] e_pblID
11.11 (["equation"],
12.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 14 10:54:53 2018 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 14 12:20:35 2018 +0100
12.3 @@ -322,7 +322,7 @@
12.4 ],
12.5 scr = EmptyScr};
12.6
12.7 -val prep_rls' = prep_rls @{theory};
12.8 +val prep_rls' = LTool.prep_rls @{theory};
12.9 *}
12.10 setup {* KEStore_Elems.add_rlss
12.11 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)),
13.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Feb 14 10:54:53 2018 +0100
13.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Feb 14 12:20:35 2018 +0100
13.3 @@ -1551,7 +1551,7 @@
13.4 scr = EmptyScr}:rls;
13.5 *}
13.6
13.7 -ML {* val prep_rls' = prep_rls @{theory} *}
13.8 +ML {* val prep_rls' = LTool.prep_rls @{theory} *}
13.9
13.10 setup {* KEStore_Elems.add_rlss
13.11 [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
14.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Feb 14 10:54:53 2018 +0100
14.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Feb 14 12:20:35 2018 +0100
14.3 @@ -440,7 +440,7 @@
14.4 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
14.5 ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")}:rls);
14.6
14.7 -val prep_rls' = prep_rls @{theory};
14.8 +val prep_rls' = LTool.prep_rls @{theory};
14.9 *}
14.10 ML{*
14.11 val complete_square = prep_rls'(
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Feb 14 10:54:53 2018 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Feb 14 12:20:35 2018 +0100
15.3 @@ -256,7 +256,7 @@
15.4 setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
15.5 ML {*
15.6
15.7 -val prep_rls' = prep_rls @{theory};
15.8 +val prep_rls' = LTool.prep_rls @{theory};
15.9
15.10 val expand_rootbinoms = prep_rls'(
15.11 Rls{id = "expand_rootbinoms", preconds = [],
16.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Wed Feb 14 10:54:53 2018 +0100
16.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Wed Feb 14 12:20:35 2018 +0100
16.3 @@ -25,7 +25,7 @@
16.4 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_")
16.5 ];
16.6
16.7 -val prep_rls' = prep_rls @{theory};
16.8 +val prep_rls' = LTool.prep_rls @{theory};
16.9 *}
16.10 setup {* KEStore_Elems.add_rlss
16.11 [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)),
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Feb 14 10:54:53 2018 +0100
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Feb 14 12:20:35 2018 +0100
17.3 @@ -494,7 +494,7 @@
17.4 eval_contains_root"#contains_root_"))
17.5 ];
17.6 *}
17.7 -ML {* val prep_rls' = prep_rls @{theory}; *}
17.8 +ML {* val prep_rls' = LTool.prep_rls @{theory}; *}
17.9 setup {* KEStore_Elems.add_rlss
17.10 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
17.11 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
18.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Feb 14 10:54:53 2018 +0100
18.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Feb 14 12:20:35 2018 +0100
18.3 @@ -23,7 +23,7 @@
18.4 rules = [Thm ("sym_thm111", @{thm thm111} RS @{thm sym}), Thm ("o_def", @{thm o_def})],
18.5 scr = EmptyScr};
18.6
18.7 -val prep_rls' = prep_rls @{theory};
18.8 +val prep_rls' = LTool.prep_rls @{theory};
18.9 *}
18.10
18.11 setup {* KEStore_Elems.add_rlss
19.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy Wed Feb 14 10:54:53 2018 +0100
19.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Wed Feb 14 12:20:35 2018 +0100
19.3 @@ -10,6 +10,6 @@
19.4
19.5 ML {*
19.6 *} ML {*
19.7 -eval_true
19.8 +
19.9 *}
19.10 end
19.11 \ No newline at end of file
20.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Wed Feb 14 10:54:53 2018 +0100
20.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Wed Feb 14 12:20:35 2018 +0100
20.3 @@ -2,6 +2,62 @@
20.4 (c) Walther Neuper 2000
20.5 *)
20.6
20.7 +signature LANGUAGE_TOOLS =
20.8 + sig
20.9 +(*.*) datatype stacexpr = Expr of term | STac of term
20.10 +(*.*) val contain_bdv: rule list -> bool
20.11 +(*.*) val contains_bdv: thm -> bool
20.12 +(*.*) type env = (term * term) list
20.13 +(*.*) val is_booll_dsc: term -> bool
20.14 +(*.*) val is_calc: term -> bool
20.15 +(*.*) val is_dsc: term -> bool
20.16 +(*.*) val is_list_dsc: term -> bool
20.17 +(*.*) val is_reall_dsc: term -> bool
20.18 +(*.*) val is_unl: term -> bool
20.19 +(*.*) val one_scr_arg: term -> term
20.20 +(*.*) val op_of_calc: term -> string
20.21 +(*.*) val pblterm: domID -> pblID -> term
20.22 +(*.*) val prep_rls: theory -> rls -> rls
20.23 +(*.*) val rep_stacexpr: stacexpr -> term
20.24 +(*.*) val stacpbls: term -> term list
20.25 +(*.*) val subpbl: string -> string list -> term
20.26 +(*.*) val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * stacexpr
20.27 +(*.*) val two_scr_arg: term -> term * term
20.28 +(*.*) val upd_env: env -> term * term -> env
20.29 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
20.30 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20.31 +(**) val Bdv: term
20.32 +(**) val Ca1: term
20.33 +(**) val Cal: term
20.34 +(**) val ID_type: typ
20.35 +(**) val IDtype: typ
20.36 +(**) val Repeat: term
20.37 +(**) val Rew: term
20.38 +(**) val Rew_Inst: term
20.39 +(**) val Rew_Set: term
20.40 +(**) val Rew_Set_Inst: term
20.41 +(**) val SEq: term
20.42 +(**) val ScrStep: term
20.43 +(**) val ScrStep_inst: term
20.44 +(**) val Subs: term
20.45 +(**) val Term: term
20.46 +(**) val Try: term
20.47 +(**) val domID: string
20.48 +(**) val pair_t: term
20.49 +(**) val pblID: term
20.50 +(**) val pbl_t: term
20.51 +(**) val rule2stac: theory -> rule -> term
20.52 +(**) val rule2stac_inst: theory -> rule -> term
20.53 +(**) val rules2scr_Rls: theory -> rule list -> term
20.54 +(**) val rules2scr_Seq: theory -> rule list -> term
20.55 +(**) val subpbl_t: term
20.56 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.57 + end
20.58 +
20.59 +(**)
20.60 +structure LTool(**): LANGUAGE_TOOLS(**) =
20.61 +struct
20.62 +(**)
20.63
20.64 fun is_reall_dsc
20.65 (Const(_,Type("fun",[Type("List.list",
20.66 @@ -322,6 +378,7 @@
20.67 ((inst_abs @{theory}) o Thm.term_of o (the:cterm option -> cterm) o
20.68 (parse @{theory})) "(_t::'z) = _t";
20.69 *)
20.70 +(*--------------------- NOT IN struct --------------------------------------------------------
20.71 ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory})) "(t::'z) = t";
20.72 ((inst_abs @{theory}) o Thm.term_of o (the:cterm option -> cterm) o
20.73 (parse @{theory})) "(t't::'z) = t't";
20.74 @@ -334,6 +391,7 @@
20.75 \ (Try (Repeat (Rewrite add_commute False))) @@ \
20.76 \ (Try (Repeat (Rewrite mult_commute False)))) \
20.77 \ t_t)";
20.78 + --------------------- NOT IN struct --------------------------------------------------------*)
20.79 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
20.80 ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))
20.81 "Script Stepwise (t_t::'z) =\
20.82 @@ -486,3 +544,5 @@
20.83 scr = Prog sc} end
20.84 | prep_rls _ (Rrls {id,...}) =
20.85 error ("prep_rls' not required for Rrls \"" ^ id ^ "\"");
20.86 +
20.87 +end
20.88 \ No newline at end of file