Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/solve-step.sml
changeset 60592 777d05447375
parent 60586 007ef64dbb08
child 60611 a25716353782
equal deleted inserted replaced
60590:35846e25713e 60592:777d05447375 
    19   val get_ruleset: 'a -> Pos.pos' -> Ctree.ctree ->
 
    19   val get_ruleset: 'a -> Pos.pos' -> Ctree.ctree ->
 
    20     string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
 
    20     string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
 
    21   val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
 
    21   val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml
 
    22 
    22 
    23 \<^isac_test>\<open>
 
    23 \<^isac_test>\<open>
 
    24   val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context
 
       
    25   val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
 
    24   val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list
 
    26 \<close>
 
    25 \<close>
 
    27 end
 
    26 end
 
    28 
    27 
    29 (**)
 
    28 (**)
 
   237 		        SOME (f', _) =>  Applicable.Yes (Tactic.Substitute' (ro, asm_rls, subte, f, f'))
 
   236 		        SOME (f', _) =>  Applicable.Yes (Tactic.Substitute' (ro, asm_rls, subte, f, f'))
 
   238 		      | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
 
   237 		      | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
 
   239 		  end
 
   238 		  end
 
   240   | check (Tactic.Tac id) (cs as (pt, pos)) =
 
   239   | check (Tactic.Tac id) (cs as (pt, pos)) =
 
   241       let 
   240       let 
   242         val thy = (Ctree.get_loc pt pos |> snd) |> Proof_Context.theory_of
 
   241         val ctxt = Ctree.get_ctxt pt pos
 
   243         val f = Calc.current_formula cs;
 
   242         val thy = ctxt |> Proof_Context.theory_of
 
   244       in
 
   243         val f = Calc.current_formula cs;
 
   245         Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
 
   244         val f' = UnparseC.term_in_ctxt ctxt f
 
       
   245       in
 
       
   246         Applicable.Yes (Tactic.Tac_ (thy, f', id, f'))
 
   246       end
 
   247       end
 
   247   | check (Tactic.Take str) (pt, pos) =
 
   248   | check (Tactic.Take str) (pt, pos) =
 
   248     let
 
   249     let
 
   249       val ctxt = (*Solve_Step.*)get_ctxt pt pos
 
   250       val ctxt = (*Solve_Step.*)get_ctxt pt pos
 
   250       val t = Prog_Tac.Take_adapt_to_type ctxt str
 
   251       val t = Prog_Tac.Take_adapt_to_type ctxt str
 
   265     (case topt of 
   266     (case topt of 
   266       SOME t => 
   267       SOME t => 
   267         let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
 
   268         let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
 
   268         in (pos, c, Test_Out.EmptyMout, pt) end
 
   269         in (pos, c, Test_Out.EmptyMout, pt) end
 
   269     | NONE => (pos, [], Test_Out.EmptyMout, pt))
 
   270     | NONE => (pos, [], Test_Out.EmptyMout, pt))
 
   270   | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
 
   271   | add (Tactic.Take' t) (l as (_, ctxt)) (pt, (p, _)) = (* val (Take' t) = m; *)
 
   271     let
 
   272     let
 
   272       val p =
 
   273       val p =
 
   273         let val (ps, p') = split_last p (* no connex to prev.ppobj *)
 
   274         let val (ps, p') = split_last p (* no connex to prev.ppobj *)
 
   274 	      in if p' = 0 then ps @ [1] else p end
 
   275 	      in if p' = 0 then ps @ [1] else p end
 
   275       val (pt, c) = Ctree.cappend_form pt p l t
 
   276       val (pt, c) = Ctree.cappend_form pt p l t
 
   276     in
 
   277     in
 
   277       ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt)
 
   278       ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
 
   278     end
 
   279     end
 
   279   | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
 
   280   | add (Tactic.Begin_Trans' t) (l as (_, ctxt)) (pt, (p, Pos.Frm)) =
 
   280     let
 
   281     let
 
   281       val (pt, c) = Ctree.cappend_form pt p l t
 
   282       val (pt, c) = Ctree.cappend_form pt p l t
 
   282       val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
 
   283       val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
 
   283       (* replace the old PrfOjb ~~~~~ *)
 
   284       (* replace the old PrfOjb ~~~~~ *)
 
   284       val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
 
   285       val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
 
   285       val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
 
   286       val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
 
   286     in
 
   287     in
 
   287       ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
 
   288       ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt)
 
   288     end
 
   289     end
 
   289   | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) = 
   290   | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) = 
   290     (*append after existing PrfObj    vvvvvvvvvvvvv*)
 
   291     (*append after existing PrfObj    vvvvvvvvvvvvv*)
 
   291     add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
 
   292     add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
 
   292   | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
 
   293   | add (Tactic.End_Trans' tasm) (l as (_, ctxt)) (pt, (p, _)) =
 
   293     let
 
   294     let
 
   294       val p' = Pos.lev_up p
 
   295       val p' = Pos.lev_up p
 
   295       val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
 
   296       val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
 
   296     in
 
   297     in
 
   297       ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
 
   298       ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*UnparseC.term_in_ctxt ctxt t*), pt)
 
   298     end
 
   299     end
 
   299   | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   300   | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   300     let
 
   301     let
 
   301       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
 
   302       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
 
   302         (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
 
   303         (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
 
   303       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   304       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   304     in
 
   305     in
 
   305       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   306       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   306     end
 
   307     end
 
   307  | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   308  | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   308    let
 
   309    let
 
   309      val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
 
   310      val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
 
   310      val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   311      val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   311    in
 
   312    in
 
   312     ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   313     ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   313    end
 
   314    end
 
   314   | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   315   | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   315     let
 
   316     let
 
   316       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 
   317       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 
   317         (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
 
   318         (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
 
   318       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   319       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   319     in
 
   320     in
 
   320       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   321       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   321     end
 
   322     end
 
   322   | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   323   | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 
   323     let
 
   324     let
 
   324       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 
   325       val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f 
   325         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
 
   326         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
 
   326       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   327       val pt = Ctree.update_branch pt p Ctree.TransitiveB
 
   327     in
 
   328     in
 
   328       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   329       ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   329     end
 
   330     end
 
   330   | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
 
   331   | add (Tactic.Check_Postcond' (_, scval)) (l as (_, ctxt)) (pt, (p, _)) =
 
   331       let
 
   332       let
 
   332         val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
 
   333         val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
 
   333       in
 
   334       in
 
   334         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt)
 
   335         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt scval), pt)
 
   335       end
 
   336       end
 
   336   | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
 
   337   | add (Tactic.Calculate' (_, op_, f, (f', _))) (l as (_, ctxt)) (pt, (p, _)) =
 
   337       let
 
   338       let
 
   338         val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
 
   339         val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
 
   339       in
 
   340       in
 
   340         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   341         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   341       end
 
   342       end
 
   342   | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
 
   343   | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) (l as (_, ctxt)) (pt, (p, _)) =
 
   343       let
 
   344       let
 
   344         val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
 
   345         val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
 
   345       in
 
   346       in
 
   346         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 
   347         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt f'), pt)
 
   347       end
 
   348       end
 
   348   | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
 
   349   | add (Tactic.Or_to_List' (ors, list)) (l as (_, ctxt)) (pt, (p, _)) =
 
   349       let
 
   350       let
 
   350         val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
 
   351         val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
 
   351       in
 
   352       in
 
   352         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt)
 
   353         ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt list), pt)
 
   353       end
 
   354       end
 
   354   | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
 
   355   | add (Tactic.Substitute' (_, _, subte, t, t')) (l as (_, ctxt)) (pt, (p, _)) =
 
   355       let
 
   356       let
 
   356         val (pt,c) =
 
   357         val (pt,c) =
 
   357           Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
 
   358           Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
 
   358         in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) 
   359         in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t'), pt) 
   359         end
 
   360         end
 
   360   | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
 
   361   | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) =
 
   361       let
 
   362       let
 
   362         val ctxt = Ctree.get_ctxt pt pos
 
   363         val ctxt = Ctree.get_ctxt pt pos
 
   363         val (pt, c) = Ctree.cappend_atomic pt p l
 
   364         val (pt, c) = Ctree.cappend_atomic pt p l
wneuper/isa