554c395 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Made a start on the high level language

commit554c3952175f3a2298e6626e41fa85b16f7bef49 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 4 Oct 2011, 14:51 (15 years ago) parentff5f762

6 files changed+175−29

compare with master

unifiedsplit

miniidris.cabal+3−1 src/Core/Evaluate.hs+15−27 src/Core/TT.hs+17 src/Idris/AbsSyntax.hs+49 src/Idris/Parser.hs+78 src/Main.hs+13−1

miniidris.cabal+3−1

@@ -19,7 +19,9 @@ Executable miniidris

1919 hs-source-dirs: src

2020 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,

2121 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

2325

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

2527 containers

src/Core/Evaluate.hs+15−27

@@ -1,11 +1,10 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

33module Core.Evaluate(normalise,

4− Fun(..), Def(..), Context, toAlist,

5− emptyContext, addToCtxt, addConstant, addDatatype,

4+ Fun(..), Def(..), Context,

5+ addToCtxt, addConstant, addDatatype,

66 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv) where

8−import qualified Data.Map as Map

98import Debug.Trace

109import Core.TT

1110

@@ -94,36 +93,25 @@ wknV i t = t

9493data Fun = Fun Type Value Term Value

9594 deriving Show

9695

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+

97102data Def = Function Fun

98103 | Constant NameType Type Value

99− deriving Show

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−-}

104+ | Operator Type [(Term, Term)] ([Value] -> Maybe Value)

112105

113−type Context = Map.Map Name Def

114−emptyContext = Map.empty

115−

116−addDef :: Name -> Def -> Context -> Context

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

106+instance Show Def where

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

108+ show (Constant nt ty val) = "Constant: " ++ show nt ++ " " ++ show ty

109+ show (Operator ty ps _) = "Operator: " ++ show ty ++ " " ++ show ps

124110

125111-------

126112

113+type Context = Ctxt Def

114+

127115addToCtxt :: Name -> Term -> Type -> Context -> Context

128116addToCtxt n tm ty ctxt = addDef n (Function (Fun ty (eval ctxt [] ty)

129117 tm (eval ctxt [] tm))) ctxt

src/Core/TT.hs+17

@@ -4,6 +4,7 @@ module Core.TT where

55import Control.Monad.State

66import Debug.Trace

7+import qualified Data.Map as Map

89{- The language has:

910 * Full dependent types

@@ -61,6 +62,22 @@ instance Show Name where

6162 show (UN (n:ns)) = show (UN [n]) ++ "." ++ show (UN ns)

6263 show (MN i s) = "{" ++ s ++ show i ++ "}"

6364

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+

6481data Raw = Var Name

6582 | RBind Name (Binder Raw) Raw

6683 | RApp Raw Raw

src/Idris/AbsSyntax.hsnew file+49

@@ -0,0 +1,49 @@

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}

3+module Idris.AbsSyntax where

5+import Core.TT

6+import Core.Evaluate

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

3+import Idris.AbsSyntax

5+import Core.CoreParser

6+import Core.TT

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 @@

11module Main where

3+import System.Console.Readline

35import Core.CoreParser

46import Core.ShellParser

57import Core.TT

@@ -7,7 +9,17 @@ import Core.Typecheck

79import Core.ProofShell

810import Core.Evaluate

911

10−main = do f <- readFile "test.mi"

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'

22+ = do f <- readFile "test.mi"

1123 case parseFile f of

1224 Left err -> print err

1325 Right defs -> do