1(* ========================================================================= *) 2(* RANDOM FINITE MODELS *) 3(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Model = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* Model size. *) 11(* ------------------------------------------------------------------------- *) 12 13type size = {size : int} 14 15(* ------------------------------------------------------------------------- *) 16(* A model of size N has integer elements 0...N-1. *) 17(* ------------------------------------------------------------------------- *) 18 19type element = int 20 21val zeroElement : element 22 23val incrementElement : size -> element -> element option 24 25(* ------------------------------------------------------------------------- *) 26(* The parts of the model that are fixed. *) 27(* ------------------------------------------------------------------------- *) 28 29type fixedFunction = size -> element list -> element option 30 31type fixedRelation = size -> element list -> bool option 32 33datatype fixed = 34 Fixed of 35 {functions : fixedFunction NameArityMap.map, 36 relations : fixedRelation NameArityMap.map} 37 38val emptyFixed : fixed 39 40val unionFixed : fixed -> fixed -> fixed 41 42val getFunctionFixed : fixed -> NameArity.nameArity -> fixedFunction 43 44val getRelationFixed : fixed -> NameArity.nameArity -> fixedRelation 45 46val insertFunctionFixed : fixed -> NameArity.nameArity * fixedFunction -> fixed 47 48val insertRelationFixed : fixed -> NameArity.nameArity * fixedRelation -> fixed 49 50val unionListFixed : fixed list -> fixed 51 52val basicFixed : fixed (* interprets equality and hasType *) 53 54(* ------------------------------------------------------------------------- *) 55(* Renaming fixed model parts. *) 56(* ------------------------------------------------------------------------- *) 57 58type fixedMap = 59 {functionMap : Name.name NameArityMap.map, 60 relationMap : Name.name NameArityMap.map} 61 62val mapFixed : fixedMap -> fixed -> fixed 63 64val ppFixedMap : fixedMap Print.pp 65 66(* ------------------------------------------------------------------------- *) 67(* Standard fixed model parts. *) 68(* ------------------------------------------------------------------------- *) 69 70(* Projections *) 71 72val projectionMin : int 73 74val projectionMax : int 75 76val projectionName : int -> Name.name 77 78val projectionFixed : fixed 79 80(* Arithmetic *) 81 82val numeralMin : int 83 84val numeralMax : int 85 86val numeralName : int -> Name.name 87 88val addName : Name.name 89 90val divName : Name.name 91 92val dividesName : Name.name 93 94val evenName : Name.name 95 96val expName : Name.name 97 98val geName : Name.name 99 100val gtName : Name.name 101 102val isZeroName : Name.name 103 104val leName : Name.name 105 106val ltName : Name.name 107 108val modName : Name.name 109 110val multName : Name.name 111 112val negName : Name.name 113 114val oddName : Name.name 115 116val preName : Name.name 117 118val subName : Name.name 119 120val sucName : Name.name 121 122val modularFixed : fixed 123 124val overflowFixed : fixed 125 126(* Sets *) 127 128val cardName : Name.name 129 130val complementName : Name.name 131 132val differenceName : Name.name 133 134val emptyName : Name.name 135 136val memberName : Name.name 137 138val insertName : Name.name 139 140val intersectName : Name.name 141 142val singletonName : Name.name 143 144val subsetName : Name.name 145 146val symmetricDifferenceName : Name.name 147 148val unionName : Name.name 149 150val universeName : Name.name 151 152val setFixed : fixed 153 154(* Lists *) 155 156val appendName : Name.name 157 158val consName : Name.name 159 160val lengthName : Name.name 161 162val nilName : Name.name 163 164val nullName : Name.name 165 166val tailName : Name.name 167 168val listFixed : fixed 169 170(* ------------------------------------------------------------------------- *) 171(* Valuations. *) 172(* ------------------------------------------------------------------------- *) 173 174type valuation 175 176val emptyValuation : valuation 177 178val zeroValuation : NameSet.set -> valuation 179 180val constantValuation : element -> NameSet.set -> valuation 181 182val peekValuation : valuation -> Name.name -> element option 183 184val getValuation : valuation -> Name.name -> element 185 186val insertValuation : valuation -> Name.name * element -> valuation 187 188val randomValuation : {size : int} -> NameSet.set -> valuation 189 190val incrementValuation : 191 {size : int} -> NameSet.set -> valuation -> valuation option 192 193val foldValuation : 194 {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a 195 196(* ------------------------------------------------------------------------- *) 197(* A type of random finite models. *) 198(* ------------------------------------------------------------------------- *) 199 200type parameters = {size : int, fixed : fixed} 201 202type model 203 204val default : parameters 205 206val new : parameters -> model 207 208val size : model -> int 209 210(* ------------------------------------------------------------------------- *) 211(* Interpreting terms and formulas in the model. *) 212(* ------------------------------------------------------------------------- *) 213 214val interpretFunction : model -> Term.functionName * element list -> element 215 216val interpretRelation : model -> Atom.relationName * element list -> bool 217 218val interpretTerm : model -> valuation -> Term.term -> element 219 220val interpretAtom : model -> valuation -> Atom.atom -> bool 221 222val interpretFormula : model -> valuation -> Formula.formula -> bool 223 224val interpretLiteral : model -> valuation -> Literal.literal -> bool 225 226val interpretClause : model -> valuation -> Thm.clause -> bool 227 228(* ------------------------------------------------------------------------- *) 229(* Check whether random groundings of a formula are true in the model. *) 230(* Note: if it's cheaper, a systematic check will be performed instead. *) 231(* ------------------------------------------------------------------------- *) 232 233val check : 234 (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model -> 235 NameSet.set -> 'a -> {T : int, F : int} 236 237val checkAtom : 238 {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int} 239 240val checkFormula : 241 {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int} 242 243val checkLiteral : 244 {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int} 245 246val checkClause : 247 {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int} 248 249(* ------------------------------------------------------------------------- *) 250(* Updating the model. *) 251(* ------------------------------------------------------------------------- *) 252 253val updateFunction : 254 model -> (Term.functionName * element list) * element -> unit 255 256val updateRelation : 257 model -> (Atom.relationName * element list) * bool -> unit 258 259(* ------------------------------------------------------------------------- *) 260(* Choosing a random perturbation to make a formula true in the model. *) 261(* ------------------------------------------------------------------------- *) 262 263val perturbTerm : model -> valuation -> Term.term * element list -> unit 264 265val perturbAtom : model -> valuation -> Atom.atom * bool -> unit 266 267val perturbLiteral : model -> valuation -> Literal.literal -> unit 268 269val perturbClause : model -> valuation -> Thm.clause -> unit 270 271(* ------------------------------------------------------------------------- *) 272(* Pretty printing. *) 273(* ------------------------------------------------------------------------- *) 274 275val pp : model Print.pp 276 277end 278