[go: nahoru, domu]
Skip to content

Instantly share code, notes, and snippets.

@VictorTaelin

VictorTaelin/tt.hs

Created August 9, 2024 22:46
Show Gist options
  • Save VictorTaelin/e25a13f91ed4117629194f1242ee924a to your computer and use it in GitHub Desktop.
Save VictorTaelin/e25a13f91ed4117629194f1242ee924a to your computer and use it in GitHub Desktop.
Download ZIP
yet another...
Raw
tt.hs
import Control.Monad (forM_)
import Data.Char (chr, ord)
import Debug.Trace
import Prelude hiding (LT, GT, EQ)
import System.Environment (getArgs)
import System.Exit (exitFailure)
import Text.Parsec ((<|>))
import qualified Data.Map.Strict as M
import qualified Text.Parsec as P
-- TT Term
-- -------
-- Term ::=
-- | All: ∀(x: A) B
-- | Lam: λx f
-- | App: (f x)
-- | Slf: $(x: A) B
-- | Ann: {x: T}
-- | Ins: ~x
-- | Sum: (| A B)
-- | Inl: -x
-- | Inr: +x
-- | Mat: λ{ -: ifl | +: ifr }
-- | Mul: (& A B)
-- | Tup: #(a,b)
-- | Get: λ{ (,): ... }
-- | Uni: ⊤
-- | One: ()
-- | Tap: λ{ (): ... }
-- | Emp: ⊥
-- | Efq: λ{}
-- | Let: let x = A; B
-- | Use: use x = A; B
-- | Set: *
-- | Ref: x
-- | Var: x
data Term
= All String Term (Term -> Term)
| Lam String (Term -> Term)
| App Term Term
| Ann Bool Term Term
| Slf String Term (Term -> Term)
| Ins Term
| Sum Term Term
| Inl Term
| Inr Term
| Mat String String Term Term
| Mul Term Term
| Tup Term Term
| Get String String Term
| Uni
| One
| Tap Term
| Emp
| Efq
| Let String Term (Term -> Term)
| Use String Term (Term -> Term)
| Set
| Ref String
| Var String Int
| Hol String [Term]
-- Book of Definitions
type Book = M.Map String Term
-- Type-Checker Error
data Error = Error Int Term Term Term Int
-- Type-Checker Result
type Result a = Either Error a
-- Binding
-- -------
bind :: Term -> Term
bind term = go term [] where
go (All nam inp bod) ctx = All nam (go inp ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go (Lam nam bod) ctx = Lam nam (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go (App fun arg) ctx = App (go fun ctx) (go arg ctx)
go (Ann chk val typ) ctx = Ann chk (go val ctx) (go typ ctx)
go (Slf nam typ bod) ctx = Slf nam (go typ ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go (Ins val) ctx = Ins (go val ctx)
go (Sum a b) ctx = Sum (go a ctx) (go b ctx)
go (Inl x) ctx = Inl (go x ctx)
go (Inr x) ctx = Inr (go x ctx)
go (Mat l r ifl ifr) ctx = Mat l r (go ifl ctx) (go ifr ctx)
go (Mul a b) ctx = Mul (go a ctx) (go b ctx)
go (Tup a b) ctx = Tup (go a ctx) (go b ctx)
go (Get a b bod) ctx = Get a b (go bod ctx)
go Uni ctx = Uni
go One ctx = One
go (Tap bod) ctx = Tap (go bod ctx)
go Emp ctx = Emp
go Efq ctx = Efq
go (Let nam val bod) ctx = Let nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go (Use nam val bod) ctx = Use nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
go Set ctx = Set
go (Ref nam) ctx = case lookup nam ctx of { Just x -> x; Nothing -> Ref nam }
go (Var nam idx) ctx = Var nam idx
go (Hol nam _) ctx = Hol nam (map snd ctx)
-- Evaluation
-- ----------
-- Evaluation levels:
-- - 0: reduces refs: never
-- - 1: reduces refs: redexes
-- - 2: reduces refs: always
reduce :: Book -> Int -> Term -> Term
reduce book lv (App fun arg) = reduceApp book lv (reduce book lv fun) arg
reduce book lv (Ann chk val typ) = reduce book lv val
reduce book lv (Ins val) = reduce book lv val
reduce book lv (Let nam val bod) = reduce book lv (bod val)
reduce book lv (Use nam val bod) = reduce book lv (bod val)
reduce book lv (Ref nam) = reduceRef book lv nam
reduce book lv (Hol nam ctx) = Hol nam ctx
reduce book lv val = val
reduceApp :: Book -> Int -> Term -> Term -> Term
reduceApp book 2 (Ref nam) arg = reduceApp book 2 (reduceRef book 2 nam) arg
reduceApp book 1 (Ref nam) arg = reduceApp book 1 (reduceRef book 1 nam) arg
reduceApp book lv (Lam nam bod) arg = reduce book lv (bod (reduce book 0 arg))
reduceApp book lv (Get a b bod) (Tup x y) = reduce book lv (App (App bod (reduce book 0 x)) (reduce book 0 y))
reduceApp book lv (Mat l r ifl ifr) (Inl x) = reduce book lv (App ifl (reduce book 0 x))
reduceApp book lv (Mat l r ifl ifr) (Inr x) = reduce book lv (App ifr (reduce book 0 x))
reduceApp book lv fun arg = App fun arg
reduceRef :: Book -> Int -> String -> Term
reduceRef book 2 nam = case M.lookup nam book of
Just val -> reduce book 2 val
Nothing -> error $ "Undefined: " ++ nam
reduceRef book 1 nam = Ref nam
reduceRef book lv nam = Ref nam
-- Normalization
-- -------------
normal :: Book -> Int -> Term -> Int -> Term
normal book lv term dep = go book lv (reduce book lv term) dep where
go book lv (All nam inp bod) dep = All nam (normal book lv inp dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
go book lv (Lam nam bod) dep = Lam nam (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
go book lv (App fun arg) dep = App (normal book lv fun dep) (normal book lv arg dep)
go book lv (Slf nam typ bod) dep = Slf nam typ (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
go book lv (Ins val) dep = Ins (normal book lv val dep)
go book lv (Sum a b) dep = Sum (normal book lv a dep) (normal book lv b dep)
go book lv (Inl x) dep = Inl (normal book lv x dep)
go book lv (Inr x) dep = Inr (normal book lv x dep)
go book lv (Mat l r ifl ifr) dep = Mat l r (normal book lv ifl dep) (normal book lv ifr dep)
go book lv (Mul a b) dep = Mul (normal book lv a dep) (normal book lv b dep)
go book lv (Tup a b) dep = Tup (normal book lv a dep) (normal book lv b dep)
go book lv (Get a b bod) dep = Get a b (normal book lv bod dep)
go book lv Uni dep = Uni
go book lv One dep = One
go book lv (Tap bod) dep = Tap (normal book lv bod dep)
go book lv Emp dep = Emp
go book lv Efq dep = Efq
go book lv (Let nam val bod) dep = Let nam (normal book lv val dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
go book lv (Use nam val bod) dep = Use nam (normal book lv val dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
go book lv Set dep = Set
go book lv (Ref nam) dep = Ref nam
go book lv (Var nam idx) dep = Var nam idx
go book lv (Ann chk val typ) dep = Ann chk (normal book lv val dep) (normal book lv typ dep)
go book lv (Hol nam ctx) dep = Hol nam ctx
-- Equality
-- --------
equal :: Book -> Term -> Term -> Int -> Result Bool
equal book a b dep = do
let a' = reduce book 2 a
let b' = reduce book 2 b
same <- identical book a' b' dep
if same
then return True
else similar book a' b' dep
similar :: Book -> Term -> Term -> Int -> Result Bool
similar book a b dep = go a b dep where
go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
eInp <- equal book aInp bInp dep
eBod <- equal book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
return (eInp && eBod)
go (Lam aNam aBod) (Lam bNam bBod) dep =
equal book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
go (App aFun aArg) (App bFun bArg) dep = do
eFun <- similar book aFun bFun dep
eArg <- equal book aArg bArg dep
return (eFun && eArg)
go (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
similar book (reduce book 0 aTyp) (reduce book 0 bTyp) dep
go (Sum aA aB) (Sum bA bB) dep = do
eA <- equal book aA bA dep
eB <- equal book aB bB dep
return (eA && eB)
go (Mul aA aB) (Mul bA bB) dep = do
eA <- equal book aA bA dep
eB <- equal book aB bB dep
return (eA && eB)
go (Hol _ _) _ dep = return True
go _ (Hol _ _) dep = return True
go a b dep = identical book a b dep
identical :: Book -> Term -> Term -> Int -> Result Bool
identical book a b dep = go a b dep where
go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
iInp <- identical book aInp bInp dep
iBod <- identical book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
return (iInp && iBod)
go (Lam aNam aBod) (Lam bNam bBod) dep =
identical book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
go (App aFun aArg) (App bFun bArg) dep = do
iFun <- identical book aFun bFun dep
iArg <- identical book aArg bArg dep
return (iFun && iArg)
go (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
identical book aTyp bTyp dep
go (Ins aVal) b dep =
identical book aVal b dep
go a (Ins bVal) dep =
identical book a bVal dep
go (Let aNam aVal aBod) b dep =
identical book (aBod aVal) b dep
go a (Let bNam bVal bBod) dep =
identical book a (bBod bVal) dep
go (Use aNam aVal aBod) b dep =
identical book (aBod aVal) b dep
go a (Use bNam bVal bBod) dep =
identical book a (bBod bVal) dep
go (Sum aA aB) (Sum bA bB) dep = do
iA <- identical book aA bA dep
iB <- identical book aB bB dep
return (iA && iB)
go (Inl aX) (Inl bX) dep =
identical book aX bX dep
go (Inr aX) (Inr bX) dep =
identical book aX bX dep
go (Mat aL aR aIfL aIfR) (Mat bL bR bIfL bIfR) dep = do
iIfL <- identical book aIfL bIfL dep
iIfR <- identical book aIfR bIfR dep
return (iIfL && iIfR)
go (Mul aA aB) (Mul bA bB) dep = do
iA <- identical book aA bA dep
iB <- identical book aB bB dep
return (iA && iB)
go (Tup aA aB) (Tup bA bB) dep = do
iA <- identical book aA bA dep
iB <- identical book aB bB dep
return (iA && iB)
go (Get aA aB aBod) (Get bA bB bBod) dep =
identical book aBod bBod dep
go Uni Uni dep =
return True
go One One dep =
return True
go (Tap aBod) (Tap bBod) dep =
identical book aBod bBod dep
go Emp Emp dep =
return True
go Efq Efq dep =
return True
go Set Set dep =
return True
go (Ann chk aVal aTyp) b dep =
identical book aVal b dep
go a (Ann chk bVal bTyp) dep =
identical book a bVal dep
go (Ref aNam) (Ref bNam) dep =
return (aNam == bNam)
go (Var aNam aIdx) (Var bNam bIdx) dep =
return (aIdx == bIdx)
go (Hol _ _) _ dep = return True
go _ (Hol _ _) dep = return True
go a b dep =
return False
-- Type-Checking
-- -------------
infer :: Book -> Term -> Int -> Result Term
infer book term dep = {-trace ("infer " ++ termStr term dep) $-} go term dep where
go (All nam inp bod) dep = do
check book inp Set dep
check book (bod (Ann False (Var nam dep) inp)) Set (dep + 1)
return Set
go (App fun arg) dep = do
ftyp <- infer book fun dep
case reduce book 2 ftyp of
(All ftyp_nam ftyp_inp ftyp_bod) -> do
check book arg ftyp_inp dep
return $ ftyp_bod arg
otherwise ->
Left (Error 0 (Ref "function") ftyp (App fun arg) dep)
go (Ann chk val typ) dep = do
if chk then
check book val typ dep
else
return ()
return typ
go (Slf nam typ bod) dep = do
check book (bod (Ann False (Var nam dep) typ)) Set (dep + 1)
return Set
go (Ins val) dep = do
vtyp <- infer book val dep
case reduce book 2 vtyp of
(Slf vtyp_nam vtyp_typ vtyp_bod) ->
return $ vtyp_bod (Ins val)
otherwise ->
Left (Error 0 (Ref "self-type") vtyp (Ins val) dep)
go (Sum a b) dep = do
check book a Set dep
check book b Set dep
return Set
go (Mul a b) dep = do
check book a Set dep
check book b Set dep
return Set
go Uni dep = return Set
go One dep = return Uni
go Emp dep = return Set
go Set dep = return Set
go (Let nam val bod) dep = do
typ <- infer book val dep
infer book (bod (Ann False (Var nam dep) typ)) dep
go (Use nam val bod) dep =
infer book (bod val) dep
go (Inl x) dep = do
xtyp <- infer book x dep
return $ Sum xtyp (Hol "right_type" [])
go (Inr x) dep = do
xtyp <- infer book x dep
return $ Sum (Hol "left_type" []) xtyp
go (Tup a b) dep = do
atyp <- infer book a dep
btyp <- infer book b dep
return $ Mul atyp btyp
go t@(Mat _ _ _ _) dep =
Left (Error 0 (Ref "type_annotation") (Ref "untyped_match") t dep)
go t@(Get _ _ _) dep =
Left (Error 0 (Ref "type_annotation") (Ref "untyped_get") t dep)
go t@(Tap _) dep =
Left (Error 0 (Ref "type_annotation") (Ref "untyped_tap") t dep)
go t@(Lam nam bod) dep =
Left (Error 0 (Ref "type_annotation") (Ref "untyped_lambda") t dep)
go (Ref nam) dep =
case M.lookup nam book of
Just val -> infer book val dep
Nothing -> Left (Error 0 (Ref "undefined") (Ref "unknown_type") (Ref nam) dep)
go (Var nam idx) dep =
Left (Error 0 (Ref "type_annotation") (Ref "untyped_variable") (Var nam idx) dep)
go (Hol nam ctx) dep = do
trace (holStr nam (Ref "_") ctx) $ return Set
check :: Book -> Term -> Term -> Int -> Result ()
check book val typ dep = {-trace ("check " ++ termStr val dep ++ " :: " ++ termStr typ dep) $-} go val typ dep where
go (Lam nam bod) typx dep =
case reduce book 2 typx of
(All typ_nam typ_inp typ_bod) -> do
let ann = Ann False (Var nam dep) typ_inp
let term = bod ann
let typx = typ_bod ann
check book term typx (dep + 1)
otherwise -> do
_ <- infer book (Lam nam bod) dep
return ()
go (Tap bod) typx dep =
case reduce book 2 typx of
(All typ_nam typ_inp typ_bod) -> do
case reduce book 2 typ_inp of
Uni -> do
check book bod (typ_bod One) dep
otherwise -> infer book (Tap bod) dep >> return ()
otherwise -> infer book (Tap bod) dep >> return ()
go (Mat l r ifl ifr) typx dep =
case reduce book 2 typx of
(All typ_nam typ_inp typ_bod) -> do
case reduce book 2 typ_inp of
(Sum typ_a typ_b) -> do
check book ifl (All l typ_a $ \x -> (typ_bod (Inl x))) dep
check book ifr (All r typ_b $ \x -> (typ_bod (Inr x))) dep
otherwise -> infer book (Mat l r ifl ifr) dep >> return ()
otherwise -> infer book (Mat l r ifl ifr) dep >> return ()
go (Get a b bod) typx dep =
case reduce book 2 typx of
(All typ_nam typ_inp typ_bod) -> do
case reduce book 2 typ_inp of
(Mul typ_a typ_b) -> do
check book bod (All a typ_a $ \x -> All b typ_b $ \y -> typ_bod (Tup x y)) dep
otherwise -> infer book (Get a b bod) dep >> return ()
otherwise -> infer book (Get a b bod) dep >> return ()
go (Ins val) typx dep =
case reduce book 2 typx of
Slf typ_nam typ_typ typ_bod ->
check book val (typ_bod (Ins val)) dep
_ -> do
_ <- infer book (Ins val) dep
return ()
go (Let nam val bod) typx dep = do
typ <- infer book val dep
check book (bod (Ann False (Var nam dep) typ)) typx dep
go (Use nam val bod) typx dep =
check book (bod val) typx dep
go (Ann chk val typ) typx dep = do
checkCompare book val typ typx dep
if chk
then check book val typ dep
else return ()
go (Inl x) typx dep =
case reduce book 2 typx of
Sum a b -> check book x a dep
_ -> infer book (Inl x) dep >> return ()
go (Inr x) typx dep =
case reduce book 2 typx of
Sum a b -> check book x b dep
_ -> infer book (Inr x) dep >> return ()
go (Tup x y) typx dep =
case reduce book 2 typx of
Mul a b -> do
check book x a dep
check book y b dep
_ -> infer book (Tup x y) dep >> return ()
go One typx dep =
case reduce book 2 typx of
Uni -> return ()
_ -> Left (Error 0 Uni typx One dep)
go (Hol nam ctx) typx dep = do
trace (holStr nam typx ctx) $ return ()
go term typx dep = do
infer <- infer book term dep
checkCompare book term typx infer dep
checkCompare :: Book -> Term -> Term -> Term -> Int -> Result ()
checkCompare book term expected detected dep = do
equal <- equal book expected detected dep
if equal then
return ()
else
Left (Error 0 expected detected term dep)
checkDef :: Book -> Term -> Result ()
checkDef book (Ref nam) =
case M.lookup nam book of
Just val -> case val of
Ann chk val typ -> check book val typ 0
Ref nm2 -> checkDef book (Ref nm2)
_ -> infer book val 0 >> return ()
Nothing -> Left (Error 0 (Ref "undefined") (Ref "unknown_type") (Ref nam) 0)
checkDef _ other = error "invalid top-level definition"
holStr :: String -> Term -> [Term] -> String
holStr name ty ctx = unlines $ ("GOAL: ?" ++ name ++ " : " ++ termStr ty 0) : map var (reverse ctx) where
var (Ann _ tm ty) = "- " ++ termStr tm 0 ++ " : " ++ termStr ty 0
var tm = "- " ++ termStr tm 0
-- Stringification
-- ---------------
termStr :: Term -> Int -> String
termStr (All nam inp bod) dep =
let nam' = nam
inp' = termStr inp dep
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["∀(" , nam' , ": " , inp' , ") " , bod']
termStr (Lam nam bod) dep =
let nam' = nam
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["λ" , nam' , " " , bod']
termStr (App fun arg) dep =
let fun' = termStr fun dep
arg' = termStr arg dep
in concat ["(" , fun' , " " , arg' , ")"]
termStr (Ann chk val typ) dep =
termStr val dep
-- let val' = termStr val dep
-- typ' = termStr typ dep
-- in concat ["{" , val' , ": " , typ' , "}"]
termStr (Slf nam typ bod) dep =
let nam' = nam
typ' = termStr typ dep
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["$(" , nam' , ": " , typ' , ") " , bod']
termStr (Ins val) dep =
let val' = termStr val dep
in concat ["~" , val']
termStr (Sum a b) dep =
let a' = termStr a dep
b' = termStr b dep
in concat ["(| " , a' , " " , b' , ")"]
termStr (Inl x) dep =
let x' = termStr x dep
in concat ["-" , x']
termStr (Inr x) dep =
let x' = termStr x dep
in concat ["+" , x']
termStr (Mat l r ifl ifr) dep =
let l' = l
r' = r
ifl' = termStr ifl dep
ifr' = termStr ifr dep
in concat ["λ{ -: " , ifl' , " | +: " , ifr' , " }"]
termStr (Mul a b) dep =
let a' = termStr a dep
b' = termStr b dep
in concat ["(& " , a' , " " , b' , ")"]
termStr (Tup a b) dep =
let a' = termStr a dep
b' = termStr b dep
in concat ["#(" , a' , "," , b' , ")"]
termStr (Get a b bod) dep =
let a' = a
b' = b
bod' = termStr bod dep
in concat ["λ{ (,): " , bod' , " }"]
termStr Uni dep = "⊤"
termStr One dep = "()"
termStr (Tap bod) dep =
let bod' = termStr bod dep
in concat ["λ{ (): " , bod' , " }"]
termStr Emp dep = "⊥"
termStr Efq dep = "λ{}"
termStr (Let nam val bod) dep =
let nam' = nam
val' = termStr val dep
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["let " , nam' , " = " , val' , "; " , bod']
termStr (Use nam val bod) dep =
let nam' = nam
val' = termStr val dep
bod' = termStr (bod (Var nam dep)) (dep + 1)
in concat ["use " , nam' , " = " , val' , "; " , bod']
termStr Set dep = "*"
termStr (Ref nam) dep = nam
termStr (Var nam idx) dep = nam
termStr (Hol nam ctx) dep = "?" ++ nam
errorStr :: Book -> Error -> String
errorStr book (Error _ expected detected value dep) =
let exp = termStr (normal book 0 expected dep) dep
det = termStr (normal book 0 detected dep) dep
val = termStr (normal book 0 value dep) dep
in concat ["TypeMismatch:\n- Expected: ", exp, "\n- Detected: ", det, "\n- Bad-Term: ", val]
-- Parsing
-- -------
doParseTerm :: String -> Term
doParseTerm input = case P.parse parseTerm "" input of
Left err -> error $ "Parse error: " ++ show err
Right term -> bind term
parseTerm :: P.Parsec String () Term
parseTerm = do
P.spaces
P.choice
[ parseAll
, parseTap
, parseMat
, parseGet
, parseLam
, parseOne
, parseSum
, parseMul
, parseApp
, parseAnn
, parseSlf
, parseIns
, parseInl
, parseInr
, parseTup
, parseUni
, parseEmp
, parseEfq
, parseUse
, parseLet
, parseSet
, parseHol
, parseRef
]
parseAll = do
P.string "∀"
P.char '('
nam <- parseName
P.char ':'
inp <- parseTerm
P.char ')'
bod <- parseTerm
return $ All nam inp (\x -> bod)
parseLam = do
P.string "λ"
nam <- parseName
bod <- parseTerm
return $ Lam nam (\x -> bod)
parseApp = do
P.char '('
fun <- parseTerm
arg <- parseTerm
P.char ')'
return $ App fun arg
parseAnn = do
P.char '{'
val <- parseTerm
P.spaces
P.char ':'
chk <- P.option False (P.char ':' >> return True)
typ <- parseTerm
P.spaces
P.char '}'
return $ Ann chk val typ
parseSlf = do
P.string "$("
nam <- parseName
P.char ':'
typ <- parseTerm
P.char ')'
bod <- parseTerm
return $ Slf nam typ (\x -> bod)
parseIns = do
P.char '~'
val <- parseTerm
return $ Ins val
parseSum = do
P.try (P.string "(|")
a <- parseTerm
b <- parseTerm
P.char ')'
return $ Sum a b
parseInl = do
P.char '-'
x <- parseTerm
return $ Inl x
parseInr = do
P.char '+'
x <- parseTerm
return $ Inr x
parseMat = do
P.try $ do
P.string "λ{"
P.spaces
P.char '-'
P.char ':'
ifl <- parseTerm
P.spaces
P.char '|'
P.spaces
P.char '+'
P.char ':'
ifr <- parseTerm
P.spaces
P.char '}'
return $ Mat "l" "r" ifl ifr
parseMul = do
P.try (P.string "(&")
a <- parseTerm
b <- parseTerm
P.char ')'
return $ Mul a b
parseTup = do
P.string "#("
a <- parseTerm
P.char ','
b <- parseTerm
P.char ')'
return $ Tup a b
parseGet = do
P.try $ do
P.string "λ{"
P.spaces
P.string "(,):"
bod <- parseTerm
P.spaces
P.char '}'
return $ Get "a" "b" bod
parseUni = P.string "⊤" >> return Uni
parseOne = P.try (P.string "()" >> return One)
parseTap = do
P.try $ do
P.string "λ{"
P.spaces
P.string "():"
bod <- parseTerm
P.spaces
P.char '}'
return $ Tap bod
parseEmp = P.string "⊥" >> return Emp
parseEfq = P.try (P.string "λ{}") >> return Efq
parseUse = do
P.try (P.string "use ")
nam <- parseName
P.spaces
P.char '='
val <- parseTerm
P.char ';'
bod <- parseTerm
return $ Use nam val (\x -> bod)
parseLet = do
P.try (P.string "let ")
nam <- parseName
P.spaces
P.char '='
val <- parseTerm
P.char ';'
bod <- parseTerm
return $ Let nam val (\x -> bod)
parseSet = P.char '*' >> return Set
parseHol = do
P.char '?'
nam <- parseName
return $ Hol nam []
parseRef = do
name <- parseName
return $ case name of
"Set" -> Set
_ -> Ref name
parseName :: P.Parsec String () String
parseName = do
P.spaces
head <- P.letter
tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_' <|> P.char '-')
return (head : tail)
parseBook :: P.Parsec String () Book
parseBook = do
defs <- P.many parseDef
return $ M.fromList defs
parseDef :: P.Parsec String () (String, Term)
parseDef = do
name <- parseName
P.spaces
(typ, hasType) <- P.option (undefined, False) $ do
P.char ':'
typ <- parseTerm
P.spaces
return (typ, True)
P.char '='
value <- parseTerm
P.char ';'
P.spaces
return (name, if hasType then Ann False value typ else value)
doParseBook :: String -> Book
doParseBook input = case P.parse parseBook "" input of
Left err -> error $ "Parse error: " ++ show err
Right book -> M.map bind book
-- API
-- ---
-- Normalizes a term
apiNormal :: Book -> Term -> IO ()
apiNormal book term = putStrLn $ termStr (normal book 2 term 0) 0
-- Type-checks a term
apiCheck :: Book -> Term -> IO ()
apiCheck book term = case checkDef book term of
Right () -> putStrLn "Checked."
Left err -> putStrLn $ errorStr book err
-- Main
-- ----
book :: Book
book = M.fromList []
main :: IO ()
main = do
content <- readFile "main.tt"
let book = doParseBook content
forM_ (M.toList book) $ \(name, term) -> do
case checkDef book (Ref name) of
Right () -> putStrLn $ "Checked " ++ name ++ "."
Left err -> putStrLn $ errorStr book err
@VictorTaelin
Copy link
Author 
Bool : * = (| ⊤ ⊤);
false : Bool = -();
true  : Bool = +();

Bool/match : ∀(P: ∀(x: Bool) *) ∀(f: (P false)) ∀(t: (P true)) ∀(x: Bool) (P x) =
  λP λf λt λ{ -: λ{ (): f } | +: λ{ (): t } };

Nat : * = (| ⊤ Nat);
zero : Nat = -();
succ : ∀(n: Nat) Nat = λn +n;

Nat/match : ∀(P: ∀(x: Nat) *) ∀(z: (P zero)) ∀(s: ∀(n: Nat) (P (succ n))) ∀(x: Nat) (P x) =
  λP λz λs λ{ -: λ{ (): z } | +: s };

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment