Removed Var "abstractions"
Olly uses De Bruijn, but was attempting to use abstractions to allow changing that. Unfortunately, these were not really abstractions. So they're now gone.
This commit is contained in:
William J. Bowman
parent
fd52c764da
commit
c7aefdb032
|
|
@ -14,11 +14,11 @@ the language.
|
|||
maybe-vars
|
||||
maybe-output-coq
|
||||
maybe-output-latex
|
||||
(nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
|
||||
(nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
|
||||
#:grammar
|
||||
[(maybe-vars
|
||||
(code:line)
|
||||
(code:line #:vars (nt-metavars ...)))
|
||||
(code:line #:vars (nt-metavar ...)))
|
||||
(maybe-output-coq
|
||||
(code:line)
|
||||
(code:line #:output-coq coq-filename))
|
||||
|
|
@ -27,26 +27,51 @@ the language.
|
|||
(code:line #:output-latex latex-filename))
|
||||
(maybe-bnfdef
|
||||
(code:line)
|
||||
(code:line ::=))]]{
|
||||
(code:line ::=))
|
||||
(non-terminal-def
|
||||
nt-metavar
|
||||
(code:line terminal)
|
||||
(code:line (terminal terminal-args ...)))
|
||||
(terminal-args
|
||||
nt-metavar
|
||||
(code:line literal)
|
||||
(code:line ())
|
||||
(code:line (#:bind nt-metavar . terminal-args))
|
||||
(code:line (terminal-args terminal-args ...)))]]{
|
||||
Defines a new language by generating inductive definitions for each
|
||||
nonterminal @racket[nt-name], whose constructors are generated by
|
||||
@racket[constructors]. The constructors must either with a tag that can
|
||||
be used to name the constructor, or be another meta-variable.
|
||||
The meta-variables @racket[nt-metavars] are replaced by the corresponding
|
||||
inductive types in @racket[constructors].
|
||||
The name of each inductive datatype is generated by
|
||||
@racket[(format-id "~a-~a" name nt-name)].
|
||||
non-terminal @racket[nt-name], whose syntax is generated by
|
||||
@racket[non-terminal-def].
|
||||
Each @racket[non-terminal-def] must either be a reference to a
|
||||
previously defined non-terminal using a @racket[nt-metavar], a
|
||||
@racket[terminal] (an identifier), or a @racket[terminal] applied to
|
||||
some @racket[terminal-args].
|
||||
The @racket[terminal-args] are a limited grammar of s-expressions,
|
||||
which can reference previously defined @racket[nt-metavar]s to be
|
||||
treated as arguments, literal symbols to be treated as syntax, binding
|
||||
declarations, or a nested @racket[terminal-arg].
|
||||
|
||||
Later nonterminals can refer to prior nonterminals, but they cannot be
|
||||
mutually inductive due to limitations in Cur. When nonterminals appear
|
||||
in @racket[constructors], a constructor is defined that coerces one
|
||||
nonterminal to another.
|
||||
The inductive definitions are generated by generating a type for each
|
||||
@racket[nt-name] whose name @racket[nt-type] is generated by
|
||||
@racket[(format-id name "~a-~a" name nt-name)] and whose constructors
|
||||
are generated by each @racket[non-terminal-def].
|
||||
For @racket[terminal]s, the constructor is a base constructor whose
|
||||
name is generated by @racket[(format-id name "~a-~a" name terminal)].
|
||||
For @racket[nt-metavar]s, the constructor is a conversion constructor
|
||||
whose name is generated by @racket[(format-id name "~a->~a" nt-type
|
||||
nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
|
||||
type generated for the nonterminal to which @racket[nt-metavars] refers.
|
||||
For @racket[(terminal terminal-args ...)], the constructor is a
|
||||
function that expects term of of the types generated by
|
||||
@racket[terminal-args ...].
|
||||
|
||||
If @racket[#:vars] is given, it should be a list of meta-variables that
|
||||
representing variables in the language. These meta-variables should only
|
||||
appear in binding positions in @racket[constructors]. These variables
|
||||
are represented as De Bruijn indexes, and Olly provides some functions
|
||||
for working with De Bruijn indexes.
|
||||
representing variables in the language.
|
||||
These variables are represented as De Bruijn indices, and uses of
|
||||
variables in the syntax are treated as type @racket[Nat].
|
||||
Binding positions in the syntax, represented by @racket[#:bind
|
||||
nt-metavar], are erased in converting to De Bruijn indices, although
|
||||
this may change if the representation of variables used by
|
||||
@racket[define-language] changes.
|
||||
|
||||
If @racket[#:output-coq] is given, it should be a string representing a
|
||||
filename. The form @racket[define-language] will output Coq versions of
|
||||
|
|
@ -66,8 +91,8 @@ Example:
|
|||
#:output-latex "stlc.tex"
|
||||
(val (v) ::= true false unit)
|
||||
(type (A B) ::= boolty unitty (-> A B) (* A A))
|
||||
(term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e)
|
||||
(let (x x) = e in e)))
|
||||
(term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
|
||||
(let (#:bind x #:bind x) = e in e)))
|
||||
]
|
||||
|
||||
This example is equivalent to
|
||||
|
|
@ -85,20 +110,17 @@ This example is equivalent to
|
|||
(stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
|
||||
|
||||
(data stlc-term : Type
|
||||
(stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
|
||||
(stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term))
|
||||
(stlc-term-lambda : (forall (x : Var)
|
||||
(forall (y : stlc-type)
|
||||
(Var->-stlc-term : (forall (x : Nat) stlc-term))
|
||||
(stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term))
|
||||
(stlc-term-lambda : (forall (y : stlc-type)
|
||||
(forall (z : stlc-term)
|
||||
stlc-term))))
|
||||
stlc-term)))
|
||||
(stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
|
||||
(stlc-term-let : (forall (x : Var)
|
||||
(forall (y : Var)
|
||||
(forall (e1 : stlc-term)
|
||||
(forall (e2 : stlc-term)
|
||||
stlc-term))))))]
|
||||
(stlc-term-let : (forall (e1 : stlc-term)
|
||||
(forall (e2 : stlc-term)
|
||||
stlc-term))))]
|
||||
|
||||
@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
|
||||
@margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
|
||||
}
|
||||
|
||||
@defform[(define-relation (name args ...)
|
||||
|
|
@ -126,20 +148,20 @@ explain the syntax in detail, here is an example:
|
|||
#:output-latex "stlc.tex"
|
||||
[(g : Gamma)
|
||||
------------------------ T-Unit
|
||||
(has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
|
||||
(has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
|
||||
|
||||
[(g : Gamma)
|
||||
------------------------ T-True
|
||||
(has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
|
||||
(has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
|
||||
|
||||
[(g : Gamma)
|
||||
------------------------ T-False
|
||||
(has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
|
||||
(has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
|
||||
|
||||
[(g : Gamma) (x : Var) (t : stlc-type)
|
||||
[(g : Gamma) (x : Nat) (t : stlc-type)
|
||||
(== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
|
||||
------------------------ T-Var
|
||||
(has-type g (Var-->-stlc-term x) t)]
|
||||
(has-type g (Var->stlc-term x) t)]
|
||||
|
||||
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
|
||||
(t1 : stlc-type) (t2 : stlc-type)
|
||||
|
|
@ -151,16 +173,15 @@ explain the syntax in detail, here is an example:
|
|||
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
|
||||
(t1 : stlc-type) (t2 : stlc-type)
|
||||
(t : stlc-type)
|
||||
(x : Var) (y : Var)
|
||||
(has-type g e1 (stlc-* t1 t2))
|
||||
(has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
|
||||
(has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
|
||||
---------------------- T-Let
|
||||
(has-type g (stlc-let x y e1 e2) t)]
|
||||
(has-type g (stlc-let e1 e2) t)]
|
||||
|
||||
[(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
|
||||
(has-type (extend-gamma g x t1) e1 t2)
|
||||
[(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
|
||||
(has-type (extend-gamma g t1) e1 t2)
|
||||
---------------------- T-Fun
|
||||
(has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
|
||||
(has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
|
||||
|
||||
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
|
||||
(t1 : stlc-type) (t2 : stlc-type)
|
||||
|
|
@ -179,22 +200,11 @@ This example is equivalent to:
|
|||
(T-Unit : (forall (g : Gamma)
|
||||
(has-type
|
||||
g
|
||||
(stlc-val-->-stlc-term stlc-unit)
|
||||
(stlc-val->stlc-term stlc-unit)
|
||||
stlc-unitty)))
|
||||
....)]
|
||||
}
|
||||
|
||||
@deftogether[(@defthing[Var Type]
|
||||
@defthing[avar (forall (x : Nat) Var)])]{
|
||||
The type of a De Bruijn variable.
|
||||
}
|
||||
|
||||
@defproc[(var-equal? [v1 Var] [v2 Var])
|
||||
Bool]{
|
||||
A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
|
||||
represent the same variable.
|
||||
}
|
||||
|
||||
@todo{Need a Scribble library for defining Cur/Racket things in the same
|
||||
library in a nice way.}
|
||||
|
||||
|
|
|
|||
|
|
@ -10,9 +10,6 @@
|
|||
(provide
|
||||
define-relation
|
||||
define-language
|
||||
Var
|
||||
avar
|
||||
var-equal?
|
||||
generate-coq
|
||||
|
||||
;; private; exported for testing only
|
||||
|
|
@ -252,7 +249,7 @@
|
|||
[(attribute x) =>
|
||||
(lambda (xls)
|
||||
(for ([x xls])
|
||||
(dict-set! (mv-map) (syntax-e x) #'Var)))])
|
||||
(dict-set! (mv-map) (syntax-e x) #'Nat)))])
|
||||
(syntax-parse #'non-terminal-defs
|
||||
[((~var defs non-terminal-def) ...)
|
||||
(let ([output #`(begin defs.def ...)])
|
||||
|
|
@ -266,15 +263,6 @@
|
|||
#'())
|
||||
#,output))])))
|
||||
|
||||
(data Var : Type (avar : (-> Nat Var)))
|
||||
|
||||
(define (var-equal? (v1 : Var) (v2 : Var))
|
||||
(match v1
|
||||
[(avar (n1 : Nat))
|
||||
(match v2
|
||||
[(avar (n2 : Nat))
|
||||
(nat-equal? n1 n2)])]))
|
||||
|
||||
;; See stlc.rkt for examples
|
||||
|
||||
;; Generate Coq from Cur:
|
||||
|
|
|
|||
|
|
@ -21,13 +21,6 @@
|
|||
(format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
|
||||
(output-latex-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
|
||||
|
||||
(check-equal?
|
||||
(var-equal? (avar z) (avar z))
|
||||
true)
|
||||
(check-equal?
|
||||
(var-equal? (avar z) (avar (s z)))
|
||||
false)
|
||||
|
||||
(begin-for-syntax
|
||||
(check-equal?
|
||||
(parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
|
||||
|
|
|
|||
|
|
@ -19,10 +19,7 @@
|
|||
(term (e) ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
|
||||
(let (#:bind x #:bind x) = e in e)))
|
||||
|
||||
(define (lookup-env (g : (List stlc-type)))
|
||||
;; TODO: Can't use match due to limitation in type inference
|
||||
(elim Var Type (lambda (x : Var) (Maybe stlc-type))
|
||||
(list-ref stlc-type g)))
|
||||
(define lookup-env (list-ref stlc-type))
|
||||
|
||||
(define (extend-env (g : (List stlc-type)) (t : stlc-type))
|
||||
(cons stlc-type t g))
|
||||
|
|
@ -42,10 +39,10 @@
|
|||
------------------------ T-False
|
||||
(has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
|
||||
|
||||
[(g : (List stlc-type)) (x : Var) (t : stlc-type)
|
||||
[(g : (List stlc-type)) (x : Nat) (t : stlc-type)
|
||||
(== (Maybe stlc-type) (lookup-env g x) (some stlc-type t))
|
||||
------------------------ T-Var
|
||||
(has-type g (Var->stlc-term x) t)]
|
||||
(has-type g (Nat->stlc-term x) t)]
|
||||
|
||||
[(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
|
||||
(t1 : stlc-type) (t2 : stlc-type)
|
||||
|
|
@ -113,19 +110,19 @@
|
|||
#'stlc-unitty]
|
||||
[(dict-ref d (syntax->datum #'e) #f) =>
|
||||
(lambda (x)
|
||||
#`(Var->stlc-term (avar #,x)))]
|
||||
#`(Nat->stlc-term #,x))]
|
||||
[else #'e])])))
|
||||
|
||||
(check-equal?
|
||||
(begin-stlc (lambda (x : 1) x))
|
||||
(stlc-lambda stlc-unitty (Var->stlc-term (avar z))))
|
||||
(stlc-lambda stlc-unitty (Nat->stlc-term z)))
|
||||
(check-equal?
|
||||
(begin-stlc ((lambda (x : 1) x) ()))
|
||||
(stlc-app (stlc-lambda stlc-unitty (Var->stlc-term (avar z)))
|
||||
(stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z))
|
||||
(stlc-val->stlc-term stlc-unit)))
|
||||
(check-equal?
|
||||
(begin-stlc (lambda (x : 1) (lambda (y : 1) x)))
|
||||
(stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Var->stlc-term (avar (s z))))))
|
||||
(stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Nat->stlc-term (s z)))))
|
||||
(check-equal?
|
||||
(begin-stlc '(() ()))
|
||||
(stlc-cons (stlc-val->stlc-term stlc-unit)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user