--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Active.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,55 @@
+(* ========================================================================= *)
+(* THE ACTIVE SET OF CLAUSES *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Active =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of active clause sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type simplify =
+ {subsume : bool,
+ reduce : bool,
+ rewrite : bool}
+
+type parameters =
+ {clause : Clause.parameters,
+ prefactor : simplify,
+ postfactor : simplify}
+
+type active
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val size : active -> int
+
+val saturation : active -> Clause.clause list
+
+(* ------------------------------------------------------------------------- *)
+(* Create a new active clause set and initialize clauses. *)
+(* ------------------------------------------------------------------------- *)
+
+val new :
+ parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} ->
+ active * {axioms : Clause.clause list, conjecture : Clause.clause list}
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set and deduce all consequences. *)
+(* ------------------------------------------------------------------------- *)
+
+val add : active -> Clause.clause -> active * Clause.clause list
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : active Print.pp
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Active.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,911 @@
+(* ========================================================================= *)
+(* THE ACTIVE SET OF CLAUSES *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Active :> Active =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*MetisDebug
+local
+ fun mkRewrite ordering =
+ let
+ fun add (cl,rw) =
+ let
+ val {id, thm = th, ...} = Clause.dest cl
+ in
+ case total Thm.destUnitEq th of
+ SOME l_r => Rewrite.add rw (id,(l_r,th))
+ | NONE => rw
+ end
+ in
+ foldl add (Rewrite.new (KnuthBendixOrder.compare ordering))
+ end;
+
+ fun allFactors red =
+ let
+ fun allClause cl =
+ List.all red (cl :: Clause.factor cl) orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.allFactors: cl" cl
+ in
+ false
+ end
+ in
+ List.all allClause
+ end;
+
+ fun allResolutions red =
+ let
+ fun allClause2 cl_lit cl =
+ let
+ fun allLiteral2 lit =
+ case total (Clause.resolve cl_lit) (cl,lit) of
+ NONE => true
+ | SOME cl => allFactors red [cl]
+ in
+ LiteralSet.all allLiteral2 (Clause.literals cl)
+ end orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.allResolutions: cl2" cl
+ in
+ false
+ end
+
+ fun allClause1 allCls cl =
+ let
+ val cl = Clause.freshVars cl
+
+ fun allLiteral1 lit = List.all (allClause2 (cl,lit)) allCls
+ in
+ LiteralSet.all allLiteral1 (Clause.literals cl)
+ end orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.allResolutions: cl1" cl
+ in
+ false
+ end
+
+ in
+ fn [] => true
+ | allCls as cl :: cls =>
+ allClause1 allCls cl andalso allResolutions red cls
+ end;
+
+ fun allParamodulations red cls =
+ let
+ fun allClause2 cl_lit_ort_tm cl =
+ let
+ fun allLiteral2 lit =
+ let
+ val para = Clause.paramodulate cl_lit_ort_tm
+
+ fun allSubterms (path,tm) =
+ case total para (cl,lit,path,tm) of
+ NONE => true
+ | SOME cl => allFactors red [cl]
+ in
+ List.all allSubterms (Literal.nonVarTypedSubterms lit)
+ end orelse
+ let
+ val () = Print.trace Literal.pp
+ "Active.isSaturated.allParamodulations: lit2" lit
+ in
+ false
+ end
+ in
+ LiteralSet.all allLiteral2 (Clause.literals cl)
+ end orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.allParamodulations: cl2" cl
+ val (_,_,ort,_) = cl_lit_ort_tm
+ val () = Print.trace Rewrite.ppOrient
+ "Active.isSaturated.allParamodulations: ort1" ort
+ in
+ false
+ end
+
+ fun allClause1 cl =
+ let
+ val cl = Clause.freshVars cl
+
+ fun allLiteral1 lit =
+ let
+ fun allCl2 x = List.all (allClause2 x) cls
+ in
+ case total Literal.destEq lit of
+ NONE => true
+ | SOME (l,r) =>
+ allCl2 (cl,lit,Rewrite.LeftToRight,l) andalso
+ allCl2 (cl,lit,Rewrite.RightToLeft,r)
+ end orelse
+ let
+ val () = Print.trace Literal.pp
+ "Active.isSaturated.allParamodulations: lit1" lit
+ in
+ false
+ end
+ in
+ LiteralSet.all allLiteral1 (Clause.literals cl)
+ end orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.allParamodulations: cl1" cl
+ in
+ false
+ end
+ in
+ List.all allClause1 cls
+ end;
+
+ fun redundant {subsume,reduce,rewrite} =
+ let
+ fun simp cl =
+ case Clause.simplify cl of
+ NONE => true
+ | SOME cl =>
+ Subsume.isStrictlySubsumed subsume (Clause.literals cl) orelse
+ let
+ val cl' = cl
+ val cl' = Clause.reduce reduce cl'
+ val cl' = Clause.rewrite rewrite cl'
+ in
+ not (Clause.equalThms cl cl') andalso
+ (simp cl' orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.redundant: cl'" cl'
+ in
+ false
+ end)
+ end
+ in
+ fn cl =>
+ simp cl orelse
+ let
+ val () = Print.trace Clause.pp
+ "Active.isSaturated.redundant: cl" cl
+ in
+ false
+ end
+ end;
+in
+ fun isSaturated ordering subs cls =
+ let
+ val rd = Units.empty
+ val rw = mkRewrite ordering cls
+ val red = redundant {subsume = subs, reduce = rd, rewrite = rw}
+ in
+ (allFactors red cls andalso
+ allResolutions red cls andalso
+ allParamodulations red cls) orelse
+ let
+ val () = Print.trace Rewrite.pp "Active.isSaturated: rw" rw
+ val () = Print.trace (Print.ppList Clause.pp)
+ "Active.isSaturated: clauses" cls
+ in
+ false
+ end
+ end;
+end;
+
+fun checkSaturated ordering subs cls =
+ if isSaturated ordering subs cls then ()
+ else raise Bug "Active.checkSaturated";
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* A type of active clause sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type simplify = {subsume : bool, reduce : bool, rewrite : bool};
+
+type parameters =
+ {clause : Clause.parameters,
+ prefactor : simplify,
+ postfactor : simplify};
+
+datatype active =
+ Active of
+ {parameters : parameters,
+ clauses : Clause.clause IntMap.map,
+ units : Units.units,
+ rewrite : Rewrite.rewrite,
+ subsume : Clause.clause Subsume.subsume,
+ literals : (Clause.clause * Literal.literal) LiteralNet.literalNet,
+ equations :
+ (Clause.clause * Literal.literal * Rewrite.orient * Term.term)
+ TermNet.termNet,
+ subterms :
+ (Clause.clause * Literal.literal * Term.path * Term.term)
+ TermNet.termNet,
+ allSubterms : (Clause.clause * Term.term) TermNet.termNet};
+
+fun getSubsume (Active {subsume = s, ...}) = s;
+
+fun setRewrite active rewrite =
+ let
+ val Active
+ {parameters,clauses,units,subsume,literals,equations,
+ subterms,allSubterms,...} = active
+ in
+ Active
+ {parameters = parameters, clauses = clauses, units = units,
+ rewrite = rewrite, subsume = subsume, literals = literals,
+ equations = equations, subterms = subterms, allSubterms = allSubterms}
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val maxSimplify : simplify = {subsume = true, reduce = true, rewrite = true};
+
+val default : parameters =
+ {clause = Clause.default,
+ prefactor = maxSimplify,
+ postfactor = maxSimplify};
+
+fun empty parameters =
+ let
+ val {clause,...} = parameters
+ val {ordering,...} = clause
+ in
+ Active
+ {parameters = parameters,
+ clauses = IntMap.new (),
+ units = Units.empty,
+ rewrite = Rewrite.new (KnuthBendixOrder.compare ordering),
+ subsume = Subsume.new (),
+ literals = LiteralNet.new {fifo = false},
+ equations = TermNet.new {fifo = false},
+ subterms = TermNet.new {fifo = false},
+ allSubterms = TermNet.new {fifo = false}}
+ end;
+
+fun size (Active {clauses,...}) = IntMap.size clauses;
+
+fun clauses (Active {clauses = cls, ...}) =
+ let
+ fun add (_,cl,acc) = cl :: acc
+ in
+ IntMap.foldr add [] cls
+ end;
+
+fun saturation active =
+ let
+ fun remove (cl,(cls,subs)) =
+ let
+ val lits = Clause.literals cl
+ in
+ if Subsume.isStrictlySubsumed subs lits then (cls,subs)
+ else (cl :: cls, Subsume.insert subs (lits,()))
+ end
+
+ val cls = clauses active
+ val (cls,_) = foldl remove ([], Subsume.new ()) cls
+ val (cls,subs) = foldl remove ([], Subsume.new ()) cls
+
+(*MetisDebug
+ val Active {parameters,...} = active
+ val {clause,...} = parameters
+ val {ordering,...} = clause
+ val () = checkSaturated ordering subs cls
+*)
+ in
+ cls
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp =
+ let
+ fun toStr active = "Active{" ^ Int.toString (size active) ^ "}"
+ in
+ Print.ppMap toStr Print.ppString
+ end;
+
+(*MetisDebug
+local
+ fun ppField f ppA a =
+ Print.blockProgram Print.Inconsistent 2
+ [Print.addString (f ^ " ="),
+ Print.addBreak 1,
+ ppA a];
+
+ val ppClauses =
+ ppField "clauses"
+ (Print.ppMap IntMap.toList
+ (Print.ppList (Print.ppPair Print.ppInt Clause.pp)));
+
+ val ppRewrite = ppField "rewrite" Rewrite.pp;
+
+ val ppSubterms =
+ ppField "subterms"
+ (TermNet.pp
+ (Print.ppMap (fn (c,l,p,t) => ((Clause.id c, l, p), t))
+ (Print.ppPair
+ (Print.ppTriple Print.ppInt Literal.pp Term.ppPath)
+ Term.pp)));
+in
+ fun pp (Active {clauses,rewrite,subterms,...}) =
+ Print.blockProgram Print.Inconsistent 2
+ [Print.addString "Active",
+ Print.addBreak 1,
+ Print.blockProgram Print.Inconsistent 1
+ [Print.addString "{",
+ ppClauses clauses,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppRewrite rewrite,
+(*MetisTrace5
+ Print.addString ",",
+ Print.addBreak 1,
+ ppSubterms subterms,
+*)
+ Print.skip],
+ Print.addString "}"];
+end;
+*)
+
+val toString = Print.toString pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Simplify clauses. *)
+(* ------------------------------------------------------------------------- *)
+
+fun simplify simp units rewr subs =
+ let
+ val {subsume = s, reduce = r, rewrite = w} = simp
+
+ fun rewrite cl =
+ let
+ val cl' = Clause.rewrite rewr cl
+ in
+ if Clause.equalThms cl cl' then SOME cl else Clause.simplify cl'
+ end
+ in
+ fn cl =>
+ case Clause.simplify cl of
+ NONE => NONE
+ | SOME cl =>
+ case (if w then rewrite cl else SOME cl) of
+ NONE => NONE
+ | SOME cl =>
+ let
+ val cl = if r then Clause.reduce units cl else cl
+ in
+ if s andalso Clause.subsumes subs cl then NONE else SOME cl
+ end
+ end;
+
+(*MetisDebug
+val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
+ let
+ fun traceCl s = Print.trace Clause.pp ("Active.simplify: " ^ s)
+(*MetisTrace4
+ val ppClOpt = Print.ppOption Clause.pp
+ val () = traceCl "cl" cl
+*)
+ val cl' = simplify simp units rewr subs cl
+(*MetisTrace4
+ val () = Print.trace ppClOpt "Active.simplify: cl'" cl'
+*)
+ val () =
+ case cl' of
+ NONE => ()
+ | SOME cl' =>
+ case
+ (case simplify simp units rewr subs cl' of
+ NONE => SOME ("away", K ())
+ | SOME cl'' =>
+ if Clause.equalThms cl' cl'' then NONE
+ else SOME ("further", fn () => traceCl "cl''" cl'')) of
+ NONE => ()
+ | SOME (e,f) =>
+ let
+ val () = traceCl "cl" cl
+ val () = traceCl "cl'" cl'
+ val () = f ()
+ in
+ raise
+ Bug
+ ("Active.simplify: clause should have been simplified "^e)
+ end
+ in
+ cl'
+ end;
+*)
+
+fun simplifyActive simp active =
+ let
+ val Active {units,rewrite,subsume,...} = active
+ in
+ simplify simp units rewrite subsume
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set. *)
+(* ------------------------------------------------------------------------- *)
+
+fun addUnit units cl =
+ let
+ val th = Clause.thm cl
+ in
+ case total Thm.destUnit th of
+ SOME lit => Units.add units (lit,th)
+ | NONE => units
+ end;
+
+fun addRewrite rewrite cl =
+ let
+ val th = Clause.thm cl
+ in
+ case total Thm.destUnitEq th of
+ SOME l_r => Rewrite.add rewrite (Clause.id cl, (l_r,th))
+ | NONE => rewrite
+ end;
+
+fun addSubsume subsume cl = Subsume.insert subsume (Clause.literals cl, cl);
+
+fun addLiterals literals cl =
+ let
+ fun add (lit as (_,atm), literals) =
+ if Atom.isEq atm then literals
+ else LiteralNet.insert literals (lit,(cl,lit))
+ in
+ LiteralSet.foldl add literals (Clause.largestLiterals cl)
+ end;
+
+fun addEquations equations cl =
+ let
+ fun add ((lit,ort,tm),equations) =
+ TermNet.insert equations (tm,(cl,lit,ort,tm))
+ in
+ foldl add equations (Clause.largestEquations cl)
+ end;
+
+fun addSubterms subterms cl =
+ let
+ fun add ((lit,path,tm),subterms) =
+ TermNet.insert subterms (tm,(cl,lit,path,tm))
+ in
+ foldl add subterms (Clause.largestSubterms cl)
+ end;
+
+fun addAllSubterms allSubterms cl =
+ let
+ fun add ((_,_,tm),allSubterms) =
+ TermNet.insert allSubterms (tm,(cl,tm))
+ in
+ foldl add allSubterms (Clause.allSubterms cl)
+ end;
+
+fun addClause active cl =
+ let
+ val Active
+ {parameters,clauses,units,rewrite,subsume,literals,
+ equations,subterms,allSubterms} = active
+ val clauses = IntMap.insert clauses (Clause.id cl, cl)
+ and subsume = addSubsume subsume cl
+ and literals = addLiterals literals cl
+ and equations = addEquations equations cl
+ and subterms = addSubterms subterms cl
+ and allSubterms = addAllSubterms allSubterms cl
+ in
+ Active
+ {parameters = parameters, clauses = clauses, units = units,
+ rewrite = rewrite, subsume = subsume, literals = literals,
+ equations = equations, subterms = subterms,
+ allSubterms = allSubterms}
+ end;
+
+fun addFactorClause active cl =
+ let
+ val Active
+ {parameters,clauses,units,rewrite,subsume,literals,
+ equations,subterms,allSubterms} = active
+ val units = addUnit units cl
+ and rewrite = addRewrite rewrite cl
+ in
+ Active
+ {parameters = parameters, clauses = clauses, units = units,
+ rewrite = rewrite, subsume = subsume, literals = literals,
+ equations = equations, subterms = subterms, allSubterms = allSubterms}
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Derive (unfactored) consequences of a clause. *)
+(* ------------------------------------------------------------------------- *)
+
+fun deduceResolution literals cl (lit as (_,atm), acc) =
+ let
+ fun resolve (cl_lit,acc) =
+ case total (Clause.resolve cl_lit) (cl,lit) of
+ SOME cl' => cl' :: acc
+ | NONE => acc
+(*MetisTrace4
+ val () = Print.trace Literal.pp "Active.deduceResolution: lit" lit
+*)
+ in
+ if Atom.isEq atm then acc
+ else foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
+ end;
+
+fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
+ let
+ fun para (cl_lit_path_tm,acc) =
+ case total (Clause.paramodulate (cl,lit,ort,tm)) cl_lit_path_tm of
+ SOME cl' => cl' :: acc
+ | NONE => acc
+ in
+ foldl para acc (TermNet.unify subterms tm)
+ end;
+
+fun deduceParamodulationInto equations cl ((lit,path,tm),acc) =
+ let
+ fun para (cl_lit_ort_tm,acc) =
+ case total (Clause.paramodulate cl_lit_ort_tm) (cl,lit,path,tm) of
+ SOME cl' => cl' :: acc
+ | NONE => acc
+ in
+ foldl para acc (TermNet.unify equations tm)
+ end;
+
+fun deduce active cl =
+ let
+ val Active {parameters,literals,equations,subterms,...} = active
+
+ val lits = Clause.largestLiterals cl
+ val eqns = Clause.largestEquations cl
+ val subtms =
+ if TermNet.null equations then [] else Clause.largestSubterms cl
+(*MetisTrace5
+ val () = Print.trace LiteralSet.pp "Active.deduce: lits" lits
+ val () = Print.trace
+ (Print.ppList
+ (Print.ppMap (fn (lit,ort,_) => (lit,ort))
+ (Print.ppPair Literal.pp Rewrite.ppOrient)))
+ "Active.deduce: eqns" eqns
+ val () = Print.trace
+ (Print.ppList
+ (Print.ppTriple Literal.pp Term.ppPath Term.pp))
+ "Active.deduce: subtms" subtms
+*)
+
+ val acc = []
+ val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
+ val acc = foldl (deduceParamodulationWith subterms cl) acc eqns
+ val acc = foldl (deduceParamodulationInto equations cl) acc subtms
+ val acc = rev acc
+
+(*MetisTrace5
+ val () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
+*)
+ in
+ acc
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extract clauses from the active set that can be simplified. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun clause_rewritables active =
+ let
+ val Active {clauses,rewrite,...} = active
+
+ fun rewr (id,cl,ids) =
+ let
+ val cl' = Clause.rewrite rewrite cl
+ in
+ if Clause.equalThms cl cl' then ids else IntSet.add ids id
+ end
+ in
+ IntMap.foldr rewr IntSet.empty clauses
+ end;
+
+ fun orderedRedexResidues (((l,r),_),ort) =
+ case ort of
+ NONE => []
+ | SOME Rewrite.LeftToRight => [(l,r,true)]
+ | SOME Rewrite.RightToLeft => [(r,l,true)];
+
+ fun unorderedRedexResidues (((l,r),_),ort) =
+ case ort of
+ NONE => [(l,r,false),(r,l,false)]
+ | SOME _ => [];
+
+ fun rewrite_rewritables active rewr_ids =
+ let
+ val Active {parameters,rewrite,clauses,allSubterms,...} = active
+ val {clause = {ordering,...}, ...} = parameters
+ val order = KnuthBendixOrder.compare ordering
+
+ fun addRewr (id,acc) =
+ if IntMap.inDomain id clauses then IntSet.add acc id else acc
+
+ fun addReduce ((l,r,ord),acc) =
+ let
+ fun isValidRewr tm =
+ case total (Subst.match Subst.empty l) tm of
+ NONE => false
+ | SOME sub =>
+ ord orelse
+ let
+ val tm' = Subst.subst (Subst.normalize sub) r
+ in
+ order (tm,tm') = SOME GREATER
+ end
+
+ fun addRed ((cl,tm),acc) =
+ let
+(*MetisTrace5
+ val () = Print.trace Clause.pp "Active.addRed: cl" cl
+ val () = Print.trace Term.pp "Active.addRed: tm" tm
+*)
+ val id = Clause.id cl
+ in
+ if IntSet.member id acc then acc
+ else if not (isValidRewr tm) then acc
+ else IntSet.add acc id
+ end
+
+(*MetisTrace5
+ val () = Print.trace Term.pp "Active.addReduce: l" l
+ val () = Print.trace Term.pp "Active.addReduce: r" r
+ val () = Print.trace Print.ppBool "Active.addReduce: ord" ord
+*)
+ in
+ List.foldl addRed acc (TermNet.matched allSubterms l)
+ end
+
+ fun addEquation redexResidues (id,acc) =
+ case Rewrite.peek rewrite id of
+ NONE => acc
+ | SOME eqn_ort => List.foldl addReduce acc (redexResidues eqn_ort)
+
+ val addOrdered = addEquation orderedRedexResidues
+
+ val addUnordered = addEquation unorderedRedexResidues
+
+ val ids = IntSet.empty
+ val ids = List.foldl addRewr ids rewr_ids
+ val ids = List.foldl addOrdered ids rewr_ids
+ val ids = List.foldl addUnordered ids rewr_ids
+ in
+ ids
+ end;
+
+ fun choose_clause_rewritables active ids = size active <= length ids
+
+ fun rewritables active ids =
+ if choose_clause_rewritables active ids then clause_rewritables active
+ else rewrite_rewritables active ids;
+
+(*MetisDebug
+ val rewritables = fn active => fn ids =>
+ let
+ val clause_ids = clause_rewritables active
+ val rewrite_ids = rewrite_rewritables active ids
+
+ val () =
+ if IntSet.equal rewrite_ids clause_ids then ()
+ else
+ let
+ val ppIdl = Print.ppList Print.ppInt
+ val ppIds = Print.ppMap IntSet.toList ppIdl
+ val () = Print.trace pp "Active.rewritables: active" active
+ val () = Print.trace ppIdl "Active.rewritables: ids" ids
+ val () = Print.trace ppIds
+ "Active.rewritables: clause_ids" clause_ids
+ val () = Print.trace ppIds
+ "Active.rewritables: rewrite_ids" rewrite_ids
+ in
+ raise Bug "Active.rewritables: ~(rewrite_ids SUBSET clause_ids)"
+ end
+ in
+ if choose_clause_rewritables active ids then clause_ids else rewrite_ids
+ end;
+*)
+
+ fun delete active ids =
+ if IntSet.null ids then active
+ else
+ let
+ fun idPred id = not (IntSet.member id ids)
+
+ fun clausePred cl = idPred (Clause.id cl)
+
+ val Active
+ {parameters,
+ clauses,
+ units,
+ rewrite,
+ subsume,
+ literals,
+ equations,
+ subterms,
+ allSubterms} = active
+
+ val clauses = IntMap.filter (idPred o fst) clauses
+ and subsume = Subsume.filter clausePred subsume
+ and literals = LiteralNet.filter (clausePred o #1) literals
+ and equations = TermNet.filter (clausePred o #1) equations
+ and subterms = TermNet.filter (clausePred o #1) subterms
+ and allSubterms = TermNet.filter (clausePred o fst) allSubterms
+ in
+ Active
+ {parameters = parameters,
+ clauses = clauses,
+ units = units,
+ rewrite = rewrite,
+ subsume = subsume,
+ literals = literals,
+ equations = equations,
+ subterms = subterms,
+ allSubterms = allSubterms}
+ end;
+in
+ fun extract_rewritables (active as Active {clauses,rewrite,...}) =
+ if Rewrite.isReduced rewrite then (active,[])
+ else
+ let
+(*MetisTrace3
+ val () = trace "Active.extract_rewritables: inter-reducing\n"
+*)
+ val (rewrite,ids) = Rewrite.reduce' rewrite
+ val active = setRewrite active rewrite
+ val ids = rewritables active ids
+ val cls = IntSet.transform (IntMap.get clauses) ids
+(*MetisTrace3
+ val ppCls = Print.ppList Clause.pp
+ val () = Print.trace ppCls "Active.extract_rewritables: cls" cls
+*)
+ in
+ (delete active ids, cls)
+ end
+(*MetisDebug
+ handle Error err =>
+ raise Bug ("Active.extract_rewritables: shouldn't fail\n" ^ err);
+*)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Factor clauses. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun prefactor_simplify active subsume =
+ let
+ val Active {parameters,units,rewrite,...} = active
+ val {prefactor,...} = parameters
+ in
+ simplify prefactor units rewrite subsume
+ end;
+
+ fun postfactor_simplify active subsume =
+ let
+ val Active {parameters,units,rewrite,...} = active
+ val {postfactor,...} = parameters
+ in
+ simplify postfactor units rewrite subsume
+ end;
+
+ val sort_utilitywise =
+ let
+ fun utility cl =
+ case LiteralSet.size (Clause.literals cl) of
+ 0 => ~1
+ | 1 => if Thm.isUnitEq (Clause.thm cl) then 0 else 1
+ | n => n
+ in
+ sortMap utility Int.compare
+ end;
+
+ fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) =
+ case postfactor_simplify active subsume cl of
+ NONE => active_subsume_acc
+ | SOME cl =>
+ let
+ val active = addFactorClause active cl
+ and subsume = addSubsume subsume cl
+ and acc = cl :: acc
+ in
+ (active,subsume,acc)
+ end;
+
+ fun factor1 (cl, active_subsume_acc as (active,subsume,_)) =
+ case prefactor_simplify active subsume cl of
+ NONE => active_subsume_acc
+ | SOME cl =>
+ let
+ val cls = sort_utilitywise (cl :: Clause.factor cl)
+ in
+ foldl factor_add active_subsume_acc cls
+ end;
+
+ fun factor' active acc [] = (active, rev acc)
+ | factor' active acc cls =
+ let
+ val cls = sort_utilitywise cls
+ val subsume = getSubsume active
+ val (active,_,acc) = foldl factor1 (active,subsume,acc) cls
+ val (active,cls) = extract_rewritables active
+ in
+ factor' active acc cls
+ end;
+in
+ fun factor active cls = factor' active [] cls;
+end;
+
+(*MetisTrace4
+val factor = fn active => fn cls =>
+ let
+ val ppCls = Print.ppList Clause.pp
+ val () = Print.trace ppCls "Active.factor: cls" cls
+ val (active,cls') = factor active cls
+ val () = Print.trace ppCls "Active.factor: cls'" cls'
+ in
+ (active,cls')
+ end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Create a new active clause set and initialize clauses. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new parameters {axioms,conjecture} =
+ let
+ val {clause,...} = parameters
+
+ fun mk_clause th =
+ Clause.mk {parameters = clause, id = Clause.newId (), thm = th}
+
+ val active = empty parameters
+ val (active,axioms) = factor active (map mk_clause axioms)
+ val (active,conjecture) = factor active (map mk_clause conjecture)
+ in
+ (active, {axioms = axioms, conjecture = conjecture})
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Add a clause into the active set and deduce all consequences. *)
+(* ------------------------------------------------------------------------- *)
+
+fun add active cl =
+ case simplifyActive maxSimplify active cl of
+ NONE => (active,[])
+ | SOME cl' =>
+ if Clause.isContradiction cl' then (active,[cl'])
+ else if not (Clause.equalThms cl cl') then factor active [cl']
+ else
+ let
+(*MetisTrace2
+ val () = Print.trace Clause.pp "Active.add: cl" cl
+*)
+ val active = addClause active cl
+ val cl = Clause.freshVars cl
+ val cls = deduce active cl
+ val (active,cls) = factor active cls
+(*MetisTrace2
+ val ppCls = Print.ppList Clause.pp
+ val () = Print.trace ppCls "Active.add: cls" cls
+*)
+ in
+ (active,cls)
+ end;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Atom.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,141 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Atom =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name
+
+type relation = relationName * int
+
+type atom = relationName * Term.term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val name : atom -> relationName
+
+val arguments : atom -> Term.term list
+
+val arity : atom -> int
+
+val relation : atom -> relation
+
+val functions : atom -> NameAritySet.set
+
+val functionNames : atom -> NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : relationName -> Term.term * Term.term -> atom
+
+val destBinop : relationName -> atom -> Term.term * Term.term
+
+val isBinop : relationName -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : atom -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : atom * atom -> order
+
+val equal : atom -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : atom -> Term.path -> Term.term
+
+val subterms : atom -> (Term.path * Term.term) list
+
+val replace : atom -> Term.path * Term.term -> atom
+
+val find : (Term.term -> bool) -> atom -> Term.path option
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> atom -> bool
+
+val freeVars : atom -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> atom -> atom
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelationName : relationName
+
+val eqRelation : relation
+
+val mkEq : Term.term * Term.term -> atom
+
+val destEq : atom -> Term.term * Term.term
+
+val isEq : atom -> bool
+
+val mkRefl : Term.term -> atom
+
+val destRefl : atom -> Term.term
+
+val isRefl : atom -> bool
+
+val sym : atom -> atom (* raises Error if given a refl *)
+
+val lhs : atom -> Term.term
+
+val rhs : atom -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : atom -> int
+
+val nonVarTypedSubterms : atom -> (Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : atom Print.pp
+
+val toString : atom -> string
+
+val fromString : string -> atom
+
+val parse : Term.term Parse.quotation -> atom
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Atom.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,247 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Atom :> Atom =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name;
+
+type relation = relationName * int;
+
+type atom = relationName * Term.term list;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun name ((rel,_) : atom) = rel;
+
+fun arguments ((_,args) : atom) = args;
+
+fun arity atm = length (arguments atm);
+
+fun relation atm = (name atm, arity atm);
+
+val functions =
+ let
+ fun f (tm,acc) = NameAritySet.union (Term.functions tm) acc
+ in
+ fn atm => foldl f NameAritySet.empty (arguments atm)
+ end;
+
+val functionNames =
+ let
+ fun f (tm,acc) = NameSet.union (Term.functionNames tm) acc
+ in
+ fn atm => foldl f NameSet.empty (arguments atm)
+ end;
+
+(* Binary relations *)
+
+fun mkBinop p (a,b) : atom = (p,[a,b]);
+
+fun destBinop p (x,[a,b]) =
+ if Name.equal x p then (a,b) else raise Error "Atom.destBinop: wrong binop"
+ | destBinop _ _ = raise Error "Atom.destBinop: not a binop";
+
+fun isBinop p = can (destBinop p);
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols atm = foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((p1,tms1),(p2,tms2)) =
+ case Name.compare (p1,p2) of
+ LESS => LESS
+ | EQUAL => lexCompare Term.compare (tms1,tms2)
+ | GREATER => GREATER;
+
+fun equal atm1 atm2 = compare (atm1,atm2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm _ [] = raise Bug "Atom.subterm: empty path"
+ | subterm ((_,tms) : atom) (h :: t) =
+ if h >= length tms then raise Error "Atom.subterm: bad path"
+ else Term.subterm (List.nth (tms,h)) t;
+
+fun subterms ((_,tms) : atom) =
+ let
+ fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
+ in
+ foldl f [] (enumerate tms)
+ end;
+
+fun replace _ ([],_) = raise Bug "Atom.replace: empty path"
+ | replace (atm as (rel,tms)) (h :: t, res) : atom =
+ if h >= length tms then raise Error "Atom.replace: bad path"
+ else
+ let
+ val tm = List.nth (tms,h)
+ val tm' = Term.replace tm (t,res)
+ in
+ if Portable.pointerEqual (tm,tm') then atm
+ else (rel, updateNth (h,tm') tms)
+ end;
+
+fun find pred =
+ let
+ fun f (i,tm) =
+ case Term.find pred tm of
+ SOME path => SOME (i :: path)
+ | NONE => NONE
+ in
+ fn (_,tms) : atom => first f (enumerate tms)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v atm = List.exists (Term.freeIn v) (arguments atm);
+
+val freeVars =
+ let
+ fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc
+ in
+ fn atm => foldl f NameSet.empty (arguments atm)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (atm as (p,tms)) : atom =
+ let
+ val tms' = Sharing.map (Subst.subst sub) tms
+ in
+ if Portable.pointerEqual (tms',tms) then atm else (p,tms')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun matchArg ((tm1,tm2),sub) = Subst.match sub tm1 tm2;
+in
+ fun match sub (p1,tms1) (p2,tms2) =
+ let
+ val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
+ raise Error "Atom.match"
+ in
+ foldl matchArg sub (zip tms1 tms2)
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun unifyArg ((tm1,tm2),sub) = Subst.unify sub tm1 tm2;
+in
+ fun unify sub (p1,tms1) (p2,tms2) =
+ let
+ val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
+ raise Error "Atom.unify"
+ in
+ foldl unifyArg sub (zip tms1 tms2)
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelationName = Name.fromString "=";
+
+val eqRelationArity = 2;
+
+val eqRelation = (eqRelationName,eqRelationArity);
+
+val mkEq = mkBinop eqRelationName;
+
+fun destEq x = destBinop eqRelationName x;
+
+fun isEq x = isBinop eqRelationName x;
+
+fun mkRefl tm = mkEq (tm,tm);
+
+fun destRefl atm =
+ let
+ val (l,r) = destEq atm
+ val _ = Term.equal l r orelse raise Error "Atom.destRefl"
+ in
+ l
+ end;
+
+fun isRefl x = can destRefl x;
+
+fun sym atm =
+ let
+ val (l,r) = destEq atm
+ val _ = not (Term.equal l r) orelse raise Error "Atom.sym: refl"
+ in
+ mkEq (r,l)
+ end;
+
+fun lhs atm = fst (destEq atm);
+
+fun rhs atm = snd (destEq atm);
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,tms) : atom) =
+ foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
+
+fun nonVarTypedSubterms (_,tms) =
+ let
+ fun addArg ((n,arg),acc) =
+ let
+ fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
+ in
+ foldl addTm acc (Term.nonVarTypedSubterms arg)
+ end
+ in
+ foldl addArg [] (enumerate tms)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppMap Term.Fn Term.pp;
+
+val toString = Print.toString pp;
+
+fun fromString s = Term.destFn (Term.fromString s);
+
+val parse = Parse.parseQuotation Term.toString fromString;
+
+end
+
+structure AtomOrdered =
+struct type t = Atom.atom val compare = Atom.compare end
+
+structure AtomMap = KeyMap (AtomOrdered);
+
+structure AtomSet = ElementSet (AtomMap);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/AtomNet.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,48 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature AtomNet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of atom sets that can be efficiently matched and unified. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {fifo : bool}
+
+type 'a atomNet
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val new : parameters -> 'a atomNet
+
+val size : 'a atomNet -> int
+
+val insert : 'a atomNet -> Atom.atom * 'a -> 'a atomNet
+
+val fromList : parameters -> (Atom.atom * 'a) list -> 'a atomNet
+
+val filter : ('a -> bool) -> 'a atomNet -> 'a atomNet
+
+val toString : 'a atomNet -> string
+
+val pp : 'a Print.pp -> 'a atomNet Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries. *)
+(* *)
+(* These function return OVER-APPROXIMATIONS! *)
+(* Filter afterwards to get the precise set of satisfying values. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : 'a atomNet -> Atom.atom -> 'a list
+
+val matched : 'a atomNet -> Atom.atom -> 'a list
+
+val unify : 'a atomNet -> Atom.atom -> 'a list
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/AtomNet.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,59 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure AtomNet :> AtomNet =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun atomToTerm atom = Term.Fn atom;
+
+fun termToAtom (Term.Var _) = raise Bug "AtomNet.termToAtom"
+ | termToAtom (Term.Fn atom) = atom;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of atom sets that can be efficiently matched and unified. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = TermNet.parameters;
+
+type 'a atomNet = 'a TermNet.termNet;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val new = TermNet.new;
+
+val size = TermNet.size;
+
+fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a);
+
+fun fromList parm l = foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
+
+val filter = TermNet.filter;
+
+fun toString net = "AtomNet[" ^ Int.toString (size net) ^ "]";
+
+val pp = TermNet.pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries. *)
+(* *)
+(* These function return OVER-APPROXIMATIONS! *)
+(* Filter afterwards to get the precise set of satisfying values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun match net atm = TermNet.match net (atomToTerm atm);
+
+fun matched net atm = TermNet.matched net (atomToTerm atm);
+
+fun unify net atm = TermNet.unify net (atomToTerm atm);
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Clause.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,107 @@
+(* ========================================================================= *)
+(* CLAUSE = ID + THEOREM *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Clause =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literalOrder =
+ NoLiteralOrder
+ | UnsignedLiteralOrder
+ | PositiveLiteralOrder
+
+type parameters =
+ {ordering : KnuthBendixOrder.kbo,
+ orderLiterals : literalOrder,
+ orderTerms : bool}
+
+type clauseId = int
+
+type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm}
+
+type clause
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val newId : unit -> clauseId
+
+val mk : clauseInfo -> clause
+
+val dest : clause -> clauseInfo
+
+val id : clause -> clauseId
+
+val thm : clause -> Thm.thm
+
+val equalThms : clause -> clause -> bool
+
+val literals : clause -> Thm.clause
+
+val isTautology : clause -> bool
+
+val isContradiction : clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The term ordering is used to cut down inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+val largestLiterals : clause -> LiteralSet.set
+
+val largestEquations :
+ clause -> (Literal.literal * Rewrite.orient * Term.term) list
+
+val largestSubterms :
+ clause -> (Literal.literal * Term.path * Term.term) list
+
+val allSubterms : clause -> (Literal.literal * Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption. *)
+(* ------------------------------------------------------------------------- *)
+
+val subsumes : clause Subsume.subsume -> clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Simplifying rules: these preserve the clause id. *)
+(* ------------------------------------------------------------------------- *)
+
+val freshVars : clause -> clause
+
+val simplify : clause -> clause option
+
+val reduce : Units.units -> clause -> clause
+
+val rewrite : Rewrite.rewrite -> clause -> clause
+
+(* ------------------------------------------------------------------------- *)
+(* Inference rules: these generate new clause ids. *)
+(* ------------------------------------------------------------------------- *)
+
+val factor : clause -> clause list
+
+val resolve : clause * Literal.literal -> clause * Literal.literal -> clause
+
+val paramodulate :
+ clause * Literal.literal * Rewrite.orient * Term.term ->
+ clause * Literal.literal * Term.path * Term.term -> clause
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val showId : bool ref
+
+val pp : clause Print.pp
+
+val toString : clause -> string
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Clause.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,360 @@
+(* ========================================================================= *)
+(* CLAUSE = ID + THEOREM *)
+(* Copyright (c) 2002-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Clause :> Clause =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+val newId =
+ let
+ val r = ref 0
+ in
+ fn () => case r of ref n => let val () = r := n + 1 in n end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of clause. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literalOrder =
+ NoLiteralOrder
+ | UnsignedLiteralOrder
+ | PositiveLiteralOrder;
+
+type parameters =
+ {ordering : KnuthBendixOrder.kbo,
+ orderLiterals : literalOrder,
+ orderTerms : bool};
+
+type clauseId = int;
+
+type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm};
+
+datatype clause = Clause of clauseInfo;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val showId = ref false;
+
+local
+ val ppIdThm = Print.ppPair Print.ppInt Thm.pp;
+in
+ fun pp (Clause {id,thm,...}) =
+ if !showId then ppIdThm (id,thm) else Thm.pp thm;
+end;
+
+fun toString cl = Print.toString pp cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters =
+ {ordering = KnuthBendixOrder.default,
+ orderLiterals = PositiveLiteralOrder,
+ orderTerms = true};
+
+fun mk info = Clause info
+
+fun dest (Clause info) = info;
+
+fun id (Clause {id = i, ...}) = i;
+
+fun thm (Clause {thm = th, ...}) = th;
+
+fun equalThms cl cl' = Thm.equal (thm cl) (thm cl');
+
+fun new parameters thm =
+ Clause {parameters = parameters, id = newId (), thm = thm};
+
+fun literals cl = Thm.clause (thm cl);
+
+fun isTautology (Clause {thm,...}) = Thm.isTautology thm;
+
+fun isContradiction (Clause {thm,...}) = Thm.isContradiction thm;
+
+(* ------------------------------------------------------------------------- *)
+(* The term ordering is used to cut down inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+fun strictlyLess ordering x_y =
+ case KnuthBendixOrder.compare ordering x_y of
+ SOME LESS => true
+ | _ => false;
+
+fun isLargerTerm ({ordering,orderTerms,...} : parameters) l_r =
+ not orderTerms orelse not (strictlyLess ordering l_r);
+
+local
+ fun atomToTerms atm =
+ case total Atom.destEq atm of
+ NONE => [Term.Fn atm]
+ | SOME (l,r) => [l,r];
+
+ fun notStrictlyLess ordering (xs,ys) =
+ let
+ fun less x = List.exists (fn y => strictlyLess ordering (x,y)) ys
+ in
+ not (List.all less xs)
+ end;
+in
+ fun isLargerLiteral ({ordering,orderLiterals,...} : parameters) lits =
+ case orderLiterals of
+ NoLiteralOrder => K true
+ | UnsignedLiteralOrder =>
+ let
+ fun addLit ((_,atm),acc) = atomToTerms atm @ acc
+
+ val tms = LiteralSet.foldl addLit [] lits
+ in
+ fn (_,atm') => notStrictlyLess ordering (atomToTerms atm', tms)
+ end
+ | PositiveLiteralOrder =>
+ case LiteralSet.findl (K true) lits of
+ NONE => K true
+ | SOME (pol,_) =>
+ let
+ fun addLit ((p,atm),acc) =
+ if p = pol then atomToTerms atm @ acc else acc
+
+ val tms = LiteralSet.foldl addLit [] lits
+ in
+ fn (pol',atm') =>
+ if pol <> pol' then pol
+ else notStrictlyLess ordering (atomToTerms atm', tms)
+ end;
+end;
+
+fun largestLiterals (Clause {parameters,thm,...}) =
+ let
+ val litSet = Thm.clause thm
+ val isLarger = isLargerLiteral parameters litSet
+ fun addLit (lit,s) = if isLarger lit then LiteralSet.add s lit else s
+ in
+ LiteralSet.foldr addLit LiteralSet.empty litSet
+ end;
+
+(*MetisTrace6
+val largestLiterals = fn cl =>
+ let
+ val ppResult = LiteralSet.pp
+ val () = Print.trace pp "Clause.largestLiterals: cl" cl
+ val result = largestLiterals cl
+ val () = Print.trace ppResult "Clause.largestLiterals: result" result
+ in
+ result
+ end;
+*)
+
+fun largestEquations (cl as Clause {parameters,...}) =
+ let
+ fun addEq lit ort (l_r as (l,_)) acc =
+ if isLargerTerm parameters l_r then (lit,ort,l) :: acc else acc
+
+ fun addLit (lit,acc) =
+ case total Literal.destEq lit of
+ NONE => acc
+ | SOME (l,r) =>
+ let
+ val acc = addEq lit Rewrite.RightToLeft (r,l) acc
+ val acc = addEq lit Rewrite.LeftToRight (l,r) acc
+ in
+ acc
+ end
+ in
+ LiteralSet.foldr addLit [] (largestLiterals cl)
+ end;
+
+local
+ fun addLit (lit,acc) =
+ let
+ fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
+ in
+ foldl addTm acc (Literal.nonVarTypedSubterms lit)
+ end;
+in
+ fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiterals cl);
+
+ fun allSubterms cl = LiteralSet.foldl addLit [] (literals cl);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Subsumption. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subsumes (subs : clause Subsume.subsume) cl =
+ Subsume.isStrictlySubsumed subs (literals cl);
+
+(* ------------------------------------------------------------------------- *)
+(* Simplifying rules: these preserve the clause id. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freshVars (Clause {parameters,id,thm}) =
+ Clause {parameters = parameters, id = id, thm = Rule.freshVars thm};
+
+fun simplify (Clause {parameters,id,thm}) =
+ case Rule.simplify thm of
+ NONE => NONE
+ | SOME thm => SOME (Clause {parameters = parameters, id = id, thm = thm});
+
+fun reduce units (Clause {parameters,id,thm}) =
+ Clause {parameters = parameters, id = id, thm = Units.reduce units thm};
+
+fun rewrite rewr (cl as Clause {parameters,id,thm}) =
+ let
+ fun simp th =
+ let
+ val {ordering,...} = parameters
+ val cmp = KnuthBendixOrder.compare ordering
+ in
+ Rewrite.rewriteIdRule rewr cmp id th
+ end
+
+(*MetisTrace4
+ val () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr
+ val () = Print.trace Print.ppInt "Clause.rewrite: id" id
+ val () = Print.trace pp "Clause.rewrite: cl" cl
+*)
+
+ val thm =
+ case Rewrite.peek rewr id of
+ NONE => simp thm
+ | SOME ((_,thm),_) => if Rewrite.isReduced rewr then thm else simp thm
+
+ val result = Clause {parameters = parameters, id = id, thm = thm}
+
+(*MetisTrace4
+ val () = Print.trace pp "Clause.rewrite: result" result
+*)
+ in
+ result
+ end
+(*MetisDebug
+ handle Error err => raise Error ("Clause.rewrite:\n" ^ err);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Inference rules: these generate new clause ids. *)
+(* ------------------------------------------------------------------------- *)
+
+fun factor (cl as Clause {parameters,thm,...}) =
+ let
+ val lits = largestLiterals cl
+
+ fun apply sub = new parameters (Thm.subst sub thm)
+ in
+ map apply (Rule.factor' lits)
+ end;
+
+(*MetisTrace5
+val factor = fn cl =>
+ let
+ val () = Print.trace pp "Clause.factor: cl" cl
+ val result = factor cl
+ val () = Print.trace (Print.ppList pp) "Clause.factor: result" result
+ in
+ result
+ end;
+*)
+
+fun resolve (cl1,lit1) (cl2,lit2) =
+ let
+(*MetisTrace5
+ val () = Print.trace pp "Clause.resolve: cl1" cl1
+ val () = Print.trace Literal.pp "Clause.resolve: lit1" lit1
+ val () = Print.trace pp "Clause.resolve: cl2" cl2
+ val () = Print.trace Literal.pp "Clause.resolve: lit2" lit2
+*)
+ val Clause {parameters, thm = th1, ...} = cl1
+ and Clause {thm = th2, ...} = cl2
+ val sub = Literal.unify Subst.empty lit1 (Literal.negate lit2)
+(*MetisTrace5
+ val () = Print.trace Subst.pp "Clause.resolve: sub" sub
+*)
+ val lit1 = Literal.subst sub lit1
+ val lit2 = Literal.negate lit1
+ val th1 = Thm.subst sub th1
+ and th2 = Thm.subst sub th2
+ val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+(*MetisTrace5
+ (trace "Clause.resolve: th1 violates ordering\n"; false) orelse
+*)
+ raise Error "resolve: clause1: ordering constraints"
+ val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+(*MetisTrace5
+ (trace "Clause.resolve: th2 violates ordering\n"; false) orelse
+*)
+ raise Error "resolve: clause2: ordering constraints"
+ val th = Thm.resolve lit1 th1 th2
+(*MetisTrace5
+ val () = Print.trace Thm.pp "Clause.resolve: th" th
+*)
+ val cl = Clause {parameters = parameters, id = newId (), thm = th}
+(*MetisTrace5
+ val () = Print.trace pp "Clause.resolve: cl" cl
+*)
+ in
+ cl
+ end;
+
+fun paramodulate (cl1,lit1,ort1,tm1) (cl2,lit2,path2,tm2) =
+ let
+(*MetisTrace5
+ val () = Print.trace pp "Clause.paramodulate: cl1" cl1
+ val () = Print.trace Literal.pp "Clause.paramodulate: lit1" lit1
+ val () = Print.trace Rewrite.ppOrient "Clause.paramodulate: ort1" ort1
+ val () = Print.trace Term.pp "Clause.paramodulate: tm1" tm1
+ val () = Print.trace pp "Clause.paramodulate: cl2" cl2
+ val () = Print.trace Literal.pp "Clause.paramodulate: lit2" lit2
+ val () = Print.trace Term.ppPath "Clause.paramodulate: path2" path2
+ val () = Print.trace Term.pp "Clause.paramodulate: tm2" tm2
+*)
+ val Clause {parameters, thm = th1, ...} = cl1
+ and Clause {thm = th2, ...} = cl2
+ val sub = Subst.unify Subst.empty tm1 tm2
+ val lit1 = Literal.subst sub lit1
+ and lit2 = Literal.subst sub lit2
+ and th1 = Thm.subst sub th1
+ and th2 = Thm.subst sub th2
+
+ val _ = isLargerLiteral parameters (Thm.clause th1) lit1 orelse
+ raise Error "Clause.paramodulate: with clause: ordering"
+ val _ = isLargerLiteral parameters (Thm.clause th2) lit2 orelse
+ raise Error "Clause.paramodulate: into clause: ordering"
+
+ val eqn = (Literal.destEq lit1, th1)
+ val eqn as (l_r,_) =
+ case ort1 of
+ Rewrite.LeftToRight => eqn
+ | Rewrite.RightToLeft => Rule.symEqn eqn
+(*MetisTrace6
+ val () = Print.trace Rule.ppEquation "Clause.paramodulate: eqn" eqn
+*)
+ val _ = isLargerTerm parameters l_r orelse
+ raise Error "Clause.paramodulate: equation: ordering constraints"
+ val th = Rule.rewrRule eqn lit2 path2 th2
+(*MetisTrace5
+ val () = Print.trace Thm.pp "Clause.paramodulate: th" th
+*)
+ in
+ Clause {parameters = parameters, id = newId (), thm = th}
+ end
+(*MetisTrace5
+ handle Error err =>
+ let
+ val () = trace ("Clause.paramodulate: failed: " ^ err ^ "\n")
+ in
+ raise Error err
+ end;
+*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/ElementSet.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,175 @@
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature ElementSet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements. *)
+(* ------------------------------------------------------------------------- *)
+
+type element
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type set
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val empty : set
+
+val singleton : element -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
+val null : set -> bool
+
+val size : set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+val peek : set -> element -> element option
+
+val member : element -> set -> bool
+
+val pick : set -> element (* an arbitrary element *)
+
+val nth : set -> int -> element (* in the range [0,size-1] *)
+
+val random : set -> element
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+val add : set -> element -> set
+
+val addList : set -> element list -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : set -> element -> set (* must be present *)
+
+val remove : set -> element -> set
+
+val deletePick : set -> element * set
+
+val deleteNth : set -> int -> element * set
+
+val deleteRandom : set -> element * set
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
+
+val union : set -> set -> set
+
+val unionList : set list -> set
+
+val intersect : set -> set -> set
+
+val intersectList : set list -> set
+
+val difference : set -> set -> set
+
+val symmetricDifference : set -> set -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+val filter : (element -> bool) -> set -> set
+
+val partition : (element -> bool) -> set -> set * set
+
+val app : (element -> unit) -> set -> unit
+
+val foldl : (element * 's -> 's) -> 's -> set -> 's
+
+val foldr : (element * 's -> 's) -> 's -> set -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : (element -> bool) -> set -> element option
+
+val findr : (element -> bool) -> set -> element option
+
+val firstl : (element -> 'a option) -> set -> 'a option
+
+val firstr : (element -> 'a option) -> set -> 'a option
+
+val exists : (element -> bool) -> set -> bool
+
+val all : (element -> bool) -> set -> bool
+
+val count : (element -> bool) -> set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : set * set -> order
+
+val equal : set -> set -> bool
+
+val subset : set -> set -> bool
+
+val disjoint : set -> set -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+val transform : (element -> 'a) -> set -> 'a list
+
+val toList : set -> element list
+
+val fromList : element list -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+val mapPartial : (element -> 'a option) -> set -> 'a map
+
+val map : (element -> 'a) -> set -> 'a map
+
+val domain : 'a map -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : set -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets *)
+(* ------------------------------------------------------------------------- *)
+
+type iterator
+
+val mkIterator : set -> iterator option
+
+val mkRevIterator : set -> iterator option
+
+val readIterator : iterator -> element
+
+val advanceIterator : iterator -> iterator option
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/ElementSet.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,347 @@
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+functor ElementSet (KM : KeyMap) :> ElementSet
+where type element = KM.key and type 'a map = 'a KM.map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements. *)
+(* ------------------------------------------------------------------------- *)
+
+type element = KM.key;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map = 'a KM.map;
+
+datatype set = Set of unit map;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun dest (Set m) = m;
+
+fun mapPartial f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.mapPartial mf m
+ end;
+
+fun map f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.map mf m
+ end;
+
+fun domain m = Set (KM.transform (fn _ => ()) m);
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val empty = Set (KM.new ());
+
+fun singleton elt = Set (KM.singleton (elt,()));
+
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun null (Set m) = KM.null m;
+
+fun size (Set m) = KM.size m;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peek (Set m) elt =
+ case KM.peekKey m elt of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE;
+
+fun member elt (Set m) = KM.inDomain elt m;
+
+fun pick (Set m) =
+ let
+ val (elt,_) = KM.pick m
+ in
+ elt
+ end;
+
+fun nth (Set m) n =
+ let
+ val (elt,_) = KM.nth m n
+ in
+ elt
+ end;
+
+fun random (Set m) =
+ let
+ val (elt,_) = KM.random m
+ in
+ elt
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun add (Set m) elt =
+ let
+ val m = KM.insert m (elt,())
+ in
+ Set m
+ end;
+
+local
+ fun uncurriedAdd (elt,set) = add set elt;
+in
+ fun addList set = List.foldl uncurriedAdd set;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Set m) elt =
+ let
+ val m = KM.delete m elt
+ in
+ Set m
+ end;
+
+fun remove (Set m) elt =
+ let
+ val m = KM.remove m elt
+ in
+ Set m
+ end;
+
+fun deletePick (Set m) =
+ let
+ val ((elt,()),m) = KM.deletePick m
+ in
+ (elt, Set m)
+ end;
+
+fun deleteNth (Set m) n =
+ let
+ val ((elt,()),m) = KM.deleteNth m n
+ in
+ (elt, Set m)
+ end;
+
+fun deleteRandom (Set m) =
+ let
+ val ((elt,()),m) = KM.deleteRandom m
+ in
+ (elt, Set m)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
+
+fun union (Set m1) (Set m2) = Set (KM.unionDomain m1 m2);
+
+fun unionList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (KM.unionListDomain ms)
+ end;
+
+fun intersect (Set m1) (Set m2) = Set (KM.intersectDomain m1 m2);
+
+fun intersectList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (KM.intersectListDomain ms)
+ end;
+
+fun difference (Set m1) (Set m2) =
+ Set (KM.differenceDomain m1 m2);
+
+fun symmetricDifference (Set m1) (Set m2) =
+ Set (KM.symmetricDifferenceDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun filter pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m => Set (KM.filter mpred m)
+ end;
+
+fun partition pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m =>
+ let
+ val (m1,m2) = KM.partition mpred m
+ in
+ (Set m1, Set m2)
+ end
+ end;
+
+fun app f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.app mf m
+ end;
+
+fun foldl f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => KM.foldl mf acc m
+ end;
+
+fun foldr f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => KM.foldr mf acc m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case KM.findl mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun findr p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case KM.findr mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun firstl f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.firstl mf m
+ end;
+
+fun firstr f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.firstr mf m
+ end;
+
+fun exists p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.exists mp m
+ end;
+
+fun all p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.all mp m
+ end;
+
+fun count p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.count mp m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compareValue ((),()) = EQUAL;
+
+fun equalValue () () = true;
+
+fun compare (Set m1, Set m2) = KM.compare compareValue (m1,m2);
+
+fun equal (Set m1) (Set m2) = KM.equal equalValue m1 m2;
+
+fun subset (Set m1) (Set m2) = KM.subsetDomain m1 m2;
+
+fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+fun transform f =
+ let
+ fun inc (x,l) = f x :: l
+ in
+ foldr inc []
+ end;
+
+fun toList (Set m) = KM.keys m;
+
+fun fromList elts = addList empty elts;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString set =
+ "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets *)
+(* ------------------------------------------------------------------------- *)
+
+type iterator = unit KM.iterator;
+
+fun mkIterator (Set m) = KM.mkIterator m;
+
+fun mkRevIterator (Set m) = KM.mkRevIterator m;
+
+fun readIterator iter =
+ let
+ val (elt,()) = KM.readIterator iter
+ in
+ elt
+ end;
+
+fun advanceIterator iter = KM.advanceIterator iter;
+
+end
+
+structure IntSet =
+ElementSet (IntMap);
+
+structure IntPairSet =
+ElementSet (IntPairMap);
+
+structure StringSet =
+ElementSet (StringMap);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/FILES Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,40 @@
+Random.sig Random.sml
+Portable.sig PortablePolyml.sml
+Useful.sig Useful.sml
+Lazy.sig Lazy.sml
+Stream.sig Stream.sml
+Ordered.sig Ordered.sml
+Map.sig Map.sml
+KeyMap.sig KeyMap.sml
+Set.sig Set.sml
+ElementSet.sig ElementSet.sml
+Sharing.sig Sharing.sml
+Heap.sig Heap.sml
+Print.sig Print.sml
+Parse.sig Parse.sml
+Options.sig Options.sml
+Name.sig Name.sml
+NameArity.sig NameArity.sml
+Term.sig Term.sml
+Subst.sig Subst.sml
+Atom.sig Atom.sml
+Formula.sig Formula.sml
+Literal.sig Literal.sml
+Thm.sig Thm.sml
+Proof.sig Proof.sml
+Rule.sig Rule.sml
+Normalize.sig Normalize.sml
+Model.sig Model.sml
+Problem.sig Problem.sml
+TermNet.sig TermNet.sml
+AtomNet.sig AtomNet.sml
+LiteralNet.sig LiteralNet.sml
+Subsume.sig Subsume.sml
+KnuthBendixOrder.sig KnuthBendixOrder.sml
+Rewrite.sig Rewrite.sml
+Units.sig Units.sml
+Clause.sig Clause.sml
+Active.sig Active.sml
+Waiting.sig Waiting.sml
+Resolution.sig Resolution.sml
+Tptp.sig Tptp.sml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Formula.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,197 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Formula =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ True
+ | False
+ | Atom of Atom.atom
+ | Not of formula
+ | And of formula * formula
+ | Or of formula * formula
+ | Imp of formula * formula
+ | Iff of formula * formula
+ | Forall of Term.var * formula
+ | Exists of Term.var * formula
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+val mkBoolean : bool -> formula
+
+val destBoolean : formula -> bool
+
+val isBoolean : formula -> bool
+
+val isTrue : formula -> bool
+
+val isFalse : formula -> bool
+
+(* Functions *)
+
+val functions : formula -> NameAritySet.set
+
+val functionNames : formula -> NameSet.set
+
+(* Relations *)
+
+val relations : formula -> NameAritySet.set
+
+val relationNames : formula -> NameSet.set
+
+(* Atoms *)
+
+val destAtom : formula -> Atom.atom
+
+val isAtom : formula -> bool
+
+(* Negations *)
+
+val destNeg : formula -> formula
+
+val isNeg : formula -> bool
+
+val stripNeg : formula -> int * formula
+
+(* Conjunctions *)
+
+val listMkConj : formula list -> formula
+
+val stripConj : formula -> formula list
+
+val flattenConj : formula -> formula list
+
+(* Disjunctions *)
+
+val listMkDisj : formula list -> formula
+
+val stripDisj : formula -> formula list
+
+val flattenDisj : formula -> formula list
+
+(* Equivalences *)
+
+val listMkEquiv : formula list -> formula
+
+val stripEquiv : formula -> formula list
+
+val flattenEquiv : formula -> formula list
+
+(* Universal quantification *)
+
+val destForall : formula -> Term.var * formula
+
+val isForall : formula -> bool
+
+val listMkForall : Term.var list * formula -> formula
+
+val setMkForall : NameSet.set * formula -> formula
+
+val stripForall : formula -> Term.var list * formula
+
+(* Existential quantification *)
+
+val destExists : formula -> Term.var * formula
+
+val isExists : formula -> bool
+
+val listMkExists : Term.var list * formula -> formula
+
+val setMkExists : NameSet.set * formula -> formula
+
+val stripExists : formula -> Term.var list * formula
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : formula -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : formula * formula -> order
+
+val equal : formula -> formula -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> formula -> bool
+
+val freeVars : formula -> NameSet.set
+
+val freeVarsList : formula list -> NameSet.set
+
+val specialize : formula -> formula
+
+val generalize : formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Term.term * Term.term -> formula
+
+val destEq : formula -> Term.term * Term.term
+
+val isEq : formula -> bool
+
+val mkNeq : Term.term * Term.term -> formula
+
+val destNeq : formula -> Term.term * Term.term
+
+val isNeq : formula -> bool
+
+val mkRefl : Term.term -> formula
+
+val destRefl : formula -> Term.term
+
+val isRefl : formula -> bool
+
+val sym : formula -> formula (* raises Error if given a refl *)
+
+val lhs : formula -> Term.term
+
+val rhs : formula -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Splitting goals. *)
+(* ------------------------------------------------------------------------- *)
+
+val splitGoal : formula -> formula list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Parse.quotation
+
+val pp : formula Print.pp
+
+val toString : formula -> string
+
+val fromString : string -> formula
+
+val parse : quotation -> formula
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Formula.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,601 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Formula :> Formula =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ True
+ | False
+ | Atom of Atom.atom
+ | Not of formula
+ | And of formula * formula
+ | Or of formula * formula
+ | Imp of formula * formula
+ | Iff of formula * formula
+ | Forall of Term.var * formula
+ | Exists of Term.var * formula;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+fun mkBoolean true = True
+ | mkBoolean false = False;
+
+fun destBoolean True = true
+ | destBoolean False = false
+ | destBoolean _ = raise Error "destBoolean";
+
+val isBoolean = can destBoolean;
+
+fun isTrue fm =
+ case fm of
+ True => true
+ | _ => false;
+
+fun isFalse fm =
+ case fm of
+ False => true
+ | _ => false;
+
+(* Functions *)
+
+local
+ fun funcs fs [] = fs
+ | funcs fs (True :: fms) = funcs fs fms
+ | funcs fs (False :: fms) = funcs fs fms
+ | funcs fs (Atom atm :: fms) =
+ funcs (NameAritySet.union (Atom.functions atm) fs) fms
+ | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+ | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+ | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+ fun functions fm = funcs NameAritySet.empty [fm];
+end;
+
+local
+ fun funcs fs [] = fs
+ | funcs fs (True :: fms) = funcs fs fms
+ | funcs fs (False :: fms) = funcs fs fms
+ | funcs fs (Atom atm :: fms) =
+ funcs (NameSet.union (Atom.functionNames atm) fs) fms
+ | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+ | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+ | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+ fun functionNames fm = funcs NameSet.empty [fm];
+end;
+
+(* Relations *)
+
+local
+ fun rels fs [] = fs
+ | rels fs (True :: fms) = rels fs fms
+ | rels fs (False :: fms) = rels fs fms
+ | rels fs (Atom atm :: fms) =
+ rels (NameAritySet.add fs (Atom.relation atm)) fms
+ | rels fs (Not p :: fms) = rels fs (p :: fms)
+ | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+ | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+ fun relations fm = rels NameAritySet.empty [fm];
+end;
+
+local
+ fun rels fs [] = fs
+ | rels fs (True :: fms) = rels fs fms
+ | rels fs (False :: fms) = rels fs fms
+ | rels fs (Atom atm :: fms) = rels (NameSet.add fs (Atom.name atm)) fms
+ | rels fs (Not p :: fms) = rels fs (p :: fms)
+ | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+ | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+ fun relationNames fm = rels NameSet.empty [fm];
+end;
+
+(* Atoms *)
+
+fun destAtom (Atom atm) = atm
+ | destAtom _ = raise Error "Formula.destAtom";
+
+val isAtom = can destAtom;
+
+(* Negations *)
+
+fun destNeg (Not p) = p
+ | destNeg _ = raise Error "Formula.destNeg";
+
+val isNeg = can destNeg;
+
+val stripNeg =
+ let
+ fun strip n (Not fm) = strip (n + 1) fm
+ | strip n fm = (n,fm)
+ in
+ strip 0
+ end;
+
+(* Conjunctions *)
+
+fun listMkConj fms =
+ case rev fms of [] => True | fm :: fms => foldl And fm fms;
+
+local
+ fun strip cs (And (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripConj True = []
+ | stripConj fm = strip [] fm;
+end;
+
+val flattenConj =
+ let
+ fun flat acc [] = acc
+ | flat acc (And (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (True :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Disjunctions *)
+
+fun listMkDisj fms =
+ case rev fms of [] => False | fm :: fms => foldl Or fm fms;
+
+local
+ fun strip cs (Or (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripDisj False = []
+ | stripDisj fm = strip [] fm;
+end;
+
+val flattenDisj =
+ let
+ fun flat acc [] = acc
+ | flat acc (Or (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (False :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Equivalences *)
+
+fun listMkEquiv fms =
+ case rev fms of [] => True | fm :: fms => foldl Iff fm fms;
+
+local
+ fun strip cs (Iff (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripEquiv True = []
+ | stripEquiv fm = strip [] fm;
+end;
+
+val flattenEquiv =
+ let
+ fun flat acc [] = acc
+ | flat acc (Iff (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (True :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Universal quantifiers *)
+
+fun destForall (Forall v_f) = v_f
+ | destForall _ = raise Error "destForall";
+
+val isForall = can destForall;
+
+fun listMkForall ([],body) = body
+ | listMkForall (v :: vs, body) = Forall (v, listMkForall (vs,body));
+
+fun setMkForall (vs,body) = NameSet.foldr Forall body vs;
+
+local
+ fun strip vs (Forall (v,b)) = strip (v :: vs) b
+ | strip vs tm = (rev vs, tm);
+in
+ val stripForall = strip [];
+end;
+
+(* Existential quantifiers *)
+
+fun destExists (Exists v_f) = v_f
+ | destExists _ = raise Error "destExists";
+
+val isExists = can destExists;
+
+fun listMkExists ([],body) = body
+ | listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body));
+
+fun setMkExists (vs,body) = NameSet.foldr Exists body vs;
+
+local
+ fun strip vs (Exists (v,b)) = strip (v :: vs) b
+ | strip vs tm = (rev vs, tm);
+in
+ val stripExists = strip [];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun sz n [] = n
+ | sz n (True :: fms) = sz (n + 1) fms
+ | sz n (False :: fms) = sz (n + 1) fms
+ | sz n (Atom atm :: fms) = sz (n + Atom.symbols atm) fms
+ | sz n (Not p :: fms) = sz (n + 1) (p :: fms)
+ | sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms)
+ | sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms);
+in
+ fun symbols fm = sz 0 [fm];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun cmp [] = EQUAL
+ | cmp (f1_f2 :: fs) =
+ if Portable.pointerEqual f1_f2 then cmp fs
+ else
+ case f1_f2 of
+ (True,True) => cmp fs
+ | (True,_) => LESS
+ | (_,True) => GREATER
+ | (False,False) => cmp fs
+ | (False,_) => LESS
+ | (_,False) => GREATER
+ | (Atom atm1, Atom atm2) =>
+ (case Atom.compare (atm1,atm2) of
+ LESS => LESS
+ | EQUAL => cmp fs
+ | GREATER => GREATER)
+ | (Atom _, _) => LESS
+ | (_, Atom _) => GREATER
+ | (Not p1, Not p2) => cmp ((p1,p2) :: fs)
+ | (Not _, _) => LESS
+ | (_, Not _) => GREATER
+ | (And (p1,q1), And (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+ | (And _, _) => LESS
+ | (_, And _) => GREATER
+ | (Or (p1,q1), Or (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+ | (Or _, _) => LESS
+ | (_, Or _) => GREATER
+ | (Imp (p1,q1), Imp (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+ | (Imp _, _) => LESS
+ | (_, Imp _) => GREATER
+ | (Iff (p1,q1), Iff (p2,q2)) => cmp ((p1,p2) :: (q1,q2) :: fs)
+ | (Iff _, _) => LESS
+ | (_, Iff _) => GREATER
+ | (Forall (v1,p1), Forall (v2,p2)) =>
+ (case Name.compare (v1,v2) of
+ LESS => LESS
+ | EQUAL => cmp ((p1,p2) :: fs)
+ | GREATER => GREATER)
+ | (Forall _, Exists _) => LESS
+ | (Exists _, Forall _) => GREATER
+ | (Exists (v1,p1), Exists (v2,p2)) =>
+ (case Name.compare (v1,v2) of
+ LESS => LESS
+ | EQUAL => cmp ((p1,p2) :: fs)
+ | GREATER => GREATER);
+in
+ fun compare fm1_fm2 = cmp [fm1_fm2];
+end;
+
+fun equal fm1 fm2 = compare (fm1,fm2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v =
+ let
+ fun f [] = false
+ | f (True :: fms) = f fms
+ | f (False :: fms) = f fms
+ | f (Atom atm :: fms) = Atom.freeIn v atm orelse f fms
+ | f (Not p :: fms) = f (p :: fms)
+ | f (And (p,q) :: fms) = f (p :: q :: fms)
+ | f (Or (p,q) :: fms) = f (p :: q :: fms)
+ | f (Imp (p,q) :: fms) = f (p :: q :: fms)
+ | f (Iff (p,q) :: fms) = f (p :: q :: fms)
+ | f (Forall (w,p) :: fms) =
+ if Name.equal v w then f fms else f (p :: fms)
+ | f (Exists (w,p) :: fms) =
+ if Name.equal v w then f fms else f (p :: fms)
+ in
+ fn fm => f [fm]
+ end;
+
+local
+ fun fv vs [] = vs
+ | fv vs ((_,True) :: fms) = fv vs fms
+ | fv vs ((_,False) :: fms) = fv vs fms
+ | fv vs ((bv, Atom atm) :: fms) =
+ fv (NameSet.union vs (NameSet.difference (Atom.freeVars atm) bv)) fms
+ | fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms)
+ | fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms)
+ | fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms);
+
+ fun add (fm,vs) = fv vs [(NameSet.empty,fm)];
+in
+ fun freeVars fm = add (fm,NameSet.empty);
+
+ fun freeVarsList fms = List.foldl add NameSet.empty fms;
+end;
+
+fun specialize fm = snd (stripForall fm);
+
+fun generalize fm = listMkForall (NameSet.toList (freeVars fm), fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun substCheck sub fm = if Subst.null sub then fm else substFm sub fm
+
+ and substFm sub fm =
+ case fm of
+ True => fm
+ | False => fm
+ | Atom (p,tms) =>
+ let
+ val tms' = Sharing.map (Subst.subst sub) tms
+ in
+ if Portable.pointerEqual (tms,tms') then fm else Atom (p,tms')
+ end
+ | Not p =>
+ let
+ val p' = substFm sub p
+ in
+ if Portable.pointerEqual (p,p') then fm else Not p'
+ end
+ | And (p,q) => substConn sub fm And p q
+ | Or (p,q) => substConn sub fm Or p q
+ | Imp (p,q) => substConn sub fm Imp p q
+ | Iff (p,q) => substConn sub fm Iff p q
+ | Forall (v,p) => substQuant sub fm Forall v p
+ | Exists (v,p) => substQuant sub fm Exists v p
+
+ and substConn sub fm conn p q =
+ let
+ val p' = substFm sub p
+ and q' = substFm sub q
+ in
+ if Portable.pointerEqual (p,p') andalso
+ Portable.pointerEqual (q,q')
+ then fm
+ else conn (p',q')
+ end
+
+ and substQuant sub fm quant v p =
+ let
+ val v' =
+ let
+ fun f (w,s) =
+ if Name.equal w v then s
+ else
+ case Subst.peek sub w of
+ NONE => NameSet.add s w
+ | SOME tm => NameSet.union s (Term.freeVars tm)
+
+ val vars = freeVars p
+ val vars = NameSet.foldl f NameSet.empty vars
+ in
+ Term.variantPrime vars v
+ end
+
+ val sub =
+ if Name.equal v v' then Subst.remove sub (NameSet.singleton v)
+ else Subst.insert sub (v, Term.Var v')
+
+ val p' = substCheck sub p
+ in
+ if Name.equal v v' andalso Portable.pointerEqual (p,p') then fm
+ else quant (v',p')
+ end;
+in
+ val subst = substCheck;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq a_b = Atom (Atom.mkEq a_b);
+
+fun destEq fm = Atom.destEq (destAtom fm);
+
+val isEq = can destEq;
+
+fun mkNeq a_b = Not (mkEq a_b);
+
+fun destNeq (Not fm) = destEq fm
+ | destNeq _ = raise Error "Formula.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = Atom (Atom.mkRefl tm);
+
+fun destRefl fm = Atom.destRefl (destAtom fm);
+
+val isRefl = can destRefl;
+
+fun sym fm = Atom (Atom.sym (destAtom fm));
+
+fun lhs fm = fst (destEq fm);
+
+fun rhs fm = snd (destEq fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Parse.quotation;
+
+val truthName = Name.fromString "T"
+and falsityName = Name.fromString "F"
+and conjunctionName = Name.fromString "/\\"
+and disjunctionName = Name.fromString "\\/"
+and implicationName = Name.fromString "==>"
+and equivalenceName = Name.fromString "<=>"
+and universalName = Name.fromString "!"
+and existentialName = Name.fromString "?";
+
+local
+ fun demote True = Term.Fn (truthName,[])
+ | demote False = Term.Fn (falsityName,[])
+ | demote (Atom (p,tms)) = Term.Fn (p,tms)
+ | demote (Not p) =
+ let
+ val ref s = Term.negation
+ in
+ Term.Fn (Name.fromString s, [demote p])
+ end
+ | demote (And (p,q)) = Term.Fn (conjunctionName, [demote p, demote q])
+ | demote (Or (p,q)) = Term.Fn (disjunctionName, [demote p, demote q])
+ | demote (Imp (p,q)) = Term.Fn (implicationName, [demote p, demote q])
+ | demote (Iff (p,q)) = Term.Fn (equivalenceName, [demote p, demote q])
+ | demote (Forall (v,b)) = Term.Fn (universalName, [Term.Var v, demote b])
+ | demote (Exists (v,b)) =
+ Term.Fn (existentialName, [Term.Var v, demote b]);
+in
+ fun pp fm = Term.pp (demote fm);
+end;
+
+val toString = Print.toString pp;
+
+local
+ fun isQuant [Term.Var _, _] = true
+ | isQuant _ = false;
+
+ fun promote (Term.Var v) = Atom (v,[])
+ | promote (Term.Fn (f,tms)) =
+ if Name.equal f truthName andalso null tms then
+ True
+ else if Name.equal f falsityName andalso null tms then
+ False
+ else if Name.toString f = !Term.negation andalso length tms = 1 then
+ Not (promote (hd tms))
+ else if Name.equal f conjunctionName andalso length tms = 2 then
+ And (promote (hd tms), promote (List.nth (tms,1)))
+ else if Name.equal f disjunctionName andalso length tms = 2 then
+ Or (promote (hd tms), promote (List.nth (tms,1)))
+ else if Name.equal f implicationName andalso length tms = 2 then
+ Imp (promote (hd tms), promote (List.nth (tms,1)))
+ else if Name.equal f equivalenceName andalso length tms = 2 then
+ Iff (promote (hd tms), promote (List.nth (tms,1)))
+ else if Name.equal f universalName andalso isQuant tms then
+ Forall (Term.destVar (hd tms), promote (List.nth (tms,1)))
+ else if Name.equal f existentialName andalso isQuant tms then
+ Exists (Term.destVar (hd tms), promote (List.nth (tms,1)))
+ else
+ Atom (f,tms);
+in
+ fun fromString s = promote (Term.fromString s);
+end;
+
+val parse = Parse.parseQuotation toString fromString;
+
+(* ------------------------------------------------------------------------- *)
+(* Splitting goals. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun add_asms asms goal =
+ if null asms then goal else Imp (listMkConj (rev asms), goal);
+
+ fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
+
+ fun split asms pol fm =
+ case (pol,fm) of
+ (* Positive splittables *)
+ (true,True) => []
+ | (true, Not f) => split asms false f
+ | (true, And (f1,f2)) => split asms true f1 @ split (f1 :: asms) true f2
+ | (true, Or (f1,f2)) => split (Not f1 :: asms) true f2
+ | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
+ | (true, Iff (f1,f2)) =>
+ split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
+ | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+ (* Negative splittables *)
+ | (false,False) => []
+ | (false, Not f) => split asms true f
+ | (false, And (f1,f2)) => split (f1 :: asms) false f2
+ | (false, Or (f1,f2)) =>
+ split asms false f1 @ split (Not f1 :: asms) false f2
+ | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
+ | (false, Iff (f1,f2)) =>
+ split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
+ | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+ (* Unsplittables *)
+ | _ => [add_asms asms (if pol then fm else Not fm)];
+in
+ fun splitGoal fm = split [] true fm;
+end;
+
+(*MetisTrace3
+val splitGoal = fn fm =>
+ let
+ val result = splitGoal fm
+ val () = Print.trace pp "Formula.splitGoal: fm" fm
+ val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
+ in
+ result
+ end;
+*)
+
+end
+
+structure FormulaOrdered =
+struct type t = Formula.formula val compare = Formula.compare end
+
+structure FormulaMap = KeyMap (FormulaOrdered);
+
+structure FormulaSet = ElementSet (FormulaMap);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Heap.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,31 @@
+(* ========================================================================= *)
+(* A HEAP DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Heap =
+sig
+
+type 'a heap
+
+val new : ('a * 'a -> order) -> 'a heap
+
+val add : 'a heap -> 'a -> 'a heap
+
+val null : 'a heap -> bool
+
+val top : 'a heap -> 'a (* raises Empty *)
+
+val remove : 'a heap -> 'a * 'a heap (* raises Empty *)
+
+val size : 'a heap -> int
+
+val app : ('a -> unit) -> 'a heap -> unit
+
+val toList : 'a heap -> 'a list
+
+val toStream : 'a heap -> 'a Stream.stream
+
+val toString : 'a heap -> string
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Heap.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,77 @@
+(* ========================================================================= *)
+(* A HEAP DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Heap :> Heap =
+struct
+
+(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)
+
+datatype 'a node = E | T of int * 'a * 'a node * 'a node;
+
+datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
+
+fun rank E = 0
+ | rank (T (r,_,_,_)) = r;
+
+fun makeT (x,a,b) =
+ if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);
+
+fun merge cmp =
+ let
+ fun mrg (h,E) = h
+ | mrg (E,h) = h
+ | mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) =
+ case cmp (x,y) of
+ GREATER => makeT (y, a2, mrg (h1,b2))
+ | _ => makeT (x, a1, mrg (b1,h2))
+ in
+ mrg
+ end;
+
+fun new cmp = Heap (cmp,0,E);
+
+fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
+
+fun size (Heap (_, n, _)) = n;
+
+fun null h = size h = 0;
+
+fun top (Heap (_,_,E)) = raise Empty
+ | top (Heap (_, _, T (_,x,_,_))) = x;
+
+fun remove (Heap (_,_,E)) = raise Empty
+ | remove (Heap (f, n, T (_,x,a,b))) = (x, Heap (f, n - 1, merge f (a,b)));
+
+fun app f =
+ let
+ fun ap [] = ()
+ | ap (E :: rest) = ap rest
+ | ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest))
+ in
+ fn Heap (_,_,a) => ap [a]
+ end;
+
+fun toList h =
+ if null h then []
+ else
+ let
+ val (x,h) = remove h
+ in
+ x :: toList h
+ end;
+
+fun toStream h =
+ if null h then Stream.Nil
+ else
+ let
+ val (x,h) = remove h
+ in
+ Stream.Cons (x, fn () => toStream h)
+ end;
+
+fun toString h =
+ "Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KeyMap.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,196 @@
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature KeyMap =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of map keys. *)
+(* ------------------------------------------------------------------------- *)
+
+type key
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val new : unit -> 'a map
+
+val singleton : key * 'a -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+val null : 'a map -> bool
+
+val size : 'a map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+val peekKey : 'a map -> key -> (key * 'a) option
+
+val peek : 'a map -> key -> 'a option
+
+val get : 'a map -> key -> 'a (* raises Error *)
+
+val pick : 'a map -> key * 'a (* an arbitrary key/value pair *)
+
+val nth : 'a map -> int -> key * 'a (* in the range [0,size-1] *)
+
+val random : 'a map -> key * 'a
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+val insert : 'a map -> key * 'a -> 'a map
+
+val insertList : 'a map -> (key * 'a) list -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : 'a map -> key -> 'a map (* must be present *)
+
+val remove : 'a map -> key -> 'a map
+
+val deletePick : 'a map -> (key * 'a) * 'a map
+
+val deleteNth : 'a map -> int -> (key * 'a) * 'a map
+
+val deleteRandom : 'a map -> (key * 'a) * 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+val merge :
+ {first : key * 'a -> 'c option,
+ second : key * 'b -> 'c option,
+ both : (key * 'a) * (key * 'b) -> 'c option} ->
+ 'a map -> 'b map -> 'c map
+
+val union :
+ ((key * 'a) * (key * 'a) -> 'a option) ->
+ 'a map -> 'a map -> 'a map
+
+val intersect :
+ ((key * 'a) * (key * 'b) -> 'c option) ->
+ 'a map -> 'b map -> 'c map
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+val inDomain : key -> 'a map -> bool
+
+val unionDomain : 'a map -> 'a map -> 'a map
+
+val unionListDomain : 'a map list -> 'a map
+
+val intersectDomain : 'a map -> 'a map -> 'a map
+
+val intersectListDomain : 'a map list -> 'a map
+
+val differenceDomain : 'a map -> 'a map -> 'a map
+
+val symmetricDifferenceDomain : 'a map -> 'a map -> 'a map
+
+val equalDomain : 'a map -> 'a map -> bool
+
+val subsetDomain : 'a map -> 'a map -> bool
+
+val disjointDomain : 'a map -> 'a map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+val mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
+
+val map : (key * 'a -> 'b) -> 'a map -> 'b map
+
+val app : (key * 'a -> unit) -> 'a map -> unit
+
+val transform : ('a -> 'b) -> 'a map -> 'b map
+
+val filter : (key * 'a -> bool) -> 'a map -> 'a map
+
+val partition :
+ (key * 'a -> bool) -> 'a map -> 'a map * 'a map
+
+val foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
+
+val foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
+
+val findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
+
+val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
+
+val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
+
+val exists : (key * 'a -> bool) -> 'a map -> bool
+
+val all : (key * 'a -> bool) -> 'a map -> bool
+
+val count : (key * 'a -> bool) -> 'a map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
+
+val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+val keys : 'a map -> key list
+
+val values : 'a map -> 'a list
+
+val toList : 'a map -> (key * 'a) list
+
+val fromList : (key * 'a) list -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : 'a map -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a iterator
+
+val mkIterator : 'a map -> 'a iterator option
+
+val mkRevIterator : 'a map -> 'a iterator option
+
+val readIterator : 'a iterator -> key * 'a
+
+val advanceIterator : 'a iterator -> 'a iterator option
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KeyMap.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1442 @@
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing from the input signature. *)
+(* ------------------------------------------------------------------------- *)
+
+type key = Key.t;
+
+val compareKey = Key.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = Portable.randomWord;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting a comparison function to an equality function. *)
+(* ------------------------------------------------------------------------- *)
+
+fun equalKey key1 key2 = compareKey (key1,key2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Priorities. *)
+(* ------------------------------------------------------------------------- *)
+
+type priority = Word.word;
+
+val randomPriority = randomWord;
+
+val comparePriority = Word.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Priority search trees. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value tree =
+ E
+ | T of 'value node
+
+and 'value node =
+ Node of
+ {size : int,
+ priority : priority,
+ left : 'value tree,
+ key : key,
+ value : 'value,
+ right : 'value tree};
+
+fun lowerPriorityNode node1 node2 =
+ let
+ val Node {priority = p1, ...} = node1
+ and Node {priority = p2, ...} = node2
+ in
+ comparePriority (p1,p2) = LESS
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+local
+ fun checkSizes tree =
+ case tree of
+ E => 0
+ | T (Node {size,left,right,...}) =>
+ let
+ val l = checkSizes left
+ and r = checkSizes right
+
+ val () = if l + 1 + r = size then () else raise Bug "wrong size"
+ in
+ size
+ end;
+
+ fun checkSorted x tree =
+ case tree of
+ E => x
+ | T (Node {left,key,right,...}) =>
+ let
+ val x = checkSorted x left
+
+ val () =
+ case x of
+ NONE => ()
+ | SOME k =>
+ case compareKey (k,key) of
+ LESS => ()
+ | EQUAL => raise Bug "duplicate keys"
+ | GREATER => raise Bug "unsorted"
+
+ val x = SOME key
+ in
+ checkSorted x right
+ end;
+
+ fun checkPriorities tree =
+ case tree of
+ E => NONE
+ | T node =>
+ let
+ val Node {left,right,...} = node
+
+ val () =
+ case checkPriorities left of
+ NONE => ()
+ | SOME lnode =>
+ if not (lowerPriorityNode node lnode) then ()
+ else raise Bug "left child has greater priority"
+
+ val () =
+ case checkPriorities right of
+ NONE => ()
+ | SOME rnode =>
+ if not (lowerPriorityNode node rnode) then ()
+ else raise Bug "right child has greater priority"
+ in
+ SOME node
+ end;
+in
+ fun treeCheckInvariants tree =
+ let
+ val _ = checkSizes tree
+
+ val _ = checkSorted NONE tree
+
+ val _ = checkPriorities tree
+ in
+ tree
+ end
+ handle Error err => raise Bug err;
+end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Tree operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNew () = E;
+
+fun nodeSize (Node {size = x, ...}) = x;
+
+fun treeSize tree =
+ case tree of
+ E => 0
+ | T x => nodeSize x;
+
+fun mkNode priority left key value right =
+ let
+ val size = treeSize left + 1 + treeSize right
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+fun mkTree priority left key value right =
+ let
+ val node = mkNode priority left key value right
+ in
+ T node
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extracting the left and right spines of a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeLeftSpine acc tree =
+ case tree of
+ E => acc
+ | T node => nodeLeftSpine acc node
+
+and nodeLeftSpine acc node =
+ let
+ val Node {left,...} = node
+ in
+ treeLeftSpine (node :: acc) left
+ end;
+
+fun treeRightSpine acc tree =
+ case tree of
+ E => acc
+ | T node => nodeRightSpine acc node
+
+and nodeRightSpine acc node =
+ let
+ val Node {right,...} = node
+ in
+ treeRightSpine (node :: acc) right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Singleton trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkNodeSingleton priority key value =
+ let
+ val size = 1
+ and left = E
+ and right = E
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+fun nodeSingleton (key,value) =
+ let
+ val priority = randomPriority ()
+ in
+ mkNodeSingleton priority key value
+ end;
+
+fun treeSingleton key_value =
+ let
+ val node = nodeSingleton key_value
+ in
+ T node
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees, where every element of the first tree is less than *)
+(* every element of the second tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeAppend tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 =>
+ if lowerPriorityNode node1 node2 then
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val left = treeAppend tree1 left
+ in
+ mkTree priority left key value right
+ end
+ else
+ let
+ val Node {priority,left,key,value,right,...} = node1
+
+ val right = treeAppend right tree2
+ in
+ mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees and a node, where every element of the first tree is *)
+(* less than the node, which in turn is less than every element of the *)
+(* second tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeCombine left node right =
+ let
+ val left_node = treeAppend left (T node)
+ in
+ treeAppend left_node right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeek pkey tree =
+ case tree of
+ E => NONE
+ | T node => nodePeek pkey node
+
+and nodePeek pkey node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeek pkey left
+ | EQUAL => SOME value
+ | GREATER => treePeek pkey right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree paths. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Generating a path by searching a tree for a key/value pair *)
+
+fun treePeekPath pkey path tree =
+ case tree of
+ E => (path,NONE)
+ | T node => nodePeekPath pkey path node
+
+and nodePeekPath pkey path node =
+ let
+ val Node {left,key,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeekPath pkey ((true,node) :: path) left
+ | EQUAL => (path, SOME node)
+ | GREATER => treePeekPath pkey ((false,node) :: path) right
+ end;
+
+(* A path splits a tree into left/right components *)
+
+fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
+ let
+ val Node {priority,left,key,value,right,...} = node
+ in
+ if wentLeft then (leftTree, mkTree priority rightTree key value right)
+ else (mkTree priority left key value leftTree, rightTree)
+ end;
+
+fun addSidesPath left_right = List.foldl addSidePath left_right;
+
+fun mkSidesPath path = addSidesPath (E,E) path;
+
+(* Updating the subtree at a path *)
+
+local
+ fun updateTree ((wentLeft,node),tree) =
+ let
+ val Node {priority,left,key,value,right,...} = node
+ in
+ if wentLeft then mkTree priority tree key value right
+ else mkTree priority left key value tree
+ end;
+in
+ fun updateTreePath tree = List.foldl updateTree tree;
+end;
+
+(* Inserting a new node at a path position *)
+
+fun insertNodePath node =
+ let
+ fun insert left_right path =
+ case path of
+ [] =>
+ let
+ val (left,right) = left_right
+ in
+ treeCombine left node right
+ end
+ | (step as (_,snode)) :: rest =>
+ if lowerPriorityNode snode node then
+ let
+ val left_right = addSidePath (step,left_right)
+ in
+ insert left_right rest
+ end
+ else
+ let
+ val (left,right) = left_right
+
+ val tree = treeCombine left node right
+ in
+ updateTreePath tree path
+ end
+ in
+ insert (E,E)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Using a key to split a node into three components: the keys comparing *)
+(* less than the supplied key, an optional equal key, and the keys comparing *)
+(* greater. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePartition pkey node =
+ let
+ val (path,pnode) = nodePeekPath pkey [] node
+ in
+ case pnode of
+ NONE =>
+ let
+ val (left,right) = mkSidesPath path
+ in
+ (left,NONE,right)
+ end
+ | SOME node =>
+ let
+ val Node {left,key,value,right,...} = node
+
+ val (left,right) = addSidesPath (left,right) path
+ in
+ (left, SOME (key,value), right)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a key/value pair. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeekKey pkey tree =
+ case tree of
+ E => NONE
+ | T node => nodePeekKey pkey node
+
+and nodePeekKey pkey node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeekKey pkey left
+ | EQUAL => SOME (key,value)
+ | GREATER => treePeekKey pkey right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Inserting new key/values into the tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeInsert key_value tree =
+ let
+ val (key,value) = key_value
+
+ val (path,inode) = treePeekPath key [] tree
+ in
+ case inode of
+ NONE =>
+ let
+ val node = nodeSingleton (key,value)
+ in
+ insertNodePath node path
+ end
+ | SOME node =>
+ let
+ val Node {size,priority,left,right,...} = node
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ updateTreePath (T node) path
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Deleting key/value pairs: it raises an exception if the supplied key is *)
+(* not present. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDelete dkey tree =
+ case tree of
+ E => raise Bug "KeyMap.delete: element not found"
+ | T node => nodeDelete dkey node
+
+and nodeDelete dkey node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+ in
+ case compareKey (dkey,key) of
+ LESS =>
+ let
+ val size = size - 1
+ and left = treeDelete dkey left
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ T node
+ end
+ | EQUAL => treeAppend left right
+ | GREATER =>
+ let
+ val size = size - 1
+ and right = treeDelete dkey right
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ T node
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Partial map is the basic operation for preserving tree structure. *)
+(* It applies its argument function to the elements *in order*. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMapPartial f tree =
+ case tree of
+ E => E
+ | T node => nodeMapPartial f node
+
+and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
+ let
+ val left = treeMapPartial f left
+ and vo = f (key,value)
+ and right = treeMapPartial f right
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value => mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping tree values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMap f tree =
+ case tree of
+ E => E
+ | T node => T (nodeMap f node)
+
+and nodeMap f node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+
+ val left = treeMap f left
+ and value = f (key,value)
+ and right = treeMap f right
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Merge is the basic operation for joining two trees. Note that the merged *)
+(* key is always the one from the second map. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMerge f1 f2 fb tree1 tree2 =
+ case tree1 of
+ E => treeMapPartial f2 tree2
+ | T node1 =>
+ case tree2 of
+ E => treeMapPartial f1 tree1
+ | T node2 => nodeMerge f1 f2 fb node1 node2
+
+and nodeMerge f1 f2 fb node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition key node1
+
+ val left = treeMerge f1 f2 fb l left
+ and right = treeMerge f1 f2 fb r right
+
+ val vo =
+ case kvo of
+ NONE => f2 (key,value)
+ | SOME kv => fb (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value =>
+ let
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnion f f2 tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 => nodeUnion f f2 node1 node2
+
+and nodeUnion f f2 node1 node2 =
+ if pointerEqual (node1,node2) then nodeMapPartial f2 node1
+ else
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition key node1
+
+ val left = treeUnion f f2 l left
+ and right = treeUnion f f2 r right
+
+ val vo =
+ case kvo of
+ NONE => SOME value
+ | SOME kv => f (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value =>
+ let
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersect f t1 t2 =
+ case t1 of
+ E => E
+ | T n1 =>
+ case t2 of
+ E => E
+ | T n2 => nodeIntersect f n1 n2
+
+and nodeIntersect f n1 n2 =
+ let
+ val Node {priority,left,key,value,right,...} = n2
+
+ val (l,kvo,r) = nodePartition key n1
+
+ val left = treeIntersect f l left
+ and right = treeIntersect f r right
+
+ val vo =
+ case kvo of
+ NONE => NONE
+ | SOME kv => f (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value => mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees which simply chooses the second value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnionDomain tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 =>
+ if pointerEqual (node1,node2) then tree2
+ else nodeUnionDomain node1 node2
+
+and nodeUnionDomain node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,_,r) = nodePartition key node1
+
+ val left = treeUnionDomain l left
+ and right = treeUnionDomain r right
+
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees which simply chooses the second value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersectDomain tree1 tree2 =
+ case tree1 of
+ E => E
+ | T node1 =>
+ case tree2 of
+ E => E
+ | T node2 =>
+ if pointerEqual (node1,node2) then tree2
+ else nodeIntersectDomain node1 node2
+
+and nodeIntersectDomain node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition key node1
+
+ val left = treeIntersectDomain l left
+ and right = treeIntersectDomain r right
+ in
+ if Option.isSome kvo then mkTree priority left key value right
+ else treeAppend left right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A difference operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDifferenceDomain t1 t2 =
+ case t1 of
+ E => E
+ | T n1 =>
+ case t2 of
+ E => t1
+ | T n2 => nodeDifferenceDomain n1 n2
+
+and nodeDifferenceDomain n1 n2 =
+ if pointerEqual (n1,n2) then E
+ else
+ let
+ val Node {priority,left,key,value,right,...} = n1
+
+ val (l,kvo,r) = nodePartition key n2
+
+ val left = treeDifferenceDomain left l
+ and right = treeDifferenceDomain right r
+ in
+ if Option.isSome kvo then treeAppend left right
+ else mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A subset operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeSubsetDomain tree1 tree2 =
+ case tree1 of
+ E => true
+ | T node1 =>
+ case tree2 of
+ E => false
+ | T node2 => nodeSubsetDomain node1 node2
+
+and nodeSubsetDomain node1 node2 =
+ pointerEqual (node1,node2) orelse
+ let
+ val Node {size,left,key,right,...} = node1
+ in
+ size <= nodeSize node2 andalso
+ let
+ val (l,kvo,r) = nodePartition key node2
+ in
+ Option.isSome kvo andalso
+ treeSubsetDomain left l andalso
+ treeSubsetDomain right r
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Picking an arbitrary key/value pair from a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePick node =
+ let
+ val Node {key,value,...} = node
+ in
+ (key,value)
+ end;
+
+fun treePick tree =
+ case tree of
+ E => raise Bug "KeyMap.treePick"
+ | T node => nodePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing an arbitrary key/value pair from a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodeDeletePick node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ ((key,value), treeAppend left right)
+ end;
+
+fun treeDeletePick tree =
+ case tree of
+ E => raise Bug "KeyMap.treeDeletePick"
+ | T node => nodeDeletePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Finding the nth smallest key/value (counting from 0). *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNth n tree =
+ case tree of
+ E => raise Bug "KeyMap.treeNth"
+ | T node => nodeNth n node
+
+and nodeNth n node =
+ let
+ val Node {left,key,value,right,...} = node
+
+ val k = treeSize left
+ in
+ if n = k then (key,value)
+ else if n < k then treeNth n left
+ else treeNth (n - (k + 1)) right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing the nth smallest key/value (counting from 0). *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDeleteNth n tree =
+ case tree of
+ E => raise Bug "KeyMap.treeDeleteNth"
+ | T node => nodeDeleteNth n node
+
+and nodeDeleteNth n node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+
+ val k = treeSize left
+ in
+ if n = k then ((key,value), treeAppend left right)
+ else if n < k then
+ let
+ val (key_value,left) = treeDeleteNth n left
+
+ val size = size - 1
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ (key_value, T node)
+ end
+ else
+ let
+ val n = n - (k + 1)
+
+ val (key_value,right) = treeDeleteNth n right
+
+ val size = size - 1
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ (key_value, T node)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value iterator =
+ LR of (key * 'value) * 'value tree * 'value node list
+ | RL of (key * 'value) * 'value tree * 'value node list;
+
+fun fromSpineLR nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,right,...} :: nodes =>
+ SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,left,...} :: nodes =>
+ SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+ case iter of
+ LR (key_value,_,_) => key_value
+ | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+ case iter of
+ LR (_,tree,nodes) => addLR nodes tree
+ | RL (_,tree,nodes) => addRL nodes tree;
+
+fun foldIterator f acc io =
+ case io of
+ NONE => acc
+ | SOME iter =>
+ let
+ val (key,value) = readIterator iter
+ in
+ foldIterator f (f (key,value,acc)) (advanceIterator iter)
+ end;
+
+fun findIterator pred io =
+ case io of
+ NONE => NONE
+ | SOME iter =>
+ let
+ val key_value = readIterator iter
+ in
+ if pred key_value then SOME key_value
+ else findIterator pred (advanceIterator iter)
+ end;
+
+fun firstIterator f io =
+ case io of
+ NONE => NONE
+ | SOME iter =>
+ let
+ val key_value = readIterator iter
+ in
+ case f key_value of
+ NONE => firstIterator f (advanceIterator iter)
+ | s => s
+ end;
+
+fun compareIterator compareValue io1 io2 =
+ case (io1,io2) of
+ (NONE,NONE) => EQUAL
+ | (NONE, SOME _) => LESS
+ | (SOME _, NONE) => GREATER
+ | (SOME i1, SOME i2) =>
+ let
+ val (k1,v1) = readIterator i1
+ and (k2,v2) = readIterator i2
+ in
+ case compareKey (k1,k2) of
+ LESS => LESS
+ | EQUAL =>
+ (case compareValue (v1,v2) of
+ LESS => LESS
+ | EQUAL =>
+ let
+ val io1 = advanceIterator i1
+ and io2 = advanceIterator i2
+ in
+ compareIterator compareValue io1 io2
+ end
+ | GREATER => GREATER)
+ | GREATER => GREATER
+ end;
+
+fun equalIterator equalValue io1 io2 =
+ case (io1,io2) of
+ (NONE,NONE) => true
+ | (NONE, SOME _) => false
+ | (SOME _, NONE) => false
+ | (SOME i1, SOME i2) =>
+ let
+ val (k1,v1) = readIterator i1
+ and (k2,v2) = readIterator i2
+ in
+ equalKey k1 k2 andalso
+ equalValue v1 v2 andalso
+ let
+ val io1 = advanceIterator i1
+ and io2 = advanceIterator i2
+ in
+ equalIterator equalValue io1 io2
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'value map =
+ Map of 'value tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+ let
+ val Map tree = m
+
+ val _ = treeCheckInvariants tree
+ in
+ m
+ end
+ handle Bug bug => raise Bug (s ^ "\n" ^ "KeyMap.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new () =
+ let
+ val tree = treeNew ()
+ in
+ Map tree
+ end;
+
+fun singleton key_value =
+ let
+ val tree = treeSingleton key_value
+ in
+ Map tree
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map tree) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map tree) key = treePeekKey key tree;
+
+fun peek (Map tree) key = treePeek key tree;
+
+fun inDomain key m = Option.isSome (peek m key);
+
+fun get m key =
+ case peek m key of
+ NONE => raise Error "KeyMap.get: element not found"
+ | SOME value => value;
+
+fun pick (Map tree) = treePick tree;
+
+fun nth (Map tree) n = treeNth n tree;
+
+fun random m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "KeyMap.random: empty"
+ else nth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map tree) key_value =
+ let
+ val tree = treeInsert key_value tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+ checkInvariants "KeyMap.insert: result"
+ (insert (checkInvariants "KeyMap.insert: input" m) kv);
+*)
+
+fun insertList m =
+ let
+ fun ins (key_value,acc) = insert acc key_value
+ in
+ List.foldl ins m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Map tree) dkey =
+ let
+ val tree = treeDelete dkey tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+ checkInvariants "KeyMap.delete: result"
+ (delete (checkInvariants "KeyMap.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map tree) =
+ let
+ val (key_value,tree) = treeDeletePick tree
+ in
+ (key_value, Map tree)
+ end;
+
+(*BasicDebug
+val deletePick = fn m =>
+ let
+ val (kv,m) = deletePick (checkInvariants "KeyMap.deletePick: input" m)
+ in
+ (kv, checkInvariants "KeyMap.deletePick: result" m)
+ end;
+*)
+
+fun deleteNth (Map tree) n =
+ let
+ val (key_value,tree) = treeDeleteNth n tree
+ in
+ (key_value, Map tree)
+ end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+ let
+ val (kv,m) = deleteNth (checkInvariants "KeyMap.deleteNth: input" m) n
+ in
+ (kv, checkInvariants "KeyMap.deleteNth: result" m)
+ end;
+*)
+
+fun deleteRandom m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "KeyMap.deleteRandom: empty"
+ else deleteNth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map tree1) (Map tree2) =
+ let
+ val tree = treeMerge first second both tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.merge: result"
+ (merge f
+ (checkInvariants "KeyMap.merge: input 1" m1)
+ (checkInvariants "KeyMap.merge: input 2" m2));
+*)
+
+fun union f (Map tree1) (Map tree2) =
+ let
+ fun f2 kv = f (kv,kv)
+
+ val tree = treeUnion f f2 tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val union = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.union: result"
+ (union f
+ (checkInvariants "KeyMap.union: input 1" m1)
+ (checkInvariants "KeyMap.union: input 2" m2));
+*)
+
+fun intersect f (Map tree1) (Map tree2) =
+ let
+ val tree = treeIntersect f tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.intersect: result"
+ (intersect f
+ (checkInvariants "KeyMap.intersect: input 1" m1)
+ (checkInvariants "KeyMap.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map tree) = treeMkIterator tree;
+
+fun mkRevIterator (Map tree) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map tree) =
+ let
+ val tree = treeMapPartial f tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+ checkInvariants "KeyMap.mapPartial: result"
+ (mapPartial f (checkInvariants "KeyMap.mapPartial: input" m));
+*)
+
+fun map f (Map tree) =
+ let
+ val tree = treeMap f tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+ checkInvariants "KeyMap.map: result"
+ (map f (checkInvariants "KeyMap.map: input" m));
+*)
+
+fun transform f = map (fn (_,value) => f value);
+
+fun filter pred =
+ let
+ fun f (key_value as (_,value)) =
+ if pred key_value then SOME value else NONE
+ in
+ mapPartial f
+ end;
+
+fun partition p =
+ let
+ fun np x = not (p x)
+ in
+ fn m => (filter p m, filter np m)
+ end;
+
+fun foldl f b m = foldIterator f b (mkIterator m);
+
+fun foldr f b m = foldIterator f b (mkRevIterator m);
+
+fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p m = findIterator p (mkIterator m);
+
+fun findr p m = findIterator p (mkRevIterator m);
+
+fun firstl f m = firstIterator f (mkIterator m);
+
+fun firstr f m = firstIterator f (mkRevIterator m);
+
+fun exists p m = Option.isSome (findl p m);
+
+fun all p =
+ let
+ fun np x = not (p x)
+ in
+ fn m => not (exists np m)
+ end;
+
+fun count pred =
+ let
+ fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
+ in
+ foldl f 0
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare compareValue (m1,m2) =
+ if pointerEqual (m1,m2) then EQUAL
+ else
+ case Int.compare (size m1, size m2) of
+ LESS => LESS
+ | EQUAL =>
+ let
+ val Map _ = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ compareIterator compareValue io1 io2
+ end
+ | GREATER => GREATER;
+
+fun equal equalValue m1 m2 =
+ pointerEqual (m1,m2) orelse
+ (size m1 = size m2 andalso
+ let
+ val Map _ = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ equalIterator equalValue io1 io2
+ end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeUnionDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.unionDomain: result"
+ (unionDomain
+ (checkInvariants "KeyMap.unionDomain: input 1" m1)
+ (checkInvariants "KeyMap.unionDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+ fun unionListDomain ms =
+ case ms of
+ [] => raise Bug "KeyMap.unionListDomain: no sets"
+ | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeIntersectDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.intersectDomain: result"
+ (intersectDomain
+ (checkInvariants "KeyMap.intersectDomain: input 1" m1)
+ (checkInvariants "KeyMap.intersectDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+ fun intersectListDomain ms =
+ case ms of
+ [] => raise Bug "KeyMap.intersectListDomain: no sets"
+ | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeDifferenceDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.differenceDomain: result"
+ (differenceDomain
+ (checkInvariants "KeyMap.differenceDomain: input 1" m1)
+ (checkInvariants "KeyMap.differenceDomain: input 2" m2));
+*)
+
+fun symmetricDifferenceDomain m1 m2 =
+ unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
+
+fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
+
+fun subsetDomain (Map tree1) (Map tree2) =
+ treeSubsetDomain tree1 tree2;
+
+fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
+
+fun values m = foldr (fn (_,value,l) => value :: l) [] m;
+
+fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
+
+fun fromList l =
+ let
+ val m = new ()
+ in
+ insertList m l
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
+
+end
+
+structure IntMap =
+KeyMap (IntOrdered);
+
+structure IntPairMap =
+KeyMap (IntPairOrdered);
+
+structure StringMap =
+KeyMap (StringOrdered);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,22 @@
+(* ========================================================================= *)
+(* THE KNUTH-BENDIX TERM ORDERING *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature KnuthBendixOrder =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0. *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+ {weight : Term.function -> int,
+ precedence : Term.function * Term.function -> order}
+
+val default : kbo
+
+val compare : kbo -> Term.term * Term.term -> order option
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,199 @@
+(* ========================================================================= *)
+(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure KnuthBendixOrder :> KnuthBendixOrder =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun notEqualTerm (x,y) = not (Term.equal x y);
+
+fun firstNotEqualTerm f l =
+ case List.find notEqualTerm l of
+ SOME (x,y) => f x y
+ | NONE => raise Bug "firstNotEqualTerm";
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0. *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+ {weight : Term.function -> int,
+ precedence : Term.function * Term.function -> order};
+
+(* Default weight = uniform *)
+
+val uniformWeight : Term.function -> int = K 1;
+
+(* Default precedence = by arity *)
+
+val arityPrecedence : Term.function * Term.function -> order =
+ fn ((f1,n1),(f2,n2)) =>
+ case Int.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => Name.compare (f1,f2)
+ | GREATER => GREATER;
+
+(* The default order *)
+
+val default = {weight = uniformWeight, precedence = arityPrecedence};
+
+(* ------------------------------------------------------------------------- *)
+(* Term weight-1 represented as a linear function of the weight-1 of the *)
+(* variables in the term (plus a constant). *)
+(* *)
+(* Note that the conditions on weight functions ensure that all weights are *)
+(* at least 1, so all weight-1s are at least 0. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype weight = Weight of int NameMap.map * int;
+
+val weightEmpty : int NameMap.map = NameMap.new ();
+
+val weightZero = Weight (weightEmpty,0);
+
+fun weightIsZero (Weight (m,c)) = c = 0 andalso NameMap.null m;
+
+fun weightNeg (Weight (m,c)) = Weight (NameMap.transform ~ m, ~c);
+
+local
+ fun add ((_,n1),(_,n2)) =
+ let
+ val n = n1 + n2
+ in
+ if n = 0 then NONE else SOME n
+ end;
+in
+ fun weightAdd (Weight (m1,c1)) (Weight (m2,c2)) =
+ Weight (NameMap.union add m1 m2, c1 + c2);
+end;
+
+fun weightSubtract w1 w2 = weightAdd w1 (weightNeg w2);
+
+fun weightTerm weight =
+ let
+ fun wt m c [] = Weight (m,c)
+ | wt m c (Term.Var v :: tms) =
+ let
+ val n = Option.getOpt (NameMap.peek m v, 0)
+ in
+ wt (NameMap.insert m (v, n + 1)) (c + 1) tms
+ end
+ | wt m c (Term.Fn (f,a) :: tms) =
+ wt m (c + weight (f, length a)) (a @ tms)
+ in
+ fn tm => wt weightEmpty ~1 [tm]
+ end;
+
+fun weightLowerBound (w as Weight (m,c)) =
+ if NameMap.exists (fn (_,n) => n < 0) m then NONE else SOME c;
+
+(*MetisDebug
+val ppWeightList =
+ let
+ fun ppCoeff n =
+ if n < 0 then Print.sequence (Print.addString "~") (ppCoeff (~n))
+ else if n = 1 then Print.skip
+ else Print.ppInt n
+
+ fun pp_tm (NONE,n) = Print.ppInt n
+ | pp_tm (SOME v, n) = Print.sequence (ppCoeff n) (Name.pp v)
+ in
+ fn [] => Print.ppInt 0
+ | tms => Print.ppOpList " +" pp_tm tms
+ end;
+
+fun ppWeight (Weight (m,c)) =
+ let
+ val l = NameMap.toList m
+ val l = map (fn (v,n) => (SOME v, n)) l
+ val l = if c = 0 then l else l @ [(NONE,c)]
+ in
+ ppWeightList l
+ end;
+
+val weightToString = Print.toString ppWeight;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* The Knuth-Bendix term order. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare {weight,precedence} =
+ let
+ fun weightDifference tm1 tm2 =
+ let
+ val w1 = weightTerm weight tm1
+ and w2 = weightTerm weight tm2
+ in
+ weightSubtract w2 w1
+ end
+
+ fun weightLess tm1 tm2 =
+ let
+ val w = weightDifference tm1 tm2
+ in
+ if weightIsZero w then precedenceLess tm1 tm2
+ else weightDiffLess w tm1 tm2
+ end
+
+ and weightDiffLess w tm1 tm2 =
+ case weightLowerBound w of
+ NONE => false
+ | SOME 0 => precedenceLess tm1 tm2
+ | SOME n => n > 0
+
+ and precedenceLess (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+ (case precedence ((f1, length a1), (f2, length a2)) of
+ LESS => true
+ | EQUAL => firstNotEqualTerm weightLess (zip a1 a2)
+ | GREATER => false)
+ | precedenceLess _ _ = false
+
+ fun weightDiffGreater w tm1 tm2 = weightDiffLess (weightNeg w) tm2 tm1
+
+ fun weightCmp tm1 tm2 =
+ let
+ val w = weightDifference tm1 tm2
+ in
+ if weightIsZero w then precedenceCmp tm1 tm2
+ else if weightDiffLess w tm1 tm2 then SOME LESS
+ else if weightDiffGreater w tm1 tm2 then SOME GREATER
+ else NONE
+ end
+
+ and precedenceCmp (Term.Fn (f1,a1)) (Term.Fn (f2,a2)) =
+ (case precedence ((f1, length a1), (f2, length a2)) of
+ LESS => SOME LESS
+ | EQUAL => firstNotEqualTerm weightCmp (zip a1 a2)
+ | GREATER => SOME GREATER)
+ | precedenceCmp _ _ = raise Bug "kboOrder.precendenceCmp"
+ in
+ fn (tm1,tm2) =>
+ if Term.equal tm1 tm2 then SOME EQUAL else weightCmp tm1 tm2
+ end;
+
+(*MetisTrace7
+val compare = fn kbo => fn (tm1,tm2) =>
+ let
+ val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm1" tm1
+ val () = Print.trace Term.pp "KnuthBendixOrder.compare: tm2" tm2
+ val result = compare kbo (tm1,tm2)
+ val () =
+ case result of
+ NONE => trace "KnuthBendixOrder.compare: result = Incomparable\n"
+ | SOME x =>
+ Print.trace Print.ppOrder "KnuthBendixOrder.compare: result" x
+ in
+ result
+ end;
+*)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Lazy.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,19 @@
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Lazy =
+sig
+
+type 'a lazy
+
+val quickly : 'a -> 'a lazy
+
+val delay : (unit -> 'a) -> 'a lazy
+
+val force : 'a lazy -> 'a
+
+val memoize : (unit -> 'a) -> unit -> 'a
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Lazy.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,38 @@
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Lazy :> Lazy =
+struct
+
+datatype 'a thunk =
+ Value of 'a
+ | Thunk of unit -> 'a;
+
+datatype 'a lazy = Lazy of 'a thunk ref;
+
+fun quickly v = Lazy (ref (Value v));
+
+fun delay f = Lazy (ref (Thunk f));
+
+fun force (Lazy s) =
+ case !s of
+ Value v => v
+ | Thunk f =>
+ let
+ val v = f ()
+
+ val () = s := Value v
+ in
+ v
+ end;
+
+fun memoize f =
+ let
+ val t = delay f
+ in
+ fn () => force t
+ end;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Literal.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,165 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Literal =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals. *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool
+
+type literal = polarity * Atom.atom
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val polarity : literal -> polarity
+
+val atom : literal -> Atom.atom
+
+val name : literal -> Atom.relationName
+
+val arguments : literal -> Term.term list
+
+val arity : literal -> int
+
+val positive : literal -> bool
+
+val negative : literal -> bool
+
+val negate : literal -> literal
+
+val relation : literal -> Atom.relation
+
+val functions : literal -> NameAritySet.set
+
+val functionNames : literal -> NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : Atom.relationName -> polarity * Term.term * Term.term -> literal
+
+val destBinop : Atom.relationName -> literal -> polarity * Term.term * Term.term
+
+val isBinop : Atom.relationName -> literal -> bool
+
+(* Formulas *)
+
+val toFormula : literal -> Formula.formula
+
+val fromFormula : Formula.formula -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : literal -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : literal * literal -> order (* negative < positive *)
+
+val equal : literal -> literal -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : literal -> Term.path -> Term.term
+
+val subterms : literal -> (Term.path * Term.term) list
+
+val replace : literal -> Term.path * Term.term -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Term.var -> literal -> bool
+
+val freeVars : literal -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Subst.subst -> literal -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : (* raises Error *)
+ Subst.subst -> literal -> literal -> Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : (* raises Error *)
+ Subst.subst -> literal -> literal -> Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Term.term * Term.term -> literal
+
+val destEq : literal -> Term.term * Term.term
+
+val isEq : literal -> bool
+
+val mkNeq : Term.term * Term.term -> literal
+
+val destNeq : literal -> Term.term * Term.term
+
+val isNeq : literal -> bool
+
+val mkRefl : Term.term -> literal
+
+val destRefl : literal -> Term.term
+
+val isRefl : literal -> bool
+
+val mkIrrefl : Term.term -> literal
+
+val destIrrefl : literal -> Term.term
+
+val isIrrefl : literal -> bool
+
+(* The following work with both equalities and disequalities *)
+
+val sym : literal -> literal (* raises Error if given a refl or irrefl *)
+
+val lhs : literal -> Term.term
+
+val rhs : literal -> Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : literal -> int
+
+val nonVarTypedSubterms : literal -> (Term.path * Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : literal Print.pp
+
+val toString : literal -> string
+
+val fromString : string -> literal
+
+val parse : Term.term Parse.quotation -> literal
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Literal.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,293 @@
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Literal :> Literal =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals. *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool;
+
+type literal = polarity * Atom.atom;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun polarity ((pol,_) : literal) = pol;
+
+fun atom ((_,atm) : literal) = atm;
+
+fun name lit = Atom.name (atom lit);
+
+fun arguments lit = Atom.arguments (atom lit);
+
+fun arity lit = Atom.arity (atom lit);
+
+fun positive lit = polarity lit;
+
+fun negative lit = not (polarity lit);
+
+fun negate (pol,atm) : literal = (not pol, atm)
+
+fun relation lit = Atom.relation (atom lit);
+
+fun functions lit = Atom.functions (atom lit);
+
+fun functionNames lit = Atom.functionNames (atom lit);
+
+(* Binary relations *)
+
+fun mkBinop rel (pol,a,b) : literal = (pol, Atom.mkBinop rel (a,b));
+
+fun destBinop rel ((pol,atm) : literal) =
+ case Atom.destBinop rel atm of (a,b) => (pol,a,b);
+
+fun isBinop rel = can (destBinop rel);
+
+(* Formulas *)
+
+fun toFormula (true,atm) = Formula.Atom atm
+ | toFormula (false,atm) = Formula.Not (Formula.Atom atm);
+
+fun fromFormula (Formula.Atom atm) = (true,atm)
+ | fromFormula (Formula.Not (Formula.Atom atm)) = (false,atm)
+ | fromFormula _ = raise Error "Literal.fromFormula";
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols ((_,atm) : literal) = Atom.symbols atm;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare = prodCompare boolCompare Atom.compare;
+
+fun equal (p1,atm1) (p2,atm2) = p1 = p2 andalso Atom.equal atm1 atm2;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm lit path = Atom.subterm (atom lit) path;
+
+fun subterms lit = Atom.subterms (atom lit);
+
+fun replace (lit as (pol,atm)) path_tm =
+ let
+ val atm' = Atom.replace atm path_tm
+ in
+ if Portable.pointerEqual (atm,atm') then lit else (pol,atm')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v lit = Atom.freeIn v (atom lit);
+
+fun freeVars lit = Atom.freeVars (atom lit);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (lit as (pol,atm)) : literal =
+ let
+ val atm' = Atom.subst sub atm
+ in
+ if Portable.pointerEqual (atm',atm) then lit else (pol,atm')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun match sub ((pol1,atm1) : literal) (pol2,atm2) =
+ let
+ val _ = pol1 = pol2 orelse raise Error "Literal.match"
+ in
+ Atom.match sub atm1 atm2
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unify sub ((pol1,atm1) : literal) (pol2,atm2) =
+ let
+ val _ = pol1 = pol2 orelse raise Error "Literal.unify"
+ in
+ Atom.unify sub atm1 atm2
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq l_r : literal = (true, Atom.mkEq l_r);
+
+fun destEq ((true,atm) : literal) = Atom.destEq atm
+ | destEq (false,_) = raise Error "Literal.destEq";
+
+val isEq = can destEq;
+
+fun mkNeq l_r : literal = (false, Atom.mkEq l_r);
+
+fun destNeq ((false,atm) : literal) = Atom.destEq atm
+ | destNeq (true,_) = raise Error "Literal.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = (true, Atom.mkRefl tm);
+
+fun destRefl (true,atm) = Atom.destRefl atm
+ | destRefl (false,_) = raise Error "Literal.destRefl";
+
+val isRefl = can destRefl;
+
+fun mkIrrefl tm = (false, Atom.mkRefl tm);
+
+fun destIrrefl (true,_) = raise Error "Literal.destIrrefl"
+ | destIrrefl (false,atm) = Atom.destRefl atm;
+
+val isIrrefl = can destIrrefl;
+
+fun sym (pol,atm) : literal = (pol, Atom.sym atm);
+
+fun lhs ((_,atm) : literal) = Atom.lhs atm;
+
+fun rhs ((_,atm) : literal) = Atom.rhs atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,atm) : literal) = Atom.typedSymbols atm;
+
+fun nonVarTypedSubterms ((_,atm) : literal) = Atom.nonVarTypedSubterms atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppMap toFormula Formula.pp;
+
+val toString = Print.toString pp;
+
+fun fromString s = fromFormula (Formula.fromString s);
+
+val parse = Parse.parseQuotation Term.toString fromString;
+
+end
+
+structure LiteralOrdered =
+struct type t = Literal.literal val compare = Literal.compare end
+
+structure LiteralMap = KeyMap (LiteralOrdered);
+
+structure LiteralSet =
+struct
+
+ local
+ structure S = ElementSet (LiteralMap);
+ in
+ open S;
+ end;
+
+ fun negateMember lit set = member (Literal.negate lit) set;
+
+ val negate =
+ let
+ fun f (lit,set) = add set (Literal.negate lit)
+ in
+ foldl f empty
+ end;
+
+ val relations =
+ let
+ fun f (lit,set) = NameAritySet.add set (Literal.relation lit)
+ in
+ foldl f NameAritySet.empty
+ end;
+
+ val functions =
+ let
+ fun f (lit,set) = NameAritySet.union set (Literal.functions lit)
+ in
+ foldl f NameAritySet.empty
+ end;
+
+ fun freeIn v = exists (Literal.freeIn v);
+
+ val freeVars =
+ let
+ fun f (lit,set) = NameSet.union set (Literal.freeVars lit)
+ in
+ foldl f NameSet.empty
+ end;
+
+ val freeVarsList =
+ let
+ fun f (lits,set) = NameSet.union set (freeVars lits)
+ in
+ List.foldl f NameSet.empty
+ end;
+
+ val symbols =
+ let
+ fun f (lit,z) = Literal.symbols lit + z
+ in
+ foldl f 0
+ end;
+
+ val typedSymbols =
+ let
+ fun f (lit,z) = Literal.typedSymbols lit + z
+ in
+ foldl f 0
+ end;
+
+ fun subst sub lits =
+ let
+ fun substLit (lit,(eq,lits')) =
+ let
+ val lit' = Literal.subst sub lit
+ val eq = eq andalso Portable.pointerEqual (lit,lit')
+ in
+ (eq, add lits' lit')
+ end
+
+ val (eq,lits') = foldl substLit (true,empty) lits
+ in
+ if eq then lits else lits'
+ end;
+
+ fun conjoin set =
+ Formula.listMkConj (List.map Literal.toFormula (toList set));
+
+ fun disjoin set =
+ Formula.listMkDisj (List.map Literal.toFormula (toList set));
+
+ val pp =
+ Print.ppMap
+ toList
+ (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp));
+
+end
+
+structure LiteralSetOrdered =
+struct type t = LiteralSet.set val compare = LiteralSet.compare end
+
+structure LiteralSetMap = KeyMap (LiteralSetOrdered);
+
+structure LiteralSetSet = ElementSet (LiteralSetMap);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/LiteralNet.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,50 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature LiteralNet =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of literal sets that can be efficiently matched and unified. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {fifo : bool}
+
+type 'a literalNet
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val new : parameters -> 'a literalNet
+
+val size : 'a literalNet -> int
+
+val profile : 'a literalNet -> {positive : int, negative : int}
+
+val insert : 'a literalNet -> Literal.literal * 'a -> 'a literalNet
+
+val fromList : parameters -> (Literal.literal * 'a) list -> 'a literalNet
+
+val filter : ('a -> bool) -> 'a literalNet -> 'a literalNet
+
+val toString : 'a literalNet -> string
+
+val pp : 'a Print.pp -> 'a literalNet Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries. *)
+(* *)
+(* These function return OVER-APPROXIMATIONS! *)
+(* Filter afterwards to get the precise set of satisfying values. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : 'a literalNet -> Literal.literal -> 'a list
+
+val matched : 'a literalNet -> Literal.literal -> 'a list
+
+val unify : 'a literalNet -> Literal.literal -> 'a list
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/LiteralNet.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,74 @@
+(* ========================================================================= *)
+(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure LiteralNet :> LiteralNet =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of literal sets that can be efficiently matched and unified. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = AtomNet.parameters;
+
+type 'a literalNet =
+ {positive : 'a AtomNet.atomNet,
+ negative : 'a AtomNet.atomNet};
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm};
+
+local
+ fun pos ({positive,...} : 'a literalNet) = AtomNet.size positive;
+
+ fun neg ({negative,...} : 'a literalNet) = AtomNet.size negative;
+in
+ fun size net = pos net + neg net;
+
+ fun profile net = {positive = pos net, negative = neg net};
+end;
+
+fun insert {positive,negative} ((true,atm),a) =
+ {positive = AtomNet.insert positive (atm,a), negative = negative}
+ | insert {positive,negative} ((false,atm),a) =
+ {positive = positive, negative = AtomNet.insert negative (atm,a)};
+
+fun fromList parm l = foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
+
+fun filter pred {positive,negative} =
+ {positive = AtomNet.filter pred positive,
+ negative = AtomNet.filter pred negative};
+
+fun toString net = "LiteralNet[" ^ Int.toString (size net) ^ "]";
+
+fun pp ppA =
+ Print.ppMap
+ (fn {positive,negative} => (positive,negative))
+ (Print.ppOp2 " + NEGATIVE" (AtomNet.pp ppA) (AtomNet.pp ppA));
+
+(* ------------------------------------------------------------------------- *)
+(* Matching and unification queries. *)
+(* *)
+(* These function return OVER-APPROXIMATIONS! *)
+(* Filter afterwards to get the precise set of satisfying values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun match ({positive,...} : 'a literalNet) (true,atm) =
+ AtomNet.match positive atm
+ | match {negative,...} (false,atm) = AtomNet.match negative atm;
+
+fun matched ({positive,...} : 'a literalNet) (true,atm) =
+ AtomNet.matched positive atm
+ | matched {negative,...} (false,atm) = AtomNet.matched negative atm;
+
+fun unify ({positive,...} : 'a literalNet) (true,atm) =
+ AtomNet.unify positive atm
+ | unify {negative,...} (false,atm) = AtomNet.unify negative atm;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Map.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,190 @@
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Map =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val new : ('key * 'key -> order) -> ('key,'a) map
+
+val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+val null : ('key,'a) map -> bool
+
+val size : ('key,'a) map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+val peekKey : ('key,'a) map -> 'key -> ('key * 'a) option
+
+val peek : ('key,'a) map -> 'key -> 'a option
+
+val get : ('key,'a) map -> 'key -> 'a (* raises Error *)
+
+val pick : ('key,'a) map -> 'key * 'a (* an arbitrary key/value pair *)
+
+val nth : ('key,'a) map -> int -> 'key * 'a (* in the range [0,size-1] *)
+
+val random : ('key,'a) map -> 'key * 'a
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
+
+val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : ('key,'a) map -> 'key -> ('key,'a) map (* must be present *)
+
+val remove : ('key,'a) map -> 'key -> ('key,'a) map
+
+val deletePick : ('key,'a) map -> ('key * 'a) * ('key,'a) map
+
+val deleteNth : ('key,'a) map -> int -> ('key * 'a) * ('key,'a) map
+
+val deleteRandom : ('key,'a) map -> ('key * 'a) * ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+val merge :
+ {first : 'key * 'a -> 'c option,
+ second : 'key * 'b -> 'c option,
+ both : ('key * 'a) * ('key * 'b) -> 'c option} ->
+ ('key,'a) map -> ('key,'b) map -> ('key,'c) map
+
+val union :
+ (('key * 'a) * ('key * 'a) -> 'a option) ->
+ ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val intersect :
+ (('key * 'a) * ('key * 'b) -> 'c option) ->
+ ('key,'a) map -> ('key,'b) map -> ('key,'c) map
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+val inDomain : 'key -> ('key,'a) map -> bool
+
+val unionDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val unionListDomain : ('key,'a) map list -> ('key,'a) map
+
+val intersectDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val intersectListDomain : ('key,'a) map list -> ('key,'a) map
+
+val differenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val symmetricDifferenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
+
+val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+val disjointDomain : ('key,'a) map -> ('key,'a) map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
+
+val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
+
+val app : ('key * 'a -> unit) -> ('key,'a) map -> unit
+
+val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
+
+val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map
+
+val partition :
+ ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map
+
+val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
+
+val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
+
+val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
+
+val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
+
+val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
+
+val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
+
+val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
+
+val count : ('key * 'a -> bool) -> ('key,'a) map -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
+
+val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+val keys : ('key,'a) map -> 'key list
+
+val values : ('key,'a) map -> 'a list
+
+val toList : ('key,'a) map -> ('key * 'a) list
+
+val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val toString : ('key,'a) map -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type ('key,'a) iterator
+
+val mkIterator : ('key,'a) map -> ('key,'a) iterator option
+
+val mkRevIterator : ('key,'a) map -> ('key,'a) iterator option
+
+val readIterator : ('key,'a) iterator -> 'key * 'a
+
+val advanceIterator : ('key,'a) iterator -> ('key,'a) iterator option
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Map.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1425 @@
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Map :> Map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = Portable.randomWord;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting a comparison function to an equality function. *)
+(* ------------------------------------------------------------------------- *)
+
+fun equalKey compareKey key1 key2 = compareKey (key1,key2) = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Priorities. *)
+(* ------------------------------------------------------------------------- *)
+
+type priority = Word.word;
+
+val randomPriority = randomWord;
+
+val comparePriority = Word.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Priority search trees. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) tree =
+ E
+ | T of ('key,'value) node
+
+and ('key,'value) node =
+ Node of
+ {size : int,
+ priority : priority,
+ left : ('key,'value) tree,
+ key : 'key,
+ value : 'value,
+ right : ('key,'value) tree};
+
+fun lowerPriorityNode node1 node2 =
+ let
+ val Node {priority = p1, ...} = node1
+ and Node {priority = p2, ...} = node2
+ in
+ comparePriority (p1,p2) = LESS
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+local
+ fun checkSizes tree =
+ case tree of
+ E => 0
+ | T (Node {size,left,right,...}) =>
+ let
+ val l = checkSizes left
+ and r = checkSizes right
+
+ val () = if l + 1 + r = size then () else raise Bug "wrong size"
+ in
+ size
+ end;
+
+ fun checkSorted compareKey x tree =
+ case tree of
+ E => x
+ | T (Node {left,key,right,...}) =>
+ let
+ val x = checkSorted compareKey x left
+
+ val () =
+ case x of
+ NONE => ()
+ | SOME k =>
+ case compareKey (k,key) of
+ LESS => ()
+ | EQUAL => raise Bug "duplicate keys"
+ | GREATER => raise Bug "unsorted"
+
+ val x = SOME key
+ in
+ checkSorted compareKey x right
+ end;
+
+ fun checkPriorities compareKey tree =
+ case tree of
+ E => NONE
+ | T node =>
+ let
+ val Node {left,right,...} = node
+
+ val () =
+ case checkPriorities compareKey left of
+ NONE => ()
+ | SOME lnode =>
+ if not (lowerPriorityNode node lnode) then ()
+ else raise Bug "left child has greater priority"
+
+ val () =
+ case checkPriorities compareKey right of
+ NONE => ()
+ | SOME rnode =>
+ if not (lowerPriorityNode node rnode) then ()
+ else raise Bug "right child has greater priority"
+ in
+ SOME node
+ end;
+in
+ fun treeCheckInvariants compareKey tree =
+ let
+ val _ = checkSizes tree
+
+ val _ = checkSorted compareKey NONE tree
+
+ val _ = checkPriorities compareKey tree
+ in
+ tree
+ end
+ handle Error err => raise Bug err;
+end;
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Tree operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNew () = E;
+
+fun nodeSize (Node {size = x, ...}) = x;
+
+fun treeSize tree =
+ case tree of
+ E => 0
+ | T x => nodeSize x;
+
+fun mkNode priority left key value right =
+ let
+ val size = treeSize left + 1 + treeSize right
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+fun mkTree priority left key value right =
+ let
+ val node = mkNode priority left key value right
+ in
+ T node
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Extracting the left and right spines of a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeLeftSpine acc tree =
+ case tree of
+ E => acc
+ | T node => nodeLeftSpine acc node
+
+and nodeLeftSpine acc node =
+ let
+ val Node {left,...} = node
+ in
+ treeLeftSpine (node :: acc) left
+ end;
+
+fun treeRightSpine acc tree =
+ case tree of
+ E => acc
+ | T node => nodeRightSpine acc node
+
+and nodeRightSpine acc node =
+ let
+ val Node {right,...} = node
+ in
+ treeRightSpine (node :: acc) right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Singleton trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkNodeSingleton priority key value =
+ let
+ val size = 1
+ and left = E
+ and right = E
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+fun nodeSingleton (key,value) =
+ let
+ val priority = randomPriority ()
+ in
+ mkNodeSingleton priority key value
+ end;
+
+fun treeSingleton key_value =
+ let
+ val node = nodeSingleton key_value
+ in
+ T node
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees, where every element of the first tree is less than *)
+(* every element of the second tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeAppend tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 =>
+ if lowerPriorityNode node1 node2 then
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val left = treeAppend tree1 left
+ in
+ mkTree priority left key value right
+ end
+ else
+ let
+ val Node {priority,left,key,value,right,...} = node1
+
+ val right = treeAppend right tree2
+ in
+ mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Appending two trees and a node, where every element of the first tree is *)
+(* less than the node, which in turn is less than every element of the *)
+(* second tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeCombine left node right =
+ let
+ val left_node = treeAppend left (T node)
+ in
+ treeAppend left_node right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeek compareKey pkey tree =
+ case tree of
+ E => NONE
+ | T node => nodePeek compareKey pkey node
+
+and nodePeek compareKey pkey node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeek compareKey pkey left
+ | EQUAL => SOME value
+ | GREATER => treePeek compareKey pkey right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tree paths. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Generating a path by searching a tree for a key/value pair *)
+
+fun treePeekPath compareKey pkey path tree =
+ case tree of
+ E => (path,NONE)
+ | T node => nodePeekPath compareKey pkey path node
+
+and nodePeekPath compareKey pkey path node =
+ let
+ val Node {left,key,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeekPath compareKey pkey ((true,node) :: path) left
+ | EQUAL => (path, SOME node)
+ | GREATER => treePeekPath compareKey pkey ((false,node) :: path) right
+ end;
+
+(* A path splits a tree into left/right components *)
+
+fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
+ let
+ val Node {priority,left,key,value,right,...} = node
+ in
+ if wentLeft then (leftTree, mkTree priority rightTree key value right)
+ else (mkTree priority left key value leftTree, rightTree)
+ end;
+
+fun addSidesPath left_right = List.foldl addSidePath left_right;
+
+fun mkSidesPath path = addSidesPath (E,E) path;
+
+(* Updating the subtree at a path *)
+
+local
+ fun updateTree ((wentLeft,node),tree) =
+ let
+ val Node {priority,left,key,value,right,...} = node
+ in
+ if wentLeft then mkTree priority tree key value right
+ else mkTree priority left key value tree
+ end;
+in
+ fun updateTreePath tree = List.foldl updateTree tree;
+end;
+
+(* Inserting a new node at a path position *)
+
+fun insertNodePath node =
+ let
+ fun insert left_right path =
+ case path of
+ [] =>
+ let
+ val (left,right) = left_right
+ in
+ treeCombine left node right
+ end
+ | (step as (_,snode)) :: rest =>
+ if lowerPriorityNode snode node then
+ let
+ val left_right = addSidePath (step,left_right)
+ in
+ insert left_right rest
+ end
+ else
+ let
+ val (left,right) = left_right
+
+ val tree = treeCombine left node right
+ in
+ updateTreePath tree path
+ end
+ in
+ insert (E,E)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Using a key to split a node into three components: the keys comparing *)
+(* less than the supplied key, an optional equal key, and the keys comparing *)
+(* greater. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePartition compareKey pkey node =
+ let
+ val (path,pnode) = nodePeekPath compareKey pkey [] node
+ in
+ case pnode of
+ NONE =>
+ let
+ val (left,right) = mkSidesPath path
+ in
+ (left,NONE,right)
+ end
+ | SOME node =>
+ let
+ val Node {left,key,value,right,...} = node
+
+ val (left,right) = addSidesPath (left,right) path
+ in
+ (left, SOME (key,value), right)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching a tree for a key/value pair. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treePeekKey compareKey pkey tree =
+ case tree of
+ E => NONE
+ | T node => nodePeekKey compareKey pkey node
+
+and nodePeekKey compareKey pkey node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ case compareKey (pkey,key) of
+ LESS => treePeekKey compareKey pkey left
+ | EQUAL => SOME (key,value)
+ | GREATER => treePeekKey compareKey pkey right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Inserting new key/values into the tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeInsert compareKey key_value tree =
+ let
+ val (key,value) = key_value
+
+ val (path,inode) = treePeekPath compareKey key [] tree
+ in
+ case inode of
+ NONE =>
+ let
+ val node = nodeSingleton (key,value)
+ in
+ insertNodePath node path
+ end
+ | SOME node =>
+ let
+ val Node {size,priority,left,right,...} = node
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ updateTreePath (T node) path
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Deleting key/value pairs: it raises an exception if the supplied key is *)
+(* not present. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDelete compareKey dkey tree =
+ case tree of
+ E => raise Bug "Map.delete: element not found"
+ | T node => nodeDelete compareKey dkey node
+
+and nodeDelete compareKey dkey node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+ in
+ case compareKey (dkey,key) of
+ LESS =>
+ let
+ val size = size - 1
+ and left = treeDelete compareKey dkey left
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ T node
+ end
+ | EQUAL => treeAppend left right
+ | GREATER =>
+ let
+ val size = size - 1
+ and right = treeDelete compareKey dkey right
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ T node
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Partial map is the basic operation for preserving tree structure. *)
+(* It applies its argument function to the elements *in order*. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMapPartial f tree =
+ case tree of
+ E => E
+ | T node => nodeMapPartial f node
+
+and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
+ let
+ val left = treeMapPartial f left
+ and vo = f (key,value)
+ and right = treeMapPartial f right
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value => mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping tree values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMap f tree =
+ case tree of
+ E => E
+ | T node => T (nodeMap f node)
+
+and nodeMap f node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+
+ val left = treeMap f left
+ and value = f (key,value)
+ and right = treeMap f right
+ in
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Merge is the basic operation for joining two trees. Note that the merged *)
+(* key is always the one from the second map. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeMerge compareKey f1 f2 fb tree1 tree2 =
+ case tree1 of
+ E => treeMapPartial f2 tree2
+ | T node1 =>
+ case tree2 of
+ E => treeMapPartial f1 tree1
+ | T node2 => nodeMerge compareKey f1 f2 fb node1 node2
+
+and nodeMerge compareKey f1 f2 fb node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition compareKey key node1
+
+ val left = treeMerge compareKey f1 f2 fb l left
+ and right = treeMerge compareKey f1 f2 fb r right
+
+ val vo =
+ case kvo of
+ NONE => f2 (key,value)
+ | SOME kv => fb (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value =>
+ let
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnion compareKey f f2 tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 => nodeUnion compareKey f f2 node1 node2
+
+and nodeUnion compareKey f f2 node1 node2 =
+ if pointerEqual (node1,node2) then nodeMapPartial f2 node1
+ else
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition compareKey key node1
+
+ val left = treeUnion compareKey f f2 l left
+ and right = treeUnion compareKey f f2 r right
+
+ val vo =
+ case kvo of
+ NONE => SOME value
+ | SOME kv => f (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value =>
+ let
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersect compareKey f t1 t2 =
+ case t1 of
+ E => E
+ | T n1 =>
+ case t2 of
+ E => E
+ | T n2 => nodeIntersect compareKey f n1 n2
+
+and nodeIntersect compareKey f n1 n2 =
+ let
+ val Node {priority,left,key,value,right,...} = n2
+
+ val (l,kvo,r) = nodePartition compareKey key n1
+
+ val left = treeIntersect compareKey f l left
+ and right = treeIntersect compareKey f r right
+
+ val vo =
+ case kvo of
+ NONE => NONE
+ | SOME kv => f (kv,(key,value))
+ in
+ case vo of
+ NONE => treeAppend left right
+ | SOME value => mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A union operation on trees which simply chooses the second value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeUnionDomain compareKey tree1 tree2 =
+ case tree1 of
+ E => tree2
+ | T node1 =>
+ case tree2 of
+ E => tree1
+ | T node2 =>
+ if pointerEqual (node1,node2) then tree2
+ else nodeUnionDomain compareKey node1 node2
+
+and nodeUnionDomain compareKey node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,_,r) = nodePartition compareKey key node1
+
+ val left = treeUnionDomain compareKey l left
+ and right = treeUnionDomain compareKey r right
+
+ val node = mkNodeSingleton priority key value
+ in
+ treeCombine left node right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* An intersect operation on trees which simply chooses the second value. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeIntersectDomain compareKey tree1 tree2 =
+ case tree1 of
+ E => E
+ | T node1 =>
+ case tree2 of
+ E => E
+ | T node2 =>
+ if pointerEqual (node1,node2) then tree2
+ else nodeIntersectDomain compareKey node1 node2
+
+and nodeIntersectDomain compareKey node1 node2 =
+ let
+ val Node {priority,left,key,value,right,...} = node2
+
+ val (l,kvo,r) = nodePartition compareKey key node1
+
+ val left = treeIntersectDomain compareKey l left
+ and right = treeIntersectDomain compareKey r right
+ in
+ if Option.isSome kvo then mkTree priority left key value right
+ else treeAppend left right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A difference operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDifferenceDomain compareKey t1 t2 =
+ case t1 of
+ E => E
+ | T n1 =>
+ case t2 of
+ E => t1
+ | T n2 => nodeDifferenceDomain compareKey n1 n2
+
+and nodeDifferenceDomain compareKey n1 n2 =
+ if pointerEqual (n1,n2) then E
+ else
+ let
+ val Node {priority,left,key,value,right,...} = n1
+
+ val (l,kvo,r) = nodePartition compareKey key n2
+
+ val left = treeDifferenceDomain compareKey left l
+ and right = treeDifferenceDomain compareKey right r
+ in
+ if Option.isSome kvo then treeAppend left right
+ else mkTree priority left key value right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A subset operation on trees. *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeSubsetDomain compareKey tree1 tree2 =
+ case tree1 of
+ E => true
+ | T node1 =>
+ case tree2 of
+ E => false
+ | T node2 => nodeSubsetDomain compareKey node1 node2
+
+and nodeSubsetDomain compareKey node1 node2 =
+ pointerEqual (node1,node2) orelse
+ let
+ val Node {size,left,key,right,...} = node1
+ in
+ size <= nodeSize node2 andalso
+ let
+ val (l,kvo,r) = nodePartition compareKey key node2
+ in
+ Option.isSome kvo andalso
+ treeSubsetDomain compareKey left l andalso
+ treeSubsetDomain compareKey right r
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Picking an arbitrary key/value pair from a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodePick node =
+ let
+ val Node {key,value,...} = node
+ in
+ (key,value)
+ end;
+
+fun treePick tree =
+ case tree of
+ E => raise Bug "Map.treePick"
+ | T node => nodePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing an arbitrary key/value pair from a tree. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nodeDeletePick node =
+ let
+ val Node {left,key,value,right,...} = node
+ in
+ ((key,value), treeAppend left right)
+ end;
+
+fun treeDeletePick tree =
+ case tree of
+ E => raise Bug "Map.treeDeletePick"
+ | T node => nodeDeletePick node;
+
+(* ------------------------------------------------------------------------- *)
+(* Finding the nth smallest key/value (counting from 0). *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeNth n tree =
+ case tree of
+ E => raise Bug "Map.treeNth"
+ | T node => nodeNth n node
+
+and nodeNth n node =
+ let
+ val Node {left,key,value,right,...} = node
+
+ val k = treeSize left
+ in
+ if n = k then (key,value)
+ else if n < k then treeNth n left
+ else treeNth (n - (k + 1)) right
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing the nth smallest key/value (counting from 0). *)
+(* ------------------------------------------------------------------------- *)
+
+fun treeDeleteNth n tree =
+ case tree of
+ E => raise Bug "Map.treeDeleteNth"
+ | T node => nodeDeleteNth n node
+
+and nodeDeleteNth n node =
+ let
+ val Node {size,priority,left,key,value,right} = node
+
+ val k = treeSize left
+ in
+ if n = k then ((key,value), treeAppend left right)
+ else if n < k then
+ let
+ val (key_value,left) = treeDeleteNth n left
+
+ val size = size - 1
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ (key_value, T node)
+ end
+ else
+ let
+ val n = n - (k + 1)
+
+ val (key_value,right) = treeDeleteNth n right
+
+ val size = size - 1
+
+ val node =
+ Node
+ {size = size,
+ priority = priority,
+ left = left,
+ key = key,
+ value = value,
+ right = right}
+ in
+ (key_value, T node)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) iterator =
+ LR of ('key * 'value) * ('key,'value) tree * ('key,'value) node list
+ | RL of ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
+
+fun fromSpineLR nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,right,...} :: nodes =>
+ SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,left,...} :: nodes =>
+ SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+ case iter of
+ LR (key_value,_,_) => key_value
+ | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+ case iter of
+ LR (_,tree,nodes) => addLR nodes tree
+ | RL (_,tree,nodes) => addRL nodes tree;
+
+fun foldIterator f acc io =
+ case io of
+ NONE => acc
+ | SOME iter =>
+ let
+ val (key,value) = readIterator iter
+ in
+ foldIterator f (f (key,value,acc)) (advanceIterator iter)
+ end;
+
+fun findIterator pred io =
+ case io of
+ NONE => NONE
+ | SOME iter =>
+ let
+ val key_value = readIterator iter
+ in
+ if pred key_value then SOME key_value
+ else findIterator pred (advanceIterator iter)
+ end;
+
+fun firstIterator f io =
+ case io of
+ NONE => NONE
+ | SOME iter =>
+ let
+ val key_value = readIterator iter
+ in
+ case f key_value of
+ NONE => firstIterator f (advanceIterator iter)
+ | s => s
+ end;
+
+fun compareIterator compareKey compareValue io1 io2 =
+ case (io1,io2) of
+ (NONE,NONE) => EQUAL
+ | (NONE, SOME _) => LESS
+ | (SOME _, NONE) => GREATER
+ | (SOME i1, SOME i2) =>
+ let
+ val (k1,v1) = readIterator i1
+ and (k2,v2) = readIterator i2
+ in
+ case compareKey (k1,k2) of
+ LESS => LESS
+ | EQUAL =>
+ (case compareValue (v1,v2) of
+ LESS => LESS
+ | EQUAL =>
+ let
+ val io1 = advanceIterator i1
+ and io2 = advanceIterator i2
+ in
+ compareIterator compareKey compareValue io1 io2
+ end
+ | GREATER => GREATER)
+ | GREATER => GREATER
+ end;
+
+fun equalIterator equalKey equalValue io1 io2 =
+ case (io1,io2) of
+ (NONE,NONE) => true
+ | (NONE, SOME _) => false
+ | (SOME _, NONE) => false
+ | (SOME i1, SOME i2) =>
+ let
+ val (k1,v1) = readIterator i1
+ and (k2,v2) = readIterator i2
+ in
+ equalKey k1 k2 andalso
+ equalValue v1 v2 andalso
+ let
+ val io1 = advanceIterator i1
+ and io2 = advanceIterator i2
+ in
+ equalIterator equalKey equalValue io1 io2
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('key,'value) map =
+ Map of ('key * 'key -> order) * ('key,'value) tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+ let
+ val Map (compareKey,tree) = m
+
+ val _ = treeCheckInvariants compareKey tree
+ in
+ m
+ end
+ handle Bug bug => raise Bug (s ^ "\n" ^ "Map.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new compareKey =
+ let
+ val tree = treeNew ()
+ in
+ Map (compareKey,tree)
+ end;
+
+fun singleton compareKey key_value =
+ let
+ val tree = treeSingleton key_value
+ in
+ Map (compareKey,tree)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map (_,tree)) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map (compareKey,tree)) key = treePeekKey compareKey key tree;
+
+fun peek (Map (compareKey,tree)) key = treePeek compareKey key tree;
+
+fun inDomain key m = Option.isSome (peek m key);
+
+fun get m key =
+ case peek m key of
+ NONE => raise Error "Map.get: element not found"
+ | SOME value => value;
+
+fun pick (Map (_,tree)) = treePick tree;
+
+fun nth (Map (_,tree)) n = treeNth n tree;
+
+fun random m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "Map.random: empty"
+ else nth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map (compareKey,tree)) key_value =
+ let
+ val tree = treeInsert compareKey key_value tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+ checkInvariants "Map.insert: result"
+ (insert (checkInvariants "Map.insert: input" m) kv);
+*)
+
+fun insertList m =
+ let
+ fun ins (key_value,acc) = insert acc key_value
+ in
+ List.foldl ins m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Map (compareKey,tree)) dkey =
+ let
+ val tree = treeDelete compareKey dkey tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+ checkInvariants "Map.delete: result"
+ (delete (checkInvariants "Map.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map (compareKey,tree)) =
+ let
+ val (key_value,tree) = treeDeletePick tree
+ in
+ (key_value, Map (compareKey,tree))
+ end;
+
+(*BasicDebug
+val deletePick = fn m =>
+ let
+ val (kv,m) = deletePick (checkInvariants "Map.deletePick: input" m)
+ in
+ (kv, checkInvariants "Map.deletePick: result" m)
+ end;
+*)
+
+fun deleteNth (Map (compareKey,tree)) n =
+ let
+ val (key_value,tree) = treeDeleteNth n tree
+ in
+ (key_value, Map (compareKey,tree))
+ end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+ let
+ val (kv,m) = deleteNth (checkInvariants "Map.deleteNth: input" m) n
+ in
+ (kv, checkInvariants "Map.deleteNth: result" m)
+ end;
+*)
+
+fun deleteRandom m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "Map.deleteRandom: empty"
+ else deleteNth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeMerge compareKey first second both tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.merge: result"
+ (merge f
+ (checkInvariants "Map.merge: input 1" m1)
+ (checkInvariants "Map.merge: input 2" m2));
+*)
+
+fun union f (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ fun f2 kv = f (kv,kv)
+
+ val tree = treeUnion compareKey f f2 tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val union = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.union: result"
+ (union f
+ (checkInvariants "Map.union: input 1" m1)
+ (checkInvariants "Map.union: input 2" m2));
+*)
+
+fun intersect f (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeIntersect compareKey f tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.intersect: result"
+ (intersect f
+ (checkInvariants "Map.intersect: input 1" m1)
+ (checkInvariants "Map.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map (_,tree)) = treeMkIterator tree;
+
+fun mkRevIterator (Map (_,tree)) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map (compareKey,tree)) =
+ let
+ val tree = treeMapPartial f tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+ checkInvariants "Map.mapPartial: result"
+ (mapPartial f (checkInvariants "Map.mapPartial: input" m));
+*)
+
+fun map f (Map (compareKey,tree)) =
+ let
+ val tree = treeMap f tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+ checkInvariants "Map.map: result"
+ (map f (checkInvariants "Map.map: input" m));
+*)
+
+fun transform f = map (fn (_,value) => f value);
+
+fun filter pred =
+ let
+ fun f (key_value as (_,value)) =
+ if pred key_value then SOME value else NONE
+ in
+ mapPartial f
+ end;
+
+fun partition p =
+ let
+ fun np x = not (p x)
+ in
+ fn m => (filter p m, filter np m)
+ end;
+
+fun foldl f b m = foldIterator f b (mkIterator m);
+
+fun foldr f b m = foldIterator f b (mkRevIterator m);
+
+fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p m = findIterator p (mkIterator m);
+
+fun findr p m = findIterator p (mkRevIterator m);
+
+fun firstl f m = firstIterator f (mkIterator m);
+
+fun firstr f m = firstIterator f (mkRevIterator m);
+
+fun exists p m = Option.isSome (findl p m);
+
+fun all p =
+ let
+ fun np x = not (p x)
+ in
+ fn m => not (exists np m)
+ end;
+
+fun count pred =
+ let
+ fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
+ in
+ foldl f 0
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare compareValue (m1,m2) =
+ if pointerEqual (m1,m2) then EQUAL
+ else
+ case Int.compare (size m1, size m2) of
+ LESS => LESS
+ | EQUAL =>
+ let
+ val Map (compareKey,_) = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ compareIterator compareKey compareValue io1 io2
+ end
+ | GREATER => GREATER;
+
+fun equal equalValue m1 m2 =
+ pointerEqual (m1,m2) orelse
+ (size m1 = size m2 andalso
+ let
+ val Map (compareKey,_) = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ equalIterator (equalKey compareKey) equalValue io1 io2
+ end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeUnionDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.unionDomain: result"
+ (unionDomain
+ (checkInvariants "Map.unionDomain: input 1" m1)
+ (checkInvariants "Map.unionDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+ fun unionListDomain ms =
+ case ms of
+ [] => raise Bug "Map.unionListDomain: no sets"
+ | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeIntersectDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.intersectDomain: result"
+ (intersectDomain
+ (checkInvariants "Map.intersectDomain: input 1" m1)
+ (checkInvariants "Map.intersectDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+ fun intersectListDomain ms =
+ case ms of
+ [] => raise Bug "Map.intersectListDomain: no sets"
+ | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeDifferenceDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.differenceDomain: result"
+ (differenceDomain
+ (checkInvariants "Map.differenceDomain: input 1" m1)
+ (checkInvariants "Map.differenceDomain: input 2" m2));
+*)
+
+fun symmetricDifferenceDomain m1 m2 =
+ unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
+
+fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
+
+fun subsetDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ treeSubsetDomain compareKey tree1 tree2;
+
+fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
+
+fun values m = foldr (fn (_,value,l) => value :: l) [] m;
+
+fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
+
+fun fromList compareKey l =
+ let
+ val m = new compareKey
+ in
+ insertList m l
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Model.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,277 @@
+(* ========================================================================= *)
+(* RANDOM FINITE MODELS *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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. *)
+(* ------------------------------------------------------------------------- *)
+
+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. *)
+(* ------------------------------------------------------------------------- *)
+
+(* 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 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 preName : Name.name
+
+val subName : Name.name
+
+val sucName : Name.name
+
+val modularFixed : fixed
+
+val overflowFixed : fixed
+
+(* Sets *)
+
+val cardName : Name.name
+
+val complementName : Name.name
+
+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 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 nullName : Name.name
+
+val tailName : Name.name
+
+val listFixed : fixed
+
+(* ------------------------------------------------------------------------- *)
+(* Valuations. *)
+(* ------------------------------------------------------------------------- *)
+
+type valuation
+
+val emptyValuation : valuation
+
+val zeroValuation : NameSet.set -> valuation
+
+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 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. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {size : int, fixed : fixed}
+
+type model
+
+val default : parameters
+
+val new : parameters -> model
+
+val size : model -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting terms and formulas in the model. *)
+(* ------------------------------------------------------------------------- *)
+
+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
+
+val interpretFormula : model -> valuation -> Formula.formula -> bool
+
+val interpretLiteral : model -> valuation -> Literal.literal -> bool
+
+val interpretClause : model -> valuation -> Thm.clause -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Check whether random groundings of a formula are true in the model. *)
+(* 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 option} -> model -> Atom.atom -> {T : int, F : int}
+
+val checkFormula :
+ {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}
+
+val checkLiteral :
+ {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}
+
+val checkClause :
+ {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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Model.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1278 @@
+(* ========================================================================= *)
+(* RANDOM FINITE MODELS *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Model :> Model =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Constants. *)
+(* ------------------------------------------------------------------------- *)
+
+val maxSpace = 1000;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+val multInt =
+ case Int.maxInt of
+ NONE => (fn x => fn y => SOME (x * y))
+ | SOME m =>
+ let
+ val m = Real.floor (Math.sqrt (Real.fromInt m))
+ in
+ fn x => fn y => if x <= m andalso y <= m then SOME (x * y) else NONE
+ end;
+
+local
+ fun iexp x y acc =
+ if y mod 2 = 0 then iexp' x y acc
+ else
+ case multInt acc x of
+ SOME acc => iexp' x y acc
+ | NONE => NONE
+
+ and iexp' x y acc =
+ if y = 1 then SOME acc
+ else
+ let
+ val y = y div 2
+ in
+ case multInt x x of
+ SOME x => iexp x y acc
+ | NONE => NONE
+ end;
+in
+ fun expInt x y =
+ if y <= 1 then
+ if y = 0 then SOME 1
+ else if y = 1 then SOME x
+ else raise Bug "expInt: negative exponent"
+ else if x <= 1 then
+ if 0 <= x then SOME x
+ else raise Bug "expInt: negative exponand"
+ else iexp x y 1;
+end;
+
+fun boolToInt true = 1
+ | boolToInt false = 0;
+
+fun intToBool 1 = true
+ | intToBool 0 = false
+ | intToBool _ = raise Bug "Model.intToBool";
+
+fun minMaxInterval i j = interval i (1 + j - i);
+
+(* ------------------------------------------------------------------------- *)
+(* Model size. *)
+(* ------------------------------------------------------------------------- *)
+
+type size = {size : int};
+
+(* ------------------------------------------------------------------------- *)
+(* A model of size N has integer elements 0...N-1. *)
+(* ------------------------------------------------------------------------- *)
+
+type element = int;
+
+val zeroElement = 0;
+
+fun incrementElement {size = N} i =
+ let
+ val i = i + 1
+ in
+ if i = N then NONE else SOME i
+ end;
+
+fun elementListSpace {size = N} arity =
+ case expInt N arity of
+ NONE => NONE
+ | s as SOME m => if m <= maxSpace then s else NONE;
+
+fun elementListIndex {size = N} =
+ let
+ fun f acc elts =
+ case elts of
+ [] => acc
+ | elt :: elts => f (N * acc + elt) elts
+ in
+ f 0
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* The parts of the model that are fixed. *)
+(* ------------------------------------------------------------------------- *)
+
+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 uselessFixedFunction : fixedFunction = K (K NONE);
+
+val uselessFixedRelation : fixedRelation = K (K NONE);
+
+val emptyFunctions : fixedFunction NameArityMap.map = NameArityMap.new ();
+
+val emptyRelations : fixedRelation NameArityMap.map = NameArityMap.new ();
+
+fun fixed0 f sz elts =
+ case elts of
+ [] => f sz
+ | _ => raise Bug "Model.fixed0: wrong arity";
+
+fun fixed1 f sz elts =
+ case elts of
+ [x] => f sz x
+ | _ => raise Bug "Model.fixed1: wrong arity";
+
+fun fixed2 f sz elts =
+ case elts of
+ [x,y] => f sz x y
+ | _ => raise Bug "Model.fixed2: wrong arity";
+
+val emptyFixed =
+ let
+ val fns = emptyFunctions
+ and rels = emptyRelations
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+
+fun peekFunctionFixed fix name_arity =
+ let
+ val Fixed {functions = fns, ...} = fix
+ in
+ NameArityMap.peek fns name_arity
+ end;
+
+fun peekRelationFixed fix name_arity =
+ let
+ val Fixed {relations = rels, ...} = fix
+ in
+ NameArityMap.peek rels name_arity
+ end;
+
+fun getFunctionFixed fix name_arity =
+ case peekFunctionFixed fix name_arity of
+ SOME f => f
+ | NONE => uselessFixedFunction;
+
+fun getRelationFixed fix name_arity =
+ case peekRelationFixed fix name_arity of
+ SOME rel => rel
+ | NONE => uselessFixedRelation;
+
+fun insertFunctionFixed fix name_arity_fn =
+ let
+ val Fixed {functions = fns, relations = rels} = fix
+
+ val fns = NameArityMap.insert fns name_arity_fn
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+
+fun insertRelationFixed fix name_arity_rel =
+ let
+ val Fixed {functions = fns, relations = rels} = fix
+
+ val rels = NameArityMap.insert rels name_arity_rel
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+
+local
+ fun union _ = raise Bug "Model.unionFixed: nameArity clash";
+in
+ fun unionFixed fix1 fix2 =
+ let
+ val Fixed {functions = fns1, relations = rels1} = fix1
+ and Fixed {functions = fns2, relations = rels2} = fix2
+
+ val fns = NameArityMap.union union fns1 fns2
+
+ val rels = NameArityMap.union union rels1 rels2
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+end;
+
+val unionListFixed =
+ let
+ fun union (fix,acc) = unionFixed acc fix
+ in
+ List.foldl union emptyFixed
+ end;
+
+local
+ fun hasTypeFn _ elts =
+ case elts of
+ [x,_] => SOME x
+ | _ => raise Bug "Model.hasTypeFn: wrong arity";
+
+ fun eqRel _ elts =
+ case elts of
+ [x,y] => SOME (x = y)
+ | _ => raise Bug "Model.eqRel: wrong arity";
+in
+ val basicFixed =
+ let
+ val fns = NameArityMap.singleton (Term.hasTypeFunction,hasTypeFn)
+
+ val rels = NameArityMap.singleton (Atom.eqRelation,eqRel)
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Renaming fixed model parts. *)
+(* ------------------------------------------------------------------------- *)
+
+type fixedMap =
+ {functionMap : Name.name NameArityMap.map,
+ relationMap : Name.name NameArityMap.map};
+
+fun mapFixed fixMap fix =
+ let
+ val {functionMap = fnMap, relationMap = relMap} = fixMap
+ and Fixed {functions = fns, relations = rels} = fix
+
+ val fns = NameArityMap.compose fnMap fns
+
+ val rels = NameArityMap.compose relMap rels
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+
+local
+ fun mkEntry tag (na,n) = (tag,na,n);
+
+ fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m);
+
+ fun ppEntry (tag,source_arity,target) =
+ Print.blockProgram Print.Inconsistent 2
+ [Print.addString tag,
+ Print.addBreak 1,
+ NameArity.pp source_arity,
+ Print.addString " ->",
+ Print.addBreak 1,
+ Name.pp target];
+in
+ fun ppFixedMap fixMap =
+ let
+ val {functionMap = fnMap, relationMap = relMap} = fixMap
+ in
+ case mkList "function" fnMap @ mkList "relation" relMap of
+ [] => Print.skip
+ | entry :: entries =>
+ Print.blockProgram Print.Consistent 0
+ (ppEntry entry ::
+ map (Print.sequence Print.addNewline o ppEntry) entries)
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Standard fixed model parts. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Projections *)
+
+val projectionMin = 1
+and projectionMax = 9;
+
+val projectionList = minMaxInterval projectionMin projectionMax;
+
+fun projectionName i =
+ let
+ val _ = projectionMin <= i orelse
+ raise Bug "Model.projectionName: less than projectionMin"
+
+ val _ = i <= projectionMax orelse
+ raise Bug "Model.projectionName: greater than projectionMax"
+ in
+ Name.fromString ("project" ^ Int.toString i)
+ end;
+
+fun projectionFn i _ elts = SOME (List.nth (elts, i - 1));
+
+fun arityProjectionFixed arity =
+ let
+ fun mkProj i = ((projectionName i, arity), projectionFn i)
+
+ fun addProj i acc =
+ if i > arity then acc
+ else addProj (i + 1) (NameArityMap.insert acc (mkProj i))
+
+ val fns = addProj projectionMin emptyFunctions
+
+ val rels = emptyRelations
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+
+val projectionFixed =
+ unionListFixed (map arityProjectionFixed projectionList);
+
+(* Arithmetic *)
+
+val numeralMin = ~100
+and numeralMax = 100;
+
+val numeralList = minMaxInterval numeralMin numeralMax;
+
+fun numeralName i =
+ let
+ val _ = numeralMin <= i orelse
+ raise Bug "Model.numeralName: less than numeralMin"
+
+ val _ = i <= numeralMax orelse
+ raise Bug "Model.numeralName: greater than numeralMax"
+
+ val s = if i < 0 then "negative" ^ Int.toString (~i) else Int.toString i
+ in
+ Name.fromString s
+ end;
+
+val addName = Name.fromString "+"
+and divName = Name.fromString "div"
+and dividesName = Name.fromString "divides"
+and evenName = Name.fromString "even"
+and expName = Name.fromString "exp"
+and geName = Name.fromString ">="
+and gtName = Name.fromString ">"
+and isZeroName = Name.fromString "isZero"
+and leName = Name.fromString "<="
+and ltName = Name.fromString "<"
+and modName = Name.fromString "mod"
+and multName = Name.fromString "*"
+and negName = Name.fromString "~"
+and oddName = Name.fromString "odd"
+and preName = Name.fromString "pre"
+and subName = Name.fromString "-"
+and sucName = Name.fromString "suc";
+
+local
+ (* Support *)
+
+ fun modN {size = N} x = x mod N;
+
+ fun oneN sz = modN sz 1;
+
+ fun multN sz (x,y) = modN sz (x * y);
+
+ (* Functions *)
+
+ fun numeralFn i sz = SOME (modN sz i);
+
+ fun addFn sz x y = SOME (modN sz (x + y));
+
+ fun divFn {size = N} x y =
+ let
+ val y = if y = 0 then N else y
+ in
+ SOME (x div y)
+ end;
+
+ fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
+
+ fun modFn {size = N} x y =
+ let
+ val y = if y = 0 then N else y
+ in
+ SOME (x mod y)
+ end;
+
+ fun multFn sz x y = SOME (multN sz (x,y));
+
+ fun negFn {size = N} x = SOME (if x = 0 then 0 else N - x);
+
+ fun preFn {size = N} x = SOME (if x = 0 then N - 1 else x - 1);
+
+ fun subFn {size = N} x y = SOME (if x < y then N + x - y else x - y);
+
+ fun sucFn {size = N} x = SOME (if x = N - 1 then 0 else x + 1);
+
+ (* Relations *)
+
+ fun dividesRel _ x y = SOME (divides x y);
+
+ fun evenRel _ x = SOME (x mod 2 = 0);
+
+ fun geRel _ x y = SOME (x >= y);
+
+ fun gtRel _ x y = SOME (x > y);
+
+ fun isZeroRel _ x = SOME (x = 0);
+
+ fun leRel _ x y = SOME (x <= y);
+
+ fun ltRel _ x y = SOME (x < y);
+
+ fun oddRel _ x = SOME (x mod 2 = 1);
+in
+ val modularFixed =
+ let
+ val fns =
+ NameArityMap.fromList
+ (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ numeralList @
+ [((addName,2), fixed2 addFn),
+ ((divName,2), fixed2 divFn),
+ ((expName,2), fixed2 expFn),
+ ((modName,2), fixed2 modFn),
+ ((multName,2), fixed2 multFn),
+ ((negName,1), fixed1 negFn),
+ ((preName,1), fixed1 preFn),
+ ((subName,2), fixed2 subFn),
+ ((sucName,1), fixed1 sucFn)])
+
+ val rels =
+ NameArityMap.fromList
+ [((dividesName,2), fixed2 dividesRel),
+ ((evenName,1), fixed1 evenRel),
+ ((geName,2), fixed2 geRel),
+ ((gtName,2), fixed2 gtRel),
+ ((isZeroName,1), fixed1 isZeroRel),
+ ((leName,2), fixed2 leRel),
+ ((ltName,2), fixed2 ltRel),
+ ((oddName,1), fixed1 oddRel)]
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+end;
+
+local
+ (* Support *)
+
+ fun cutN {size = N} x = if x >= N then N - 1 else x;
+
+ fun oneN sz = cutN sz 1;
+
+ fun multN sz (x,y) = cutN sz (x * y);
+
+ (* Functions *)
+
+ fun numeralFn i sz = if i < 0 then NONE else SOME (cutN sz i);
+
+ fun addFn sz x y = SOME (cutN sz (x + y));
+
+ fun divFn _ x y = if y = 0 then NONE else SOME (x div y);
+
+ fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
+
+ fun modFn {size = N} x y =
+ if y = 0 orelse x = N - 1 then NONE else SOME (x mod y);
+
+ fun multFn sz x y = SOME (multN sz (x,y));
+
+ fun negFn _ x = if x = 0 then SOME 0 else NONE;
+
+ fun preFn _ x = if x = 0 then NONE else SOME (x - 1);
+
+ fun subFn {size = N} x y =
+ if y = 0 then SOME x
+ else if x = N - 1 orelse x < y then NONE
+ else SOME (x - y);
+
+ fun sucFn sz x = SOME (cutN sz (x + 1));
+
+ (* Relations *)
+
+ fun dividesRel {size = N} x y =
+ if x = 1 orelse y = 0 then SOME true
+ else if x = 0 then SOME false
+ else if y = N - 1 then NONE
+ else SOME (divides x y);
+
+ fun evenRel {size = N} x =
+ if x = N - 1 then NONE else SOME (x mod 2 = 0);
+
+ fun geRel {size = N} y x =
+ if x = N - 1 then if y = N - 1 then NONE else SOME false
+ else if y = N - 1 then SOME true else SOME (x <= y);
+
+ fun gtRel {size = N} y x =
+ if x = N - 1 then if y = N - 1 then NONE else SOME false
+ else if y = N - 1 then SOME true else SOME (x < y);
+
+ fun isZeroRel _ x = SOME (x = 0);
+
+ fun leRel {size = N} x y =
+ if x = N - 1 then if y = N - 1 then NONE else SOME false
+ else if y = N - 1 then SOME true else SOME (x <= y);
+
+ fun ltRel {size = N} x y =
+ if x = N - 1 then if y = N - 1 then NONE else SOME false
+ else if y = N - 1 then SOME true else SOME (x < y);
+
+ fun oddRel {size = N} x =
+ if x = N - 1 then NONE else SOME (x mod 2 = 1);
+in
+ val overflowFixed =
+ let
+ val fns =
+ NameArityMap.fromList
+ (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ numeralList @
+ [((addName,2), fixed2 addFn),
+ ((divName,2), fixed2 divFn),
+ ((expName,2), fixed2 expFn),
+ ((modName,2), fixed2 modFn),
+ ((multName,2), fixed2 multFn),
+ ((negName,1), fixed1 negFn),
+ ((preName,1), fixed1 preFn),
+ ((subName,2), fixed2 subFn),
+ ((sucName,1), fixed1 sucFn)])
+
+ val rels =
+ NameArityMap.fromList
+ [((dividesName,2), fixed2 dividesRel),
+ ((evenName,1), fixed1 evenRel),
+ ((geName,2), fixed2 geRel),
+ ((gtName,2), fixed2 gtRel),
+ ((isZeroName,1), fixed1 isZeroRel),
+ ((leName,2), fixed2 leRel),
+ ((ltName,2), fixed2 ltRel),
+ ((oddName,1), fixed1 oddRel)]
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+end;
+
+(* Sets *)
+
+val cardName = Name.fromString "card"
+and complementName = Name.fromString "complement"
+and differenceName = Name.fromString "difference"
+and emptyName = Name.fromString "empty"
+and memberName = Name.fromString "member"
+and insertName = Name.fromString "insert"
+and intersectName = Name.fromString "intersect"
+and singletonName = Name.fromString "singleton"
+and subsetName = Name.fromString "subset"
+and symmetricDifferenceName = Name.fromString "symmetricDifference"
+and unionName = Name.fromString "union"
+and universeName = Name.fromString "universe";
+
+local
+ (* Support *)
+
+ fun eltN {size = N} =
+ let
+ fun f 0 acc = acc
+ | f x acc = f (x div 2) (acc + 1)
+ in
+ f N ~1
+ end;
+
+ fun posN i = Word.<< (0w1, Word.fromInt i);
+
+ fun univN sz = Word.- (posN (eltN sz), 0w1);
+
+ fun setN sz x = Word.andb (Word.fromInt x, univN sz);
+
+ (* Functions *)
+
+ fun cardFn sz x =
+ let
+ fun f 0w0 acc = acc
+ | f s acc =
+ let
+ val acc = if Word.andb (s,0w1) = 0w0 then acc else acc + 1
+ in
+ f (Word.>> (s,0w1)) acc
+ end
+ in
+ SOME (f (setN sz x) 0)
+ end;
+
+ fun complementFn sz x = SOME (Word.toInt (Word.xorb (univN sz, setN sz x)));
+
+ fun differenceFn sz x y =
+ let
+ val x = setN sz x
+ and y = setN sz y
+ in
+ SOME (Word.toInt (Word.andb (x, Word.notb y)))
+ end;
+
+ fun emptyFn _ = SOME 0;
+
+ fun insertFn sz x y =
+ let
+ val x = x mod eltN sz
+ and y = setN sz y
+ in
+ SOME (Word.toInt (Word.orb (posN x, y)))
+ end;
+
+ fun intersectFn sz x y =
+ SOME (Word.toInt (Word.andb (setN sz x, setN sz y)));
+
+ fun singletonFn sz x =
+ let
+ val x = x mod eltN sz
+ in
+ SOME (Word.toInt (posN x))
+ end;
+
+ fun symmetricDifferenceFn sz x y =
+ let
+ val x = setN sz x
+ and y = setN sz y
+ in
+ SOME (Word.toInt (Word.xorb (x,y)))
+ end;
+
+ fun unionFn sz x y =
+ SOME (Word.toInt (Word.orb (setN sz x, setN sz y)));
+
+ fun universeFn sz = SOME (Word.toInt (univN sz));
+
+ (* Relations *)
+
+ fun memberRel sz x y =
+ let
+ val x = x mod eltN sz
+ and y = setN sz y
+ in
+ SOME (Word.andb (posN x, y) <> 0w0)
+ end;
+
+ fun subsetRel sz x y =
+ let
+ val x = setN sz x
+ and y = setN sz y
+ in
+ SOME (Word.andb (x, Word.notb y) = 0w0)
+ end;
+in
+ val setFixed =
+ let
+ val fns =
+ NameArityMap.fromList
+ [((cardName,1), fixed1 cardFn),
+ ((complementName,1), fixed1 complementFn),
+ ((differenceName,2), fixed2 differenceFn),
+ ((emptyName,0), fixed0 emptyFn),
+ ((insertName,2), fixed2 insertFn),
+ ((intersectName,2), fixed2 intersectFn),
+ ((singletonName,1), fixed1 singletonFn),
+ ((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn),
+ ((unionName,2), fixed2 unionFn),
+ ((universeName,0), fixed0 universeFn)]
+
+ val rels =
+ NameArityMap.fromList
+ [((memberName,2), fixed2 memberRel),
+ ((subsetName,2), fixed2 subsetRel)]
+ in
+ Fixed
+ {functions = fns,
+ relations = rels}
+ end;
+end;
+
+(* Lists *)
+
+val appendName = Name.fromString "@"
+and consName = Name.fromString "::"
+and lengthName = Name.fromString "length"
+and nilName = Name.fromString "nil"
+and nullName = Name.fromString "null"
+and tailName = Name.fromString "tail";
+
+local
+ val baseFix =
+ let
+ val fix = unionFixed projectionFixed overflowFixed
+
+ val sucFn = getFunctionFixed fix (sucName,1)
+
+ fun suc2Fn sz _ x = sucFn sz [x]
+ in
+ insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn)
+ end;
+
+ val fixMap =
+ {functionMap = NameArityMap.fromList
+ [((appendName,2),addName),
+ ((consName,2),sucName),
+ ((lengthName,1), projectionName 1),
+ ((nilName,0), numeralName 0),
+ ((tailName,1),preName)],
+ relationMap = NameArityMap.fromList
+ [((nullName,1),isZeroName)]};
+
+in
+ val listFixed = mapFixed fixMap baseFix;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Valuations. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype valuation = Valuation of element NameMap.map;
+
+val emptyValuation = Valuation (NameMap.new ());
+
+fun insertValuation (Valuation m) v_i = Valuation (NameMap.insert m v_i);
+
+fun peekValuation (Valuation m) v = NameMap.peek m v;
+
+fun constantValuation i =
+ let
+ fun add (v,V) = insertValuation V (v,i)
+ in
+ NameSet.foldl add emptyValuation
+ end;
+
+val zeroValuation = constantValuation zeroElement;
+
+fun getValuation V v =
+ case peekValuation V v of
+ SOME i => i
+ | NONE => raise Error "Model.getValuation: incomplete valuation";
+
+fun randomValuation {size = N} vs =
+ let
+ fun f (v,V) = insertValuation V (v, Portable.randomInt N)
+ in
+ NameSet.foldl f emptyValuation vs
+ end;
+
+fun incrementValuation N vars =
+ let
+ fun inc vs V =
+ case vs of
+ [] => NONE
+ | v :: vs =>
+ let
+ val (carry,i) =
+ case incrementElement N (getValuation V v) of
+ SOME i => (false,i)
+ | NONE => (true,zeroElement)
+
+ val V = insertValuation V (v,i)
+ in
+ if carry then inc vs V else SOME V
+ end
+ in
+ inc (NameSet.toList vars)
+ end;
+
+fun foldValuation N vars f =
+ let
+ val inc = incrementValuation N vars
+
+ fun fold V acc =
+ let
+ val acc = f (V,acc)
+ in
+ case inc V of
+ NONE => acc
+ | SOME V => fold V acc
+ end
+
+ val zero = zeroValuation vars
+ in
+ fold zero
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite mapping Z^n -> Z. *)
+(* ------------------------------------------------------------------------- *)
+
+val UNKNOWN = ~1;
+
+datatype table =
+ ForgetfulTable
+ | ArrayTable of int Array.array;
+
+fun newTable N arity =
+ case elementListSpace {size = N} arity of
+ NONE => ForgetfulTable
+ | SOME space => ArrayTable (Array.array (space,UNKNOWN));
+
+local
+ fun randomResult R = Portable.randomInt R;
+in
+ fun lookupTable N R table elts =
+ case table of
+ ForgetfulTable => randomResult R
+ | ArrayTable a =>
+ let
+ val i = elementListIndex {size = N} elts
+
+ val r = Array.sub (a,i)
+ in
+ if r <> UNKNOWN then r
+ else
+ let
+ val r = randomResult R
+
+ val () = Array.update (a,i,r)
+ in
+ r
+ end
+ end;
+end;
+
+fun updateTable N table (elts,r) =
+ case table of
+ ForgetfulTable => ()
+ | ArrayTable a =>
+ let
+ val i = elementListIndex {size = N} elts
+
+ val () = Array.update (a,i,r)
+ in
+ ()
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite mappings name * arity -> Z^arity -> Z. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype tables =
+ Tables of
+ {domainSize : int,
+ rangeSize : int,
+ tableMap : table NameArityMap.map ref};
+
+fun newTables N R =
+ Tables
+ {domainSize = N,
+ rangeSize = R,
+ tableMap = ref (NameArityMap.new ())};
+
+fun getTables tables n_a =
+ let
+ val Tables {domainSize = N, rangeSize = _, tableMap = tm} = tables
+
+ val ref m = tm
+ in
+ case NameArityMap.peek m n_a of
+ SOME t => t
+ | NONE =>
+ let
+ val (_,a) = n_a
+
+ val t = newTable N a
+
+ val m = NameArityMap.insert m (n_a,t)
+
+ val () = tm := m
+ in
+ t
+ end
+ end;
+
+fun lookupTables tables (n,elts) =
+ let
+ val Tables {domainSize = N, rangeSize = R, ...} = tables
+
+ val a = length elts
+
+ val table = getTables tables (n,a)
+ in
+ lookupTable N R table elts
+ end;
+
+fun updateTables tables ((n,elts),r) =
+ let
+ val Tables {domainSize = N, ...} = tables
+
+ val a = length elts
+
+ val table = getTables tables (n,a)
+ in
+ updateTable N table (elts,r)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of random finite models. *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters = {size : int, fixed : fixed};
+
+datatype model =
+ Model of
+ {size : int,
+ fixedFunctions : (element list -> element option) NameArityMap.map,
+ fixedRelations : (element list -> bool option) NameArityMap.map,
+ randomFunctions : tables,
+ randomRelations : tables};
+
+fun new {size = N, fixed} =
+ let
+ val Fixed {functions = fns, relations = rels} = fixed
+
+ val fixFns = NameArityMap.transform (fn f => f {size = N}) fns
+ and fixRels = NameArityMap.transform (fn r => r {size = N}) rels
+
+ val rndFns = newTables N N
+ and rndRels = newTables N 2
+ in
+ Model
+ {size = N,
+ fixedFunctions = fixFns,
+ fixedRelations = fixRels,
+ randomFunctions = rndFns,
+ randomRelations = rndRels}
+ end;
+
+fun size (Model {size = N, ...}) = N;
+
+fun peekFixedFunction M (n,elts) =
+ let
+ val Model {fixedFunctions = fixFns, ...} = M
+ in
+ case NameArityMap.peek fixFns (n, length elts) of
+ NONE => NONE
+ | SOME fixFn => fixFn elts
+ end;
+
+fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts);
+
+fun peekFixedRelation M (n,elts) =
+ let
+ val Model {fixedRelations = fixRels, ...} = M
+ in
+ case NameArityMap.peek fixRels (n, length elts) of
+ NONE => NONE
+ | SOME fixRel => fixRel elts
+ end;
+
+fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts);
+
+(* A default model *)
+
+val defaultSize = 8;
+
+val defaultFixed =
+ unionListFixed
+ [basicFixed,
+ projectionFixed,
+ modularFixed,
+ setFixed,
+ listFixed];
+
+val default = {size = defaultSize, fixed = defaultFixed};
+
+(* ------------------------------------------------------------------------- *)
+(* Taking apart terms to interpret them. *)
+(* ------------------------------------------------------------------------- *)
+
+fun destTerm tm =
+ case tm of
+ Term.Var _ => tm
+ | Term.Fn f_tms =>
+ case Term.stripApp tm of
+ (_,[]) => tm
+ | (v as Term.Var _, tms) => Term.Fn (Term.appName, v :: tms)
+ | (Term.Fn (f,tms), tms') => Term.Fn (f, tms @ tms');
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting terms and formulas in the model. *)
+(* ------------------------------------------------------------------------- *)
+
+fun interpretFunction M n_elts =
+ case peekFixedFunction M n_elts of
+ SOME r => r
+ | NONE =>
+ let
+ val Model {randomFunctions = rndFns, ...} = M
+ in
+ lookupTables rndFns n_elts
+ end;
+
+fun interpretRelation M n_elts =
+ case peekFixedRelation M n_elts of
+ SOME r => r
+ | NONE =>
+ let
+ val Model {randomRelations = rndRels, ...} = M
+ in
+ intToBool (lookupTables rndRels n_elts)
+ end;
+
+fun interpretTerm M V =
+ let
+ fun interpret tm =
+ case destTerm tm of
+ Term.Var v => getValuation V v
+ | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+ in
+ interpret
+ end;
+
+fun interpretAtom M V (r,tms) =
+ interpretRelation M (r, map (interpretTerm M V) tms);
+
+fun interpretFormula M =
+ let
+ val N = size M
+
+ fun interpret V fm =
+ case fm of
+ Formula.True => true
+ | Formula.False => false
+ | Formula.Atom atm => interpretAtom M V atm
+ | Formula.Not p => not (interpret V p)
+ | Formula.Or (p,q) => interpret V p orelse interpret V q
+ | Formula.And (p,q) => interpret V p andalso interpret V q
+ | Formula.Imp (p,q) => interpret V (Formula.Or (Formula.Not p, q))
+ | Formula.Iff (p,q) => interpret V p = interpret V q
+ | Formula.Forall (v,p) => interpret' V p v N
+ | Formula.Exists (v,p) =>
+ interpret V (Formula.Not (Formula.Forall (v, Formula.Not p)))
+
+ and interpret' V fm v i =
+ i = 0 orelse
+ let
+ val i = i - 1
+ val V' = insertValuation V (v,i)
+ in
+ interpret V' fm andalso interpret' V fm v i
+ end
+ in
+ interpret
+ end;
+
+fun interpretLiteral M V (pol,atm) =
+ let
+ val b = interpretAtom M V atm
+ in
+ if pol then b else not b
+ end;
+
+fun interpretClause M V cl = LiteralSet.exists (interpretLiteral M V) cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Check whether random groundings of a formula are true in the model. *)
+(* Note: if it's cheaper, a systematic check will be performed instead. *)
+(* ------------------------------------------------------------------------- *)
+
+fun check interpret {maxChecks} M fv x =
+ let
+ val N = size M
+
+ fun score (V,{T,F}) =
+ if interpret M V x then {T = T + 1, F = F} else {T = T, F = F + 1}
+
+ fun randomCheck acc = score (randomValuation {size = N} fv, acc)
+
+ val maxChecks =
+ case maxChecks of
+ NONE => maxChecks
+ | SOME m =>
+ case expInt N (NameSet.size fv) of
+ SOME n => if n <= m then NONE else maxChecks
+ | NONE => maxChecks
+ in
+ case maxChecks of
+ SOME m => funpow m randomCheck {T = 0, F = 0}
+ | NONE => foldValuation {size = N} fv score {T = 0, F = 0}
+ end;
+
+fun checkAtom maxChecks M atm =
+ check interpretAtom maxChecks M (Atom.freeVars atm) atm;
+
+fun checkFormula maxChecks M fm =
+ check interpretFormula maxChecks M (Formula.freeVars fm) fm;
+
+fun checkLiteral maxChecks M lit =
+ check interpretLiteral maxChecks M (Literal.freeVars lit) lit;
+
+fun checkClause maxChecks M cl =
+ check interpretClause maxChecks M (LiteralSet.freeVars cl) cl;
+
+(* ------------------------------------------------------------------------- *)
+(* Updating the model. *)
+(* ------------------------------------------------------------------------- *)
+
+fun updateFunction M func_elts_elt =
+ let
+ val Model {randomFunctions = rndFns, ...} = M
+
+ val () = updateTables rndFns func_elts_elt
+ in
+ ()
+ end;
+
+fun updateRelation M (rel_elts,pol) =
+ let
+ val Model {randomRelations = rndRels, ...} = M
+
+ val () = updateTables rndRels (rel_elts, boolToInt pol)
+ in
+ ()
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of terms with interpretations embedded in the subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype modelTerm =
+ ModelVar
+ | ModelFn of Term.functionName * modelTerm list * int list;
+
+fun modelTerm M V =
+ let
+ fun modelTm tm =
+ case destTerm tm of
+ Term.Var v => (ModelVar, getValuation V v)
+ | Term.Fn (f,tms) =>
+ let
+ val (tms,xs) = unzip (map modelTm tms)
+ in
+ (ModelFn (f,tms,xs), interpretFunction M (f,xs))
+ end
+ in
+ modelTm
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Perturbing the model. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype perturbation =
+ FunctionPerturbation of (Term.functionName * element list) * element
+ | RelationPerturbation of (Atom.relationName * element list) * bool;
+
+fun perturb M pert =
+ case pert of
+ FunctionPerturbation func_elts_elt => updateFunction M func_elts_elt
+ | RelationPerturbation rel_elts_pol => updateRelation M rel_elts_pol;
+
+local
+ fun pertTerm _ [] _ acc = acc
+ | pertTerm M target tm acc =
+ case tm of
+ ModelVar => acc
+ | ModelFn (func,tms,xs) =>
+ let
+ fun onTarget ys = mem (interpretFunction M (func,ys)) target
+
+ val func_xs = (func,xs)
+
+ val acc =
+ if isFixedFunction M func_xs then acc
+ else
+ let
+ fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc
+ in
+ foldl add acc target
+ end
+ in
+ pertTerms M onTarget tms xs acc
+ end
+
+ and pertTerms M onTarget =
+ let
+ val N = size M
+
+ fun filterElements pred =
+ let
+ fun filt 0 acc = acc
+ | filt i acc =
+ let
+ val i = i - 1
+ val acc = if pred i then i :: acc else acc
+ in
+ filt i acc
+ end
+ in
+ filt N []
+ end
+
+ fun pert _ [] [] acc = acc
+ | pert ys (tm :: tms) (x :: xs) acc =
+ let
+ fun pred y =
+ y <> x andalso onTarget (List.revAppend (ys, y :: xs))
+
+ val target = filterElements pred
+
+ val acc = pertTerm M target tm acc
+ in
+ pert (x :: ys) tms xs acc
+ end
+ | pert _ _ _ _ = raise Bug "Model.pertTerms.pert"
+ in
+ pert []
+ end;
+
+ fun pertAtom M V target (rel,tms) acc =
+ let
+ fun onTarget ys = interpretRelation M (rel,ys) = target
+
+ val (tms,xs) = unzip (map (modelTerm M V) tms)
+
+ val rel_xs = (rel,xs)
+
+ val acc =
+ if isFixedRelation M rel_xs then acc
+ else RelationPerturbation (rel_xs,target) :: acc
+ in
+ pertTerms M onTarget tms xs acc
+ end;
+
+ fun pertLiteral M V ((pol,atm),acc) = pertAtom M V pol atm acc;
+
+ fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;
+
+ fun pickPerturb M perts =
+ if null perts then ()
+ else perturb M (List.nth (perts, Portable.randomInt (length perts)));
+in
+ fun perturbTerm M V (tm,target) =
+ pickPerturb M (pertTerm M target (fst (modelTerm M V tm)) []);
+
+ fun perturbAtom M V (atm,target) =
+ pickPerturb M (pertAtom M V target atm []);
+
+ fun perturbLiteral M V lit = pickPerturb M (pertLiteral M V (lit,[]));
+
+ fun perturbClause M V cl = pickPerturb M (pertClause M V cl []);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun pp M =
+ Print.program
+ [Print.addString "Model{",
+ Print.ppInt (size M),
+ Print.addString "}"];
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Name.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,45 @@
+(* ========================================================================= *)
+(* NAMES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Name =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of names. *)
+(* ------------------------------------------------------------------------- *)
+
+type name
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : name * name -> order
+
+val equal : name -> name -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh names. *)
+(* ------------------------------------------------------------------------- *)
+
+val newName : unit -> name
+
+val newNames : int -> name list
+
+val variantPrime : (name -> bool) -> name -> name
+
+val variantNum : (name -> bool) -> name -> name
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : name Print.pp
+
+val toString : name -> string
+
+val fromString : string -> name
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Name.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,98 @@
+(* ========================================================================= *)
+(* NAMES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Name :> Name =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of names. *)
+(* ------------------------------------------------------------------------- *)
+
+type name = string;
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare = String.compare;
+
+fun equal n1 n2 = n1 = n2;
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh variables. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val prefix = "_";
+
+ fun numName i = mkPrefix prefix (Int.toString i);
+in
+ fun newName () = numName (newInt ());
+
+ fun newNames n = map numName (newInts n);
+end;
+
+fun variantPrime acceptable =
+ let
+ fun variant n = if acceptable n then n else variant (n ^ "'")
+ in
+ variant
+ end;
+
+local
+ fun isDigitOrPrime #"'" = true
+ | isDigitOrPrime c = Char.isDigit c;
+in
+ fun variantNum acceptable n =
+ if acceptable n then n
+ else
+ let
+ val n = stripSuffix isDigitOrPrime n
+
+ fun variant i =
+ let
+ val n_i = n ^ Int.toString i
+ in
+ if acceptable n_i then n_i else variant (i + 1)
+ end
+ in
+ variant 0
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Print.ppString;
+
+fun toString s : string = s;
+
+fun fromString s : name = s;
+
+end
+
+structure NameOrdered =
+struct type t = Name.name val compare = Name.compare end
+
+structure NameMap = KeyMap (NameOrdered);
+
+structure NameSet =
+struct
+
+ local
+ structure S = ElementSet (NameMap);
+ in
+ open S;
+ end;
+
+ val pp =
+ Print.ppMap
+ toList
+ (Print.ppBracket "{" "}" (Print.ppOpList "," Name.pp));
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/NameArity.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,47 @@
+(* ========================================================================= *)
+(* NAME/ARITY PAIRS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature NameArity =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of name/arity pairs. *)
+(* ------------------------------------------------------------------------- *)
+
+type nameArity = Name.name * int
+
+val name : nameArity -> Name.name
+
+val arity : nameArity -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Testing for different arities. *)
+(* ------------------------------------------------------------------------- *)
+
+val nary : int -> nameArity -> bool
+
+val nullary : nameArity -> bool
+
+val unary : nameArity -> bool
+
+val binary : nameArity -> bool
+
+val ternary : nameArity -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : nameArity * nameArity -> order
+
+val equal : nameArity -> nameArity -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : nameArity Print.pp
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/NameArity.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,91 @@
+(* ========================================================================= *)
+(* NAME/ARITY PAIRS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure NameArity :> NameArity =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of name/arity pairs. *)
+(* ------------------------------------------------------------------------- *)
+
+type nameArity = Name.name * int;
+
+fun name ((n,_) : nameArity) = n;
+
+fun arity ((_,i) : nameArity) = i;
+
+(* ------------------------------------------------------------------------- *)
+(* Testing for different arities. *)
+(* ------------------------------------------------------------------------- *)
+
+fun nary i n_i = arity n_i = i;
+
+val nullary = nary 0
+and unary = nary 1
+and binary = nary 2
+and ternary = nary 3;
+
+(* ------------------------------------------------------------------------- *)
+(* A total ordering. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((n1,i1),(n2,i2)) =
+ case Name.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => Int.compare (i1,i2)
+ | GREATER => GREATER;
+
+fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun pp (n,i) =
+ Print.blockProgram Print.Inconsistent 0
+ [Name.pp n,
+ Print.addString "/",
+ Print.ppInt i];
+
+end
+
+structure NameArityOrdered =
+struct type t = NameArity.nameArity val compare = NameArity.compare end
+
+structure NameArityMap =
+struct
+
+ local
+ structure S = KeyMap (NameArityOrdered);
+ in
+ open S;
+ end;
+
+ fun compose m1 m2 =
+ let
+ fun pk ((_,a),n) = peek m2 (n,a)
+ in
+ mapPartial pk m1
+ end;
+
+end
+
+structure NameAritySet =
+struct
+
+ local
+ structure S = ElementSet (NameArityMap);
+ in
+ open S;
+ end;
+
+ val allNullary = all NameArity.nullary;
+
+ val pp =
+ Print.ppMap
+ toList
+ (Print.ppBracket "{" "}" (Print.ppOpList "," NameArity.pp));
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Normalize.sig Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,55 @@
+(* ========================================================================= *)
+(* NORMALIZING FORMULAS *)
+(* Copyright (c) 2001-2009 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Normalize =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Negation normal form. *)
+(* ------------------------------------------------------------------------- *)
+
+val nnf : Formula.formula -> Formula.formula
+
+(* ------------------------------------------------------------------------- *)
+(* Conjunctive normal form derivations. *)
+(* ------------------------------------------------------------------------- *)
+
+type thm
+
+datatype inference =
+ Axiom of Formula.formula
+ | Definition of string * Formula.formula
+ | Simplify of thm * thm list
+ | Conjunct of thm
+ | Specialize of thm
+ | Skolemize of thm
+ | Clausify of thm
+
+val mkAxiom : Formula.formula -> thm
+
+val destThm : thm -> Formula.formula * inference
+
+val proveThms :
+ thm list -> (Formula.formula * inference * Formula.formula list) list
+
+val toStringInference : inference -> string
+
+val ppInference : inference Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* Conjunctive normal form. *)
+(* ------------------------------------------------------------------------- *)
+
+type cnf
+
+val initialCnf : cnf
+
+val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf
+
+val proveCnf : thm list -> (Thm.clause * thm) list
+
+val cnf : Formula.formula -> Thm.clause list
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Normalize.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,1386 @@
+(* ========================================================================= *)
+(* NORMALIZING FORMULAS *)
+(* Copyright (c) 2001-2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Normalize :> Normalize =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Constants. *)
+(* ------------------------------------------------------------------------- *)
+
+val prefix = "FOFtoCNF";
+
+val skolemPrefix = "skolem" ^ prefix;
+
+val definitionPrefix = "definition" ^ prefix;
+
+(* ------------------------------------------------------------------------- *)
+(* Storing huge real numbers as their log. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype logReal = LogReal of real;
+
+fun compareLogReal (LogReal logX, LogReal logY) =
+ Real.compare (logX,logY);
+
+val zeroLogReal = LogReal ~1.0;
+
+val oneLogReal = LogReal 0.0;
+
+local
+ fun isZero logX = logX < 0.0;
+
+ (* Assume logX >= logY >= 0.0 *)
+ fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
+in
+ fun isZeroLogReal (LogReal logX) = isZero logX;
+
+ fun multiplyLogReal (LogReal logX) (LogReal logY) =
+ if isZero logX orelse isZero logY then zeroLogReal
+ else LogReal (logX + logY);
+
+ fun addLogReal (lx as LogReal logX) (ly as LogReal logY) =
+ if isZero logX then ly
+ else if isZero logY then lx
+ else if logX < logY then LogReal (add logY logX)
+ else LogReal (add logX logY);
+
+ fun withinRelativeLogReal logDelta (LogReal logX) (LogReal logY) =
+ isZero logX orelse
+ (not (isZero logY) andalso logX < logY + logDelta);
+end;
+
+fun toStringLogReal (LogReal logX) = Real.toString logX;
+
+(* ------------------------------------------------------------------------- *)
+(* Counting the clauses that would be generated by conjunctive normal form. *)
+(* ------------------------------------------------------------------------- *)
+
+val countLogDelta = 0.01;
+
+datatype count = Count of {positive : logReal, negative : logReal};
+
+fun countCompare (count1,count2) =
+ let
+ val Count {positive = p1, negative = _} = count1
+ and Count {positive = p2, negative = _} = count2
+ in
+ compareLogReal (p1,p2)
+ end;
+
+fun countNegate (Count {positive = p, negative = n}) =
+ Count {positive = n, negative = p};
+
+fun countLeqish count1 count2 =
+ let
+ val Count {positive = p1, negative = _} = count1
+ and Count {positive = p2, negative = _} = count2
+ in
+ withinRelativeLogReal countLogDelta p1 p2
+ end;
+
+(*MetisDebug
+fun countEqualish count1 count2 =
+ countLeqish count1 count2 andalso
+ countLeqish count2 count1;
+
+fun countEquivish count1 count2 =
+ countEqualish count1 count2 andalso
+ countEqualish (countNegate count1) (countNegate count2);
+*)
+
+val countTrue = Count {positive = zeroLogReal, negative = oneLogReal};
+
+val countFalse = Count {positive = oneLogReal, negative = zeroLogReal};
+
+val countLiteral = Count {positive = oneLogReal, negative = oneLogReal};
+
+fun countAnd2 (count1,count2) =
+ let
+ val Count {positive = p1, negative = n1} = count1
+ and Count {positive = p2, negative = n2} = count2
+ val p = addLogReal p1 p2
+ and n = multiplyLogReal n1 n2
+ in
+ Count {positive = p, negative = n}
+ end;
+
+fun countOr2 (count1,count2) =
+ let
+ val Count {positive = p1, negative = n1} = count1
+ and Count {positive = p2, negative = n2} = count2
+ val p = multiplyLogReal p1 p2
+ and n = addLogReal n1 n2
+ in
+ Count {positive = p, negative = n}
+ end;
+
+(* Whether countXor2 is associative or not is an open question. *)
+
+fun countXor2 (count1,count2) =
+ let
+ val Count {positive = p1, negative = n1} = count1
+ and Count {positive = p2, negative = n2} = count2
+ val p = addLogReal (multiplyLogReal p1 p2) (multiplyLogReal n1 n2)
+ and n = addLogReal (multiplyLogReal p1 n2) (multiplyLogReal n1 p2)
+ in
+ Count {positive = p, negative = n}
+ end;
+
+fun countDefinition body_count = countXor2 (countLiteral,body_count);
+
+val countToString =
+ let
+ val rToS = toStringLogReal
+ in
+ fn Count {positive = p, negative = n} =>
+ "(+" ^ rToS p ^ ",-" ^ rToS n ^ ")"
+ end;
+
+val ppCount = Print.ppMap countToString Print.ppString;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of normalized formula. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ True
+ | False
+ | Literal of NameSet.set * Literal.literal
+ | And of NameSet.set * count * formula Set.set
+ | Or of NameSet.set * count * formula Set.set
+ | Xor of NameSet.set * count * bool * formula Set.set
+ | Exists of NameSet.set * count * NameSet.set * formula
+ | Forall of NameSet.set * count * NameSet.set * formula;
+
+fun compare f1_f2 =
+ if Portable.pointerEqual f1_f2 then EQUAL
+ else
+ case f1_f2 of
+ (True,True) => EQUAL
+ | (True,_) => LESS
+ | (_,True) => GREATER
+ | (False,False) => EQUAL
+ | (False,_) => LESS
+ | (_,False) => GREATER
+ | (Literal (_,l1), Literal (_,l2)) => Literal.compare (l1,l2)
+ | (Literal _, _) => LESS
+ | (_, Literal _) => GREATER
+ | (And (_,_,s1), And (_,_,s2)) => Set.compare (s1,s2)
+ | (And _, _) => LESS
+ | (_, And _) => GREATER
+ | (Or (_,_,s1), Or (_,_,s2)) => Set.compare (s1,s2)
+ | (Or _, _) => LESS
+ | (_, Or _) => GREATER
+ | (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) =>
+ (case boolCompare (p1,p2) of
+ LESS => LESS
+ | EQUAL => Set.compare (s1,s2)
+ | GREATER => GREATER)
+ | (Xor _, _) => LESS
+ | (_, Xor _) => GREATER
+ | (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) =>
+ (case NameSet.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => compare (f1,f2)
+ | GREATER => GREATER)
+ | (Exists _, _) => LESS
+ | (_, Exists _) => GREATER
+ | (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) =>
+ (case NameSet.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => compare (f1,f2)
+ | GREATER => GREATER);
+
+val empty = Set.empty compare;
+
+val singleton = Set.singleton compare;
+
+local
+ fun neg True = False
+ | neg False = True
+ | neg (Literal (fv,lit)) = Literal (fv, Literal.negate lit)
+ | neg (And (fv,c,s)) = Or (fv, countNegate c, neg_set s)
+ | neg (Or (fv,c,s)) = And (fv, countNegate c, neg_set s)
+ | neg (Xor (fv,c,p,s)) = Xor (fv, c, not p, s)
+ | neg (Exists (fv,c,n,f)) = Forall (fv, countNegate c, n, neg f)
+ | neg (Forall (fv,c,n,f)) = Exists (fv, countNegate c, n, neg f)
+
+ and neg_set s = Set.foldl neg_elt empty s
+
+ and neg_elt (f,s) = Set.add s (neg f);
+in
+ val negate = neg;
+
+ val negateSet = neg_set;
+end;
+
+fun negateMember x s = Set.member (negate x) s;
+
+local
+ fun member s x = negateMember x s;
+in
+ fun negateDisjoint s1 s2 =
+ if Set.size s1 < Set.size s2 then not (Set.exists (member s2) s1)
+ else not (Set.exists (member s1) s2);
+end;
+
+fun polarity True = true
+ | polarity False = false
+ | polarity (Literal (_,(pol,_))) = not pol
+ | polarity (And _) = true
+ | polarity (Or _) = false
+ | polar