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

   val is_empty : Proof.context -> bool

   val isac_ctxt : 'a -> Proof.context

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

   val add_constraints: term list -> Proof.context -> 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 avoid_contradict: term -> term list -> term * term list

   val subpbl_to_caller : Proof.context -> term -> Proof.context -> term * 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

   val contradict : term list -> term -> bool

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

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

 end

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

 struct

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

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

 fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});

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

 val declare_constraints = Variable.declare_constraints

 fun add_constraints ts ctxt =

   fold Variable.declare_constraints (TermC.vars' ts) ctxt

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

 fun initialise thy' ts =

   let

     val ctxt = ThyC.get_theory thy' |> Proof_Context.init_global

     val frees = TermC.vars' ts

     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 |> TermC.vars'

     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 op = (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.

 *)

 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

 (* there is still much TODO: factorise polynomials, etc *)

 fun contradict asm res = fold (curry or_) (map (fn p => TermC.negates res p) asm) false;

 (*

   Check a term for contradiction with a predicate list.

   This makes only sense for types bool and bool list. In these cases return

   the probably updated term together with 

   a respective list of non-contradicting predicates

 *)

 fun avoid_contradict t preds = 

       if TermC.is_bool_list t then

         let

           val no_contra = t |> TermC.dest_list' |> filter_out (contradict preds)

         in (no_contra |> TermC.list2isalist HOLogic.boolT, no_contra)

         end

       else if Term.type_of t = HOLogic.boolT then

         if contradict preds t then (@{term bool_undef}, []) else (t, [t])

       else (t (* type_of t \<noteq> bool *), [(* no predicate to add *)])

 (* for Canonical Argument Order used by |> below *)

 fun insert_assumptions_cao ctxt tms  = insert_assumptions tms ctxt

 fun subpbl_to_caller sub_ctxt prog_res caller_ctxt = caller_ctxt

   |> get_assumptions 

   |> avoid_contradict prog_res

   |> apsnd (insert_assumptions_cao caller_ctxt)

   |> apsnd (transfer_asms_from_to sub_ctxt)

 end