1(* ======================================================================== *)
2(* FILE          : Subst.sml                                                *)
3(* DESCRIPTION   : Explicit substitutions                                   *)
4(*                                                                          *)
5(* AUTHOR        : (c) Bruno Barras, Cambridge University and               *)
6(*                                   INRIA Rocquencourt                     *)
7(* DATE          : 1999                                                     *)
8(*                                                                          *)
9(*                                                                          *)
10(* Type of explicit substitutions on an abstract type of term 'a.           *)
11(*                                                                          *)
12(* - Id is the identity substitution                                        *)
13(*     { 0/0 .... i/i ... }                                                 *)
14(*                                                                          *)
15(* - Cons(S,T) is the parallel substitution                                 *)
16(*     { T/0 S(0)/1 .... S(i-1)/i ... }                                     *)
17(*                                                                          *)
18(* - Shift(k,S) is substitution S followed by a relocation of k:            *)
19(*     { k/0 .... i+k/i ... } o S   or  { ^k(S(0))/0 ... ^k(S(i))/i ... }   *)
20(*                                                                          *)
21(* - Lift(k,S) applies S without affecting the k last variables:            *)
22(*     { 0/0 ... k-1/k-1  ^k(S(0))/k ...  ^k(S(i))/k+i ... }                *)
23(* ======================================================================== *)
24
25
26structure Subst :> Subst =
27struct
28
29datatype 'a subs =
30    Id
31  | Cons  of 'a subs * 'a
32  | Shift of int * 'a subs
33  | Lift  of int * 'a subs
34;
35
36(*---------------------------------------------------------------------------
37 * These constructors allow the following invariants to be asserted:
38 *
39 *  - shifts and lifts always collapsed (and non-zero)
40 *  - no Lift(_,Id), which is equivalent to Id
41 *
42 *---------------------------------------------------------------------------*)
43
44val id = Id;
45
46val cons = Cons;
47
48fun shift (0, s)           = s
49  | shift (k, Shift(k',s)) = shift(k+k', s)
50  | shift (k, s)           = Shift(k,s)
51;
52
53fun lift (0, s)          = s
54  | lift (k, Id)         = Id
55  | lift (k, Lift(k',s)) = lift(k+k', s)
56  | lift (k, s)          = Lift(k,s)
57;
58
59fun is_id Id = true
60  | is_id _ = false;
61
62
63(*---------------------------------------------------------------------------
64 * Destructor: applies substitution subs to de Bruijn index db. In other
65 * words, sigma-reduces [subs]db.
66 * Returns:
67 *  - (n,SOME t) when db is bound by a Cons(_,t). n is the number of variables
68 *    to relocate t. i.e.    [subs]db reduces to ^n(t)
69 *  - (n,NONE) when variable db was bound by a Lift or Id. This means that
70 *    [subs]db reduces to n.
71 *---------------------------------------------------------------------------*)
72
73fun exp_rel (subs,db) =
74  let fun exp (lams, Id,         n) = (lams+n, NONE)
75        | exp (lams, Cons(s,x),  0) = (lams, SOME x)
76        | exp (lams, Cons(s,x),  n) = exp(lams, s, n-1)
77        | exp (lams, Shift(k,s), n) = exp(lams+k, s, n)
78        | exp (lams, Lift(k,s),  n) = if n < k then (lams+n, NONE)
79                                      else exp(lams+k, s, n-k)
80  in exp(0,subs,db)
81  end
82;
83
84(*---------------------------------------------------------------------------
85 * Composition of 2 substitution. We need to provide a function [mk_cl] that
86 * given a subst S and a term t, builds the term [S]t.
87 *
88 * There is a critical pair: (Shift(k,s)) o (Cons(s',x)) could be reduced in
89 * 2 ways:
90 *     Cons(shift k (s o s'), mk_cl (Shift(k,s)) x)
91 *  or shift k (Cons (s o s', mk_cl s x)) <-- was prefered
92 *---------------------------------------------------------------------------*)
93
94fun comp mk_cl =
95  let fun Id           o s'             = s'
96        | s            o Id             = s
97        | (Shift(k,s)) o s'             = shift(k, s o s')
98        | s            o (Cons(s',x))   = Cons(s o s', mk_cl(s,x))
99        | (Cons(s,x))  o (Shift(k,s'))  = s o shift(k-1, s')
100        | (Cons(s,x))  o (Lift(k,s'))   = Cons(s o lift(k-1, s'), x)
101        | (Lift(k,s))  o (Shift(k',s')) = if k<k'
102                                          then shift(k, s o shift(k'-k, s'))
103                                          else shift(k', lift(k-k', s) o s')
104        | (Lift(k,s))  o (Lift(k',s'))  = if k<k'
105                                          then lift(k, s o lift(k'-k, s'))
106                                          else lift(k', lift(k-k', s) o s')
107  in (op o)
108  end
109;
110
111
112end;
113