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

     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.Check_Postcond pI) (_, (p, p_)) =

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

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

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

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

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

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

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

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

    36     else

    37       let

    38         val pp = Ctree.par_pblobj pt p;

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

    40         val thy = ThyC.get_theory thy';

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

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

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

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

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

    46       in

    47         let

    48           val subst = Subst.T_from_input thy subs;

    49         in

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

    51             SOME (f',asm) =>

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

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

    54         end

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

    56       end

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

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

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

    60     else

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

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

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

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

    68       in

    69         if msg = "OK"

    70         then

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

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

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

    74         else Applicable.No msg

    75       end

    76   | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =

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

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

    79     else

    80       let

    81         val pp = Ctree.par_pblobj pt p;

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

    83         val thy = ThyC.get_theory thy';

    84         val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p

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

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

    87         val subst = Subst.T_from_input thy subs

    88       in

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

    90           SOME (f', asm)

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

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

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

    94       end

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

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

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

    98     else

    99       let

   100         val pp = Ctree.par_pblobj pt p;

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

   102         val thy = ThyC.get_theory thy';

   103         val (f, _) = case p_ of

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

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

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

   107     	  val subst = Subst.T_from_input thy subs;

   108       in

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

   110           SOME (f',asm)

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

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

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

   114       end

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

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

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

   118     else

   119       let

   120         val pp = Ctree.par_pblobj pt p;

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

   122         val (f, _) = case p_ of

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

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

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

   126       in

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

   128           SOME (f', asm)

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

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

   131       end

   132   | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =

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

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

   135     else

   136     	let

   137     	  val pp = Ctree.par_pblobj pt p

   138     	  val thy' = Ctree.get_obj Ctree.g_domID pt pp

   139     	  val f = case p_ of

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

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

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

   143     	in

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

   145     	    SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))

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

   147     	end

   148   | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)

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

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

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

   152     else

   153       let

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

   155         val f = case p_ of

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

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

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

   159       in

   160         if msg = "OK"

   161         then

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

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

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

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

   166         else Applicable.No msg

   167       end

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

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

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

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

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

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

   174       else

   175         let

   176           val pp = Ctree.par_pblobj pt p

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

   178           val f = case p_ of

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

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

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

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

   183 		      val subte = Subst.input_to_terms sube

   184 		      val subst = Subst.T_from_string_eqs thy sube

   185 		      val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

   186 		    in

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

   188 		      then (*1*)

   189 		        let val f' = subst_atomic subst f

   190 		        in if f = f'

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

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

   193 		        end

   194 		      else (*2*)

   195 		        case Rewrite.rewrite_terms_ thy ro erls subte f of

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

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

   198 		    end

   199   | check  (Tactic.Apply_Assumption cts') _ =

   200     raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))

   201     (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)

   202   | check (Tactic.Take_Inst ct') _ =

   203     raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))

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

   205      if Pos.on_specification p_

   206      then

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

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

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

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

   211   | check (Tactic.End_Subproblem) _ =

   212     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)

   213   | check (Tactic.CAScmd ct') _ =

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

   215   | check (Tactic.Split_And) _ =

   216     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)

   217   | check (Tactic.Conclude_And) _ =

   218     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)

   219   | check (Tactic.Split_Or) _ =

   220     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)

   221   | check (Tactic.Conclude_Or) _ =

   222     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)

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

   224     let

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

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

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

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

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

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

   231     end

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

   233     if p_ = Pos.Res

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

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

   236   | check (Tactic.Begin_Sequ) _ =

   237     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))

   238   | check (Tactic.End_Sequ) _ =

   239     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))

   240   | check (Tactic.Split_Intersect) _ =

   241     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))

   242   | check (Tactic.End_Intersect) _ =

   243     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))

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

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

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

   247     else

   248       let

   249         val pp = Ctree.par_pblobj pt p;

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

   251         val thy = ThyC.get_theory thy'

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

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

   254         val (f, asm) = case p_ of

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

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

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

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

   259       in

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

   261       end

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

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

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

   265     else

   266       let

   267         val f = case p_ of

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

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

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

   271       in (let val ls = Prog_Expr.or2list f

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

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

   274       end

   275   | check Tactic.Collect_Trues _ =

   276     error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)

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

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

   279     let

   280       val pp = Ctree.par_pblobj pt p;

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

   282       val thy = ThyC.get_theory thy';

   283       val f = case p_ of

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

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

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

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

   288     in case id of

   289       "subproblem_equation_dummy" =>

   290   	  if TermC.is_expliceq f

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

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

   293     | "solve_equation_dummy" =>

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

   295   	  in

   296   	    if id' <> "subproblem_equation_dummy"

   297   	    then Applicable.No "no subproblem"

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

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

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

   301       end

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

   303     end

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

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

   306 (*-----^^^^^- solve ---------------------------------------------------------------------------*)

   310 (**)end(**);

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 01 May 2020 16:06:59 +0200
changeset 59922	9dbb624c2ec2
parent 59921	0766dade4a78
child 59923	cd730f07c9ac
permissions	-rw-r--r--