6 signature SOLVE_PHASE = |
6 signature SOLVE_PHASE = |
7 sig |
7 sig |
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl |
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl |
9 | CompleteToSubpbl | Steps of int |
9 | CompleteToSubpbl | Steps of int |
10 val autoord : auto -> int |
10 val autoord : auto -> int |
11 type tac'_ |
|
12 val mk_tac'_ : Tactic.input -> string * Tactic.input |
|
13 val specsteps : string list |
11 val specsteps : string list |
14 |
12 |
15 val all_solve : auto -> Ctree.pos' list -> Ctree.state -> |
13 val all_solve : auto -> Ctree.pos' list -> Ctree.state -> |
16 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_)) |
14 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_)) |
17 val complete_solve : |
15 val complete_solve : |
18 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state |
16 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state |
19 val inform : Chead.calcstate' -> string -> string * Chead.calcstate' |
17 val inform : Chead.calcstate' -> string -> string * Chead.calcstate' |
20 |
18 |
21 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' |
19 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' |
22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
23 val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout |
21 (*NONE*) |
24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
25 (*NONE*) |
23 (*NONE*) |
26 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
27 |
25 |
28 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
26 (*----- unused code, kept as hints to design ideas ---------------------------------------------*) |
33 structure Solve(**): SOLVE_PHASE(**) = |
31 structure Solve(**): SOLVE_PHASE(**) = |
34 struct |
32 struct |
35 (**) |
33 (**) |
36 open Ctree; |
34 open Ctree; |
37 open Pos |
35 open Pos |
38 |
|
39 type mstID = string; |
|
40 type tac'_ = mstID * Tactic.input; (*DG <-> ME*) |
|
41 |
|
42 fun mk_tac'_ m = case m of (* scr not cleaned -- will disappear eventually *) |
|
43 Tactic.Init_Proof (ppc, spec) => ("Init_Proof", Tactic.Init_Proof (ppc, spec )) |
|
44 | Tactic.Model_Problem => ("Model_Problem", Tactic.Model_Problem) |
|
45 | Tactic.Refine_Tacitly pblID => ("Refine_Tacitly", Tactic.Refine_Tacitly pblID) |
|
46 | Tactic.Refine_Problem pblID => ("Refine_Problem", Tactic.Refine_Problem pblID) |
|
47 | Tactic.Add_Given cterm' => ("Add_Given", Tactic.Add_Given cterm') |
|
48 | Tactic.Del_Given cterm' => ("Del_Given", Tactic.Del_Given cterm') |
|
49 | Tactic.Add_Find cterm' => ("Add_Find", Tactic.Add_Find cterm') |
|
50 | Tactic.Del_Find cterm' => ("Del_Find", Tactic.Del_Find cterm') |
|
51 | Tactic.Add_Relation cterm' => ("Add_Relation", Tactic.Add_Relation cterm') |
|
52 | Tactic.Del_Relation cterm' => ("Del_Relation", Tactic.Del_Relation cterm') |
|
53 |
|
54 | Tactic.Specify_Theory domID => ("Specify_Theory", Tactic.Specify_Theory domID) |
|
55 | Tactic.Specify_Problem pblID => ("Specify_Problem", Tactic.Specify_Problem pblID) |
|
56 | Tactic.Specify_Method metID => ("Specify_Method", Tactic.Specify_Method metID) |
|
57 | Tactic.Apply_Method metID => ("Apply_Method", Tactic.Apply_Method metID) |
|
58 | Tactic.Check_Postcond pblID => ("Check_Postcond", Tactic.Check_Postcond pblID) |
|
59 | Tactic.Free_Solve => ("Free_Solve", Tactic.Free_Solve) |
|
60 |
|
61 | Tactic.Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Tactic.Rewrite_Inst (subs, thm')) |
|
62 | Tactic.Rewrite thm' => ("Rewrite", Tactic.Rewrite thm') |
|
63 | Tactic.Rewrite_Asm thm' => ("Rewrite_Asm", Tactic.Rewrite_Asm thm') |
|
64 | Tactic.Rewrite_Set_Inst (subs, rls') |
|
65 => ("Rewrite_Set_Inst", Tactic.Rewrite_Set_Inst (subs, rls')) |
|
66 | Tactic.Rewrite_Set rls' => ("Rewrite_Set", Tactic.Rewrite_Set rls') |
|
67 | Tactic.End_Ruleset => ("End_Ruleset", Tactic.End_Ruleset) |
|
68 |
|
69 | Tactic.End_Detail => ("End_Detail", Tactic.End_Detail) |
|
70 | Tactic.Detail_Set rls' => ("Detail_Set", Tactic.Detail_Set rls') |
|
71 | Tactic.Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Tactic.Detail_Set_Inst (s, rls')) |
|
72 |
|
73 | Tactic.Calculate op_ => ("Calculate", Tactic.Calculate op_) |
|
74 | Tactic.Substitute sube => ("Substitute", Tactic.Substitute sube) |
|
75 | Tactic.Apply_Assumption cts' => ("Apply_Assumption", Tactic.Apply_Assumption cts') |
|
76 |
|
77 | Tactic.Take cterm' => ("Take", Tactic.Take cterm') |
|
78 | Tactic.Take_Inst cterm' => ("Take_Inst", Tactic.Take_Inst cterm') |
|
79 | Tactic.Subproblem (domID, pblID) => ("Subproblem", Tactic.Subproblem (domID, pblID)) |
|
80 (* |
|
81 | Tactic.Subproblem_Full(spec,cts')=> ("Subproblem_Full", Tactic.Subproblem_Full(spec,cts')) |
|
82 *) |
|
83 | Tactic.End_Subproblem => ("End_Subproblem", Tactic.End_Subproblem) |
|
84 | Tactic.CAScmd cterm' => ("CAScmd", Tactic.CAScmd cterm') |
|
85 |
|
86 | Tactic.Split_And => ("Split_And", Tactic.Split_And) |
|
87 | Tactic.Conclude_And => ("Conclude_And", Tactic.Conclude_And) |
|
88 | Tactic.Split_Or => ("Split_Or", Tactic.Split_Or) |
|
89 | Tactic.Conclude_Or => ("Conclude_Or", Tactic.Conclude_Or) |
|
90 | Tactic.Begin_Trans => ("Begin_Trans", Tactic.Begin_Trans) |
|
91 | Tactic.End_Trans => ("End_Trans", Tactic.End_Trans) |
|
92 | Tactic.Begin_Sequ => ("Begin_Sequ", Tactic.Begin_Sequ) |
|
93 | Tactic.End_Sequ => ("End_Sequ", Tactic.Begin_Sequ) |
|
94 | Tactic.Split_Intersect => ("Split_Intersect", Tactic.Split_Intersect) |
|
95 | Tactic.End_Intersect => ("End_Intersect", Tactic.End_Intersect) |
|
96 | Tactic.Check_elementwise cterm' => ("Check_elementwise", Tactic.Check_elementwise cterm') |
|
97 | Tactic.Or_to_List => ("Or_to_List", Tactic.Or_to_List) |
|
98 | Tactic.Collect_Trues => ("Collect_Results", Tactic.Collect_Trues) |
|
99 |
|
100 | Tactic.Empty_Tac => ("Empty_Tac", Tactic.Empty_Tac) |
|
101 | Tactic.Tac string => ("Tac", Tactic.Tac string) |
|
102 | Tactic.End_Proof' => ("End_Proof'", Tactic.End_Proof') |
|
103 | _ => error "mk_tac'_: uncovered case"; |
|
104 |
36 |
105 type squ = ctree; (* TODO: safe etc. *) |
37 type squ = ctree; (* TODO: safe etc. *) |
106 |
38 |
107 val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem", |
39 val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem", |
108 "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation", |
40 "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation", |
201 val newnds = children (get_nd pt'' p) |
133 val newnds = children (get_nd pt'' p) |
202 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*) |
134 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*) |
203 in ("detailrls", pt''', (p @ [length newnds], Res)) end |
135 in ("detailrls", pt''', (p @ [length newnds], Res)) end |
204 end; |
136 end; |
205 |
137 |
206 fun get_form (mI, m) (p,p_) pt = |
|
207 case Applicable.applicable_in (p, p_) pt m of |
|
208 Applicable.Notappl e => Generate.Error' e |
|
209 | Applicable.Appl m => |
|
210 if Tactic.for_specify' m |
|
211 then |
|
212 let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt |
|
213 in f end |
|
214 else Generate.EmptyMout; |
|
215 |
|
216 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = |
138 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = |
217 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of |
139 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of |
218 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*)) |
140 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*)) |
219 | SOME f_in => |
141 | SOME f_in => |
220 let |
142 let |