git.iko.soy/Idris-dev
on master help sign in
Made a start on the high level language
554c395Edwin Brady
miniidris.cabal+3−1
compare with master
unifiedsplit
@@ -19,7 +19,9 @@ Executable miniidris
19 hs-source-dirs: src
19 hs-source-dirs: src
20 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
20 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
21 Core.ProofShell, Core.ProofState, Core.CoreParser,
21 Core.ProofShell, Core.ProofState, Core.CoreParser,
22− Core.ShellParser, Core.Unify, Core.Elaborate
22+ Core.ShellParser, Core.Unify, Core.Elaborate,
23+
24+ Idris.AbsSyntax Idris.Parser
23
25
24 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
26 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,
25 containers
27 containers
src/Core/Evaluate.hs+15−27
@@ -1,11 +1,10 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3module Core.Evaluate(normalise,
3module Core.Evaluate(normalise,
4− Fun(..), Def(..), Context, toAlist,
4+ Fun(..), Def(..), Context,
5− emptyContext, addToCtxt, addConstant, addDatatype,
5+ addToCtxt, addConstant, addDatatype,
6 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
6 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where
7
7
8−import qualified Data.Map as Map
9import Debug.Trace
8import Debug.Trace
10import Core.TT
9import Core.TT
11
10
@@ -94,36 +93,25 @@ wknV i t = t
94data Fun = Fun Type Value Term Value
93data Fun = Fun Type Value Term Value
95 deriving Show
94 deriving Show
96
95
96+{- A definition is either a simple function (just an expression with a type),
97+ a constant, which could be a data or type constructor, an axiom or as an
98+ yet undefined function, or an Operator.
99+ An Operator is a collection of pattern matching definitions, and a function
100+ which explains how to reduce. -}
101+
97data Def = Function Fun
102data Def = Function Fun
98 | Constant NameType Type Value
103 | Constant NameType Type Value
99− deriving Show
104+ | Operator Type [(Term, Term)] ([Value] -> Maybe Value)
100−
101−{-
102−type Context = [(Name, Def)]
103−
104−emptyContext = []
105−
106−addDef :: Name -> Def -> Context -> Context
107−addDef n d ctxt = (n, d) : ctxt
108−
109−lookupCtxt :: Name -> Context -> Maybe Def
110−lookupCtxt n c = lookup n c
111−-}
112
105
113−type Context = Map.Map Name Def
106+instance Show Def where
114−emptyContext = Map.empty
107+ show (Function f) = "Function: " ++ show f
115−
108+ show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty
116−addDef :: Name -> Def -> Context -> Context
109+ show (Operator ty ps _) = "Operator: " ++ show ty ++ " " ++ show ps
117−addDef = Map.insert
118−
119−lookupCtxt :: Name -> Context -> Maybe Def
120−lookupCtxt = Map.lookup
121−
122−toAlist :: Context -> [(Name, Def)]
123−toAlist = Map.toList
124
110
125-------
111-------
126
112
113+type Context = Ctxt Def
114+
127addToCtxt :: Name -> Term -> Type -> Context -> Context
115addToCtxt :: Name -> Term -> Type -> Context -> Context
128addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
116addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)
129 tm (eval ctxt [] tm))) ctxt
117 tm (eval ctxt [] tm))) ctxt
src/Core/TT.hs+17
@@ -4,6 +4,7 @@ module Core.TT where
4
4
5import Control.Monad.State
5import Control.Monad.State
6import Debug.Trace
6import Debug.Trace
7+import qualified Data.Map as Map
7
8
8{- The language has:
9{- The language has:
9 * Full dependent types
10 * Full dependent types
@@ -61,6 +62,22 @@ instance Show Name where
61 show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)
62 show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)
62 show (MN i s) = "{" ++ s ++ show i ++ "}"
63 show (MN i s) = "{" ++ s ++ show i ++ "}"
63
64
65+
66+-- Contexts allow us to map names to things
67+
68+type Ctxt a = Map.Map Name a
69+emptyContext = Map.empty
70+
71+addDef :: Name -> a -> Ctxt a -> Ctxt a
72+addDef = Map.insert
73+
74+lookupCtxt :: Name -> Ctxt a -> Maybe a
75+lookupCtxt = Map.lookup
76+
77+toAlist :: Ctxt a -> [(Name, a)]
78+toAlist = Map.toList
79+
80+
64data Raw = Var Name
81data Raw = Var Name
65 | RBind Name (Binder Raw) Raw
82 | RBind Name (Binder Raw) Raw
66 | RApp Raw Raw
83 | RApp Raw Raw
src/Idris/AbsSyntax.hsnew file+49
@@ -0,0 +1,49 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
2+
3+module Idris.AbsSyntax where
4+
5+import Core.TT
6+import Core.Evaluate
7+
8+data IState = IState { tt_ctxt :: Context,
9+ tt_infixes :: [(String,
10+ (Fixity, PTerm -> PTerm -> PTerm))]
11+ }
12+
13+
14+{- Plan:
15+ Treat it as a theorem prover - one definition at a time, parse, elaborate,
16+ and add to context. Since elaboration can be affected by definitions we've
17+ added (e.g. plicity) -}
18+
19+-- Parsed declarations
20+
21+data Fixity = Infixl { prec :: Int }
22+ | Infixr { prec :: Int }
23+ | InfixN { prec :: Int }
24+ deriving (Show, Eq)
25+
26+data Plicity = Imp | Exp deriving Show
27+
28+data PDecl = PFix Fixity String -- fixity declaration
29+ | PTy Name PTerm -- type declaration
30+ | PClause PTerm PTerm -- pattern clause
31+ | PData PData -- data declaration
32+ deriving Show
33+
34+data PData = PDatadecl { d_name :: Name,
35+ d_tcon :: PTerm,
36+ d_cons :: [(Name, PTerm)] }
37+ deriving Show
38+
39+-- High level language terms
40+
41+data PTerm = PQuote Raw
42+ | PRef Name
43+ | PLam Name PTerm PTerm
44+ | PPi Plicity Name PTerm PTerm
45+ | PApp PTerm [(Name, PTerm)] [PTerm]
46+ | Placeholder
47+ deriving Show
48+
49+
src/Idris/Parser.hsnew file+78
@@ -0,0 +1,78 @@
1+module Idris.Parser where
2+
3+import Idris.AbsSyntax
4+
5+import Core.CoreParser
6+import Core.TT
7+
8+import Text.ParserCombinators.Parsec
9+import Text.ParserCombinators.Parsec.Expr
10+import Text.ParserCombinators.Parsec.Language
11+import qualified Text.ParserCombinators.Parsec.Token as PTok
12+
13+import Debug.Trace
14+
15+type TokenParser a = PTok.TokenParser a
16+
17+lexer :: TokenParser ()
18+lexer = PTok.makeTokenParser haskellDef
19+
20+whiteSpace= PTok.whiteSpace lexer
21+lexeme = PTok.lexeme lexer
22+symbol = PTok.symbol lexer
23+natural = PTok.natural lexer
24+parens = PTok.parens lexer
25+semi = PTok.semi lexer
26+comma = PTok.comma lexer
27+identifier= PTok.identifier lexer
28+reserved = PTok.reserved lexer
29+operator = PTok.operator lexer
30+reservedOp= PTok.reservedOp lexer
31+lchar = lexeme.char
32+
33+parseExpr = parse pFullExpr "(input)"
34+
35+pFullExpr = do x <- pExpr; eof; return x
36+
37+pExpr' :: Parser PTerm
38+pExpr' = try pApp
39+ <|> pSimpleExpr
40+ <|> try pLambda
41+ <|> try pPi
42+
43+pExpr = buildExpressionParser table pExpr'
44+
45+pSimpleExpr =
46+ try (do symbol "!["; t <- pTerm; lchar ']'
47+ return $ PQuote t)
48+ <|> try (do x <- iName; return (PRef x))
49+ <|> try (do lchar '_'; return Placeholder)
50+ <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
51+
52+pApp = do f <- pSimpleExpr
53+ args <- many1 pSimpleExpr
54+ return (PApp f [] args)
55+
56+pTSig = do lchar ':'
57+ pExpr
58+
59+pLambda = do lchar '\\'; x <- iName; t <- option Placeholder pTSig
60+ symbol "=>"
61+ sc <- pExpr
62+ return (PLam x t sc)
63+
64+pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
65+ symbol "->"
66+ sc <- pExpr
67+ return (PPi Exp x t sc)
68+ <|> do lchar '{'; x <- iName; t <- pTSig; lchar '}'
69+ symbol "->"
70+ sc <- pExpr
71+ return (PPi Imp x t sc)
72+
73+
74+table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
75+ [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
76+
77+binary name f assoc = Infix (do { reservedOp name; return f }) assoc
78+
src/Main.hs+13−1
@@ -1,5 +1,7 @@
1module Main where
1module Main where
2
2
3+import System.Console.Readline
4+
3import Core.CoreParser
5import Core.CoreParser
4import Core.ShellParser
6import Core.ShellParser
5import Core.TT
7import Core.TT
@@ -7,7 +9,17 @@ import Core.Typecheck
7import Core.ProofShell
9import Core.ProofShell
8import Core.Evaluate
10import Core.Evaluate
9
11
12+import Idris.AbsSyntax
13+import Idris.Parser
14+
15+main = do Just x <- readline "> "
16+ case parseExpr x of
17+ Left err -> print err
18+ Right d -> print d
19+ main
20+
21+main'
10−main = do f <- readFile "test.mi"
22+ = do f <- readFile "test.mi"
11 case parseFile f of
23 case parseFile f of
12 Left err -> print err
24 Left err -> print err
13 Right defs -> do
25 Right defs -> do