0 | ||| Abstract binding trees are a generic representation of terms over
  1 | ||| a given signature
  2 | module Language.IntrinsicTyping.ABT
  3 |
  4 | import Data.SnocList.Elem
  5 |
  6 | %default total
  7 |
  8 | ------------------------------------------------------------------------
  9 | -- The Type
 10 |
 11 | parameters {0 kind : Type}
 12 |
 13 |   ||| A constructor's argument describes the kind of the variables that
 14 |   ||| will be bound in the subterm as well as the overall type of the
 15 |   ||| argument.
 16 |   |||   The argument `n` in `S n`   is described by `MkArgument [] Nat`
 17 |   |||   The argument `b` in `\x. b` is described by `MkArgument [s] t`
 18 |   public export
 19 |   record Argument where
 20 |     constructor MkArgument
 21 |     binders : List kind
 22 |     argType : kind
 23 |
 24 |   ||| A signature is a relation describing constructors.
 25 |   ||| Each constructor has a list of arguments and a return type.
 26 |   public export
 27 |   0 Signature : Type
 28 |   Signature = List Argument -> kind -> Type
 29 |
 30 |   ||| Terms and Args are mutually defined.
 31 |   ||| A term is either a variable or a constructor fully applied to its arguments.
 32 |   data Term : (sig : Signature) -> (ctx : SnocList kind) -> kind -> Type
 33 |
 34 |   ||| Terms and Args are mutually defined.
 35 |   ||| Arguments are an Arguments-indexed list of subterms.
 36 |   data Args : (sig : Signature) -> (ctx : SnocList kind) -> List Argument -> Type
 37 |
 38 |   public export
 39 |   data Term : (sig : Signature) -> (ctx : SnocList kind) -> kind -> Type where
 40 |     ||| Variables are represented using typed De Bruijn indices.
 41 |     Var : Elem s ctx -> Term sig ctx s
 42 |     ||| Constructors are provided by the signature
 43 |     Con : sig args s -> Args sig ctx args -> Term sig ctx s
 44 |
 45 |   public export
 46 |   data Args : (sig : Signature) -> (ctx : SnocList kind) -> List Argument -> Type where
 47 |     ||| Empty list
 48 |     Nil  : Args sig ctx []
 49 |     ||| An argument with binders `bds` and return type `s` is provided by a term
 50 |     ||| whose scope has been extended by `bds` and whose return type is `s`.
 51 |     (::) : {bds : List kind} ->
 52 |            Term sig (ctx <>< bds) s ->
 53 |            Args sig ctx args ->
 54 |            Args sig ctx (MkArgument bds s :: args)
 55 |
 56 | ------------------------------------------------------------------------
 57 | -- An example: STLC + Nat
 58 |
 59 | namespace Example
 60 |
 61 |   ||| The natural numbers & arrow types
 62 |   data TY = NAT | ARR TY TY
 63 |
 64 |   ||| A signature for STLC with natural numbers
 65 |   data SIG : Signature {kind = TY} where
 66 |     ||| Zero takes no argument
 67 |     ||| and returns a NAT
 68 |     Z : SIG [] NAT
 69 |     ||| Succ takes one argument (of type NAT, with no extra variable in scope),
 70 |     ||| and returns a NAT
 71 |     S : SIG [MkArgument [] NAT] NAT
 72 |     ||| Lam takes one argument (of type t, with an extra variable of type s in scope),
 73 |     ||| and returns a function from s to t
 74 |     LAM : SIG [MkArgument [s] t] (ARR s t)
 75 |     ||| App takes two arguments (of type (Arr s t) and s respectively,
 76 |     ||| with no extra variable in scope for either), and returns a t
 77 |     APP : SIG [MkArgument [] (ARR s t), MkArgument [] s] t
 78 |
 79 |   ||| Pattern synonym for Zero
 80 |   Zero : Term SIG ctx NAT
 81 |   Zero = Con Z []
 82 |
 83 |   ||| Pattern synonym for Succ
 84 |   Succ : Term SIG ctx NAT -> Term SIG ctx NAT
 85 |   Succ n = Con S [n]
 86 |
 87 |   ||| Pattern synonym for Lam
 88 |   Lam : {s : TY} -> Term SIG (ctx :< s) t -> Term SIG ctx (ARR s t)
 89 |   Lam b = Con LAM [b]
 90 |
 91 |   ||| Pattern synonym for App
 92 |   App : Term SIG ctx (ARR s t) -> Term SIG ctx s -> Term SIG ctx t
 93 |   App f t = Con APP [f, t]
 94 |
 95 | ------------------------------------------------------------------------
 96 | -- Generic renaming
 97 |
 98 | public export
 99 | lift : (forall s. Elem s ctx -> Elem s ctx') ->
100 |        (forall s. Elem s (ctx :< t) -> Elem s (ctx' :< t))
101 | lift f Here = Here
102 | lift f (There v) = There (f v)
103 |
104 | public export
105 | lifts : (bds : List kind) ->
106 |         (forall s. Elem s ctx -> Elem s ctx') ->
107 |         (forall s. Elem s (ctx <>< bds) -> Elem s (ctx' <>< bds))
108 | lifts [] f = f
109 | lifts (s :: ss) f = lifts ss (lift f)
110 |
111 | public export
112 | rename : (forall s. Elem s ctx -> Elem s ctx') ->
113 |          (forall s. Term sig ctx s -> Term sig ctx' s)
114 |
115 | public export
116 | renames : (forall s. Elem s ctx -> Elem s ctx') ->
117 |           (forall args. Args sig ctx args -> Args sig ctx' args)
118 |
119 | rename f (Var v) = Var (f v)
120 | rename f (Con c args) = Con c (renames f args)
121 |
122 | renames f [] = []
123 | renames f (arg :: args) = rename (lifts _ f) arg :: renames f args
124 |
125 | ------------------------------------------------------------------------
126 | -- Generic substitution
127 |
128 | public export
129 | extend : (forall s. Elem s ctx -> Term sig ctx' s) ->
130 |          (forall s. Elem s (ctx :< t) -> Term sig (ctx' :< t) s)
131 | extend f Here = Var Here
132 | extend f (There v) = rename There (f v)
133 |
134 | public export
135 | extends : (bds : List kind) ->
136 |           (forall s. Elem s ctx -> Term sig ctx' s) ->
137 |           (forall s. Elem s (ctx <>< bds) -> Term sig (ctx' <>< bds) s)
138 | extends [] f = f
139 | extends (s :: ss) f = extends ss (extend f)
140 |
141 | public export
142 | substitute : (forall s. Elem s ctx -> Term sig ctx' s) ->
143 |              (forall s. Term sig ctx s -> Term sig ctx' s)
144 |
145 | public export
146 | substitutes : (forall s. Elem s ctx -> Term sig ctx' s) ->
147 |               (forall args. Args sig ctx args -> Args sig ctx' args)
148 |
149 | substitute f (Var v) = f v
150 | substitute f (Con c args) = Con c (substitutes f args)
151 |
152 | substitutes f [] = []
153 | substitutes f (arg :: args) = substitute (extends _ f) arg :: substitutes f args
154 |