1.1 --- a/src/Tools/isac/Interpret/script.sml Tue Feb 04 16:45:36 2020 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,623 +0,0 @@
1.4 -(* Title: interpreter for scripts
1.5 - Author: Walther Neuper 2000
1.6 - (c) due to copyright terms
1.7 -*)
1.8 -
1.9 -signature LUCAS_INTERPRETER_DEL =
1.10 -sig
1.11 -
1.12 - type step = Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
1.13 - datatype ass =
1.14 - Ass of Tactic.T * term * Proof.context
1.15 - | Ass_Weak of Tactic.T * term * Proof.context
1.16 - | NotAss;
1.17 - val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
1.18 -
1.19 -(* can these functions be local to Lucin or part of LItools ? *)
1.20 - val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
1.21 - val init_form : 'a -> Program.T -> (term * term) list -> term option
1.22 - val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
1.23 -
1.24 - val get_simplifier : Calc.T -> Rule.rls
1.25 -(*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.26 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
1.27 -(*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.28 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
1.29 - val rule2thm'' : Rule.rule -> Celem.thm''
1.30 - val rule2rls' : Rule.rule -> string
1.31 - val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
1.32 -(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
1.33 - val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
1.34 - val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
1.35 - val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
1.36 - val check_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
1.37 - string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
1.38 - Program.leaf * term option
1.39 -
1.40 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.41 - (*NONE*)
1.42 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.43 - val is_spec_pos : Ctree.pos_ -> bool
1.44 - val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
1.45 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.46 -
1.47 -end
1.48 -
1.49 -(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
1.50 -val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
1.51 -
1.52 -(**)
1.53 -structure Lucin(**): LUCAS_INTERPRETER_DEL(**) =
1.54 -struct
1.55 -(**)
1.56 -open Ctree
1.57 -open Pos
1.58 -(*TODO open Celem for L,R,D;
1.59 - the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
1.60 -
1.61 -(**)
1.62 -(* data for creating a new node in ctree; designed for use as:
1.63 - fun ass* pstate steps = / ... case ass* pstate steps of /
1.64 - Accept_Tac1 (pstate, steps) => ... ass* pstate steps *)
1.65 -type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
1.66 - WN190713 COMPARE: taci list, see papernote #139 *)
1.67 - Tactic.T (*transformed from associated tac *)
1.68 - * Generate.mout (*result with indentation etc. *)
1.69 - * ctree (*containing node created by tac_ + resp. pstate *)
1.70 - * pos' (*position in ctree; ctree * pos' is the proofstate *)
1.71 - * pos' list; (*of ctree-nodes probably cut (by fst tac_)
1.72 - WN190713 COMPARE: pos' list also in calcstate'*)
1.73 -
1.74 -fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
1.75 - | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
1.76 -fun rule2rls' (Rule.Rls_ rls) = Rule.id_rls rls
1.77 - | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
1.78 -
1.79 -(*check if there are tacs for rewriting only*)
1.80 -fun rew_only ([]:step list) = true
1.81 - | rew_only (((Tactic.Rewrite' _ ,_,_,_,_))::ss) = rew_only ss
1.82 - | rew_only (((Tactic.Rewrite_Inst' _ ,_,_,_,_))::ss) = rew_only ss
1.83 - | rew_only (((Tactic.Rewrite_Set' _ ,_,_,_,_))::ss) = rew_only ss
1.84 - | rew_only (((Tactic.Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss
1.85 - | rew_only (((Tactic.Calculate' _ ,_,_,_,_))::ss) = rew_only ss
1.86 - | rew_only (((Tactic.Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
1.87 - | rew_only (((Tactic.End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
1.88 - | rew_only _ = false;
1.89 -
1.90 -(* functions for the environment stack: NOT YET IMPLEMENTED
1.91 -fun accessenv id es = the (assoc ((top es) : Env.update, id))
1.92 - handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
1.93 -fun updateenv id vl (es : Env.update stack) =
1.94 - (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
1.95 -fun pushenv id vl (es : Env.update stack) =
1.96 - (push (overwrite(top es, (id, vl))) es) : Env.update stack;
1.97 -val popenv = pop : Env.update stack -> Env.update stack;
1.98 -*)
1.99 -
1.100 -fun de_esc_underscore str =
1.101 - let
1.102 - fun scan [] = []
1.103 - | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
1.104 - in (implode o scan o Symbol.explode) str end;
1.105 -
1.106 -fun init_form thy (Rule.Prog sc) env =
1.107 - (case Prog_Tac.get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
1.108 - | init_form _ _ _ = error "init_form: no match";
1.109 -
1.110 -type dsc = typ; (* <-> nam..unknow in Descript.thy *)
1.111 -
1.112 -(*.create the actual parameters (args) of script: their order
1.113 - is given by the order in met.pat .*)
1.114 -(*WN.5.5.03: ?: does this allow for different descriptions ???
1.115 - ?: why not taken from formal args of script ???
1.116 -!: FIXXXME penv: push it here in itms2args into script-evaluation*)
1.117 -val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
1.118 -fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
1.119 -"itms:\n" ^ Model.itms2str_ @{context} itms)
1.120 -fun itms2args _ mI itms =
1.121 - let
1.122 - val mvat = Model.max_vt itms
1.123 - fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
1.124 - val itms = filter (okv mvat) itms
1.125 - fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
1.126 - fun itm2arg itms (_,(d,_)) =
1.127 - case find_first (test_dsc d) itms of
1.128 - NONE => raise ERROR (errmsg2 d itms)
1.129 - | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
1.130 - (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
1.131 - penv postponed; presently penv holds already Env.update for script*)
1.132 - val pats = (#ppc o Specify.get_met) mI
1.133 - val _ = if pats = [] then raise ERROR errmsg else ()
1.134 - in (flat o (map (itm2arg itms))) pats end;
1.135 -
1.136 -(* convert a script-tac 'stac' to 'tac' for users;
1.137 - for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.138 - if stac is an initac, then convert to a 'tac_' (as required in scan_dn).
1.139 - arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.140 -fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
1.141 - let
1.142 - val tid = HOLogic.dest_string thmID
1.143 - in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
1.144 - | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
1.145 - let
1.146 - val tid = HOLogic.dest_string thmID
1.147 - in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
1.148 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
1.149 - (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.150 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
1.151 - (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.152 - | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
1.153 - (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
1.154 - | stac2tac_ _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
1.155 - | stac2tac_ _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
1.156 - (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
1.157 - | stac2tac_ _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
1.158 - (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
1.159 - (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
1.160 - | stac2tac_ _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
1.161 -
1.162 - (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
1.163 - | stac2tac_ pt _ (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
1.164 - let
1.165 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
1.166 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
1.167 - val ags = TermC.isalist2list ags';
1.168 - val (pI, pors, mI) =
1.169 - if mI = ["no_met"]
1.170 - then
1.171 - let
1.172 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.173 - (* Chead.match_ags : theory -> pat list -> term list -> ori list
1.174 - ^^^ variables ^^^ values *)
1.175 - handle ERROR "actual args do not match formal args"
1.176 - => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
1.177 - val pI' = Specify.refine_ori' pors pI;
1.178 - in (pI', pors (* refinement over models with diff.prec only *),
1.179 - (hd o #met o Specify.get_pbt) pI') end
1.180 - else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.181 - handle ERROR "actual args do not match formal args"
1.182 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
1.183 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
1.184 - val {cas,ppc,thy,...} = Specify.get_pbt pI
1.185 - val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
1.186 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
1.187 - val ctxt = ContextC.initialise dI vals
1.188 - val hdl =
1.189 - case cas of
1.190 - NONE => Auto_Prog.pblterm dI pI
1.191 - | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
1.192 - val f = Auto_Prog.subpbl (strip_thy dI) pI
1.193 - in (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
1.194 - end
1.195 - | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
1.196 -
1.197 -fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
1.198 -
1.199 -datatype ass =
1.200 - Ass of
1.201 - Tactic.T (* SubProblem gets args instantiated in associate *)
1.202 - * term (* for itr_arg, result in ets *)
1.203 - * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
1.204 - | Ass_Weak of Tactic.T * term * Proof.context
1.205 - | NotAss;
1.206 -
1.207 -(* check if tac_ is associated with stac.
1.208 - Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
1.209 - Additional tasks:
1.210 - (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
1.211 - (2) check if term t (the result has been calculated from) in tac_
1.212 - has been changed (see "datatype tac_"); if yes, recalculate result
1.213 - TODO.WN120106 recalculate impl.only for Substitute'
1.214 -args
1.215 - pt : ctree for pushing the thy specified in rootpbl into subpbls
1.216 - d : unused (planned for data for comparison)
1.217 - tac_ : from user (via applicable_in); to be compared with ...
1.218 - stac : found in program
1.219 -returns
1.220 - Ass : associated: e.g. thmID in stac = thmID in m
1.221 - +++ arg in stac = arg in m
1.222 - Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.223 - NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.224 -*)
1.225 -fun associate _ ctxt (m as Tactic.Rewrite_Inst'
1.226 - (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.227 - (case stac of
1.228 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
1.229 - if thmID = HOLogic.dest_string thmID_
1.230 - then
1.231 - if f = f_
1.232 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.233 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.234 - else ((*tracing"3### associate ..NotAss";*) NotAss)
1.235 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
1.236 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.237 - then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.238 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.239 - else NotAss
1.240 - | _ => NotAss)
1.241 - | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.242 - (case stac of
1.243 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
1.244 - if thmID = HOLogic.dest_string thmID_
1.245 - then
1.246 - if f = f_
1.247 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.248 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.249 - else NotAss
1.250 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
1.251 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.252 - then
1.253 - if f = f_
1.254 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.255 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.256 - else NotAss
1.257 - | _ => NotAss)
1.258 - | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.259 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.260 - if Rule.id_rls rls = HOLogic.dest_string rls_
1.261 - then
1.262 - if f = f_
1.263 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.264 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.265 - else NotAss
1.266 - | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.267 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.268 - if Rule.id_rls rls = HOLogic.dest_string rls_
1.269 - then
1.270 - if f = f_
1.271 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.272 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.273 - else NotAss
1.274 - | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
1.275 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.276 - if Rule.id_rls rls = HOLogic.dest_string rls_
1.277 - then
1.278 - if f = f_
1.279 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.280 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.281 - else NotAss
1.282 - | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
1.283 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.284 - if Rule.id_rls rls = HOLogic.dest_string rls_
1.285 - then
1.286 - if f = f_
1.287 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.288 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.289 - else NotAss
1.290 - | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
1.291 - (case stac of
1.292 - (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
1.293 - if op_ = HOLogic.dest_string op__
1.294 - then
1.295 - if f = f_
1.296 - then Ass (m, f', ctxt)
1.297 - else Ass_Weak (m ,f', ctxt)
1.298 - else NotAss
1.299 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
1.300 - let val thy = Celem.assoc_thy "Isac_Knowledge";
1.301 - in
1.302 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
1.303 - (assoc_rls (HOLogic.dest_string rls_))
1.304 - then
1.305 - if f = f_
1.306 - then Ass (m, f', ctxt)
1.307 - else Ass_Weak (m ,f', ctxt)
1.308 - else NotAss
1.309 - end
1.310 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
1.311 - let val thy = Celem.assoc_thy "Isac_Knowledge";
1.312 - in
1.313 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
1.314 - (assoc_rls (HOLogic.dest_string rls_))
1.315 - then
1.316 - if f = f_
1.317 - then Ass (m, f', ctxt)
1.318 - else Ass_Weak (m ,f', ctxt)
1.319 - else NotAss
1.320 - end
1.321 - | _ => NotAss)
1.322 - | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
1.323 - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
1.324 - if consts = consts'
1.325 - then Ass (m, consts_chkd, ctxt)
1.326 - else NotAss
1.327 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
1.328 - Ass (m, list, ctxt)
1.329 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
1.330 - | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
1.331 - (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
1.332 - if f = t then Ass (m, f', ctxt)
1.333 - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.334 - if foldl and_ (true, map TermC.contains_Var subte)
1.335 - then
1.336 - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
1.337 - in if t = t' then error "associate: Substitute' not applicable to val of Expr"
1.338 - else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
1.339 - end
1.340 - else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
1.341 - SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
1.342 - | NONE => error "associate: Substitute' not applicable to val of Expr")
1.343 -
1.344 - (*compare "| stac2tac_ thy (Const ("Prog_Tac.SubProblem",_)" ..TODO: extract common code *)
1.345 - | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
1.346 - (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) =
1.347 - let
1.348 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
1.349 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
1.350 - val ags = TermC.isalist2list ags';
1.351 - val (pI, pors, mI) =
1.352 - if mI = ["no_met"]
1.353 - then
1.354 - let
1.355 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.356 - handle ERROR "actual args do not match formal args"
1.357 - => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
1.358 - val pI' = Specify.refine_ori' pors pI;
1.359 - in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
1.360 - end
1.361 - else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.362 - handle ERROR "actual args do not match formal args"
1.363 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
1.364 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
1.365 - val {cas, ppc, thy, ...} = Specify.get_pbt pI
1.366 - val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
1.367 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
1.368 - val ctxt = ContextC.initialise dI vals
1.369 - val hdl =
1.370 - case cas of
1.371 - NONE => Auto_Prog.pblterm dI pI
1.372 - | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
1.373 - val f = Auto_Prog.subpbl (strip_thy dI) pI
1.374 - in
1.375 - if domID = dI andalso pblID = pI
1.376 - then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ContextC.e_ctxt(*TODO rm*), f), f, ctxt)
1.377 - else NotAss
1.378 - end
1.379 - | associate _ _ (m, _) =
1.380 - (if (!trace_script)
1.381 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
1.382 - ^ "@@@ tac_ = " ^ Tactic.string_of m)
1.383 - else ();
1.384 - NotAss);
1.385 -
1.386 -(* create the initial interpreter state
1.387 - from the items of the guard and the formal arguments of the partial_function.
1.388 -Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
1.389 - (a) fmz is given by a math author
1.390 - (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
1.391 - (c) modelling creates an itm list from ori list + possible user input
1.392 - (d) specifying a theory might add some items and create a guard for the partial_function
1.393 - (e) fun relate_args creates an environment for evaluating the partial_function.
1.394 -Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
1.395 - * Since the arguments of the partial_function have no description (see Descript.thy),
1.396 - (e) depends on the sequence in fmz_ and on the types of the formal arguments.
1.397 - * pairing formal arguments with itm's follows the sequence
1.398 - * Thus the resulting sequence-relation can be ambiguous.
1.399 - * Ambiguities are done by rearranging fmz_ or the formal arguments.
1.400 - * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
1.401 - *)
1.402 -local
1.403 -val errmsg = "ERROR: found no actual arguments for prog. of "
1.404 -fun msg_miss sc metID caller f formals actuals =
1.405 - "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
1.406 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
1.407 - "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
1.408 - "with:\n" ^
1.409 - (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
1.410 - (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
1.411 -fun msg_miss_type sc metID f formals actuals =
1.412 - "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
1.413 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
1.414 - "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
1.415 - "\" doesn't mach an actual arg.\nwith:\n" ^
1.416 - (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
1.417 - (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
1.418 - " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
1.419 -fun msg_ambiguous sc metID f aas formals actuals =
1.420 - "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
1.421 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
1.422 - "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
1.423 - "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
1.424 - "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
1.425 - "with\n" ^
1.426 - "formals: " ^ Rule.terms2str formals ^ "\n" ^
1.427 - "actuals: " ^ Rule.terms2str actuals
1.428 -fun trace_init metID =
1.429 - if (!trace_script)
1.430 - then tracing("@@@ program " ^ strs2str metID)
1.431 - else ();
1.432 -fun trace_istate env =
1.433 - if (!trace_script)
1.434 - then tracing("@@@ istate " ^ Env.env2str env)
1.435 - else ();
1.436 -in
1.437 -fun init_pstate srls ctxt itms metID =
1.438 - let
1.439 - val itms = Specify.hack_until_review_Specify_2 metID itms
1.440 - val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
1.441 - val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
1.442 - val (scr, sc) = (case (#scr o Specify.get_met) metID of
1.443 - scr as Rule.Prog sc => (trace_init metID; (scr, sc))
1.444 - | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
1.445 - val formals = Program.formal_args sc
1.446 - fun assoc_by_type f aa =
1.447 - case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
1.448 - [] => error (msg_miss_type sc metID f formals actuals)
1.449 - | [a] => (f, a)
1.450 - | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
1.451 - fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
1.452 - | relate_args env [] _ = env (*may drop Find?*)
1.453 - | relate_args env (f::ff) (aas as (a::aa)) =
1.454 - if type_of f = type_of a
1.455 - then relate_args (env @ [(f, a)]) ff aa
1.456 - else
1.457 - let val (f, a) = assoc_by_type f aas
1.458 - in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
1.459 - val {pre, prls, ...} = Specify.get_met metID;
1.460 - val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
1.461 - val ctxt = ctxt |> ContextC.insert_assumptions pres;
1.462 - val ist = Istate.e_pstate
1.463 - |> Istate.set_eval srls
1.464 - |> Istate.set_env_true (relate_args [] formals actuals)
1.465 - in
1.466 - (Istate.Pstate ist, ctxt, scr)
1.467 - end;
1.468 -end (*local*)
1.469 -
1.470 -fun get_simplifier (pt, (p, _)) =
1.471 - let
1.472 - val p' = Ctree.par_pblobj pt p
1.473 - val metID = Ctree.get_obj Ctree.g_metID pt p'
1.474 - val {srls, ...} = Specify.get_met metID
1.475 - in srls end
1.476 -
1.477 -(* decide, where to get program/istate from:
1.478 - (* 1 *) from PblObj.Env.update: at begin of program if no init_form
1.479 - (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
1.480 - (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
1.481 -fun from_pblobj_or_detail' _ (p, p_) pt =
1.482 - if member op = [Pbl, Met] p_
1.483 - then case get_obj g_env (*?DEPRECATED?*) pt p of
1.484 - NONE => error "from_pblobj_or_detail': no istate"
1.485 - | SOME (Istate.Pstate pst, ctxt) =>
1.486 - let
1.487 - val metID = get_obj g_metID pt p
1.488 - val {srls, ...} = Specify.get_met metID
1.489 - in
1.490 - (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
1.491 - end
1.492 - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
1.493 - else
1.494 - let val (pbl, p', rls') = par_pbl_det pt p
1.495 - in if pbl
1.496 - then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
1.497 - let
1.498 - val metID = get_obj g_metID pt p'
1.499 - val {srls, ...} = Specify.get_met metID
1.500 - val (is, ctxt) =
1.501 - case get_loc pt (p, p_) of
1.502 - (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
1.503 - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
1.504 - in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
1.505 - else
1.506 - let
1.507 - (*TODO.thy Auto_Prog.generate SHOULD REPLACE ALL HIS..*)
1.508 - val prog = case rls' of
1.509 - Rule.Rls {scr = Rule.Prog prog,...} => prog
1.510 - | Rule.Seq {scr = Rule.Prog prog,...} => prog
1.511 - | _ => raise ERROR ("from_pblobj_or_detail': not for rule-set \"" ^ Rule.id_rls rls' ^ "\"")
1.512 - val t = get_last_formula (pt, (p, p_))
1.513 - val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
1.514 - in (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') end
1.515 - end
1.516 -
1.517 -fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
1.518 - let
1.519 - val p' = par_pblobj pt p
1.520 - val itms =
1.521 - (case get_obj I pt p' of
1.522 - PblObj {meth = itms, ...} => itms
1.523 - | PrfObj _ => error "from_pblobj' NOT with PrfObj")
1.524 - val metID = get_obj g_metID pt p'
1.525 - val {srls, scr, ...} = Specify.get_met metID
1.526 - in
1.527 - if last_elem p = 0 (*nothing written to pt yet*)
1.528 - then
1.529 - let
1.530 - val ctxt = ContextC.initialise thy' (Model.vars_of itms)
1.531 - val (is, ctxt, scr) = init_pstate srls ctxt itms metID
1.532 - in (srls(*..\<in> is*), (is, ctxt), scr) end
1.533 - else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
1.534 - end;
1.535 -
1.536 -(*.get the stactics and problems of a script as tacs
1.537 - instantiated with the current environment;
1.538 - l is the location which generated the given formula.*)
1.539 -(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
1.540 -fun is_spec_pos Pbl = true
1.541 - | is_spec_pos Met = true
1.542 - | is_spec_pos _ = false;
1.543 -
1.544 -(* handle a leaf at the end of recursive descent:
1.545 - a leaf is either a tactic or an 'expr' in "let v = expr"
1.546 - where "expr" does not contain a tactic.
1.547 - Handling a leaf comprises
1.548 - (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
1.549 - (2) rewrite the leaf by 'srls'
1.550 -*)
1.551 -fun check_leaf call ctxt srls (E, (a, v)) t =
1.552 - case Prog_Tac.eval_leaf E a v t of
1.553 - (Program.Tac stac, a') =>
1.554 - let val stac' =
1.555 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
1.556 - (subst_atomic (Env.update_opt E (a,v)) stac)
1.557 - in
1.558 - (if (! trace_script)
1.559 - then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
1.560 - else ();
1.561 - (Program.Tac stac', a'))
1.562 - end
1.563 - | (Program.Expr lexpr, a') =>
1.564 - let val lexpr' =
1.565 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
1.566 - in
1.567 - (if (! trace_script)
1.568 - then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
1.569 - else ();
1.570 - (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
1.571 - end;
1.572 -
1.573 -(*. fetch _all_ tactics from script .*)
1.574 -fun sel_rules _ (([],Res):pos') =
1.575 - raise PTREE "no tactics applicable at the end of a calculation"
1.576 - | sel_rules pt (p,p_) =
1.577 - if is_spec_pos p_
1.578 - then [get_obj g_tac pt p]
1.579 - else
1.580 - let
1.581 - val pp = par_pblobj pt p;
1.582 - val thy' = get_obj g_domID pt pp;
1.583 - val thy = Celem.assoc_thy thy';
1.584 - val metID = get_obj g_metID pt pp;
1.585 - val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
1.586 - val (sc, srls) = (case Specify.get_met metID' of
1.587 - {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
1.588 - val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
1.589 - val ctxt = get_ctxt pt (p, p_)
1.590 - in map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
1.591 - (check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
1.592 - end;
1.593 -
1.594 -(* fetch tactics from script and filter _applicable_ tactics;
1.595 - in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
1.596 -fun sel_appl_atomic_tacs _ (([], Res) : pos') =
1.597 - raise PTREE "no tactics applicable at the end of a calculation"
1.598 - | sel_appl_atomic_tacs pt (p, p_) =
1.599 - if is_spec_pos p_
1.600 - then [get_obj g_tac pt p]
1.601 - else
1.602 - let
1.603 - val pp = par_pblobj pt p
1.604 - val thy' = get_obj g_domID pt pp
1.605 - val thy = Celem.assoc_thy thy'
1.606 - val metID = get_obj g_metID pt pp
1.607 - val metID' =
1.608 - if metID = Celem.e_metID
1.609 - then (thd3 o snd3) (get_obj g_origin pt pp)
1.610 - else metID
1.611 - val (sc, srls, erls, ro) = (case Specify.get_met metID' of
1.612 - {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
1.613 - | _ => error "sel_appl_atomic_tacs 1")
1.614 - val (env, (a, v)) = (case get_istate pt (p, p_) of
1.615 - Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
1.616 - val ctxt = get_ctxt pt (p, p_)
1.617 - val alltacs = (*we expect at least 1 stac in a script*)
1.618 - map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
1.619 - (check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
1.620 - val f =
1.621 - (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
1.622 - | _ => error "")
1.623 - (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
1.624 - in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
1.625 -
1.626 -(**)end(**)