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

     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.CAScmd ct') _ =

    28     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))

    29   | check (m as Tactic.Calculate op_) (pt, (p, p_)) =

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

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

    32     else

    33       let

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

    35         val f = case p_ of

    36           Frm => Ctree.get_obj Ctree.g_form pt p

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

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

    39       in

    40         if msg = "OK"

    41         then

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

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

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

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

    46         else Applicable.No msg

    47       end

    48   | check (Tactic.Check_Postcond pI) (_, (p, p_)) =

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

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

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

    52   | check (m as Tactic.Check_elementwise pred) (pt, (p, p_)) =

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

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

    55     else

    56       let

    57         val pp = Ctree.par_pblobj pt p;

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

    59         val thy = ThyC.get_theory thy'

    60         val metID = (Ctree.get_obj Ctree.g_metID pt pp)

    61         val {crls, ...} =  Specify.get_met metID

    62         val (f, asm) = case p_ of

    63           Frm => (Ctree.get_obj Ctree.g_form pt p , [])

    64         | Pos.Res => Ctree.get_obj Ctree.g_result pt p

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

    66         val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> ApplicableOLD.mk_set thy pt p f;

    67       in

    68         Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))

    69       end

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

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

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

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

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

    75     else

    76       let

    77         val f = case p_ of

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

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

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

    81       in (let val ls = Prog_Expr.or2list f

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

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

    84       end

    85   | check (m as Tactic.Rewrite thm'') (pt, (p, p_)) =

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

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

    88     else

    89       let

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

    91         val thy = ThyC.get_theory thy';

    92         val f = case p_ of

    93           Frm => Ctree.get_obj Ctree.g_form pt p

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

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

    96       in

    97         if msg = "OK"

    98         then

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

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

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

   102         else Applicable.No msg

   103       end

   104   | check (m as Tactic.Rewrite_Inst (subs, thm'')) (pt, (p, p_)) =

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

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

   107     else

   108       let

   109         val pp = Ctree.par_pblobj pt p;

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

   111         val thy = ThyC.get_theory thy';

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

   113         val (f, _) = case p_ of (*p 12.4.00 unnecessary*)

   114                       Frm => (Ctree.get_obj Ctree.g_form pt p, p)

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

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

   117       in

   118         let

   119           val subst = Subst.T_from_input thy subs;

   120         in

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

   122             SOME (f',asm) =>

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

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

   125         end

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

   127       end

   128   | check (m as Tactic.Rewrite_Set rls) (pt, (p, p_)) =

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

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

   131     else

   132       let

   133         val pp = Ctree.par_pblobj pt p;

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

   135         val (f, _) = case p_ of

   136           Frm => (Ctree.get_obj Ctree.g_form pt p, p)

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

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

   139       in

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

   141           SOME (f', asm)

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

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

   144       end

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

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

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

   148     else

   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, _) = case p_ of

   154           Frm => (Ctree.get_obj Ctree.g_form pt p, p)

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

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

   157     	  val subst = Subst.T_from_input thy subs;

   158       in

   159         case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of

   160           SOME (f',asm)

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

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

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

   164       end

   165   | check (m as Tactic.Subproblem (domID, pblID)) (_, (p, p_)) =

   166      if Pos.on_specification p_

   167      then

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

   169      else (*some fields filled later in LI*)

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

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

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

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

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

   175   | check (m as Tactic.Substitute sube) (pt, (p, p_)) =

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

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

   178       else

   179         let

   180           val pp = Ctree.par_pblobj pt p

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

   182           val f = case p_ of

   183 		        Frm => Ctree.get_obj Ctree.g_form pt p

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

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

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

   187 		      val subte = Subst.input_to_terms sube

   188 		      val subst = Subst.T_from_string_eqs thy sube

   189 		      val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

   190 		    in

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

   192 		      then (*1*)

   193 		        let val f' = subst_atomic subst f

   194 		        in if f = f'

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

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

   197 		        end

   198 		      else (*2*)

   199 		        case Rewrite.rewrite_terms_ thy ro erls subte f of

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

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

   202 		    end

   203   | check (Tactic.Tac id) (pt, (p, p_)) =

   204     let

   205       val pp = Ctree.par_pblobj pt p;

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

   207       val thy = ThyC.get_theory thy';

   208       val f = case p_ of

   209          Frm => Ctree.get_obj Ctree.g_form pt p

   210       | Pos.Pbl => error "Solve_Step.check (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"

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

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

   213     in case id of

   214       "subproblem_equation_dummy" =>

   215   	  if TermC.is_expliceq f

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

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

   218     | "solve_equation_dummy" =>

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

   220   	  in

   221   	    if id' <> "subproblem_equation_dummy"

   222   	    then Applicable.No "no subproblem"

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

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

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

   226       end

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

   228     end

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

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

   231     let

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

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

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

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

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

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

   238     end

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

   240     if p_ = Pos.Res

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

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

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

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

   246 (**)end(**);

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 02 May 2020 12:13:20 +0200
changeset 59927	877d6bc38715
parent 59925	caf3839e53c5
child 59928	7601a1fa20b9
permissions	-rw-r--r--