(* 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 is_e_ctxt : Proof.context -> bool

  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

(*val subpbl_to_caller  .. rename according to naming convention TODO*)

(* ---- 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

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

struct

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

(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)

fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{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