mirror of
https://github.com/c-cube/ocaml-containers.git
synced 2025-12-06 03:05:28 -05:00
rational terms improved, with unification, equality, substitution and De Bruijn index
This commit is contained in:
Simon Cruanes
parent
3167afe929
commit
097106d259
2 changed files with 115 additions and 102 deletions
197
ratTerm.ml
197
ratTerm.ml
|
|
@ -38,9 +38,11 @@ module type S = sig
|
|||
type t = private
|
||||
| Var of int
|
||||
| Ref of int
|
||||
| App of Symbol.t * int option * t list
|
||||
| App of Symbol.t * t list
|
||||
|
||||
type term = t
|
||||
|
||||
type 'a env = 'a RAL.t
|
||||
|
||||
(** Structural equality and comparisons. Two terms being different
|
||||
for {!eq} may still be equal, but with distinct representations.
|
||||
|
|
@ -50,15 +52,21 @@ module type S = sig
|
|||
val eq : t -> t -> bool
|
||||
val cmp : t -> t -> int
|
||||
|
||||
val eq_set : t -> t -> bool
|
||||
(** Proper equality on terms. This returns [true] if the two terms represent
|
||||
the same infinite tree, not only if they have the same shape. *)
|
||||
|
||||
val var : unit -> t
|
||||
(** free variable, with a fresh name *)
|
||||
|
||||
val mk_ref : int -> t
|
||||
(** Back-ref of [n] levels down (see De Bruijn indices) *)
|
||||
|
||||
val app : Symbol.t -> t list -> t
|
||||
(** Application of a symbol to a list, possibly with a unique label *)
|
||||
|
||||
val app_fix : Symbol.t -> (t -> t list) -> t
|
||||
(** Same as {!app}, but the arguments are generated by a function
|
||||
that takes a reference to the result as a parameter. *)
|
||||
val const : Symbol.t -> t
|
||||
(** Shortcut for [app s []] *)
|
||||
|
||||
val pp : Buffer.t -> t -> unit
|
||||
val fmt : Format.formatter -> t -> unit
|
||||
|
|
@ -72,7 +80,7 @@ module type S = sig
|
|||
val empty : t
|
||||
val bind : t -> int -> term -> t
|
||||
val deref : t -> term -> term
|
||||
val apply : t -> term -> term
|
||||
val apply : ?depth:int -> t -> term -> term
|
||||
|
||||
val pp : Buffer.t -> t -> unit
|
||||
val fmt : Format.formatter -> t -> unit
|
||||
|
|
@ -89,7 +97,7 @@ module Make(Symbol : SYMBOL) = struct
|
|||
type t =
|
||||
| Var of int
|
||||
| Ref of int
|
||||
| App of Symbol.t * int option * t list
|
||||
| App of Symbol.t * t list
|
||||
|
||||
type term = t
|
||||
|
||||
|
|
@ -103,9 +111,8 @@ module Make(Symbol : SYMBOL) = struct
|
|||
let hash i = i land max_int
|
||||
end)
|
||||
|
||||
let _add_ref map t = match t with
|
||||
| App (_, Some i, _) -> IMap.add i t map
|
||||
| _ -> map
|
||||
type 'a env = 'a RAL.t
|
||||
(** Environment for De Bruijn variables: a random-access list. *)
|
||||
|
||||
let _to_int = function
|
||||
| Var _ -> 1
|
||||
|
|
@ -115,7 +122,7 @@ module Make(Symbol : SYMBOL) = struct
|
|||
let rec cmp t1 t2 = match t1, t2 with
|
||||
| Var i1, Var i2 -> i1 - i2
|
||||
| Ref i1, Ref i2 -> i1 - i2
|
||||
| App (f1, r1, l1), App (f2, r2, l2) ->
|
||||
| App (f1, l1), App (f2, l2) ->
|
||||
let c = Symbol.compare f1 f2 in
|
||||
if c <> 0 then c
|
||||
else cmp_list l1 l2
|
||||
|
|
@ -130,6 +137,33 @@ module Make(Symbol : SYMBOL) = struct
|
|||
|
||||
let eq t1 t2 = cmp t1 t2 = 0
|
||||
|
||||
module Set2T = Set.Make(struct
|
||||
type t = term*term
|
||||
let compare (l1,r1)(l2,r2) =
|
||||
let c = cmp l1 l2 in
|
||||
if c <> 0 then c else cmp r1 r2
|
||||
end)
|
||||
|
||||
let eq_set t1 t2 =
|
||||
let cycle = ref Set2T.empty in
|
||||
let rec eq env t1 t2 = match t1, t2 with
|
||||
| Ref i, _ -> eq env (RAL.get env i) t2
|
||||
| _, Ref j -> eq env t1 (RAL.get env j)
|
||||
| Var i, Var j -> i=j
|
||||
| _ when Set2T.mem (t1,t2) !cycle -> true
|
||||
| App(f1,l1), App(f2,l2) when Symbol.compare f1 f2 = 0 ->
|
||||
(* if the subterms are equal, and we try to solve again t1=t2,
|
||||
then we shouldn't cycle. Hence we protect ourself. *)
|
||||
cycle := Set2T.add (t1, t2) !cycle;
|
||||
let env = RAL.cons t1 env in
|
||||
begin try
|
||||
List.for_all2 (eq env) l1 l2
|
||||
with Invalid_argument _ -> false
|
||||
end
|
||||
| _ -> false
|
||||
in
|
||||
eq RAL.empty t1 t2
|
||||
|
||||
let _count = ref 0
|
||||
|
||||
let var () =
|
||||
|
|
@ -137,25 +171,18 @@ module Make(Symbol : SYMBOL) = struct
|
|||
incr _count;
|
||||
v
|
||||
|
||||
let app s l = App (s, None, l)
|
||||
let mk_ref i = Ref i
|
||||
|
||||
let app_fix s f =
|
||||
let i = !_count in
|
||||
incr _count;
|
||||
let l = f (Ref i) in
|
||||
match l with
|
||||
| [] -> App (s, None, [])
|
||||
| _ -> App (s, Some i, l)
|
||||
let app s l = App (s, l)
|
||||
|
||||
let const s = App (s, [])
|
||||
|
||||
let rec pp buf t = match t with
|
||||
| Var i -> Printf.bprintf buf "X%d" i
|
||||
| Ref i -> Printf.bprintf buf "*%d" i
|
||||
| App (_, Some _, []) -> assert false
|
||||
| App (s, None, []) ->
|
||||
| App (s, []) ->
|
||||
Buffer.add_string buf (Symbol.to_string s)
|
||||
| App (s, Some r, l) ->
|
||||
Printf.bprintf buf "%d: %s(%a)" r (Symbol.to_string s) pp_list l
|
||||
| App (s, None, l) ->
|
||||
| App (s, l) ->
|
||||
Printf.bprintf buf "%s(%a)" (Symbol.to_string s) pp_list l
|
||||
and pp_list buf l = match l with
|
||||
| [] -> ()
|
||||
|
|
@ -172,7 +199,7 @@ module Make(Symbol : SYMBOL) = struct
|
|||
|
||||
let rename t =
|
||||
let names = IHTbl.create 16 in
|
||||
let rec rename back t = match t with
|
||||
let rec rename t = match t with
|
||||
| Var i ->
|
||||
begin try IHTbl.find names i
|
||||
with Not_found ->
|
||||
|
|
@ -181,18 +208,10 @@ module Make(Symbol : SYMBOL) = struct
|
|||
IHTbl.add names i v;
|
||||
v
|
||||
end
|
||||
| Ref i ->
|
||||
begin try IMap.find i back
|
||||
with Not_found -> failwith "ill-formed term"
|
||||
end
|
||||
| App (s, None, l) ->
|
||||
app s (List.map (rename back) l)
|
||||
| App (s, Some r, l) ->
|
||||
app_fix s
|
||||
(fun r' ->
|
||||
let back' = IMap.add r r' back in
|
||||
List.map (rename back') l)
|
||||
in rename IMap.empty t
|
||||
| Ref _ -> t (* no need to rename *)
|
||||
| App (s, l) ->
|
||||
app s (List.map rename l)
|
||||
in rename t
|
||||
|
||||
module Subst = struct
|
||||
type t = term IMap.t
|
||||
|
|
@ -218,66 +237,47 @@ module Make(Symbol : SYMBOL) = struct
|
|||
match deref subst t with
|
||||
| Var _ -> eq var t
|
||||
| Ref _
|
||||
| App (_, _, []) -> false
|
||||
| App (_, _, l) -> List.exists (_occur subst ~var) l
|
||||
| App (_, []) -> false
|
||||
| App (_, l) -> List.exists (_occur subst ~var) l
|
||||
|
||||
let apply subst t =
|
||||
let names = IHTbl.create 16 in
|
||||
let rec apply subst t = match t with
|
||||
| Ref i ->
|
||||
begin try
|
||||
IHTbl.find names i
|
||||
with Not_found -> failwith "Subst.apply: invalid term"
|
||||
end
|
||||
let apply ?(depth=0) subst t =
|
||||
(* [depth]: current depth w.r.t root, [back]: map from var to
|
||||
the depth of the term they are bound to *)
|
||||
let rec apply depth back subst t = match t with
|
||||
| Ref _ -> t
|
||||
| Var i ->
|
||||
let t' = deref subst t in
|
||||
(* interesting case. Either [t] is bound to a term [t']
|
||||
that contains it, which makes a cyclic term, or it's
|
||||
not in which case it's easy. *)
|
||||
begin match t' with
|
||||
| Ref _ -> t'
|
||||
| App (s, Some r, l) ->
|
||||
| Ref _ -> t
|
||||
| App (s, l) ->
|
||||
if _occur subst ~var:t t'
|
||||
then
|
||||
then
|
||||
(* in any case we are possibly going to modify [r']
|
||||
by replacing [x] by a backref. Therefore we need a
|
||||
new backref to designate the new term. *)
|
||||
app_fix s
|
||||
(fun r' ->
|
||||
(* alias r -> r' *)
|
||||
IHTbl.add names r r';
|
||||
(* now [x] designates the cyclic term, ie [r'] *)
|
||||
let subst' = IMap.add i r' subst in
|
||||
List.map (apply subst') l)
|
||||
else
|
||||
(* simply evaluate [t'] *)
|
||||
apply subst t'
|
||||
| App (s, None, l) ->
|
||||
(* same problem: does [x] introduce a cycle? *)
|
||||
if _occur subst ~var:t t'
|
||||
then
|
||||
app_fix s
|
||||
(fun r' ->
|
||||
let subst' = IMap.add i r' subst in
|
||||
List.map (apply subst') l)
|
||||
else apply subst t'
|
||||
by replacing [x] by a backref. *)
|
||||
let back = IMap.add i depth back in
|
||||
let subst = IMap.remove i subst in
|
||||
app s (List.map (apply (depth+1) back subst) l)
|
||||
else
|
||||
(* simply keep t'->s(l) *)
|
||||
app s (List.map (apply (depth+1) back subst) l)
|
||||
| Var j ->
|
||||
assert (not (IMap.mem j subst));
|
||||
t'
|
||||
begin try
|
||||
let k = IMap.find j back in
|
||||
(* the variable is actually bound to a superterm,
|
||||
which is at depth [k]. The depth difference is
|
||||
therefore [depth-k]. *)
|
||||
Ref (depth-k)
|
||||
with Not_found ->
|
||||
t' (* truly unbound variable. *)
|
||||
end
|
||||
end
|
||||
| App (s, None, l) ->
|
||||
app s (List.map (apply subst) l)
|
||||
| App (s, Some r, l) ->
|
||||
begin try
|
||||
(* alias? *)
|
||||
IHTbl.find names r
|
||||
with Not_found ->
|
||||
app_fix s
|
||||
(fun r' ->
|
||||
IHTbl.add names r r';
|
||||
List.map (apply subst) l)
|
||||
end
|
||||
in apply subst t
|
||||
| App (s, l) ->
|
||||
app s (List.map (apply (depth+1) back subst) l)
|
||||
in apply depth IMap.empty subst t
|
||||
|
||||
let pp buf subst =
|
||||
Buffer.add_string buf "{";
|
||||
|
|
@ -300,31 +300,34 @@ module Make(Symbol : SYMBOL) = struct
|
|||
|
||||
exception Fail
|
||||
|
||||
let _add_tbl tbl r t = match r with
|
||||
| None -> ()
|
||||
| Some r -> IHTbl.replace tbl r t
|
||||
|
||||
let matching ?(subst=Subst.empty) t1 t2 =
|
||||
assert false (* TODO (need to gather variables of [t2]... *)
|
||||
|
||||
let unify ?(subst=Subst.empty) t1 t2 =
|
||||
let names = IHTbl.create 16 in
|
||||
let rec unif subst t1 t2 =
|
||||
(* pairs of terms already unified *)
|
||||
let cycle = ref Set2T.empty in
|
||||
(* [env] contains references to superterms *)
|
||||
let rec unif env subst t1 t2 =
|
||||
match Subst.deref subst t1, Subst.deref subst t2 with
|
||||
| Ref i1, _ -> unif env subst (RAL.get env i1) t2
|
||||
| _, Ref i2 -> unif env subst t1 (RAL.get env i2)
|
||||
| Var i, Var j when i=j -> subst
|
||||
| Var i, _ -> Subst.bind subst i t2
|
||||
| _, Var j -> Subst.bind subst j t1
|
||||
| Ref i1, _ -> unif subst (IHTbl.find names i1) t2
|
||||
| _, Ref i2 -> unif subst t1 (IHTbl.find names i2)
|
||||
| App (f1, r1, l1), App (f2, r2, l2) ->
|
||||
| t1, t2 when Set2T.mem (t1,t2) !cycle ->
|
||||
subst (* t1,t2 already being unified, avoid cycling forever *)
|
||||
| App (f1, l1) as t1, (App (f2, l2) as t2) ->
|
||||
if Symbol.compare f1 f2 <> 0 then raise Fail;
|
||||
_add_tbl names r1 t1;
|
||||
_add_tbl names r2 t2;
|
||||
(* remember we are unifying those terms *)
|
||||
cycle := Set2T.add (t1, t2) !cycle;
|
||||
(* now we can assume [t1 = t2] if unification succeeds, so
|
||||
we just push [t1] into the env *)
|
||||
let env = RAL.cons t1 env in
|
||||
try
|
||||
List.fold_left2 unif subst l1 l2
|
||||
List.fold_left2 (unif env) subst l1 l2
|
||||
with Invalid_argument _ -> raise Fail
|
||||
in
|
||||
try Some (unif subst t1 t2)
|
||||
try Some (unif RAL.empty subst t1 t2)
|
||||
with Fail -> None
|
||||
end
|
||||
|
||||
|
|
|
|||
20
ratTerm.mli
20
ratTerm.mli
|
|
@ -38,9 +38,11 @@ module type S = sig
|
|||
type t = private
|
||||
| Var of int
|
||||
| Ref of int
|
||||
| App of Symbol.t * int option * t list
|
||||
| App of Symbol.t * t list
|
||||
|
||||
type term = t
|
||||
|
||||
type 'a env = 'a RAL.t
|
||||
|
||||
(** Structural equality and comparisons. Two terms being different
|
||||
for {!eq} may still be equal, but with distinct representations.
|
||||
|
|
@ -50,15 +52,21 @@ module type S = sig
|
|||
val eq : t -> t -> bool
|
||||
val cmp : t -> t -> int
|
||||
|
||||
val eq_set : t -> t -> bool
|
||||
(** Proper equality on terms. This returns [true] if the two terms represent
|
||||
the same infinite tree, not only if they have the same shape. *)
|
||||
|
||||
val var : unit -> t
|
||||
(** free variable, with a fresh name *)
|
||||
|
||||
val mk_ref : int -> t
|
||||
(** Back-ref of [n] levels down (see De Bruijn indices) *)
|
||||
|
||||
val app : Symbol.t -> t list -> t
|
||||
(** Application of a symbol to a list, possibly with a unique label *)
|
||||
|
||||
val app_fix : Symbol.t -> (t -> t list) -> t
|
||||
(** Same as {!app}, but the arguments are generated by a function
|
||||
that takes a reference to the result as a parameter. *)
|
||||
val const : Symbol.t -> t
|
||||
(** Shortcut for [app s []] *)
|
||||
|
||||
val pp : Buffer.t -> t -> unit
|
||||
val fmt : Format.formatter -> t -> unit
|
||||
|
|
@ -72,7 +80,7 @@ module type S = sig
|
|||
val empty : t
|
||||
val bind : t -> int -> term -> t
|
||||
val deref : t -> term -> term
|
||||
val apply : t -> term -> term
|
||||
val apply : ?depth:int -> t -> term -> term
|
||||
|
||||
val pp : Buffer.t -> t -> unit
|
||||
val fmt : Format.formatter -> t -> unit
|
||||
|
|
@ -90,6 +98,8 @@ module Str : SYMBOL with type t = string
|
|||
module Default : sig
|
||||
include S with module Symbol = Str
|
||||
|
||||
(* TODO
|
||||
val of_string : string -> t option
|
||||
val of_string_exn : string -> t (** @raise Failure possibly *)
|
||||
*)
|
||||
end
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue