wneuper@59276: (* Title: generate specific entries into Ctree wneuper@59276: Author: Walther Neuper wneuper@59276: (c) due to copyright terms wneuper@59276: *) wneuper@59276: wneuper@59271: signature GENERATE_CALC_TREE = wneuper@59276: sig wneuper@59276: (* vvv request into signature is incremental with *.sml *) wneuper@59276: (* for calchead.sml --------------------------------------------------------------- vvv *) wneuper@59266: type taci wneuper@59266: val e_taci : taci wneuper@59266: datatype pblmet = Method of metID | Problem of pblID | Upblmet wneuper@59268: datatype mout = wneuper@59268: EmptyMout wneuper@59268: | Error' of string wneuper@59268: | FormKF of cterm' wneuper@59268: | PpcKF of pblmet * item ppc wneuper@59267: | RefinedKF of pblID * (itm list * (bool * term) list) wneuper@59276: val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context -> wneuper@59279: Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *) wneuper@59276: val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *) wneuper@59266: val init_pbl : (string * (term * 'a)) list -> itm list wneuper@59266: val init_pbl' : (string * (term * term)) list -> itm list wneuper@59279: val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *) wneuper@59268: val generate_hard : (* for solve.sml *) wneuper@59279: theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree wneuper@59276: val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list -> wneuper@59279: Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *) wneuper@59276: val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context -> wneuper@59279: Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *) wneuper@59266: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59266: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59266: end neuper@37906: wneuper@59266: (**) wneuper@59271: structure Generate(**): GENERATE_CALC_TREE(**) = wneuper@59266: (**) wneuper@59266: struct wneuper@59276: open Ctree wneuper@59266: (* initialize istate for Detail_Set *) neuper@37906: fun init_istate (Rewrite_Set rls) t = neuper@37906: (case assoc_rls rls of wneuper@59266: Rrls {scr = Rfuns {init_state = ii, ...}, ...} => RrlsState (ii t) wneuper@59266: | Rls {scr = EmptyScr, ...} => wneuper@59266: error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ wneuper@59266: "use prep_rls' for storing rule-sets !") wneuper@59266: | Rls {scr = Prog s, ...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) wneuper@59266: | Seq {scr=EmptyScr,...} => wneuper@59266: error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^ wneuper@59266: "use prep_rls' for storing rule-sets !") wneuper@59266: | Seq {scr = Prog s,...} => (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) wneuper@59266: | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls") neuper@37906: | init_istate (Rewrite_Set_Inst (subs, rls)) t = wneuper@59266: let wneuper@59266: val v = case subs2subst (assoc_thy "Isac") subs of wneuper@59266: (_, v) :: _ => v wneuper@59266: | _ => error "init_istate: uncovered case " neuper@37906: (*...we suppose the substitution of only _one_ bound variable*) neuper@37906: in case assoc_rls rls of wneuper@59266: Rls {scr = EmptyScr, ...} => wneuper@59266: error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ wneuper@59266: "use prep_rls' for storing rule-sets !") wneuper@59266: | Rls {scr = Prog s, ...} => wneuper@59266: let val (form, bdv) = two_scr_arg s wneuper@59266: in (ScrState ([(form, t), (bdv, v)], [], NONE, e_term, Sundef,true)) wneuper@59266: end wneuper@59266: | Seq {scr = EmptyScr, ...} => wneuper@59266: error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^ wneuper@59266: "use prep_rls' for storing rule-sets !") wneuper@59266: | Seq {scr = Prog s,...} => wneuper@59266: let val (form, bdv) = two_scr_arg s wneuper@59266: in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) wneuper@59266: end wneuper@59266: | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls" wneuper@59266: end wneuper@59266: | init_istate tac _ = error ("init_istate: uncovered definition for " ^ tac2str tac) neuper@37906: wneuper@59266: (* a taci holds alle information required to build a node in the calc-tree; neuper@37906: a taci is assumed to be used efficiently such that the calc-tree neuper@37906: resulting from applying a taci need not be stored separately; wneuper@59266: see "type calcstate" *) neuper@37906: (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate" neuper@37906: TODO.WN0512 ? redesign this _list_: neuper@37906: # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs neuper@37906: # the latter problem may be resolved automatically if "fun autocalc" is neuper@37906: not any more used for the specify-phase and for changing the phases*) neuper@37906: type taci = wneuper@59266: (tac * (* for comparison with input tac *) wneuper@59279: tac_ * (* for ctree generation *) wneuper@59279: (pos' * (* after applying tac_, for ctree generation *) wneuper@59279: (istate * Proof.context))) (* after applying tac_, for ctree generation *) wneuper@59266: val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci bonzai@41948: fun taci2str ((tac, tac_, (pos', (istate, _))):taci) = wneuper@59266: "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^ wneuper@59266: istate2str istate ^ " ))" wneuper@59266: fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis neuper@37906: wneuper@59266: datatype pblmet = (*%^%*) wneuper@59266: Upblmet (*undefined*) wneuper@59266: | Problem of pblID (*%^%*) wneuper@59266: | Method of metID; (*%^%*) wneuper@59266: fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*) wneuper@59266: | pblmet2str (Method metID) = "Method " ^ metID2str metID (*%^%*) wneuper@59266: | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x) neuper@37906: neuper@37906: (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*) neuper@37906: datatype foppFK = (* in DG cases div 2 *) neuper@37906: EmptyFoppFK (*DG internal*) neuper@37906: | FormFK of cterm' wneuper@59266: | PpcFK of cterm' ppc wneuper@59266: fun foppFK2str (FormFK ct') ="FormFK " ^ ct' wneuper@59266: | foppFK2str (PpcFK ppc) ="PpcFK " ^ ppc2str ppc wneuper@59266: | foppFK2str EmptyFoppFK ="EmptyFoppFK" neuper@37906: neuper@37906: datatype nest = Open | Closed | Nundef; neuper@37906: fun nest2str Open = "Open" neuper@37906: | nest2str Closed = "Closed" wneuper@59266: | nest2str Nundef = "Nundef" neuper@37906: neuper@37906: type indent = int; neuper@37906: datatype edit = EdUndef | Write | Protect; neuper@37906: (* bridge --> kernel *) neuper@37906: (* bridge <-> kernel *) neuper@37906: (* needed in dialog.sml *) (* bridge <-- kernel *) neuper@37906: fun edit2str EdUndef = "EdUndef" neuper@37906: | edit2str Write = "Write" neuper@37906: | edit2str Protect = "Protect"; neuper@37906: neuper@42023: datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*) wneuper@59266: Error_ of string (*<--*) neuper@37906: | FormKF of cellID * edit * indent * nest * cterm' (*<--*) neuper@37906: | PpcKF of cellID * edit * indent * nest * (pblmet * item ppc) (*<--*) neuper@37906: | RefineKF of match list (*<--*) wneuper@59266: | RefinedKF of (pblID * ((itm list) * ((bool * term) list))) (*<--*) neuper@37906: neuper@37906: fun inout2str End_Proof = "End_Proof" neuper@37906: | inout2str (Error_ s) = "Error_ "^s neuper@37906: | inout2str (FormKF (cellID, edit, indent, nest, ct')) = neuper@37906: "FormKF ("^(string_of_int cellID)^"," neuper@37906: ^(edit2str edit)^","^(string_of_int indent)^"," neuper@37906: ^(nest2str nest)^",(" neuper@37906: ^ct' ^")" neuper@37906: | inout2str (PpcKF (cellID, edit, indent, nest, (pm,itemppc))) = neuper@37906: "PpcKF ("^(string_of_int cellID)^"," neuper@37906: ^(edit2str edit)^","^(string_of_int indent)^"," neuper@37906: ^(nest2str nest)^",(" neuper@37906: ^(pblmet2str pm)^","^(itemppc2str itemppc)^"))" neuper@37906: | inout2str (RefineKF ms) = "RefineKF "^(matchs2str ms) wneuper@59266: | inout2str _ = error "inout2str: uncovered definition" wneuper@59266: fun inouts2str ios = (strs2str' o (map inout2str)) ios neuper@37906: wneuper@59267: (* wneuper@59267: datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout wneuper@59267: *) neuper@37906: datatype mout = wneuper@59267: FormKF of cterm' wneuper@59267: | PpcKF of (pblmet * item ppc) wneuper@59267: | RefinedKF of pblID * (itm list * (bool * term) list) wneuper@59267: | Error' of string wneuper@59267: | EmptyMout neuper@37906: wneuper@59267: fun mout2str (FormKF cterm') = "FormKF " ^ cterm' wneuper@59267: | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ itemppc2str itemppc ^ ")" wneuper@59267: | mout2str (RefinedKF (pblID, ls)) = "mout2str: RefinedKF not impl." wneuper@59267: | mout2str (Error' str) = "Error' " ^ str wneuper@59267: | mout2str (EmptyMout ) = "EmptyMout" neuper@37906: neuper@37906: (* init pbl with ...,dsc,empty | [] *) neuper@37906: fun init_pbl pbt = wneuper@59266: let wneuper@59266: fun pbt2itm (f, (d, _)) = ((0, [], false, f, Inc ((d, []), (e_term, []))) : itm) wneuper@59266: in map pbt2itm pbt end wneuper@59266: wneuper@59266: (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *) neuper@37906: fun init_pbl' pbt = neuper@37906: let wneuper@59266: fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm) wneuper@59266: in map pbt2itm pbt end neuper@37906: wneuper@59279: (*generate 1 ppobj in ctree*) neuper@37906: (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) wneuper@59266: fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = wneuper@59269: (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]), wneuper@59266: case p_ of wneuper@59266: Pbl => update_pbl pt p itmlist wneuper@59266: | Met => update_met pt p itmlist wneuper@59266: | _ => error ("uncovered case " ^ pos_2str p_)) wneuper@59266: (* WN110515 probably declare_constraints with input item (without dsc) -- wneuper@59266: -- important when specifying without formalisation *) wneuper@59266: | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt = wneuper@59269: (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc thy [] [])), wneuper@59266: case p_ of wneuper@59266: Pbl => update_pbl pt p itmlist wneuper@59266: | Met => update_met pt p itmlist wneuper@59266: | _ => error ("uncovered case " ^ pos_2str p_)) neuper@41994: (*WN110515 probably declare_constraints with input item (without dsc)*) wneuper@59266: | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt = wneuper@59269: (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), wneuper@59266: case p_ of wneuper@59266: Pbl => update_pbl pt p itmlist wneuper@59266: | Met => update_met pt p itmlist wneuper@59266: | _ => error ("uncovered case " ^ pos_2str p_)) bonzai@41948: | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt = wneuper@59269: (pos, [] , PpcKF (Upblmet, Specify.itms2itemppc thy [] []), wneuper@59266: update_domID pt p domID) wneuper@59266: | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt = wneuper@59266: let wneuper@59266: val pt = update_pbl pt p itms wneuper@59266: val pt = update_pblID pt p pI wneuper@59266: in wneuper@59269: ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt = wneuper@59266: let wneuper@59266: val pt = update_oris pt p oris wneuper@59266: val pt = update_met pt p itms wneuper@59266: val pt = update_metID pt p mID wneuper@59266: in wneuper@59269: ((p, Met), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) wneuper@59266: end bonzai@41948: | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt = wneuper@59266: let wneuper@59266: val pt = update_pbl pt p itms wneuper@59266: val pt = update_met pt p met wneuper@59266: in wneuper@59269: (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) neuper@37906: end wneuper@59266: | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt = wneuper@59266: let wneuper@59266: val pt = update_pbl pt p pbl wneuper@59266: val pt = update_orispec pt p (domID, pIre, metID) wneuper@59266: in wneuper@59269: (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt = wneuper@59266: let wneuper@59266: val (dI, _, mI) = get_obj g_spec pt p wneuper@59266: val pt = update_spec pt p (dI, pI, mI) wneuper@59266: in wneuper@59269: (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt = wneuper@59266: (case topt of wneuper@59266: SOME t => wneuper@59266: let val (pt, c) = cappend_form pt p (is, ctxt) t wneuper@59266: in (pos, c, EmptyMout, pt) end wneuper@59266: | NONE => (pos, [], EmptyMout, update_env pt p (SOME (is, ctxt)))) wneuper@59266: | generate1 _ (Take' t) l (p, _) pt = (* val (Take' t) = m; *) wneuper@59266: let wneuper@59266: val p = wneuper@59266: let val (ps, p') = split_last p (* no connex to prev.ppobj *) wneuper@59266: in if p' = 0 then ps @ [1] else p end wneuper@59266: val (pt, c) = cappend_form pt p l t wneuper@59266: in wneuper@59267: ((p, Frm): pos', c, FormKF (term2str t), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Begin_Trans' t) l (p, Frm) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_form pt p l t neuper@37906: val pt = update_branch pt p TransitiveB (*040312*) wneuper@59266: (* replace the old PrfOjb ~~~~~ *) wneuper@59266: val p = (lev_on o lev_dn (* starts with [...,0] *)) p wneuper@59266: val (pt, c') = cappend_form pt p l t (*FIXME.0402 same istate ???*) wneuper@59266: in wneuper@59267: ((p, Frm), c @ c', FormKF (term2str t), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Begin_Trans' t) l (p, Res) pt = wneuper@59266: (*append after existing PrfObj vvvvvvvvvvvvv*) wneuper@59266: generate1 thy (Begin_Trans' t) l (lev_on p, Frm) pt wneuper@59266: | generate1 _ (End_Trans' tasm) l (p, _) pt = wneuper@59266: let wneuper@59266: val p' = lev_up p wneuper@59266: val (pt, c) = append_result pt p' l tasm Complete wneuper@59266: in wneuper@59267: ((p', Res), c, FormKF (term2str t), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f wneuper@59266: (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete; wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59267: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59267: end wneuper@59266: | generate1 _ (Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f wneuper@59266: (Rewrite thm') (f', asm) Complete wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt wneuper@59266: | generate1 _ (Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f wneuper@59266: (Rewrite_Set_Inst (subst2subs subs', id_rls rls')) (f', asm) Complete wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val ctxt' = insert_assumptions asm ctxt wneuper@59266: val (pt, _) = cappend_form pt p (is, ctxt') f wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f wneuper@59266: val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt') wneuper@59266: val pos' = ((lev_on o lev_dn) p, Frm) wneuper@59266: in wneuper@59266: generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*) wneuper@59266: end wneuper@59266: | generate1 _ (Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f wneuper@59266: (Rewrite_Set (id_rls rls')) (f',asm) Complete wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59266: end wneuper@59266: | generate1 thy (Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt = wneuper@59266: let wneuper@59266: val ctxt' = insert_assumptions asm ctxt wneuper@59266: val (pt, _) = cappend_form pt p (is, ctxt') f wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: val is = init_istate (Rewrite_Set (id_rls rls)) f wneuper@59266: val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt') wneuper@59266: val pos' = ((lev_on o lev_dn) p, Frm) wneuper@59266: in wneuper@59266: generate1 thy tac_ (is, ctxt') pos' pt (*implicit Take*) wneuper@59266: end wneuper@59266: | generate1 _ (Check_Postcond' (_, (scval, asm))) l (p, _) pt = neuper@42394: let wneuper@59266: val (pt, c) = append_result pt p l (scval, asm) Complete wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str scval), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Calculate' (_, op_, f, (f', _))) l (p, _) pt = neuper@42394: let wneuper@59266: val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f', []) Complete wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Check_elementwise' (consts, pred, (f', asm))) l (p, _) pt = neuper@42394: let wneuper@59266: val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str f'), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Or_to_List' (ors, list)) l (p, _) pt = neuper@42394: let wneuper@59266: val (pt,c) = cappend_atomic pt p l ors Or_to_List (list, []) Complete wneuper@59266: in wneuper@59267: ((p, Res), c, FormKF (term2str list), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Substitute' (_, _, subte, t, t')) l (p, _) pt = neuper@41983: let neuper@41983: val (pt,c) = wneuper@59266: cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete wneuper@59267: in ((p, Res), c, FormKF (term2str t'), pt) wneuper@59266: end wneuper@59266: | generate1 _ (Tac_ (_, f, id, f')) l (p, _) pt = neuper@42394: let wneuper@59266: val (pt, c) = cappend_atomic pt p l (str2term f) (Tac id) (str2term f', []) Complete wneuper@59266: in wneuper@59267: ((p,Res), c, FormKF f', pt) wneuper@59266: end wneuper@59266: | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p, _) pt = wneuper@59266: let wneuper@59266: val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl) wneuper@59266: val pt = update_ctxt pt p ctxt wneuper@59266: val f = Syntax.string_of_term (thy2ctxt thy) f wneuper@59266: in wneuper@59267: ((p, Pbl), c, FormKF f, pt) wneuper@59266: end wneuper@59266: | generate1 _ m' _ _ _ = error ("generate1: not impl.for " ^ tac_2str m') bonzai@41951: neuper@42437: fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt = neuper@42434: let wneuper@59266: val f = get_curr_formula (pt, pos) wneuper@59266: val pos' as (p', _) = (lev_on p, Res) wneuper@59266: val (pt, _) = case subs_opt of wneuper@59266: NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f wneuper@59266: (Rewrite thm') (f', []) Inconsistent wneuper@59266: | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f wneuper@59266: (Rewrite_Inst (subs, thm')) (f', []) Inconsistent wneuper@59266: val pt = update_branch pt p' TransitiveB neuper@42437: in (pt, pos') end neuper@42432: neuper@37906: fun generate_hard thy m' (p,p_) pt = neuper@37906: let wneuper@59266: val p = case p_ of wneuper@59266: Frm => p | Res => lev_on p wneuper@59266: | _ => error ("generate_hard: call by " ^ pos'2str (p,p_)) wneuper@59266: in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end neuper@37906: wneuper@59266: (* tacis are in reverse order from nxt_solve_/specify_: last = fst to insert *) neuper@37906: fun generate ([]: taci list) ptp = ptp wneuper@59266: | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))= wneuper@59266: let wneuper@59266: val (tacis', (_, tac_, (p, is))) = split_last tacis wneuper@59266: val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt wneuper@59266: in wneuper@59266: generate tacis' (pt', c@c', p') wneuper@59266: end neuper@37906: wneuper@59266: (* update pos in tacis for embedding by generate *) wneuper@59266: fun insert_pos (_: pos) [] = [] wneuper@59266: | insert_pos (p: pos) (((tac, tac_, (_, ist)): taci) :: tacis) = wneuper@59266: ((tac, tac_, ((p, Res), ist)): taci) :: (insert_pos (lev_on p) tacis) neuper@37906: wneuper@59266: fun res_from_taci (_, Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm) wneuper@59266: | res_from_taci (_, Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm) wneuper@59266: | res_from_taci (_, tac_, _) = error ("res_from_taci: called with" ^ tac_2str tac_) neuper@37906: wneuper@59266: (* embed the tacis created by a '_deriv'ation; sys.form <> input.form wneuper@59266: tacis are in order, thus are reverted for generate *) wneuper@59266: fun embed_deriv (tacis: taci list) (pt, pos as (p, Frm): pos') = neuper@37906: (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402 neuper@37906: and transfer the istate (from _after_ compare_deriv) from Frm to Res*) wneuper@59266: let wneuper@59266: val (res, asm) = (res_from_taci o last_elem) tacis wneuper@59266: val (ist, ctxt) = case get_obj g_loc pt p of wneuper@59266: (SOME (ist, ctxt), _) => (ist, ctxt) wneuper@59266: | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj" wneuper@59266: val form = get_obj g_form pt p wneuper@59266: (*val p = lev_on p; ---------------only difference to (..,Res) below*) wneuper@59266: val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) :: wneuper@59266: (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), wneuper@59266: (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))] wneuper@59269: val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p)) wneuper@59266: val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) wneuper@59266: val pt = update_tac pt p (Derive (id_rls nrls)) wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: in (c, (pt, pos: pos')) end wneuper@59266: | embed_deriv tacis (pt, (p, Res)) = wneuper@59266: (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ? wneuper@59266: and transfer the istate (from _after_ compare_deriv) from Res to new Res*) neuper@37906: let val (res, asm) = (res_from_taci o last_elem) tacis wneuper@59266: val (ist, ctxt) = case get_obj g_loc pt p of wneuper@59266: (_, SOME (ist, ctxt)) => (ist, ctxt) wneuper@59266: | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj" wneuper@59266: val (f, _) = get_obj g_result pt p wneuper@59266: val p = lev_on p(*---------------only difference to (..,Frm) above*); wneuper@59266: val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) :: wneuper@59266: (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm), wneuper@59266: (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]; wneuper@59269: val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p)) wneuper@59266: val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res)) wneuper@59266: val pt = update_tac pt p (Derive (id_rls nrls)) wneuper@59266: val pt = update_branch pt p TransitiveB wneuper@59266: in (c, (pt, pos)) end wneuper@59266: | embed_deriv _ _ = error "embed_deriv: uncovered definition" wneuper@59266: end