wneuper/isa: src/Tools/isac/Specify/generate.sml@caf3839e53c5

     1 (* Title: generate specific entries into Ctree

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     6 signature GENERATE_CALC_TREE =

     7 sig

     8   datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet

     9   datatype mout =

    10     EmptyMout

    11   | Error' of string

    12   | FormKF of TermC.as_string

    13   | PpcKF of pblmet * Model.item Model.ppc

    14   | RefinedKF of Problem.id * (Model.itm list * (bool * term) list)

    15   val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T

    16     -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree

    17   val init_istate : Tactic.input -> term -> Istate_Def.T

    18   val init_pbl : (string * (term * 'a)) list -> Model.itm list

    19   val init_pbl' : (string * (term * term)) list -> Model.itm list

    20   val embed_deriv : State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T

    21   val generate_hard :

    22     theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree

    23   val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->

    24     Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'

    25   val generate_inconsistent_rew : Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->

    26     Pos.pos' -> Ctree.ctree -> Calc.T

    27 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    28   val mout2str : mout -> string

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

    30   (* NONE *)

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

    32 end

    34 (**)

    35 structure Generate(**): GENERATE_CALC_TREE(**) =

    36 struct

    37 (**)

    38 open Ctree

    39 open Pos

    41 (* initialize istate for Detail_Set *)

    42 fun init_istate (Tactic.Rewrite_Set rls) t =

    43     let

    44       val thy = ThyC.get_theory "Isac_Knowledge"

    45       val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args

    46     in

    47       Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])

    48     end

    49   | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =

    50     let

    51       val thy = ThyC.get_theory "Isac_Knowledge"

    52       val rls' = assoc_rls rls

    53       val v = case Subst.T_from_input thy subs of

    54         (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)

    55       | _ => raise ERROR "init_istate: uncovered case"

    56       val prog = Auto_Prog.gen thy t rls'

    57       val args = Program.formal_args prog

    58     in

    59       Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))

    60     end

    61   | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.input_to_string tac)

    64 datatype pblmet =           (*%^%*)

    65   Upblmet                   (*undefined*)

    66 | Problem of Problem.id    (*%^%*)

    67 | Method of Method.id;    (*%^%*)

    68 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)

    69   | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)

    70   | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)

    72 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)

    73 datatype foppFK =                  (* in DG cases div 2 *)

    74   EmptyFoppFK         (*DG internal*)

    75 | FormFK of TermC.as_string

    76 | PpcFK of TermC.as_string Model.ppc

    77 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'

    78   | foppFK2str (PpcFK  ppc) ="PpcFK " ^ Model.ppc2str ppc

    79   | foppFK2str EmptyFoppFK  ="EmptyFoppFK"

    81 datatype nest = Open | Closed | Nundef;

    82 fun nest2str Open = "Open"

    83   | nest2str Closed = "Closed"

    84   | nest2str Nundef = "Nundef"

    86 type indent = int;

    87 datatype edit = EdUndef | Write | Protect;

    88                                    (* bridge --> kernel *)

    89                                    (* bridge <-> kernel *)

    90 (* needed in dialog.sml *)         (* bridge <-- kernel *)

    91 fun edit2str EdUndef = "EdUndef"

    92   | edit2str Write = "Write"

    93   | edit2str Protect = "Protect";

    95 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)

    96   Error_ of string                                                         (*<--*)

    97 | FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)

    98 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)

    99 | RefineKF of Stool.match list                                             (*<--*)

   100 | RefinedKF of (Problem.id * ((Model.itm list) * ((bool * term) list)))   (*<--*)

   102 (*

   103   datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout

   104 *)

   105 datatype mout =

   106   FormKF of TermC.as_string

   107 | PpcKF of (pblmet * Model.item Model.ppc)

   108 | RefinedKF of Problem.id * (Model.itm list * (bool * term) list)

   109 | Error' of string

   110 | EmptyMout

   112 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'

   113   | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"

   114   | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."

   115   | mout2str (Error'  str) = "Error' " ^ str

   116   | mout2str (EmptyMout    ) = "EmptyMout"

   118 (* init pbl with ...,dsc,empty | [] *)

   119 fun init_pbl pbt =

   120   let

   121     fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (TermC.empty, [])))

   122   in map pbt2itm pbt end

   124 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)

   125 fun init_pbl' pbt =

   126   let

   127     fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (TermC.empty, [])))

   128   in map pbt2itm pbt end

   129 (* generate 1 ppobj in Ctree *)

   130 fun generate1 (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =

   131     let

   132       val pt = update_pbl pt p itms

   133 	    val pt = update_met pt p met

   134     in

   135       (pos, [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

   136     end

   137   | generate1 (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =

   138     (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [][]),

   139        case p_ of

   140          Pbl => update_pbl pt p itmlist

   141 	     | Met => update_met pt p itmlist

   142        | _ => error ("uncovered case " ^ pos_2str p_))

   143     (* WN110515 probably declare_constraints with input item (without dsc) --

   144       -- important when specifying without formalisation *)

   145   | generate1 (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =

   146     (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] [])),

   147        case p_ of

   148          Pbl => update_pbl pt p itmlist

   149 	     | Met => update_met pt p itmlist

   150        | _ => error ("uncovered case " ^ pos_2str p_))

   151     (*WN110515 probably declare_constraints with input item (without dsc)*)

   152   | generate1 (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =

   153     (pos, [],  PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []),

   154        case p_ of

   155          Pbl => update_pbl pt p itmlist

   156 	     | Met => update_met pt p itmlist

   157        | _ => error ("uncovered case " ^ pos_2str p_))

   158   | generate1 (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =

   159     (pos, [] , PpcKF  (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []),

   160       update_domID pt p domID)

   161   | generate1 (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =

   162     let

   163       val pt = update_pbl pt p itms

   164       val pt = update_pblID pt p pI

   165     in

   166       ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

   167     end

   168   | generate1 (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =

   169     let

   170       val pt = update_oris pt p oris

   171       val pt = update_met pt p itms

   172       val pt = update_metID pt p mID

   173     in

   174       ((p, Met), [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

   175     end

   176   | generate1 (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =

   177     let

   178       val pt = update_pbl pt p pbl

   179       val pt = update_orispec pt p (domID, pIre, metID)

   180     in

   181       (pos, [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

   182     end

   183   | generate1 (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =

   184     let

   185       val (dI, _, mI) = get_obj g_spec pt p

   186       val pt = update_spec pt p (dI, pI, mI)

   187     in

   188       (pos, [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)

   189     end

   190   | generate1 (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =

   191     (case topt of

   192       SOME t =>

   193         let val (pt, c) = cappend_form pt p (is, ctxt) t

   194         in (pos, c, EmptyMout, pt) end

   195     | NONE => (pos, [], EmptyMout, pt))

   196   | generate1 (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)

   197     let

   198       val p =

   199         let val (ps, p') = split_last p (* no connex to prev.ppobj *)

   200 	      in if p' = 0 then ps @ [1] else p end

   201       val (pt, c) = cappend_form pt p l t

   202     in

   203       ((p, Frm): pos', c, FormKF (UnparseC.term t), pt)

   204     end

   205   | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =

   206     let

   207       val (pt, c) = cappend_form pt p l t

   208       val pt = update_branch pt p TransitiveB (*040312*)

   209       (* replace the old PrfOjb ~~~~~ *)

   210       val p = (lev_on o lev_dn (* starts with [...,0] *)) p

   211       val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*)

   212     in

   213       ((p, Frm), c @ c', FormKF (UnparseC.term t), pt)

   214     end

   215   | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Res)) =

   216     (*append after existing PrfObj    vvvvvvvvvvvvv*)

   217     generate1 (Tactic.Begin_Trans' t) l (pt, (lev_on p, Frm))

   218   | generate1 (Tactic.End_Trans' tasm) l (pt, (p, _)) =

   219     let

   220       val p' = lev_up p

   221       val (pt, c) = append_result pt p' l tasm Complete

   222     in

   223       ((p', Res), c, FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)

   224     end

   225   | generate1 (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   226     let

   227       val (pt, c) = cappend_atomic pt p (is, ctxt) f

   228         (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Complete;

   229       val pt = update_branch pt p TransitiveB

   230     in

   231       ((p, Res), c, FormKF (UnparseC.term f'), pt)

   232     end

   233  | generate1 (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   234    let

   235      val (pt, c) = cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Complete

   236      val pt = update_branch pt p TransitiveB

   237    in

   238     ((p, Res), c, FormKF (UnparseC.term f'), pt)

   239    end

   240   | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   241     let

   242       val (pt, c) = cappend_atomic pt p (is, ctxt) f

   243         (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Complete

   244       val pt = update_branch pt p TransitiveB

   245     in

   246       ((p, Res), c, FormKF (UnparseC.term f'), pt)

   247     end

   248   | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =

   249     let

   250       val (pt, c) = cappend_atomic pt p (is, ctxt) f

   251         (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Complete

   252       val pt = update_branch pt p TransitiveB

   253     in

   254       ((p, Res), c, FormKF (UnparseC.term f'), pt)

   255     end

   256   | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =

   257       let

   258         val (pt, c) = append_result pt p l (scval, []) Complete

   259       in

   260         ((p, Res), c, FormKF (UnparseC.term scval), pt)

   261       end

   262   | generate1 (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =

   263       let

   264         val (pt,c) = cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Complete

   265       in

   266         ((p, Res), c, FormKF (UnparseC.term f'), pt)

   267       end

   268   | generate1 (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =

   269       let

   270         val (pt,c) = cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Complete

   271       in

   272         ((p, Res), c, FormKF (UnparseC.term f'), pt)

   273       end

   274   | generate1 (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =

   275       let

   276         val (pt,c) = cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Complete

   277       in

   278         ((p, Res), c, FormKF (UnparseC.term list), pt)

   279       end

   280   | generate1 (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =

   281       let

   282         val (pt,c) =

   283           cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Complete

   284         in ((p, Res), c, FormKF (UnparseC.term t'), pt)

   285         end

   286   | generate1 (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =

   287       let

   288         val (pt, c) = cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Complete

   289       in

   290         ((p,Res), c, FormKF f', pt)

   291       end

   292   | generate1 (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))

   293       (l as (_, ctxt)) (pt, (p, _)) =

   294     let

   295 	    val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))

   296 	      (oris, (domID, pblID, metID), hdl, ctxt_specify)

   297 	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f

   298     in

   299       ((p, Pbl), c, FormKF f, pt)

   300     end

   301   | generate1 m' _ _ = error ("generate1: not impl.for " ^ Tactic.string_of m')

   303 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =

   304   let

   305     val f = get_curr_formula (pt, pos)

   306     val pos' as (p', _) = (lev_on p, Res)

   307     val (pt, _) = case subs_opt of

   308       NONE => cappend_atomic pt p' (is, ctxt) f

   309         (Tactic.Rewrite thm') (f', []) Inconsistent

   310     | SOME subs => cappend_atomic pt p' (is, ctxt) f

   311         (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent

   312     val pt = update_branch pt p' TransitiveB

   313   in (pt, pos') end

   315 fun generate_hard _(*thy*) m' (p,p_) pt =

   316   let

   317     val p = case p_ of

   318       Frm => p | Res => lev_on p

   319     | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))

   320   in

   321     generate1 m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))

   322   end

   324 (* tacis are in reverse order from do_next/specify_: last = fst to insert *)

   325 fun generate ([]: State_Steps.T) ptp = ptp

   326   | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*)) =

   327     let

   328       val (tacis', (_, tac_, (p, is))) = split_last tacis

   329 	    val (p',c',_,pt') = generate1 tac_ is (pt, p)

   330     in

   331       generate tacis' (pt', c@c', p')

   332     end

   334 (* embed the tacis created by a '_deriv'ation; sys.form <> input.form

   335   tacis are in order, thus are reverted for generate *)

   336 fun embed_deriv tacis (pt, pos as (p, Frm)) =

   337   (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402

   338     and transfer the istate (from _after_ compare_deriv) from Frm to Res*)

   339     let

   340       val (res, asm) = (State_Steps.result o last_elem) tacis

   341     	val (ist, ctxt) = case get_obj g_loc pt p of

   342     	  (SOME (ist, ctxt), _) => (ist, ctxt)

   343       | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"

   344     	val form = get_obj g_form pt p

   345       (*val p = lev_on p; ---------------only difference to (..,Res) below*)

   346     	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::

   347     		(State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),

   348     			(pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]

   349     	val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))

   350     	val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))

   351     	val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))

   352     	val pt = update_branch pt p TransitiveB

   353     in (c, (pt, pos: pos')) end

   354   | embed_deriv tacis (pt, (p, Res)) =

   355     (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?

   356       and transfer the istate (from _after_ compare_deriv) from Res to new Res*)

   357     let val (res, asm) = (State_Steps.result o last_elem) tacis

   358     	val (ist, ctxt) = case get_obj g_loc pt p of

   359     	  (_, SOME (ist, ctxt)) => (ist, ctxt)

   360       | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"

   361     	val (f, _) = get_obj g_result pt p

   362     	val p = lev_on p(*---------------only difference to (..,Frm) above*);

   363     	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate_Def.Uistate, ctxt))) ::

   364     		(State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),

   365     			(pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];

   366     	val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))

   367     	val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))

   368     	val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))

   369     	val pt = update_branch pt p TransitiveB

   370     in (c, (pt, pos)) end

   371   | embed_deriv _ _ = error "embed_deriv: uncovered definition"

   372 end

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 02 May 2020 10:57:04 +0200
changeset 59925	caf3839e53c5
parent 59912	dc53f7815edc
child 59931	cc5b51681c4b
permissions	-rw-r--r--