mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Initial working type checker
This commit is contained in:
parent
469eb5976d
commit
27afb25616
611
checker.hvm
Normal file
611
checker.hvm
Normal file
@ -0,0 +1,611 @@
|
||||
Main =
|
||||
let term = (Rule0 Main.)
|
||||
let type = (TypeOf Main.)
|
||||
(Kind2.Result
|
||||
(Checked (Check term type Nil 0))
|
||||
(Reduced (Eval term)))
|
||||
|
||||
// Prelude
|
||||
// -------
|
||||
|
||||
// U60.if -(r: Type) U60 r r : r
|
||||
(U60.if 0 then else) = else
|
||||
(U60.if 1 then else) = then
|
||||
|
||||
// U60.equal U60 U60 : Bool
|
||||
(U60.equal a b) = (U60.if (== a b) True False)
|
||||
|
||||
// Bool.if -(r: Type) Bool r r : r
|
||||
(Bool.if False then else) = else
|
||||
(Bool.if True then else) = then
|
||||
|
||||
// Bool.and Bool Bool : Bool
|
||||
(Bool.and True b) = b
|
||||
(Bool.and False b) = False
|
||||
|
||||
// Maybe.case -(a: Type) -(r: Type) (Maybe a) r (a -> r) : r
|
||||
(Maybe.case None none some) = none
|
||||
(Maybe.case (Some val) none some) = (some val)
|
||||
|
||||
// Result.chain -(a: Type) -(b: Type) (Result a) (a -> Result b) : Result b
|
||||
(Result.chain (Done val) cont) = (cont val)
|
||||
(Result.chain (Fail msg) cont) = (Fail msg)
|
||||
|
||||
// List.at -(a: Type) (List a) U60 : (Maybe a)
|
||||
(List.at (Cons x xs) 0) = (Some x)
|
||||
(List.at (Cons x xs) n) = (List.at xs (- n 1))
|
||||
(List.at Nil n) = None
|
||||
|
||||
// Term.if_all -(r: Type) Term (Term -> (Term -> Term) -> r) r : r
|
||||
(Term.if_all (All type body) then else) = (then type body)
|
||||
(Term.if_all other then else) = else
|
||||
|
||||
// Arr Term Term : Term
|
||||
(Arr type retr) = (All type λx(retr))
|
||||
|
||||
// Equal Term Term : Bool
|
||||
// ----------------------
|
||||
|
||||
// Var equality
|
||||
(Equal (Var a.index) (Var b.index) dep) =
|
||||
(U60.equal a.index b.index)
|
||||
|
||||
// Typ equality
|
||||
(Equal Typ Typ dep) =
|
||||
True
|
||||
|
||||
// All equality
|
||||
(Equal (All a.type a.body) (All b.type b.body) dep) =
|
||||
let type = (Equal a.type b.type dep)
|
||||
let body = (Equal (a.body (Var dep)) (b.body (Var dep)) (+ dep 1))
|
||||
(Bool.and type body)
|
||||
|
||||
// Lam equality
|
||||
(Equal (Lam a.body) (Lam b.body) dep) =
|
||||
let body = (Equal (a.body (Var dep)) (b.body (Var dep)) (+ dep 1))
|
||||
body
|
||||
|
||||
// App equality
|
||||
(Equal (App a.func a.argm) (App b.func b.argm) dep) =
|
||||
let func = (Equal a.func b.func dep)
|
||||
let argm = (Equal a.argm b.argm dep)
|
||||
(Bool.and func argm)
|
||||
|
||||
// Ct0 equality
|
||||
(Equal (Ct0 a.ctid) (Ct0 b.ctid) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
ctid
|
||||
|
||||
// Ct1 equality
|
||||
(Equal (Ct1 a.ctid a.x0) (Ct1 b.ctid b.x0) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
(Bool.and ctid x0)
|
||||
|
||||
// Ct2 equality
|
||||
(Equal (Ct2 a.ctid a.x0 a.x1) (Ct2 b.ctid b.x0 b.x1) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
(Bool.and ctid (Bool.and x0 x1))
|
||||
|
||||
// Ct3 equality
|
||||
(Equal (Ct3 a.ctid a.x0 a.x1 a.x2) (Ct3 b.ctid b.x0 b.x1 b.x2) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))
|
||||
|
||||
// Ct4 equality
|
||||
(Equal (Ct4 a.ctid a.x0 a.x1 a.x2 a.x3) (Ct4 b.ctid b.x0 b.x1 b.x2 b.x3) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
let x3 = (Equal a.x3 b.x3 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3))))
|
||||
|
||||
// Ct5 equality
|
||||
(Equal (Ct5 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4) (Ct5 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
let x3 = (Equal a.x3 b.x3 dep)
|
||||
let x4 = (Equal a.x4 b.x4 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))) )
|
||||
|
||||
// Ct6 equality
|
||||
(Equal (Ct6 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Ct6 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
let x3 = (Equal a.x3 b.x3 dep)
|
||||
let x4 = (Equal a.x4 b.x4 dep)
|
||||
let x5 = (Equal a.x5 b.x5 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5))))))
|
||||
|
||||
// Ct7 equality
|
||||
(Equal (Ct7 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Ct7 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
let x3 = (Equal a.x3 b.x3 dep)
|
||||
let x4 = (Equal a.x4 b.x4 dep)
|
||||
let x5 = (Equal a.x5 b.x5 dep)
|
||||
let x6 = (Equal a.x6 b.x6 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6)))))))
|
||||
|
||||
// Ct8 equality
|
||||
(Equal (Ct8 a.ctid a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Ct8 b.ctid b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7) dep) =
|
||||
let ctid = (U60.equal (MakeId a.ctid) (MakeId b.ctid))
|
||||
let x0 = (Equal a.x0 b.x0 dep)
|
||||
let x1 = (Equal a.x1 b.x1 dep)
|
||||
let x2 = (Equal a.x2 b.x2 dep)
|
||||
let x3 = (Equal a.x3 b.x3 dep)
|
||||
let x4 = (Equal a.x4 b.x4 dep)
|
||||
let x5 = (Equal a.x5 b.x5 dep)
|
||||
let x6 = (Equal a.x6 b.x6 dep)
|
||||
let x7 = (Equal a.x7 b.x7 dep)
|
||||
(Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7))))))))
|
||||
|
||||
// Not equal
|
||||
(Equal a b dep) =
|
||||
False
|
||||
|
||||
// Infer Term (List Term) U60 : Result Term
|
||||
// ----------------------------------------
|
||||
|
||||
// Infers Var
|
||||
(Infer (Var index) ctx dep) =
|
||||
(Maybe.case (List.at ctx (- (- dep index) 1))
|
||||
// case none:
|
||||
(Fail UnboundVariable)
|
||||
// case some:
|
||||
λvar_type (Done var_type))
|
||||
|
||||
// Infers Typ
|
||||
(Infer Typ ctx dep) =
|
||||
(Done Typ)
|
||||
|
||||
// Infers All
|
||||
(Infer (All type body) ctx dep) =
|
||||
(Result.chain (Check type Typ ctx dep) λtype_chk
|
||||
(Result.chain (Check (body (Var dep)) Typ (Cons type ctx) (+ dep 1)) λbody_chk
|
||||
(Done Typ)))
|
||||
|
||||
// Infers Lam
|
||||
(Infer (Lam body) ctx dep) =
|
||||
(Fail CantInferLambda)
|
||||
|
||||
// Infers App
|
||||
(Infer (App func argm) ctx dep) =
|
||||
(Result.chain (Infer func ctx dep) λfunc_typ
|
||||
(Term.if_all func_typ
|
||||
// then
|
||||
λfunc_typ_type λfunc_typ_body
|
||||
(Result.chain (Check argm func_typ_type ctx dep) λargm_chk
|
||||
(Done (func_typ_body argm)))
|
||||
// else
|
||||
(Fail NonFunctionApplication)
|
||||
))
|
||||
|
||||
// Infers Ct0
|
||||
(Infer (Ct0 ctid) ctx dep) =
|
||||
(Done (TypeOf ctid))
|
||||
|
||||
// Infers Ct1
|
||||
(Infer (Ct1 ctid x0) ctx dep) =
|
||||
(Infer (App (Ct0 ctid) x0) ctx dep)
|
||||
|
||||
// Infers Ct2
|
||||
(Infer (Ct2 ctid x0 x1) ctx dep) =
|
||||
(Infer (App (App (Ct0 ctid) x0) x1) ctx dep)
|
||||
|
||||
// Infers Ct3
|
||||
(Infer (Ct3 ctid x0 x1 x2) ctx dep) =
|
||||
(Infer (App (App (App (Ct0 ctid) x0) x1) x2) ctx dep)
|
||||
|
||||
// Infers Ct4
|
||||
(Infer (Ct4 ctid x0 x1 x2 x3) ctx dep) =
|
||||
(Infer (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) ctx dep)
|
||||
|
||||
// Infers Ct5
|
||||
(Infer (Ct5 ctid x0 x1 x2 x3 x4) ctx dep) =
|
||||
(Infer (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) ctx dep)
|
||||
|
||||
// Infers Ct6
|
||||
(Infer (Ct6 ctid x0 x1 x2 x3 x4 x5) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5) ctx dep)
|
||||
|
||||
// Infers Ct7
|
||||
(Infer (Ct7 ctid x0 x1 x2 x3 x4 x5 x6) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5) x6) ctx dep)
|
||||
|
||||
// Infers Ct8
|
||||
(Infer (Ct8 ctid x0 x1 x2 x3 x4 x5 x6 x7) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (App (App (Ct0 ctid) x0) x1) x2) x3) x4) x5) x6) x7) ctx dep)
|
||||
|
||||
// Infers Fn0
|
||||
(Infer (Fn0 ctid) ctx dep) =
|
||||
(Done (TypeOf ctid))
|
||||
|
||||
// Infers Fn1
|
||||
(Infer (Fn1 ctid x0) ctx dep) =
|
||||
(Infer (App (Fn0 ctid) x0) ctx dep)
|
||||
|
||||
// Infers Fn2
|
||||
(Infer (Fn2 ctid x0 x1) ctx dep) =
|
||||
(Infer (App (App (Fn0 ctid) x0) x1) ctx dep)
|
||||
|
||||
// Infers Fn3
|
||||
(Infer (Fn3 ctid x0 x1 x2) ctx dep) =
|
||||
(Infer (App (App (App (Fn0 ctid) x0) x1) x2) ctx dep)
|
||||
|
||||
// Infers Fn4
|
||||
(Infer (Fn4 ctid x0 x1 x2 x3) ctx dep) =
|
||||
(Infer (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) ctx dep)
|
||||
|
||||
// Infers Fn5
|
||||
(Infer (Fn5 ctid x0 x1 x2 x3 x4) ctx dep) =
|
||||
(Infer (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) ctx dep)
|
||||
|
||||
// Infers Fn6
|
||||
(Infer (Fn6 ctid x0 x1 x2 x3 x4 x5) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5) ctx dep)
|
||||
|
||||
// Infers Fn7
|
||||
(Infer (Fn7 ctid x0 x1 x2 x3 x4 x5 x6) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5) x6) ctx dep)
|
||||
|
||||
// Infers Fn8
|
||||
(Infer (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7) ctx dep) =
|
||||
(Infer (App (App (App (App (App (App (App (App (Fn0 ctid) x0) x1) x2) x3) x4) x5) x6) x7) ctx dep)
|
||||
|
||||
// Check Term Term (List Term) U60 : Result Unit
|
||||
// ---------------------------------------------
|
||||
|
||||
// Checks Lam
|
||||
(Check (Lam body) (All t_type t_body) ctx dep) =
|
||||
(Result.chain (Check (body (Var dep)) (t_body (Var dep)) (Cons t_type ctx) (+ dep 1)) λbody_chk
|
||||
(Done Unit))
|
||||
|
||||
// Checks others
|
||||
(Check term type ctx dep) =
|
||||
(Result.chain (Infer term ctx dep) λterm_typ
|
||||
(Bool.if (Equal term_typ type dep)
|
||||
// then
|
||||
(Done Unit)
|
||||
// else
|
||||
(Fail (TypeMismatch term_typ type)) // TODO: pass up for Rust to display
|
||||
))
|
||||
|
||||
// Show Term U60 : Term
|
||||
// ---------------------
|
||||
|
||||
// Show Var
|
||||
(Show (Var index) dep) =
|
||||
(Var index)
|
||||
|
||||
// Show Typ
|
||||
(Show Typ dep) =
|
||||
Typ
|
||||
|
||||
// Show All
|
||||
(Show (All type body) dep) =
|
||||
(All (Show type dep) λx (Show (body (Var dep)) (+ dep 1)))
|
||||
|
||||
// Show Lam
|
||||
(Show (Lam body) dep) =
|
||||
(Lam λx (Show (body (Var dep)) (+ dep 1)))
|
||||
|
||||
// Show App
|
||||
(Show (App func argm) dep) =
|
||||
(App (Show func dep) (Show argm dep))
|
||||
|
||||
// Show Ct0
|
||||
(Show (Ct0 ctid) dep) =
|
||||
(Ct0 ctid)
|
||||
|
||||
// Show Ct1
|
||||
(Show (Ct1 ctid x0) dep) =
|
||||
(Ct1 ctid (Show x0 dep))
|
||||
|
||||
// Show Ct2
|
||||
(Show (Ct2 ctid x0 x1) dep) =
|
||||
(Ct2 ctid (Show x0 dep) (Show x1 dep))
|
||||
|
||||
// Show Ct3
|
||||
(Show (Ct3 ctid x0 x1 x2) dep) =
|
||||
(Ct3 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep))
|
||||
|
||||
// Show Ct4
|
||||
(Show (Ct4 ctid x0 x1 x2 x3) dep) =
|
||||
(Ct4 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep))
|
||||
|
||||
// Show Ct5
|
||||
(Show (Ct5 ctid x0 x1 x2 x3 x4) dep) =
|
||||
(Ct5 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep))
|
||||
|
||||
// Show Ct6
|
||||
(Show (Ct6 ctid x0 x1 x2 x3 x4 x5) dep) =
|
||||
(Ct6 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep))
|
||||
|
||||
// Show Ct7
|
||||
(Show (Ct7 ctid x0 x1 x2 x3 x4 x5 x6) dep) =
|
||||
(Ct7 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep) (Show x6 dep))
|
||||
|
||||
// Show Ct8
|
||||
(Show (Ct8 ctid x0 x1 x2 x3 x4 x5 x6 x7) dep) =
|
||||
(Ct8 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep) (Show x6 dep) (Show x7 dep))
|
||||
|
||||
// Show Fn0
|
||||
(Show (Fn0 ctid) dep) =
|
||||
(Fn0 ctid)
|
||||
|
||||
// Show Fn1
|
||||
(Show (Fn1 ctid x0) dep) =
|
||||
(Fn1 ctid (Show x0 dep))
|
||||
|
||||
// Show Fn2
|
||||
(Show (Fn2 ctid x0 x1) dep) =
|
||||
(Fn2 ctid (Show x0 dep) (Show x1 dep))
|
||||
|
||||
// Show Fn3
|
||||
(Show (Fn3 ctid x0 x1 x2) dep) =
|
||||
(Fn3 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep))
|
||||
|
||||
// Show Fn4
|
||||
(Show (Fn4 ctid x0 x1 x2 x3) dep) =
|
||||
(Fn4 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep))
|
||||
|
||||
// Show Fn5
|
||||
(Show (Fn5 ctid x0 x1 x2 x3 x4) dep) =
|
||||
(Fn5 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep))
|
||||
|
||||
// Show Fn6
|
||||
(Show (Fn6 ctid x0 x1 x2 x3 x4 x5) dep) =
|
||||
(Fn6 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep))
|
||||
|
||||
// Show Fn7
|
||||
(Show (Fn7 ctid x0 x1 x2 x3 x4 x5 x6) dep) =
|
||||
(Fn7 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep) (Show x6 dep))
|
||||
|
||||
// Show Fn8
|
||||
(Show (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7) dep) =
|
||||
(Fn8 ctid (Show x0 dep) (Show x1 dep) (Show x2 dep) (Show x3 dep) (Show x4 dep) (Show x5 dep) (Show x6 dep) (Show x7 dep))
|
||||
|
||||
// Eval Term (List Term) : Term
|
||||
// ----------------------------
|
||||
|
||||
// Eval Var
|
||||
(Eval (Var index)) =
|
||||
(Var index)
|
||||
|
||||
// Eval Typ
|
||||
(Eval Typ) =
|
||||
Typ
|
||||
|
||||
// Eval All
|
||||
(Eval (All type body)) =
|
||||
(All (Eval type) λx (Eval (body x)))
|
||||
|
||||
// Eval Lam
|
||||
(Eval (Lam body)) =
|
||||
(Lam λx (Eval (body x)))
|
||||
|
||||
// Eval App
|
||||
(Eval (App func argm)) =
|
||||
(Apply (Eval func) (Eval argm))
|
||||
|
||||
// Eval Ct0
|
||||
(Eval (Ct0 ctid)) =
|
||||
(Ct0 ctid)
|
||||
|
||||
// Eval Ct1
|
||||
(Eval (Ct1 ctid x0)) =
|
||||
(Ct1 ctid (Eval x0))
|
||||
|
||||
// Eval Ct2
|
||||
(Eval (Ct2 ctid x0 x1)) =
|
||||
(Ct2 ctid (Eval x0) (Eval x1))
|
||||
|
||||
// Eval Ct3
|
||||
(Eval (Ct3 ctid x0 x1 x2)) =
|
||||
(Ct3 ctid (Eval x0) (Eval x1) (Eval x2))
|
||||
|
||||
// Eval Ct4
|
||||
(Eval (Ct4 ctid x0 x1 x2 x3)) =
|
||||
(Ct4 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3))
|
||||
|
||||
// Eval Ct5
|
||||
(Eval (Ct5 ctid x0 x1 x2 x3 x4)) =
|
||||
(Ct5 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4))
|
||||
|
||||
// Eval Ct6
|
||||
(Eval (Ct6 ctid x0 x1 x2 x3 x4 x5)) =
|
||||
(Ct6 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5))
|
||||
|
||||
// Eval Ct7
|
||||
(Eval (Ct7 ctid x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Ct7 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6))
|
||||
|
||||
// Eval Ct8
|
||||
(Eval (Ct8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Ct8 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6) (Eval x7))
|
||||
|
||||
// Eval Fn0
|
||||
(Eval (Fn0 ctid)) =
|
||||
(Eval (Rule0 ctid))
|
||||
|
||||
// Eval Fn1
|
||||
(Eval (Fn1 ctid x0)) =
|
||||
(Eval (Rule1 ctid (Eval x0)))
|
||||
|
||||
// Eval Fn2
|
||||
(Eval (Fn2 ctid x0 x1)) =
|
||||
(Eval (Rule2 ctid (Eval x0) (Eval x1)))
|
||||
|
||||
// Eval Fn3
|
||||
(Eval (Fn3 ctid x0 x1 x2)) =
|
||||
(Eval (Rule3 ctid (Eval x0) (Eval x1) (Eval x2)))
|
||||
|
||||
// Eval Fn4
|
||||
(Eval (Fn4 ctid x0 x1 x2 x3)) =
|
||||
(Eval (Rule4 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3)))
|
||||
|
||||
// Eval Fn5
|
||||
(Eval (Fn5 ctid x0 x1 x2 x3 x4)) =
|
||||
(Eval (Rule5 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4)))
|
||||
|
||||
// Eval Fn6
|
||||
(Eval (Fn6 ctid x0 x1 x2 x3 x4 x5)) =
|
||||
(Eval (Rule6 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5)))
|
||||
|
||||
// Eval Fn7
|
||||
(Eval (Fn7 ctid x0 x1 x2 x3 x4 x5 x6)) =
|
||||
(Eval (Rule7 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6)))
|
||||
|
||||
// Eval Fn8
|
||||
(Eval (Fn8 ctid x0 x1 x2 x3 x4 x5 x6 x7)) =
|
||||
(Eval (Rule8 ctid (Eval x0) (Eval x1) (Eval x2) (Eval x3) (Eval x4) (Eval x5) (Eval x6) (Eval x7)))
|
||||
|
||||
|
||||
// Apply Term Term : Term
|
||||
// ----------------------
|
||||
|
||||
(Apply (Lam fbody) argm) = (fbody argm)
|
||||
(Apply func argm) = (App func argm)
|
||||
|
||||
//// Reduction Rules
|
||||
//// ---------------
|
||||
|
||||
//(Call1 Not. (Ct0 True.)) = (Eval (Ct0 False.))
|
||||
//(Call1 Not. (Ct0 False.)) = (Eval (Ct0 True.))
|
||||
//(Call2 And. (Ct0 True.) (Ct0 True.)) = (Eval (Ct0 True.))
|
||||
//(Call2 And. (Ct0 True.) (Ct0 False.)) = (Eval (Ct0 True.))
|
||||
//(Call2 And. (Ct0 False.) (Ct0 True.)) = (Eval (Ct0 True.))
|
||||
//(Call2 And. (Ct0 False.) (Ct0 False.)) = (Eval (Ct0 True.))
|
||||
//(Call1 Theo. (Ct0 True.)) = (Eval (Ct0 Refl.))
|
||||
//(Call1 Theo. (Ct0 False.)) = (Eval (Ct0 Refl.))
|
||||
//(Call1 Mul2. (Ct0 Zero.)) = (Eval (Ct0 Zero.))
|
||||
//(Call1 Mul2. (Ct1 Succ. n)) = (Eval (Ct1 Succ. (Ct1 Succ. (Call1 Mul2. n))))
|
||||
//(Call1 F. a) = (Eval (Lam λb (Fn2 G. a b)))
|
||||
//(Call2 G. (Ct0 U.) (Ct0 U.)) = (Eval (Lam λx x))
|
||||
//(Call0 Test.0.) = (Eval (App (Fn1 F. (Ct0 U.)) (Ct0 U.)))
|
||||
//(Call0 Test.1.) = (Eval (Fn1 Mul2. (Fn1 Mul2. (Ct1 Succ. (Ct1 Succ. (Ct0 Zero.))))))
|
||||
|
||||
//// Type Annotations
|
||||
//// ----------------
|
||||
|
||||
//(TypeOf Bool.) = Typ
|
||||
//(TypeOf True.) = (Ct0 Bool.)
|
||||
//(TypeOf False.) = (Ct0 Bool.)
|
||||
//(TypeOf Nat.) = Typ
|
||||
//(TypeOf Zero.) = (Ct0 Nat.)
|
||||
//(TypeOf Succ.) = (All (Ct0 Nat.) λx0 (Ct0 Nat.))
|
||||
//(TypeOf Not.) = (All (Ct0 Bool.) λx0 (Ct0 Bool.))
|
||||
//(TypeOf And.) = (All (Ct0 Bool.) λx0 (All (Ct0 Bool.) λx1 (Ct0 Bool.)))
|
||||
|
||||
//// Label to Id
|
||||
//// -----------
|
||||
|
||||
//(MakeId Bool.) = 0
|
||||
//(MakeId True.) = 1
|
||||
//(MakeId False.) = 2
|
||||
//(MakeId Nat.) = 3
|
||||
//(MakeId Zero.) = 4
|
||||
//(MakeId Succ.) = 5
|
||||
|
||||
// User-Defined Functions
|
||||
// ----------------------
|
||||
|
||||
// Nat
|
||||
// ---
|
||||
|
||||
(MakeId Nat.) = %Nat
|
||||
(TypeOf Nat.) = Typ
|
||||
|
||||
// False
|
||||
// -----
|
||||
|
||||
(MakeId False.) = %False
|
||||
(TypeOf False.) = (Ct0 Bool.)
|
||||
|
||||
// List
|
||||
// ----
|
||||
|
||||
(MakeId List.) = %List
|
||||
(TypeOf List.) = (All Typ λa Typ)
|
||||
|
||||
// True
|
||||
// ----
|
||||
|
||||
(MakeId True.) = %True
|
||||
(TypeOf True.) = (Ct0 Bool.)
|
||||
|
||||
// Bool
|
||||
// ----
|
||||
|
||||
(MakeId Bool.) = %Bool
|
||||
(TypeOf Bool.) = Typ
|
||||
|
||||
// Succ
|
||||
// ----
|
||||
|
||||
(MakeId Succ.) = %Succ
|
||||
(TypeOf Succ.) = (All (Ct0 Nat.) λpred (Ct0 Nat.))
|
||||
|
||||
// Negate
|
||||
// ------
|
||||
|
||||
(MakeId Negate.) = %Negate
|
||||
(TypeOf Negate.) = (All (Ct1 List. (Ct0 Bool.)) λxs (Ct1 List. (Ct0 Bool.)))
|
||||
(Rule1 Negate. (Ct3 Cons. (Ct0 Bool.) x xs)) = (Ct3 Cons. (Ct0 Bool.) (Fn1 Not. x) (Fn1 Negate. xs))
|
||||
(Rule1 Negate. (Ct1 Nil. (Ct0 Bool.))) = (Ct1 Nil. (Ct0 Bool.))
|
||||
|
||||
// Cons
|
||||
// ----
|
||||
|
||||
(MakeId Cons.) = %Cons
|
||||
(TypeOf Cons.) = (All Typ λa (All a λx (All (Ct1 List. a) λxs (Ct1 List. a))))
|
||||
|
||||
// And
|
||||
// ---
|
||||
|
||||
(MakeId And.) = %And
|
||||
(TypeOf And.) = (All (Ct0 Bool.) λa (All (Ct0 Bool.) λb (Ct0 Bool.)))
|
||||
(Rule2 And. (Ct0 True.) (Ct0 True.)) = (Ct0 True.)
|
||||
(Rule2 And. (Ct0 True.) (Ct0 False.)) = (Ct0 False.)
|
||||
(Rule2 And. (Ct0 False.) (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule2 And. (Ct0 False.) (Ct0 False.)) = (Ct0 False.)
|
||||
|
||||
// Not
|
||||
// ---
|
||||
|
||||
(MakeId Not.) = %Not
|
||||
(TypeOf Not.) = (All (Ct0 Bool.) λa (Ct0 Bool.))
|
||||
(Rule1 Not. (Ct0 True.)) = (Ct0 False.)
|
||||
(Rule1 Not. (Ct0 False.)) = (Ct0 True.)
|
||||
|
||||
// Nil
|
||||
// ---
|
||||
|
||||
(MakeId Nil.) = %Nil
|
||||
(TypeOf Nil.) = (All Typ λa (Ct1 List. a))
|
||||
|
||||
// Zero
|
||||
// ----
|
||||
|
||||
(MakeId Zero.) = %Zero
|
||||
(TypeOf Zero.) = (Ct0 Nat.)
|
||||
|
||||
// Main
|
||||
// ----
|
||||
|
||||
(MakeId Main.) = %Main
|
||||
(TypeOf Main.) = (Ct1 List. (Ct0 Bool.))
|
||||
(Rule0 Main.) = (Fn1 Negate. (Ct3 Cons. (Ct0 Bool.) (Ct0 True.) (Ct3 Cons. (Ct0 Bool.) (Ct0 False.) (Ct1 Nil. (Ct0 Bool.)))))
|
237
src/main.rs
237
src/main.rs
@ -1,7 +1,8 @@
|
||||
#![allow(dead_code)]
|
||||
#![allow(unused_variables)]
|
||||
|
||||
// imports hashmap
|
||||
// TODO: type{} syntax
|
||||
|
||||
use std::collections::HashMap;
|
||||
|
||||
// type Bool {
|
||||
@ -19,19 +20,19 @@ use std::collections::HashMap;
|
||||
// }
|
||||
//
|
||||
// Add (a: Nat) (b: Nat) : Nat {
|
||||
// {Zero} b => b
|
||||
// {Succ a} b => {Succ (Add a b)}
|
||||
// Add {Zero} b => b
|
||||
// Add {Succ a} b => {Succ (Add a b)}
|
||||
// }
|
||||
//
|
||||
// Add (a: Nat) (b: Nat) : Nat =
|
||||
// match a {
|
||||
// {Zero} => b
|
||||
// {Succ a} => {Succ (Add a b)}
|
||||
// Add {Zero} => b
|
||||
// Add {Succ a} => {Succ (Add a b)}
|
||||
// }
|
||||
//
|
||||
// Map <A: Type> <B: Type> (f: A -> B) (xs: List A) : List B {
|
||||
// A B f {Cons x xs} => {Cons (f x) (map A B f xs)}
|
||||
// A B f {Nil} => {Nil}
|
||||
// Map A B f {Cons x xs} => {Cons (f x) (map A B f xs)}
|
||||
// Map A B f {Nil} => {Nil}
|
||||
// }
|
||||
//
|
||||
// Main : (List Nat) =
|
||||
@ -60,9 +61,9 @@ pub enum Term {
|
||||
Typ,
|
||||
Var { name: String },
|
||||
Let { name: String, expr: Box<Term>, body: Box<Term> },
|
||||
App { func: Box<Term>, argm: Box<Term> },
|
||||
Lam { name: String, body: Box<Term> },
|
||||
All { name: String, tipo: Box<Term>, body: Box<Term> },
|
||||
Lam { name: String, body: Box<Term> },
|
||||
App { func: Box<Term>, argm: Box<Term> },
|
||||
Ctr { name: String, args: Vec<Box<Term>> },
|
||||
Fun { name: String, args: Vec<Box<Term>> },
|
||||
}
|
||||
@ -76,6 +77,7 @@ pub struct Argument {
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Rule {
|
||||
name: String,
|
||||
pats: Vec<Box<Term>>,
|
||||
body: Box<Term>,
|
||||
}
|
||||
@ -93,6 +95,9 @@ pub struct File {
|
||||
entries: HashMap<String, Box<Entry>>
|
||||
}
|
||||
|
||||
// Parser
|
||||
// ======
|
||||
|
||||
pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
parser::guard(
|
||||
Box::new(|state| {
|
||||
@ -247,23 +252,27 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
let (state, name) = parser::name1(state)?;
|
||||
let (state, args) = parser::until(parser::text_parser(":"), Box::new(parse_argument), state)?;
|
||||
let (state, tipo) = parse_term(state)?;
|
||||
let (state, head) = parser::get_char(state)?;
|
||||
let (state, head) = parser::peek_char(state)?;
|
||||
if head == '=' {
|
||||
let (state, _) = parser::consume("=", state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
let rules = vec![Box::new(Rule { pats: vec![], body })];
|
||||
let rules = vec![Box::new(Rule { name: name.clone(), pats: vec![], body })];
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
|
||||
} else if head == '{' {
|
||||
let (state, rules) = parser::until(parser::text_parser("}"), Box::new(parse_rule), state)?;
|
||||
let (state, _) = parser::consume("{", state)?;
|
||||
let name_clone = name.clone();
|
||||
let (state, rules) = parser::until(parser::text_parser("}"), Box::new(move |state| parse_rule(state, name_clone.clone())), state)?;
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
|
||||
} else {
|
||||
parser::expected("'=' or '{'", 1, state)
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules: vec![] })));
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_rule(state: parser::State) -> parser::Answer<Box<Rule>> {
|
||||
let (state, pats) = parser::until(parser::text_parser("=>"), Box::new(parse_term), state)?;
|
||||
pub fn parse_rule(state: parser::State, name: String) -> parser::Answer<Box<Rule>> {
|
||||
let (state, _) = parser::consume(&name, state)?;
|
||||
let (state, pats) = parser::until(parser::text_parser("="), Box::new(parse_term), state)?;
|
||||
let (state, body) = parse_term(state)?;
|
||||
return Ok((state, Box::new(Rule { pats, body })));
|
||||
return Ok((state, Box::new(Rule { name, pats, body })));
|
||||
}
|
||||
|
||||
pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
|
||||
@ -325,12 +334,13 @@ pub fn show_term(term: &Term) -> String {
|
||||
}
|
||||
|
||||
pub fn show_rule(rule: &Rule) -> String {
|
||||
let name = &rule.name;
|
||||
let mut pats = vec![];
|
||||
for pat in &rule.pats {
|
||||
pats.push(show_term(pat));
|
||||
}
|
||||
let body = show_term(&rule.body);
|
||||
format!("{} => {}", pats.join(" "), body)
|
||||
format!("{} {} => {}", name, pats.join(" "), body)
|
||||
}
|
||||
|
||||
pub fn show_entry(entry: &Entry) -> String {
|
||||
@ -339,12 +349,16 @@ pub fn show_entry(entry: &Entry) -> String {
|
||||
for arg in &entry.args {
|
||||
args.push(format!(" ({}: {})", arg.name, show_term(&arg.tipo)));
|
||||
}
|
||||
if entry.rules.len() == 0 {
|
||||
format!("{}{} : {}", name, args.join(""), show_term(&entry.tipo))
|
||||
} else {
|
||||
let mut rules = vec![];
|
||||
for rule in &entry.rules {
|
||||
rules.push(format!("\n {}", show_rule(rule)));
|
||||
}
|
||||
format!("{}{} : {} {{{}\n}}", name, args.join(""), show_term(&entry.tipo), rules.join(""))
|
||||
}
|
||||
}
|
||||
|
||||
pub fn show_file(file: &File) -> String {
|
||||
let mut entries = vec![];
|
||||
@ -362,56 +376,169 @@ pub fn read_file(code: &str) -> Result<Box<File>, String> {
|
||||
parser::read(Box::new(parse_file), code)
|
||||
}
|
||||
|
||||
// Compiler
|
||||
// ========
|
||||
|
||||
//pub enum Term {
|
||||
//Typ,
|
||||
//Var { name: String },
|
||||
//Let { name: String, expr: Box<Term>, body: Box<Term> },
|
||||
//App { func: Box<Term>, argm: Box<Term> },
|
||||
//Lam { name: String, body: Box<Term> },
|
||||
//All { name: String, tipo: Box<Term>, body: Box<Term> },
|
||||
//Ctr { name: String, args: Vec<Box<Term>> },
|
||||
//Fun { name: String, args: Vec<Box<Term>> },
|
||||
//}
|
||||
pub fn compile_term(term: &Term) -> String {
|
||||
match term {
|
||||
Term::Typ => {
|
||||
format!("Typ")
|
||||
}
|
||||
Term::Var { name } => {
|
||||
name.clone()
|
||||
}
|
||||
Term::Let { name, expr, body } => {
|
||||
todo!()
|
||||
}
|
||||
Term::All { name, tipo, body } => {
|
||||
format!("(All {} λ{} {})", compile_term(tipo), name, compile_term(body))
|
||||
}
|
||||
Term::Lam { name, body } => {
|
||||
format!("(Lam λ{} {})", name, compile_term(body))
|
||||
}
|
||||
Term::App { func, argm } => {
|
||||
format!("(App {} {})", compile_term(func), compile_term(argm))
|
||||
}
|
||||
Term::Ctr { name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg)));
|
||||
}
|
||||
format!("(Ct{} {}.{})", args.len(), name, args_strs.join(""))
|
||||
}
|
||||
Term::Fun { name, args } => {
|
||||
let mut args_strs : Vec<String> = Vec::new();
|
||||
for arg in args {
|
||||
args_strs.push(format!(" {}", compile_term(arg)));
|
||||
}
|
||||
format!("(Fn{} {}.{})", args.len(), name, args_strs.join(""))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//pub struct Entry {
|
||||
//name: String,
|
||||
//args: Vec<Box<Argument>>,
|
||||
//tipo: Box<Term>,
|
||||
//rules: Vec<Box<Rule>>
|
||||
//}
|
||||
pub fn compile_entry(entry: &Entry) -> String {
|
||||
fn compile_type(args: &Vec<Box<Argument>>, tipo: &Box<Term>, index: usize) -> String {
|
||||
if index < args.len() {
|
||||
let arg = &args[index];
|
||||
format!("(All {} λ{} {})", compile_term(&arg.tipo), arg.name, compile_type(args, tipo, index + 1))
|
||||
} else {
|
||||
compile_term(tipo)
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_rule(rule: &Rule) -> String {
|
||||
let mut pats = vec![];
|
||||
for pat in &rule.pats {
|
||||
pats.push(format!(" {}", compile_term(pat)));
|
||||
}
|
||||
let body = compile_term(&rule.body);
|
||||
let mut text = String::new();
|
||||
//text.push_str(&format!(" (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
|
||||
text.push_str(&format!(" (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body));
|
||||
return text;
|
||||
}
|
||||
|
||||
let mut result = String::new();
|
||||
result.push_str(&format!(" (MakeId {}.) = %{}\n", entry.name, entry.name));
|
||||
result.push_str(&format!(" (TypeOf {}.) = {}\n", entry.name, compile_type(&entry.args, &entry.tipo, 0)));
|
||||
for rule in &entry.rules {
|
||||
result.push_str(&compile_rule(&rule));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
pub fn compile_file(file: &File) -> String {
|
||||
let mut result = String::new();
|
||||
for entry in file.entries.values() {
|
||||
result.push_str(&format!(" // {}\n", entry.name));
|
||||
result.push_str(&format!(" // {}\n", "-".repeat(entry.name.len())));
|
||||
result.push_str(&format!("\n"));
|
||||
result.push_str(&compile_entry(&entry));
|
||||
result.push_str(&format!("\n"));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
fn main() -> Result<(), String> {
|
||||
|
||||
//let term = read_term("{Foo @x(x) {Tic} {Tac}}")?;
|
||||
//println!("Parsed: {}", show_term(&*term));
|
||||
//let file = read_file("
|
||||
//Bool : Type
|
||||
//True : Bool
|
||||
//False : Bool
|
||||
|
||||
//List (a: Type) : Type
|
||||
//Nil (a: Type) : (List a)
|
||||
//Cons (a: Type) (x: a) (xs: (List a)) : (List a)
|
||||
|
||||
//Add (a: Nat) (b: Nat) : Nat {
|
||||
//Add {Zero} b = b
|
||||
//Add {Succ a} b = {Succ (Add a b)}
|
||||
//}
|
||||
|
||||
//Not (a: Bool) : Bool {
|
||||
//Not {True} = {False}
|
||||
//Not {False} = {True}
|
||||
//}
|
||||
|
||||
//Map (a: Type) (b: Type) (f: (x: a) a) (xs: {List a}) : {List b} {
|
||||
//Map a b f {Cons x xs} = {Cons (f x) (Map a b f xs)}
|
||||
//Map a b f Nil = {Nil}
|
||||
//}
|
||||
//")?;
|
||||
|
||||
let file = read_file("
|
||||
Bool : Type {}
|
||||
True : Bool {}
|
||||
False : Bool {}
|
||||
Bool : Type
|
||||
True : Bool
|
||||
False : Bool
|
||||
|
||||
Add (a: Nat) (b: Nat) : Nat {
|
||||
{Zero} b => b
|
||||
{Succ a} b => {Succ (Add a b)}
|
||||
}
|
||||
Nat : Type
|
||||
Zero : Nat
|
||||
Succ (pred: Nat) : Nat
|
||||
|
||||
List (a: Type) : Type
|
||||
Nil (a: Type) : {List a}
|
||||
Cons (a: Type) (x: a) (xs: {List a}) : {List a}
|
||||
|
||||
Not (a: Bool) : Bool {
|
||||
{True} => {False}
|
||||
{False} => {True}
|
||||
Not True = False
|
||||
Not False = True
|
||||
}
|
||||
|
||||
Map (a: Type) (b: Type) (f: (x: a) a) (xs: (List a)) : (List b) {
|
||||
a b f {Cons x xs} => {Cons (f x) (Map a b f xs)}
|
||||
a b f Nil => {Nil}
|
||||
And (a: Bool) (b: Bool) : Bool {
|
||||
And True True = True
|
||||
And True False = False
|
||||
And False True = False
|
||||
And False False = False
|
||||
}
|
||||
|
||||
Negate (xs: {List Bool}) : {List Bool} {
|
||||
Negate {Cons Bool x xs} = {Cons Bool (Not x) (Negate xs)}
|
||||
Negate {Nil Bool} = {Nil Bool}
|
||||
}
|
||||
|
||||
Main : {List Bool} = (Negate {Cons Bool True {Cons Bool False {Nil Bool}}})
|
||||
")?;
|
||||
|
||||
println!("parsed:\n\n{}", show_file(&file));
|
||||
println!("Parsed:\n\n{}\n\n", show_file(&file));
|
||||
|
||||
println!("Compiled:\n\n");
|
||||
println!("{}", compile_file(&file));
|
||||
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
//Map (a: {Type}) (b: {Type}) (f: (x: a) a) (xs: ({List} a)) : ({List} b) {
|
||||
//a b f {Cons x xs} => {Cons (f x) ({Map} a b f xs)}
|
||||
//a b f {Nil} => {Nil}
|
||||
//}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user