Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Update Epic.lhs to use the evaluator

  • Loading branch information...
commit f50afc0fbf7bde394654d11606c5a4e0f4ec43d3 1 parent f4ee6cc
Edwin Brady authored
View
13 Epic/Epic.lhs
@@ -36,6 +36,7 @@
> Epic.Epic.compile, compileObj, Epic.Epic.link,
> Epic.Epic.compileWith, compileObjWith, Epic.Epic.linkWith,
> run,
+> evaluate,
> CompileOptions(..),
> -- * Some basic definitions
> basic_defs) where
@@ -45,9 +46,12 @@ Combinators for constructing an expression
> import Control.Monad.State
> import System
> import System.IO
+> import Debug.Trace
> import Epic.Language
> import Epic.Compiler
+> import Epic.Evaluator
+> import Epic.Scopecheck
> import Epic.Parser
Allow Haskell functions to be used to build expressions.
@@ -444,6 +448,10 @@ Remaining expression constructs
> mkDecl (Epic.Epic.Link f) = Epic.Language.Link f
> mkDecl (Epic.Epic.CType f) = Epic.Language.CType f
+> mkEvalDecl :: Decl -> EvalDecl
+> mkEvalDecl (Decl n _ f _ _) = EDecl n (mkHOAS f)
+> mkEvalDecl _ = EDirective
+
> -- |Compile a program to an executable
> compile :: Program -> FilePath -> IO ()
> compile = compileWith []
@@ -480,6 +488,11 @@ Remaining expression constructs
> system tmpn
> return ()
+> evaluate :: EpicExpr e => Program -> e -> Expr
+> evaluate tms e = case checkAll [] (map mkDecl tms) of
+> Just (_, tms') -> eval (map mkEvalDecl tms')
+> (evalState (term e) 0)
+
Some useful functions
> putStr_ :: Expr -> Term
View
111 Epic/Language.lhs
@@ -1,3 +1,5 @@
+> {-# OPTIONS_GHC -fglasgow-exts -XFlexibleInstances #-}
+
> module Epic.Language where
> import Control.Monad
@@ -6,6 +8,8 @@
> import System.Directory
> import System.Environment
+> import Debug.Trace
+
> -- | (Debugging) options to give to compiler
> data CompileOptions = KeepC -- ^ Keep intermediate C file
> | Trace -- ^ Generate trace at run-time (debug)
@@ -98,6 +102,8 @@ Get the arity of a definition in the context
> type Tag = Int
+> type HFun = Expr -> Expr
+
> data Expr = V Int -- Locally bound name
> | R Name -- Global reference
> | App Expr [Expr] -- Function application
@@ -113,8 +119,10 @@ Get the arity of a definition in the context
> | Op Op Expr Expr -- Infix operator
> | Let Name Type Expr Expr -- Let binding
> | LetM Name Expr Expr -- Update a variable
+> | HLet Name Type Expr HFun -- HOAS let, for evaluation
> | Update Int Expr Expr -- Update a variable (scope-checked)
> | Lam Name Type Expr -- inner lambda
+> | HLam Name Type HFun -- HOAS lambda, for evaluation
> | Error String -- Exit with error message
> | Impossible -- Claimed impossible to reach code
> | WithMem Allocator Expr Expr -- evaluate with manual allocation
@@ -126,11 +134,24 @@ Get the arity of a definition in the context
> alt_args :: [(Name, Type)], -- bound arguments
> alt_expr :: Expr -- what to do
> }
+> | HAlt { alt_tag :: Tag,
+> alt_numargs :: Int,
+> alt_binds :: HRHS }
> | ConstAlt { alt_const :: Int,
> alt_expr :: Expr }
> | DefaultCase { alt_expr :: Expr }
> deriving Eq
+> data HRHS = HExp Expr
+> | HBind Name Type (Expr -> HRHS)
+> deriving Eq
+
+> instance Eq (Expr -> Expr) where -- can't compare HOAS for equality
+> _ == _ = False
+
+> instance Eq (Expr -> HRHS) where -- can't compare HOAS for equality
+> _ == _ = False
+
> instance Ord CaseAlt where -- only the tag matters
> compare (Alt t1 _ _) (Alt t2 _ _) = compare t1 t2
> compare (Alt _ _ _) (DefaultCase _) = LT
@@ -211,6 +232,96 @@ Programs
> | CType String
> deriving Show
+> data EvalDecl = EDecl { ename :: Name,
+> edef :: Expr -- as HOAS
+> }
+> | EDirective
+
+> class SubstV x where
+> subst :: Int -> Expr -> x -> x
+
+> instance SubstV a => SubstV [a] where
+> subst v rep xs = map (subst v rep) xs
+
+> instance SubstV (Expr, Type) where
+> subst v rep (x, t) = (subst v rep x, t)
+
+> instance SubstV Expr where
+> subst v rep (V x) | v == x = rep
+> subst v rep (App x xs) = App (subst v rep x) (subst v rep xs)
+> subst v rep (Lazy x) = Lazy (subst v rep x)
+> subst v rep (Effect x) = Effect (subst v rep x)
+> subst v rep (Con t xs) = Con t (subst v rep xs)
+> subst v rep (Proj x i) = Proj (subst v rep x) i
+> subst v rep (Case x alts) = Case (subst v rep x) (subst v rep alts)
+> subst v rep (If a t e)
+> = If (subst v rep a) (subst v rep t) (subst v rep e)
+> subst v rep (While a e) = While (subst v rep a) (subst v rep e)
+> subst v rep (WhileAcc a t e)
+> = WhileAcc (subst v rep a) (subst v rep t) (subst v rep e)
+> subst v rep (Op o x y) = Op o (subst v rep x) (subst v rep y)
+> subst v rep (Let n ty val sc)
+> = Let n ty (subst v rep val) (subst v rep sc)
+> subst v rep (LetM n val sc)
+> = LetM n (subst v rep val) (subst v rep sc)
+> subst v rep (Lam n t e) = Lam n t (subst v rep e)
+> subst v rep (WithMem a x y) = WithMem a (subst v rep x) (subst v rep y)
+> subst v rep (ForeignCall t s xs) = ForeignCall t s (subst v rep xs)
+> subst v rep (LazyForeignCall t s xs)
+> = LazyForeignCall t s (subst v rep xs)
+> subst v rep x = x
+
+> instance SubstV CaseAlt where
+> subst v rep (Alt t as e) = Alt t as (subst v rep e)
+> subst v rep (ConstAlt i e) = ConstAlt i (subst v rep e)
+> subst v rep (DefaultCase e) = DefaultCase (subst v rep e)
+
+> class HOAS a b | a -> b where
+> hoas :: Int -> a -> b
+> mkHOAS :: a -> b
+> mkHOAS = hoas 0
+
+> instance HOAS a a => HOAS [a] [a] where
+> hoas v xs = map (hoas v) xs
+
+> instance HOAS a a => HOAS (a, Type) (a, Type) where
+> hoas v (x, t) = (hoas v x, t)
+
+> instance HOAS Func Expr where
+> hoas v (Bind args locs def flags) = hargs v args def where
+> hargs v [] def = hoas v def
+> hargs v ((x,t):xs) def
+> = HLam x t (\var -> hargs (v+1) xs (subst v var def))
+
+> instance HOAS Expr Expr where
+> hoas v (App f xs) = App (hoas v f) (hoas v xs)
+> hoas v (Lazy x) = Lazy (hoas v x)
+> hoas v (Effect x) = Effect (hoas v x)
+> hoas v (Con t xs) = Con t (hoas v xs)
+> hoas v (Proj x i) = Proj (hoas v x) i
+> hoas v (Case x xs) = Case (hoas v x) (hoas v xs)
+> hoas v (If x t e) = If (hoas v x) (hoas v t) (hoas v e)
+> hoas v (While x y) = While (hoas v x) (hoas v y)
+> hoas v (WhileAcc x y z) = WhileAcc (hoas v x) (hoas v y) (hoas v z)
+> hoas v (Op o x y) = Op o (hoas v x) (hoas v y)
+> hoas v (Let n t val sc)
+> = HLet n t val (\var -> subst v var (hoas (v+1) sc))
+> hoas v (Lam n ty sc)
+> = HLam n ty (\var -> subst v var (hoas (v+1) sc))
+> hoas v (WithMem a x y) = WithMem a (hoas v x) (hoas v y)
+> hoas v (ForeignCall t n xs) = ForeignCall t n (hoas v xs)
+> hoas v (LazyForeignCall t n xs) = LazyForeignCall t n (hoas v xs)
+> hoas v x = x
+
+> instance HOAS CaseAlt CaseAlt where
+> hoas v (Alt t args rhs) = HAlt t (length args) (hbind v args rhs) where
+> hbind v [] rhs = HExp (hoas v rhs)
+> hbind v ((x,t):xs) rhs
+> = HBind x t (\var -> hbind (v+1) xs (subst v var rhs))
+> hoas v (ConstAlt i e) = ConstAlt i (hoas v e)
+> hoas v (DefaultCase e) = DefaultCase (hoas v e)
+
+
> data CGFlag = Inline | Strict
> deriving (Show, Eq)
View
6 FL/src/Main.lhs
@@ -15,4 +15,8 @@
> testdefs = [(name "add", add), (name "main", main_)]
-> main = execute testdefs
+> main = do let prog = mkProgram testdefs
+> let addNums = build (App (App (Ref (name "add")) (Const (CInt 5))) (Const (CInt 6)))
+> let exp = evaluate prog addNums
+> print exp
+> run prog
View
2  Papers/Epic-TFP/conclusions.tex
@@ -41,7 +41,7 @@ \section{Conclusion}
\subsubsection{Future work}
Epic is currently used in practice by a dependently typed functional
-language, Idris~\cite{idris-plpv}, and experimentally by
+language, Idris~\cite{plpv11}, and experimentally by
Agda~\cite{norell-thesis} and Epigram~\cite{levitation}. Future work
will therefore have an emphasis on providing an efficient executable
environment for these and related languages. An interesting research
View
2  Papers/Epic-TFP/epic.tex
@@ -50,7 +50,7 @@
\begin{document}
-\title{Epic --- A Library for Generating Compilers\\(Research Paper)}
+\title{Epic --- A Library for Generating Compilers}
\author{Edwin Brady}
\institute{University of St Andrews, KY16 9SX, Scotland/UK,\\
View
2  Papers/Epic-TFP/intro.tex
@@ -33,7 +33,7 @@ \section{Introduction}
Epic was originally written as a back end for
Epigram~\cite{levitation} (the name\footnote{Coined by James McKinna}
is short for ``\textbf{Epi}gram \textbf{C}ompiler''). It is now used
-by Idris~\cite{idris-plpv} and as an experimental back end for
+by Idris~\cite{plpv11} and as an experimental back end for
Agda. It is specifically designed for reuse by other source languages.
View
7 Papers/Epic-TFP/literature.bib
@@ -68,13 +68,6 @@ @inproceedings{mitchell-super
}
-@inproceedings{idris-plpv,
- author = {Edwin Brady},
- title = {Idris --- Systems Programming Meets Dependent Types},
- year = 2011,
- booktitle = {Programming Languages Meets Program Verification}
-}
-
@inproceedings{devil-osdi00,
author = {Fabrice M{\'e}rillon and
Laurent R{\'e}veill{\`e}re and
View
8 epic.cabal
@@ -1,5 +1,5 @@
Name: epic
-Version: 0.1.12
+Version: 0.1.13
Author: Edwin Brady
License: BSD3
License-file: LICENSE
@@ -26,7 +26,8 @@ Library
Exposed-modules: Epic.Compiler Epic.Epic
Other-modules: Epic.Bytecode Epic.Parser Epic.Scopecheck
Epic.Language Epic.Lexer Epic.CodegenC Epic.CodegenStack
- Epic.OTTLang Epic.Simplify Epic.Stackcode Paths_epic
+ Epic.OTTLang Epic.Simplify Epic.Stackcode
+ Epic.Evaluator Paths_epic
Build-depends: base >=4 && <5 , haskell98, mtl, Cabal, array, directory
@@ -34,6 +35,7 @@ Executable epic
Main-is: Main.lhs
Other-modules: Epic.Bytecode Epic.Parser Epic.Scopecheck
Epic.Language Epic.Lexer Epic.CodegenC Epic.CodegenStack
- Epic.OTTLang Epic.Simplify Epic.Stackcode Paths_epic
+ Epic.OTTLang Epic.Simplify Epic.Stackcode
+ Epic.Evaluator Paths_epic
Build-depends: base >=4 && <5, mtl, array, haskell98, Cabal, directory
Please sign in to comment.
Something went wrong with that request. Please try again.