# HG changeset patch # User Walther Neuper # Date 1562160631 -7200 # Node ID ef74a832fd69bff5a54a3d3c75f3b7d7671604da # Parent d50fe358f04abc6b989297c76c338ba561032728 lucin: rename scr --> program diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:30:31 2019 +0200 @@ -5,22 +5,22 @@ signature LUCAS_INTERPRETER = sig - val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> + val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe) datatype locate = Steps of Selem.istate * Lucin.step list | NotLocatable - val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a -> + val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.program * 'a -> Selem.istate * Proof.context -> locate datatype input_formula_result = Step of Ctree.state * Selem.istate * Proof.context | Not_Derivable of Chead.calcstate' - val locate_input_formula : Rule.scr -> Ctree.state -> Selem.istate -> Proof.context -> term + val locate_input_formula : Rule.program -> Ctree.state -> Selem.istate -> Proof.context -> term -> input_formula_result + val do_solve_step : Ctree.state -> + (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state val begin_end_prog : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state -> (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state - val do_solve_step : Ctree.state -> - (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) type assoc @@ -29,11 +29,11 @@ datatype appy = Appy of Tac.tac_ * Selem.scrstate | Napp of LTool.env | Skip of term * LTool.env datatype appy_ = Napp_ | Skip_ val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate' - val nstep_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env -> + val nstep_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> LTool.env -> Celem.lrd list -> appy_ -> term option -> term -> appy val appy : Rule.theory' * Rule.rls -> Ctree.state -> LTool.env -> Celem.lrd list -> term -> term option -> term -> appy - val nxt_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env -> + val nxt_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> LTool.env -> Celem.lrd list -> appy_ -> term -> term option -> term -> appy datatype asap = Aundef | AssOnly | AssGen; val go : Celem.loc_ -> term -> term diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/Interpret/mathengine.sml --- a/src/Tools/isac/Interpret/mathengine.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed Jul 03 15:30:31 2019 +0200 @@ -17,9 +17,9 @@ val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' val get_pblID : Ctree.state -> Celem.pblID option - val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Rule.scr * Model.itm list * (bool * term) list + val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Rule.program * Model.itm list * (bool * term) list val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list - val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Rule.scr * Model.itm list * (bool * term) list + val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Rule.program * Model.itm list * (bool * term) list val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/Interpret/script.sml Wed Jul 03 15:30:31 2019 +0200 @@ -11,12 +11,12 @@ (* can these functions be local to Lucin or part of LItools ? *) val sel_rules : Ctree.ctree -> Ctree.pos' -> Tac.tac list - val init_form : 'a -> Rule.scr -> (term * term) list -> term option + val init_form : 'a -> Rule.program -> (term * term) list -> term option val tac_2tac : Tac.tac_ -> Tac.tac - val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Rule.scr - val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.scr + val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Rule.program + val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.program val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> - Rule.rls * (Selem.istate * Proof.context) * Rule.scr + Rule.rls * (Selem.istate * Proof.context) * Rule.program val rule2thm'' : Rule.rule -> Celem.thm'' val rule2rls' : Rule.rule -> string val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tac.tac list diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/ThydataC/rule.sml --- a/src/Tools/isac/ThydataC/rule.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/ThydataC/rule.sml Wed Jul 03 15:30:31 2019 +0200 @@ -34,14 +34,14 @@ datatype rls = Erls | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls} + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls} | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls} + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls} | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string, - prepat: (term list * term) list, rew_ord: rew_ord, scr: scr} + prepat: (term list * term) list, rew_ord: rew_ord, scr: program} and rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule | Rls_ of rls | Thm of string * thm - and scr + and program = EmptyScr | Prog of term | Rfuns of @@ -57,14 +57,14 @@ val id_rule: rule -> string val eq_rule: rule * rule -> bool - val scr2str: scr -> string + val scr2str: program -> string val e_rrls: rls val e_rls: rls val rls2str: rls -> string val id_rls: rls -> string val rep_rls: rls -> {calc: calc list, erls: rls, errpats: errpatID list, id: string, - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls} + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls} val append_rls: string -> rls -> rule list -> rls val merge_rls: string -> rls -> rls -> rls val remove_rls: string -> rls -> rule list -> rls @@ -237,7 +237,7 @@ or left/right-hand-side of eqality .*) eval_fn | Rls_ of rls (*.ie. rule sets may be nested.*) -and scr = +and program = EmptyScr | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr' where 'exp' does not contain a tactic. *) @@ -299,7 +299,7 @@ calc : calc list, (*for Calculate in scr, set by prep_rls' *) rules : rule list, errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *) - scr : scr} (*Prog term: generating intermed.steps *) + scr : program} (*Prog term: generating intermed.steps *) | Seq of (*a sequence of rules to be tried only once *) {id : string, (*for trace_rewrite:=true *) preconds : term list, (*unused 20.8.02 *) @@ -311,7 +311,7 @@ calc : calc list, (*for Calculate in scr, set by prep_rls' *) rules : rule list, errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*) - scr : scr} (*Prog term (how to restrict type ???)*) + scr : program} (*Prog term (how to restrict type ???)*) (*Rrls call SML-code and simulate an rls difference: there is always _ONE_ redex rewritten in 1 call, @@ -329,7 +329,7 @@ erls : rls, (* for the conditions in rules and preconds *) calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *) errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*) - scr : scr}; (* Rfuns {...} (how to restrict type ???) *) + scr : program}; (* Rfuns {...} (how to restrict type ???) *) fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls"*) | id_rls (Rls {id, ...}) = id diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/calcelems.sml Wed Jul 03 15:30:31 2019 +0200 @@ -606,7 +606,7 @@ copy-named items are 'generating' if they are NOT "*'''" ?WN120516?? see ME/calchead.sml 'fun is_copy_named'. *) pre : term list, (* preconditions in where *) - scr : Rule.scr (* progam, empty as @{thm refl} or Rfuns *) + scr : Rule.program (* progam, empty as @{thm refl} or Rfuns *) }; val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'", erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls, diff -r d50fe358f04a -r ef74a832fd69 src/Tools/isac/xmlsrc/datatypes.sml --- a/src/Tools/isac/xmlsrc/datatypes.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Wed Jul 03 15:30:31 2019 +0200 @@ -40,7 +40,7 @@ val rls2xml : int -> Rule.thyID * Rule.rls -> Celem.xml val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml - val scr2xml : int -> Rule.scr -> Celem.xml + val scr2xml : int -> Rule.program -> Celem.xml val spec2xml : int -> Celem.spec -> Celem.xml val sub2xml : int -> Term.term * Term.term -> Celem.xml val subs2xml : int -> Selem.subs -> Celem.xml diff -r d50fe358f04a -r ef74a832fd69 test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:09:16 2019 +0200 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 03 15:30:31 2019 +0200 @@ -124,7 +124,7 @@ LucinNEW.Step (cstate, get_istate pt' pos', get_ctxt pt' pos') | _ => raise ERROR "compare_step: uncovered case" ; -locate_input_formula: scr -> state -> istate -> Proof.context -> term -> input_formula_result; +locate_input_formula: program -> state -> istate -> Proof.context -> term -> input_formula_result; "~~~~~ to inform return val:"; val () = (); case locate_input_formula prog (pt, pos) istate ctxt f_in of LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>