Steve Dunham
f3a18fa658
Sometimes a Bound variable on the LHS became Defined to itself. This commit also resurfaces INFO messages, to aid finding the root cause of errors.
76 lines
3.2 KiB
Agda
76 lines
3.2 KiB
Agda
module WellTyped
|
|
|
|
-- Idris2's "Well Typed Interpreter" example
|
|
-- This is a little painful for lack of overloading.
|
|
-- I can add idris/haskell style sections.
|
|
-- This is revealing some issues. :/
|
|
|
|
-- I had to put {0 ctxt : Vect n Ty} → in manually, the `∀ ctxt` wasn't inferring the type.
|
|
-- This may be because we have `n`, which becomes a parameter when do it manually.
|
|
-- That would explain why Idris adds those...
|
|
|
|
-- This also revealed an issue in case tree building where a bound name was accidentally made into a defined one.
|
|
|
|
import Prelude
|
|
import Data.Vect
|
|
import Data.Fin
|
|
|
|
data Ty = TyInt | TyBool | TyFun Ty Ty
|
|
|
|
interpTy : Ty → U
|
|
interpTy TyInt = Int
|
|
interpTy TyBool = Bool
|
|
interpTy (TyFun x y) = interpTy x → interpTy y
|
|
|
|
data HasType : ∀ n. (i : Fin n) → Vect n Ty → Ty → U where
|
|
Stop : ∀ t n. {0 ctxt : Vect n Ty} → HasType FZ (t :- ctxt) t
|
|
Pop : ∀ n t u. {0 ctxt : Vect n Ty} {0 k : Fin n} → HasType k ctxt t → HasType (FS k) (u :- ctxt) t
|
|
|
|
data Expr : ∀ n. Vect n Ty → Ty → U where
|
|
Var : ∀ t n. {0 ctxt : Vect n Ty} {0 i : Fin n} → HasType i ctxt t → Expr ctxt t
|
|
Val : ∀ n. {0 ctxt : Vect n Ty} → (x : Int) → Expr ctxt TyInt
|
|
Lam : ∀ a n t. {0 ctxt : Vect n Ty} → Expr (a :- ctxt) t → Expr ctxt (TyFun a t)
|
|
App : ∀ n a t. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun a t) → Expr ctxt a → Expr ctxt t
|
|
Op : ∀ a b c n. {0 ctxt : Vect n Ty} → (interpTy a → interpTy b → interpTy c) →
|
|
Expr ctxt a → Expr ctxt b → Expr ctxt c
|
|
-- TODO Idris has Lazy on the arms, should work if we explicitly force
|
|
If : ∀ n a. {0 ctxt : Vect n Ty} → Expr ctxt TyBool →
|
|
(Expr ctxt a) →
|
|
(Expr ctxt a) → Expr ctxt a
|
|
|
|
infixr 4 _:::_
|
|
data Env : ∀ n. Vect n Ty → U where
|
|
Empty : Env VNil
|
|
_:::_ : ∀ a n. {0 ctxt : Vect n Ty} → interpTy a → Env ctxt → Env (a :- ctxt)
|
|
|
|
lookup : ∀ n t. {0 ctxt : Vect n Ty} {0 i : Fin n} → HasType i ctxt t → Env ctxt → interpTy t
|
|
lookup Stop (x ::: xs) = x
|
|
lookup () Empty
|
|
lookup (Pop k) (x ::: xs) = lookup k xs
|
|
|
|
interp : ∀ n t. {0 ctxt : Vect n Ty} → Env ctxt → Expr ctxt t → interpTy t
|
|
interp env (Var i) = lookup i env
|
|
interp env (Val x) = x
|
|
interp env (Lam x) = \y => interp (y ::: env) x
|
|
interp env (App x y) = interp env x $ interp env y
|
|
interp env (Op f x y) = f (interp env x) (interp env y)
|
|
interp env (If x y z) = if interp env x then interp env y
|
|
else interp env z
|
|
|
|
add : ∀ n. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
|
|
add = Lam (Lam (Op _+_ (Var Stop) (Var (Pop Stop))))
|
|
|
|
fact : ∀ n. {0 ctxt : Vect n Ty} → Expr ctxt (TyFun TyInt TyInt)
|
|
-- TODO the `Bool =?= interpTy ...` is stuck on ?m14
|
|
-- I think we may need to need to delay the constraint until m14 is solved?
|
|
-- But I think I have code to do that already
|
|
fact = Lam (If (Op {_} {_} {TyBool} _==_ (Var Stop) (Val 0))
|
|
(Val 1)
|
|
(Op _*_ (App fact (Op _-_ (Var Stop) (Val 1)))
|
|
(Var Stop)))
|
|
|
|
-- main : IO Unit
|
|
-- main = do putStr "Enter a number: "
|
|
-- Right x <- readLine | _ => putStrLn "EOF"
|
|
-- printLn (interp Empty fact (stringToInt x))
|