1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:12:18 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:36:20 2016 +0100
1.3 @@ -8,21 +8,21 @@
1.4 signature LUCAS_INTERPRETER =
1.5 sig
1.6
1.7 - type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list
1.8 + type step = Ctree.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
1.9 datatype locate = NotLocatable | Steps of Ctree.istate * step list
1.10
1.11 val next_tac : (*diss: next-tactic-function*)
1.12 - theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
1.13 + theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
1.14 val locate_gen : (*diss: locate-function*)
1.15 - theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
1.16 + theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
1.17
1.18 (* can these functions be local to Lucin or part of LItools ? *)
1.19 - val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
1.20 + val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
1.21 val init_form : 'a -> scr -> (term * term) list -> term option
1.22 val tac_2tac : Ctree.tac_ -> Ctree.tac
1.23 val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr
1.24 - val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr
1.25 - val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree ->
1.26 + val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ctree -> rls * (Ctree.istate * Proof.context) * scr
1.27 + val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ctree ->
1.28 rls * (Ctree.istate * Proof.context) * scr
1.29 val rule2thm'' : rule -> thm''
1.30 val rule2rls' : rule -> string
1.31 @@ -31,7 +31,7 @@
1.32 datatype asap = Aundef | AssOnly | AssGen
1.33 datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
1.34 datatype appy_ = Napp_ | Skip_
1.35 - val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
1.36 + val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
1.37 val formal_args : term -> term list
1.38 val get_stac : 'a -> term -> term option
1.39 val go : loc_ -> term -> term
1.40 @@ -40,11 +40,11 @@
1.41 val id_of_scr : term -> string
1.42 val is_spec_pos : Ctree.pos_ -> bool
1.43 val itms2args : 'a -> metID -> itm list -> term list
1.44 - val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ ->
1.45 + val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ ->
1.46 term option -> term -> appy
1.47 - val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
1.48 - val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac
1.49 - val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_
1.50 + val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
1.51 + val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac
1.52 + val stac2tac_ : Ctree.ctree -> theory -> term -> Ctree.tac * Ctree.tac_
1.53 val upd_env_opt : env -> term option * term -> env
1.54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.55 end
1.56 @@ -64,9 +64,9 @@
1.57 type step =
1.58 tac_ (*transformed from associated tac *)
1.59 * Generate.mout (*result with indentation etc. *)
1.60 - * ptree (*containing node created by tac_ + resp. scrstate *)
1.61 - * pos' (*position in ptree; ptree * pos' is the proofstate *)
1.62 - * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
1.63 + * ctree (*containing node created by tac_ + resp. scrstate *)
1.64 + * pos' (*position in ctree; ctree * pos' is the proofstate *)
1.65 + * pos' list; (*of ctree-nodes probably cut (by fst tac_) *)
1.66
1.67 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
1.68 | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r);
1.69 @@ -213,7 +213,7 @@
1.70
1.71 (* convert a script-tac 'stac' to a tactic 'tac';
1.72 if stac is an initac, then convert to a 'tac_' (as required in appy).
1.73 - arg ptree for pushing the thy specified in rootpbl into subpbls *)
1.74 + arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.75 fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =
1.76 let
1.77 val tid = (de_esc_underscore o strip_thy) thmID
1.78 @@ -295,7 +295,7 @@
1.79 has been changed (see "datatype tac_"); if yes, recalculate result
1.80 TODO.WN120106 recalculate impl.only for Substitute'
1.81 args
1.82 - pt : ptree for pushing the thy specified in rootpbl into subpbls
1.83 + pt : ctree for pushing the thy specified in rootpbl into subpbls
1.84 d : unused (planned for data for comparison)
1.85 tac_ : from user (via applicable_in); to be compared with ...
1.86 stac : found in Script
1.87 @@ -563,8 +563,8 @@
1.88 (step list) (* list of steps done until associated stac found;
1.89 initiated with the data for doing the 1st step,
1.90 thus the head holds these data further on,
1.91 - while the tail holds steps finished (incl.scrstate in ptree) *)
1.92 -| NasApp of (* stac not associated, but applicable, ptree-node generated *)
1.93 + while the tail holds steps finished (incl.scrstate in ctree) *)
1.94 +| NasApp of (* stac not associated, but applicable, ctree-node generated *)
1.95 scrstate * (step list)
1.96 | NasNap of (* stac not associated, not applicable, nothing generated;
1.97 for distinction in Or, for leaving iterations, leaving Seq,
1.98 @@ -789,7 +789,7 @@
1.99 datatype locate =
1.100 Steps of istate (* producing hd of step list (which was latest)
1.101 for next_tac, for reporting Safe|Unsafe to DG *)
1.102 - * step (* (scrstate producing this step is in ptree !) *)
1.103 + * step (* (scrstate producing this step is in ctree !) *)
1.104 list (* locate_gen may produce intermediate steps *)
1.105 | NotLocatable; (* no (m Ass m') or (m AssWeak m') found *)
1.106
1.107 @@ -798,7 +798,7 @@
1.108 or the end of the script
1.109 args
1.110 m : input by the user, already checked by applicable_in,
1.111 - (to be searched within Or; and _not_ an m doing the step on ptree !)
1.112 + (to be searched within Or; and _not_ an m doing the step on ctree !)
1.113 p,pt: (incl ets) at the time of input
1.114 scr : the script
1.115 d : canonical simplifier for locating Take, Substitute, Subproblems etc.
1.116 @@ -819,7 +819,7 @@
1.117 (case lo rss f (Thm thm) of
1.118 [] => NotLocatable
1.119 | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.120 - | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
1.121 + | locate_gen (thy',srls) (m:tac_) ((pt,p):ctree * pos')
1.122 (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.123 let val thy = assoc_thy thy';
1.124 in case if l = [] orelse (
1.125 @@ -1042,7 +1042,7 @@
1.126 | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
1.127 (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
1.128 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.129 - | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body))
1.130 + | next_tac thy (ptp as (pt, (p, _)):ctree * pos') (sc as Prog (_ $ body))
1.131 (ScrState (E,l,a,v,s,_), ctxt) =
1.132 (case if l = [] then appy thy ptp E [R] body NONE v
1.133 else nstep_up thy ptp sc E l Skip_ a v of