Skip to content
Browse files

Made a start on the high level language

  • Loading branch information...
1 parent ff5f762 commit 554c3952175f3a2298e6626e41fa85b16f7bef49 Edwin Brady committed
Showing with 175 additions and 29 deletions.
  1. +3 −1 miniidris.cabal
  2. +15 −27 src/Core/Evaluate.hs
  3. +17 −0 src/Core/TT.hs
  4. +49 −0 src/Idris/AbsSyntax.hs
  5. +78 −0 src/Idris/Parser.hs
  6. +13 −1 src/Main.hs
View
4 miniidris.cabal
@@ -19,7 +19,9 @@ Executable miniidris
hs-source-dirs: src
Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
Core.ProofShell, Core.ProofState, Core.CoreParser,
- Core.ShellParser, Core.Unify, Core.Elaborate
+ Core.ShellParser, Core.Unify, Core.Elaborate,
+
+ Idris.AbsSyntax Idris.Parser
Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
containers
View
42 src/Core/Evaluate.hs
@@ -1,11 +1,10 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module Core.Evaluate(normalise,
- Fun(..), Def(..), Context, toAlist,
- emptyContext, addToCtxt, addConstant, addDatatype,
+ Fun(..), Def(..), Context,
+ addToCtxt, addConstant, addDatatype,
lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
-import qualified Data.Map as Map
import Debug.Trace
import Core.TT
@@ -94,36 +93,25 @@ wknV i t = t
data Fun = Fun Type Value Term Value
deriving Show
+{- A definition is either a simple function (just an expression with a type),
+ a constant, which could be a data or type constructor, an axiom or as an
+ yet undefined function, or an Operator.
+ An Operator is a collection of pattern matching definitions, and a function
+ which explains how to reduce. -}
+
data Def = Function Fun
| Constant NameType Type Value
- deriving Show
-
-{-
-type Context = [(Name, Def)]
-
-emptyContext = []
-
-addDef :: Name -> Def -> Context -> Context
-addDef n d ctxt = (n, d) : ctxt
-
-lookupCtxt :: Name -> Context -> Maybe Def
-lookupCtxt n c = lookup n c
--}
+ | Operator Type [(Term, Term)] ([Value] -> Maybe Value)
-type Context = Map.Map Name Def
-emptyContext = Map.empty
-
-addDef :: Name -> Def -> Context -> Context
-addDef = Map.insert
-
-lookupCtxt :: Name -> Context -> Maybe Def
-lookupCtxt = Map.lookup
-
-toAlist :: Context -> [(Name, Def)]
-toAlist = Map.toList
+instance Show Def where
+ show (Function f) = "Function: " ++ show f
+ show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty
+ show (Operator ty ps _) = "Operator: " ++ show ty ++ " " ++ show ps
-------
+type Context = Ctxt Def
+
addToCtxt :: Name -> Term -> Type -> Context -> Context
addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
tm (eval ctxt [] tm))) ctxt
View
17 src/Core/TT.hs
@@ -4,6 +4,7 @@ module Core.TT where
import Control.Monad.State
import Debug.Trace
+import qualified Data.Map as Map
{- The language has:
* Full dependent types
@@ -61,6 +62,22 @@ instance Show Name where
show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)
show (MN i s) = "{" ++ s ++ show i ++ "}"
+
+-- Contexts allow us to map names to things
+
+type Ctxt a = Map.Map Name a
+emptyContext = Map.empty
+
+addDef :: Name -> a -> Ctxt a -> Ctxt a
+addDef = Map.insert
+
+lookupCtxt :: Name -> Ctxt a -> Maybe a
+lookupCtxt = Map.lookup
+
+toAlist :: Ctxt a -> [(Name, a)]
+toAlist = Map.toList
+
+
data Raw = Var Name
| RBind Name (Binder Raw) Raw
| RApp Raw Raw
View
49 src/Idris/AbsSyntax.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
+
+module Idris.AbsSyntax where
+
+import Core.TT
+import Core.Evaluate
+
+data IState = IState { tt_ctxt :: Context,
+ tt_infixes :: [(String,
+ (Fixity, PTerm -> PTerm -> PTerm))]
+ }
+
+
+{- Plan:
+ Treat it as a theorem prover - one definition at a time, parse, elaborate,
+ and add to context. Since elaboration can be affected by definitions we've
+ added (e.g. plicity) -}
+
+-- Parsed declarations
+
+data Fixity = Infixl { prec :: Int }
+ | Infixr { prec :: Int }
+ | InfixN { prec :: Int }
+ deriving (Show, Eq)
+
+data Plicity = Imp | Exp deriving Show
+
+data PDecl = PFix Fixity String -- fixity declaration
+ | PTy Name PTerm -- type declaration
+ | PClause PTerm PTerm -- pattern clause
+ | PData PData -- data declaration
+ deriving Show
+
+data PData = PDatadecl { d_name :: Name,
+ d_tcon :: PTerm,
+ d_cons :: [(Name, PTerm)] }
+ deriving Show
+
+-- High level language terms
+
+data PTerm = PQuote Raw
+ | PRef Name
+ | PLam Name PTerm PTerm
+ | PPi Plicity Name PTerm PTerm
+ | PApp PTerm [(Name, PTerm)] [PTerm]
+ | Placeholder
+ deriving Show
+
+
View
78 src/Idris/Parser.hs
@@ -0,0 +1,78 @@
+module Idris.Parser where
+
+import Idris.AbsSyntax
+
+import Core.CoreParser
+import Core.TT
+
+import Text.ParserCombinators.Parsec
+import Text.ParserCombinators.Parsec.Expr
+import Text.ParserCombinators.Parsec.Language
+import qualified Text.ParserCombinators.Parsec.Token as PTok
+
+import Debug.Trace
+
+type TokenParser a = PTok.TokenParser a
+
+lexer :: TokenParser ()
+lexer = PTok.makeTokenParser haskellDef
+
+whiteSpace= PTok.whiteSpace lexer
+lexeme = PTok.lexeme lexer
+symbol = PTok.symbol lexer
+natural = PTok.natural lexer
+parens = PTok.parens lexer
+semi = PTok.semi lexer
+comma = PTok.comma lexer
+identifier= PTok.identifier lexer
+reserved = PTok.reserved lexer
+operator = PTok.operator lexer
+reservedOp= PTok.reservedOp lexer
+lchar = lexeme.char
+
+parseExpr = parse pFullExpr "(input)"
+
+pFullExpr = do x <- pExpr; eof; return x
+
+pExpr' :: Parser PTerm
+pExpr' = try pApp
+ <|> pSimpleExpr
+ <|> try pLambda
+ <|> try pPi
+
+pExpr = buildExpressionParser table pExpr'
+
+pSimpleExpr =
+ try (do symbol "!["; t <- pTerm; lchar ']'
+ return $ PQuote t)
+ <|> try (do x <- iName; return (PRef x))
+ <|> try (do lchar '_'; return Placeholder)
+ <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
+
+pApp = do f <- pSimpleExpr
+ args <- many1 pSimpleExpr
+ return (PApp f [] args)
+
+pTSig = do lchar ':'
+ pExpr
+
+pLambda = do lchar '\\'; x <- iName; t <- option Placeholder pTSig
+ symbol "=>"
+ sc <- pExpr
+ return (PLam x t sc)
+
+pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
+ symbol "->"
+ sc <- pExpr
+ return (PPi Exp x t sc)
+ <|> do lchar '{'; x <- iName; t <- pTSig; lchar '}'
+ symbol "->"
+ sc <- pExpr
+ return (PPi Imp x t sc)
+
+
+table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
+ [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
+
+binary name f assoc = Infix (do { reservedOp name; return f }) assoc
+
View
14 src/Main.hs
@@ -1,5 +1,7 @@
module Main where
+import System.Console.Readline
+
import Core.CoreParser
import Core.ShellParser
import Core.TT
@@ -7,7 +9,17 @@ import Core.Typecheck
import Core.ProofShell
import Core.Evaluate
-main = do f <- readFile "test.mi"
+import Idris.AbsSyntax
+import Idris.Parser
+
+main = do Just x <- readline "> "
+ case parseExpr x of
+ Left err -> print err
+ Right d -> print d
+ main
+
+main'
+ = do f <- readFile "test.mi"
case parseFile f of
Left err -> print err
Right defs -> do

0 comments on commit 554c395

Please sign in to comment.
Something went wrong with that request. Please try again.