Implement LF as a more in-depth test case

[GoogleCodeExporter]

(Notes from Stephanie:)

I was thinking that another good idea for a test case for RepLib would be a LF
checker. LF is a pretty simple dependently typed language, and there are lots of
tests out there that we can use to stress test the system. (Aaron Stump has a
library of some on his page http://www.cs.uiowa.edu/~astump/). We wouldn't worry
about type reconstruction---we'll only work with the implicit version of LF.

Basically LF is defined by the following grammar:

data Kind = Pi (Bind (Name Tm, Annot Ty) Kind) | Star

data Ty   = Pi (Bind (Name Tm, Annot Ty) Ty)   | TyApp Ty Tm | TyConst (Name Ty)
  -- also called "Families"

data Tm   = Lam (Bind (Name Tm, Annot Ty) Tm)  | TmApp Tm Tm | TmVar (Name Tm) |
TmConst (Name Tm)
  -- also called "Objects"

LF itself is not too hard to parse. Here is a sample input file:
----------------
o : type.
trm : type.

== : trm -> trm -> o.
imp : o -> o -> o.
all : (trm -> o) -> o.
f: trm -> trm.

%infix right 3 ==.
%infix right 5 imp.

pf : o -> type.

refl : {x:trm} pf (x == x).
symm : {x:trm} {y:trm} pf (x == y) -> pf (y == x).
trans : {x:trm} {y:trm} {z:trm} pf (x == y) -> pf (y == z) -> pf (x == z).
congf : {x:trm} {y:trm} pf (x == y) -> pf ((f x) == (f y)).

mp : {p:o} {q:o} pf (p imp q) -> pf p -> pf q.
impi : {p:o} {q:o} (pf p -> pf q) -> pf (p imp q).

alli : {P:trm -> o} ({x:trm} pf (P x)) -> pf (all P).
alle : {P:trm -> o} {t:trm} pf (all P) -> pf (P t).

a : trm.
b : trm.
c : trm.

g : trm -> trm = [x:trm] f x.
-----------------------------------------------
Basically, checking LF is gradually building up a signature of type and term
constant declarations and definitions. Each entry is ended by a period. If "x :
blah." ends with "type" it is a type constant declaration. If it ends with
anything else, it is a term declaration. Terms can also have definitions
associated with them.  { } is for Pi binding and [ ] is for lambda binding. ->
is an abbreviation for a non-dependent Pi.

We can use the type checking algorithm in this paper as it uses normal
substitution. (More recent algorithms are based on hereditary substitution.)

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.3167

On Equivalence and Canonical Forms In LF,  Robert Harper,  Frank Pfenning

Original issue reported on code.google.com by byor...@gmail.com on 7 Dec 2010 at 5:07

[GoogleCodeExporter]

Original comment by byor...@gmail.com on 7 Dec 2010 at 8:08

• Changed state: Started

[GoogleCodeExporter]

Original comment by byor...@gmail.com on 3 Feb 2011 at 6:23

• Changed state: Fixed