Permalink
Browse files

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

  • Loading branch information...
1 parent 38a6bc7 commit 20861ec18945e66eedf25902b2a6afa78e0c3a96 Edwin Brady committed Oct 14, 2011
Showing with 90 additions and 53 deletions.
  1. +2 −16 interp.idr
  2. +2 −1 lib/prelude.idr
  3. +2 −1 miniidris.cabal
  4. +10 −9 src/Core/Evaluate.hs
  5. +6 −2 src/Idris/AbsSyntax.hs
  6. +1 −1 src/Idris/ElabDecls.hs
  7. +7 −3 src/Idris/Parser.hs
  8. +57 −20 src/Idris/Primitives.hs
  9. +2 −0 src/Idris/REPL.hs
  10. +1 −0 src/Idris/REPLParser.hs
View
@@ -5,32 +5,18 @@ interpTy : Ty -> Set;
interpTy TyNat = Nat;
interpTy (TyFun s t) = interpTy s -> interpTy t;
-data Fin : Nat -> Set where
- fO : Fin (S k)
- | fS : Fin k -> Fin (S k);
-
-infixr 7 :: ;
-
-data Vect : Set -> Nat -> Set where
- VNil : Vect a O
- | (::) : a -> Vect a k -> Vect a (S k);
-
using (G : Vect Ty n) {
data Env : Vect Ty n -> Set where
Empty : Env VNil
| Extend : interpTy a -> Env G -> Env (a :: G);
- lookup : (i : Fin n) -> Vect a n -> a;
- lookup fO (x :: xs) = x;
- lookup (fS k) (x :: xs) = lookup k xs;
-
- envLookup : (i : Fin n) -> Env G -> interpTy (lookup i G);
+ envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);
envLookup fO (Extend x xs) = x;
envLookup (fS i) (Extend x xs) = envLookup i xs;
data Expr : Vect Ty n -> Ty -> Set where
- Var : (i : Fin n) -> Expr G (lookup i G)
+ Var : (i : Fin n) -> Expr G (vlookup i G)
| Val : Nat -> Expr G TyNat
| Lam : Expr (a :: G) t -> Expr G (TyFun a t)
| App : Expr G (TyFun a t) -> Expr G a -> Expr G t
View
@@ -1,5 +1,6 @@
import nat;
import list;
+import vect;
import io;
data Bool = False | True;
@@ -81,7 +82,7 @@ div = prim__divInt;
---- some basic io
putStr : String -> IO ();
-putStr = mkForeign (FFun "putStr" (Cons FString Nil) FUnit);
+putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;
putStrLn : String -> IO ();
putStrLn x = putStr (x ++ "\n");
View
@@ -32,7 +32,8 @@ Executable miniidris
Paths_miniidris
Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
- containers, process, transformers, filepath, directory
+ containers, process, transformers, filepath, directory,
+ epic
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances
View
@@ -56,7 +56,7 @@ eval ctxt genv tm = ev [] tm where
ev env (P Ref n ty) = case lookupDef n ctxt of
Just (Function (Fun _ _ _ v)) -> v
Just (TyDecl nt ty hty) -> VP nt n hty
- Just (CaseOp _ [] tree) ->
+ Just (CaseOp _ _ [] tree) ->
case evCase env [] [] tree of
(Nothing, _) -> VP Ref n (ev env ty)
(Just v, _) -> v
@@ -79,7 +79,7 @@ eval ctxt genv tm = ev [] tm where
apply env (VBind n (Lam t) sc) (a:as) = wknV (-1) $ apply env (sc a) as
apply env (VP Ref n ty) args
- | Just (CaseOp _ ns tree) <- lookupDef n ctxt
+ | Just (CaseOp _ _ ns tree) <- lookupDef n ctxt
= case evCase env ns args tree of
(Nothing, _) -> unload env (VP Ref n ty) args
(Just v, rest) -> evApply env rest v
@@ -174,13 +174,13 @@ data Fun = Fun Type Value Term Value
data Def = Function Fun
| TyDecl NameType Type Value
| Operator Type Int ([Value] -> Maybe Value)
- | CaseOp Type [Name] SC
+ | CaseOp Type [(Term, Term)] [Name] SC
instance Show Def where
show (Function f) = "Function: " ++ show f
show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty
show (Operator ty _ _) = "Operator: " ++ show ty
- show (CaseOp ty ns sc) = "Case: " ++ show ns ++ " " ++ show sc
+ show (CaseOp ty _ ns sc) = "Case: " ++ show ns ++ " " ++ show sc
-------
@@ -205,9 +205,10 @@ addDatatype (Data n ty cons) ctxt
addCons (tag+1) cons (addDef n
(TyDecl (DCon tag (arity ty')) ty (eval ctxt [] ty)) ctxt)
-addCasedef :: Name -> CaseDef -> Type -> Context -> Context
-addCasedef n (CaseDef args sc) ty ctxt
- = addDef n (CaseOp ty args sc) ctxt
+addCasedef :: Name -> [(Term, Term)] -> Type -> Context -> Context
+addCasedef n ps ty ctxt
+ = case simpleCase ps of
+ CaseDef args sc -> addDef n (CaseOp ty ps args sc) ctxt
addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator n ty a op ctxt
@@ -219,15 +220,15 @@ lookupTy n ctxt = do def <- lookupCtxt n ctxt
(Function (Fun ty _ _ _)) -> return ty
(TyDecl _ ty _) -> return ty
(Operator ty _ _) -> return ty
- (CaseOp ty _ _) -> return ty
+ (CaseOp ty _ _ _) -> return ty
lookupP :: Name -> Context -> Maybe Term
lookupP n ctxt
= do def <- lookupCtxt n ctxt
case def of
(Function (Fun ty _ tm _)) -> return (P Ref n ty)
(TyDecl nt ty hty) -> return (P nt n ty)
- (CaseOp ty _ _) -> return (P Ref n ty)
+ (CaseOp ty _ _ _) -> return (P Ref n ty)
(Operator ty _ _) -> return (P Ref n ty)
lookupDef :: Name -> Context -> Maybe Def
@@ -11,6 +11,8 @@ import Data.List
import Data.Char
import Debug.Trace
+import qualified Epic.Epic as E
+
data IOption = IOption { opt_logLevel :: Int }
deriving (Show, Eq)
@@ -27,10 +29,11 @@ data IState = IState { tt_ctxt :: Context,
idris_log :: String,
idris_options :: IOption,
idris_name :: Int,
- imported :: [FilePath]
+ imported :: [FilePath],
+ idris_prims :: [(Name, ([E.Name], E.Term))]
}
-idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 []
+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] []
-- The monad for the main REPL - reading and processing files and updating
-- global state (hence the IO inner monad).
@@ -83,6 +86,7 @@ iLOG = logLvl 1
-- Commands in the REPL
data Command = Quit | Help | Eval PTerm
+ | Compile String
| TTShell
| NOP
@@ -67,7 +67,7 @@ elabClauses info n_in cs = let n = liftname info n_in in
logLvl 3 (show tree)
ctxt <- getContext
case lookupTy n ctxt of
- Just ty -> updateContext (addCasedef n tree ty)
+ Just ty -> updateContext (addCasedef n (map debind pats) ty)
Nothing -> return ()
where
debind (x, y) = (depat x, depat y)
View
@@ -226,9 +226,13 @@ pHSimpleExpr syn
return $ PHidden e
pApp syn = do f <- pSimpleExpr syn
- iargs <- many (pImplicitArg syn)
- args <- many1 (pSimpleExpr syn)
- return (PApp f (iargs ++ map PExp args))
+ args <- many1 (pArg syn)
+ return (PApp f args)
+
+pArg :: SyntaxInfo -> IParser PArg
+pArg syn = pImplicitArg syn
+ <|> do e <- pSimpleExpr syn
+ return (PExp e)
pImplicitArg syn = do lchar '{'; n <- iName
v <- option (PRef n) (do lchar '='; pExpr syn)
@@ -1,3 +1,5 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
+
module Idris.Primitives(elabPrims) where
import Idris.ElabDecls
@@ -6,35 +8,67 @@ import Idris.AbsSyntax
import Core.TT
import Core.Evaluate
+import Epic.Epic hiding (Term, Type, Name, fn)
+import qualified Epic.Epic as E
+
data Prim = Prim { p_name :: Name,
p_type :: Type,
p_arity :: Int,
- p_def :: [Value] -> Maybe Value
+ p_def :: [Value] -> Maybe Value,
+ p_epic :: ([E.Name], E.Term)
}
ty [] x = Constant x
ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
+type ETm = E.Term
+type EOp = E.Op
+
+fun = E.fn
+ref = E.ref
+
+eOp :: EOp -> ([E.Name], ETm)
+eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
+
primitives =
- [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+)),
- Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-)),
- Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*)),
- Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div)),
- Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==)),
- Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<)),
- Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=)),
- Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>)),
- Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=)),
- Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+)),
- Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-)),
- Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*)),
- Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/)),
- Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==)),
- Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),
- Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),
- Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>)),
- Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=)),
+ [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))
+ (eOp E.plus_),
+ Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))
+ (eOp E.minus_),
+ Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*))
+ (eOp E.times_),
+ Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div))
+ (eOp E.divide_),
+ Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==))
+ (eOp E.eq_),
+ Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<))
+ (eOp E.lt_),
+ Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=))
+ (eOp E.lte_),
+ Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>))
+ (eOp E.gt_),
+ Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=))
+ (eOp E.gte_),
+ Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+))
+ (eOp E.plusF_),
+ Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-))
+ (eOp E.minusF_),
+ Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*))
+ (eOp E.timesF_),
+ Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/))
+ (eOp E.divideF_),
+ Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==))
+ (eOp E.eqF_),
+ Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<))
+ (eOp E.ltF_),
+ Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=))
+ (eOp E.lteF_),
+ Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>))
+ (eOp E.gtF_),
+ Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))
+ (eOp E.gteF_),
Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))
+ ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")
]
iBin 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))
sBin _ _ = Nothing
elabPrim :: Prim -> Idris ()
-elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)
+elabPrim (Prim n ty i def epic)
+ = do updateContext (addOperator n ty i def)
+ i <- getIState
+ putIState i { idris_prims = (n, epic) : idris_prims i }
elabPrims :: Idris ()
elabPrims = do mapM_ (elabDecl toplevel)
View
@@ -7,6 +7,7 @@ import Idris.REPLParser
import Idris.ElabDecls
import Idris.Error
import Idris.Delaborate
+import Idris.Compiler
import Core.Evaluate
import Core.ProofShell
@@ -52,5 +53,6 @@ process TTShell = do ist <- get
let shst = initState (tt_ctxt ist)
shst' <- lift $ runShell shst
return ()
+process (Compile f) = do compile f
process NOP = return ()
@@ -22,5 +22,6 @@ pCmd :: IParser Command
pCmd = try (do cmd ["q", "quit"]; return Quit)
<|> try (do cmd ["h", "?", "help"]; return Help)
<|> try (do cmd ["ttshell"]; return TTShell)
+ <|> try (do cmd ["c", "compile"]; f <- identifier; return (Compile f))
<|> do t <- pFullExpr defaultSyntax; return (Eval t)
<|> do eof; return NOP

0 comments on commit 20861ec

Please sign in to comment.