module Core.Core import Core.Envimport Core.TTimport Data.Vectimport Parser.Support import public Control.Catchableimport public Data.IORefimport System %default covering public exportdata TTCErrorMsg    = Format String Int Int    | EndOfBuffer String    | Corrupt String public exportdata CaseError = DifferingArgNumbers               | DifferingTypes               | MatchErased (vars ** (Env Term vars, Term vars))               | NotFullyApplied Name               | UnknownType public exportdata DotReason = NonLinearVar               | VarApplied               | NotConstructor               | ErasedArg               | UserDotted               | UnknownDot exportShow DotReason where  show NonLinearVar = "Non linear pattern variable"  show VarApplied = "Variable applied to arguments"  show NotConstructor = "Not a constructor application or primitive"  show ErasedArg = "Erased argument"  show UserDotted = "User dotted"  show UnknownDot = "Unknown reason" -- All possible errors, carrying a locationpublic exportdata Error    = Fatal Error -- flag as unrecoverable (so don't postpone awaiting further info)    | CantConvert FC (Env Term vars) (Term vars) (Term vars)    | CantSolveEq FC (Env Term vars) (Term vars) (Term vars)    | PatternVariableUnifies FC (Env Term vars) Name (Term vars)    | CyclicMeta FC (Env Term vars) Name (Term vars)    | WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error    | ValidCase FC (Env Term vars) (Either (Term vars) Error)    | UndefinedName FC Name    | InvisibleName FC Name (Maybe (List String))    | BadTypeConType FC Name    | BadDataConType FC Name Name    | NotCovering FC Name Covering    | NotTotal FC Name PartialReason    | LinearUsed FC Nat Name    | LinearMisuse FC Name RigCount RigCount    | BorrowPartial FC (Env Term vars) (Term vars) (Term vars)    | BorrowPartialType FC (Env Term vars) (Term vars)    | AmbiguousName FC (List Name)    | AmbiguousElab FC (Env Term vars) (List (Term vars))    | AmbiguousSearch FC (Env Term vars) (List (Term vars))    | AmbiguityTooDeep FC Name (List Name)    | AllFailed (List (Maybe Name, Error))    | RecordTypeNeeded FC (Env Term vars)    | NotRecordField FC String (Maybe Name)    | NotRecordType FC Name    | IncompatibleFieldUpdate FC (List String)    | InvalidImplicits FC (Env Term vars) (List (Maybe Name)) (Term vars)    | TryWithImplicits FC (Env Term vars) (List (Name, Term vars))    | BadUnboundImplicit FC (Env Term vars) Name (Term vars)    | CantSolveGoal FC (Env Term vars) (Term vars)    | DeterminingArg FC Name Int (Env Term vars) (Term vars)    | UnsolvedHoles (List (FC, Name))    | CantInferArgType FC (Env Term vars) Name Name (Term vars)    | SolvedNamedHole FC (Env Term vars) Name (Term vars)    | VisibilityError FC Visibility Name Visibility Name    | NonLinearPattern FC Name    | BadPattern FC Name    | NoDeclaration FC Name    | AlreadyDefined FC Name    | NotFunctionType FC (Env Term vars) (Term vars)    | RewriteNoChange FC (Env Term vars) (Term vars) (Term vars)    | NotRewriteRule FC (Env Term vars) (Term vars)    | CaseCompile FC Name CaseError    | MatchTooSpecific FC (Env Term vars) (Term vars)    | BadDotPattern FC (Env Term vars) DotReason (Term vars) (Term vars)    | BadImplicit FC String    | BadRunElab FC (Env Term vars) (Term vars)    | GenericMsg FC String    | TTCError TTCErrorMsg    | FileErr String FileError    | ParseFail FC ParseError    | ModuleNotFound FC (List String)    | CyclicImports (List (List String))    | ForceNeeded    | InternalError String     | InType FC Name Error    | InCon FC Name Error    | InLHS FC Name Error    | InRHS FC Name Error exportShow TTCErrorMsg where  show (Format file ver exp) =    let age = if ver < exp then "older" else "newer" in        "TTC data is in an " ++ age ++ " format, file: " ++ file ++ ", expected version: " ++ show exp ++ ", actual version: " ++ show ver  show (EndOfBuffer when) = "End of buffer when reading " ++ when  show (Corrupt ty) = "Corrupt TTC data for " ++ ty -- Simplest possible display - higher level languages should unelaborate names-- and display annotations appropriatelyexportShow Error where  show (Fatal err) = show err  show (CantConvert fc env x y)      = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y  show (CantSolveEq fc env x y)      = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"  show (PatternVariableUnifies fc env n x)      = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x  show (CyclicMeta fc env n tm)      = show fc ++ ":Cycle detected in metavariable solution " ++ show n             ++ " = " ++ show tm  show (WhenUnifying fc _ x y err)      = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err  show (ValidCase fc _ prob)      = show fc ++ ":" ++           case prob of             Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"             Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)  show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x  show (InvisibleName fc x (Just ns))       = show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++         showSep "." (reverse ns) ++ " is not explicitly imported"  show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private"  show (BadTypeConType fc n)       = show fc ++ ":Return type of " ++ show n ++ " must be Type"  show (BadDataConType fc n fam)       = show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam  show (NotCovering fc n cov)       = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++            case cov of                 IsCovering => "Oh yes it is (Internal error!)"                 MissingCases cs => "Missing cases:\n\t" ++                                           showSep "\n\t" (map show cs)                 NonCoveringCall ns => "Calls non covering function"                                           ++ (case ns of                                                   [fn] => " " ++ show fn                                                   _ => "s: " ++ showSep ", " (map show ns))   show (NotTotal fc n r)       = show fc ++ ":" ++ show n ++ " is not total"  show (LinearUsed fc count n)      = show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n  show (LinearMisuse fc n exp ctx)      = show fc ++ ":Trying to use " ++ showRig exp ++ " name " ++ show n ++                   " in " ++ showRel ctx ++ " context"     where       showRig : RigCount -> String       showRig = elimSemi         "linear"         "irrelevant"         (const "unrestricted")        showRel : RigCount -> String       showRel = elimSemi         "relevant"         "irrelevant"         (const "non-linear")  show (BorrowPartial fc env t arg)      = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++                   " so must be fully applied"  show (BorrowPartialType fc env t)      = show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type"   show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns  show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts  show (AmbiguousSearch fc env ts) = show fc ++ ":Ambiguous search " ++ show ts  show (AmbiguityTooDeep fc n ns)      = show fc ++ ":Ambiguity too deep in " ++ show n ++ " " ++ show ns  show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)  show (RecordTypeNeeded fc env)      = show fc ++ ":Can't infer type of record to update"  show (NotRecordField fc fld Nothing)      = show fc ++ ":" ++ fld ++ " is not part of a record type"  show (NotRecordField fc fld (Just ty))      = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld  show (NotRecordType fc ty)      = show fc ++ ":" ++ show ty ++ " is not a record type"  show (IncompatibleFieldUpdate fc flds)      = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"  show (InvalidImplicits fc env ns tm)     = show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm  show (TryWithImplicits fc env imps)     = show fc ++ ":Need to bind implicits "          ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)          ++ "\n(The front end should probably have done this for you. Please report!)"  show (BadUnboundImplicit fc env n ty)      = show fc ++ ":Can't bind name " ++ nameRoot n ++                   " with type " ++ show ty  show (CantSolveGoal fc env g)      = show fc ++ ":Can't solve goal " ++ assert_total (show g)  show (DeterminingArg fc n i env g)      = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++                " since argument " ++ show n ++ " can't be inferred"  show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs  show (CantInferArgType fc env n h ty)      = show fc ++ ":Can't infer type for " ++ show n ++                   " (got " ++ show ty ++ " with hole " ++ show h ++ ")"  show (SolvedNamedHole fc _ h _) = show fc ++ ":Named hole " ++ show h ++ " is solved by unification"  show (VisibilityError fc vx x vy y)      = show fc ++ ":" ++ show vx ++ " " ++ show x ++ " cannot refer to "                       ++ show vy ++ " " ++ show y  show (NonLinearPattern fc n) = show fc ++ ":Non linear pattern variable " ++ show n  show (BadPattern fc n) = show fc ++ ":Pattern not allowed here: " ++ show n  show (NoDeclaration fc x) = show fc ++ ":No type declaration for " ++ show x  show (AlreadyDefined fc x) = show fc ++ ":" ++ show x ++ " is already defined"  show (NotFunctionType fc env tm) = show fc ++ ":Not a function type: " ++ show tm  show (RewriteNoChange fc env rule ty)      = show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty  show (NotRewriteRule fc env rule)      = show fc ++ ":" ++ show rule ++ " is not a rewrite rule type"  show (CaseCompile fc n DifferingArgNumbers)      = show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments"  show (CaseCompile fc n DifferingTypes)      = show fc ++ ":Patterns for " ++ show n ++ " require matching on different types"  show (CaseCompile fc n UnknownType)      = show fc ++ ":Can't infer type to match in " ++ show n  show (CaseCompile fc n (MatchErased (_ ** (env, tm))))      = show fc ++ ":Attempt to match on erased argument " ++ show tm ++                   " in " ++ show n  show (CaseCompile fc n (NotFullyApplied c))      = show fc ++ ":Constructor " ++ show c ++ " is not fully applied"  show (MatchTooSpecific fc env tm)      = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"  show (BadDotPattern fc env reason x y)      = show fc ++ ":Can't match on " ++ show x ++           " (" ++ show reason ++ ")" ++           " - it elaborates to " ++ show y  show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"  show (BadRunElab fc env script) = show fc ++ ":Bad elaborator script " ++ show script  show (GenericMsg fc str) = show fc ++ ":" ++ str  show (TTCError msg) = "Error in TTC file: " ++ show msg  show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err  show (ParseFail fc err) = "Parse error (" ++ show err ++ ")"  show (ModuleNotFound fc ns)      = show fc ++ ":" ++ showSep "." (reverse ns) ++ " not found"  show (CyclicImports ns)      = "Module imports form a cycle: " ++ showSep " -> " (map showMod ns)    where      showMod : List String -> String      showMod ns = showSep "." (reverse ns)  show ForceNeeded = "Internal error when resolving implicit laziness"  show (InternalError str) = "INTERNAL ERROR: " ++ str   show (InType fc n err)       = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++         show err  show (InCon fc n err)       = show fc ++ ":When elaborating type of constructor " ++ show n ++ ":\n" ++         show err  show (InLHS fc n err)       = show fc ++ ":When elaborating left hand side of " ++ show n ++ ":\n" ++         show err  show (InRHS fc n err)       = show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++         show err exportgetErrorLoc : Error -> Maybe FCgetErrorLoc (Fatal err) = getErrorLoc errgetErrorLoc (CantConvert loc _ _ _) = Just locgetErrorLoc (CantSolveEq loc _ _ _) = Just locgetErrorLoc (PatternVariableUnifies loc _ _ _) = Just locgetErrorLoc (CyclicMeta loc _ _ _) = Just locgetErrorLoc (WhenUnifying loc _ _ _ _) = Just locgetErrorLoc (ValidCase loc _ _) = Just locgetErrorLoc (UndefinedName loc _) = Just locgetErrorLoc (InvisibleName loc _ _) = Just locgetErrorLoc (BadTypeConType loc _) = Just locgetErrorLoc (BadDataConType loc _ _) = Just locgetErrorLoc (NotCovering loc _ _) = Just locgetErrorLoc (NotTotal loc _ _) = Just locgetErrorLoc (LinearUsed loc _ _) = Just locgetErrorLoc (LinearMisuse loc _ _ _) = Just locgetErrorLoc (BorrowPartial loc _ _ _) = Just locgetErrorLoc (BorrowPartialType loc _ _) = Just locgetErrorLoc (AmbiguousName loc _) = Just locgetErrorLoc (AmbiguousElab loc _ _) = Just locgetErrorLoc (AmbiguousSearch loc _ _) = Just locgetErrorLoc (AmbiguityTooDeep loc _ _) = Just locgetErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc xgetErrorLoc (AllFailed []) = NothinggetErrorLoc (RecordTypeNeeded loc _) = Just locgetErrorLoc (NotRecordField loc _ _) = Just locgetErrorLoc (NotRecordType loc _) = Just locgetErrorLoc (IncompatibleFieldUpdate loc _) = Just locgetErrorLoc (InvalidImplicits loc _ _ _) = Just locgetErrorLoc (TryWithImplicits loc _ _) = Just locgetErrorLoc (BadUnboundImplicit loc _ _ _) = Just locgetErrorLoc (CantSolveGoal loc _ _) = Just locgetErrorLoc (DeterminingArg loc _ _ _ _) = Just locgetErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just locgetErrorLoc (UnsolvedHoles []) = NothinggetErrorLoc (CantInferArgType loc _ _ _ _) = Just locgetErrorLoc (SolvedNamedHole loc _ _ _) = Just locgetErrorLoc (VisibilityError loc _ _ _ _) = Just locgetErrorLoc (NonLinearPattern loc _) = Just locgetErrorLoc (BadPattern loc _) = Just locgetErrorLoc (NoDeclaration loc _) = Just locgetErrorLoc (AlreadyDefined loc _) = Just locgetErrorLoc (NotFunctionType loc _ _) = Just locgetErrorLoc (RewriteNoChange loc _ _ _) = Just locgetErrorLoc (NotRewriteRule loc _ _) = Just locgetErrorLoc (CaseCompile loc _ _) = Just locgetErrorLoc (MatchTooSpecific loc _ _) = Just locgetErrorLoc (BadDotPattern loc _ _ _ _) = Just locgetErrorLoc (BadImplicit loc _) = Just locgetErrorLoc (BadRunElab loc _ _) = Just locgetErrorLoc (GenericMsg loc _) = Just locgetErrorLoc (TTCError _) = NothinggetErrorLoc (FileErr _ _) = NothinggetErrorLoc (ParseFail loc _) = Just locgetErrorLoc (ModuleNotFound loc _) = Just locgetErrorLoc (CyclicImports _) = NothinggetErrorLoc ForceNeeded = NothinggetErrorLoc (InternalError _) = NothinggetErrorLoc (InType _ _ err) = getErrorLoc errgetErrorLoc (InCon _ _ err) = getErrorLoc errgetErrorLoc (InLHS _ _ err) = getErrorLoc errgetErrorLoc (InRHS _ _ err) = getErrorLoc err -- Core is a wrapper around IO that is specialised for efficiency.exportrecord Core t where  constructor MkCore  runCore : IO (Either Error t) exportcoreRun : Core a ->          (Error -> IO b) -> (a -> IO b) -> IO bcoreRun (MkCore act) err ok    = either err ok !act exportcoreFail : Error -> Core acoreFail e = MkCore (pure (Left e)) exportwrapError : (Error -> Error) -> Core a -> Core awrapError fe (MkCore prog)    = MkCore (prog >>=                 (\x => case x of                             Left err => pure (Left (fe err))                             Right val => pure (Right val))) -- This would be better if we restrict it to a limited set of IO operationsexport%inlinecoreLift : IO a -> Core acoreLift op = MkCore (do op' <- op                         pure (Right op')) {- Monad, Applicative, Traversable are specialised by hand for Core.In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn'tspecialise interfaces under 'case' expressions, and this has a significantimpact on both compile time and run time. Of course it would be a good idea to fix this in Idris, but it's not an urgentthing on the road to self hosting, and we can make sure this isn't a problemin the next version (i.e., in this project...)! -} -- Functor (specialised)export %inlinemap : (a -> b) -> Core a -> Core bmap f (MkCore a) = MkCore (map (map f) a) export %inline(<$>) : (a -> b) -> Core a -> Core b(<$>) f (MkCore a) = MkCore (map (map f) a) -- Monad (specialised)export %inline(>>=) : Core a -> (a -> Core b) -> Core b(>>=) (MkCore act) f    = MkCore (act >>=                   (\x => case x of                               Left err => pure (Left err)                               Right val => runCore (f val))) -- Applicative (specialised)export %inlinepure : a -> Core apure x = MkCore (pure (pure x)) export(<*>) : Core (a -> b) -> Core a -> Core b(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |] export %inlinewhen : Bool -> Lazy (Core ()) -> Core ()when True f = fwhen False f = pure () exportCatchable Core Error where  catch (MkCore prog) h      = MkCore ( do p' <- prog                    case p' of                         Left e => let MkCore he = h e in he                         Right val => pure (Right val))  throw = coreFail -- Traversable (specialised)traverse' : (a -> Core b) -> List a -> List b -> Core (List b)traverse' f [] acc = pure (reverse acc)traverse' f (x :: xs) acc    = traverse' f xs (!(f x) :: acc) exporttraverse : (a -> Core b) -> List a -> Core (List b)traverse f xs = traverse' f xs [] exporttraverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)traverseVect f [] = pure []traverseVect f (x :: xs) = [| f x :: traverseVect f xs |] exporttraverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)traverseOpt f Nothing = pure NothingtraverseOpt f (Just x) = map Just (f x) exporttraverse_ : (a -> Core b) -> List a -> Core ()traverse_ f [] = pure ()traverse_ f (x :: xs)    = do f x         traverse_ f xs namespace PiInfo  export  traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b)  traverse f Explicit = pure Explicit  traverse f Implicit = pure Implicit  traverse f AutoImplicit = pure AutoImplicit  traverse f (DefImplicit t) = pure (DefImplicit !(f t)) namespace Binder  export  traverse : (a -> Core b) -> Binder a -> Core (Binder b)  traverse f (Lam c p ty) = pure $ Lam c !(traverse f p) !(f ty)  traverse f (Let c val ty) = pure $ Let c !(f val) !(f ty)  traverse f (Pi c p ty) = pure $ Pi c !(traverse f p) !(f ty)  traverse f (PVar c p ty) = pure $ PVar c !(traverse f p) !(f ty)  traverse f (PLet c val ty) = pure $ PLet c !(f val) !(f ty)  traverse f (PVTy c ty) = pure $ PVTy c !(f ty) exportanyM : (a -> Core Bool) -> List a -> Core BoolanyM f [] = pure FalseanyM f (x :: xs)    = if !(f x)         then pure True         else anyM f xs exportallM : (a -> Core Bool) -> List a -> Core BoolallM f [] = pure TrueallM f (x :: xs)    = if !(f x)         then allM f xs         else pure False exportfilterM : (a -> Core Bool) -> List a -> Core (List a)filterM p [] = pure []filterM p (x :: xs)    = if !(p x)         then do xs' <- filterM p xs                 pure (x :: xs')         else filterM p xs exportdata Ref : label -> Type -> Type where	   MkRef : IORef a -> Ref x a exportnewRef : (x : label) -> t -> Core (Ref x t)newRef x val    = do ref <- coreLift (newIORef val)         pure (MkRef ref) export %inline

Lines 1–500 of 518. Load more