git.iko.soy/Idris-dev
on 6923ac1 help sign in
Idris-dev/src/Core.hs
182 lines 5.7 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
3module Core where
5import Control.Monad.State
6import Debug.Trace
8{- The language has:
9 * Full dependent types
10 * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
11 * Pattern matching letrec binding
12 * (primitive types defined externally)
14 Some technical stuff:
15 * Typechecker is kept as simple as possible
16 - no unification, just a checker for incomplete terms.
17 * We have a simple collection of tactics which we use to elaborate source
18 programs with implicit syntax into fully explicit terms.
19-}
21data Option = SetInSet
22 | CheckConv
23 deriving Eq
25-- RAW TERMS ----------------------------------------------------------------
27-- Names are hierarchies of strings, describing scope (so no danger of
28-- duplicate names, but need to be careful on lookup).
29-- Also MN for machine chosen names
31data Name = UN [String]
32 | MN Int String
33 deriving Eq
35instance Show Name where
36 show (UN [n]) = n
37 show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)
38 show (MN i s) = "{" ++ s ++ show i ++ "}"
40data Raw = Var Name
41 | RBind Name (Binder Raw) Raw
42 | RApp Raw Raw
43 | RSet Int
44 deriving Show
46data Binder b = Lam { binderTy :: b }
47 | Pi { binderTy :: b }
48 | Let { binderTy :: b,
49 binderVal :: b }
50 | Hole { binderTy :: b}
51 | Guess { binderTy :: b,
52 binderVal :: b }
53 | PVar { binderTy :: b }
54 deriving (Show, Eq, Functor)
56data RawFun = RawFun { rtype :: Raw,
57 rval :: Raw
58 }
59 deriving Show
61data RDef = RFunction RawFun
62 | RConst Raw
63 deriving Show
65type RProgram = [(Name, RDef)]
67-- WELL TYPED TERMS ---------------------------------------------------------
69data NameType = Ref | DCon Int Int | TCon Int
70 deriving (Show, Eq)
72data TT n = P NameType n (TT n) -- embed type
73 | V Int
74 | Bind n (Binder (TT n)) (TT n)
75 | App (TT n) (TT n) (TT n) -- function, function type, arg
76 | Set Int
77 deriving (Functor, Eq)
79type EnvTT n = [(n, Binder (TT n))]
81bindEnv :: EnvTT n -> TT n -> TT n
82bindEnv [] tm = tm
83bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
85type Term = TT Name
86type Type = Term
88type Env = EnvTT Name
90instance Show n => Show (TT n) where
91 show t = se 10 [] t where
92 se p env (P _ n _) = show n
93 se p env (V i) | i < length env = show $ fst $ env!!i
94 | otherwise = "!!V " ++ show i ++ "!!"
95 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
96 se p env (App f t a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
97 se p env (Set i) = "Set" ++ show i
99 sb env n (Lam t) = showb env "\\ " " => " n t
100 sb env n (Hole t) = showb env "? " ". " n t
101 sb env n (Pi t) = showb env "forall " " -> " n t
102 sb env n (PVar t) = showb env "! " ". " n t
103 sb env n (Let t v) = showbv env "let " " in " n t v
104 sb env n (Guess t v) = showbv env "?? " " in " n t v
106 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
107 showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
108 se 10 env v ++ sc
110 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
111 | otherwise = str
113-- WELL TYPED TERMS AS HOAS -------------------------------------------------
115data HTT = HP NameType Name HTT
116 | HV Int
117 | HBind Name (Binder HTT) (HTT -> HTT)
118 | HApp HTT HTT HTT
119 | HSet Int
120 | HTmp Int
122instance Show HTT where
123 show h = "<<HOAS>>"
125hoas :: [HTT] -> TT Name -> HTT
126hoas env (P nt n ty) = HP nt n (hoas env ty)
127hoas env (V i) | i < length env = env!!i
128 | otherwise = HV i
129hoas env (Bind n b sc) = HBind n (hbind b) (\x -> hoas (x:env) sc)
130 where hbind (Lam t) = Lam (hoas env t)
131 hbind (Pi t) = Pi (hoas env t)
132 hbind (Hole t) = Hole (hoas env t)
133 hbind (PVar t) = PVar (hoas env t)
134 hbind (Let v t) = Let (hoas env v) (hoas env t)
135 hbind (Guess v t) = Guess (hoas env v) (hoas env t)
136hoas env (App f t a) = HApp (hoas env f) (hoas env t) (hoas env a)
137hoas env (Set i) = HSet i
139-- CONTEXTS -----------------------------------------------------------------
141data Fun = Fun Type HTT Term HTT
142 deriving Show
144data Def = Function Fun
145 | Constant NameType Type HTT
146 deriving Show
148type Context = [(Name, Def)]
150emptyContext = []
152lookupTy :: Name -> Context -> Maybe Type
153lookupTy n ctxt = do def <- lookup n ctxt
154 case def of
155 (Function (Fun ty _ _ _)) -> return ty
156 (Constant _ ty _) -> return ty
158lookupP :: Name -> Context -> Maybe Term
159lookupP n ctxt
160 = do def <- lookup n ctxt
161 case def of
162 (Function (Fun ty _ tm _)) -> return (P Ref n ty)
163 (Constant nt ty hty) -> return (P nt n ty)
165lookupVal :: Name -> Context -> Maybe HTT
166lookupVal n ctxt
167 = do def <- lookup n ctxt
168 case def of
169 (Function (Fun _ _ _ htm)) -> return htm
170 (Constant nt ty hty) -> return (HP nt n hty)
172lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
173lookupTyEnv n env = li n 0 env where
174 li n i [] = Nothing
175 li n i ((x, b): xs)
176 | n == x = Just (i, binderTy b)
177 | otherwise = li n (i+1) xs
180x = UN ["x"]
181xt = UN ["X"]
182testtm = RBind xt (Lam (RSet 0)) (RBind x (Lam (Var xt)) (Var x))