(* Title: tools for 'modeling' und 'specifying' to be used in

          modspec.sml. The types are separated into this file,

          because some of them are stored in the calc-tree, and thus are required

          _before_ ctree.sml. 

           TODO: allocate elements of Selem and of Stool appropriately

   Author: Walther Neuper, Mathias Lehnfeld

   (c) due to copyright terms

*)

signature SPECIFY_TOOL =

sig

  val check_preconds : 'a -> Celem.rls -> term list -> Model.itm list -> (bool * term) list

  val check_preconds' : Celem.rls -> term list -> Model.itm list -> 'a -> (bool * term) list

  val get_assumptions : Proof.context -> term list

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

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

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

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

  datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_

  val refined_ : match_ list -> match_ option

  datatype match = Matches of Celem.pblID * Model.item Model.ppc | NoMatch of Celem.pblID * Model.item Model.ppc

  val matchs2str : match list -> string

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

  val pres2str : (bool * term) list -> string

  val refined : match list -> Celem.pblID

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

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

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  val pblID_of_match : match -> Celem.pblID

  val refined_IDitms : match list -> match option

end

structure Stool(**) : SPECIFY_TOOL(**) =

struct

datatype match = 

  Matches of Celem.pblID *  Model.item Model.ppc

| NoMatch of Celem.pblID *  Model.item  Model.ppc;

fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^  Model.itemppc2str ppc ^ ")"

  | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^  Model.itemppc2str ppc ^ ")";

fun matchs2str ms = (strs2str o (map match2str)) ms;

fun pblID_of_match (Matches (pI, _)) = pI

  | pblID_of_match (NoMatch (pI, _)) = pI;

(* 10.03 for Refine_Problem *)

datatype match_ = 

  Match_ of Celem.pblID * (( Model.itm list) * ((bool * term) list))

| NoMatch_;

(* the refined pbt is the last_element Matches in the list *)

fun is_matches (Matches _) = true

  | is_matches _ = false;

fun matches_pblID (Matches (pI, _)) = pI

  | matches_pblID _ = error "matches_pblID: uncovered case in fun.def.";

fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)

    handle _ => [];

fun refined_IDitms ms = ((find_first is_matches) o rev) ms;

(* the refined pbt is the last_element Matches in the list, for Refine_Problem, tryrefine *)

fun is_matches_ (Match_ _) = true

  | is_matches_ _ = false;

fun refined_ ms = ((find_first is_matches_) o rev) ms;

(* check a predicate labelled with indication of incomplete substitution;

  rls ->    (* for eval_true                                               *)

  bool * 	  (* have _all_ variables(Free) from the model-pattern 

               been substituted by a value from the pattern's environment ?*)

  term ->   (* the precondition                                            *)

  bool * 	  (* has the precondition evaluated to true                      *)

  term      (* the precondition (for map)                                  *)

*)

fun evalprecond _ (false, pre) = 

  (*NOT ALL Free's have been substituted, eg. because of incomplete model*)

    (false, pre)

  | evalprecond prls (true, pre) =

    if Rewrite.eval_true (Celem.assoc_thy "Isac") (* for Pattern.match    *)

		  [pre] prls                    (* pre parsed, prls.thy *)

    then (true , pre)

    else (false , pre);

fun pre2str (b, t) = pair2str(bool2str b, Celem.term2str t);

fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);

(* check preconditions, return true if all true *)

fun check_preconds' _ [] _ _ = []   (* empty preconditions are true   *)

  | check_preconds' prls pres pbl _ (* FIXME.WN0308 mvat re-introduce *) =

    let

      val env = Model.mk_env pbl;

      val pres' = map (TermC.subst_atomic_all env) pres;

    in map (evalprecond prls) pres' end;

fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);

fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;

(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)

fun declare_constraints t ctxt =

  let

    fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of

            (_, _ :: _) => (Free (v, T) :: get_vars vs)

          | (_, []  ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)

      | get_vars [] = [];

    val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

  in fold Variable.declare_constraints ts 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 |> Model.dest_list' |> insert_assumptions) caller_ctxt

  in transfer_asms_from_to sub_ctxt caller_ctxt end;

end;