wneuper/isa: src/Tools/isac/Interpret/solve-step.sml@cc5b51681c4b

     1 (* Title:  Specify/solve-step.sml

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     5 Code for the solve-phase in analogy to structure Specify_Step for the specify-phase.

     6 *)

     8 signature SOLVE_STEP =

     9 sig

    10   val check: Tactic.input -> Calc.T -> Applicable.T

    11   val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out

    12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    13   (*NONE*)

    14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    15   (*NONE*)

    16 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    17 end

    19 (**)

    20 structure Solve_Step(** ): SOLVE_STEP( **) =

    21 struct

    22 (**)

    24 (*

    25   check tactics (input by the user, mostly) for applicability

    26   and determine as much of the result of the tactic as possible initially.

    27 *)

    28 fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =

    29       let

    30         val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;

    31         val f = Calc.current_formula cs;

    32       in

    33         if msg = "OK"

    34         then

    35     	    case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of

    36     	      SOME (f', (id, thm))

    37     	        => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))

    38     	    | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable")

    39         else Applicable.No msg

    40       end

    41   | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)

    42       Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))

    43   | check (Tactic.Check_elementwise pred) cs =

    44       let

    45         val f = Calc.current_formula cs;

    46       in

    47         Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))

    48       end

    49   | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"

    50   | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')

    51   | check Tactic.Or_to_List cs =

    52        let

    53         val f = Calc.current_formula cs;

    54         val ls = Prog_Expr.or2list f;

    55       in

    56         Applicable.Yes (Tactic.Or_to_List' (f, ls))

    57       end

    58   | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =

    59       let

    60         val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;

    61         val thy = ThyC.get_theory thy';

    62         val f = Calc.current_formula cs;

    63       in

    64         if msg = "OK"

    65         then

    66           case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of

    67             SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))

    68           | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable")

    69         else Applicable.No msg

    70       end

    71   | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) =

    72       let

    73         val pp = Ctree.par_pblobj pt p;

    74         val thy' = Ctree.get_obj Ctree.g_domID pt pp;

    75         val thy = ThyC.get_theory thy';

    76         val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);

    77         val f = Calc.current_formula cs;

    78         val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)

    79       in

    80         case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of

    81           SOME (f', asm) =>

    82             Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))

    83         | NONE => Applicable.No (fst thm ^ " not applicable")

    84       end

    85   | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =

    86       let

    87         val pp = Ctree.par_pblobj pt p;

    88         val thy' = Ctree.get_obj Ctree.g_domID pt pp;

    89         val f = Calc.current_formula cs;

    90       in

    91         case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of

    92           SOME (f', asm)

    93             => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))

    94           | NONE => Applicable.No (rls ^ " not applicable")

    95       end

    96   | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =

    97       let

    98         val pp = Ctree.par_pblobj pt p;

    99         val thy' = Ctree.get_obj Ctree.g_domID pt pp;

   100         val thy = ThyC.get_theory thy';

   101         val f = Calc.current_formula cs;

   102     	  val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)

   103       in

   104         case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of

   105           SOME (f', asm)

   106             => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))

   107         | NONE => Applicable.No (rls ^ " not applicable")

   108       end

   109   | check (Tactic.Subproblem (domID, pblID)) (_, _) =

   110       Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],

   111 			  TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))

   112    | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =

   113       let

   114         val pp = Ctree.par_pblobj pt p

   115         val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)

   116         val f = Calc.current_formula cs;

   117 		    val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)

   118 		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)

   119 		    val subst = Subst.T_from_string_eqs thy sube

   120 		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

   121 		  in

   122 		    if foldl and_ (true, map TermC.contains_Var subte)

   123 		    then (*1*)

   124 		      let val f' = subst_atomic subst f

   125 		      in if f = f'

   126 		        then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")

   127 		        else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))

   128 		      end

   129 		    else (*2*)

   130 		      case Rewrite.rewrite_terms_ thy ro erls subte f of

   131 		        SOME (f', _) =>  Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))

   132 		      | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")

   133 		  end

   134   | check (Tactic.Tac id) (cs as (pt, (p, _))) =

   135       let

   136         val pp = Ctree.par_pblobj pt p;

   137         val thy' = Ctree.get_obj Ctree.g_domID pt pp;

   138         val thy = ThyC.get_theory thy';

   139         val f = Calc.current_formula cs;

   140       in case id of

   141         "subproblem_equation_dummy" =>

   142     	  if TermC.is_expliceq f

   143     	  then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))

   144     	  else Applicable.No "applicable only to equations made explicit"

   145       | "solve_equation_dummy" =>

   146     	  let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);

   147     	  in

   148     	    if id' <> "subproblem_equation_dummy"

   149     	    then Applicable.No "no subproblem"

   150     	    else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq

   151     		    then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))

   152     		    else error ("Solve_Step.check: f= " ^ f')

   153         end

   154       | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))

   155       end

   156   | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)

   157   | check (Tactic.Begin_Trans) cs =

   158       Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))

   159   | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)

   160     if p_ = Pos.Res

   161 	  then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))

   162     else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"

   163   | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''

   164   | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);

   166 fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)

   167     let

   168       val p =

   169         let val (ps, p') = split_last p (* no connex to prev.ppobj *)

   170 	      in if p' = 0 then ps @ [1] else p end

   171       val (pt, c) = Ctree.cappend_form pt p l t

   172     in

   173       ((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt)

   174     end

   175   | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =

   176     let

   177       val (pt, c) = Ctree.cappend_form pt p l t

   178       val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)

   179       (* replace the old PrfOjb ~~~~~ *)

   180       val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p

   181       val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)

   182     in

   183       ((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)

   184     end

   185   | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =

   186     (*append after existing PrfObj    vvvvvvvvvvvvv*)

   187     add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))

   188   | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =

   189     let

   190       val p' = Pos.lev_up p

   191       val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete

   192     in

   193       ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)

   194     end

   195   | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   196     let

   197       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f

   198         (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;

   199       val pt = Ctree.update_branch pt p Ctree.TransitiveB

   200     in

   201       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   202     end

   203  | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   204    let

   205      val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete

   206      val pt = Ctree.update_branch pt p Ctree.TransitiveB

   207    in

   208     ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   209    end

   210   | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   211     let

   212       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f

   213         (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete

   214       val pt = Ctree.update_branch pt p Ctree.TransitiveB

   215     in

   216       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   217     end

   218   | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   219     let

   220       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f

   221         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete

   222       val pt = Ctree.update_branch pt p Ctree.TransitiveB

   223     in

   224       ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   225     end

   226   | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =

   227       let

   228         val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete

   229       in

   230         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)

   231       end

   232   | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =

   233       let

   234         val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete

   235       in

   236         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   237       end

   238   | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =

   239       let

   240         val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete

   241       in

   242         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)

   243       end

   244   | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =

   245       let

   246         val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete

   247       in

   248         ((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)

   249       end

   250   | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =

   251       let

   252         val (pt,c) =

   253           Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete

   254         in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt)

   255         end

   256   | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =

   257       let

   258         val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete

   259       in

   260         ((p,Pos.Res), c, Generate.FormKF f', pt)

   261       end

   262   | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))

   263       (l as (_, ctxt)) (pt, (p, _)) =

   264     let

   265 	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))

   266 	      (oris, (domID, pblID, metID), hdl, ctxt_specify)

   267 	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f

   268     in

   269       ((p, Pos.Pbl), c, Generate.FormKF f, pt)

   270     end

   271   | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m')

   273 (**)end(**);

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 02 May 2020 17:39:04 +0200
changeset 59931	cc5b51681c4b
parent 59929	d2be99d0bf1e
child 59932	87336f3b021f
permissions	-rw-r--r--