1.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Dec 19 10:37:44 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Dec 21 08:57:47 2016 +0100
1.3 @@ -337,7 +337,7 @@
1.4 | ("end-of-calculation", _) => message2xml cI "end-of-calculation"
1.5 | ("failure", _) => sysERROR2xml cI "failure"
1.6 | ("not-applicable", _) => (*the rule comes from anywhere..*)
1.7 - (case applicable_in ip pt tac of
1.8 + (case Applicable.applicable_in ip pt tac of
1.9 Chead.Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
1.10 | Chead.Appl m =>
1.11 let
2.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 19 10:37:44 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Wed Dec 21 08:57:47 2016 +0100
2.3 @@ -4,6 +4,11 @@
2.4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.5 10 20 30 40 50 60 70 80
2.6 *)
2.7 +
2.8 +structure Applicable = (* intermediately to avoid too many "Ctree." *)
2.9 +struct
2.10 +(*open Ctree*)
2.11 +
2.12 val e_cterm' = empty_cterm';
2.13
2.14
2.15 @@ -716,3 +721,4 @@
2.16 | Chead.Notappl _ => error ("tac2mstp': fails with"^
2.17 (tac2str m));
2.18
2.19 +end
2.20 \ No newline at end of file
3.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Dec 19 10:37:44 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Dec 21 08:57:47 2016 +0100
3.3 @@ -544,7 +544,7 @@
3.4 val p' = lev_on p;
3.5 val tac = get_obj g_tac pt p';
3.6 in
3.7 - case applicable_in pos pt tac of
3.8 + case Applicable.applicable_in pos pt tac of
3.9 Chead.Notappl msg => (msg, Tac "")
3.10 | Chead.Appl rew =>
3.11 let
4.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Dec 19 10:37:44 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 08:57:47 2016 +0100
4.3 @@ -84,7 +84,7 @@
4.4 let
4.5 val (mI, m) = mk_tac'_ tac;
4.6 in
4.7 - case applicable_in p pt m of
4.8 + case Applicable.applicable_in p pt m of
4.9 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
4.10 | Chead.Appl m =>
4.11 let
5.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Dec 19 10:37:44 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Dec 21 08:57:47 2016 +0100
5.3 @@ -363,7 +363,7 @@
5.4 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite thm'') =
5.5 let val thm_deriv = deriv_of_thm'' thm''
5.6 in
5.7 - (case applicable_in pos pt tac of
5.8 + (case Applicable.applicable_in pos pt tac of
5.9 Chead.Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
5.10 ContThm
5.11 {thyID = theory'2thyID thy',
5.12 @@ -390,7 +390,7 @@
5.13 | context_thy (pt, pos as (p, p_)) (tac as Rewrite_Inst (subs, (thmID, _))) =
5.14 let val thm = Global_Theory.get_thm (Isac ()) thmID
5.15 in
5.16 - (case applicable_in pos pt tac of
5.17 + (case Applicable.applicable_in pos pt tac of
5.18 Chead.Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
5.19 let
5.20 val thm_deriv = Thm.get_name_hint thm
5.21 @@ -424,7 +424,7 @@
5.22 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
5.23 end
5.24 | context_thy (pt, p) (tac as Rewrite_Set rls') =
5.25 - (case applicable_in p pt tac of
5.26 + (case Applicable.applicable_in p pt tac of
5.27 Chead.Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
5.28 ContRls
5.29 {thyID = theory'2thyID thy',
5.30 @@ -432,7 +432,7 @@
5.31 applto = f, result = res, asms = asm}
5.32 | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
5.33 | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) =
5.34 - (case applicable_in p pt tac of
5.35 + (case Applicable.applicable_in p pt tac of
5.36 Chead.Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
5.37 ContRlsInst
5.38 {thyID = theory'2thyID thy',
6.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 19 10:37:44 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Dec 21 08:57:47 2016 +0100
6.3 @@ -675,7 +675,7 @@
6.4 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
6.5 AssOnly => (NasNap (v, E))
6.6 | _ =>
6.7 - (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
6.8 + (case Applicable.applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
6.9 Chead.Appl m' =>
6.10 let
6.11 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
6.12 @@ -928,7 +928,7 @@
6.13 in case m of
6.14 Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
6.15 | _ =>
6.16 - (case applicable_in p pt m of
6.17 + (case Applicable.applicable_in p pt m of
6.18 Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
6.19 | _ => Napp E)
6.20 end
7.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 19 10:37:44 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed Dec 21 08:57:47 2016 +0100
7.3 @@ -468,7 +468,7 @@
7.4 get_form ((mI,m):tac'_) ((p,p_):pos') ppp;
7.5 *)
7.6 fun get_form ((mI,m):tac'_) ((p,p_):pos') pt =
7.7 - case applicable_in (p,p_) pt m of
7.8 + case Applicable.applicable_in (p,p_) pt m of
7.9 Chead.Notappl e => Generate.Error' e
7.10 | Chead.Appl m =>
7.11 (* val Appl m=applicable_in (p,p_) pt m;
8.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 19 10:37:44 2016 +0100
8.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Dec 21 08:57:47 2016 +0100
8.3 @@ -75,8 +75,10 @@
8.4 open Inform; cas_input;
8.5 open Rtools; trtas2str;
8.6 open Chead; pt_extract;
8.7 - open Ctree; (*//*)
8.8 + open Generate; (*NONE*)
8.9 +(*open Ctree; (*? ?*) *)
8.10 open Specify; show_ptyps;
8.11 + open Applicable (*TODO*)
8.12 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.13 *}
8.14 ML {*
9.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 19 10:37:44 2016 +0100
9.2 +++ b/test/Tools/isac/Test_Some.thy Wed Dec 21 08:57:47 2016 +0100
9.3 @@ -11,6 +11,7 @@
9.4 open Chead; pt_extract;
9.5 open Ctree; (*//*)
9.6 open Specify; show_ptyps;
9.7 + open Applicable. (*TODO*)
9.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.9 *}
9.10 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"