From 909d7c9edd05868d1fba2dae65e6ff775a41dcbe Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 14 Feb 2002 15:54:01 +0000
Subject: - Reforme de la gestion des args recursifs (via arbres reguliers) -
 coqtop -byte -opt bouclait!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/rtree.ml  | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 lib/rtree.mli |  34 ++++++++++++++++++
 2 files changed, 145 insertions(+)
 create mode 100644 lib/rtree.ml
 create mode 100644 lib/rtree.mli

(limited to 'lib')

diff --git a/lib/rtree.ml b/lib/rtree.ml
new file mode 100644
index 0000000000..9361a28589
--- /dev/null
+++ b/lib/rtree.ml
@@ -0,0 +1,111 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+
+(* Type of regular trees:
+   - Param denotes tree variables (like de Bruijn indices)
+   - Node denotes the usual tree node, labelles 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 globals to the
+     current Rec node (as usual in de Bruijn binding system)
+ *)
+type 'a t =
+    Param of int 
+  | Node of 'a * 'a t array
+  | Rec of int * 'a t array
+
+(* Building trees *)
+let mk_param i = Param i
+let mk_node lab sons = Node (lab, sons)
+
+(* Given a vector of n bodies, builds the n mutual recursive trees.
+   Recursive calls are made with parameters 0 to n-1. We check
+   the bodies actually build something by checking it is not
+   directly one of the parameters 0 to n-1. *)
+let mk_rec defs =
+  Array.mapi
+    (fun i d ->
+      (match d with
+          Param k when k < Array.length defs -> failwith "invalid rec call"
+        | _ -> ());
+      Rec(i,defs))
+    defs
+
+(* The usual lift operation *)
+let rec lift_rtree_rec depth n = function
+    Param i -> if i < depth then Param i else Param (i+n)
+  | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons)
+  | Rec(j,defs) ->
+      Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs)
+
+let lift n t = if 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 ->
+      if i < depth then Param i
+      else if i-depth < Array.length sub then lift depth sub.(i-depth)
+      else Param (i-Array.length sub)
+  | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
+  | Rec(j,defs) ->
+      Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs)
+
+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_rtree = function
+  | Rec(j,defs) ->
+      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
+      expand_rtree (subst_rtree sub defs.(j))
+  | t -> t
+
+(* Tree destructors, expanding loops when necessary *)
+let dest_param t = 
+  match expand_rtree t with
+      Param i -> i
+    | _ -> failwith "dest_param"
+
+let dest_node t = 
+  match expand_rtree t with
+      Node (l,sons) -> (l,sons)
+    | _ -> failwith "dest_node"
+
+(* Tests if a given tree is infinite or not. It proceeds *)
+let rec is_infinite = function
+    Param i -> i = (-1)
+  | Node(_,sons) -> Util.array_exists is_infinite sons
+  | Rec(j,defs) ->
+      let newdefs =
+        Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in
+      let sub =
+        Array.init (Array.length defs)
+          (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in
+      is_infinite (subst_rtree sub defs.(j))
+
+(* Pretty-print a tree (not so pretty) *)
+open Pp
+
+let rec pp_tree prl t =
+  match t with
+      Param k -> str"#"++int k
+    | 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_coma (pp_tree prl) v++str")")
+    | Rec(i,v) ->
+        if Array.length v = 0 then str"Rec{}"
+        else if 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_coma (pp_tree prl) v++str"}")
diff --git a/lib/rtree.mli b/lib/rtree.mli
new file mode 100644
index 0000000000..5a34c819e6
--- /dev/null
+++ b/lib/rtree.mli
@@ -0,0 +1,34 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(* Type of regular tree with nodes labelled by values of type 'a *)
+type 'a t
+
+(* Building trees *)
+(* build a recursive call *) 
+val mk_param : int -> 'a t
+(* build a node given a label and the vector of sons *)
+val mk_node  : 'a -> 'a t array -> 'a t
+(* build mutually dependent trees *)
+val mk_rec   : 'a t array -> 'a t array
+
+(* [lift k t] increases of [k] the free parameters of [t]. Needed
+   to avoid captures when a tree appears under mk_rec *) 
+val lift : int -> 'a t -> 'a t
+
+(* Destructors (recursive calls are expanded) *)
+val dest_param : 'a t -> int
+val dest_node  : 'a t -> 'a * 'a t array
+
+(* Tells if a tree has an infinite branch *)
+val is_infinite : 'a t -> bool
+
+(* A rather simple minded pretty-printer *)
+val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
-- 
cgit v1.2.3