git.iko.soy/Idris-dev
on master help sign in
Some proof state, some showing of terms
205fcefEdwin Brady
impl-paper/intro.tex+9−8
compare with master
unifiedsplit
@@ -1,12 +1,13 @@
1\section{Introduction}
1\section{Introduction}
2
2
3−This paper documents a new implementation of \Idris{}~\cite{plpv11},
3+This paper documents a new implementation of \Idris{}~\cite{plpv11}, in which
4−in which I attempt to learn from the mistakes of the previous
4+I attempt to learn from the mistakes of the previous implementation and make
5−implementation and make it nice and clean and solid. Maybe I'll keep
5+it nice and clean and solid. Maybe I'll keep it up to date as I write the
6−it up to date as I write the code.
6+code.
7
7
8The title is deliberately a reordering of the words in my thesis
8The title is deliberately a reordering of the words in my thesis
9−title~\cite{brady-thesis}. Whereas that was about taking elaborated
9+title~\cite{brady-thesis}. Whereas that was about taking elaborated programs
10−programs in the core type theory of \Epigram{}~\cite{view-left} and
10+in the core type theory of \Epigram{}~\cite{view-left} and compiling them
11−compiling them efficiently (i.e. making the language implementation
11+efficiently (i.e. making the language implementation practical) this paper is
12−practical) this paper is about making the language itself practical.
12+about making the language itself practical.
13+
impl-paper/overview.tex+6−1
@@ -7,5 +7,10 @@ High level view of steps we've taken to implement this new version:
7\item An evaluator for well-typed terms
7\item An evaluator for well-typed terms
8\item The important bit: a simple type checker. No unification or
8\item The important bit: a simple type checker. No unification or
9 inference.
9 inference.
10−\item The proof state and a tactic engine.
10+\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).
11\end{itemize}
11\end{itemize}
12+
13+For the high level language: we need nothing more than the core type theory,
14+and a way of putting stuff together. So we typecheck each pattern match clause
15+individually, in an appropriate context. There is no need for the core type
16+theory to have pattern matching.
src/Core.hs+33−4
@@ -1,8 +1,9 @@
1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
2
2
3module Core where
3module Core where
4
4
5import Control.Monad.State
5import Control.Monad.State
6+import Debug.Trace
6
7
7{- The language has:
8{- The language has:
8 * Full dependent types
9 * Full dependent types
@@ -29,7 +30,12 @@ data Option = SetInSet
29
30
30data Name = UN [String]
31data Name = UN [String]
31 | MN Int String
32 | MN Int String
32− deriving (Show, Eq)
33+ deriving Eq
34+
35+instance 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 ++ "}"
33
39
34data Raw = Var Name
40data Raw = Var Name
35 | RBind Name (Binder Raw) Raw
41 | RBind Name (Binder Raw) Raw
@@ -45,7 +51,7 @@ data Binder b = Lam { binderTy :: b }
45 | Guess { binderTy :: b,
51 | Guess { binderTy :: b,
46 binderVal :: b }
52 binderVal :: b }
47 | PVar { binderTy :: b }
53 | PVar { binderTy :: b }
48− deriving (Show, Eq)
54+ deriving (Show, Eq, Functor)
49
55
50data RawFun = RawFun { rtype :: Raw,
56data RawFun = RawFun { rtype :: Raw,
51 rval :: Raw
57 rval :: Raw
@@ -68,7 +74,7 @@ data TT n = P NameType n (TT n) -- embed type
68 | Bind n (Binder (TT n)) (TT n)
74 | Bind n (Binder (TT n)) (TT n)
69 | App (TT n) (TT n) (TT n) -- function, function type, arg
75 | App (TT n) (TT n) (TT n) -- function, function type, arg
70 | Set Int
76 | Set Int
71− deriving (Show, Eq)
77+ deriving Eq
72
78
73type EnvTT n = [(n, Binder (TT n))]
79type EnvTT n = [(n, Binder (TT n))]
74
80
@@ -81,6 +87,29 @@ type Type = Term
81
87
82type Env = EnvTT Name
88type Env = EnvTT Name
83
89
90+instance 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
98+
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
105+
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
109+
110+ bracket outer inner str | inner > outer = "(" ++ str ++ ")"
111+ | otherwise = str
112+
84-- WELL TYPED TERMS AS HOAS -------------------------------------------------
113-- WELL TYPED TERMS AS HOAS -------------------------------------------------
85
114
86data HTT = HP NameType Name HTT
115data HTT = HP NameType Name HTT
src/Evaluate.hs+16−4
@@ -5,18 +5,30 @@ module Evaluate(normalise) where
5import Debug.Trace
5import Debug.Trace
6import Core
6import Core
7
7
8−normalise :: Context -> TT Name -> TT Name
8+normalise :: Context -> Env -> TT Name -> TT Name
9−normalise ctxt t = quote 0 (eval ctxt (hoas [] t))
9+normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))
10+
11+type HEnv = [(Name, Binder HTT)]
12+
13+evalEnv :: Env -> HEnv
14+evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))
10
15
11-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
16-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
12-- level things, so, if we remove a binder, we need to strengthen the
17-- level things, so, if we remove a binder, we need to strengthen the
13-- indices appropriately.
18-- indices appropriately.
14
19
15−eval :: Context -> HTT -> HTT
20+eval :: Context -> HEnv -> HTT -> HTT
16−eval ctxt t = ev t where
21+eval ctxt env t = ev t where
17 ev (HP Ref n ty)
22 ev (HP Ref n ty)
18 | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
23 | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
19 ev (HP nt n ty) = HP nt n (ev ty)
24 ev (HP nt n ty) = HP nt n (ev ty)
25+{-
26+ ev (HV i)
27+ | i < length env = case env!! i of
28+ (n, Let t v) -> ev v
29+ _ -> HV i
30+ | otherwise = HV i
31+-}
20 ev (HApp f t a)
32 ev (HApp f t a)
21 = evSpine f [(a, t)]
33 = evSpine f [(a, t)]
22 where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)
34 where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)
src/Main.hs+1
@@ -1,5 +1,6 @@
1module Main where
1module Main where
2
2
3import Typecheck
3import Typecheck
4+import ProofState
4
5
5main = putStrLn "Nothing Happens"
6main = putStrLn "Nothing Happens"
src/Parser.hs+4
@@ -64,6 +64,10 @@ pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm
64 symbol "=>";
64 symbol "=>";
65 sc <- pTerm
65 sc <- pTerm
66 return (RBind (UN [x]) (Lam ty) sc)
66 return (RBind (UN [x]) (Lam ty) sc)
67+ <|> try (do lchar '?'; x <- identifier; lchar ':'; ty <- pTerm
68+ lchar '.';
69+ sc <- pTerm
70+ return (RBind (UN [x]) (Lam ty) sc))
67 <|> try (do lchar '(';
71 <|> try (do lchar '(';
68 x <- identifier; lchar ':'; ty <- pTerm
72 x <- identifier; lchar ':'; ty <- pTerm
69 lchar ')';
73 lchar ')';
src/ProofState.hs+53
@@ -5,4 +5,57 @@ module ProofState where
5import Typecheck
5import Typecheck
6import Evaluate
6import Evaluate
7import Core
7import Core
8+import Control.Monad.State
9+
10+data ProofState = PS { holes :: [Name], -- holes still to be solved
11+ nextname :: Int, -- name supply
12+ pterm :: Term -- current proof term
13+ }
14+
15+data Goal = GD { premises :: Env,
16+ goalType :: Term
17+ }
18+
19+data TacticAction = AddGoal Name
20+
21+type Tactic = Context -> Env -> Term -> StateT [TacticAction] TC Term
22+type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
23+
24+goal :: Hole -> Term -> Context -> TC Goal
25+goal h tm ctxt = g [] tm where
26+ g env (Bind n b sc) | hole b && same h n = return $ GD env (binderTy b)
27+ | otherwise = gb env b `mplus` g ((n,b):env) sc
28+ g env (App f t a) = g env f `mplus` g env t `mplus` g env a
29+ g env t = Error "Can't find hole"
30+
31+ gb env (Let t v) = g env t `mplus` g env v
32+ gb env (Guess t v) = g env t `mplus` g env v
33+ gb env t = g env (binderTy t)
34+
35+tactic :: Hole -> Term -> Context -> Tactic -> StateT [TacticAction] TC Term
36+tactic h tm ctxt f = atH [] tm where
37+ atH env binder@(Bind n b sc)
38+ | hole b && same h n = f ctxt env binder
39+ | otherwise = do b' <- atHb env b
40+ sc' <- atH ((n,b):env) sc
41+ return (Bind n b' sc')
42+ atH env (App f t a) = do f' <- atH env t; t' <- atH env t; a' <- atH env a
43+ return (App f' t' a')
44+ atH env t = do return t
45+
46+ atHb env (Let t v) = do t' <- atH env t
47+ v' <- atH env v
48+ return $ Let t' v'
49+ atHb env (Guess t v) = do t' <- atH env t
50+ v' <- atH env v
51+ return $ Let t' v'
52+ atHb env t = do ty' <- atH env (binderTy t)
53+ return $ t { binderTy = ty' }
54+
55+same Nothing n = True
56+same (Just x) n = x == n
57+
58+hole (Hole _) = True
59+hole (Guess _ _) = True
60+
8
61
src/Typecheck.hs+23−17
@@ -22,9 +22,15 @@ instance Monad TC where
22 Error e -> Error e
22 Error e -> Error e
23 fail = Error
23 fail = Error
24
24
25+instance MonadPlus TC where
26+ mzero = Error "Unknown error"
27+ (OK x) `mplus` _ = OK x
28+ _ `mplus` (OK y) = OK y
29+ err `mplus` _ = err
30+
25converts :: Context -> Env -> Term -> Term -> TC ()
31converts :: Context -> Env -> Term -> Term -> TC ()
26−converts ctxt env x y = if (normalise ctxt (bindEnv env x) ==
32+converts ctxt env x y = if (normalise ctxt env (bindEnv env x) ==
27− normalise ctxt (bindEnv env y))
33+ normalise ctxt env (bindEnv env y))
28 then return ()
34 then return ()
29 else fail ("Can't convert between " ++
35 else fail ("Can't convert between " ++
30 show x ++ " and " ++ show y)
36 show x ++ " and " ++ show y)
@@ -41,12 +47,12 @@ check ctxt env (Var n)
41check ctxt env (RApp f a)
47check ctxt env (RApp f a)
42 = do (fv, fty) <- check ctxt env f
48 = do (fv, fty) <- check ctxt env f
43 (av, aty) <- check ctxt env a
49 (av, aty) <- check ctxt env a
44− let fty' = normalise ctxt fty
50+ let fty' = normalise ctxt env fty
45 case fty' of
51 case fty' of
46 Bind x (Pi s) t ->
52 Bind x (Pi s) t ->
47 do converts ctxt env s aty
53 do converts ctxt env s aty
48 return (App fv fty av,
54 return (App fv fty av,
49− normalise ctxt (Bind x (Let av aty) t))
55+ normalise ctxt env (Bind x (Let av aty) t))
50 t -> fail "Can't apply a non-function type"
56 t -> fail "Can't apply a non-function type"
51check ctxt env (RSet i) = return (Set i, Set (i+1))
57check ctxt env (RSet i) = return (Set i, Set (i+1))
52check ctxt env (RBind n b sc)
58check ctxt env (RBind n b sc)
@@ -55,42 +61,42 @@ check ctxt env (RBind n b sc)
55 discharge n b' scv sct
61 discharge n b' scv sct
56 where checkBinder (Lam t)
62 where checkBinder (Lam t)
57 = do (tv, tt) <- check ctxt env t
63 = do (tv, tt) <- check ctxt env t
58− let tv' = normalise ctxt tv
64+ let tv' = normalise ctxt env tv
59− let tt' = normalise ctxt tt
65+ let tt' = normalise ctxt env tt
60 isSet tt'
66 isSet tt'
61 return (Lam tv')
67 return (Lam tv')
62 checkBinder (Pi t)
68 checkBinder (Pi t)
63 = do (tv, tt) <- check ctxt env t
69 = do (tv, tt) <- check ctxt env t
64− let tv' = normalise ctxt tv
70+ let tv' = normalise ctxt env tv
65− let tt' = normalise ctxt tt
71+ let tt' = normalise ctxt env tt
66 isSet tt'
72 isSet tt'
67 return (Pi tv')
73 return (Pi tv')
68 checkBinder (Let t v)
74 checkBinder (Let t v)
69 = do (tv, tt) <- check ctxt env t
75 = do (tv, tt) <- check ctxt env t
70 (vv, vt) <- check ctxt env v
76 (vv, vt) <- check ctxt env v
71− let tv' = normalise ctxt tv
77+ let tv' = normalise ctxt env tv
72− let tt' = normalise ctxt tt
78+ let tt' = normalise ctxt env tt
73 converts ctxt env tv vt
79 converts ctxt env tv vt
74 isSet tt'
80 isSet tt'
75 return (Let tv' vv)
81 return (Let tv' vv)
76 checkBinder (Hole t)
82 checkBinder (Hole t)
77 = do (tv, tt) <- check ctxt env t
83 = do (tv, tt) <- check ctxt env t
78− let tv' = normalise ctxt tv
84+ let tv' = normalise ctxt env tv
79− let tt' = normalise ctxt tt
85+ let tt' = normalise ctxt env tt
80 isSet tt'
86 isSet tt'
81 return (Hole tv')
87 return (Hole tv')
82 checkBinder (Guess t v)
88 checkBinder (Guess t v)
83 = do (tv, tt) <- check ctxt env t
89 = do (tv, tt) <- check ctxt env t
84 (vv, vt) <- check ctxt env v
90 (vv, vt) <- check ctxt env v
85− let tv' = normalise ctxt tv
91+ let tv' = normalise ctxt env tv
86− let tt' = normalise ctxt tt
92+ let tt' = normalise ctxt env tt
87 converts ctxt env tv vt
93 converts ctxt env tv vt
88 isSet tt'
94 isSet tt'
89 return (Guess tv' vv)
95 return (Guess tv' vv)
90 checkBinder (PVar t)
96 checkBinder (PVar t)
91 = do (tv, tt) <- check ctxt env t
97 = do (tv, tt) <- check ctxt env t
92− let tv' = normalise ctxt tv
98+ let tv' = normalise ctxt env tv
93− let tt' = normalise ctxt tt
99+ let tt' = normalise ctxt env tt
94 isSet tt'
100 isSet tt'
95 return (PVar tv')
101 return (PVar tv')
96
102
@@ -131,4 +137,4 @@ checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
131 isSet tyt'
137 isSet tyt'
132 converts ctxt [] ty' valt'
138 converts ctxt [] ty' valt'
133 checkProgram ((n, Function (Fun ty' (hoas [] ty')
139 checkProgram ((n, Function (Fun ty' (hoas [] ty')
134− val' (hoas [] val'))):ctxt) xs
140+ val' (hoas [] val'))):ctxt) xs
src/test.mi+2
@@ -9,3 +9,5 @@ three : N = S two;
9Vect : (A:Set 0) -> (n:N) -> Set 0;
9Vect : (A:Set 0) -> (n:N) -> Set 0;
10Nil : (A:Set 0) -> (Vect A O);
10Nil : (A:Set 0) -> (Vect A O);
11Cons : (A:Set 0) -> (k:N) -> (Vect A k) -> (Vect A (S k));
11Cons : (A:Set 0) -> (k:N) -> (Vect A k) -> (Vect A (S k));
12+
13+vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);