git.iko.soy/Idris-dev
on master help sign in
Change fixity declarations
commit70ac28d1ddeb297d7d5671c2a0f727146bb0b092 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 4 Oct 2011, 17:45 (15 years ago) parentaa85339
2 files changed+19−8
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+10−6 src/Idris/Parser.hs+9−2
src/Idris/AbsSyntax.hs+10−6
@@ -6,10 +6,8 @@ import Core.TT
66import Core.Evaluate
77
88data IState = IState { tt_ctxt :: Context,
9− tt_infixes :: [(String,
10− (Fixity, PTerm -> PTerm -> PTerm))]
9+ tt_infixes :: [FixDecl]
1110 }
12−
1311
1412{- Plan:
1513 Treat it as a theorem prover - one definition at a time, parse, elaborate,
@@ -20,12 +18,18 @@ data IState = IState { tt_ctxt :: Context,
2018
2119data Fixity = Infixl { prec :: Int }
2220 | Infixr { prec :: Int }
23− | InfixN { prec :: Int }
21+ | InfixN { prec :: Int }
2422 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+
2630data Plicity = Imp | Exp deriving Show
2731
28−data PDecl = PFix Fixity String -- fixity declaration
32+data PDecl = PFix Fixity String -- fixity declaration
2933 | PTy Name PTerm -- type declaration
3034 | PClause PTerm PTerm -- pattern clause
3135 | PData PData -- data declaration
src/Idris/Parser.hs+9−2
@@ -14,8 +14,15 @@ import Debug.Trace
1414
1515type TokenParser a = PTok.TokenParser a
1616
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+
1724lexer :: TokenParser ()
18−lexer = PTok.makeTokenParser haskellDef
25+lexer = PTok.makeTokenParser idrisDef
1926
2027whiteSpace= PTok.whiteSpace lexer
2128lexeme = PTok.lexeme lexer
@@ -47,6 +54,7 @@ pSimpleExpr =
4754 return $ PQuote t)
4855 <|> try (do x <- iName; return (PRef x))
4956 <|> try (do lchar '_'; return Placeholder)
57+ <|> try (do lchar '('; o <- operator; lchar ')'; return (PRef (UN [o])))
5058 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)
5159
5260pApp = do f <- pSimpleExpr
@@ -70,7 +78,6 @@ pPi = do lchar '('; x <- iName; t <- pTSig; lchar ')'
7078 sc <- pExpr
7179 return (PPi Imp x t sc)
7280
73−
7481table = [[binary "=" (\x y -> PApp (PRef (UN ["="])) [] [x,y]) AssocLeft],
7582 [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]
7683