1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Jul 11 16:39:46 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Jul 24 09:32:17 2019 +0200
1.3 @@ -8,14 +8,17 @@
1.4
1.5 type step = Tac.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
1.6 datatype ass = Ass of Tac.tac_ * term | AssWeak of Tac.tac_ * term | NotAss;
1.7 + val assod: Ctree.ctree -> 'a -> Tac.tac_ -> term -> ass
1.8
1.9 (* can these functions be local to Lucin or part of LItools ? *)
1.10 val sel_rules : Ctree.ctree -> Ctree.pos' -> Tac.tac list
1.11 val init_form : 'a -> Rule.program -> (term * term) list -> term option
1.12 val tac_2tac : Tac.tac_ -> Tac.tac
1.13 val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Rule.program
1.14 - val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.program
1.15 - val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.16 +
1.17 + val get_simplifier : Ctree.state -> Rule.rls
1.18 +(*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.program
1.19 +(*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.20 Rule.rls * (Selem.istate * Proof.context) * Rule.program
1.21 val rule2thm'' : Rule.rule -> Celem.thm''
1.22 val rule2rls' : Rule.rule -> string
1.23 @@ -24,7 +27,6 @@
1.24 val upd_env_opt : LTool.env -> term option * term -> LTool.env
1.25 val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_
1.26 val tac_2res : Tac.tac_ -> term
1.27 - val assod: Ctree.ctree -> 'a -> Tac.tac_ -> term -> ass
1.28 val stac2tac : Ctree.ctree -> theory -> term -> Tac.tac
1.29 val rts2steps:
1.30 (Tac.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list ->
1.31 @@ -58,12 +60,14 @@
1.32 (* data for creating a new node in ctree; designed for use as:
1.33 fun ass* scrstate steps = / ... case ass* scrstate steps of /
1.34 Assoc (scrstate, steps) => ... ass* scrstate steps *)
1.35 -type step =
1.36 +type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
1.37 + WN190713 COMPARE: taci list, see papernote #139 *)
1.38 Tac.tac_ (*transformed from associated tac *)
1.39 * Generate.mout (*result with indentation etc. *)
1.40 * ctree (*containing node created by tac_ + resp. scrstate *)
1.41 * pos' (*position in ctree; ctree * pos' is the proofstate *)
1.42 - * pos' list; (*of ctree-nodes probably cut (by fst tac_) *)
1.43 + * pos' list; (*of ctree-nodes probably cut (by fst tac_)
1.44 + WN190713 COMPARE: pos' list also in calcstate'*)
1.45
1.46 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
1.47 | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
1.48 @@ -81,30 +85,6 @@
1.49 | rew_only (((Tac.End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
1.50 | rew_only _ = false;
1.51
1.52 -(*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
1.53 - complicated with current t in rrlsstate.*)
1.54 -fun rts2steps steps ((pt, p), (f, f'', rss, rts), (thy', ro, er, pa)) [(r, (f', am))] =
1.55 - let
1.56 - val thy = Celem.assoc_thy thy'
1.57 - val ctxt = get_ctxt pt p |> Stool.insert_assumptions am
1.58 - val m = Tac.Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.59 - val is = Selem.RrlsState (f', f'', rss, rts)
1.60 - val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.61 - val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
1.62 - in (is, (m, mout, pt', p', cid) :: steps) end
1.63 - | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
1.64 - let
1.65 - val thy = Celem.assoc_thy thy'
1.66 - val ctxt = get_ctxt pt p |> Stool.insert_assumptions am
1.67 - val m = Tac.Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.68 - val is = Selem.RrlsState (f', f'', rss, rts)
1.69 - val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.70 - val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt
1.71 - in rts2steps ((m, mout, pt', p', cid)::steps)
1.72 - ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
1.73 - end
1.74 - | rts2steps _ _ _ = error "rts2steps: uncovered fun-def"
1.75 -
1.76 (* functions for the environment stack: NOT YET IMPLEMENTED
1.77 fun accessenv id es = the (assoc ((top es) : LTool.env, id))
1.78 handle _ => error ("accessenv: " ^ free2str id ^ " not in LTool.env");
1.79 @@ -282,14 +262,16 @@
1.80 | NotAss;
1.81
1.82 (* check if tac_ is associated with stac.
1.83 - Additional task: check if term t (the result has been calculated from) in tac_
1.84 + Additional tasks:
1.85 + (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
1.86 + (2) check if term t (the result has been calculated from) in tac_
1.87 has been changed (see "datatype tac_"); if yes, recalculate result
1.88 TODO.WN120106 recalculate impl.only for Substitute'
1.89 args
1.90 pt : ctree for pushing the thy specified in rootpbl into subpbls
1.91 d : unused (planned for data for comparison)
1.92 tac_ : from user (via applicable_in); to be compared with ...
1.93 - stac : found in Script
1.94 + stac : found in program
1.95 returns
1.96 Ass : associated: e.g. thmID in stac = thmID in m
1.97 +++ arg in stac = arg in m
1.98 @@ -617,11 +599,18 @@
1.99 in (Selem.ScrState (env, [], NONE, Rule.e_term, Selem.Safe, true), ctxt, scr) end;
1.100 end (*local*)
1.101
1.102 +fun get_simplifier (pt, (p, _)) =
1.103 + let
1.104 + val p' = Ctree.par_pblobj pt p
1.105 + val metID = Ctree.get_obj Ctree.g_metID pt p'
1.106 + val {srls, ...} = Specify.get_met metID
1.107 + in srls end
1.108 +
1.109 (* decide, where to get script/istate from:
1.110 (* 1 *) from PblObj.LTool.env: at begin of script if no init_form
1.111 (* 2 *) from PblObj/PrfObj: if stac is in the middle of the script
1.112 - (* 3 *) from rls/PrfObj: in case of detail a ruleset *)
1.113 -fun from_pblobj_or_detail' _ (p, p_) pt =
1.114 + (* 3 *) from rls/PrfObj: in case of detail a ruleset DEPRECATED in favour of inter_steps *)
1.115 +fun from_pblobj_or_detail' _ (p, p_) pt = (* DEPRECATED *)
1.116 if member op = [Pbl, Met] p_
1.117 then case get_obj g_env pt p of
1.118 NONE => error "from_pblobj_or_detail': no istate"
1.119 @@ -633,13 +622,13 @@
1.120 else
1.121 let val (pbl, p', rls') = par_pbl_det pt p
1.122 in if pbl
1.123 - then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
1.124 + then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
1.125 let
1.126 val metID = get_obj g_metID pt p'
1.127 val {srls,...} = Specify.get_met metID
1.128 in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end
1.129 - else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in inform, determine_next_tactic*) (* 3 *)
1.130 - (Rule.e_rls, get_loc pt (p,p_),
1.131 + else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in inform, determine_next_tactic*)
1.132 + (Rule.e_rls(*!!!*), get_loc pt (p,p_), (* 3 *)
1.133 case rls' of
1.134 Rule.Rls {scr = scr,...} => scr
1.135 | Rule.Seq {scr = scr,...} => scr
1.136 @@ -647,8 +636,7 @@
1.137 | Rule.Erls => error "from_pblobj_or_detail' with Erls")
1.138 end
1.139
1.140 -(*.get script and istate from PblObj, see ( * 1 *)
1.141 -fun from_pblobj' thy' (p,p_) pt =
1.142 +fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
1.143 let
1.144 val p' = par_pblobj pt p
1.145 val thy = Celem.assoc_thy thy'
1.146 @@ -665,6 +653,8 @@
1.147 in (srls, (is, ctxt), scr) end
1.148 else (srls, get_loc pt (p,p_), scr)
1.149 end;
1.150 +
1.151 +
1.152
1.153 (*.get the stactics and problems of a script as tacs
1.154 instantiated with the current environment;