git.iko.soy/Idris-dev
on 2bdb46b help sign in
Idris-dev/src/Idris/Parser.hs
1337 lines 52 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2module Idris.Parser(module Idris.Parser,
3 module Idris.ParseExpr,
4 module Idris.ParseHelpers,
5 module Idris.ParseOps) where
7import Prelude hiding (pi)
9import Text.Trifecta.Delta
10import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
11import Text.Parser.LookAhead
12import Text.Parser.Expression
13import qualified Text.Parser.Token as Tok
14import qualified Text.Parser.Char as Chr
15import qualified Text.Parser.Token.Highlight as Hi
17import Idris.AbsSyntax
18import Idris.DSL
19import Idris.Imports
20import Idris.Error
21import Idris.ElabDecls
22import Idris.ElabTerm hiding (namespace, params)
23import Idris.Coverage
24import Idris.IBC
25import Idris.Unlit
26import Idris.Providers
28import Idris.ParseHelpers
29import Idris.ParseOps
30import Idris.ParseExpr
32import Paths_idris
34import Util.DynamicLinker
36import Core.TT
37import Core.Evaluate
39import Control.Applicative
40import Control.Monad
41import Control.Monad.State.Strict
43import Data.Maybe
44import qualified Data.List.Split as Spl
45import Data.List
46import Data.Monoid
47import Data.Char
48import qualified Data.HashSet as HS
49import qualified Data.Text as T
50import qualified Data.ByteString.UTF8 as UTF8
52import Debug.Trace
54import System.FilePath
55{-
56 grammar shortcut notation:
57 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
58 RULE? = optional rule (i.e. RULE or nothing)
59 RULE* = repeated rule (i.e. RULE zero or more times)
60 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
61 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
62 RULE{n} = rule repeated n times
63-}
65-- | Adds accessibility option for function
66addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
67addAcc n a = do i <- get
68 put (i { hide_list = (n, a) : hide_list i })
70{- | Add accessbility option for data declarations
71 (works for classes too - 'abstract' means the data/class is visible but members not) -}
72accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
73accData (Just Frozen) n ns = do addAcc n (Just Frozen)
74 mapM_ (\n -> addAcc n (Just Hidden)) ns
75accData a n ns = do addAcc n a
76 mapM_ (`addAcc` a) ns
79{- * Error reporting helpers -}
80{- | Error message with possible fixes list -}
81fixErrorMsg :: String -> [String] -> String
82fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
84{- * Main grammar -}
86{- | Parses module definition
87 ModuleHeader ::= 'module' Identifier_t ';'?;
88-}
89moduleHeader :: IdrisParser [String]
90moduleHeader = try (do reserved "module"
91 i <- identifier
92 option ';' (lchar ';')
93 return (moduleName i))
94 <|> return []
95 where moduleName x = case span (/='.') x of
96 (x, "") -> [x]
97 (x, '.':y) -> x : moduleName y
99{- | Parses an import statement
100 Import ::= 'import' Identifier_t ';'?;
101 -}
102import_ :: IdrisParser String
103import_ = do reserved "import"
104 id <- identifier
105 option ';' (lchar ';')
106 return (toPath id)
107 <?> "import statement"
108 where toPath f = foldl1' (</>) (Spl.splitOn "." f)
110{- | Parses program source
111 Prog ::= Decl* EOF;
112 -}
113prog :: SyntaxInfo -> IdrisParser [PDecl]
114prog syn = do whiteSpace
115 decls <- many (decl syn)
116 notOpenBraces
117 eof
118 let c = (concat decls)
119 return c
121{- | Parses a top-level declaration
122Decl ::=
123 Decl'
124 | Using
125 | Params
126 | Mutual
127 | Namespace
128 | Class
129 | Instance
130 | DSL
131 | Directive
132 | Provider
133 | Transform
134 | Import!
135 ;
136-}
137decl :: SyntaxInfo -> IdrisParser [PDecl]
138decl syn = do notEndBlock
139 declBody
140 where declBody :: IdrisParser [PDecl]
141 declBody = declBody'
142 <|> using_ syn
143 <|> params syn
144 <|> mutual syn
145 <|> namespace syn
146 <|> class_ syn
147 <|> instance_ syn
148 <|> do d <- dsl syn; return [d]
149 <|> directive syn
150 <|> provider syn
151 <|> transform syn
152 <|> do import_; fail "imports must be at top of file"
153 <?> "declaration"
154 declBody' :: IdrisParser [PDecl]
155 declBody' = do d <- decl' syn
156 i <- get
157 let d' = fmap (desugar syn i) d
158 return [d']
160{- | Parses a top-level declaration with possible syntax sugar
161Decl' ::=
162 Fixity
163 | FunDecl'
164 | Data
165 | Record
166 | SyntaxDecl
167 ;
168-}
169decl' :: SyntaxInfo -> IdrisParser PDecl
170decl' syn = fixity
171 <|> syntaxDecl syn
172 <|> fnDecl' syn
173 <|> data_ syn
174 <|> record syn
175 <?> "declaration"
177{- | Parses a syntax extension declaration (and adds the rule to parser state)
178 SyntaxDecl ::= SyntaxRule;
179-}
180syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
181syntaxDecl syn = do s <- syntaxRule syn
182 i <- get
183 let rs = syntax_rules i
184 let ns = syntax_keywords i
185 let ibc = ibc_write i
186 let ks = map show (names s)
187 put (i { syntax_rules = s : rs,
188 syntax_keywords = ks ++ ns,
189 ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
190 fc <- getFC
191 return (PSyntax fc s)
192 where names (Rule syms _ _) = mapMaybe ename syms
193 ename (Keyword n) = Just n
194 ename _ = Nothing
196{- | Parses a syntax extension declaration
197SyntaxRuleOpts ::= 'term' | 'pattern';
199SyntaxRule ::=
200 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
202SyntaxSym ::= '[' Name_t ']'
203 | '{' Name_t '}'
204 | Name_t
205 | StringLiteral_t
206 ;
207-}
208syntaxRule :: SyntaxInfo -> IdrisParser Syntax
209syntaxRule syn
210 = do sty <- try (do
211 pushIndent
212 sty <- option AnySyntax (do reserved "term"; return TermSyntax
213 <|> do reserved "pattern"; return PatternSyntax)
214 reserved "syntax"
215 return sty)
216 syms <- some syntaxSym
217 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
218 let ns = mapMaybe getName syms
219 when (length ns /= length (nub ns))
220 $ unexpected "repeated variable in syntax rule"
221 lchar '='
222 tm <- typeExpr (allowImp syn)
223 terminator
224 return (Rule (mkSimple syms) tm sty)
225 where
226 isExpr (Expr _) = True
227 isExpr _ = False
228 getName (Expr n) = Just n
229 getName _ = Nothing
230 -- Can't parse two full expressions (i.e. expressions with application) in a row
231 -- so change them both to a simple expression
232 mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
233 mkSimple xs = mkSimple' xs
235 mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
236 mkSimple es
237 mkSimple' (e : es) = e : mkSimple' es
238 mkSimple' [] = []
241{- | Parses a syntax symbol (either binding variable, keyword or expression)
242SyntaxSym ::= '[' Name_t ']'
243 | '{' Name_t '}'
244 | Name_t
245 | StringLiteral_t
246 ;
247 -}
248syntaxSym :: IdrisParser SSymbol
249syntaxSym = try (do lchar '['; n <- name; lchar ']'
250 return (Expr n))
251 <|> try (do lchar '{'; n <- name; lchar '}'
252 return (Binding n))
253 <|> do n <- iName []
254 return (Keyword n)
255 <|> do sym <- stringLiteral
256 return (Symbol sym)
257 <?> "syntax symbol"
259{- | Parses a function declaration with possible syntax sugar
260 FunDecl ::= FunDecl';
261-}
262fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
263fnDecl syn
264 = try (do notEndBlock
265 d <- fnDecl' syn
266 i <- get
267 let d' = fmap (desugar syn i) d
268 return [d'])
269 <?> "function declaration"
271{- Parses a function declaration
272 FunDecl' ::=
273 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
274 | Postulate
275 | Pattern
276 | CAF
277 ;
278-}
279fnDecl' :: SyntaxInfo -> IdrisParser PDecl
280fnDecl' syn = do (doc, fc, opts', n, acc) <- try (do
281 doc <- option "" (docComment '|')
282 pushIndent
283 ist <- get
284 let initOpts = if default_total ist
285 then [TotalFn]
286 else []
287 opts <- fnOpts initOpts
288 acc <- optional accessibility
289 opts' <- fnOpts opts
290 n_in <- fnName
291 let n = expandNS syn n_in
292 fc <- getFC
293 lchar ':'
294 return (doc, fc, opts', n, acc))
295 ty <- typeExpr (allowImp syn)
296 terminator
297 addAcc n acc
298 return (PTy doc syn fc opts' n ty)
299 <|> postulate syn
300 <|> caf syn
301 <|> pattern syn
302 <?> "function declaration"
305{- Parses function options given initial options
306FnOpts ::= 'total'
307 | 'partial'
308 | 'implicit'
309 | '%' 'assert_total'
310 | '%' 'reflection'
311 | '%' 'specialise' '[' NameTimesList? ']'
312 ;
314NameTimes ::= FnName Natural?;
316NameTimesList ::=
317 NameTimes
318 | NameTimes ',' NameTimesList
319 ;
321-}
322-- FIXME: Check compatability for function options (i.e. partal/total)
323fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
324fnOpts opts
325 = do reserved "total"; fnOpts (TotalFn : opts)
326 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
327 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
328 fnOpts (CExport c : opts)
329 <|> do try (lchar '%' *> reserved "assert_total");
330 fnOpts (AssertTotal : opts)
331 <|> do try (lchar '%' *> reserved "reflection");
332 fnOpts (Reflection : opts)
333 <|> do lchar '%'; reserved "specialise";
334 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
335 fnOpts (Specialise ns : opts)
336 <|> do reserved "implicit"; fnOpts (Implicit : opts)
337 <|> return opts
338 <?> "function modifier"
339 where nameTimes :: IdrisParser (Name, Maybe Int)
340 nameTimes = do n <- fnName
341 t <- option Nothing (do reds <- natural
342 return (Just (fromInteger reds)))
343 return (n, t)
345{- | Parses an accessibilty modifier (e.g. public, private) -}
346accessibility :: IdrisParser Accessibility
347accessibility = do reserved "public"; return Public
348 <|> do reserved "abstract"; return Frozen
349 <|> do reserved "private"; return Hidden
350 <?> "accessibility modifier"
354{- | Parses a postulate
356Postulate ::=
357 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
358 ;
359-}
360postulate :: SyntaxInfo -> IdrisParser PDecl
361postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
362 pushIndent
363 reserved "postulate"
364 return doc
365 ist <- get
366 let initOpts = if default_total ist
367 then [TotalFn]
368 else []
369 opts <- fnOpts initOpts
370 acc <- optional accessibility
371 opts' <- fnOpts opts
372 n_in <- fnName
373 let n = expandNS syn n_in
374 lchar ':'
375 ty <- typeExpr (allowImp syn)
376 fc <- getFC
377 terminator
378 addAcc n acc
379 return (PPostulate doc syn fc opts' n ty)
380 <?> "postulate"
382{- | Parses a using declaration
384Using ::=
385 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
386 ;
387 -}
388using_ :: SyntaxInfo -> IdrisParser [PDecl]
389using_ syn =
390 do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
391 openBlock
392 let uvars = using syn
393 ds <- many (decl (syn { using = uvars ++ ns }))
394 closeBlock
395 return (concat ds)
396 <?> "using declaration"
398{- | Parses a parameters declaration
400Params ::=
401 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
402 ;
403 -}
404params :: SyntaxInfo -> IdrisParser [PDecl]
405params syn =
406 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
407 openBlock
408 let pvars = syn_params syn
409 ds <- many (decl syn { syn_params = pvars ++ ns })
410 closeBlock
411 fc <- getFC
412 return [PParams fc ns (concat ds)]
413 <?> "parameters declaration"
415{- | Parses a mutual declaration (for mutually recursive functions)
417Mutual ::=
418 'mutual' OpenBlock Decl* CloseBlock
419 ;
420-}
421mutual :: SyntaxInfo -> IdrisParser [PDecl]
422mutual syn =
423 do reserved "mutual"
424 openBlock
425 let pvars = syn_params syn
426 ds <- many (decl syn)
427 closeBlock
428 fc <- getFC
429 return [PMutual fc (concat ds)]
430 <?> "mutual block"
432{- | Parses a namespace declaration
434Namespace ::=
435 'namespace' identifier OpenBlock Decl+ CloseBlock
436 ;
437-}
438namespace :: SyntaxInfo -> IdrisParser [PDecl]
439namespace syn =
440 do reserved "namespace"; n <- identifier;
441 openBlock
442 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
443 closeBlock
444 return [PNamespace n (concat ds)]
445 <?> "namespace declaration"
447{- | Parses a fixity declaration
449Fixity ::=
450 FixityType Natural_t OperatorList Terminator
451 ;
452-}
453fixity :: IdrisParser PDecl
454fixity = do pushIndent
455 f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
456 terminator
457 let prec = fromInteger i
458 istate <- get
459 let infixes = idris_infixes istate
460 let fs = map (Fix (f prec)) ops
461 let redecls = map (alreadyDeclared infixes) fs
462 let ill = filter (not . checkValidity) redecls
463 if null ill
464 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
465 , ibc_write = map IBCFix fs ++ ibc_write istate
466 })
467 fc <- getFC
468 return (PFix fc (f prec) ops)
469 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
470 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
471 <?> "fixity declaration"
472 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
473 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
475 checkValidity :: (FixDecl, [FixDecl]) -> Bool
476 checkValidity (f, fs) = all (== f) fs
478 extractName :: FixDecl -> String
479 extractName (Fix _ n) = n
481{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
482FixityType ::=
483 'infixl'
484 | 'infixr'
485 | 'infix'
486 | 'prefix'
487 ;
488 -}
489fixityType :: IdrisParser (Int -> Fixity)
490fixityType = do reserved "infixl"; return Infixl
491 <|> do reserved "infixr"; return Infixr
492 <|> do reserved "infix"; return InfixN
493 <|> do reserved "prefix"; return PrefixN
494 <?> "fixity type"
496{- |Parses a methods block (for type classes and instances)
497 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
498 -}
499methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
500methodsBlock syn = do reserved "where"
501 openBlock
502 ds <- many (fnDecl syn)
503 closeBlock
504 return (concat ds)
505 <?> "methods block"
507{- |Parses a type class declaration
509ClassArgument ::=
510 Name
511 | '(' Name ':' Expr ')'
512 ;
514Class ::=
515 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
516 ;
517-}
518class_ :: SyntaxInfo -> IdrisParser [PDecl]
519class_ syn = do (doc, acc) <- try (do
520 doc <- option "" (docComment '|')
521 acc <- optional accessibility
522 return (doc, acc))
523 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
524 let n = expandNS syn n_in
525 cs <- many carg
526 ds <- option [] (methodsBlock syn)
527 accData acc n (concatMap declared ds)
528 return [PClass doc syn fc cons n cs ds]
529 <?> "type-class declaration"
530 where
531 carg :: IdrisParser (Name, PTerm)
532 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
533 return (i, ty)
534 <|> do i <- name;
535 return (i, PType)
537{- |Parses a type class instance declaration
539 Instance ::=
540 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
541 ;
543 InstanceName ::= '[' Name ']';
544-}
545instance_ :: SyntaxInfo -> IdrisParser [PDecl]
546instance_ syn = do reserved "instance"; fc <- getFC
547 en <- optional instanceName
548 cs <- constraintList syn
549 cn <- name
550 args <- many (simpleExpr syn)
551 let sc = PApp fc (PRef fc cn) (map pexp args)
552 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
553 ds <- option [] (methodsBlock syn)
554 return [PInstance syn fc cs cn args t en ds]
555 <?> "instance declaratioN"
556 where instanceName :: IdrisParser Name
557 instanceName = do lchar '['; n_in <- fnName; lchar ']'
558 let n = expandNS syn n_in
559 return n
560 <?> "instance name"
563{- | Parses a using declaration list
564UsingDeclList ::=
565 UsingDeclList'
566 | NameList TypeSig
567 ;
569UsingDeclList' ::=
570 UsingDecl
571 | UsingDecl ',' UsingDeclList'
572 ;
574NameList ::=
575 Name
576 | Name ',' NameList
577 ;
578-}
579usingDeclList :: SyntaxInfo -> IdrisParser [Using]
580usingDeclList syn
581 = try (sepBy1 (usingDecl syn) (lchar ','))
582 <|> do ns <- sepBy1 name (lchar ',')
583 lchar ':'
584 t <- typeExpr (disallowImp syn)
585 return (map (\x -> UImplicit x t) ns)
586 <?> "using declaration list"
588{- |Parses a using declaration
589UsingDecl ::=
590 FnName TypeSig
591 | FnName FnName+
592 ;
593-}
594usingDecl :: SyntaxInfo -> IdrisParser Using
595usingDecl syn = try (do x <- fnName
596 lchar ':'
597 t <- typeExpr (disallowImp syn)
598 return (UImplicit x t))
599 <|> do c <- fnName
600 xs <- some fnName
601 return (UConstraint c xs)
602 <?> "using declaration"
604{- |Parses a record type declaration
605Record ::=
606 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
607-}
608record :: SyntaxInfo -> IdrisParser PDecl
609record syn = do (doc, acc) <- try (do
610 doc <- option "" (docComment '|')
611 acc <- optional accessibility
612 reserved "record"
613 return (doc, acc))
614 fc <- getFC
615 tyn_in <- fnName
616 lchar ':'
617 ty <- typeExpr (allowImp syn)
618 let tyn = expandNS syn tyn_in
619 reserved "where"
620 (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
621 accData acc tyn [cn]
622 let rsyn = syn { syn_namespace = show (nsroot tyn) :
623 syn_namespace syn }
624 let fns = getRecNames rsyn cty
625 mapM_ (\n -> addAcc n acc) fns
626 return $ PRecord doc rsyn fc tyn ty cdoc cn cty
627 <?> "record type declaration"
628 where
629 getRecNames :: SyntaxInfo -> PTerm -> [Name]
630 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
631 ++ getRecNames syn sc
632 getRecNames _ _ = []
634 toFreeze :: Maybe Accessibility -> Maybe Accessibility
635 toFreeze (Just Frozen) = Just Hidden
636 toFreeze x = x
638{- | Parses data declaration type (normal or codata)
639DataI ::= 'data' | 'codata';
640-}
641dataI :: IdrisParser Bool
642dataI = do reserved "data"; return False
643 <|> do reserved "codata"; return True
645{- | Parses a data type declaration
646Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
647 | DocComment? Accessibility? DataI FnName Name* DataRest?
648 ;
649Constructor' ::= Constructor KeepTerminator;
650ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
652DataRest ::= '=' SimpleConstructorList Terminator
653  | 'where'!
654 ;
655SimpleConstructorList ::=
656 SimpleConstructor
657 | SimpleConstructor '|' SimpleConstructorList
658 ;
659-}
660data_ :: SyntaxInfo -> IdrisParser PDecl
661data_ syn = do (doc, acc, co) <- try (do
662 doc <- option "" (docComment '|')
663 pushIndent
664 acc <- optional accessibility
665 co <- dataI
666 return (doc, acc, co))
667 fc <- getFC
668 tyn_in <- fnName
669 (do try (lchar ':')
670 popIndent
671 ty <- typeExpr (allowImp syn)
672 let tyn = expandNS syn tyn_in
673 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
674 reserved "where"
675 cons <- indentedBlock (constructor syn)
676 accData acc tyn (map (\ (_, n, _, _) -> n) cons)
677 return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do
678 args <- many name
679 let ty = bindArgs (map (const PType) args) PType
680 let tyn = expandNS syn tyn_in
681 option (PData doc syn fc co (PLaterdecl tyn ty)) (do
682 try (lchar '=') <|> do reserved "where"
683 let kw = (if co then "co" else "") ++ "data "
684 let n = show tyn_in ++ " "
685 let s = kw ++ n
686 let as = concat (intersperse " " $ map show args) ++ " "
687 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
688 let ss = concat (intersperse " -> " $ map (const "Type") args)
689 let fix1 = s ++ as ++ " = ..."
690 let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
691 let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
692 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
693 cons <- sepBy1 (simpleConstructor syn) (lchar '|')
694 terminator
695 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
696 cons' <- mapM (\ (doc, x, cargs, cfc) ->
697 do let cty = bindArgs cargs conty
698 return (doc, x, cty, cfc)) cons
699 accData acc tyn (map (\ (_, n, _, _) -> n) cons')
700 return $ PData doc syn fc co (PDatadecl tyn ty cons')))
701 <?> "data type declaration"
702 where
703 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
704 mkPApp fc t [] = t
705 mkPApp fc t xs = PApp fc t (map pexp xs)
706 bindArgs :: [PTerm] -> PTerm -> PTerm
707 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
710{- | Parses a type constructor declaration
711 Constructor ::= DocComment? FnName TypeSig;
712-}
713constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
714constructor syn
715 = do doc <- option "" (docComment '|')
716 cn_in <- fnName; fc <- getFC
717 let cn = expandNS syn cn_in
718 lchar ':'
719 ty <- typeExpr (allowImp syn)
720 return (doc, cn, ty, fc)
721 <?> "constructor"
723{- | Parses a constructor for simple discriminative union data types
724 SimpleConstructor ::= FnName SimpleExpr* DocComment?
725-}
726simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
727simpleConstructor syn
728 = do cn_in <- fnName
729 let cn = expandNS syn cn_in
730 fc <- getFC
731 args <- many (do notEndApp
732 simpleExpr syn)
733 doc <- option "" (docComment '^')
734 return (doc, cn, args, fc)
735 <?> "constructor"
737{- | Parses a dsl block declaration
738DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
739 -}
740dsl :: SyntaxInfo -> IdrisParser PDecl
741dsl syn = do reserved "dsl"
742 n <- fnName
743 bs <- indentedBlock (overload syn)
744 let dsl = mkDSL bs (dsl_info syn)
745 checkDSL dsl
746 i <- get
747 put (i { idris_dsls = addDef n dsl (idris_dsls i) })
748 return (PDSL n dsl)
749 <?> "dsl block declaration"
750 where mkDSL :: [(String, PTerm)] -> DSL -> DSL
751 mkDSL bs dsl = let var = lookup "variable" bs
752 first = lookup "index_first" bs
753 next = lookup "index_next" bs
754 leto = lookup "let" bs
755 lambda = lookup "lambda" bs in
756 initDSL { dsl_var = var,
757 index_first = first,
758 index_next = next,
759 dsl_lambda = lambda,
760 dsl_let = leto }
762{- | Checks DSL for errors -}
763-- FIXME: currently does nothing, check if DSL is really sane
764checkDSL :: DSL -> IdrisParser ()
765checkDSL dsl = return ()
767{- | Parses a DSL overload declaration
768OverloadIdentifier ::= 'let' | Identifier;
769Overload ::= OverloadIdentifier '=' Expr;
770-}
771overload :: SyntaxInfo -> IdrisParser (String, PTerm)
772overload syn = do o <- identifier <|> do reserved "let"
773 return "let"
774 if o `notElem` overloadable
775 then fail $ show o ++ " is not an overloading"
776 else do
777 lchar '='
778 t <- expr syn
779 return (o, t)
780 <?> "dsl overload declaratioN"
781 where overloadable = ["let","lambda","index_first","index_next","variable"]
783{- | Parse a clause with patterns
784Pattern ::= Clause;
785-}
786pattern :: SyntaxInfo -> IdrisParser PDecl
787pattern syn = do fc <- getFC
788 clause <- clause syn
789 return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
790 <?> "pattern"
792{- | Parse a constant applicative form declaration
793 CAF ::= 'let' FnName '=' Expr Terminator;
794-}
795caf :: SyntaxInfo -> IdrisParser PDecl
796caf syn = do reserved "let"
797 n_in <- fnName; let n = expandNS syn n_in
798 lchar '='
799 t <- expr syn
800 terminator
801 fc <- getFC
802 return (PCAF fc n t)
803 <?> "constant applicative form declaration"
805{- | Parse an argument expression
806 ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
807-}
808argExpr :: SyntaxInfo -> IdrisParser PTerm
809argExpr syn = let syn' = syn { inPattern = True } in
810 try (hsimpleExpr syn') <|> simpleExternalExpr syn'
811 <?> "argument expression"
813{- | Parse a right hand side of a function
814RHS ::= '=' Expr
815 | '?=' RHSName? Expr
816 | 'impossible'
817 ;
819RHSName ::= '{' FnName '}';
820-}
821rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
822rhs syn n = do lchar '='; expr syn
823 <|> do symbol "?=";
824 name <- option n' (do symbol "{"; n <- fnName; symbol "}";
825 return n)
826 r <- expr syn
827 return (addLet name r)
828 <|> do reserved "impossible"; return PImpossible
829 <?> "function right hand side"
830 where mkN :: Name -> Name
831 mkN (UN x) = UN (x++"_lemma_1")
832 mkN (NS x n) = NS (mkN x) n
833 n' :: Name
834 n' = mkN n
835 addLet :: Name -> PTerm -> PTerm
836 addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
837 addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
838 where addLetC (l, r) = (l, addLet nm r)
839 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
841{- |Parses a function clause
842RHSOrWithBlock ::= RHS WhereOrTerminator
843 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
844 ;
845Clause ::= WExpr+ RHSOrWithBlock
846 | SimpleExpr '<==' FnName RHS WhereOrTerminator
847 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
848 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
849 ;
850ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
851WhereOrTerminator ::= WhereBlock | Terminator;
852-}
853clause :: SyntaxInfo -> IdrisParser PClause
854clause syn
855 = do wargs <- try (do pushIndent; some (wExpr syn))
856 fc <- getFC
857 ist <- get
858 n <- case lastParse ist of
859 Just t -> return t
860 Nothing -> fail "Invalid clause"
861 (do r <- rhs syn n
862 let ctxt = tt_ctxt ist
863 let wsyn = syn { syn_namespace = [] }
864 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
865 popIndent
866 return x,
867 do terminator
868 return ([], [])]
869 return $ PClauseR fc wargs r wheres) <|> (do
870 popIndent
871 reserved "with"
872 wval <- simpleExpr syn
873 openBlock
874 ds <- some $ fnDecl syn
875 let withs = concat ds
876 closeBlock
877 return $ PWithR fc wargs wval withs)
878 <|> do ty <- try (do pushIndent
879 ty <- simpleExpr syn
880 symbol "<=="
881 return ty)
882 fc <- getFC
883 n_in <- fnName; let n = expandNS syn n_in
884 r <- rhs syn n
885 ist <- get
886 let ctxt = tt_ctxt ist
887 let wsyn = syn { syn_namespace = [] }
888 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
889 popIndent
890 return x,
891 do terminator
892 return ([], [])]
893 let capp = PLet (MN 0 "match")
894 ty
895 (PMatchApp fc n)
896 (PRef fc (MN 0 "match"))
897 ist <- get
898 put (ist { lastParse = Just n })
899 return $ PClause fc n capp [] r wheres
900 <|> do (l, op) <- try (do
901 pushIndent
902 l <- argExpr syn
903 op <- operator
904 when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
905 return (l, op))
906 let n = expandNS syn (UN op)
907 r <- argExpr syn
908 fc <- getFC
909 wargs <- many (wExpr syn)
910 (do rs <- rhs syn n
911 let wsyn = syn { syn_namespace = [] }
912 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
913 popIndent
914 return x,
915 do terminator
916 return ([], [])]
917 ist <- get
918 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
919 put (ist { lastParse = Just n })
920 return $ PClause fc n capp wargs rs wheres) <|> (do
921 popIndent
922 reserved "with"
923 lchar '(' <?> "parenthesized expression"
924 wval <- bracketed syn
925 openBlock
926 ds <- some $ fnDecl syn
927 closeBlock
928 ist <- get
929 let capp = PApp fc (PRef fc n) [pexp l, pexp r]
930 let withs = map (fillLHSD n capp wargs) $ concat ds
931 put (ist { lastParse = Just n })
932 return $ PWith fc n capp wargs wval withs)
933 <|> do pushIndent
934 n_in <- fnName; let n = expandNS syn n_in
935 cargs <- many (constraintArg syn)
936 fc <- getFC
937 args <- many (try (implicitArg (syn { inPattern = True } ))
938 <|> (fmap pexp (argExpr syn)))
939 wargs <- many (wExpr syn)
940 let capp = PApp fc (PRef fc n)
941 (cargs ++ args)
942 (do r <- rhs syn n
943 ist <- get
944 let ctxt = tt_ctxt ist
945 let wsyn = syn { syn_namespace = [] }
946 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
947 popIndent
948 return x,
949 do terminator
950 return ([], [])]
951 ist <- get
952 put (ist { lastParse = Just n })
953 return $ PClause fc n capp wargs r wheres) <|> (do
954 reserved "with"
955 ist <- get
956 put (ist { lastParse = Just n })
957 lchar '(' <?> "parenthesized expression"
958 wval <- bracketed syn
959 openBlock
960 ds <- some $ fnDecl syn
961 let withs = map (fillLHSD n capp wargs) $ concat ds
962 closeBlock
963 popIndent
964 return $ PWith fc n capp wargs wval withs)
965 <?> "function clause"
966 where
967 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
968 fillLHS n capp owargs (PClauseR fc wargs v ws)
969 = PClause fc n capp (owargs ++ wargs) v ws
970 fillLHS n capp owargs (PWithR fc wargs v ws)
971 = PWith fc n capp (owargs ++ wargs) v
972 (map (fillLHSD n capp (owargs ++ wargs)) ws)
973 fillLHS _ _ _ c = c
975 fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
976 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
977 fillLHSD n c a x = x
979{- |Parses with pattern
980 WExpr ::= '|' Expr';
981-}
982wExpr :: SyntaxInfo -> IdrisParser PTerm
983wExpr syn = do lchar '|'
984 expr' syn
985 <?> "with pattern"
987{- |Parses a where block
988WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
989 -}
990whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
991whereBlock n syn
992 = do reserved "where"
993 ds <- indentedBlock1 (decl syn)
994 let dns = concatMap (concatMap declared) ds
995 return (concat ds, map (\x -> (x, decoration syn x)) dns)
996 <?> "where block"
998{- |Parses a code generation target language name
999Codegen ::= 'C'
1000 | 'Java'
1001 | 'JavaScript'
1002 | 'Node'
1003 | 'LLVM'
1004 | 'Bytecode'
1007codegen_ :: IdrisParser Codegen
1008codegen_ = do reserved "C"; return ViaC
1009 <|> do reserved "Java"; return ViaJava
1010 <|> do reserved "JavaScript"; return ViaJavaScript
1011 <|> do reserved "Node"; return ViaNode
1012 <|> do reserved "LLVM"; return ViaLLVM
1013 <|> do reserved "Bytecode"; return Bytecode
1014 <?> "code generation language"
1016{- |Parses a compiler directive
1017StringList ::=
1018 String
1019 | String ',' StringList
1022Directive ::= '%' Directive';
1024Directive' ::= 'lib' CodeGen String_t
1025 | 'link' CodeGen String_t
1026 | 'flag' CodeGen String_t
1027 | 'include' CodeGen String_t
1028 | 'hide' Name
1029 | 'freeze' Name
1030 | 'access' Accessibility
1031 | 'default' Totality
1032 | 'logging' Natural
1033 | 'dynamic' StringList
1034 | 'language' 'TypeProviders'
1035 | 'language' 'ErrorReflection'
1038directive :: SyntaxInfo -> IdrisParser [PDecl]
1039directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
1040 return [PDirective (do addLib cgn lib
1041 addIBC (IBCLib cgn lib))]
1042 <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
1043 return [PDirective (do dirs <- allImportDirs
1044 o <- liftIO $ findInPath dirs obj
1045 addIBC (IBCObj cgn obj) -- just name, search on loading ibc
1046 addObjectFile cgn o)]
1047 <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
1048 flag <- stringLiteral
1049 return [PDirective (do addIBC (IBCCGFlag cgn flag)
1050 addFlag cgn flag)]
1051 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
1052 return [PDirective (do addHdr cgn hdr
1053 addIBC (IBCHeader cgn hdr))]
1054 <|> do try (lchar '%' *> reserved "hide"); n <- iName []
1055 return [PDirective (do setAccessibility n Hidden
1056 addIBC (IBCAccess n Hidden))]
1057 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
1058 return [PDirective (do setAccessibility n Frozen
1059 addIBC (IBCAccess n Frozen))]
1060 <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
1061 return [PDirective (do i <- get
1062 put(i { default_access = acc }))]
1063 <|> do try (lchar '%' *> reserved "default"); tot <- totality
1064 i <- get
1065 put (i { default_total = tot } )
1066 return [PDirective (do i <- get
1067 put(i { default_total = tot }))]
1068 <|> do try (lchar '%' *> reserved "logging"); i <- natural;
1069 return [PDirective (setLogLevel (fromInteger i))]
1070 <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
1071 return [PDirective (do added <- addDyLib libs
1072 case added of
1073 Left lib -> addIBC (IBCDyLib (lib_name lib))
1074 Right msg ->
1075 fail $ msg)]
1076 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
1077 return [PDirective (addLangExt ext)]
1078 <?> "directive"
1080pLangExt :: IdrisParser LanguageExt
1081pLangExt = (reserved "TypeProviders" >> return TypeProviders)
1082 <|> (reserved "ErrorReflection" >> return ErrorReflection)
1084{- | Parses a totality
1085Totality ::= 'partial' | 'total'
1087totality :: IdrisParser Bool
1088totality
1089 = do reserved "total"; return True
1090 <|> do reserved "partial"; return False
1092{- | Parses a type provider
1093Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
1094 -}
1095provider :: SyntaxInfo -> IdrisParser [PDecl]
1096provider syn = do try (lchar '%' *> reserved "provide");
1097 lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1098 fc <- getFC
1099 reserved "with"
1100 e <- expr syn
1101 return [PProvider syn fc n t e]
1102 <?> "type provider"
1104{- | Parses a transform
1105Transform ::= '%' 'transform' Expr '==>' Expr
1107transform :: SyntaxInfo -> IdrisParser [PDecl]
1108transform syn = do try (lchar '%' *> reserved "transform")
1109 -- leave it unchecked, until we work out what this should
1110 -- actually mean...
1111-- safety <- option True (do reserved "unsafe"
1112-- return False)
1113 l <- expr syn
1114 fc <- getFC
1115 symbol "==>"
1116 r <- expr syn
1117 return [PTransform fc False l r]
1118 <?> "transform"
1121{- * Loading and parsing -}
1122{- | Parses an expression from input -}
1123parseExpr :: IState -> String -> Result PTerm
1124parseExpr st = parseString (runInnerParser (evalStateT (fullExpr defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
1126{- | Parses a tactic from input -}
1127parseTactic :: IState -> String -> Result PTactic
1128parseTactic st = parseString (runInnerParser (evalStateT (fullTactic defaultSyntax) st)) (Directed (UTF8.fromString "(input)") 0 0 0 0)
1130-- | Parse module header and imports
1131parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
1132parseImports fname input
1133 = do i <- getIState
1134 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1135 Failure err -> fail (show err)
1136 Success (x, i) -> do -- Discard state updates (there should be
1137 -- none anyway)
1138 return x
1139 where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
1140 imports = do whiteSpace
1141 mname <- moduleHeader
1142 ps <- many import_
1143 mrk <- mark
1144 isEof <- lookAheadMatches eof
1145 let mrk' = if isEof
1146 then Nothing
1147 else Just mrk
1148 i <- get
1149 return ((mname, ps, mrk'), i)
1152-- | A program is a list of declarations, possibly with associated
1153-- documentation strings.
1154parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
1155 Idris [PDecl]
1156parseProg syn fname input mrk
1157 = do i <- getIState
1158 case parseString (runInnerParser (evalStateT mainProg i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
1159 Failure doc -> do iputStrLn (show doc)
1160 -- FIXME: Get error location from trifecta
1161 --let errl = sourceLine (errorPos err)
1162 i <- getIState
1163 putIState (i { errLine = Just 0 }) -- Just errl })
1164 return []
1165 Success (x, i) -> do putIState i
1166 return $ collect x
1167 where mainProg :: IdrisParser ([PDecl], IState)
1168 mainProg = case mrk of
1169 Nothing -> do i <- get; return ([], i)
1170 Just mrk -> do
1171 release mrk
1172 ds <- prog syn
1173 i' <- get
1174 return (ds, i')
1176-- | Collect 'PClauses' with the same function name
1177collect :: [PDecl] -> [PDecl]
1178collect (c@(PClauses _ o _ _) : ds)
1179 = clauses (cname c) [] (c : ds)
1180 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
1181 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
1182 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
1183 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
1184 | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
1185 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
1186 clauses Nothing acc (x:xs) = collect xs
1187 clauses Nothing acc [] = []
1189 cname :: PDecl -> Maybe Name
1190 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
1191 cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
1192 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
1193 cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
1194 fcOf :: PDecl -> FC
1195 fcOf (PClauses fc _ _ _) = fc
1196collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
1197collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
1198collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
1199collect (PClass doc f s cs n ps ds : ds')
1200 = PClass doc f s cs n ps (collect ds) : collect ds'
1201collect (PInstance f s cs n ps t en ds : ds')
1202 = PInstance f s cs n ps t en (collect ds) : collect ds'
1203collect (d : ds) = d : collect ds
1204collect [] = []
1206{- | Load idris module -}
1207loadModule :: FilePath -> Idris String
1208loadModule f
1209 = idrisCatch (do i <- getIState
1210 let file = takeWhile (/= ' ') f
1211 ibcsd <- valIBCSubDir i
1212 ids <- allImportDirs
1213 fp <- liftIO $ findImport ids ibcsd file
1214 if file `elem` imported i
1215 then iLOG $ "Already read " ++ file
1216 else do putIState (i { imported = file : imported i })
1217 case fp of
1218 IDR fn -> loadSource False fn
1219 LIDR fn -> loadSource True fn
1220 IBC fn src ->
1221 idrisCatch (loadIBC fn)
1222 (\c -> do iLOG $ fn ++ " failed " ++ show c
1223 case src of
1224 IDR sfn -> loadSource False sfn
1225 LIDR sfn -> loadSource True sfn)
1226 let (dir, fh) = splitFileName file
1227 return (dropExtension fh))
1228 (\e -> do let msg = show e
1229 setErrLine (getErrLine msg)
1230 iputStrLn msg
1231 return "")
1233{- | Load idris code from file -}
1234loadFromIFile :: IFileType -> Idris ()
1235loadFromIFile i@(IBC fn src)
1236 = do iLOG $ "Skipping " ++ getSrcFile i
1237 idrisCatch (loadIBC fn)
1238 (\c -> do fail $ fn ++ " failed " ++ show c)
1239 where
1240 getSrcFile (IDR fn) = fn
1241 getSrcFile (LIDR fn) = fn
1242 getSrcFile (IBC f src) = getSrcFile src
1244loadFromIFile (IDR fn) = loadSource' False fn
1245loadFromIFile (LIDR fn) = loadSource' True fn
1247{-| Load idris source code and show error if something wrong happens -}
1248loadSource' :: Bool -> FilePath -> Idris ()
1249loadSource' lidr r
1250 = idrisCatch (loadSource lidr r)
1251 (\e -> do let msg = show e
1252 setErrLine (getErrLine msg)
1253 iputStrLn msg)
1255{- | Load Idris source code-}
1256loadSource :: Bool -> FilePath -> Idris ()
1257loadSource lidr f
1258 = do iLOG ("Reading " ++ f)
1259 i <- getIState
1260 let def_total = default_total i
1261 file_in <- liftIO $ readFile f
1262 file <- if lidr then tclift $ unlit f file_in else return file_in
1263 (mname, modules, pos) <- parseImports f file
1264 i <- getIState
1265 putIState (i { default_access = Hidden })
1266 clearIBC -- start a new .ibc file
1267 mapM_ (addIBC . IBCImport) modules
1268 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
1269 f file pos
1270 unless (null ds') $ do
1271 let ds = namespaces mname ds'
1272 logLvl 3 (dumpDecls ds)
1273 i <- getIState
1274 logLvl 10 (show (toAlist (idris_implicits i)))
1275 logLvl 3 (show (idris_infixes i))
1276 -- Now add all the declarations to the context
1277 v <- verbose
1278 when v $ iputStrLn $ "Type checking " ++ f
1279 -- we totality check after every Mutual block, so if
1280 -- anything is a single definition, wrap it in a
1281 -- mutual block on its own
1282 elabDecls toplevel (map toMutual ds)
1283 i <- getIState
1284 -- simplify every definition do give the totality checker
1285 -- a better chance
1286 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1287 updateContext (simplifyCasedef n))
1288 (map snd (idris_totcheck i))
1289 -- build size change graph from simplified definitions
1290 iLOG "Totality checking"
1291 i <- getIState
1292 mapM_ buildSCG (idris_totcheck i)
1293 mapM_ checkDeclTotality (idris_totcheck i)
1294 iLOG ("Finished " ++ f)
1295 ibcsd <- valIBCSubDir i
1296 iLOG "Universe checking"
1297 iucheck
1298 let ibc = ibcPathNoFallback ibcsd f
1299 i <- getIState
1300 addHides (hide_list i)
1301 ok <- noErrors
1302 when ok $
1303 idrisCatch (do writeIBC f ibc; clearIBC)
1304 (\c -> return ()) -- failure is harmless
1305 i <- getIState
1306 putIState (i { default_total = def_total,
1307 hide_list = [] })
1308 return ()
1309 return ()
1310 where
1311 namespaces :: [String] -> [PDecl] -> [PDecl]
1312 namespaces [] ds = ds
1313 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
1315 toMutual :: PDecl -> PDecl
1316 toMutual m@(PMutual _ d) = m
1317 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
1318 case x of
1319 PClauses _ _ _ _ -> r
1320 PClass _ _ _ _ _ _ _ -> r
1321 PInstance _ _ _ _ _ _ _ _ -> r
1322 _ -> x
1324{- | Adds names to hide list -}
1325addHides :: [(Name, Maybe Accessibility)] -> Idris ()
1326addHides xs = do i <- getIState
1327 let defh = default_access i
1328 let (hs, as) = partition isNothing xs
1329 unless (null as) $
1330 mapM_ doHide
1331 (map (\ (n, _) -> (n, defh)) hs ++
1332 map (\ (n, Just a) -> (n, a)) as)
1333 where isNothing (_, Nothing) = True
1334 isNothing _ = False
1336 doHide (n, a) = do setAccessibility n a
1337 addIBC (IBCAccess n a)