diff options
Diffstat (limited to 'stlc-ext.rkt')
| -rw-r--r-- | stlc-ext.rkt | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 04c84bd..1ab83ba 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -88,6 +88,12 @@ [(`(type ,t1 ,t2 ,in) with) (check- in with (dict-set Γ t1 t2))] + [(`(inc ,e) 'Nat) + (check- e 'Nat Γ)] + [(`(if ,c ,e1 ,e2) with) + (and (check- c 'Bool Γ) + (check- e1 with Γ) (check e2 with Γ))] + [(`(pair ,e1 ,e2) `(× ,t1 ,t2)) (and (check- e1 t1 Γ) (check- e2 t2 Γ))] [(`(car ,e) with) @@ -151,6 +157,17 @@ [`(type ,t1 ,t2 ,in) (infer in (dict-set Γ t1 t2))] + [`(inc ,e) + (if (check- e 'Nat Γ) 'Nat + (err (format "calling inc on incorrect type ~a" (infer- e Γ))))] + [`(if ,c ,e1 ,e2) + (if (check- c 'Bool Γ) + (let ([t (infer- e1 Γ)]) + (if (check- e2 t Γ) t + (err (format "condition has branches of differing types ~a and ~a" + t (infer- e2 Γ))))) + (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))] + [`(pair ,e1 ,e2) `(× ,(infer- e1 Γ) ,(infer- e2 Γ))] [`(car ,e) |