(* Title: ../contextC.sml

   Author: Walther Neuper, Mathias Lehnfeld

   (c) due to copyright terms

*)

(* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)

signature CONTEXT_C =

sig

  val e_ctxt : Proof.context

  val isac_ctxt : 'a -> Proof.context

  val initialise : string -> term list -> Proof.context

  val initialise' : theory -> string list -> Proof.context

  val get_assumptions : Proof.context -> term list

  val insert_assumptions : term list -> Proof.context -> Proof.context

  val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context

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

  (*NONE*)

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

  val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context

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

end

(* survey on handling contexts:

-------------------------------

 theory is required for Pattern.match (and thus for Tactic.Rewrite* ), while

 ctxt is required for parsing and for managing pre-conditions and assumptions.

 * model-specify-phase:

   * Tactic.Model_Problem does declare_constraints for parsing (in Tactic.Add_Given, etc)

     ("insert_assumptions pres" has to wait for completing Tactic.Add_Given, etc)

     (Tactic.Refine_Problem uses theory NOT ctxt due to Pattern.match)

   * 

   * 

 * solve-phase by Lucas-Interpretation:

   * locate_input_tactic: 

     * Tactic.Apply_Method

       * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_pstate

         * in solve for root problem

         * in begin_end_prog for subproblem

     * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate

     * associate..Subproblem' returns ctxt ONLY with declare_constraints',

       with insert_assumptions wait for Tactic.Apply_Method

     * storing ctxt is done after return form locate_input_tactic

   * determine_next_tactic: 

     * TODO initialises ctxt by TODO

     * Tactic.Rewrite* create assumptions; respective insert_assumptions TODO

     * 

     * 

     * 

   * locate_input_formula: follows sig. of determine_next_tactic

 * changing from one method to another (in determine_next_tactic only):

   * from method to sub-program: just add new preconditions of the guard

     * locate_input_tactic: init_pstate by begin_end_prog

     * determine_next_tactic: 

   * from_subpbl_to_caller

 * finishing a method:

   * Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented)

 *

   * 

     * 

       * 

================================================================================================

call hierarchy

================================================================================================

  locatetac

    applicable_in (p, p_) pt (Tactic.Apply_Method pres

      insert_assumptions

  context_thy

    applicable_in (p, p_) pt (Tactic.Apply_Method pres

      insert_assumptions

    generate1 _ (Tactic.Rewrite***

      insert_assumptions

------------------------------------------------------------------------------------------------

solve phase before LI

------------------------------------------------------------------------------------------------

autocalc

  all_modspec

    declare_constraints'

  complete_solve

    all_modspec

      declare_constraints'

all_solve

  begin_end_prog (Tactic.Apply_Method'

    init_pstate

      declare_constraints'

      insert_assumptions

nxt_specify_

  begin_end_prog (Tactic.Apply_Method'

    init_pstate

      declare_constraints'

      insert_assumptions

------------------------------------------------------------------------------------------------

LI

------------------------------------------------------------------------------------------------

solve ("Apply_Method"                                          root-program

  init_pstate

    declare_constraints'

    insert_assumptions

  locate_input_tactic

    scan_to_tactic1

      scan_dn1 ..leaf                                              sub-program

        associate

          declare_constraints'

        applicable_in .. Tactic.Apply_Method pres

          insert_assumptions

  ? generate1 (look in test with "from ... to..))

determine_next_tactic

  scan_to_tactic2

    scan_dn2 ..leaf

      stac2tac_

        declare_constraints'

      applicable_in (p, p_) pt (Tactic.Apply_Method pres

        insert_assumptions

  ? generate1 (look in test with "from ... to..))

locate_input_formula                                          uses determine_next_tactic

  compare_step

    all_modspec

      declare_constraints'

    begin_end_prog (Tactic.Apply_Method'

      init_pstate

        declare_constraints'

        insert_assumptions

------------------------------------------------------------------------------------------------

specification phase

------------------------------------------------------------------------------------------------

  loc_specify_

    specify (Tactic.Init_Proof'

      prep_ori

        declare_constraints

  CalcTree

    nxt_specify_init_calc

      prep_ori

        declare_constraints

  modifyCalcHead

    input_icalhd

      prep_ori

        declare_constraints

  refine

    refin'

      prep_ori

        declare_constraints

------------------------------------------------------------------------------------------------

unused ?!

------------------------------------------------------------------------------------------------

  ??

    match_pbl

      prep_ori

        declare_constraints

  ??

    from_pblobj'

      init_pstate

        declare_constraints'

        insert_assumptions

  ??

    tac2tac_

      applicable_in (p, p_) pt (Tactic.Apply_Method pres

        insert_assumptions

*)

structure ContextC(**) : CONTEXT_C(**) =

struct

val e_ctxt = Proof_Context.init_global @{theory "Pure"};

fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx)

(* in Subproblem take respective actual arguments from program *)

fun initialise thy' ts =

  let

    val ctxt = Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global

    val frees = map TermC.vars ts |> flat |> distinct

    val _ = TermC.raise_type_conflicts frees

  in

    fold Variable.declare_constraints frees ctxt

  end

(* in root-problem take respective formalisation *)

fun initialise' thy fmz =

  let 

    val ctxt = thy |> Proof_Context.init_global

    val frees = map (TermC.parseNEW' ctxt) fmz |> map TermC.vars |> flat |> distinct

    val _ = TermC.raise_type_conflicts frees

  in

    fold Variable.declare_constraints frees ctxt

  end

structure Context_Data = Proof_Data (type T = term list fun init _ = []);

fun get_assumptions ctxt = Context_Data.get ctxt

fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))

(* transfer assumptions from one to another ctxt.

   does NOT respect scope: in a calculation identifiers are unique.

   but environments are scoped as usual in Luacs-interpretation.

   WN110520 redo (1) take declare_constraints (2) with combinators*)

fun transfer_asms_from_to from_ctxt to_ctxt =

  let

    val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat

    fun transfer [] to_ctxt = to_ctxt

        | transfer (from_asm :: fas) to_ctxt =

            if inter op = (TermC.vars from_asm) to_vars = []

            then transfer fas to_ctxt

            else transfer fas (insert_assumptions [from_asm] to_ctxt)

  in transfer (get_assumptions from_ctxt) to_ctxt end

(* exported from a subproblem to the context of the calling method:

   # 'scrval': the result of script interpretation and

   # those assumptions in the subproblem wich contain a variable known

     in the calling method. *)

fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =

  let

    val caller_ctxt = (scrval |> TermC.dest_list' |> insert_assumptions) caller_ctxt

  in transfer_asms_from_to sub_ctxt caller_ctxt end;

end