added code

src/README

@@ -0,0 +1,7 @@
+This comprises the working draft of LFinLF development, including soundness
+and completeness of translation to canonical forms, family-level lambdas,
+and constants.
+
+All code by Chris Martens
+
+Last updated 3/29/2011

src/canonical-explicit.elf

@@ -0,0 +1,141 @@
+%%% ordered variables %%%
+
+isvar : atm -> nat -> type.
+%%mode isvar *X1 *X2.
+
+- : (isvar _ _ -> isvar _ _) -> type.
+
+
+precedes : atm -> atm -> type.
+
+precedes/i : precedes X Y
+              <- isvar X I
+              <- isvar Y J
+              <- lt I J.
+
+
+%%% contexts %%%
+
+ctx : type.  %name ctx G.
+
+nil : ctx.
+cons : ctx -> atm -> tp -> ctx.
+
+
+bounded : ctx -> atm -> type.
+
+bounded/nil  : bounded nil X
+                <- isvar X _.
+bounded/cons : bounded (cons G Y _) X
+                <- precedes Y X
+                <- bounded G Y.
+
+
+ordered : ctx -> type.
+
+ordered/nil  : ordered nil.
+ordered/cons : ordered (cons G X _)
+                <- bounded G X.
+
+
+lookup : ctx -> atm -> tp -> type.
+
+lookup/hit  : lookup (cons G X A) X A.
+
+lookup/miss : lookup (cons G Y _) X A
+               <- lookup G X A.
+
+
+csub : (atm -> ctx) -> tm -> ctx -> type.
+
+csub/nil  : csub ([_] nil) _ nil.
+csub/base : csub ([x] cons G x A) M G.
+csub/cons : csub ([x] cons (G x) Y (A x)) M (cons G' Y A')
+             <- csub ([x] G x) M G'
+             <- tpsub ([x] A x) M A'.
+
+
+append : ctx -> ctx -> ctx -> type.
+
+append/nil : append G nil G.
+append/cons : append G1 (cons G2 X A) (cons G X A)
+               <- append G1 G2 G.
+
+
+%%% typing with explicit contexts %%%
+
+ofe     : ctx -> tm -> tp -> type.
+at-ofe  : ctx -> atm -> tp -> type.
+kofe    : ctx -> tp -> kind -> type.
+at-kofe : ctx -> atp -> kind -> type.
+wfkinde : ctx -> kind -> type.
+
+% objects
+
+at-ofe/closed : at-ofe G R A
+                <- at-of R A.
+
+at-ofe/const : at-ofe G (const C) A
+                <- cof C A
+                <- kofe G A ktype
+%                <- tclosed A
+                .
+
+at-ofe/var   : at-ofe G X A
+                <- lookup G X A
+                <- kofe G A ktype.
+
+at-ofe/app   : at-ofe G (app R M) B'
+                <- at-ofe G R (pi A ([x] B x))
+                <- ofe G M A
+                <- tpsub ([x] B x) M B'.
+
+ofe/at       : ofe G (at R) (base P)
+                <- at-ofe G R (base P).
+
+ofe/lam      : ofe G (lam [x] M x) (pi A [x] B x)
+                <- ({x} ofe (cons G x A) (M x) (B x))
+                <- kofe G A ktype.
+
+% families
+
+at-kofe/closed : at-kofe G P K
+                  <- at-kof P K.
+
+at-kofe/const : at-kofe G (aconst A) K
+                 <- ckof A K
+                 <- wfkinde G K
+                    .
+%                 <- kclosed K.
+
+at-kofe/app   : at-kofe G (aapp P M) K'
+                 <- at-kofe G P (kpi B ([x] K x))
+                 <- ofe G M B
+                 <- ksub ([x] K x) M K'.
+
+kofe/pi       : kofe G (pi A ([x] B x)) ktype
+                 <- kofe G A ktype
+                 <- ({x} kofe (cons G x A) (B x) ktype).
+
+kofe/base     : kofe G (base P) ktype
+                 <- at-kofe G P ktype.
+
+kofe/lam      : kofe G (alam ([x] B x)) (kpi A ([x] K x))
+                 <- kofe G A ktype
+                 <- ({x} kofe (cons G x A) (B x) (K x)).
+
+
+% kinds
+
+wfkinde/tp : wfkinde G ktype.
+
+wfkinde/pi : wfkinde G (kpi A ([x] K x))
+              <- kofe G A ktype
+              <- ({x} wfkinde (cons G x A) (K x)).
+
+
+%%% worlds %%%
+
+
+%block ovar  : some {n:nat} block {x:atm} {d:isvar x n}.
+

src/canonical-simple.elf

@@ -0,0 +1,173 @@
+
+%%% simple types %%%
+
+stp : type.  %name stp T.
+
+o       : stp.
+arrow   : stp -> stp -> stp.
+
+
+simp   : tp -> stp -> type.
+
+simp/pi : simp (pi A [x] B x) (arrow S T)
+           <- simp A S
+           <- ({x} simp (B x) T).
+
+simp/base : simp (base _) o.
+
+simp/lam  : simp (alam ([x] A x)) T
+             <- ({x} simp (A x) T).
+
+
+%%% simple kinds %%%
+
+skind : type.  %name skind H.
+
+sktype  : skind.
+karrow  : stp -> skind -> skind.
+
+
+ksimp : kind -> skind -> type.
+
+ksimp/pi : ksimp (kpi A [x] K x) (karrow S H)
+            <- simp A S
+            <- ({x} ksimp (K x) H).
+
+ksimp/type : ksimp ktype sktype.
+
+
+%%% leq relation on simple types %%%
+
+stp-leq : stp -> stp -> type.
+
+stp-leq/eq : stp-leq T T.
+stp-leq/arr1 : stp-leq S (arrow T1 T2)
+                <- stp-leq S T1.
+stp-leq/arr2 : stp-leq S (arrow T1 T2)
+                <- stp-leq S T2.
+
+
+%%% simple contexts %%%
+
+sctx : type.  %name sctx G.
+
+snil : sctx.
+scons : sctx -> atm -> stp -> sctx.
+
+
+sbounded : sctx -> atm -> type.
+
+sbounded/nil  : sbounded snil X
+                 <- isvar X _.
+sbounded/cons : sbounded (scons G Y _) X
+                 <- precedes Y X
+                 <- sbounded G Y.
+
+
+sordered : sctx -> type.
+
+sordered/nil  : sordered snil.
+sordered/cons : sordered (scons G X _)
+                 <- sbounded G X.
+
+
+slookup : sctx -> atm -> stp -> type.
+
+slookup/hit  : slookup (scons G X T) X T.
+slookup/miss : slookup (scons G Y _) X T
+                <- slookup G X T.
+
+
+drop : (atm -> sctx) -> sctx -> type.
+
+drop/closed : drop ([_] G) G.
+drop/base   : drop ([x] scons (G x) x A) G'
+               <- drop ([x] G x) G'.
+drop/cons   : drop ([x] scons (G x) Y T) (scons G' Y T)
+               <- drop ([x] G x) G'.
+
+sappend : sctx -> sctx -> sctx -> type.
+
+sappend/nil  : sappend G snil G.
+sappend/cons : sappend G1 (scons G2 X A) (scons G X A)
+                <- sappend G1 G2 G.
+
+
+%%% simplifying contexts %%%
+
+simpctx : ctx -> sctx -> type.
+
+simpctx/nil  : simpctx nil snil.
+simpctx/cons : simpctx (cons G X A) (scons G' X T)
+                <- simpctx G G'
+                <- simp A T.
+
+
+%%% simple typing with explicit contexts %%%
+
+wfkindes : sctx -> kind -> type.
+at-kofes : sctx -> atp -> skind -> type.
+kofes    : sctx -> tp -> skind -> type.
+at-ofes  : sctx -> atm -> stp -> type.
+ofes     : sctx -> tm -> stp -> type.
+
+at-ofes/closed : at-ofes G R T
+                <- at-of R A
+                <- simp A T.
+
+at-ofes/const  : at-ofes G (const C) T
+                  <- cof C A
+                  <- kofes G A sktype
+%                  <- tclosed A
+                  <- simp A T.
+
+at-ofes/var    : at-ofes G X T
+                <- slookup G X T.
+
+at-ofes/app    : at-ofes G (app R M) T
+                <- at-ofes G R (arrow S T)
+                <- ofes G M S.
+
+
+ofes/at  : ofes G (at R) o
+            <- at-ofes G R o.
+
+ofes/lam : ofes G (lam [x] M x) (arrow S T)
+            <- ({x} ofes (scons G x S) (M x) T).
+
+
+%% kofes/at-kofes.
+
+at-kofes/closed : at-kofes G P H
+                   <- at-kof P K
+                   <- ksimp K H.
+
+at-kofes/const  : at-kofes G (aconst A) H
+                   <- ckof A K
+                   <- wfkindes G K
+%                   <- kclosed K
+                   <- ksimp K H.
+
+at-kofes/app    : at-kofes G (aapp P M) H
+                   <- at-kofes G P (karrow S H)
+                   <- ofes G M S.
+
+kofes/base  : kofes G (base P) sktype
+               <- at-kofes G P sktype.
+
+kofes/pi    : kofes G (pi A1 [x] A2 x) sktype
+               <- kofes G A1 sktype
+               <- simp A1 T1
+               <- ({x:atm} kofes (scons G x T1) (A2 x) sktype).
+
+kofes/lam   : kofes G (alam ([x] B x)) (karrow T H)
+               <- ({x:atm} kofes (scons G x T) (B x) H).
+
+%% wfkindes
+
+wfkindes/type : wfkindes G ktype.
+
+wfkindes/pi   : wfkindes G (kpi A ([x] K x))
+                 <- kofes G A sktype
+                 <- simp A T
+                 <- ({x} wfkindes (scons G x T) (K x)).