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
112
113
114
115
116
117
118
119
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
open Util
(*********************)
(* Lifting *)
(*********************)
(* Explicit lifts and basic operations *)
type lift =
| ELID
| ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
| ELLFT of int * lift (* ELLFT(n,l) == apply l to de Bruijn > n *)
(* i.e under n binders *)
(* compose a relocation of magnitude n *)
let rec el_shft_rec n = function
| ELSHFT(el,k) -> el_shft_rec (k+n) el
| el -> ELSHFT(el,n)
let el_shft n el = if n = 0 then el else el_shft_rec n el
(* cross n binders *)
let rec el_liftn_rec n = function
| ELID -> ELID
| ELLFT(k,el) -> el_liftn_rec (n+k) el
| el -> ELLFT(n, el)
let el_liftn n el = if n = 0 then el else el_liftn_rec n el
let el_lift el = el_liftn_rec 1 el
(* relocation of de Bruijn n in an explicit lift *)
let rec reloc_rel n = function
| ELID -> n
| ELLFT(k,el) ->
if n <= k then n else (reloc_rel (n-k) el) + k
| ELSHFT(el,k) -> (reloc_rel (n+k) el)
let rec is_lift_id = function
| ELID -> true
| ELSHFT(e,n) -> n=0 & is_lift_id e
| ELLFT (_,e) -> is_lift_id e
(*********************)
(* Substitutions *)
(*********************)
(* (bounded) explicit substitutions of type 'a *)
type 'a subs =
| ESID of int (* ESID(n) = %n END bounded identity *)
| CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *)
| SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
(* with n vars *)
| LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
(* operations of subs: collapses constructors when possible.
* Needn't be recursive if we always use these functions
*)
let subs_cons(x,s) = CONS(x,s)
let subs_liftn n = function
| ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
| LIFT (p,lenv) -> LIFT (p+n, lenv)
| lenv -> LIFT (n,lenv)
let subs_lift a = subs_liftn 1 a
let subs_shft = function
| (0, s) -> s
| (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
| (n, s) -> SHIFT (n,s)
let subs_shift_cons = function
(0, s, t) -> CONS(t,s)
| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
| (k, s, t) -> CONS(t,SHIFT(k, s));;
(* Tests whether a substitution is extensionnaly equal to the identity *)
let rec is_subs_id = function
ESID _ -> true
| LIFT(_,s) -> is_subs_id s
| SHIFT(0,s) -> is_subs_id s
| _ -> false
(* Expands de Bruijn k in the explicit substitution subs
* lams accumulates de shifts to perform when retrieving the i-th value
* the rules used are the following:
*
* [id]k --> k
* [S.t]1 --> t
* [S.t]k --> [S](k-1) if k > 1
* [^n o S] k --> [^n]([S]k)
* [(%n S)] k --> k if k <= n
* [(%n S)] k --> [^n]([S](k-n))
*
* the result is (Inr (k+lams,p)) when the variable is just relocated
* where p is None if the variable points inside subs and Some(k) if the
* variable points k bindings beyond subs.
*)
let rec exp_rel lams k subs =
match (k,subs) with
| (1, CONS (def,_)) -> Inl(lams,def)
| (_, CONS (_,l)) -> exp_rel lams (pred k) l
| (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None)
| (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
| (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
| (_, ESID n) when k<=n -> Inr(lams+k,None)
| (_, ESID n) -> Inr(lams+k,Some (k-n))
let expand_rel k subs = exp_rel 0 k subs
|
