1.1 --- a/src/Tools/isac/MathEngine/solve.sml Thu Dec 19 17:41:51 2019 +0100
1.2 +++ b/src/Tools/isac/MathEngine/solve.sml Fri Dec 20 09:41:11 2019 +0100
1.3 @@ -8,8 +8,6 @@
1.4 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl
1.5 | CompleteToSubpbl | Steps of int
1.6 val autoord : auto -> int
1.7 - type tac'_
1.8 - val mk_tac'_ : Tactic.input -> string * Tactic.input
1.9 val specsteps : string list
1.10
1.11 val all_solve : auto -> Ctree.pos' list -> Ctree.state ->
1.12 @@ -20,7 +18,7 @@
1.13
1.14 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
1.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.16 - val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
1.17 + (*NONE*)
1.18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.19 (*NONE*)
1.20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.21 @@ -36,72 +34,6 @@
1.22 open Ctree;
1.23 open Pos
1.24
1.25 -type mstID = string;
1.26 -type tac'_ = mstID * Tactic.input; (*DG <-> ME*)
1.27 -
1.28 -fun mk_tac'_ m = case m of (* scr not cleaned -- will disappear eventually *)
1.29 - Tactic.Init_Proof (ppc, spec) => ("Init_Proof", Tactic.Init_Proof (ppc, spec ))
1.30 -| Tactic.Model_Problem => ("Model_Problem", Tactic.Model_Problem)
1.31 -| Tactic.Refine_Tacitly pblID => ("Refine_Tacitly", Tactic.Refine_Tacitly pblID)
1.32 -| Tactic.Refine_Problem pblID => ("Refine_Problem", Tactic.Refine_Problem pblID)
1.33 -| Tactic.Add_Given cterm' => ("Add_Given", Tactic.Add_Given cterm')
1.34 -| Tactic.Del_Given cterm' => ("Del_Given", Tactic.Del_Given cterm')
1.35 -| Tactic.Add_Find cterm' => ("Add_Find", Tactic.Add_Find cterm')
1.36 -| Tactic.Del_Find cterm' => ("Del_Find", Tactic.Del_Find cterm')
1.37 -| Tactic.Add_Relation cterm' => ("Add_Relation", Tactic.Add_Relation cterm')
1.38 -| Tactic.Del_Relation cterm' => ("Del_Relation", Tactic.Del_Relation cterm')
1.39 -
1.40 -| Tactic.Specify_Theory domID => ("Specify_Theory", Tactic.Specify_Theory domID)
1.41 -| Tactic.Specify_Problem pblID => ("Specify_Problem", Tactic.Specify_Problem pblID)
1.42 -| Tactic.Specify_Method metID => ("Specify_Method", Tactic.Specify_Method metID)
1.43 -| Tactic.Apply_Method metID => ("Apply_Method", Tactic.Apply_Method metID)
1.44 -| Tactic.Check_Postcond pblID => ("Check_Postcond", Tactic.Check_Postcond pblID)
1.45 -| Tactic.Free_Solve => ("Free_Solve", Tactic.Free_Solve)
1.46 -
1.47 -| Tactic.Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Tactic.Rewrite_Inst (subs, thm'))
1.48 -| Tactic.Rewrite thm' => ("Rewrite", Tactic.Rewrite thm')
1.49 -| Tactic.Rewrite_Asm thm' => ("Rewrite_Asm", Tactic.Rewrite_Asm thm')
1.50 -| Tactic.Rewrite_Set_Inst (subs, rls')
1.51 - => ("Rewrite_Set_Inst", Tactic.Rewrite_Set_Inst (subs, rls'))
1.52 -| Tactic.Rewrite_Set rls' => ("Rewrite_Set", Tactic.Rewrite_Set rls')
1.53 -| Tactic.End_Ruleset => ("End_Ruleset", Tactic.End_Ruleset)
1.54 -
1.55 -| Tactic.End_Detail => ("End_Detail", Tactic.End_Detail)
1.56 -| Tactic.Detail_Set rls' => ("Detail_Set", Tactic.Detail_Set rls')
1.57 -| Tactic.Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Tactic.Detail_Set_Inst (s, rls'))
1.58 -
1.59 -| Tactic.Calculate op_ => ("Calculate", Tactic.Calculate op_)
1.60 -| Tactic.Substitute sube => ("Substitute", Tactic.Substitute sube)
1.61 -| Tactic.Apply_Assumption cts' => ("Apply_Assumption", Tactic.Apply_Assumption cts')
1.62 -
1.63 -| Tactic.Take cterm' => ("Take", Tactic.Take cterm')
1.64 -| Tactic.Take_Inst cterm' => ("Take_Inst", Tactic.Take_Inst cterm')
1.65 -| Tactic.Subproblem (domID, pblID) => ("Subproblem", Tactic.Subproblem (domID, pblID))
1.66 -(*
1.67 -| Tactic.Subproblem_Full(spec,cts')=> ("Subproblem_Full", Tactic.Subproblem_Full(spec,cts'))
1.68 -*)
1.69 -| Tactic.End_Subproblem => ("End_Subproblem", Tactic.End_Subproblem)
1.70 -| Tactic.CAScmd cterm' => ("CAScmd", Tactic.CAScmd cterm')
1.71 -
1.72 -| Tactic.Split_And => ("Split_And", Tactic.Split_And)
1.73 -| Tactic.Conclude_And => ("Conclude_And", Tactic.Conclude_And)
1.74 -| Tactic.Split_Or => ("Split_Or", Tactic.Split_Or)
1.75 -| Tactic.Conclude_Or => ("Conclude_Or", Tactic.Conclude_Or)
1.76 -| Tactic.Begin_Trans => ("Begin_Trans", Tactic.Begin_Trans)
1.77 -| Tactic.End_Trans => ("End_Trans", Tactic.End_Trans)
1.78 -| Tactic.Begin_Sequ => ("Begin_Sequ", Tactic.Begin_Sequ)
1.79 -| Tactic.End_Sequ => ("End_Sequ", Tactic.Begin_Sequ)
1.80 -| Tactic.Split_Intersect => ("Split_Intersect", Tactic.Split_Intersect)
1.81 -| Tactic.End_Intersect => ("End_Intersect", Tactic.End_Intersect)
1.82 -| Tactic.Check_elementwise cterm' => ("Check_elementwise", Tactic.Check_elementwise cterm')
1.83 -| Tactic.Or_to_List => ("Or_to_List", Tactic.Or_to_List)
1.84 -| Tactic.Collect_Trues => ("Collect_Results", Tactic.Collect_Trues)
1.85 -
1.86 -| Tactic.Empty_Tac => ("Empty_Tac", Tactic.Empty_Tac)
1.87 -| Tactic.Tac string => ("Tac", Tactic.Tac string)
1.88 -| Tactic.End_Proof' => ("End_Proof'", Tactic.End_Proof')
1.89 -| _ => error "mk_tac'_: uncovered case";
1.90 -
1.91 type squ = ctree; (* TODO: safe etc. *)
1.92
1.93 val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem",
1.94 @@ -203,16 +135,6 @@
1.95 in ("detailrls", pt''', (p @ [length newnds], Res)) end
1.96 end;
1.97
1.98 -fun get_form (mI, m) (p,p_) pt =
1.99 - case Applicable.applicable_in (p, p_) pt m of
1.100 - Applicable.Notappl e => Generate.Error' e
1.101 - | Applicable.Appl m =>
1.102 - if Tactic.for_specify' m
1.103 - then
1.104 - let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt
1.105 - in f end
1.106 - else Generate.EmptyMout;
1.107 -
1.108 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
1.109 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
1.110 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
2.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 19 17:41:51 2019 +0100
2.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Dec 20 09:41:11 2019 +0100
2.3 @@ -190,7 +190,6 @@
2.4 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
2.5
2.6 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
2.7 - val (mI, m) = Solve.mk_tac'_ tac;
2.8 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
2.9 (*if*) member op = Solve.specsteps mI; (*else*)
2.10
3.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 19 17:41:51 2019 +0100
3.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Dec 20 09:41:11 2019 +0100
3.3 @@ -36,7 +36,6 @@
3.4
3.5 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
3.6 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
3.7 -val (mI,m) = mk_tac'_ tac;
3.8 val Appl m = applicable_in p pt m;
3.9 member op = specsteps mI (*false*);
3.10 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
3.11 @@ -109,7 +108,6 @@
3.12
3.13 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
3.14 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
3.15 - val (mI, m) = Solve.mk_tac'_ tac;
3.16 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
3.17 (*if*) member op = Solve.specsteps mI; (*else*)
3.18
3.19 @@ -273,7 +271,6 @@
3.20 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
3.21 (** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
3.22 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
3.23 - val (mI, m) = Solve.mk_tac'_ tac;
3.24 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
3.25 (*if*) member op = Solve.specsteps mI (*else*);
3.26
4.1 --- a/test/Tools/isac/Interpret/script.sml Thu Dec 19 17:41:51 2019 +0100
4.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Dec 20 09:41:11 2019 +0100
4.3 @@ -59,7 +59,6 @@
4.4
4.5 (*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
4.6 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
4.7 -val (mI,m) = mk_tac'_ tac;
4.8 applicable_in p pt m ; (*Appl*)
4.9 member op = specsteps mI; (*false*)
4.10 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
4.11 @@ -108,7 +107,6 @@
4.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.13 "~~~~~ fun me, args:"; val tac = nxt;
4.14 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
4.15 -val (mI,m) = mk_tac'_ tac;
4.16 val Appl m = applicable_in p pt m;
4.17 member op = specsteps mI; (*false*)
4.18 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
5.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Thu Dec 19 17:41:51 2019 +0100
5.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Fri Dec 20 09:41:11 2019 +0100
5.3 @@ -143,7 +143,6 @@
5.4 AbleitungBiegelinie
5.5 *)
5.6 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.7 - val (mI, m) = Solve.mk_tac'_ tac;
5.8 val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
5.9 (*if*) member op = Solve.specsteps mI = false; (*else*)
5.10
5.11 @@ -225,7 +224,6 @@
5.12 ("ok", (_, _, ptp)) => ptp
5.13 ;
5.14 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.15 - val (mI, m) = Solve.mk_tac'_ tac;
5.16 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
5.17 (*if*) member op = Solve.specsteps mI = true; (*then*)
5.18
6.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Dec 19 17:41:51 2019 +0100
6.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Fri Dec 20 09:41:11 2019 +0100
6.3 @@ -184,7 +184,6 @@
6.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
6.5 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
6.6 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.7 -val (mI,m) = mk_tac'_ tac;
6.8 val Appl m = applicable_in p pt m;
6.9 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
6.10 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
7.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Dec 19 17:41:51 2019 +0100
7.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Fri Dec 20 09:41:11 2019 +0100
7.3 @@ -47,7 +47,6 @@
7.4 "~~~~~ fun me, args:"; val tac = nxt;
7.5 val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);
7.6 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
7.7 -val (mI,m) = mk_tac'_ tac; (*mI = "Apply_Method"*)
7.8 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*)
7.9 member op = specsteps mI; (*false*)
7.10 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
8.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 19 17:41:51 2019 +0100
8.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Dec 20 09:41:11 2019 +0100
8.3 @@ -35,7 +35,6 @@
8.4 (*ERROR WAS: scan_dn1: call by ([3], Pbl)*)
8.5 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
8.6 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
8.7 - val (mI, m) = Solve.mk_tac'_ tac;
8.8 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
8.9 member op = Solve.specsteps mI (* = false*);
8.10
9.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 19 17:41:51 2019 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Fri Dec 20 09:41:11 2019 +0100
9.3 @@ -26,7 +26,6 @@
9.4 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
9.5
9.6 "~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
9.7 -val (mI,m) = mk_tac'_ tac;
9.8 val Appl m = applicable_in p pt m;
9.9 member op = specsteps mI; (*false*)
9.10 (*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
10.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 19 17:41:51 2019 +0100
10.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Fri Dec 20 09:41:11 2019 +0100
10.3 @@ -40,7 +40,6 @@
10.4
10.5 locatetac tac (pt, p) (*of*);
10.6 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
10.7 - val (mI,m) = mk_tac'_ tac;
10.8 val Appl m = (*case*) applicable_in p pt m (*of*);
10.9 member op = specsteps mI; (*else*)
10.10
11.1 --- a/test/Tools/isac/Test_Some.thy Thu Dec 19 17:41:51 2019 +0100
11.2 +++ b/test/Tools/isac/Test_Some.thy Fri Dec 20 09:41:11 2019 +0100
11.3 @@ -210,8 +210,6 @@
11.4 \<close> ML \<open>
11.5 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
11.6 \<close> ML \<open>
11.7 - val (mI, m) = Solve.mk_tac'_ tac;
11.8 -\<close> ML \<open>
11.9 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
11.10 \<close> ML \<open>
11.11 (*if*) member op = Solve.specsteps mI (*else*);