205fcef · Idris-dev · git.iko.soy

impl-paper/intro.tex+9−8

@@ -1,12 +1,13 @@

11\section{Introduction}

22

3−This paper documents a new implementation of \Idris{}~\cite{plpv11},

4−in which I attempt to learn from the mistakes of the previous

5−implementation and make it nice and clean and solid. Maybe I'll keep

6−it up to date as I write the code.

3+This paper documents a new implementation of \Idris{}~\cite{plpv11}, in which

4+I attempt to learn from the mistakes of the previous implementation and make

5+it nice and clean and solid. Maybe I'll keep it up to date as I write the

6+code.

77

88The title is deliberately a reordering of the words in my thesis

9−title~\cite{brady-thesis}. Whereas that was about taking elaborated

10−programs in the core type theory of \Epigram{}~\cite{view-left} and

11−compiling them efficiently (i.e. making the language implementation

12−practical) this paper is about making the language itself practical.

9+title~\cite{brady-thesis}. Whereas that was about taking elaborated programs

10+in the core type theory of \Epigram{}~\cite{view-left} and compiling them

11+efficiently (i.e. making the language implementation practical) this paper is

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:

77\item An evaluator for well-typed terms

88\item The important bit: a simple type checker. No unification or

99 inference.

10−\item The proof state and a tactic engine.

10+\item The proof state and a tactic engine (Oleg style~\cite{mcbride-thesis}).

1111\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 #-}

22

33module Core where

44

55import Control.Monad.State

6+import Debug.Trace

67

78{- The language has:

89 * Full dependent types

@@ -29,7 +30,12 @@ data Option = SetInSet

2930

3031data Name = UN [String]

3132 | 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 ++ "}"

3339

3440data Raw = Var Name

3541 | RBind Name (Binder Raw) Raw

@@ -45,7 +51,7 @@ data Binder b = Lam { binderTy :: b }

4551 | Guess { binderTy :: b,

4652 binderVal :: b }

4753 | PVar { binderTy :: b }

48− deriving (Show, Eq)

54+ deriving (Show, Eq, Functor)

4955

5056data RawFun = RawFun { rtype :: Raw,

5157 rval :: Raw

@@ -68,7 +74,7 @@ data TT n = P NameType n (TT n) -- embed type

6874 | Bind n (Binder (TT n)) (TT n)

6975 | App (TT n) (TT n) (TT n) -- function, function type, arg

7076 | Set Int

71− deriving (Show, Eq)

77+ deriving Eq

7278

7379type EnvTT n = [(n, Binder (TT n))]

7480

@@ -81,6 +87,29 @@ type Type = Term

8187

8288type Env = EnvTT Name

8389

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+

84113-- WELL TYPED TERMS AS HOAS -------------------------------------------------

85114

86115data HTT = HP NameType Name HTT

src/Evaluate.hs+16−4

@@ -5,18 +5,30 @@ module Evaluate(normalise) where

55import Debug.Trace

66import Core

77

8−normalise :: Context -> TT Name -> TT Name

9−normalise ctxt t = quote 0 (eval ctxt (hoas [] t))

8+normalise :: Context -> Env -> TT Name -> TT Name

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))

1015

1116-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher

1217-- level things, so, if we remove a binder, we need to strengthen the

1318-- indices appropriately.

1419

15−eval :: Context -> HTT -> HTT

16−eval ctxt t = ev t where

20+eval :: Context -> HEnv -> HTT -> HTT

21+eval ctxt env t = ev t where

1722 ev (HP Ref n ty)

1823 | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling

1924 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+-}

2032 ev (HApp f t a)

2133 = evSpine f [(a, t)]

2234 where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)

src/Main.hs+1

@@ -1,5 +1,6 @@

11module Main where

22

33import Typecheck

4+import ProofState

45

56main = putStrLn "Nothing Happens"

src/Parser.hs+4

@@ -64,6 +64,10 @@ pExp = do lchar '\\'; x <- identifier; lchar ':'; ty <- pTerm

6464 symbol "=>";

6565 sc <- pTerm

6666 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))

6771 <|> try (do lchar '(';

6872 x <- identifier; lchar ':'; ty <- pTerm

6973 lchar ')';

src/ProofState.hs+53

@@ -5,4 +5,57 @@ module ProofState where

55import Typecheck

66import Evaluate

77import 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+

861

src/Typecheck.hs+23−17

@@ -22,9 +22,15 @@ instance Monad TC where

2222 Error e -> Error e

2323 fail = Error

2424

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+

2531converts :: Context -> Env -> Term -> Term -> TC ()

26−converts ctxt env x y = if (normalise ctxt (bindEnv env x) ==

27− normalise ctxt (bindEnv env y))

32+converts ctxt env x y = if (normalise ctxt env (bindEnv env x) ==

33+ normalise ctxt env (bindEnv env y))

2834 then return ()

2935 else fail ("Can't convert between " ++

3036 show x ++ " and " ++ show y)

@@ -41,12 +47,12 @@ check ctxt env (Var n)

4147check ctxt env (RApp f a)

4248 = do (fv, fty) <- check ctxt env f

4349 (av, aty) <- check ctxt env a

44− let fty' = normalise ctxt fty

50+ let fty' = normalise ctxt env fty

4551 case fty' of

4652 Bind x (Pi s) t ->

4753 do converts ctxt env s aty

4854 return (App fv fty av,

49− normalise ctxt (Bind x (Let av aty) t))

55+ normalise ctxt env (Bind x (Let av aty) t))

5056 t -> fail "Can't apply a non-function type"

5157check ctxt env (RSet i) = return (Set i, Set (i+1))

5258check ctxt env (RBind n b sc)

@@ -55,42 +61,42 @@ check ctxt env (RBind n b sc)

5561 discharge n b' scv sct

5662 where checkBinder (Lam t)

5763 = do (tv, tt) <- check ctxt env t

58− let tv' = normalise ctxt tv

59− let tt' = normalise ctxt tt

64+ let tv' = normalise ctxt env tv

65+ let tt' = normalise ctxt env tt

6066 isSet tt'

6167 return (Lam tv')

6268 checkBinder (Pi t)

6369 = do (tv, tt) <- check ctxt env t

64− let tv' = normalise ctxt tv

65− let tt' = normalise ctxt tt

70+ let tv' = normalise ctxt env tv

71+ let tt' = normalise ctxt env tt

6672 isSet tt'

6773 return (Pi tv')

6874 checkBinder (Let t v)

6975 = do (tv, tt) <- check ctxt env t

7076 (vv, vt) <- check ctxt env v

71− let tv' = normalise ctxt tv

72− let tt' = normalise ctxt tt

77+ let tv' = normalise ctxt env tv

78+ let tt' = normalise ctxt env tt

7379 converts ctxt env tv vt

7480 isSet tt'

7581 return (Let tv' vv)

7682 checkBinder (Hole t)

7783 = do (tv, tt) <- check ctxt env t

78− let tv' = normalise ctxt tv

79− let tt' = normalise ctxt tt

84+ let tv' = normalise ctxt env tv

85+ let tt' = normalise ctxt env tt

8086 isSet tt'

8187 return (Hole tv')

8288 checkBinder (Guess t v)

8389 = do (tv, tt) <- check ctxt env t

8490 (vv, vt) <- check ctxt env v

85− let tv' = normalise ctxt tv

86− let tt' = normalise ctxt tt

91+ let tv' = normalise ctxt env tv

92+ let tt' = normalise ctxt env tt

8793 converts ctxt env tv vt

8894 isSet tt'

8995 return (Guess tv' vv)

9096 checkBinder (PVar t)

9197 = do (tv, tt) <- check ctxt env t

92− let tv' = normalise ctxt tv

93− let tt' = normalise ctxt tt

98+ let tv' = normalise ctxt env tv

99+ let tt' = normalise ctxt env tt

94100 isSet tt'

95101 return (PVar tv')

96102

@@ -131,4 +137,4 @@ checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)

131137 isSet tyt'

132138 converts ctxt [] ty' valt'

133139 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;

99Vect : (A:Set 0) -> (n:N) -> Set 0;

1010Nil : (A:Set 0) -> (Vect A O);

1111Cons : (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);