From 097106d259d2f41abe56bfa9c44e71705632aed2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 19 Apr 2014 01:27:21 +0200 Subject: [PATCH] rational terms improved, with unification, equality, substitution and De Bruijn index --- ratTerm.ml | 197 ++++++++++++++++++++++++++-------------------------- ratTerm.mli | 20 ++++-- 2 files changed, 115 insertions(+), 102 deletions(-) diff --git a/ratTerm.ml b/ratTerm.ml index 93610a82..722e7fbb 100644 --- a/ratTerm.ml +++ b/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 diff --git a/ratTerm.mli b/ratTerm.mli index 45b4ea14..b84a72d6 100644 --- a/ratTerm.mli +++ b/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