Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

fixes from ar.

  • Loading branch information...
commit 372c11b933861641ccd7f65bf839a8acab8723ce 1 parent 48466ff
@samth authored
Showing with 7 additions and 6 deletions.
  1. +7 −6 constraints.rkt
View
13 constraints.rkt
@@ -37,28 +37,29 @@
(define-metafunction js
norm-C : Cs -> Cs
[(norm-C (C_1 ... ⊤ C_2 ...)) (norm-C (C_1 ... C_2 ...))]
- [(norm-C (C_1 ... C_2 ...)) bot]
+ [(norm-C (C_1 ... bot C_2 ...)) bot]
[(norm-C Cs) Cs])
;; typing rules
(define-metafunction js
+ fresh-ρ : -> ρ
[(fresh-ρ) ,(gensym )])
(define-metafunction js
- fresh-var : any ... -> α
- [(fresh-var any_1 ...) ,(gensym ) #;(variable-not-in (term (any_1 ...)) )])
+ fresh-var : -> α
+ [(fresh-var) ,(gensym )])
(define-judgment-form js
#:mode (typ/e I I O O)
#:contract (typ/e Γ e σ Cs)
- [(where α (fresh-var Γ x))
+ [(where α (fresh-var))
---
(typ/e Γ x α ((:= α (Γ x))))]
[(typ/e Γ e σ (C ...))
- (where α (fresh-var Γ e σ (C ...)))
+ (where α (fresh-var))
---
(typ/e Γ (dot e x) α (norm-C (C ... (:= α (dot σ x)))))]
@@ -79,7 +80,7 @@
#:mode (typ/m I I O O)
#:contract (typ/m Γ m σ Cs)
- [(where α (fresh-var Γ x))
+ [(where α (fresh-var))
---
(typ/m Γ x α ((:= α (Γ x))))]
Please sign in to comment.
Something went wrong with that request. Please try again.