20861ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Enough Epic to compile 'hello world' (but not much else yet...)

commit20861ec18945e66eedf25902b2a6afa78e0c3a96 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 15 Oct 2011, 00:14 (15 years ago) parent38a6bc7

10 files changed+90−53

compare with master

unifiedsplit

interp.idr+2−16 lib/prelude.idr+2−1 miniidris.cabal+2−1 src/Core/Evaluate.hs+10−9 src/Idris/AbsSyntax.hs+6−2 src/Idris/ElabDecls.hs+1−1 src/Idris/Parser.hs+7−3 src/Idris/Primitives.hs+57−20 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+1

interp.idr+2−16

@@ -5,32 +5,18 @@ interpTy : Ty -> Set;

55interpTy TyNat = Nat;

66interpTy (TyFun s t) = interpTy s -> interpTy t;

8−data Fin : Nat -> Set where

9− fO : Fin (S k)

10− | fS : Fin k -> Fin (S k);

11−

12−infixr 7 :: ;

13−

14−data Vect : Set -> Nat -> Set where

15− VNil : Vect a O

16− | (::) : a -> Vect a k -> Vect a (S k);

17−

188using (G : Vect Ty n) {

199

2010 data Env : Vect Ty n -> Set where

2111 Empty : Env VNil

2212 | Extend : interpTy a -> Env G -> Env (a :: G);

2313

24− lookup : (i : Fin n) -> Vect a n -> a;

25− lookup fO (x :: xs) = x;

26− lookup (fS k) (x :: xs) = lookup k xs;

27−

28− envLookup : (i : Fin n) -> Env G -> interpTy (lookup i G);

14+ envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);

2915 envLookup fO (Extend x xs) = x;

3016 envLookup (fS i) (Extend x xs) = envLookup i xs;

3117

3218 data Expr : Vect Ty n -> Ty -> Set where

33− Var : (i : Fin n) -> Expr G (lookup i G)

19+ Var : (i : Fin n) -> Expr G (vlookup i G)

3420 | Val : Nat -> Expr G TyNat

3521 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

3622 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

lib/prelude.idr+2−1

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

11import nat;

22import list;

3+import vect;

34import io;

56data Bool = False | True;

@@ -81,7 +82,7 @@ div = prim__divInt;

8182---- some basic io

8283

8384putStr : String -> IO ();

84−putStr = mkForeign (FFun "putStr" (Cons FString Nil) FUnit);

85+putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

8586

8687putStrLn : String -> IO ();

8788putStrLn x = putStr (x ++ "\n");

miniidris.cabal+2−1

@@ -32,7 +32,8 @@ Executable miniidris

3232 Paths_miniidris

3333

3434 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

35− containers, process, transformers, filepath, directory

35+ containers, process, transformers, filepath, directory,

36+ epic

3637

3738 Extensions: MultiParamTypeClasses, FunctionalDependencies,

3839 FlexibleInstances

src/Core/Evaluate.hs+10−9

@@ -56,7 +56,7 @@ eval ctxt genv tm = ev [] tm where

5656 ev env (P Ref n ty) = case lookupDef n ctxt of

5757 Just (Function (Fun _ _ _ v)) -> v

5858 Just (TyDecl nt ty hty) -> VP nt n hty

59− Just (CaseOp _ [] tree) ->

59+ Just (CaseOp _ _ [] tree) ->

6060 case evCase env [] [] tree of

6161 (Nothing, _) -> VP Ref n (ev env ty)

6262 (Just v, _) -> v

@@ -79,7 +79,7 @@ eval ctxt genv tm = ev [] tm where

7979

8080 apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc a) as

8181 apply env (VP Ref n ty) args

82− | Just (CaseOp _ ns tree) <- lookupDef n ctxt

82+ | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt

8383 = case evCase env ns args tree of

8484 (Nothing, _) -> unload env (VP Ref n ty) args

8585 (Just v, rest) -> evApply env rest v

@@ -174,13 +174,13 @@ data Fun = Fun Type Value Term Value

174174data Def = Function Fun

175175 | TyDecl NameType Type Value

176176 | Operator Type Int ([Value] -> Maybe Value)

177− | CaseOp Type [Name] SC

177+ | CaseOp Type [(Term, Term)] [Name] SC

178178

179179instance Show Def where

180180 show (Function f) = "Function: " ++ show f

181181 show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

182182 show (Operator ty _ _) = "Operator: " ++ show ty

183− show (CaseOp ty ns sc) = "Case: " ++ show ns ++ " " ++ show sc

183+ show (CaseOp ty _ ns sc) = "Case: " ++ show ns ++ " " ++ show sc

184184

185185-------

186186

@@ -205,9 +205,10 @@ addDatatype (Data n ty cons) ctxt

205205 addCons (tag+1) cons (addDef n

206206 (TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)

207207

208−addCasedef :: Name -> CaseDef -> Type -> Context -> Context

209−addCasedef n (CaseDef args sc) ty ctxt

210− = addDef n (CaseOp ty args sc) ctxt

208+addCasedef :: Name -> [(Term, Term)] -> Type -> Context -> Context

209+addCasedef n ps ty ctxt

210+ = case simpleCase ps of

211+ CaseDef args sc -> addDef n (CaseOp ty ps args sc) ctxt

211212

212213addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

213214addOperator n ty a op ctxt

@@ -219,7 +220,7 @@ lookupTy n ctxt = do def <- lookupCtxt n ctxt

219220 (Function (Fun ty _ _ _)) -> return ty

220221 (TyDecl _ ty _) -> return ty

221222 (Operator ty _ _) -> return ty

222− (CaseOp ty _ _) -> return ty

223+ (CaseOp ty _ _ _) -> return ty

223224

224225lookupP :: Name -> Context -> Maybe Term

225226lookupP n ctxt

@@ -227,7 +228,7 @@ lookupP n ctxt

227228 case def of

228229 (Function (Fun ty _ tm _)) -> return (P Ref n ty)

229230 (TyDecl nt ty hty) -> return (P nt n ty)

230− (CaseOp ty _ _) -> return (P Ref n ty)

231+ (CaseOp ty _ _ _) -> return (P Ref n ty)

231232 (Operator ty _ _) -> return (P Ref n ty)

232233

233234lookupDef :: Name -> Context -> Maybe Def

src/Idris/AbsSyntax.hs+6−2

@@ -11,6 +11,8 @@ import Data.List

1111import Data.Char

1212import Debug.Trace

1313

14+import qualified Epic.Epic as E

15+

1416data IOption = IOption { opt_logLevel :: Int }

1517 deriving (Show, Eq)

1618

@@ -27,10 +29,11 @@ data IState = IState { tt_ctxt :: Context,

2729 idris_log :: String,

2830 idris_options :: IOption,

2931 idris_name :: Int,

30− imported :: [FilePath]

32+ imported :: [FilePath],

33+ idris_prims :: [(Name, ([E.Name], E.Term))]

3134 }

3235

33−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 []

36+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] []

3437

3538-- The monad for the main REPL - reading and processing files and updating

3639-- global state (hence the IO inner monad).

@@ -83,6 +86,7 @@ iLOG = logLvl 1

8386-- Commands in the REPL

8487

8588data Command = Quit | Help | Eval PTerm

89+ | Compile String

8690 | TTShell

8791 | NOP

8892

src/Idris/ElabDecls.hs+1−1

@@ -67,7 +67,7 @@ elabClauses info n_in cs = let n = liftname info n_in in

6767 logLvl 3 (show tree)

6868 ctxt <- getContext

6969 case lookupTy n ctxt of

70− Just ty -> updateContext (addCasedef n tree ty)

70+ Just ty -> updateContext (addCasedef n (map debind pats) ty)

7171 Nothing -> return ()

7272 where

7373 debind (x, y) = (depat x, depat y)

src/Idris/Parser.hs+7−3

@@ -226,9 +226,13 @@ pHSimpleExpr syn

226226 return $ PHidden e

227227

228228pApp syn = do f <- pSimpleExpr syn

229− iargs <- many (pImplicitArg syn)

230− args <- many1 (pSimpleExpr syn)

231− return (PApp f (iargs ++ map PExp args))

229+ args <- many1 (pArg syn)

230+ return (PApp f args)

231+

232+pArg :: SyntaxInfo -> IParser PArg

233+pArg syn = pImplicitArg syn

234+ <|> do e <- pSimpleExpr syn

235+ return (PExp e)

232236

233237pImplicitArg syn = do lchar '{'; n <- iName

234238 v <- option (PRef n) (do lchar '='; pExpr syn)

src/Idris/Primitives.hs+57−20

@@ -1,3 +1,5 @@

1+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}

13module Idris.Primitives(elabPrims) where

35import Idris.ElabDecls

@@ -6,35 +8,67 @@ import Idris.AbsSyntax

68import Core.TT

79import Core.Evaluate

810

11+import Epic.Epic hiding (Term, Type, Name, fn)

12+import qualified Epic.Epic as E

13+

914data Prim = Prim { p_name :: Name,

1015 p_type :: Type,

1116 p_arity :: Int,

12− p_def :: [Value] -> Maybe Value

17+ p_def :: [Value] -> Maybe Value,

18+ p_epic :: ([E.Name], E.Term)

1319 }

1420

1521ty [] x = Constant x

1622ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

1723

24+type ETm = E.Term

25+type EOp = E.Op

26+

27+fun = E.fn

28+ref = E.ref

29+

30+eOp :: EOp -> ([E.Name], ETm)

31+eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))

32+

1833primitives =

19− [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+)),

20− Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-)),

21− Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*)),

22− Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div)),

23− Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==)),

24− Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<)),

25− Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=)),

26− Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>)),

27− Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=)),

28− Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+)),

29− Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-)),

30− Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*)),

31− Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/)),

32− Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==)),

33− Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),

34− Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),

35− Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>)),

36− Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=)),

34+ [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))

35+ (eOp E.plus_),

36+ Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))

37+ (eOp E.minus_),

38+ Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*))

39+ (eOp E.times_),

40+ Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div))

41+ (eOp E.divide_),

42+ Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==))

43+ (eOp E.eq_),

44+ Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<))

45+ (eOp E.lt_),

46+ Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=))

47+ (eOp E.lte_),

48+ Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>))

49+ (eOp E.gt_),

50+ Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=))

51+ (eOp E.gte_),

52+ Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+))

53+ (eOp E.plusF_),

54+ Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-))

55+ (eOp E.minusF_),

56+ Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*))

57+ (eOp E.timesF_),

58+ Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/))

59+ (eOp E.divideF_),

60+ Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==))

61+ (eOp E.eqF_),

62+ Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<))

63+ (eOp E.ltF_),

64+ Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=))

65+ (eOp E.lteF_),

66+ Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>))

67+ (eOp E.gtF_),

68+ Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))

69+ (eOp E.gteF_),

3770 Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))

71+ ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")

3872 ]

3973

4074iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

@@ -53,7 +87,10 @@ sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

5387sBin _ _ = Nothing

5488

5589elabPrim :: Prim -> Idris ()

56−elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

90+elabPrim (Prim n ty i def epic)

91+ = do updateContext (addOperator n ty i def)

92+ i <- getIState

93+ putIState i { idris_prims = (n, epic) : idris_prims i }

5794

5895elabPrims :: Idris ()

5996elabPrims = do mapM_ (elabDecl toplevel)

src/Idris/REPL.hs+2

@@ -7,6 +7,7 @@ import Idris.REPLParser

77import Idris.ElabDecls

88import Idris.Error

99import Idris.Delaborate

10+import Idris.Compiler

1011

1112import Core.Evaluate

1213import Core.ProofShell

@@ -52,5 +53,6 @@ process TTShell = do ist <- get

5253 let shst = initState (tt_ctxt ist)

5354 shst' <- lift $ runShell shst

5455 return ()

56+process (Compile f) = do compile f

5557process NOP = return ()

5658

src/Idris/REPLParser.hs+1

@@ -22,5 +22,6 @@ pCmd :: IParser Command

2222pCmd = try (do cmd ["q", "quit"]; return Quit)

2323 <|> try (do cmd ["h", "?", "help"]; return Help)

2424 <|> try (do cmd ["ttshell"]; return TTShell)

25+ <|> try (do cmd ["c", "compile"]; f <- identifier; return (Compile f))

2526 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

2627 <|> do eof; return NOP