(* Title:  Specify/where_-conds.sml

    Author: Walther Neuper 110226

    (c) due to copyright terms

 Operations on models.

 *)

 signature PRE_CONDITIONS =

 sig

   type T

   type input

   val to_string : T -> string

   val check: Rule_Set.T -> term list -> I_Model.T -> 'a -> bool * (bool * term) list (**)

 \<^isac_test>\<open>

   val eval: Rule_Set.T -> bool * term -> bool * term

 \<close>

 end

 (**)

 structure Pre_Conds(**) : PRE_CONDITIONS(**) =

 struct

 (**)

 (*type unchecked = term list*)

 (*type checked = Pre_Conds_Def.T;*)

 type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)

 type input = string list;

 fun to_str (b, t) = pair2str (bool2str b, UnparseC.term t);

 fun to_string pres = strs2str' (map (linefeed o to_str) pres);

 fun eval _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)

   | eval where_rls (true, where_) =

     if Rewrite.eval_true (Proof_Context.init_global (ThyC.Isac "")) [where_] where_rls

     then (true , where_)

     else (false , where_);

 fun check _ [] _ _ = (true, [])

   | check where_rls pres pbl (_ (* FIXME.WN0308 re-introduce I_Model.variants *)) =

     let

       val env = I_Model.environment pbl;

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

       val evals = map (eval where_rls) pres';

     in (foldl and_ (true, map fst evals), evals) end;

 (**)end(**)