diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/rtree.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/rtree.ml')
-rw-r--r-- | lib/rtree.ml | 189 |
1 files changed, 107 insertions, 82 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index cfac6aa4..f395c086 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,17 +8,15 @@ open Util - (* Type of regular trees: - Param denotes tree variables (like de Bruijn indices) the first int is the depth of the occurrence, and the second int - is the index in the array of trees introduced at that depth + is the index in the array of trees introduced at that depth. + Warning: Param's indices both start at 0! - Node denotes the usual tree node, labelled with 'a - Rec(j,v1..vn) introduces infinite tree. It denotes v(j+1) with parameters 0..n-1 replaced by Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively. - Parameters n and higher denote parameters global to the - current Rec node (as usual in de Bruijn binding system) *) type 'a t = Param of int * int @@ -36,27 +34,26 @@ let rec lift_rtree_rec depth n = function | Rec(j,defs) -> Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs) -let lift n t = if n=0 then t else lift_rtree_rec 0 n t +let lift n t = if Int.equal n 0 then t else lift_rtree_rec 0 n t (* The usual subst operation *) let rec subst_rtree_rec depth sub = function Param (i,j) as t -> if i < depth then t - else if i-depth < Array.length sub then - lift depth sub.(i-depth).(j) - else Param (i-Array.length sub,j) + else if i = depth then + lift depth (Rec (j, sub)) + else Param (i - 1, j) | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons) | Rec(j,defs) -> Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs) -let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t +let subst_rtree sub t = subst_rtree_rec 0 sub t (* To avoid looping, we must check that every body introduces a node or a parameter *) let rec expand = function | Rec(j,defs) -> - let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in - expand (subst_rtree sub defs.(j)) + expand (subst_rtree defs defs.(j)) | t -> t (* Given a vector of n bodies, builds the n mutual recursive trees. @@ -65,12 +62,13 @@ let rec expand = function directly one of the parameters of depth 0. Some care is taken to accept definitions like rec X=Y and Y=f(X,Y) *) let mk_rec defs = - let rec check histo d = - match expand d with - Param(0,j) when List.mem j histo -> failwith "invalid rec call" - | Param(0,j) -> check (j::histo) defs.(j) - | _ -> () in - Array.mapi (fun i d -> check [i] d; Rec(i,defs)) defs + let rec check histo d = match expand d with + | Param (0, j) -> + if Int.Set.mem j histo then failwith "invalid rec call" + else check (Int.Set.add j histo) defs.(j) + | _ -> () + in + Array.mapi (fun i d -> check (Int.Set.singleton i) d; Rec(i,defs)) defs (* let v(i,j) = lift i (mk_rec_calls(j+1)).(j);; let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);; @@ -100,69 +98,96 @@ let rec map f t = match t with | Node (a,sons) -> Node (f a, Array.map (map f) sons) | Rec(j,defs) -> Rec (j, Array.map (map f) defs) -let rec smartmap f t = match t with +let smartmap f t = match t with Param _ -> t | Node (a,sons) -> - let a'=f a and sons' = Util.array_smartmap (map f) sons in - if a'==a && sons'==sons then - t - else - Node (a',sons') + let a'=f a and sons' = Array.smartmap (map f) sons in + if a'==a && sons'==sons then t + else Node (a',sons') | Rec(j,defs) -> - let defs' = Util.array_smartmap (map f) defs in - if defs'==defs then - t - else - Rec(j,defs') - -(* Fixpoint operator on trees: - f is the body of the fixpoint. Arguments passed to f are: - - a boolean telling if the subtree has already been seen - - the current subtree - - a function to make recursive calls on subtrees - *) -let fold f t = - let rec fold histo t = - let seen = List.mem t histo in - let nhisto = if not seen then t::histo else histo in - f seen (expand t) (fold nhisto) in - fold [] t - - -(* Tests if a given tree is infinite, i.e. has an branch of infinte length. *) -let is_infinite t = fold - (fun seen t is_inf -> - seen || - (match t with - Node(_,v) -> array_exists is_inf v - | Param _ -> false - | _ -> assert false)) - t - -let fold2 f t x = - let rec fold histo t x = - let seen = List.mem (t,x) histo in - let nhisto = if not seen then (t,x)::histo else histo in - f seen (expand t) x (fold nhisto) in - fold [] t x - -let compare_rtree f = fold2 - (fun seen t1 t2 cmp -> - seen || - let b = f t1 t2 in - if b < 0 then false - else if b > 0 then true - else match expand t1, expand t2 with - Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 -> - array_for_all2 cmp v1 v2 - | _ -> false) - -let eq_rtree cmp t1 t2 = - t1 == t2 || t1=t2 || - compare_rtree - (fun t1 t2 -> - if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0 - else (-1)) t1 t2 + let defs' = Array.smartmap (map f) defs in + if defs'==defs then t + else Rec(j,defs') + +(** Structural equality test, parametrized by an equality on elements *) + +let rec raw_eq cmp t t' = match t, t' with + | Param (i,j), Param (i',j') -> Int.equal i i' && Int.equal j j' + | Node (x, a), Node (x', a') -> cmp x x' && Array.equal (raw_eq cmp) a a' + | Rec (i, a), Rec (i', a') -> Int.equal i i' && Array.equal (raw_eq cmp) a a' + | _ -> false + +let raw_eq2 cmp (t,u) (t',u') = raw_eq cmp t t' && raw_eq cmp u u' + +(** Equivalence test on expanded trees. It is parametrized by two + equalities on elements: + - [cmp] is used when checking for already seen trees + - [cmp'] is used when comparing node labels. *) + +let equiv cmp cmp' = + let rec compare histo t t' = + List.mem_f (raw_eq2 cmp) (t,t') histo || + match expand t, expand t' with + | Node(x,v), Node(x',v') -> + cmp' x x' && + Int.equal (Array.length v) (Array.length v') && + Array.for_all2 (compare ((t,t')::histo)) v v' + | _ -> false + in compare [] + +(** The main comparison on rtree tries first physical equality, then + the structural one, then the logical equivalence *) + +let equal cmp t t' = + t == t' || raw_eq cmp t t' || equiv cmp cmp t t' + +(** Deprecated alias *) +let eq_rtree = equal + +(** Intersection of rtrees of same arity *) +let rec inter cmp interlbl def n histo t t' = + try + let (i,j) = List.assoc_f (raw_eq2 cmp) (t,t') histo in + Param (n-i-1,j) + with Not_found -> + match t, t' with + | Param (i,j), Param (i',j') -> + assert (Int.equal i i' && Int.equal j j'); t + | Node (x, a), Node (x', a') -> + (match interlbl x x' with + | None -> mk_node def [||] + | Some x'' -> Node (x'', Array.map2 (inter cmp interlbl def n histo) a a')) + | Rec (i,v), Rec (i',v') -> + (* If possible, we preserve the shape of input trees *) + if Int.equal i i' && Int.equal (Array.length v) (Array.length v') then + let histo = ((t,t'),(n,i))::histo in + Rec(i, Array.map2 (inter cmp interlbl def (n+1) histo) v v') + else + (* Otherwise, mutually recursive trees are transformed into nested trees *) + let histo = ((t,t'),(n,0))::histo in + Rec(0, [|inter cmp interlbl def (n+1) histo (expand t) (expand t')|]) + | Rec _, _ -> inter cmp interlbl def n histo (expand t) t' + | _ , Rec _ -> inter cmp interlbl def n histo t (expand t') + | _ -> assert false + +let inter cmp interlbl def t t' = inter cmp interlbl def 0 [] t t' + +(** Inclusion of rtrees. We may want a more efficient implementation. *) +let incl cmp interlbl def t t' = + equal cmp t (inter cmp interlbl def t t') + +(** Tests if a given tree is infinite, i.e. has a branch of infinite length. + This corresponds to a cycle when visiting the expanded tree. + We use a specific comparison to detect already seen trees. *) + +let is_infinite cmp t = + let rec is_inf histo t = + List.mem_f (raw_eq cmp) t histo || + match expand t with + | Node (_,v) -> Array.exists (is_inf (t::histo)) v + | _ -> false + in + is_inf [] t (* Pretty-print a tree (not so pretty) *) open Pp @@ -173,11 +198,11 @@ let rec pp_tree prl t = | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") | Node(lab,v) -> hov 2 (str"("++prl lab++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")") + prvect_with_sep pr_comma (pp_tree prl) v++str")") | Rec(i,v) -> - if Array.length v = 0 then str"Rec{}" - else if Array.length v = 1 then + if Int.equal (Array.length v) 0 then str"Rec{}" + else if Int.equal (Array.length v) 1 then hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") else hov 2 (str"Rec{"++int i++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}") + prvect_with_sep pr_comma (pp_tree prl) v++str"}") |