(* 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 build_while_parsing: Formalise.model -> theory -> term list * Proof.context

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

  val initialise' : theory -> TermC.as_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

\<^isac_test>\<open>

  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

\<close>

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

fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt)

  | build_while_parsing_ (str :: strs) (ts, ctxt) = 

    let

      val t as (_ $ tm) = Syntax.read_term ctxt str

        handle ERROR msg => raise ERROR ("ContextC.build_while_parsing " ^ quote str ^ " " ^ msg)

      val vars = TermC.vars tm

      val ctxt' = add_constraints vars ctxt

    in build_while_parsing_ strs (ts @ [t], ctxt') end

(* shouldn't that be done by fold ?

   fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *)

fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy)

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

(* FIXME: should be replaced by build_while_parsing *)

fun initialise ctxt ts =

  let

    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 expr_val caller_ctxt = caller_ctxt

  |> get_assumptions 

  |> avoid_contradict expr_val

  |> apsnd (insert_assumptions_cao caller_ctxt)

  |> apsnd (transfer_asms_from_to sub_ctxt)

end