1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sat Mar 07 17:53:32 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sat Mar 07 18:44:31 2020 +0100
1.3 @@ -19,8 +19,6 @@
1.4 val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
1.5 Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
1.6
1.7 -(*@NEW 1 vvv del*)
1.8 - val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
1.9 val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input
1.10 val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
1.11 Program.leaf * term option
1.12 @@ -43,16 +41,6 @@
1.13 (*TODO open Celem for L,R,D;
1.14 the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
1.15
1.16 -(* functions for the environment stack: NOT YET IMPLEMENTED
1.17 -fun accessenv id es = the (assoc ((top es) : Env.update, id))
1.18 - handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
1.19 -fun updateenv id vl (es : Env.update stack) =
1.20 - (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
1.21 -fun pushenv id vl (es : Env.update stack) =
1.22 - (push (overwrite(top es, (id, vl))) es) : Env.update stack;
1.23 -val popenv = pop : Env.update stack -> Env.update stack;
1.24 -*)
1.25 -
1.26 fun de_esc_underscore str =
1.27 let
1.28 fun scan [] = []
1.29 @@ -89,35 +77,31 @@
1.30 val _ = if pats = [] then raise ERROR errmsg else ()
1.31 in (flat o (map (itm2arg itms))) pats end;
1.32
1.33 -(*@NEW 2 vvv tac_from_prog, RM Empty_Tac_ *)
1.34 (* convert a Prog_Tac to Tactic.input *)
1.35 -fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
1.36 +fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
1.37 let
1.38 val tid = HOLogic.dest_string thmID
1.39 - in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
1.40 - | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
1.41 + in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid)) end
1.42 + | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
1.43 let
1.44 val tid = HOLogic.dest_string thmID
1.45 - in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
1.46 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
1.47 - (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.48 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
1.49 - (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.50 - | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
1.51 - (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
1.52 - | stac2tac_ _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
1.53 - | stac2tac_ _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
1.54 - (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
1.55 - | stac2tac_ _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
1.56 + in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid))) end
1.57 + | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
1.58 + (Tactic.Rewrite_Set (HOLogic.dest_string rls))
1.59 + | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
1.60 + (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls))
1.61 + | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
1.62 + (Tactic.Calculate (HOLogic.dest_string op_))
1.63 + | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t))
1.64 + | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
1.65 + (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub))
1.66 + | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
1.67 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
1.68 - (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
1.69 - | stac2tac_ _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
1.70 - | stac2tac_ pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
1.71 - Sub_Problem.tac_from_prog pt ptac (*might involve problem refinement etc*)
1.72 - | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
1.73 -
1.74 -(*@NEW 3 vvv RM *)
1.75 -fun tac_from_prog pt thy t = (fst o stac2tac_ pt thy) t;
1.76 + (Tactic.Check_elementwise (Rule.term_to_string''' thy pred))
1.77 + | tac_from_prog _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = Tactic.Or_to_List
1.78 + | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
1.79 + fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
1.80 + | tac_from_prog _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
1.81
1.82 datatype ass =
1.83 Ass of
1.84 @@ -263,8 +247,6 @@
1.85 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
1.86 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
1.87 | NONE => error "associate: Substitute' not applicable to val of Expr")
1.88 -
1.89 - (*compare "| stac2tac_ thy (Const ("Prog_Tac.SubProblem",_)" ..TODO: extract common code *)
1.90 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
1.91 (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
1.92 (case Sub_Problem.tac_from_prog pt stac of