git.iko.soy/Idris-dev
on master help sign in
Change fixity declarations
70ac28dEdwin Brady
src/Idris/AbsSyntax.hs+10−6
compare with master
unifiedsplit
@@ -6,10 +6,8 @@ import Core.TT
6import Core.Evaluate
6import Core.Evaluate
7
7
8data IState = IState { tt_ctxt :: Context,
8data IState = IState { tt_ctxt :: Context,
9− tt_infixes :: [(String,
9+ tt_infixes :: [FixDecl]
10− (Fixity, PTerm -> PTerm -> PTerm))]
11 }
10 }
12−
13
11
14{- Plan:
12{- Plan:
15 Treat it as a theorem prover - one definition at a time, parse, elaborate,
13 Treat it as a theorem prover - one definition at a time, parse, elaborate,
@@ -20,12 +18,18 @@ data IState = IState { tt_ctxt :: Context,
20
18
21data Fixity = Infixl { prec :: Int }
19data Fixity = Infixl { prec :: Int }
22 | Infixr { prec :: Int }
20 | Infixr { prec :: Int }
23− | InfixN { prec :: Int }
21+ | InfixN { prec :: Int }
24 deriving (Show, Eq)
22 deriving (Show, Eq)
25−
23+
24+data FixDecl = Fix Fixity String
25+ deriving (Show, Eq)
26+
27+instance Ord FixDecl where
28+ compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
29+
26data Plicity = Imp | Exp deriving Show
30data Plicity = Imp | Exp deriving Show
27
31
28−data PDecl = PFix Fixity String -- fixity declaration
32+data PDecl = PFix Fixity String -- fixity declaration
29 | PTy Name PTerm -- type declaration
33 | PTy Name PTerm -- type declaration
30 | PClause PTerm PTerm -- pattern clause
34 | PClause PTerm PTerm -- pattern clause
31 | PData PData -- data declaration
35 | PData PData -- data declaration
src/Idris/Parser.hs+9−2
@@ -14,8 +14,15 @@ import Debug.Trace
14
14
15type TokenParser a = PTok.TokenParser a
15type TokenParser a = PTok.TokenParser a
16
16
17+idrisDef = haskellDef {
18+ reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>"],
19+ reservedNames = ["let", "in", "data", "Set", "if", "then", "else",
20+ "do", "dsl", "import", "infix", "infixl", "infixr",
21+ "where", "forall"]
22+ }
23+
17lexer :: TokenParser ()
24lexer :: TokenParser ()
18−lexer = PTok.makeTokenParser haskellDef
25+lexer = PTok.makeTokenParser idrisDef
19
26
20whiteSpace= PTok.whiteSpace lexer
27whiteSpace= PTok.whiteSpace lexer
21lexeme = PTok.lexeme lexer
28lexeme = PTok.lexeme lexer
@@ -47,6 +54,7 @@ pSimpleExpr =
47 return $ PQuote t)
54 return $ PQuote t)
48 <|> try (do x <- iName; return (PRef x))
55 <|> try (do x <- iName; return (PRef x))
49 <|> try (do lchar '_'; return Placeholder)
56 <|> try (do lchar '_'; return Placeholder)
57+ <|> try (do lchar '('; o <- operator; lchar ')'; return (PRef (UN [o])))
50 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
58 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
51
59
52pApp = do f <- pSimpleExpr
60pApp = do f <- pSimpleExpr
@@ -70,7 +78,6 @@ pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
70 sc <- pExpr
78 sc <- pExpr
71 return (PPi Imp x t sc)
79 return (PPi Imp x t sc)
72
80
73−
74table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
81table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
75 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
82 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
76
83