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

interp.idr+2−16

compare with master

unifiedsplit

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

5interpTy TyNat = Nat;

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

7

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−

18using (G : Vect Ty n) {

8using (G : Vect Ty n) {

19

9

20 data Env : Vect Ty n -> Set where

10 data Env : Vect Ty n -> Set where

21 Empty : Env VNil

11 Empty : Env VNil

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

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

23

13

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

29 envLookup fO (Extend x xs) = x;

15 envLookup fO (Extend x xs) = x;

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

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

31

17

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

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

34 | Val : Nat -> Expr G TyNat

20 | Val : Nat -> Expr G TyNat

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

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

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

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

lib/prelude.idr+2−1

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

1import nat;

2import list;

3+import vect;

3import io;

4import io;

4

5

5data Bool = False | True;

6data Bool = False | True;

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

81---- some basic io

82---- some basic io

82

83

83putStr : String -> IO ();

84putStr : String -> IO ();

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

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

85

86

86putStrLn : String -> IO ();

87putStrLn : String -> IO ();

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

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

miniidris.cabal+2−1

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

32 Paths_miniidris

33

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

35− containers, process, transformers, filepath, directory

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

36+ epic

36

37

37 Extensions: MultiParamTypeClasses, FunctionalDependencies,

38 Extensions: MultiParamTypeClasses, FunctionalDependencies,

38 FlexibleInstances

39 FlexibleInstances

src/Core/Evaluate.hs+10−9

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

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

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

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

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

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

60 case evCase env [] [] tree of

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

62 (Just v, _) -> v

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

79

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

81 apply env (VP Ref n ty) args

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

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

83 = case evCase env ns args tree of

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

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

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

174data Def = Function Fun

175 | TyDecl NameType Type Value

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

177− | CaseOp Type [Name] SC

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

178

179instance Show Def where

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

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

182 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

184

185-------

186

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

205 addCons (tag+1) cons (addDef n

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

207

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

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

209−addCasedef n (CaseDef args sc) ty ctxt

209+addCasedef n ps ty ctxt

210+ = case simpleCase ps of

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

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

211

212

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

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

213addOperator n ty a op ctxt

214addOperator n ty a op ctxt

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

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

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

220 (TyDecl _ ty _) -> return ty

221 (TyDecl _ ty _) -> return ty

221 (Operator ty _ _) -> return ty

222 (Operator ty _ _) -> return ty

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

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

223

224

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

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

225lookupP n ctxt

226lookupP n ctxt

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

227 case def of

228 case def of

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

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

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

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

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

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

232

233

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

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

src/Idris/AbsSyntax.hs+6−2

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

11import Data.Char

12import Debug.Trace

13

14+import qualified Epic.Epic as E

15+

14data IOption = IOption { opt_logLevel :: Int }

16data IOption = IOption { opt_logLevel :: Int }

15 deriving (Show, Eq)

17 deriving (Show, Eq)

16

18

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

27 idris_log :: String,

29 idris_log :: String,

28 idris_options :: IOption,

30 idris_options :: IOption,

29 idris_name :: Int,

31 idris_name :: Int,

30− imported :: [FilePath]

32+ imported :: [FilePath],

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

31 }

34 }

32

35

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

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

34

37

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

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

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

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

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

83-- Commands in the REPL

86-- Commands in the REPL

84

87

85data Command = Quit | Help | Eval PTerm

88data Command = Quit | Help | Eval PTerm

89+ | Compile String

86 | TTShell

90 | TTShell

87 | NOP

91 | NOP

88

92

src/Idris/ElabDecls.hs+1−1

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

67 logLvl 3 (show tree)

68 ctxt <- getContext

69 case lookupTy n ctxt of

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

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

71 Nothing -> return ()

72 where

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

src/Idris/Parser.hs+7−3

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

226 return $ PHidden e

227

228pApp syn = do f <- pSimpleExpr syn

229− iargs <- many (pImplicitArg syn)

230− args <- many1 (pSimpleExpr syn)

229+ args <- many1 (pArg syn)

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

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)

232

236

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

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

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

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

src/Idris/Primitives.hs+57−20

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

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

2+

1module Idris.Primitives(elabPrims) where

3module Idris.Primitives(elabPrims) where

2

4

3import Idris.ElabDecls

5import Idris.ElabDecls

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

6import Core.TT

8import Core.TT

7import Core.Evaluate

9import Core.Evaluate

8

10

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

12+import qualified Epic.Epic as E

13+

9data Prim = Prim { p_name :: Name,

14data Prim = Prim { p_name :: Name,

10 p_type :: Type,

15 p_type :: Type,

11 p_arity :: Int,

16 p_arity :: Int,

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

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

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

13 }

19 }

14

20

15ty [] x = Constant x

21ty [] x = Constant x

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

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

17

23

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+

18primitives =

33primitives =

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

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

35+ (eOp E.plus_),

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

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

37+ (eOp E.minus_),

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

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

39+ (eOp E.times_),

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

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

41+ (eOp E.divide_),

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

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

43+ (eOp E.eq_),

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

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

45+ (eOp E.lt_),

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

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

47+ (eOp E.lte_),

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

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

49+ (eOp E.gt_),

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

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

51+ (eOp E.gte_),

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

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

53+ (eOp E.plusF_),

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

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

55+ (eOp E.minusF_),

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

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

57+ (eOp E.timesF_),

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

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

59+ (eOp E.divideF_),

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

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

61+ (eOp E.eqF_),

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

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

63+ (eOp E.ltF_),

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

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

65+ (eOp E.lteF_),

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

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

67+ (eOp E.gtF_),

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

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

69+ (eOp E.gteF_),

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

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

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

38 ]

72 ]

39

73

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

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

53sBin _ _ = Nothing

87sBin _ _ = Nothing

54

88

55elabPrim :: Prim -> Idris ()

89elabPrim :: Prim -> Idris ()

90+elabPrim (Prim n ty i def epic)

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

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

92+ i <- getIState

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

57

94

58elabPrims :: Idris ()

95elabPrims :: Idris ()

59elabPrims = do mapM_ (elabDecl toplevel)

96elabPrims = do mapM_ (elabDecl toplevel)

src/Idris/REPL.hs+2

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

7import Idris.ElabDecls

8import Idris.Error

9import Idris.Delaborate

10+import Idris.Compiler

10

11

11import Core.Evaluate

12import Core.Evaluate

12import Core.ProofShell

13import Core.ProofShell

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

52 let shst = initState (tt_ctxt ist)

53 let shst = initState (tt_ctxt ist)

53 shst' <- lift $ runShell shst

54 shst' <- lift $ runShell shst

54 return ()

55 return ()

56+process (Compile f) = do compile f

55process NOP = return ()

57process NOP = return ()

56

58

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

26 <|> do eof; return NOP

27 <|> do eof; return NOP