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

     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 (*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)

    24 fun check (Tactic.Check_Postcond pI) (_, (p, p_)) =

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

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

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

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

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

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

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

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

    33     else

    34       let

    35         val pp = Ctree.par_pblobj pt p;

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

    37         val thy = ThyC.get_theory thy';

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

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

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

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

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

    43       in

    44         let

    45           val subst = Subst.T_from_input thy subs;

    46         in

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

    48             SOME (f',asm) =>

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

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

    51         end

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

    53       end

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

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

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

    57     else

    58       let

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

    60         val thy = ThyC.get_theory thy';

    61         val f = case p_ of

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

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

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

    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 (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) =

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

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

    76     else

    77       let

    78         val pp = Ctree.par_pblobj pt p;

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

    80         val thy = ThyC.get_theory thy';

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

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

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

    84         val subst = Subst.T_from_input thy subs

    85       in

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

    87           SOME (f', asm)

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

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

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

    91       end

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

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

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

    95     else

    96       let

    97         val pp = Ctree.par_pblobj pt p;

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

    99         val thy = ThyC.get_theory thy';

   100         val (f, _) = case p_ of

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

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

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

   104     	  val subst = Subst.T_from_input thy subs;

   105       in

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

   107           SOME (f',asm)

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

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

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

   111       end

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

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

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

   115     else

   116       let

   117         val pp = Ctree.par_pblobj pt p;

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

   119         val (f, _) = case p_ of

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

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

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

   123       in

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

   125           SOME (f', asm)

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

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

   128       end

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

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

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

   132     else

   133     	let

   134     	  val pp = Ctree.par_pblobj pt p

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

   136     	  val f = case p_ of

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

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

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

   140     	in

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

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

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

   144     	end

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

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

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

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

   149     else

   150       let

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

   152         val f = case p_ of

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

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

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

   156       in

   157         if msg = "OK"

   158         then

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

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

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

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

   163         else Applicable.No msg

   164       end

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

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

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

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

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

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

   171       else

   172         let

   173           val pp = Ctree.par_pblobj pt p

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

   175           val f = case p_ of

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

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

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

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

   180 		      val subte = Subst.input_to_terms sube

   181 		      val subst = Subst.T_from_string_eqs thy sube

   182 		      val ro = Rewrite_Ord.assoc_rew_ord rew_ord'

   183 		    in

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

   185 		      then (*1*)

   186 		        let val f' = subst_atomic subst f

   187 		        in if f = f'

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

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

   190 		        end

   191 		      else (*2*)

   192 		        case Rewrite.rewrite_terms_ thy ro erls subte f of

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

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

   195 		    end

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

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

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

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

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

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

   202      if Pos.on_specification p_

   203      then

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

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

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

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

   208   | check (Tactic.End_Subproblem) _ =

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

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

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

   212   | check (Tactic.Split_And) _ =

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

   214   | check (Tactic.Conclude_And) _ =

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

   216   | check (Tactic.Split_Or) _ =

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

   218   | check (Tactic.Conclude_Or) _ =

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

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

   221     let

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

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

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

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

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

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

   228     end

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

   230     if p_ = Pos.Res

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

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

   233   | check (Tactic.Begin_Sequ) _ =

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

   235   | check (Tactic.End_Sequ) _ =

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

   237   | check (Tactic.Split_Intersect) _ =

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

   239   | check (Tactic.End_Intersect) _ =

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

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

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

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

   244     else

   245       let

   246         val pp = Ctree.par_pblobj pt p;

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

   248         val thy = ThyC.get_theory thy'

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

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

   251         val (f, asm) = case p_ of

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

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

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

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

   256       in

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

   258       end

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

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

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

   262     else

   263       let

   264         val f = case p_ of

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

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

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

   268       in (let val ls = Prog_Expr.or2list f

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

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

   271       end

   272   | check Tactic.Collect_Trues _ =

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

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

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

   276     let

   277       val pp = Ctree.par_pblobj pt p;

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

   279       val thy = ThyC.get_theory thy';

   280       val f = case p_ of

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

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

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

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

   285     in case id of

   286       "subproblem_equation_dummy" =>

   287   	  if TermC.is_expliceq f

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

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

   290     | "solve_equation_dummy" =>

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

   292   	  in

   293   	    if id' <> "subproblem_equation_dummy"

   294   	    then Applicable.No "no subproblem"

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

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

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

   298       end

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

   300     end

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

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

   303 (*-----^^^^^- solve ---------------------------------------------------------------------------*)

   307 (**)end(**);

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 01 May 2020 15:28:40 +0200
changeset 59921	0766dade4a78
parent 59920	33913fe24685
child 59922	9dbb624c2ec2
permissions	-rw-r--r--