--- a/src/Tools/Metis/src/Model.sig Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Model.sig Mon Sep 13 21:24:10 2010 +0200
@@ -1,39 +1,197 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Model =
sig
(* ------------------------------------------------------------------------- *)
+(* Model size. *)
+(* ------------------------------------------------------------------------- *)
+
+type size = {size : int}
+
+(* ------------------------------------------------------------------------- *)
+(* A model of size N has integer elements 0...N-1. *)
+(* ------------------------------------------------------------------------- *)
+
+type element = int
+
+val zeroElement : element
+
+val incrementElement : size -> element -> element option
+
+(* ------------------------------------------------------------------------- *)
(* The parts of the model that are fixed. *)
-(* Note: a model of size N has integer elements 0...N-1. *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedFunction = size -> element list -> element option
+
+type fixedRelation = size -> element list -> bool option
+
+datatype fixed =
+ Fixed of
+ {functions : fixedFunction NameArityMap.map,
+ relations : fixedRelation NameArityMap.map}
+
+val emptyFixed : fixed
+
+val unionFixed : fixed -> fixed -> fixed
+
+val getFunctionFixed : fixed -> NameArity.nameArity -> fixedFunction
+
+val getRelationFixed : fixed -> NameArity.nameArity -> fixedRelation
+
+val insertFunctionFixed : fixed -> NameArity.nameArity * fixedFunction -> fixed
+
+val insertRelationFixed : fixed -> NameArity.nameArity * fixedRelation -> fixed
+
+val unionListFixed : fixed list -> fixed
+
+val basicFixed : fixed (* interprets equality and hasType *)
+
+(* ------------------------------------------------------------------------- *)
+(* Renaming fixed model parts. *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedMap =
+ {functionMap : Name.name NameArityMap.map,
+ relationMap : Name.name NameArityMap.map}
+
+val mapFixed : fixedMap -> fixed -> fixed
+
+val ppFixedMap : fixedMap Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Standard fixed model parts. *)
(* ------------------------------------------------------------------------- *)
-type fixed =
- {size : int} ->
- {functions : (Term.functionName * int list) -> int option,
- relations : (Atom.relationName * int list) -> bool option}
+(* Projections *)
+
+val projectionMin : int
+
+val projectionMax : int
+
+val projectionName : int -> Name.name
+
+val projectionFixed : fixed
+
+(* Arithmetic *)
+
+val numeralMin : int
+
+val numeralMax : int
+
+val numeralName : int -> Name.name
+
+val addName : Name.name
+
+val divName : Name.name
+
+val dividesName : Name.name
+
+val evenName : Name.name
+
+val expName : Name.name
+
+val geName : Name.name
-val fixedMerge : fixed -> fixed -> fixed (* Prefers the second fixed *)
+val gtName : Name.name
+
+val isZeroName : Name.name
+
+val leName : Name.name
+
+val ltName : Name.name
+
+val modName : Name.name
+
+val multName : Name.name
+
+val negName : Name.name
+
+val oddName : Name.name
-val fixedMergeList : fixed list -> fixed
+val preName : Name.name
+
+val subName : Name.name
+
+val sucName : Name.name
+
+val modularFixed : fixed
-val fixedPure : fixed (* : = *)
+val overflowFixed : fixed
+
+(* Sets *)
+
+val cardName : Name.name
+
+val complementName : Name.name
-val fixedBasic : fixed (* id fst snd #1 #2 #3 <> *)
+val differenceName : Name.name
+
+val emptyName : Name.name
+
+val memberName : Name.name
+
+val insertName : Name.name
+
+val intersectName : Name.name
+
+val singletonName : Name.name
+
+val subsetName : Name.name
+
+val symmetricDifferenceName : Name.name
-val fixedModulo : fixed (* <numerals> suc pre ~ + - * exp div mod *)
- (* is_0 divides even odd *)
+val unionName : Name.name
+
+val universeName : Name.name
+
+val setFixed : fixed
+
+(* Lists *)
+
+val appendName : Name.name
+
+val consName : Name.name
+
+val lengthName : Name.name
+
+val nilName : Name.name
-val fixedOverflowNum : fixed (* <numerals> suc pre + - * exp div mod *)
- (* is_0 <= < >= > divides even odd *)
+val nullName : Name.name
+
+val tailName : Name.name
+
+val listFixed : fixed
+
+(* ------------------------------------------------------------------------- *)
+(* Valuations. *)
+(* ------------------------------------------------------------------------- *)
+
+type valuation
+
+val emptyValuation : valuation
+
+val zeroValuation : NameSet.set -> valuation
-val fixedOverflowInt : fixed (* <numerals> suc pre + - * exp div mod *)
- (* is_0 <= < >= > divides even odd *)
+val constantValuation : element -> NameSet.set -> valuation
+
+val peekValuation : valuation -> Name.name -> element option
+
+val getValuation : valuation -> Name.name -> element
+
+val insertValuation : valuation -> Name.name * element -> valuation
-val fixedSet : fixed (* empty univ union intersect compl card in subset *)
+val randomValuation : {size : int} -> NameSet.set -> valuation
+
+val incrementValuation :
+ {size : int} -> NameSet.set -> valuation -> valuation option
+
+val foldValuation :
+ {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a
(* ------------------------------------------------------------------------- *)
(* A type of random finite models. *)
@@ -43,28 +201,21 @@
type model
+val default : parameters
+
val new : parameters -> model
val size : model -> int
(* ------------------------------------------------------------------------- *)
-(* Valuations. *)
-(* ------------------------------------------------------------------------- *)
-
-type valuation = int NameMap.map
-
-val valuationEmpty : valuation
-
-val valuationRandom : {size : int} -> NameSet.set -> valuation
-
-val valuationFold :
- {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a
-
-(* ------------------------------------------------------------------------- *)
(* Interpreting terms and formulas in the model. *)
(* ------------------------------------------------------------------------- *)
-val interpretTerm : model -> valuation -> Term.term -> int
+val interpretFunction : model -> Term.functionName * element list -> element
+
+val interpretRelation : model -> Atom.relationName * element list -> bool
+
+val interpretTerm : model -> valuation -> Term.term -> element
val interpretAtom : model -> valuation -> Atom.atom -> bool
@@ -79,16 +230,48 @@
(* Note: if it's cheaper, a systematic check will be performed instead. *)
(* ------------------------------------------------------------------------- *)
+val check :
+ (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
+ NameSet.set -> 'a -> {T : int, F : int}
+
val checkAtom :
- {maxChecks : int} -> model -> Atom.atom -> {T : int, F : int}
+ {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int}
val checkFormula :
- {maxChecks : int} -> model -> Formula.formula -> {T : int, F : int}
+ {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}
val checkLiteral :
- {maxChecks : int} -> model -> Literal.literal -> {T : int, F : int}
+ {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}
val checkClause :
- {maxChecks : int} -> model -> Thm.clause -> {T : int, F : int}
+ {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int}
+
+(* ------------------------------------------------------------------------- *)
+(* Updating the model. *)
+(* ------------------------------------------------------------------------- *)
+
+val updateFunction :
+ model -> (Term.functionName * element list) * element -> unit
+
+val updateRelation :
+ model -> (Atom.relationName * element list) * bool -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Choosing a random perturbation to make a formula true in the model. *)
+(* ------------------------------------------------------------------------- *)
+
+val perturbTerm : model -> valuation -> Term.term * element list -> unit
+
+val perturbAtom : model -> valuation -> Atom.atom * bool -> unit
+
+val perturbLiteral : model -> valuation -> Literal.literal -> unit
+
+val perturbClause : model -> valuation -> Thm.clause -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : model Print.pp
end