1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
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"}")
|
