1.1 --- a/src/Tools/isac/Interpret/derive.sml	Sat May 02 17:39:04 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Mon May 04 09:25:51 2020 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4  (*val concat_deriv *)
     1.5    val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
     1.6      bool * der list
     1.7 +  val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
     1.8  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.9    (*  NONE *)
    1.10  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.11 @@ -141,4 +142,44 @@
    1.12        else (false, [])
    1.13    end
    1.14  
    1.15 +(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
    1.16 +  tacis are in order, thus are reverted for generate *)
    1.17 +fun embed tacis (pt, pos as (p, Pos.Frm)) =
    1.18 +  (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
    1.19 +    and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
    1.20 +    let
    1.21 +      val (res, asm) = (State_Steps.result o last_elem) tacis
    1.22 +    	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
    1.23 +    	  (SOME (ist, ctxt), _) => (ist, ctxt)
    1.24 +      | (NONE, _) => error "Derive.embed Frm: uncovered case get_obj"
    1.25 +    	val form =  Ctree.get_obj  Ctree.g_form pt p
    1.26 +      (*val p = lev_on p; ---------------only difference to (..,Res) below*)
    1.27 +    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
    1.28 +    		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
    1.29 +    			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
    1.30 +    	val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
    1.31 +    	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
    1.32 +    	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
    1.33 +    	val pt = Ctree.update_branch pt p Ctree.TransitiveB
    1.34 +    in (c, (pt, pos)) end
    1.35 +  | embed tacis (pt, (p, Pos.Res)) =
    1.36 +    (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
    1.37 +      and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
    1.38 +    let
    1.39 +      val (res, asm) = (State_Steps.result o last_elem) tacis
    1.40 +    	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
    1.41 +    	  (_, SOME (ist, ctxt)) => (ist, ctxt)
    1.42 +      | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
    1.43 +    	val (f, _) = Ctree.get_obj Ctree.g_result pt p
    1.44 +    	val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
    1.45 +    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
    1.46 +    		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), 
    1.47 +    			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
    1.48 +    	val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
    1.49 +    	val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
    1.50 +    	val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
    1.51 +    	val pt = Ctree.update_branch pt p Ctree.TransitiveB
    1.52 +    in (c, (pt, pos)) end
    1.53 +  | embed _ _ = error "Derive.embed: uncovered definition"
    1.54 +
    1.55  (**)end(**)