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

     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 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    12   (*NONE*)

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

    14   (*NONE*)

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

    16 end

    18 (**)

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

    20 struct

    21 (**)

    23 (*

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

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

    26 *)

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

    28       let

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

    30         val f = Calc.current_formula cs;

    31       in

    32         if msg = "OK"

    33         then

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

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

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

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

    38         else Applicable.No msg

    39       end

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

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

    42   | check (Tactic.Check_elementwise pred) cs =

    43       let

    44         val f = Calc.current_formula cs;

    45       in

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

    47       end

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

    49   | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')        (* always applicable *)

    50   | check Tactic.Or_to_List (pt, (p, p_)) =

    51        let

    52         val f = case p_ of

    53           Pos.Frm => Ctree.get_obj Ctree.g_form pt p

    54     	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p

    55         | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

    56       in (let val ls = Prog_Expr.or2list f

    57           in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)

    58          handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)

    59       end

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

    61       let

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

    63         val thy = ThyC.get_theory thy';

    64         val f = Calc.current_formula cs;

    65       in

    66         if msg = "OK"

    67         then

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

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

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

    71         else Applicable.No msg

    72       end

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

    74       let

    75         val pp = Ctree.par_pblobj pt p;

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

    77         val thy = ThyC.get_theory thy';

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

    79         val f = Calc.current_formula cs;

    80       in

    81         let

    82           val subst = Subst.T_from_input thy subs;

    83         in

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

    85             SOME (f',asm) =>

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

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

    88         end

    89         handle _ => Applicable.No ("syntax error in " ^ subs2str subs)

    90       end

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

    92       let

    93         val pp = Ctree.par_pblobj pt p;

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

    95         val f = Calc.current_formula cs;

    96       in

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

    98           SOME (f', asm)

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

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

   101       end

   102   | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =

   103     if member op = [Pos.Pbl, Pos.Met] p_

   104     then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))

   105     else

   106       let

   107         val pp = Ctree.par_pblobj pt p;

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

   109         val thy = ThyC.get_theory thy';

   110         val f = Calc.current_formula cs;

   111     	  val subst = Subst.T_from_input thy subs;

   112       in

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

   114           SOME (f', asm)

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

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

   117         handle _ => Applicable.No ("syntax error in " ^(subs2str subs))

   118       end

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

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

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

   123    (*Substitute combines two different kind of "substitution":

   124       (1) subst_atomic: for ?a..?z

   125       (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)

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

   127       let

   128         val pp = Ctree.par_pblobj pt p

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

   130         val f = Calc.current_formula cs;

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

   132 		    val subte = Subst.input_to_terms sube

   133 		    val subst = Subst.T_from_string_eqs thy sube

   134 		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

   135 		  in

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

   137 		    then (*1*)

   138 		      let val f' = subst_atomic subst f

   139 		      in if f = f'

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

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

   142 		      end

   143 		    else (*2*)

   144 		      case Rewrite.rewrite_terms_ thy ro erls subte f of

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

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

   147 		  end

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

   149     let

   150       val pp = Ctree.par_pblobj pt p;

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

   152       val thy = ThyC.get_theory thy';

   153       val f = Calc.current_formula cs;

   154     in case id of

   155       "subproblem_equation_dummy" =>

   156   	  if TermC.is_expliceq f

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

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

   159     | "solve_equation_dummy" =>

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

   161   	  in

   162   	    if id' <> "subproblem_equation_dummy"

   163   	    then Applicable.No "no subproblem"

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

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

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

   167       end

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

   169     end

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

   171   | check (Tactic.Begin_Trans) (pt, (p, p_)) =

   172     let

   173       val (f, _) = case p_ of   (*p 12.4.00 unnecessary, implizit Take in gen*)

   174         Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)

   175       | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)

   176       | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));

   177     in (Applicable.Yes (Tactic.Begin_Trans' f))

   178       handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds  syntaxerror in '" ^ UnparseC.term f ^ "'")

   179     end

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

   181     if p_ = Pos.Res

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

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

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

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

   187 (**)end(**);

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 02 May 2020 15:41:27 +0200
changeset 59928	7601a1fa20b9
parent 59927	877d6bc38715
child 59929	d2be99d0bf1e
permissions	-rw-r--r--