diff --git a/src/egraph_simple.ml b/src/egraph_simple.ml
index df72c4cfe8d107420c17213db2d36531cf8aa97c..e6daee473bb3799143dabe197613535b3f14ba69 100644
--- a/src/egraph_simple.ml
+++ b/src/egraph_simple.ml
@@ -30,6 +30,7 @@
let dont_clean_use = false
+
open Stdlib
open Shuffle
@@ -72,23 +73,25 @@ let rec normalize env cl =
Debug.dprintf debug
"[EGraph] normalize @[%a@]@."
Cl.print cl;
- let cl',env = match UnionFind.base cl with
- | Term.Cst _ as v ->
+ let cl',env =
+ let v = UnionFind.base cl in
+ let leaves = Term.leaves v in
+ if Cl.S.is_empty leaves
+ then
let env = UnionFind.set_repr env cl v in
cl,env
- | Term.App (f,g) ->
- let clf,env = normalize env (UnionFind.find env f) in
- let clg,env = normalize env (UnionFind.find env g) in
- let v = Term.App(clf,clg) in
+ else
+ let env,leaves = Cl.M.mapi_fold (fun arg () env ->
+ let cl, env = normalize env (UnionFind.find env arg) in env,cl)
+ leaves env in
+ let v = Term.subst leaves v in
let cl,env = UnionFind.basecl env v in
if has_repr env cl then cl,env
else
- let env = UnionFind.add_use env cl v clf in
- let env = if not (Cl.equal clf clg)
- then UnionFind.add_use env cl v clg
- else env in
- let env = UnionFind.set_repr env cl v in
- cl,env
+ let env = Cl.M.fold (fun _ norm env ->
+ UnionFind.add_use env cl v norm) leaves env in
+ let env = UnionFind.set_repr env cl v in
+ cl,env
in
let env = UnionFind.union_force env cl cl' in
Debug.dprintf debug
@@ -103,33 +106,31 @@ let add env cl =
Debug.dprintf debug
"[EGraph] Add @[@[%a@]@ as@ @[%a@]@]@."
(print_repr env) cl (print_repr env) cl';
- let rec tag env cl =
+ let rec tag cl env =
if UnionFind.is_added env cl then env
else
let env = UnionFind.added env cl in
- match repr env cl with
- | Term.Cst _ -> env
- | Term.App (f,g) -> tag (tag env f) g
+ let leaves = Term.leaves (repr env cl) in
+ let env = Cl.S.fold tag leaves env in
+ env
in
- cl',tag env cl'
+ cl',tag cl' env
let unuse env cl v =
Debug.dprintf debug
"[EGraph] @[Unuse @[%a@]@ @[%a@]@]@."
(print_repr env) cl (UnionFind.print_value env) v;
- match v with
- | Term.Cst _ -> assert false
+ let leaves = Term.leaves v in
+ if Cl.S.is_empty leaves then
+ assert false
(* no leaves so can't have been used in the first place *)
- | Term.App (clf,clg) ->
- let remove env cl v arg =
+ else
+ let remove arg env =
Debug.dprintf debug " Remove in @[%a@]@\n"
(print_repr env) arg;
UnionFind.remove_use env cl v arg
- in
- let env = remove env cl v clf in
- let env = if not (Cl.equal clf clg)
- then remove env cl v clg
- else env in
+ in
+ let env = Cl.S.fold remove leaves env in
env
let rec is_equal env cl1 cl2 =
@@ -145,12 +146,8 @@ let rec is_equal env cl1 cl2 =
(** t1 -> t2, t1 must be a direct subterm of t3 *)
let subst t1 t2 t3 =
- match t3 with
- | Term.Cst _ -> assert false; (** can't substitute somthing without leaves *)
- | Term.App(f,g) ->
- assert ( Cl.equal t1 f || Cl.equal t1 g);
- let subst t1 t2 arg = if Cl.equal t1 arg then t2 else arg in
- Term.App (subst t1 t2 f, subst t1 t2 g)
+ let s = Cl.M.singleton t1 t2 in
+ Term.subst s t3
exception ExitEnv of UnionFind.t
diff --git a/src/egraph_simple.mli b/src/egraph_simple.mli
index 86344acd6d8f19172191be96d0c8e19dd4a8f093..40516ba9dec7aef34d2a389e0ac22240ca611c8e 100644
--- a/src/egraph_simple.mli
+++ b/src/egraph_simple.mli
@@ -23,8 +23,62 @@
val debug: Debug.flag
+(** For using the theories *)
+
type env = Term.UnionFind.t
val add: env -> Term.cl -> Term.cl * env
val is_equal: env -> Term.cl -> Term.cl -> bool
val equal: env -> Term.cl -> Term.cl -> env
+
+(*
+(** Used by the theories *)
+
+type cl (** class *)
+type value (** semantical value *)
+type delayed (** Environnement given to theories
+ Modifications are delayed
+ *)
+val delayed_of_env : env -> delayed
+val find_cl : delayed -> value -> cl
+
+
+(** Register a theory *)
+
+module type S = sig
+ type repr
+ val print: delayed -> Format.formatter -> repr -> unit
+ val make: repr -> value
+ val extract: value -> repr option
+end
+
+module type Th = sig
+ val kind: thkind
+
+ type repr
+ val hash: repr -> int
+ val equal: repr -> repr -> bool
+
+ val leaves: repr -> Cl.S.t
+ val subst: delayed -> cl Cl.M.t -> repr -> cl
+ (** todo cl? et UnionFind.delayed? *)
+ (** Normally substitute only existing leaves *)
+
+ val solve: delayed -> repr -> value -> cl Cl.M.t * cl
+end
+
+module type ThMake = sig
+ type repr
+
+ module Make(X:S with type repr := repr) : sig
+ val print: (Format.formatter -> cl -> unit) ->
+ Format.formatter -> repr -> unit
+ include Th with type repr := repr
+ end
+end
+
+module Make(X:ThMake): sig
+ include S with type repr = X.repr
+ include Th with type repr := X.repr
+end
+*)
diff --git a/src/term.ml b/src/term.ml
index a0b915afe1f4d61d7e9e85b834be9086928448e3..114c640dd239c2f2d90cd8eb80d416140461522c 100644
--- a/src/term.ml
+++ b/src/term.ml
@@ -29,47 +29,141 @@ let debug = Debug.register_info_flag
type tag = int
-type cl = {
- tag : int;
- base : (** not the representative *) value;
-}
+type thkind =
+ | Polite
+ | Other
-and value =
- | Cst of Strings.Hashcons.t
- | App of cl * cl
+
+module rec Cl : Datatype with type t = Def.cl = struct
+ type t = Def.cl
+ module Cl = MakeMSH(struct type t = Def.cl let tag t = t.Def.tag end)
+ include Cl.T
+ let rec print fmt cl = Format.fprintf fmt "@[@@%i@]" cl.Def.tag
+ include Cl
+end
+
+and ModType : sig
+ module type Th = sig
+ type repr
+
+ val kind: thkind
+
+ val hash: repr -> int
+ val equal: repr -> repr -> bool
+ val print: (Format.formatter -> Cl.t -> unit) ->
+ Format.formatter -> repr -> unit
+
+ val leaves: repr -> Cl.S.t
+ val subst: Cl.t Cl.M.t -> repr -> Def.value
+ val solve: repr -> Def.value -> Cl.t Cl.M.t * Def.value
+ val id: int
+ end
+end = struct
+
+ module type Th = sig
+ type repr
+
+ val kind: thkind
+
+ val hash: repr -> int
+ val equal: repr -> repr -> bool
+ val print: (Format.formatter -> Cl.t -> unit) ->
+ Format.formatter -> repr -> unit
+
+ val leaves: repr -> Cl.S.t
+ val subst: Cl.t Cl.M.t -> repr -> Def.value
+ val solve: repr -> Def.value -> Cl.t Cl.M.t * Def.value
+ val id: int
+ end
+end
+
+and Def : sig
+
+ type 'a th = (module ModType.Th with type repr = 'a)
+
+ type cl = {
+ tag : int;
+ base : (** not the representative *) value;
+ }
+
+ and value =
+ | Value: 'a th * 'a -> value
+end = struct
+ type 'a th = (module ModType.Th with type repr = 'a)
+
+ type cl = {
+ tag : int;
+ base : (** not the representative *) value;
+ }
+
+ and value =
+ | Value: 'a th * 'a -> value
+
+end
+
+include Def
+
+module EqTh = Eqtype.Make(struct type 'a t = 'a th end)
+
+let eqth :
+ type a b. a th -> b th -> (a,b) Eqtype.eq option =
+ fun a b ->
+ let module A = (val a) in
+ let module B = (val b) in
+ if A.id <> B.id then None else
+ match EqTh.eq_type a b with
+ | None -> assert false (** id must be unique *)
+ | x -> x
let equal n m =
- match n, m with
- | Cst i, Cst j -> i = j
- | App (g1,f1), App(g2,f2) -> g1.tag = g2.tag && f1.tag = f2.tag
- | _ -> false
+ match n, m with
+ | Value(nth,nv) , Value(mth,mv) ->
+ match eqth nth mth with
+ | None -> false
+ | Some Eqtype.Eq ->
+ let module Th = (val nth) in
+ Th.equal nv mv
+
+let leaves n =
+ match n with
+ | Value(th,v) ->
+ let module Th = (val th) in
+ Th.leaves v
+
+let subst s n =
+ match n with
+ | Value(th,v) ->
+ let module Th = (val th) in
+ Th.subst s v
+
+let solve n m =
+ match n with
+ | Value(nth,nv) ->
+ let module NTh = (val nth) in
+ match NTh.kind with
+ | Other -> NTh.solve nv m
+ | Polite ->
+ match m with
+ | Value(mth,mv) ->
+ let module MTh = (val mth) in
+ MTh.solve mv n
module ClHashcons = struct
type t = cl
let hash n =
match n.base with
- | Cst i -> 2 * (i :> int)
- | App(g,f) -> 3 * g.tag + 5 * f.tag
+ | Value(nth, n) ->
+ let module Nth = (val nth) in
+ 3 * Nth.id + 17 * Nth.hash n
- let equal n m =
- match n.base, m.base with
- | Cst i, Cst j -> i = j
- | App (g1,f1), App(g2,f2) -> g1.tag = g2.tag && f1.tag = f2.tag
- | _ -> false
+ let equal n m = equal n.base m.base
let tag tag node = {node with tag}
end
-module Cl = struct
- type t = cl
- module Cl = MakeMSH(struct type t = cl let tag t = t.tag end)
- include Cl.T
- let rec print fmt cl = Format.fprintf fmt "@[@@%i@]" cl.tag
- include Cl
-end
-
+let print_depth = ref 7
module UnionFind =
struct
@@ -87,14 +181,12 @@ struct
let repr exn t cl = Cl.M.find_exn exn cl t.repr
let rec print_value nb env fmt v =
- match v with
- | Cst i -> Format.fprintf fmt "%a"
- Strings.Hashcons.print i
- | App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])"
- (print_repr nb env) f (print_repr nb env) g
-
+ match v with
+ | Value (th,v) ->
+ let module Th = (val th) in
+ Th.print (print_repr' nb env) fmt v
- and print_repr nb env fmt k =
+ and print_repr' nb env fmt k =
if nb = 0 then Cl.print fmt k else
try
Format.fprintf fmt "%a"
@@ -102,10 +194,10 @@ struct
with Exit ->
Format.pp_print_string fmt "<NoRepr>"
- let print_value env fmt v = print_value 7 env fmt v
+ let print_value env fmt v = print_value (!print_depth) env fmt v
let print_repr env fmt k =
Format.fprintf fmt "%a[%a]"
- Cl.print k (print_repr 7 env) k
+ Cl.print k (print_repr' (!print_depth) env) k
let empty =
{ eq = Cl.M.empty;
@@ -117,7 +209,7 @@ struct
(** union but t2 becomes the representatives *)
let rec find t cl =
let r = Cl.M.find cl t.eq in
- if Cl.T.equal cl r then r else find t r
+ if Cl.equal cl r then r else find t r
let rec is_findable t cl = Cl.equal (find t cl) cl
@@ -143,40 +235,6 @@ struct
basecl, {t with eq = Cl.M.add basecl basecl t.eq}
let base cl = cl.base
-
- let cst t s = basecl t (Cst (Strings.Hashcons.make s))
- let app t f g = basecl t (App(f,g))
-
-
- let appl t f l =
- let rec aux t = function
- | [] -> assert false
- | [a] -> a,t
- | a::l -> let l,t = aux t l in app t a l in
- let l,t = aux t l in
- app t f l
-
- let fun1 t s =
- let f,t = cst t s in
- (fun t x -> app t f x), t
-
- let fun2 t s =
- let f,t = cst t s in
- (fun t x1 x2 -> appl t f [x1;x2]), t
-
- let fun3 t s =
- let f,t = cst t s in
- (fun t x1 x2 x3 -> appl t f [x1;x2;x3]), t
-
- let fun4 t s =
- let f,t = cst t s in
- (fun t x1 x2 x3 x4 -> appl t f [x1;x2;x3;x4]), t
-
- let fun5 t s =
- let f,t = cst t s in
- (fun t x1 x2 x3 x4 x5 -> appl t f [x1;x2;x3;x4;x5]), t
-
-
(** For others *)
@@ -195,7 +253,7 @@ struct
{t with use =
Cl.M.change (function
| None -> invalid_arg "can't remove what is not here"
- | Some m -> assert( Cl.M.find cl m = v );
+ | Some m -> assert( equal (Cl.M.find cl m) v );
let m = Cl.M.remove cl m in
if Cl.M.is_empty m then None else Some m) arg t.use}
@@ -235,5 +293,69 @@ struct
Format.pp_print_flush fmt ();
close_out cout
+ module Delayed = struct
+ type env = t
+ type t = env ref
+ let basecl env v =
+ let cl,e = basecl !env v in
+ env := e; cl
+ end
end
+
+
+
+module type S = sig
+ type repr
+ val print: UnionFind.t -> Format.formatter -> repr -> unit
+ val make: repr -> value
+ val extract: value -> repr option
+end
+
+module type Th = sig
+ type repr
+
+ val kind: thkind
+
+ val hash: repr -> int
+ val equal: repr -> repr -> bool
+
+ val leaves: repr -> Cl.S.t
+ val subst: Cl.t Cl.M.t -> repr -> value
+ val solve: repr -> Def.value -> Cl.t Cl.M.t * value
+end
+
+module type ThMake = sig
+ type repr
+
+ module Make(X:S with type repr := repr) : sig
+ val print: (Format.formatter -> cl -> unit) ->
+ Format.formatter -> repr -> unit
+ include Th with type repr := repr
+ end
+end
+
+let thid = ref (-1)
+
+module Make(X:ThMake) = struct
+ module rec Th : ModType.Th with type repr = X.repr = struct
+ module T = X.Make(S)
+ type repr = X.repr
+ include T
+ let id = incr thid; !thid
+ end and S : S with type repr := X.repr = struct
+ let th = (module Th : ModType.Th with type repr = X.repr)
+
+ let print env fmt v =
+ Th.print (UnionFind.print_repr' (!print_depth) env) fmt v
+ let make r = Value(th,r)
+ let extract : value -> X.repr option = fun v ->
+ match v with
+ | Value(vth,r) ->
+ match eqth (th: X.repr th) vth with
+ | None -> None
+ | Some Eqtype.Eq -> Some r
+ end
+ include S
+ include (Th : Th with type repr = X.repr)
+end
diff --git a/src/term.mli b/src/term.mli
index 563d508ccb86c07f9dec501e236361c294ada851..aacd819d11f1f0e5184b666523546e7e32b12852 100644
--- a/src/term.mli
+++ b/src/term.mli
@@ -22,16 +22,17 @@
open Stdlib
-type tag = private int
type cl
+module Cl : Datatype with type t = cl
-type value =
- | Cst of Strings.Hashcons.t
- | App of cl * cl
-
+type value
val equal: value -> value -> bool
+val leaves: value -> Cl.S.t
+val subst: cl Cl.M.t -> value -> value
+val solve: value -> value -> cl Cl.M.t * value
+
module UnionFind (* simple *) :
sig
type t
@@ -44,15 +45,6 @@ sig
val union_force: t -> cl -> cl -> t
val iter: (cl -> cl -> unit) -> t -> unit
- val cst: t -> string -> cl * t
- val app: t -> cl -> cl -> cl * t
-
- val fun1 : t -> string -> (t -> cl -> cl * t) * t
- val fun2 : t -> string -> (t -> cl -> cl -> cl * t) * t
- val fun3 : t -> string -> (t -> cl -> cl -> cl -> cl * t) * t
- val fun4 : t -> string -> (t -> cl -> cl -> cl -> cl -> cl * t) * t
- val fun5 : t -> string -> (t -> cl -> cl -> cl -> cl -> cl -> cl * t) * t
-
val repr: exn -> t -> cl -> value
val set_repr: t -> cl -> value -> t
val print_repr: t -> Format.formatter -> cl -> unit
@@ -69,5 +61,46 @@ sig
end
+type thkind =
+ | Polite (** really? don't work with the representant *)
+ | Other (** very precise... *)
+
+
+
+module type S = sig
+ type repr
+ val print: UnionFind.t -> Format.formatter -> repr -> unit
+ val make: repr -> value
+ val extract: value -> repr option
+end
+
+module type Th = sig
+ val kind: thkind
+
+ type repr
+ val hash: repr -> int
+ val equal: repr -> repr -> bool
+
+ val leaves: repr -> Cl.S.t
+ val subst: cl Cl.M.t -> repr -> value
+ (** todo cl? et UnionFind.delayed? *)
+ (** Normally substitute only existing leaves *)
+
+ val solve: repr -> value -> cl Cl.M.t * value
+end
+
+module type ThMake = sig
+ type repr
+
+ module Make(X:S with type repr := repr) : sig
+ val print: (Format.formatter -> cl -> unit) ->
+ Format.formatter -> repr -> unit
+ include Th with type repr := repr
+ end
+end
+
+module Make(X:ThMake): sig
+ include S with type repr = X.repr
+ include Th with type repr := X.repr
+end
-module Cl : Datatype with type t = cl
diff --git a/src/uninterp.ml b/src/uninterp.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0d2d3f7dceb5bf5207da057f1c20d0076a0df9a1
--- /dev/null
+++ b/src/uninterp.ml
@@ -0,0 +1,88 @@
+open Term
+
+
+type t =
+| Cst of Strings.Hashcons.t
+| App of cl * cl
+
+module Th = struct
+ type repr = t
+
+ module Make(X:S with type repr := repr)= struct
+ let kind = Polite
+
+ let equal n m =
+ match n, m with
+ | Cst i, Cst j -> (i :> int) = (j :> int)
+ | App (g1,f1), App(g2,f2) -> Cl.equal g1 g2 && Cl.equal f1 f2
+ | _ -> false
+
+ let hash n =
+ match n with
+ | Cst i -> 2 * (i :> int)
+ | App(g,f) -> 3 * (Cl.hash g) + 5 * (Cl.hash f)
+
+ let print print_cl fmt v =
+ match v with
+ | Cst i -> Format.fprintf fmt "%a"
+ Strings.Hashcons.print i
+ | App (f,g) -> Format.fprintf fmt "(@[%a@],@,@[%a@])"
+ print_cl f print_cl g
+
+ let leaves t =
+ match t with
+ | Cst _ -> Cl.S.empty
+ | App(f,g) ->
+ Cl.S.add g (Cl.S.singleton f)
+
+ (* No more classes to merge than the two given class themselves *)
+ let solve _ v = Cl.M.empty,v
+
+ let subst s t3 =
+ match t3 with
+ | Cst _ -> assert false (** Can't substitute something without leaves *)
+ | App(f,g) ->
+ assert ( Cl.M.mem f s || Cl.M.mem g s);
+ let subst s arg = Cl.M.find_def arg arg s in
+ X.make(App (subst s f,subst s g))
+ end
+
+end
+
+
+module M = Term.Make(Th)
+type env = UnionFind.t
+
+let basecl t r = Term.UnionFind.basecl t (M.make r)
+
+ let cst t s = basecl t (Cst (Strings.Hashcons.make s))
+ let app t f g = basecl t (App(f,g))
+
+
+ let appl t f l =
+ let rec aux t = function
+ | [] -> assert false
+ | [a] -> a,t
+ | a::l -> let l,t = aux t l in app t a l in
+ let l,t = aux t l in
+ app t f l
+
+ let fun1 t s =
+ let f,t = cst t s in
+ (fun t x -> app t f x), t
+
+ let fun2 t s =
+ let f,t = cst t s in
+ (fun t x1 x2 -> appl t f [x1;x2]), t
+
+ let fun3 t s =
+ let f,t = cst t s in
+ (fun t x1 x2 x3 -> appl t f [x1;x2;x3]), t
+
+ let fun4 t s =
+ let f,t = cst t s in
+ (fun t x1 x2 x3 x4 -> appl t f [x1;x2;x3;x4]), t
+
+ let fun5 t s =
+ let f,t = cst t s in
+ (fun t x1 x2 x3 x4 x5 -> appl t f [x1;x2;x3;x4;x5]), t
diff --git a/src/uninterp.mli b/src/uninterp.mli
new file mode 100644
index 0000000000000000000000000000000000000000..368be04f229256b10ed8c9e94836dada3c6a686f
--- /dev/null
+++ b/src/uninterp.mli
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Term
+
+
+type t =
+ | Cst of Strings.Hashcons.t
+ | App of cl * cl
+
+type env = UnionFind.t
+
+val cst: env -> string -> cl * env
+val app: env -> cl -> cl -> cl * env
+
+val fun1 : env -> string -> (env -> cl -> cl * env) * env
+val fun2 : env -> string -> (env -> cl -> cl -> cl * env) * env
+val fun3 : env -> string -> (env -> cl -> cl -> cl -> cl * env) * env
+val fun4 : env -> string -> (env -> cl -> cl -> cl -> cl -> cl * env) * env
+val fun5 : env -> string -> (env -> cl -> cl -> cl -> cl -> cl -> cl * env) * env
diff --git a/src/util/eqtype.ml b/src/util/eqtype.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e6f89763d292c06b03ac083c7b8db865ff119d74
--- /dev/null
+++ b/src/util/eqtype.ml
@@ -0,0 +1,13 @@
+type (_,_) eq = Eq : ('a,'a) eq
+
+module Make(X : sig type 'a t end) =
+struct
+
+ let eq_type :
+ type a b. a X.t -> b X.t -> (a,b) eq option =
+ fun a b ->
+ if Obj.repr a == Obj.repr b
+ then Some (Obj.magic (Eq : (a,a) eq) : (a,b) eq)
+ else None
+
+end
diff --git a/src/util/eqtype.mli b/src/util/eqtype.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ee14f68cac12b8b7d3be44e885eb36bbb59497b1
--- /dev/null
+++ b/src/util/eqtype.mli
@@ -0,0 +1,9 @@
+type (_,_) eq = Eq : ('a,'a) eq
+
+module Make(X : sig type 'a t end) : sig
+
+ val eq_type : 'a X.t -> 'b X.t -> ('a,'b) eq option
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned *)
+
+end
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index de89ca005e88cf25ed8694af9ad0af5f3631cffa..9eb62fb73c935ba7973b3960e02312d6d88eaff1 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -7,12 +7,12 @@ module Uf = Term.UnionFind
let env = Uf.empty
-let f,env = Uf.fun1 env "f"
-let g,env = Uf.fun2 env "g"
+let f,env = Uninterp.fun1 env "f"
+let g,env = Uninterp.fun2 env "g"
-let a,env = Uf.cst env "a"
-let b,env = Uf.cst env "b"
-let c,env = Uf.cst env "c"
+let a,env = Uninterp.cst env "a"
+let b,env = Uninterp.cst env "b"
+let c,env = Uninterp.cst env "c"
let a,env = add env a
let b,env = add env b
@@ -55,8 +55,8 @@ let _2level' () = assert_bool "a = c => f(f(a)) = f(f(c))"
let bigger () =
let env = Uf.empty in
- let f,env = Uf.fun1 env "f" in
- let a,env = Uf.cst env "a" in
+ let f,env = Uninterp.fun1 env "f" in
+ let a,env = Uninterp.cst env "a" in
let fe (c,env) = f env c in
let rec bf env n = if n < 1 then a,env else (fe (bf env (n-1))) in
let fffa, env = adde (bf env 3) in
@@ -108,10 +108,10 @@ let altergo1 =
"h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a" >::
fun () ->
let env = Uf.empty in
- let h,env = Uf.fun1 env "h" in
- let g,env = Uf.fun2 env "g" in
- let x,env = Uf.cst env "x" in
- let a,env = Uf.cst env "a" in
+ let h,env = Uninterp.fun1 env "h" in
+ let g,env = Uninterp.fun2 env "g" in
+ let x,env = Uninterp.cst env "x" in
+ let a,env = Uninterp.cst env "a" in
let hx,env = h env x in
let env = equal env hx x in
let gax, env = g env a x in
@@ -126,12 +126,12 @@ let altergo2 =
h(g(g(x,y),y),a)=h(x,f(a))" >::
fun () ->
let env = Uf.empty in
- let f,env = Uf.fun1 env "f" in
- let h,env = Uf.fun2 env "h" in
- let g,env = Uf.fun2 env "g" in
- let x,env = Uf.cst env "x" in
- let y,env = Uf.cst env "y" in
- let a,env = Uf.cst env "a" in
+ let f,env = Uninterp.fun1 env "f" in
+ let h,env = Uninterp.fun2 env "h" in
+ let g,env = Uninterp.fun2 env "g" in
+ let x,env = Uninterp.cst env "x" in
+ let y,env = Uninterp.cst env "y" in
+ let a,env = Uninterp.cst env "a" in
let rec bf env n = if n < 1 then a,env else (fe (bf env (n-1))) in
let fffa, env = bf env 3 in
let env = equal env fffa a in