(* 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 -> Rule.rls -> term list -> Model.itm list -> (bool * term) list

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

   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

   val common_subthy : theory * theory -> theory

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

   (*NONE*)

 ( *\--- ! 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_Knowledge") (* for Pattern.match    *)

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

     then (true , pre)

     else (false , pre);

 fun pre2str (b, t) = pair2str (bool2str b, Rule.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 common_subthy (thy1, thy2) =

   if Context.subthy (thy1, thy2) then thy2

   else if Context.subthy (thy2, thy1) then thy1

     else Celem.assoc_thy "Isac_Knowledge"

 end;