Add more documentation

This commit is contained in:
Isaac Shoebottom 2025-03-26 16:50:55 -03:00
parent f6ada75b3c
commit cbefb85dba

View File

@ -118,18 +118,27 @@
[(timesE l r) (num2 l r (numT))]
[(leqE l r) (num2 l r (boolT))]
[(varE s) (type-lookup s env)]
; todo ensure correctness?
; https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=127
[(lamE name te body) (arrowT (interp-te te) (typecheck body (type-extend env name (interp-te te))))]
[(appE fn arg) (type-case Type (typecheck fn env) ; todo use local to reduce duplicate calls
; todo use local to reduce duplicate calls
; https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=124
[(appE fn arg) (type-case Type (typecheck fn env)
[(arrowT a b) (typecheck fn env)]
[else (error 'app "Function application must be a function")])]
[(ifE c t f) (if (equal? (typecheck c env) (boolT)) ; todo use type case/local to reduce duplicate calls`
; todo use type case/local to reduce duplicate calls
; https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=119
[(ifE c t f) (if (equal? (typecheck c env) (boolT))
(if (equal? (typecheck t env) (typecheck f env))
(typecheck t env)
(error 'if "Both if conditions must be of the same type"))
(error 'if "Condition must be a boolean expression"))]
; https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=129
[(let1E var te val body) (typecheck body (type-extend env var (interp-te te)))]
[(recE var te val body) (typecheck body (type-extend env var (interp-te te)))] ; figure out https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=132
)))
; https://www.cs.unb.ca/~bremner/teaching/cs4613/docs/plai-3.2.2.pdf#page=132
[(recE var te val body) (type-case Type (typecheck body (type-extend env var (interp-te te)))
[(arrowT a b) b]
[else (error 'rec "rec body must be a function")])])))
(tc : (S-Exp -> Type))
(define (tc s)
@ -148,3 +157,15 @@
(test/exn (tc `{lam {n : num} {if n 1 2}}) "boolean")
(test/exn (tc `{1 1}) "function")
; Tests added for complete coverage
(test (tc `false) (boolT))
(test (tc `true) (boolT))
(test (tc `{- 2 1}) (numT))
(test (tc `{* 2 2}) (numT))
(test/exn (tc `{rec {[fact : (num -> num)] {lam {n : num} {if {<= n 0} 1 {* n {fact {- n 1}}}}}} false}) "function")
(test/exn (tc `{lam {n : num} {if {<= n 0} 1 false}}) "same type")