wneuper/isa: comparison src/Tools/isac/MathEngBasic/tactic.sml

equal deleted inserted replaced

-:e7910a62eaf2
+:5037ca1b112b
 signature TACTIC =
 sig
 datatype T =
 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
 | Add_Relation' of TermC.as_string * Model.itm list
-| Apply_Method' of Spec.metID * term option * Istate_Def.T * Proof.context
+| Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
 | Begin_Sequ' | Begin_Trans' of term
 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
 | End_Sequ' | End_Trans' of Selem.result
 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
 | CAScmd' of term
 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
-| Check_Postcond' of Spec.pblID * term
+| Check_Postcond' of Problem.id * term
 | Check_elementwise' of term * TermC.as_string * Selem.result
 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
 | Derive' of Rule_Set.T
 | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
 | End_Detail' of Selem.result
 | Empty_Tac_
 | Free_Solve'
-| Init_Proof' of TermC.as_string list * Spec.spec
+| Init_Proof' of TermC.as_string list * Spec.T
-| Model_Problem' of Spec.pblID * Model.itm list * Model.itm list
+| Model_Problem' of Problem.id * Model.itm list * Model.itm list
 | Or_to_List' of term * term
-| Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
+| Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
-| Refine_Tacitly' of Spec.pblID * Spec.pblID * ThyC.id * Spec.metID * Model.itm list
+| Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
-| Specify_Method' of Spec.metID * Model.ori list * Model.itm list
+| Specify_Method' of Method.id * Model.ori list * Model.itm list
-| Specify_Problem' of Spec.pblID * (bool * (Model.itm list * (bool * term) list))
+| Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
 | Specify_Theory' of ThyC.id
 | Subproblem' of
-Spec.spec * Model.ori list *
+Spec.T * Model.ori list *
 term *          (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
 Selem.fmz_ *    (* either input to root-probl.  or derived from prog. in ???  *)
 (*Istate.T *       ?       *)
 Proof.context * (* derived from prog. in ???  *)
 term            (* ?UNUSED, e.g."Subproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test'')" *)
 val string_of: T -> string
 datatype input =
 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
 | Apply_Assumption of TermC.as_string list
-| Apply_Method of Spec.metID
+| Apply_Method of Method.id
 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
 | Begin_Sequ | Begin_Trans
 | Split_And | Split_Or | Split_Intersect
 | Conclude_And | Conclude_Or | Collect_Trues
 | End_Sequ | End_Trans
 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
 | CAScmd of TermC.as_string
 | Calculate of string
-| Check_Postcond of Spec.pblID
+| Check_Postcond of Problem.id
 | Check_elementwise of TermC.as_string
 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
 | Derive of Rule_Set.id
 | Detail_Set of Rule_Set.id
 | End_Detail
 | Empty_Tac
 | Free_Solve
-| Init_Proof of TermC.as_string list * Spec.spec
+| Init_Proof of TermC.as_string list * Spec.T
 | Model_Problem
 | Or_to_List
-| Refine_Problem of Spec.pblID
+| Refine_Problem of Problem.id
-| Refine_Tacitly of Spec.pblID
+| Refine_Tacitly of Problem.id
 | Rewrite of ThmC.T
 | Rewrite_Inst of Selem.subs * ThmC.T
 | Rewrite_Set of Rule_Set.id
 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
-| Specify_Method of Spec.metID
+| Specify_Method of Method.id
-| Specify_Problem of Spec.pblID
+| Specify_Problem of Problem.id
 | Specify_Theory of ThyC.id
-| Subproblem of ThyC.id * Spec.pblID
+| Subproblem of ThyC.id * Problem.id
 | Substitute of Selem.sube
 | Tac of string
 | Take of TermC.as_string | Take_Inst of TermC.as_string
 val input_to_string : input -> string
 see 'type tac_' for the internal representation of tactics
 *)
 datatype input =
 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
 | Apply_Assumption of TermC.as_string list
-| Apply_Method of Spec.metID
+| Apply_Method of Method.id
 (* creates an "istate" in PblObj.env; in case of "implicit_take"
 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
 a "SOME istate" at fst of "loc".
 As each step (in the solve-phase) has a resulting formula (at the front-end)
 Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
 | End_Sequ | End_Trans
 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
 | CAScmd of TermC.as_string
 | Calculate of string
-| Check_Postcond of Spec.pblID
+| Check_Postcond of Problem.id
 | Check_elementwise of TermC.as_string
 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
 | Derive of Rule_Set.id                 (* WN0509 drop *)
 | Detail_Set of Rule_Set.id             (* WN0509 drop *)
 | End_Detail                     (* WN0509 drop *)
 | Empty_Tac
 | Free_Solve
-| Init_Proof of TermC.as_string list * Spec.spec
+| Init_Proof of TermC.as_string list * Spec.T
 | Model_Problem
 | Or_to_List
-| Refine_Problem of Spec.pblID
+| Refine_Problem of Problem.id
-| Refine_Tacitly of Spec.pblID
+| Refine_Tacitly of Problem.id
 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
 because there all the thms are present with both (thmID, thm)
 (where user-views can show both or only one of (thmID, thm)),
 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
 | Rewrite of ThmC.T
 | Rewrite_Inst of Selem.subs * ThmC.T
 | Rewrite_Set of Rule_Set.id
 | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
-| Specify_Method of Spec.metID
+| Specify_Method of Method.id
-| Specify_Problem of Spec.pblID
+| Specify_Problem of Problem.id
 | Specify_Theory of ThyC.id
-| Subproblem of ThyC.id * Spec.pblID (* WN0509 drop *)
+| Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
 | Substitute of Selem.sube
 | Tac of string               (* WN0509 drop *)
 | Take of TermC.as_string | Take_Inst of TermC.as_string
 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
 | Add_Relation' of TermC.as_string * Model.itm list
 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
 * tactic Apply_Method metID
 * formula term                                        *)
-Spec.metID *  (* key for Know_Store                                     *)
+Method.id *  (* key for Know_Store                                     *)
 term option *  (* the first formula of Calc.T. TODO: rm option        *)
 Istate_Def.T * (* for the newly started program                       *)
 Proof.context  (* for the newly started program                       *)
 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
 | Begin_Sequ' | Begin_Trans' of term
 | End_Sequ' | End_Trans' of Selem.result
 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
 | CAScmd' of term
 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
-| Check_Postcond' of Spec.pblID *
+| Check_Postcond' of Problem.id *
 term         (* returnvalue of program in solve *)
 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
 term *       (* (1) the current formula: [x=1,x=...]                      *)
 string *     (* (2) the pred from Check_elementwise                       *)
 Selem.result (* (3) composed from (1) and (2): {x. pred}                  *)
 | End_Detail' of Selem.result
 | Empty_Tac_
 | Free_Solve'
-| Init_Proof' of TermC.as_string list * Spec.spec
+| Init_Proof' of TermC.as_string list * Spec.T
 | Model_Problem' of (* first step in specifying   *)
-Spec.pblID *     (* key into Know_Store           *)
+Problem.id *     (* key into Know_Store           *)
 Model.itm list *  (* the 'untouched' pbl        *)
 Model.itm list    (* the casually completed met *)
 | Or_to_List' of term * term
-| Refine_Problem' of Spec.pblID * (Model.itm list * (bool * term) list)
+| Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
 | Refine_Tacitly' of
-Spec.pblID *     (* input                                                                *)
+Problem.id *     (* input                                                                *)
-Spec.pblID *     (* the refined from applicable_in                                       *)
+Problem.id *     (* the refined from applicable_in                                       *)
 ThyC.id *      (* from new pbt?! filled in specify                                     *)
-Spec.metID *     (* from new pbt?! filled in specify                                     *)
+Method.id *     (* from new pbt?! filled in specify                                     *)
 Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
 | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
-| Specify_Method' of Spec.metID * Model.ori list * Model.itm list
+| Specify_Method' of Method.id * Model.ori list * Model.itm list
-| Specify_Problem' of Spec.pblID *
+| Specify_Problem' of Problem.id *
 (bool *                  (* matches	                                  *)
 (Model.itm list *      (* ppc	                                      *)
 (bool * term) list)) (* preconditions marked true/false           *)
 | Specify_Theory' of ThyC.id
 | Subproblem' of
-Spec.spec *
+Spec.T *
 		(Model.ori list) *       (* filled in associate Subproblem'           *)
 		term *                   (* filled -"-, headline of calc-head         *)
 		Selem.fmz_ *             (* string list from arguments                *)
 Proof.context *          (* for specify-phase                         *)
 		term                     (* Subproblem (thyID, pbl) OR cascmd         *)
 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
 | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^
 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
-Spec.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
+Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
 (spair2str (strs2str pblID, UnparseC.term scval))

changeset 59903	5037ca1b112b
parent 59902	e7910a62eaf2
child 59910	778899c624a6