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