idris 0.11.1 → 0.11.2
raw patch · 78 files changed
+1685/−462 lines, 78 filesdep +aesondep ~fsnotifysetup-changedPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: aeson
Dependency ranges changed: fsnotify
API changes (from Hackage documentation)
- Idris.Elab.Clause: propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
+ IRTS.Defunctionalise: Apply2Case :: a -> EvalApply a
+ IRTS.Defunctionalise: mkApply2 :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Bytecode.BC
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Bytecode.Reg
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.CodegenCommon.CodegenInfo
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Defunctionalise.DAlt
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Defunctionalise.DDecl
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Defunctionalise.DExp
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.Export
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.ExportIFace
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.FDesc
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.LAlt
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.LDecl
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.LExp
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.LOpt
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.LVar
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Lang.PrimFn
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Portable.CodegenFile
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Simplified.SAlt
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Simplified.SDecl
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON IRTS.Simplified.SExp
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON Idris.Core.CaseTree.CaseType
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON Idris.Core.TT.ArithTy
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON Idris.Core.TT.Const
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON Idris.Core.TT.IntTy
+ IRTS.Portable: instance Data.Aeson.Types.Class.ToJSON Idris.Core.TT.Name
+ IRTS.Portable: writePortable :: Handle -> CodegenInfo -> IO ()
+ Idris.AbsSyntax: addOpenImpl :: [Name] -> Idris [Name]
+ Idris.AbsSyntax: expandInstanceScope :: t -> t1 -> [(Name, t3)] -> t2 -> PDecl' t3 -> PDecl' t3
+ Idris.AbsSyntax: getOpenImpl :: Idris [Name]
+ Idris.AbsSyntax: setInjectivity :: Name -> Injectivity -> Idris ()
+ Idris.AbsSyntax: setOpenImpl :: [Name] -> Idris ()
+ Idris.AbsSyntaxTree: DInjective :: Name -> Directive
+ Idris.AbsSyntaxTree: DefaultCheckingCovering :: DefaultTotality
+ Idris.AbsSyntaxTree: DefaultCheckingPartial :: DefaultTotality
+ Idris.AbsSyntaxTree: DefaultCheckingTotal :: DefaultTotality
+ Idris.AbsSyntaxTree: IBCFormat :: IRFormat
+ Idris.AbsSyntaxTree: IBCInjective :: Name -> Injectivity -> IBCWrite
+ Idris.AbsSyntaxTree: JSONFormat :: IRFormat
+ Idris.AbsSyntaxTree: POpenInterfaces :: FC -> [Name] -> [PDecl' t] -> PDecl' t
+ Idris.AbsSyntaxTree: [constraintAllowed] :: SyntaxInfo -> Bool
+ Idris.AbsSyntaxTree: [idris_openimpls] :: IState -> [Name]
+ Idris.AbsSyntaxTree: data DefaultTotality
+ Idris.AbsSyntaxTree: data IRFormat
+ Idris.AbsSyntaxTree: instance GHC.Classes.Eq Idris.AbsSyntaxTree.DefaultTotality
+ Idris.AbsSyntaxTree: instance GHC.Classes.Eq Idris.AbsSyntaxTree.IRFormat
+ Idris.AbsSyntaxTree: instance GHC.Show.Show Idris.AbsSyntaxTree.DefaultTotality
+ Idris.AbsSyntaxTree: instance GHC.Show.Show Idris.AbsSyntaxTree.IRFormat
+ Idris.Core.Evaluate: lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
+ Idris.Core.Evaluate: setInjective :: Name -> Injectivity -> Context -> Context
+ Idris.Core.Evaluate: type Injectivity = Bool
+ Idris.Coverage: totalityCheckBlock :: Idris ()
+ Idris.DeepSeq: instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.DefaultTotality
+ Idris.DeepSeq: instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IRFormat
+ Idris.Elab.Utils: propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
+ Idris.IBC: instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.IRFormat
+ Idris.Parser: fnOpt :: IdrisParser FnOpt
+ Idris.Parser: openInterface :: SyntaxInfo -> IdrisParser [PDecl]
+ Idris.Parser.Expr: allowConstr :: SyntaxInfo -> SyntaxInfo
+ Idris.Parser.Expr: constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
- Idris.ASTUtils: known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))
+ Idris.ASTUtils: known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))
- Idris.AbsSyntaxTree: CI :: Name -> [(Name, (FnOpts, PTerm))] -> [(Name, (Name, PDecl))] -> [PDecl] -> [Name] -> [(Name, Bool)] -> [Int] -> ClassInfo
+ Idris.AbsSyntaxTree: CI :: Name -> [(Name, (Bool, FnOpts, PTerm))] -> [(Name, (Name, PDecl))] -> [PDecl] -> [Name] -> [(Name, Bool)] -> [Int] -> ClassInfo
- Idris.AbsSyntaxTree: DDefault :: Bool -> Directive
+ Idris.AbsSyntaxTree: DDefault :: DefaultTotality -> Directive
- Idris.AbsSyntaxTree: IState :: Context -> Set ConstraintFC -> [FixDecl] -> Ctxt [PArg] -> Ctxt [Bool] -> Ctxt ClassInfo -> Ctxt RecordInfo -> Ctxt DSL -> Ctxt OptInfo -> Ctxt TypeInfo -> Ctxt [Name] -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm]) -> Ctxt [FnOpt] -> Ctxt CGInfo -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]) -> Ctxt (Docstring DocTerm) -> Ctxt TIData -> Ctxt FnInfo -> Ctxt [(Term, Term)] -> Ctxt [Name] -> [(FC, Name)] -> [(FC, Name)] -> [(FC, String)] -> IOption -> Int -> [((FilePath, Int), PTerm)] -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name] -> [(Term, Term)] -> SyntaxRules -> [String] -> [FilePath] -> [(Name, (Int, PrimFn))] -> [(Codegen, FilePath)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(FilePath, Bool)] -> [(Name, (Bool, [String]))] -> Maybe FC -> [(FC, Err)] -> Maybe Name -> [Int] -> [Maybe Int] -> Maybe FC -> Maybe FC -> Ctxt Accessibility -> Accessibility -> Bool -> [IBCWrite] -> Maybe String -> [DynamicLib] -> [LanguageExt] -> OutputMode -> Bool -> ColourTheme -> [Name] -> (Int, Ctxt (Int, Name)) -> Ctxt (Map Name (Set Name)) -> Map [Text] [Text] -> ConsoleWidth -> Set Name -> Set (Name, Int) -> [(Name, Int)] -> Maybe (Map Name [Name]) -> Maybe (Map Name [Name]) -> [Name] -> [(Name, Bool)] -> Map Name Name -> [Name] -> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)] -> Ctxt String -> Set Name -> Map Term (Int, Term) -> Ctxt String -> IState
+ Idris.AbsSyntaxTree: IState :: Context -> Set ConstraintFC -> [FixDecl] -> Ctxt [PArg] -> Ctxt [Bool] -> Ctxt ClassInfo -> [Name] -> Ctxt RecordInfo -> Ctxt DSL -> Ctxt OptInfo -> Ctxt TypeInfo -> Ctxt [Name] -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm]) -> Ctxt [FnOpt] -> Ctxt CGInfo -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]) -> Ctxt (Docstring DocTerm) -> Ctxt TIData -> Ctxt FnInfo -> Ctxt [(Term, Term)] -> Ctxt [Name] -> [(FC, Name)] -> [(FC, Name)] -> [(FC, String)] -> IOption -> Int -> [((FilePath, Int), PTerm)] -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name] -> [(Term, Term)] -> SyntaxRules -> [String] -> [FilePath] -> [(Name, (Int, PrimFn))] -> [(Codegen, FilePath)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(FilePath, Bool)] -> [(Name, (Bool, [String]))] -> Maybe FC -> [(FC, Err)] -> Maybe Name -> [Int] -> [Maybe Int] -> Maybe FC -> Maybe FC -> Ctxt Accessibility -> Accessibility -> DefaultTotality -> [IBCWrite] -> Maybe String -> [DynamicLib] -> [LanguageExt] -> OutputMode -> Bool -> ColourTheme -> [Name] -> (Int, Ctxt (Int, Name)) -> Ctxt (Map Name (Set Name)) -> Map [Text] [Text] -> ConsoleWidth -> Set Name -> Set (Name, Int) -> [(Name, Int)] -> Maybe (Map Name [Name]) -> Maybe (Map Name [Name]) -> [Name] -> [(Name, Bool)] -> Map Name Name -> [Name] -> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)] -> Ctxt String -> Set Name -> Map Term (Int, Term) -> Ctxt String -> IState
- Idris.AbsSyntaxTree: PInstance :: (Docstring (Either Err t)) -> [(Name, Docstring (Either Err t))] -> SyntaxInfo -> FC -> [(Name, t)] -> Accessibility -> FnOpts -> Name -> FC -> [t] -> t -> (Maybe Name) -> [PDecl' t] -> PDecl' t
+ Idris.AbsSyntaxTree: PInstance :: (Docstring (Either Err t)) -> [(Name, Docstring (Either Err t))] -> SyntaxInfo -> FC -> [(Name, t)] -> [Name] -> Accessibility -> FnOpts -> Name -> FC -> [t] -> [(Name, t)] -> t -> (Maybe Name) -> [PDecl' t] -> PDecl' t
- Idris.AbsSyntaxTree: Syn :: [Using] -> [(Name, PTerm)] -> [String] -> [Name] -> [Name] -> (Name -> Name) -> Bool -> Bool -> Maybe Int -> Int -> DSL -> Int -> Bool -> Bool -> SyntaxInfo
+ Idris.AbsSyntaxTree: Syn :: [Using] -> [(Name, PTerm)] -> [String] -> [Name] -> [Name] -> (Name -> Name) -> Bool -> Bool -> Bool -> Maybe Int -> Int -> DSL -> Int -> Bool -> Bool -> SyntaxInfo
- Idris.AbsSyntaxTree: Via :: String -> Codegen
+ Idris.AbsSyntaxTree: Via :: IRFormat -> String -> Codegen
- Idris.AbsSyntaxTree: [class_methods] :: ClassInfo -> [(Name, (FnOpts, PTerm))]
+ Idris.AbsSyntaxTree: [class_methods] :: ClassInfo -> [(Name, (Bool, FnOpts, PTerm))]
- Idris.AbsSyntaxTree: [default_total] :: IState -> Bool
+ Idris.AbsSyntaxTree: [default_total] :: IState -> DefaultTotality
- Idris.Core.Evaluate: definitions :: Context -> Ctxt (Def, Accessibility, Totality, MetaInformation)
+ Idris.Core.Evaluate: definitions :: Context -> Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)
- Idris.Elab.Instance: elabInstance :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> ElabWhat -> FC -> [(Name, PTerm)] -> Accessibility -> FnOpts -> Name -> FC -> [PTerm] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()
+ Idris.Elab.Instance: elabInstance :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> ElabWhat -> FC -> [(Name, PTerm)] -> [Name] -> Accessibility -> FnOpts -> Name -> FC -> [PTerm] -> [(Name, PTerm)] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()
- Idris.Parser: fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
+ Idris.Parser: fnOpts :: IdrisParser ([FnOpt], Accessibility)
- Idris.Parser: totality :: IdrisParser Bool
+ Idris.Parser: totality :: IdrisParser DefaultTotality
Files
- CHANGELOG.md +41/−0
- CONTRIBUTING.md +2/−2
- Setup.hs +2/−1
- codegen/idris-codegen-c/Main.hs +1/−1
- codegen/idris-codegen-javascript/Main.hs +1/−1
- codegen/idris-codegen-node/Main.hs +1/−1
- idris.cabal +25/−12
- libs/base/Data/Fin.idr +11/−0
- libs/base/Data/Primitives/Views.idr +75/−0
- libs/base/base.ipkg +1/−0
- libs/contrib/Classes/Verified.idr +1/−1
- libs/contrib/Network/Socket.idr +3/−0
- libs/prelude/Builtins.idr +16/−13
- libs/prelude/Prelude/File.idr +2/−2
- libs/prelude/Prelude/Stream.idr +2/−2
- rts/idris_gc.c +2/−4
- rts/idris_main.c +1/−1
- rts/idris_rts.c +0/−14
- rts/idris_rts.h +4/−2
- src/IRTS/Compiler.hs +17/−8
- src/IRTS/Defunctionalise.hs +33/−2
- src/IRTS/Portable.hs +277/−0
- src/IRTS/System.hs +2/−1
- src/Idris/ASTUtils.hs +1/−1
- src/Idris/AbsSyntax.hs +55/−8
- src/Idris/AbsSyntaxTree.hs +47/−19
- src/Idris/CaseSplit.hs +27/−10
- src/Idris/CmdOptions.hs +8/−1
- src/Idris/Core/Evaluate.hs +45/−32
- src/Idris/Core/Unify.hs +5/−3
- src/Idris/Core/WHNF.hs +1/−0
- src/Idris/Coverage.hs +24/−4
- src/Idris/DeepSeq.hs +16/−7
- src/Idris/Directives.hs +5/−0
- src/Idris/Docs.hs +2/−2
- src/Idris/Elab/Class.hs +28/−10
- src/Idris/Elab/Clause.hs +16/−34
- src/Idris/Elab/Data.hs +2/−2
- src/Idris/Elab/Instance.hs +187/−32
- src/Idris/Elab/Term.hs +33/−7
- src/Idris/Elab/Utils.hs +24/−0
- src/Idris/ElabDecls.hs +7/−2
- src/Idris/IBC.hs +44/−9
- src/Idris/Parser.hs +118/−72
- src/Idris/Parser/Data.hs +11/−7
- src/Idris/Parser/Expr.hs +32/−15
- src/Idris/Parser/Helpers.hs +3/−2
- src/Idris/ProofSearch.hs +23/−11
- src/Idris/REPL.hs +4/−5
- src/Idris/REPL/Parser.hs +2/−2
- src/Idris/TypeSearch.hs +4/−4
- src/Util/DynamicLinker.hs +7/−9
- test/classes001/ClassName.idr +0/−49
- test/classes001/expected +0/−29
- test/classes001/input +0/−2
- test/classes001/run +0/−3
- test/directives002/directives002.idr +14/−0
- test/directives002/expected +2/−0
- test/directives002/run +4/−0
- test/interfaces001/ClassName.idr +49/−0
- test/interfaces001/expected +29/−0
- test/interfaces001/input +2/−0
- test/interfaces001/run +3/−0
- test/interfaces002/expected +1/−0
- test/interfaces002/interfaces002.idr +39/−0
- test/interfaces002/run +4/−0
- test/interfaces003/expected +2/−0
- test/interfaces003/interfaces003.idr +22/−0
- test/interfaces003/run +4/−0
- test/interfaces004/expected +4/−0
- test/interfaces004/interfaces004.idr +35/−0
- test/interfaces004/run +4/−0
- test/interfaces005/expected +7/−0
- test/interfaces005/interfaces005.idr +53/−0
- test/interfaces005/interfaces005a.idr +50/−0
- test/interfaces005/interfaces005b.idr +50/−0
- test/interfaces005/run +5/−0
- test/reg072/expected +1/−1
CHANGELOG.md view
@@ -6,6 +6,46 @@ dependent types * `rewrite` can now be given an optional rewriting lemma, with the syntax `rewrite [rule] using [rewrite_lemma] in [scope]`.++* Reorganised elaboration of `implementation`, so that interfaces with+ dependencies between methods now work more smoothly++* Allow naming of parent implementations when defining an implementation.+ For example:++ ```+ [PlusNatSemi] Semigroup Nat where+ (<+>) x y = x + y+ + [MultNatSemi] Semigroup Nat where+ (<+>) x y = x * y+ + -- use PlusNatSemi as the parent implementation+ [PlusNatMonoid] Monoid Nat using PlusNatSemi where+ neutral = 0+ + -- use MultNatSemi as the parent implementation+ [MultNatMonoid] Monoid Nat using MultNatSemi where+ neutral = 1+ ```++* Interface definitions can now include data declarations (but not data+ definitions). Any implementation of the interface must define the method+ using a data type. The effect is to cause Idris to treat the method as+ a data type (for unification and interface resolution purposes).++* Experimentally, allow named implementations to be available by default in a+ block of declarations with `using` notation. For example:++ ```+ using implementation PlusNatMonoid+ test : Nat -> Nat+ test x = x <+> x <+> neutral+ ```++* Constraint arguments can now appear anywhere in function types, not just+ at the top level or after an implicit argument binding.+ * Experimental extended `with` syntax, which allows calling functions defined in a with block directly. For example: @@ -39,6 +79,7 @@ `Prelude.WellFounded`. * Added `Data.List.Views` with views on `List` and their covering functions. * Added `Data.Nat.Views` with views on `Nat` and their covering functions.+* Added `Data.Primitives.Views` with views on various primitive types and their covering functions. ## Miscellaneous updates
CONTRIBUTING.md view
@@ -157,9 +157,9 @@ * [Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki); * [Zen Of Idris](https://github.com/idris-lang/Idris-dev/wiki/The-Zen-of-Idris);-* Idris FAQs: [Official](http://www.idris-lang.org/documentation/faq/); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);+* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ); * [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);-* [Idris Tutorial](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf);+* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html); * [Idris News](http://www.idris-lang.org/news/); * [other Idris docs](http://www.idris-lang.org/documentation/). * [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
Setup.hs view
@@ -38,7 +38,8 @@ -- Make Commands -- use GNU make on FreeBSD-#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)+#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)\+ || defined(openbsd_HOST_OS) || defined(netbsd_HOST_OS) mymake = "gmake" #else mymake = "make"
codegen/idris-codegen-c/Main.hs view
@@ -40,7 +40,7 @@ mainProg <- if interface opts then liftM Just elabMain else return Nothing- ir <- compile (Via "c") (output opts) mainProg+ ir <- compile (Via IBCFormat "c") (output opts) mainProg runIO $ codegenC ir main :: IO ()
codegen/idris-codegen-javascript/Main.hs view
@@ -34,7 +34,7 @@ jsMain opts = do elabPrims loadInputs (inputs opts) Nothing mainProg <- elabMain- ir <- compile (Via "javascript") (output opts) (Just mainProg)+ ir <- compile (Via IBCFormat "javascript") (output opts) (Just mainProg) runIO $ codegenJavaScript ir main :: IO ()
codegen/idris-codegen-node/Main.hs view
@@ -33,7 +33,7 @@ jsMain opts = do elabPrims loadInputs (inputs opts) Nothing mainProg <- elabMain- ir <- compile (Via "node") (output opts) (Just mainProg)+ ir <- compile (Via IBCFormat "node") (output opts) (Just mainProg) runIO $ codegenNode ir main :: IO ()
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.11.1+Version: 0.11.2 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -115,6 +115,7 @@ libs/base/Control/Monad/*.idr libs/base/Data/*.idr libs/base/Data/Nat/*.idr+ libs/base/Data/Primitives/*.idr libs/base/Data/List/*.idr libs/base/Data/Vect/*.idr libs/base/Data/String/*.idr@@ -399,11 +400,6 @@ test/bignum002/*.idr test/bignum002/expected - test/classes001/*.idr- test/classes001/run- test/classes001/expected- test/classes001/input- test/corecords001/*.idr test/corecords001/run test/corecords001/expected@@ -414,6 +410,9 @@ test/directives001/*.idr test/directives001/run test/directives001/expected+ test/directives002/*.idr+ test/directives002/run+ test/directives002/expected test/delab001/*.idr test/delab001/run@@ -609,6 +608,23 @@ test/interactive013/run test/interactive013/*.idr + test/interfaces001/*.idr+ test/interfaces001/run+ test/interfaces001/expected+ test/interfaces001/input+ test/interfaces002/*.idr+ test/interfaces002/run+ test/interfaces002/expected+ test/interfaces003/*.idr+ test/interfaces003/run+ test/interfaces003/expected+ test/interfaces004/*.idr+ test/interfaces004/run+ test/interfaces004/expected+ test/interfaces005/*.idr+ test/interfaces005/run+ test/interfaces005/expected+ test/io001/run test/io001/*.idr test/io001/expected@@ -1016,6 +1032,7 @@ , IRTS.Inliner , IRTS.Lang , IRTS.LangOpts+ , IRTS.Portable , IRTS.Simplified , IRTS.System @@ -1036,6 +1053,7 @@ , Tools_idris Build-depends: base >=4 && <5+ , aeson >= 0.6 && < 0.12 , annotated-wl-pprint >= 0.7 && < 0.8 , ansi-terminal < 0.7 , ansi-wl-pprint < 0.7@@ -1072,7 +1090,7 @@ , vector-binary-instances < 0.3 , zip-archive > 0.2.3.5 && < 0.4 , safe- , fsnotify < 2.2+ , fsnotify >= 0.2 && < 2.2 , async < 2.2 -- zlib >= 0.6.1 is broken with GHC < 7.10.3@@ -1090,19 +1108,14 @@ ghc-prof-options: -auto-all -caf-all if os(linux)- cpp-options: -DLINUX build-depends: unix < 2.8 if os(freebsd)- cpp-options: -DFREEBSD build-depends: unix < 2.8 -- if os(dragonfly)--- cpp-options: -DDRAGONFLY -- build-depends: unix < 2.8 if os(darwin)- cpp-options: -DMACOSX build-depends: unix < 2.8 if os(windows)- cpp-options: -DWINDOWS build-depends: Win32 < 2.4 if flag(FFI) build-depends: libffi < 0.2
libs/base/Data/Fin.idr view
@@ -127,6 +127,17 @@ fromInteger {n} x {prf} with (integerToFin x n) fromInteger {n} x {prf = ItIsJust} | Just y = y +||| Convert an Integer to a Fin in the required bounds/+||| This is essentially a composition of `mod` and `fromInteger`+export+restrict : (n : Nat) -> Integer -> Fin (S n)+restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in+ -- reasoning about primitives, so we need the+ -- 'believe_me'. It's fine because val' must be+ -- in the right range+ fromInteger val'+ {prf = believe_me {a=IsJust (Just val')} ItIsJust}+ %language ErrorReflection ||| Attempt to convert a reflected (fromInteger n) to a Nat
+ libs/base/Data/Primitives/Views.idr view
@@ -0,0 +1,75 @@+module Data.Primitives.Views++-- We need all the believe_mes and asserts throughout this file because we're+-- working with primitive here! We also have separate implementations per+-- primitive, rather than using interfaces, because we're only going to trust+-- the primitive implementations.++namespace Integer+ ||| View for expressing a number as a multiplication + a remainder+ public export+ data Divides : Integer -> (d : Integer) -> Type where+ DivByZero : Divides x 0+ DivBy : (prf : rem >= 0 && rem < d = True) ->+ Divides ((d * div) + rem) d+ + ||| Covering function for the `Divides` view+ export+ divides : (val : Integer) -> (d : Integer) -> Divides val d+ divides val 0 = DivByZero+ divides val d+ = let dividend = if d < 0 then -(val `div` abs d)+ else val `div` d+ remainder = val `mod` d in+ believe_me (DivBy {d} {div = dividend} {rem = remainder}+ (believe_me (Refl {x = True})))++ ||| View for recursion over Integers+ data IntegerRec : Integer -> Type where+ IntegerZ : IntegerRec 0+ IntegerSucc : IntegerRec (n - 1) -> IntegerRec n+ IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)+ + ||| Covering function for `IntegerRec`+ integerRec : (x : Integer) -> IntegerRec x+ integerRec 0 = IntegerZ+ integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))+ else believe_me (IntegerPred {n=-x} + (assert_total (believe_me (integerRec (x + 1)))))++namespace Int+ ||| View for expressing a number as a multiplication + a remainder+ public export+ data Divides : Int -> (d : Int) -> Type where+ DivByZero : Int.Divides x 0+ DivBy : (prf : rem >= 0 && rem < d = True) ->+ Int.Divides ((d * div) + rem) d+ + -- I have assumed, but not actually verified, that this will still+ -- give a right result (i.e. still adding up) when the Ints overflow.+ -- TODO: Someone please check this and fix if necessary...++ ||| Covering function for the `Divides` view+ export+ divides : (val : Int) -> (d : Int) -> Divides val d+ divides val 0 = DivByZero+ divides val d+ = let dividend = if d < 0 then -(val `div` abs d)+ else val `div` d+ remainder = val `mod` d in+ believe_me (DivBy {d} {div = dividend} {rem = remainder}+ (believe_me (Refl {x = True})))++ ||| View for recursion over Ints+ data IntRec : Int -> Type where+ IntZ : IntRec 0+ IntSucc : IntRec (n - 1) -> IntRec n+ IntPred : IntRec ((-n) + 1) -> IntRec (-n)+ + ||| Covering function for `IntRec`+ intRec : (x : Int) -> IntRec x+ intRec 0 = IntZ+ intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))+ else believe_me (IntPred {n=-x}+ (assert_total (believe_me (intRec (x + 1)))))+
libs/base/base.ipkg view
@@ -19,6 +19,7 @@ Data.Erased, Data.List, Data.List.Views, Data.List.Quantifiers, Data.Nat.Views,+ Data.Primitives.Views, Data.String.Views, Data.So, Data.String,
libs/contrib/Classes/Verified.idr view
@@ -28,7 +28,7 @@ applicativeHomomorphism : (x : a) -> (g : a -> b) -> (<*>) {f} (pure g) (pure x) = pure {f} (g x) applicativeInterchange : (x : a) -> (g : f (a -> b)) ->- g <*> pure x = pure (\g' : a -> b => g' x) <*> g+ g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
libs/contrib/Network/Socket.idr view
@@ -273,6 +273,7 @@ freeRecvfromStruct : RecvfromStructPtr -> IO () freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p +export recv : Socket -> Int -> IO (Either SocketError (String, ByteLength)) recv sock len = do -- Firstly make the request, get some kind of recv structure which@@ -309,6 +310,7 @@ else return $ Right recv_res +export sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength) sendTo sock addr p dat = do sendto_res <- foreign FFI_C "idrnet_sendto"@@ -344,6 +346,7 @@ port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr return port +export recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength)) recvFrom sock bl = do recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)
libs/prelude/Builtins.idr view
@@ -106,38 +106,41 @@ trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c trans Refl Refl = Refl -||| There are two types of laziness: that arising from lazy functions, and that-||| arising from codata. They differ in their totality condition.-data LazyType = LazyCodata | LazyEval+||| Two types of delayed computation: that arising from lazy functions, and that+||| arising from infinite data. They differ in their totality condition.+data DelayReason = Infinite | LazyValue ||| The underlying implementation of Lazy and Inf. %error_reverse-data Lazy' : LazyType -> Type -> Type where+data Delayed : DelayReason -> Type -> Type where ||| A delayed computation. ||| ||| Delay is inserted automatically by the elaborator where necessary. ||| ||| Note that compiled code gives `Delay` special semantics.- ||| @ t whether this is laziness from codata or normal lazy evaluation+ ||| @ t whether this is laziness from an infinite structure or lazy evaluation ||| @ a the type of the eventual value ||| @ val a computation that will produce a value- Delay : {t, a : _} -> (val : a) -> Lazy' t a+ Delay : {t, a : _} -> (val : a) -> Delayed t a ||| Compute a value from a delayed computation. ||| ||| Inserted by the elaborator where necessary.-Force : {t, a : _} -> Lazy' t a -> a+Force : {t, a : _} -> Delayed t a -> a Force (Delay x) = x -||| Lazily evaluated values. This has special evaluation semantics.+||| Lazily evaluated values. +||| At run time, the delayed value will only be computed when required by+||| a case split. Lazy : Type -> Type-Lazy t = Lazy' LazyEval t+Lazy t = Delayed LazyValue t -||| Recursive parameters to codata. Inserted automatically by the elaborator-||| on a "codata" definition but is necessary by hand if mixing inductive and-||| coinductive parameters.+||| Possibly infinite data. +||| A value which may be infinite is accepted by the totality checker if+||| it appears under a data constructor. At run time, the delayed value will+||| only be computed when required by a case split. Inf : Type -> Type-Inf t = Lazy' LazyCodata t+Inf t = Delayed Infinite t namespace Ownership ||| A read-only version of a unique value
libs/prelude/Prelude/File.idr view
@@ -233,7 +233,7 @@ return (p > 0) ||| Read the contents of a file into a string-partial -- might be reading something infinitely long like /dev/null ...+-- might be reading something infinitely long like /dev/null ... covering export readFile : String -> IO (Either FileError String) readFile fn = do Right h <- openFile fn Read@@ -242,7 +242,7 @@ closeFile h return c where- partial+ covering readFile' : File -> String -> IO (Either FileError String) readFile' h contents = do x <- fEOF h
libs/prelude/Prelude/Stream.idr view
@@ -13,8 +13,8 @@ %default total ||| An infinite stream-codata Stream : Type -> Type where- (::) : (e : a) -> Stream a -> Stream a+data Stream : Type -> Type where+ (::) : (e : a) -> Inf (Stream a) -> Stream a -- Hints for interactive editing %name Stream xs,ys,zs,ws
rts/idris_gc.c view
@@ -4,7 +4,7 @@ #include <assert.h> VAL copy(VM* vm, VAL x) {- int i, ar;+ int ar; Closure* cl = NULL; if (x==NULL || ISINT(x)) { return x;@@ -16,9 +16,7 @@ return x; } else { allocCon(cl, vm, CTAG(x), ar, 1);- for(i = 0; i < ar; ++i) {- cl->info.c.args[i] = x->info.c.args[i];- }+ memcpy(&(cl->info.c.args), &(x->info.c.args), sizeof(VAL)*ar); } break; case CT_FLOAT:
rts/idris_main.c view
@@ -4,7 +4,7 @@ #include "idris_gmp.h" // The default options should give satisfactory results under many circumstances. RTSOpts opts = { - .init_heap_size = 4096000,+ .init_heap_size = 16384000, .max_stack_size = 4096000, .show_summary = 0 };
rts/idris_rts.c view
@@ -391,20 +391,6 @@ return cl; } -void PROJECT(VM* vm, VAL r, int loc, int arity) {- int i;- for(i = 0; i < arity; ++i) {- LOC(i+loc) = r->info.c.args[i];- }-}--void SLIDE(VM* vm, int args) {- int i;- for(i = 0; i < args; ++i) {- LOC(i) = TOP(i);- }-}- void dumpStack(VM* vm) { int i = 0; VAL* root;
rts/idris_rts.h view
@@ -259,8 +259,10 @@ #define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a)) #define GETARG(x, i) ((x)->info.c.args)[i] -void PROJECT(VM* vm, VAL r, int loc, int arity);-void SLIDE(VM* vm, int args);+#define PROJECT(vm,r,loc,num) \+ memcpy(&(LOC(loc)), &((r)->info.c.args), sizeof(VAL)*num)+#define SLIDE(vm, args) \+ memcpy(&(LOC(0)), &(TOP(0)), sizeof(VAL)*args) void* allocate(size_t size, int outerlock); // void* allocCon(VM* vm, int arity, int outerlock);
src/IRTS/Compiler.hs view
@@ -12,6 +12,7 @@ import IRTS.CodegenJavaScript import IRTS.Inliner import IRTS.Exports+import IRTS.Portable import Idris.AbsSyntax import Idris.AbsSyntaxTree@@ -125,13 +126,21 @@ generate codegen mainmod ir = case codegen of -- Built-in code generators (FIXME: lift these out!)- Via "c" -> codegenC ir+ Via _ "c" -> codegenC ir -- Any external code generator- Via cg -> do let cmd = "idris-codegen-" ++ cg- args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir- exit <- rawSystem cmd args- when (exit /= ExitSuccess) $- putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)+ Via fm cg -> do input <- case fm of+ IBCFormat -> return mainmod+ JSONFormat -> do+ tempdir <- getTemporaryDirectory+ (fn, h) <- openTempFile tempdir "idris-cg.json"+ writePortable h ir+ hClose h+ return fn+ let cmd = "idris-codegen-" ++ cg+ args = [input, "-o", outputFile ir] ++ compilerFlags ir+ exit <- rawSystem cmd args+ when (exit /= ExitSuccess) $+ putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args) Bytecode -> dumpBC (simpleDecls ir) (outputFile ir) irMain :: TT Name -> Idris LDecl@@ -350,7 +359,7 @@ -- overapplied GT -> ifail ("overapplied data constructor: " ++ show tm ++- "\nDEBUG INFO:\n" ++ + "\nDEBUG INFO:\n" ++ "Arity: " ++ show arity ++ "\n" ++ "Arguments: " ++ show args ++ "\n" ++ "Pruned arguments: " ++ show argsPruned)@@ -439,7 +448,7 @@ | otherwise = n used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)- fst4 (x,_,_,_) = x+ fst4 (x,_,_,_,_) = x irTerm vs env (P _ n _) = return $ LV (Glob n) irTerm vs env (V i)
src/IRTS/Defunctionalise.hs view
@@ -51,8 +51,9 @@ newacons = sortBy conord $ concatMap (toConsA anames') (getFn all) eval = mkEval newecons app = mkApply newacons+ app2 = mkApply2 newacons condecls = declare nexttag (newecons ++ newacons) in- addAlist (eval : app : condecls ++ allD) emptyContext+ addAlist (eval : app : app2 : condecls ++ allD) emptyContext where conord (n, _, _) (n', _, _) = compare n n' getFn :: [(Name, LDecl)] -> [(Name, Int)]@@ -152,6 +153,8 @@ = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args) chainAPPLY f [] = f+-- chainAPPLY f (a : b : as) +-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as -- if anything in the DExp is projected from, we'll need to evaluate it,@@ -184,6 +187,7 @@ data EvalApply a = EvalCase (Name -> a) | ApplyCase a+ | Apply2Case a -- For a function name, generate a list of -- data constuctors, and whether to handle them in EVAL or APPLY@@ -219,7 +223,15 @@ (DApp False (mkUnderCon fname (ar - (n + 1))) (map (DV . Glob) (take n (genArgs 0) ++ [sMN 0 "arg"])))))- : mkApplyCase fname (n + 1) ar+ : + if (ar - (n + 2) >=0 )+ then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))+ (DApp False (mkUnderCon fname (ar - (n + 2)))+ (map (DV . Glob) (take n (genArgs 0) +++ [sMN 0 "arg0", sMN 0 "arg1"])))))+ :+ mkApplyCase fname (n + 1) ar+ else mkApplyCase fname (n + 1) ar mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl) mkEval xs = (sMN 0 "EVAL", DFun (sMN 0 "EVAL") [sMN 0 "arg"]@@ -241,6 +253,25 @@ [DDefaultCase DNothing]))) where applyCase (n, t, ApplyCase x) = Just x+ applyCase _ = Nothing++mkApply2 :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)+mkApply2 xs = (sMN 0 "APPLY2", DFun (sMN 0 "APPLY2") [sMN 0 "fn", sMN 0 "arg0", sMN 0 "arg1"]+ (case mapMaybe applyCase xs of+ [] -> DNothing+ cases ->+ mkBigCase (sMN 0 "APPLY") 256+ (DV (Glob (sMN 0 "fn")))+ (cases +++ [DDefaultCase + (DApp False (sMN 0 "APPLY")+ [DApp False (sMN 0 "APPLY")+ [DV (Glob (sMN 0 "fn")),+ DV (Glob (sMN 0 "arg0"))],+ DV (Glob (sMN 0 "arg1"))])+ ])))+ where+ applyCase (n, t, Apply2Case x) = Just x applyCase _ = Nothing
+ src/IRTS/Portable.hs view
@@ -0,0 +1,277 @@+{-# LANGUAGE OverloadedStrings #-}++module IRTS.Portable (writePortable) where++import Data.Aeson+import qualified Data.ByteString.Lazy as B+import qualified Data.Text as T++import Idris.Core.CaseTree+import Idris.Core.TT++import IRTS.Bytecode+import IRTS.CodegenCommon+import IRTS.Defunctionalise+import IRTS.Lang+import IRTS.Simplified++import System.IO++data CodegenFile = CGFile {+ fileType :: String,+ version :: Int,+ cgInfo :: CodegenInfo+}++-- Update the version when the format changes+formatVersion :: Int+formatVersion = 1++writePortable :: Handle -> CodegenInfo -> IO ()+writePortable file ci = do+ let json = encode $ CGFile "idris-codegen" formatVersion ci+ B.hPut file json++instance ToJSON CodegenFile where+ toJSON (CGFile ft v ci) = object ["file-type" .= ft,+ "version" .= v,+ "codegen-info" .= toJSON ci]++instance ToJSON CodegenInfo where+ toJSON ci = object ["output-file" .= (outputFile ci),+ "includes" .= (includes ci),+ "import-dirs" .= (importDirs ci),+ "compile-objs" .= (compileObjs ci),+ "compile-libs" .= (compileLibs ci),+ "compiler-flags" .= (compilerFlags ci),+ "interfaces" .= (interfaces ci),+ "exports" .= (exportDecls ci),+ "lift-decls" .= (liftDecls ci),+ "defun-decls" .= (defunDecls ci),+ "simple-decls" .= (simpleDecls ci),+ "bytecode" .= (map toBC (simpleDecls ci))]++instance ToJSON Name where+ toJSON n = toJSON $ showCG n++instance ToJSON ExportIFace where+ toJSON (Export n f xs) = object ["ffi-desc" .= n,+ "interface-file" .= f,+ "exports" .= xs]++instance ToJSON FDesc where+ toJSON (FCon n) = object ["FCon" .= n]+ toJSON (FStr s) = object ["FStr" .= s]+ toJSON (FUnknown) = object ["FUnknown" .= Null]+ toJSON (FIO fd) = object ["FIO" .= fd]+ toJSON (FApp n xs) = object ["FApp" .= (n, xs)]++instance ToJSON Export where+ toJSON (ExportData fd) = object ["ExportData" .= fd]+ toJSON (ExportFun n dsc ret args) = object ["ExportFun" .= (n, dsc, ret, args)]++instance ToJSON LDecl where+ toJSON (LFun opts name args def) = object ["LFun" .= (opts, name, args, def)]+ toJSON (LConstructor name tag ar) = object ["LConstructor" .= (name, tag, ar)]++instance ToJSON LOpt where+ toJSON Inline = String "Inline"+ toJSON NoInline = String "NoInline"++instance ToJSON LExp where+ toJSON (LV lv) = object ["LV" .= lv]+ toJSON (LApp tail exp args) = object ["LApp" .= (tail, exp, args)]+ toJSON (LLazyApp name exps) = object ["LLazyApp" .= (name, exps)]+ toJSON (LLazyExp exp) = object ["LLazyExp" .= exp]+ toJSON (LForce exp) = object ["LForce" .= exp]+ toJSON (LLet name a b) = object ["LLet" .= (name, a, b)]+ toJSON (LLam args exp) = object ["LLam" .= (args, exp)]+ toJSON (LProj exp i) = object ["LProj" .= (exp, i)]+ toJSON (LCon lv i n exps) = object ["LCon" .= (lv, i, n, exps)]+ toJSON (LCase ct exp alts) = object ["LCase" .= (ct, exp, alts)]+ toJSON (LConst c) = object ["LConst" .= c]+ toJSON (LForeign fd ret exps) = object ["LForeign" .= (fd, ret, exps)]+ toJSON (LOp prim exps) = object ["LOp" .= (prim, exps)]+ toJSON LNothing = object ["LNothing" .= Null]+ toJSON (LError s) = object ["LError" .= s]++instance ToJSON LVar where+ toJSON (Loc i) = object ["Loc" .= i]+ toJSON (Glob n) = object ["Glob" .= n]++instance ToJSON CaseType where+ toJSON Updatable = String "Updatable"+ toJSON Shared = String "Shared"++instance ToJSON LAlt where+ toJSON (LConCase i n ns exp) = object ["LConCase" .= (i, n, ns, exp)]+ toJSON (LConstCase c exp) = object ["LConstCase" .= (c, exp)]+ toJSON (LDefaultCase exp) = object ["LDefaultCase" .= exp]++instance ToJSON Const where+ toJSON (I i) = object ["int" .= i]+ toJSON (BI i) = object ["bigint" .= (show i)]+ toJSON (Fl d) = object ["double" .= d]+ toJSON (Ch c) = object ["char" .= (show c)]+ toJSON (Str s) = object ["string" .= s]+ toJSON (B8 b) = object ["bits8" .= b]+ toJSON (B16 b) = object ["bits16" .= b]+ toJSON (B32 b) = object ["bits32" .= b]+ toJSON (B64 b) = object ["bits64" .= b]+ toJSON (AType at) = object ["atype" .= at]+ toJSON StrType = object ["strtype" .= Null]+ toJSON WorldType = object ["worldtype" .= Null]+ toJSON TheWorld = object ["theworld" .= Null]+ toJSON VoidType = object ["voidtype" .= Null]+ toJSON Forgot = object ["forgot" .= Null]++instance ToJSON ArithTy where+ toJSON (ATInt it) = object ["ATInt" .= it]+ toJSON ATFloat = object ["ATFloat" .= Null]++instance ToJSON IntTy where+ toJSON it = toJSON $ intTyName it++instance ToJSON PrimFn where+ toJSON (LPlus aty) = object ["LPlus" .= aty]+ toJSON (LMinus aty) = object ["LMinus" .= aty]+ toJSON (LTimes aty) = object ["LTimes" .= aty]+ toJSON (LUDiv aty) = object ["LUDiv" .= aty]+ toJSON (LSDiv aty) = object ["LSDiv" .= aty]+ toJSON (LAnd ity) = object ["LAnd" .= ity]+ toJSON (LOr ity) = object ["LOr" .= ity]+ toJSON (LXOr ity) = object ["LXOr" .= ity]+ toJSON (LCompl ity) = object ["LCompl" .= ity]+ toJSON (LSHL ity) = object ["LSHL" .= ity]+ toJSON (LLSHR ity) = object ["LLSHR" .= ity]+ toJSON (LASHR ity) = object ["LASHR" .= ity]+ toJSON (LEq aty) = object ["LEq" .= aty]+ toJSON (LLt ity) = object ["LLt" .= ity]+ toJSON (LLe ity) = object ["LLe" .= ity]+ toJSON (LGt ity) = object ["LGt" .= ity]+ toJSON (LGe ity) = object ["LGe" .= ity]+ toJSON (LSLt aty) = object ["LSLt" .= aty]+ toJSON (LSLe aty) = object ["LSLe" .= aty]+ toJSON (LSGt aty) = object ["LSGt" .= aty]+ toJSON (LSGe aty) = object ["LSGe" .= aty]+ toJSON (LZExt from to) = object ["LZExt" .= (from, to)]+ toJSON (LSExt from to) = object ["LSExt" .= (from, to)]+ toJSON (LTrunc from to) = object ["LTrunc" .= (from, to)]+ toJSON LStrConcat = object ["LStrConcat" .= Null]+ toJSON LStrLt = object ["LStrLt" .= Null]+ toJSON LStrEq = object ["LStrEq" .= Null]+ toJSON LStrLen = object ["LStrLen" .= Null]+ toJSON (LIntFloat ity) = object ["LIntFloat" .= ity]+ toJSON (LFloatInt ity) = object ["LFloatInt" .= ity]+ toJSON (LIntStr ity) = object ["LIntStr" .= ity]+ toJSON (LStrInt ity) = object ["LStrInt" .= ity]+ toJSON (LIntCh ity) = object ["LIntCh" .= ity]+ toJSON (LChInt ity) = object ["LChInt" .= ity]+ toJSON LFloatStr = object ["LFloatStr" .= Null]+ toJSON LStrFloat = object ["LStrFloat" .= Null]+ toJSON (LBitCast from to) = object ["LBitCast" .= (from, to)]+ toJSON LFExp = object ["LFExp" .= Null]+ toJSON LFLog = object ["LFLog" .= Null]+ toJSON LFSin = object ["LFSin" .= Null]+ toJSON LFCos = object ["LFCos" .= Null]+ toJSON LFTan = object ["LFTan" .= Null]+ toJSON LFASin = object ["LFASin" .= Null]+ toJSON LFACos = object ["LFACos" .= Null]+ toJSON LFATan = object ["LFATan" .= Null]+ toJSON LFSqrt = object ["LFSqrt" .= Null]+ toJSON LFFloor = object ["LFFloor" .= Null]+ toJSON LFCeil = object ["LFCeil" .= Null]+ toJSON LFNegate = object ["LFNegate" .= Null]+ toJSON LStrHead = object ["LStrHead" .= Null]+ toJSON LStrTail = object ["LStrTail" .= Null]+ toJSON LStrCons = object ["LStrCons" .= Null]+ toJSON LStrIndex = object ["LStrIndex" .= Null]+ toJSON LStrRev = object ["LStrRev" .= Null]+ toJSON LStrSubstr = object ["LStrSubstr" .= Null]+ toJSON LReadStr = object ["LReadStr" .= Null]+ toJSON LWriteStr = object ["LWriteStr" .= Null]+ toJSON LSystemInfo = object ["LSystemInfo" .= Null]+ toJSON LFork = object ["LFork" .= Null]+ toJSON LPar = object ["LPar" .= Null]+ toJSON (LExternal name) = object ["LExternal" .= name]+ toJSON LNoOp = object ["LNoOp" .= Null]++++++instance ToJSON DDecl where+ toJSON (DFun name args exp) = object ["DFun" .= (name, args, exp)]+ toJSON (DConstructor name tag arity) = object ["DConstructor" .= (name, tag, arity)]++instance ToJSON DExp where+ toJSON (DV lv) = object ["DV" .= lv]+ toJSON (DApp tail name exps) = object ["DApp" .= (tail, name, exps)]+ toJSON (DLet name a b) = object ["DLet" .= (name, a, b)]+ toJSON (DUpdate name exp) = object ["DUpdate" .= (name,exp)]+ toJSON (DProj exp i) = object ["DProj" .= (exp, i)]+ toJSON (DC lv i name exp) = object ["DC" .= (lv, i, name, exp)]+ toJSON (DCase ct exp alts) = object ["DCase" .= (ct, exp, alts)]+ toJSON (DChkCase exp alts) = object ["DChkCase" .= (exp, alts)]+ toJSON (DConst c) = object ["DConst" .= c]+ toJSON (DForeign fd ret exps) = object ["DForeign" .= (fd, ret, exps)]+ toJSON (DOp prim exps) = object ["DOp" .= (prim, exps)]+ toJSON DNothing = object ["DNothing" .= Null]+ toJSON (DError s) = object ["DError" .= s]++instance ToJSON DAlt where+ toJSON (DConCase i n ns exp) = object ["DConCase" .= (i, n, ns, exp)]+ toJSON (DConstCase c exp) = object ["DConstCase" .= (c, exp)]+ toJSON (DDefaultCase exp) = object ["DDefaultCase" .= exp]++instance ToJSON SDecl where+ toJSON (SFun name args i exp) = object ["SFun" .= (name, args, i, exp)]++instance ToJSON SExp where+ toJSON (SV lv) = object ["SV" .= lv]+ toJSON (SApp tail name exps) = object ["SApp" .= (tail, name, exps)]+ toJSON (SLet lv a b) = object ["SLet" .= (lv, a, b)]+ toJSON (SUpdate lv exp) = object ["SUpdate" .= (lv, exp)]+ toJSON (SProj lv i) = object ["DProj" .= (lv, i)]+ toJSON (SCon lv i name vars) = object ["SCon" .= (lv, i, name, vars)]+ toJSON (SCase ct lv alts) = object ["SCase" .= (ct, lv, alts)]+ toJSON (SChkCase lv alts) = object ["DChkCase" .= (lv, alts)]+ toJSON (SConst c) = object ["SConst" .= c]+ toJSON (SForeign fd ret exps) = object ["SForeign" .= (fd, ret, exps)]+ toJSON (SOp prim vars) = object ["DOp" .= (prim, vars)]+ toJSON SNothing = object ["SNothing" .= Null]+ toJSON (SError s) = object ["SError" .= s]++instance ToJSON SAlt where+ toJSON (SConCase i j n ns exp) = object ["SConCase" .= (i, j, n, ns, exp)]+ toJSON (SConstCase c exp) = object ["SConstCase" .= (c, exp)]+ toJSON (SDefaultCase exp) = object ["SDefaultCase" .= exp]++instance ToJSON BC where+ toJSON (ASSIGN r1 r2) = object ["ASSIGN" .= (r1, r2)]+ toJSON (ASSIGNCONST r c) = object ["ASSIGNCONST" .= (r, c)]+ toJSON (UPDATE r1 r2) = object ["UPDATE" .= (r1, r2)]+ toJSON (MKCON con mr i regs) = object ["MKCON" .= (con, mr, i, regs)]+ toJSON (CASE b r alts def) = object ["CASE" .= (b, r, alts, def)]+ toJSON (PROJECT r loc arity) = object ["PROJECT" .= (r, loc, arity)]+ toJSON (PROJECTINTO r1 r2 loc) = object ["PROJECTINTO" .= (r1, r2, loc)]+ toJSON (CONSTCASE r alts def) = object ["CONSTCASE" .= (r, alts, def)]+ toJSON (CALL name) = object ["CALL" .= name]+ toJSON (TAILCALL name) = object ["TAILCALL" .= name]+ toJSON (FOREIGNCALL r fd ret exps) = object ["FOREIGNCALL" .= (r, fd, ret, exps)]+ toJSON (SLIDE i) = object ["SLIDE" .= i]+ toJSON (RESERVE i) = object ["RESERVE" .= i]+ toJSON (ADDTOP i) = object ["ADDTOP" .= i]+ toJSON (TOPBASE i) = object ["TOPBASE" .= i]+ toJSON (BASETOP i) = object ["BASETOP" .= i]+ toJSON REBASE = object ["REBASE" .= Null]+ toJSON STOREOLD = object ["STOREOLD" .= Null]+ toJSON (OP r prim args) = object ["OP" .= (r, prim, args)]+ toJSON (NULL r) = object ["NULL" .= r]+ toJSON (ERROR s) = object ["ERROR" .= s]++instance ToJSON Reg where+ toJSON RVal = object ["RVal" .= Null]+ toJSON (T i) = object ["T" .= i]+ toJSON (L i) = object ["L" .= i]+ toJSON Tmp = object ["Tmp" .= Null]
src/IRTS/System.hs view
@@ -29,7 +29,8 @@ getTargetDir :: IO String getTargetDir = overrideDataDirWith "TARGET" -#if defined(FREEBSD) || defined(DRAGONFLY)+#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)\+ || defined(openbsd_HOST_OS) || defined(netbsd_HOST_OS) extraLib = ["-L/usr/local/lib"] extraInclude = ["-I/usr/local/include"] #else
src/Idris/ASTUtils.hs view
@@ -138,7 +138,7 @@ ------------- -- This has a terrible name, but I'm not sure of a better one that isn't -- confusingly close to tt_ctxt-known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))+known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)) known_terms = Field (definitions . tt_ctxt) (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
src/Idris/AbsSyntax.hs view
@@ -45,7 +45,11 @@ getContext = do i <- getIState; return (tt_ctxt i) forCodegen :: Codegen -> [(Codegen, a)] -> [a]-forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']+forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']+ where+ eqLang (Via _ x) (Via _ y) = x == y+ eqLang Bytecode Bytecode = True+ eqLang _ _ = False getObjectFiles :: Codegen -> Idris [FilePath] getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)@@ -218,6 +222,12 @@ let ctxt = setTotal n a (tt_ctxt i) putIState $ i { tt_ctxt = ctxt } +setInjectivity :: Name -> Injectivity -> Idris ()+setInjectivity n a+ = do i <- getIState+ let ctxt = setInjective n a (tt_ctxt i)+ putIState $ i { tt_ctxt = ctxt }+ getTotality :: Name -> Idris Totality getTotality n = do i <- getIState@@ -446,6 +456,33 @@ chaser (NS n _) = chaser n chaser _ = False +-- Add a privileged implementation - one which instance search will happily+-- resolve immediately if it is type correct+-- This is used for naming parent implementations when defining an+-- implementation with constraints.+-- Returns the old list, so we can revert easily at the end of a block++addOpenImpl :: [Name] -> Idris [Name]+addOpenImpl ns = do ist <- getIState+ ns' <- mapM (checkValid ist) ns+ let open = idris_openimpls ist+ putIState $ ist { idris_openimpls = nub (ns' ++ open) }+ return open+ where+ checkValid ist n+ = case lookupCtxtName n (idris_implicits ist) of+ [(n', _)] -> return n'+ [] -> throwError (NoSuchVariable n)+ more -> throwError (CantResolveAlts (map fst more))++setOpenImpl :: [Name] -> Idris ()+setOpenImpl ns = do ist <- getIState+ putIState $ ist { idris_openimpls = ns }++getOpenImpl :: Idris [Name]+getOpenImpl = do ist <- getIState+ return (idris_openimpls ist)+ addClass :: Name -> ClassInfo -> Idris () addClass n i = do ist <- getIState@@ -913,6 +950,7 @@ codegen = do i <- getIState return (opt_codegen (idris_options i)) + setOutputTy :: OutputType -> Idris () setOutputTy t = do i <- getIState let opts = idris_options i@@ -1249,7 +1287,7 @@ updateps yn nm [] = [] updateps yn nm (((a, t), i):as) | (a `elem` nm) == yn = (a, t) : updateps yn nm as- | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as+ | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as removeBound lhs ns = ns \\ nub (bnames lhs) @@ -1290,19 +1328,28 @@ (map (expandParamsD rhs ist dec ps ns) decls) cn cd-expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params ty cn decls)- = PInstance doc argDocs info f+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)+ = let cn' = case cn of+ Just n -> if n `elem` ns then Just (dec n) else Just n+ Nothing -> Nothing in+ PInstance doc argDocs info f (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)- acc opts n+ pnames acc opts n nfc (map (expandParams dec ps ns []) params)+ (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra) (expandParams dec ps ns [] ty)- cn- (map (expandParamsD rhs ist dec ps ns) decls)+ cn'+ (map (expandParamsD True ist dec ps ns) decls) expandParamsD rhs ist dec ps ns d = d mapsnd f (x, t) = (x, f t) +expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)+ = PInstance doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)+ ty cn decls+expandInstanceScope ist dec ps ns d = d+ -- Calculate a priority for a type, for deciding elaboration order -- * if it's just a type variable or concrete type, do it early (0) -- * if there's only type variables and injective constructors, do it next (1)@@ -2287,7 +2334,7 @@ sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y) sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y) sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)- sm 0 (PAlternative ms a as) + sm 0 (PAlternative ms a as) = PAlternative (map shadowAlt ms) a (map (sm 0) as) sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts) sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
src/Idris/AbsSyntaxTree.hs view
@@ -112,7 +112,7 @@ , opt_verbose = True , opt_nobanner = False , opt_quiet = False- , opt_codegen = Via "c"+ , opt_codegen = Via IBCFormat "c" , opt_outputTy = Executable , opt_ibcsubdir = "" , opt_importdirs = []@@ -181,6 +181,11 @@ | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise deriving (Show, Eq) +-- | If a function has no totality annotation, what do we assume?+data DefaultTotality = DefaultCheckingTotal -- ^ Total+ | DefaultCheckingPartial -- ^ Partial+ | DefaultCheckingCovering -- ^Total coverage, but may diverge+ deriving (Show, Eq) -- | The global state used in the Idris monad data IState = IState {@@ -191,6 +196,7 @@ idris_implicits :: Ctxt [PArg], idris_statics :: Ctxt [Bool], idris_classes :: Ctxt ClassInfo,+ idris_openimpls :: [Name], -- ^ Privileged implementations, will resolve immediately idris_records :: Ctxt RecordInfo, idris_dsls :: Ctxt DSL, idris_optimisation :: Ctxt OptInfo,@@ -244,7 +250,7 @@ idris_parsedSpan :: Maybe FC, hide_list :: Ctxt Accessibility, default_access :: Accessibility,- default_total :: Bool,+ default_total :: DefaultTotality, ibc_write :: [IBCWrite], compiled_so :: Maybe String, idris_dynamic_libs :: [DynamicLib],@@ -327,6 +333,7 @@ | IBCAccess Name Accessibility | IBCMetaInformation Name MetaInformation | IBCTotal Name Totality+ | IBCInjective Name Injectivity | IBCFlags Name [FnOpt] | IBCFnInfo Name FnInfo | IBCTrans Name (Term, Term)@@ -354,13 +361,13 @@ -- | The initial state for the compiler idrisInit :: IState idrisInit = IState initContext S.empty []- emptyContext emptyContext emptyContext emptyContext+ emptyContext emptyContext emptyContext [] emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []- [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []+ [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] [] (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] [] emptyContext S.empty M.empty emptyContext@@ -379,18 +386,15 @@ -- Commands in the REPL -data Codegen = Via String--- | ViaC--- | ViaJava--- | ViaNode--- | ViaJavaScript--- | ViaLLVM+data Codegen = Via IRFormat String | Bytecode deriving (Show, Eq) {-! deriving instance NFData Codegen !-} +data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)+ data HowMuchDocs = FullDocs | OverviewDocs -- | REPL commands@@ -703,6 +707,7 @@ | PCAF FC Name t -- ^ Top level constant | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration. | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block+ | POpenInterfaces FC [Name] [PDecl' t] -- ^ Open block/declaration | PNamespace String FC [PDecl' t] -- ^ New namespace, where FC is accurate location of the -- namespace in the file@@ -733,11 +738,13 @@ [(Name, Docstring (Either Err t))] -- Parameter docs SyntaxInfo FC [(Name, t)] -- constraints+ [Name] -- parent dictionaries to search for constraints Accessibility FnOpts Name -- class FC -- precise location of class [t] -- parameters+ [(Name, t)] -- Extra names in scope in the body t -- full instance type (Maybe Name) -- explicit name [PDecl' t]@@ -766,8 +773,9 @@ | DInclude Codegen String | DHide Name | DFreeze Name+ | DInjective Name | DAccess Accessibility- | DDefault Bool+ | DDefault DefaultTotality | DLogging Integer | DDynamicLibs [String] | DNameHint Name FC [(Name, FC)]@@ -880,6 +888,8 @@ PParams (f fc) (map (\(n, ty) -> (n, mapPTermFC f g ty)) params) (map (mapPDeclFC f g) decls)+mapPDeclFC f g (POpenInterfaces fc ifs decls) =+ POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls) mapPDeclFC f g (PNamespace ns fc decls) = PNamespace ns (f fc) (map (mapPDeclFC f g) decls) mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =@@ -900,10 +910,11 @@ (map (mapPDeclFC f g) body) (fmap (\(n, nfc) -> (n, g nfc)) ctor) ctorDoc-mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params instTy instN body) =+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra instTy instN body) = PInstance doc paramDocs syn (f fc) (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)- cn acc opts (g cnfc) (map (mapPTermFC f g) params)+ pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)+ (map (\(en, et) -> (en, mapPTermFC f g et)) pextra) (mapPTermFC f g instTy) instN (map (mapPDeclFC f g) body)@@ -940,10 +951,14 @@ where fstt (_, _, a, _, _, _, _) = a declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n] declared (PParams _ _ ds) = concatMap declared ds+declared (POpenInterfaces _ _ ds) = concatMap declared ds declared (PNamespace _ _ ds) = concatMap declared ds declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn) declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)-declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)+ = case mn of+ Nothing -> []+ Just n -> [n] declared (PDSL n _) = [n] declared (PSyntax _ _) = [] declared (PMutual _ ds) = concatMap declared ds@@ -960,10 +975,14 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts where fstt (_, _, a, _, _, _, _) = a tldeclared (PParams _ _ ds) = []+tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds tldeclared (PMutual _ ds) = concatMap tldeclared ds tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)-tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)+ = case mn of+ Nothing -> []+ Just n -> [n] tldeclared _ = [] defined :: PDecl -> [Name]@@ -976,10 +995,14 @@ where fstt (_, _, a, _, _, _, _) = a defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = [] defined (PParams _ _ ds) = concatMap defined ds+defined (POpenInterfaces _ _ ds) = concatMap defined ds defined (PNamespace _ _ ds) = concatMap defined ds defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn) defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)-defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)+ = case mn of+ Nothing -> []+ Just n -> [n] defined (PDSL n _) = [n] defined (PSyntax _ _) = [] defined (PMutual _ ds) = concatMap defined ds@@ -1353,7 +1376,7 @@ -- Type class data data ClassInfo = CI { instanceCtorName :: Name,- class_methods :: [(Name, (FnOpts, PTerm))],+ class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl class_default_superclasses :: [PDecl], class_params :: [Name],@@ -1523,6 +1546,7 @@ decoration :: Name -> Name, inPattern :: Bool, implicitAllowed :: Bool,+ constraintAllowed :: Bool, maxline :: Maybe Int, mut_nesting :: Int, dsl_info :: DSL,@@ -1535,7 +1559,7 @@ deriving instance Binary SyntaxInfo !-} -defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True True+defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True expandNS :: SyntaxInfo -> Name -> Name expandNS syn n@(NS _ _) = n@@ -1792,6 +1816,9 @@ depth d . bracket p startPrec $ lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc+ prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])+ | basename neg == sUN "negate" =+ lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen -- This case preserves the behavior of the former constructor PEq. -- It should be removed if feasible when the pretty-printing of infix -- operators in general is improved.@@ -2163,11 +2190,12 @@ indent 2 (vsep (map (showCImp o) cs)) showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)+showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line) showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line) showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn) showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _) = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds-showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ t _ ds)+showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds) = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds showDeclImp _ _ = text "..." -- showDeclImp (PImport o) = "import " ++ o
src/Idris/CaseSplit.hs view
@@ -12,6 +12,7 @@ import Idris.ElabDecls import Idris.Delaborate import Idris.Parser+import Idris.Parser.Helpers import Idris.Error import Idris.Output @@ -284,10 +285,12 @@ replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String] replaceSplits l ups impossible- = updateRHSs 1 (map (rep (expandBraces l)) ups)+ = do ist <- getIState+ updateRHSs 1 (map (rep ist (expandBraces l)) ups) where- rep str [] = str ++ "\n"- rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups+ rep ist str [] = str ++ "\n"+ rep ist str ((n, tm) : ups) + = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups updateRHSs i [] = return [] updateRHSs i (x : xs)@@ -368,6 +371,20 @@ (before, ('_' : after)) -> nameRoot (acc ++ [before]) after _ -> showSep "_" (acc ++ [nm]) +-- Show a name for use in pattern definitions on the lhs+showLHSName :: Name -> String+showLHSName n = let fn = show n in + if any (flip elem opChars) fn+ then "(" ++ fn ++ ")"+ else fn++-- Show a name for the purpose of generating a metavariable name on the rhs+showRHSName :: Name -> String+showRHSName n = let fn = show n in + if any (flip elem opChars) fn+ then "op"+ else fn+ getClause :: Int -- ^ line number that the type is declared on -> Name -- ^ Function name -> Name -- ^ User given name@@ -383,8 +400,8 @@ x -> x ist <- get let ap = mkApp ist ty []- return (show un ++ " " ++ ap ++ "= ?"- ++ show un ++ "_rhs")+ return (showLHSName un ++ " " ++ ap ++ "= ?"+ ++ showRHSName un ++ "_rhs") where mkApp :: IState -> PTerm -> [Name] -> String mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used = let n = getNameFrom i used ty in@@ -410,14 +427,14 @@ sUN "z"]) used -- write method declarations, indent with 4 spaces- mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String+ mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String mkClassBodies i ns = showSep "\n"- (zipWith (\(n, (_, ty)) m -> " " +++ (zipWith (\(n, (_, _, ty)) m -> " " ++ def (show (nsroot n)) ++ " " ++ mkApp i ty [] ++ "= ?"- ++ show un ++ "_rhs_" ++ show m) ns [1..])+ ++ showRHSName un ++ "_rhs_" ++ show m) ns [1..]) def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")" def n = n@@ -431,7 +448,7 @@ let ty = case ty_in of PTyped n t -> t x -> x- return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")+ return (mkApp ty ++ " = ?" ++ showRHSName fn ++ "_rhs") where mkApp (PPi _ _ _ _ sc) = mkApp sc mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn @@ -451,7 +468,7 @@ newpat ('>':patstr) = '>':newpat patstr newpat patstr = " " ++- replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"+ replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs" -- Replace _ with names in missing clauses
src/Idris/CmdOptions.hs view
@@ -149,6 +149,12 @@ <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))+++ <|> ((\s -> UseCodegen $ Via JSONFormat s) <$> strOption (long "portable-codegen"+ <> metavar "TARGET"+ <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))+ <|> (CodegenArgs <$> strOption (long "cg-opt" <> metavar "ARG" <> help "Arguments to pass to code generator"))@@ -206,7 +212,8 @@ parseCodegen :: String -> Codegen parseCodegen "bytecode" = Bytecode-parseCodegen cg = Via (map toLower cg)+parseCodegen cg = Via IBCFormat (map toLower cg)+ parseLogCats :: Monad m => String -> m [LogCat] parseLogCats s =
src/Idris/Core/Evaluate.hs view
@@ -6,14 +6,15 @@ normaliseAll, normaliseBlocking, toValue, quoteTerm, rt_simplify, simplify, specialise, hnf, convEq, convEq', Def(..), CaseInfo(..), CaseDefs(..),- Accessibility(..), Totality(..), PReason(..), MetaInformation(..),+ Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..), Context, initContext, ctxtAlist, next_tvar,- addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,+ addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl, addDatatype, addCasedef, simplifyCasedef, addOperator, lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal, mapDefCtxt, - lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,+ lookupTotal, lookupTotalExact, lookupInjectiveExact,+ lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName, Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions, isUniverse) where @@ -759,6 +760,8 @@ show Private = "private" show Hidden = "hidden" +type Injectivity = Bool+ -- | The result of totality checking data Totality = Total [Int] -- ^ well-founded arguments | Productive -- ^ productive@@ -816,7 +819,7 @@ -- universe constraints and existing definitions. data Context = MkContext { next_tvar :: Int,- definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)+ definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation) } deriving Show @@ -826,47 +829,53 @@ mapDefCtxt :: (Def -> Def) -> Context -> Context mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)- where f' (!d, a, t, m) = f' (f d, a, t, m)+ where f' (!d, i, a, t, m) = f' (f d, i, a, t, m) -- | Get the definitions from a context ctxtAlist :: Context -> [(Name, Def)]-ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)+ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt) veval ctxt env t = evalState (eval False ctxt [] env t []) initEval addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt = let ctxt = definitions uctxt- !ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in+ !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in uctxt { definitions = ctxt' } setAccess :: Name -> Accessibility -> Context -> Context setAccess n a uctxt = let ctxt = definitions uctxt- !ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in+ !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in uctxt { definitions = ctxt' } +setInjective :: Name -> Injectivity -> Context -> Context+setInjective n i uctxt+ = let ctxt = definitions uctxt+ !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in+ uctxt { definitions = ctxt' }+ setTotal :: Name -> Totality -> Context -> Context setTotal n t uctxt = let ctxt = definitions uctxt- !ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in+ !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in uctxt { definitions = ctxt' } setMetaInformation :: Name -> MetaInformation -> Context -> Context setMetaInformation n m uctxt = let ctxt = definitions uctxt- !ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in+ !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in uctxt { definitions = ctxt' } addCtxtDef :: Name -> Def -> Context -> Context addCtxtDef n d c = let ctxt = definitions c- !ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in+ !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in c { definitions = ctxt' } addTyDecl :: Name -> NameType -> Type -> Context -> Context addTyDecl n nt ty uctxt = let ctxt = definitions uctxt- !ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in+ !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in uctxt { definitions = ctxt' } addDatatype :: Datatype Name -> Context -> Context@@ -874,14 +883,14 @@ = let ctxt = definitions uctxt ty' = normalise uctxt [] ty !ctxt' = addCons 0 cons (addDef n- (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in+ (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in uctxt { definitions = ctxt' } where addCons tag [] ctxt = ctxt addCons tag ((n, ty) : cons) ctxt = let ty' = normalise uctxt [] ty in addCons (tag+1) cons (addDef n- (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)+ (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt) -- FIXME: Too many arguments! Refactor all these Bools. --@@ -923,7 +932,7 @@ (args_rt, sc_rt) op = (CaseOp (ci { case_inlinable = inlc }) ty argtys ps_in ps_tot cdef,- access, Unchecked, EmptyMI)+ False, access, Unchecked, EmptyMI) in return $ addDef n op ctxt -- other -> tfail (Msg $ "Error adding case def: " ++ show other) return uctxt { definitions = ctxt' }@@ -933,15 +942,15 @@ simplifyCasedef n ei uctxt = do let ctxt = definitions uctxt ctxt' <- case lookupCtxt n ctxt of- [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->+ [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] -> return ctxt -- nothing to simplify (or already done...)- [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->+ [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] -> do let ps_in' = map simpl ps_in pdef = map debind ps_in' CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei return $ addDef n (CaseOp ci ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),- acc, tot, metainf) ctxt+ inj, acc, tot, metainf) ctxt _ -> return ctxt return uctxt { definitions = ctxt' }@@ -961,10 +970,10 @@ Context -> Context addOperator n ty a op uctxt = let ctxt = definitions uctxt- ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in+ ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in uctxt { definitions = ctxt' } -tfst (a, _, _, _) = a+tfst (a, _, _, _, _) = a lookupNames :: Name -> Context -> [Name] lookupNames n ctxt@@ -1041,10 +1050,10 @@ lookupP_all all exact n ctxt = do (n', def) <- names p <- case def of- (Function ty tm, a, _, _) -> return (P Ref n' ty, a)- (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)- (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n' ty, a)- (Operator ty _ _, a, _, _) -> return (P Ref n' ty, a)+ (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)+ (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)+ (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)+ (Operator ty _ _, inj, a, _, _) -> return (P Ref n' ty, a) case snd p of Hidden -> if all then return (fst p) else [] Private -> if all then return (fst p) else []@@ -1071,25 +1080,29 @@ lookupDefAcc n mkpublic ctxt = map mkp $ lookupCtxt n (definitions ctxt) -- io_bind a special case for REPL prettiness- where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))- then (d, Public) else (d, a)+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))+ then (d, Public) else (d, a) lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility) lookupDefAccExact n mkpublic ctxt = fmap mkp $ lookupCtxtExact n (definitions ctxt) -- io_bind a special case for REPL prettiness- where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))- then (d, Public) else (d, a)+ where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))+ then (d, Public) else (d, a) lookupTotal :: Name -> Context -> [Totality] lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)- where mkt (d, a, t, m) = t+ where mkt (d, inj, a, t, m) = t lookupTotalExact :: Name -> Context -> Maybe Totality lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)- where mkt (d, a, t, m) = t+ where mkt (d, inj, a, t, m) = t +lookupInjectiveExact :: Name -> Context -> Maybe Injectivity+lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)+ where mkt (d, inj, a, t, m) = inj+ -- Check if a name is reducible in the type checker. Partial definitions -- are not reducible (so treated as a constant) tcReducible :: Name -> Context -> Bool@@ -1100,10 +1113,10 @@ lookupMetaInformation :: Name -> Context -> [MetaInformation] lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)- where mkm (d, a, t, m) = m+ where mkm (d, inj, a, t, m) = m lookupNameTotal :: Name -> Context -> [(Name, Totality)]-lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions+lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions lookupVal :: Name -> Context -> [Value]
src/Idris/Core/Unify.hs view
@@ -292,6 +292,8 @@ injective (P (DCon _ _ _) _ _) = True injective (P (TCon _ _) _ _) = True+ injective (P Ref n _) + | Just i <- lookupInjectiveExact n ctxt = i injective (App _ f a) = injective f -- && injective a injective _ = False @@ -573,7 +575,7 @@ rigid (P (DCon _ _ _) _ _) = True rigid (P (TCon _ _) _ _) = True- rigid t@(P Ref _ _) = inenv t || globmetavar t+ rigid t@(P Ref _ _) = inenv t || globmetavar t rigid (Constant _) = True rigid (App _ f a) = rigid f && rigid a rigid t = not (metavar t) || globmetavar t@@ -710,9 +712,9 @@ -- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722 -- recoverable t@(App _ _ _) _- | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False+ | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False recoverable _ t@(App _ _ _)- | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False+ | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y recoverable (TType _) (P (DCon _ _ _) y _) = False
src/Idris/Core/WHNF.hs view
@@ -75,6 +75,7 @@ = let wp = case nt of DCon t a u -> WDCon t a u n (ty, env) TCon t a -> WTCon t a n (ty, env)+ Ref -> WPRef n (ty, env) _ -> WPRef n (ty, env) in case lookupDefExact n ctxt of
src/Idris/Coverage.hs view
@@ -493,9 +493,9 @@ | (P _ (UN l) _, [_, _, arg]) <- unApply t, l == txt "Force" = delazy' all arg | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,- l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg+ l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,- l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg+ l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg delazy' all (App s f a) = App s (delazy' all f) (delazy' all a) delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc) delazy' all t = t@@ -518,6 +518,10 @@ -- that it is total. | (P _ (UN at) _, [_, _]) <- unApply ap, at == txt "assert_total" = []+ -- don't go under calls to functions which are asserted total+ | (P _ n _, _) <- unApply ap,+ Just opts <- lookupCtxtExact n (idris_flags ist),+ AssertTotal `elem` opts = [] -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't -- check under guarded constructors. | (P _ (UN del) _, [_,_,arg]) <- unApply ap,@@ -745,8 +749,11 @@ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist) = Total [] tryPath desc path (e@(f, args) : es) arg+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a | e `elem` es && allNothing args = Partial (Mutual [f]) tryPath desc path (e@(f, nextargs) : es) arg+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a+ | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f]) | Just d <- lookup (e, arg) path = if desc - d > 0 -- Now lower than when we were last here then -- trace ("Descent " ++ show (desc - d) ++ " "@@ -781,8 +788,6 @@ -- trace (show (desc, argspos, path, es, pathres)) $ collapse pathres - | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a- | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f]) | otherwise = Unchecked allNothing :: [Maybe a] -> Bool@@ -808,3 +813,18 @@ collapse' def (d : xs) = collapse' d xs -- collapse' Unchecked [] = Total [] collapse' def [] = def++totalityCheckBlock :: Idris ()+totalityCheckBlock = do+ ist <- getIState+ -- Do totality checking after entire mutual block+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n+ ctxt' <- do ctxt <- getContext+ tclift $ simplifyCasedef n (getErasureInfo ist) ctxt+ setContext ctxt')+ (map snd (idris_totcheck ist))+ mapM_ buildSCG (idris_totcheck ist)+ mapM_ checkDeclTotality (idris_totcheck ist)+ clear_totcheck++
src/Idris/DeepSeq.hs view
@@ -284,6 +284,7 @@ rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` () rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` () rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()+ rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` () rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` () rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` () rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()@@ -360,9 +361,12 @@ rnf (FnInfo x1) = rnf x1 `seq` () instance NFData Codegen where- rnf (Via x1) = rnf x1 `seq` ()+ rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf Bytecode = () +instance NFData IRFormat where+ rnf _ = ()+ instance NFData LogCat where rnf _ = () @@ -444,6 +448,7 @@ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` () rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()+ rnf (POpenInterfaces x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` () rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` () rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) = rnf x1 `seq`@@ -468,7 +473,7 @@ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()- rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq`@@ -477,7 +482,7 @@ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq`- rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` () rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` () rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()@@ -682,25 +687,29 @@ rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` () instance NFData SyntaxInfo where- rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq`- rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` ()+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` () instance NFData OutputMode where rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong rnf (IdeMode x y) = rnf x `seq` () +instance NFData DefaultTotality where+ rnf DefaultCheckingTotal = ()+ rnf DefaultCheckingPartial = ()+ rnf DefaultCheckingCovering = () instance NFData IState where rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60- x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76)+ x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq` rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq` rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`- rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` ()+ rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` rnf x77 `seq` ()
src/Idris/Directives.hs view
@@ -42,6 +42,11 @@ mapM_ (\n -> do setAccessibility n Frozen addIBC (IBCAccess n Frozen)) ns+directiveAction (DInjective n') = do+ ns <- allNamespaces n'+ mapM_ (\n -> do+ setInjectivity n True+ addIBC (IBCInjective n True)) ns directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })
src/Idris/Docs.hs view
@@ -319,8 +319,8 @@ namedInst n@(UN _) = Just n namedInst _ = Nothing - getDInst (PInstance _ _ _ _ _ _ _ _ _ _ t _ _) = Just t- getDInst _ = Nothing+ getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t+ getDInst _ = Nothing isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
src/Idris/Elab/Class.hs view
@@ -119,6 +119,11 @@ -- Elaborate the the top level methods mapM_ (rec_elabDecl info EAll info) (concat fns) + -- Flag all the top level data declarations as injective+ mapM_ (\n -> do setInjectivity n True+ addIBC (IBCInjective n True))+ (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))+ -- add the default definitions mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs)) addIBC (IBCClass tn)@@ -130,7 +135,7 @@ maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn where- nodoc (n, (_, _, o, t)) = (n, (o, t))+ nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t)) pibind [] x = x pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))@@ -144,7 +149,7 @@ -- TODO: probably should normalise checkDefaultSuperclassInstance :: PDecl -> Idris ()- checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ n _ ps _ _ _)+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _) = do when (not $ null cs) . tclift $ tfail (At fc (Msg $ "Default superclass instances can't have constraints.")) i <- getIState@@ -171,14 +176,26 @@ conbind [] x = x getMName (PTy _ _ _ _ _ n nfc _) = nsroot n+ getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n+ tdecl allmeths (PTy doc _ syn _ o n nfc t) = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t' return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),- (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)+ (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps) (\ l s p -> Imp l s p Nothing True) t'))), (n, (nfc, syn, o, t) ) )- tdecl _ _ = ifail "Not allowed in a class declaration"+ tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t)) + = do let o = []+ t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t+ logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'+ return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),+ (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)+ (\ l s p -> Imp l s p Nothing True) t'))),+ (n, (nfc, syn, o, t) ) )+ tdecl allmeths (PData doc _ syn _ _ _) + = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")+ tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration") -- Create default definitions defdecl mtys c d@(PClauses fc opts n cs) =@@ -190,17 +207,18 @@ PClauses fc (o ++ opts) n cs] logElab 1 (show ds) return (n, ((defaultdec n, ds!!1), ds))- _ -> ifail $ show n ++ " is not a method"+ _ -> ierror $ At fc (Msg (show n ++ " is not a method")) defdecl _ _ _ = ifail "Can't happen (defdecl)" defaultdec (UN n) = sUN ("default#" ++ str n) defaultdec (NS n ns) = NS (defaultdec n) ns - tydecl (PTy _ _ _ _ _ _ _ _) = True+ tydecl (PTy{}) = True+ tydecl (PData _ _ _ _ _ _) = True tydecl _ = False- instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = True+ instdecl (PInstance{}) = True instdecl _ = False- clause (PClauses _ _ _ _) = True+ clause (PClauses{}) = True clause _ = False -- Generate a function for chasing a dictionary constraint@@ -233,10 +251,10 @@ tfun :: Name -- ^ The name of the class -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings -> SyntaxInfo -> [Name] -- ^ All the method names- -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))+ -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm)) -- ^ The present declaration -> Idris [PDecl]- tfun cn c syn all (m, (mfc, doc, o, ty))+ tfun cn c syn all (m, (isdata, mfc, doc, o, ty)) = do let ty' = expandMethNS syn (insertConstraint c all ty) let mnames = take (length all) $ map (\x -> sMN x "meth") [0..] let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
src/Idris/Elab/Clause.hs view
@@ -194,17 +194,11 @@ logElab 5 $ "After data structure transformations:\n" ++ show pdef' ist <- getIState- -- let wf = wellFounded ist n sc- let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later+ let tot | pcover = Unchecked -- finish later+ | AssertTotal `elem` opts = Total [] | PEGenerated `elem` opts = Generated | otherwise = Partial NotCovering -- already know it's not total - -- case lookupCtxt (namespace info) n (idris_flags ist) of- -- [fs] -> if TotalFn `elem` fs- -- then case tot of- -- Total _ -> return ()- -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))- -- _ -> return () case tree of CaseDef _ _ [] -> return () CaseDef _ _ xs -> mapM_ (\x ->@@ -506,29 +500,6 @@ else return (validCoverageCase ctxt err || recoverableCoverage ctxt err) --propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm-propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)- = PApp fc (PRef fc hls n) (addP t args)- where addP (Bind n _ sc) (t : ts)- | Placeholder <- getTm t,- n `elem` ps,- not (n `elem` bound)- = t { getTm = PPatvar NoFC n } : addP sc ts- addP (Bind n _ sc) (t : ts) = t : addP sc ts- addP _ ts = ts-propagateParams i ps t bound (PApp fc ap args)- = PApp fc (propagateParams i ps t bound ap) args-propagateParams i ps t bound (PRef fc hls n)- = case lookupCtxt n (idris_implicits i) of- [is] -> let ps' = filter (isImplicit is) ps in- PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')- _ -> PRef fc hls n- where isImplicit [] n = False- isImplicit (PImp _ _ _ x _ : is) n | x == n = True- isImplicit (_ : is) n = isImplicit is n-propagateParams i ps t bound x = x- findUnique :: Context -> Env -> Term -> [Name] findUnique ctxt env (Bind n b sc) = let rawTy = forgetEnv (map fst env) (binderTy b)@@ -583,6 +554,7 @@ let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $ propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)+ -- let lhs = mkLHSapp $ -- propagateParams i params fn_ty (addImplPat i lhs_in) logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))@@ -657,6 +629,7 @@ let winfo = (pinfo info newargs defs windex) { elabFC = Just fc } let wb = map (mkStatic static_names) $+ map (expandInstanceScope ist decorate newargs defs) $ map (expandParamsD False ist decorate newargs defs) whereblock -- Split the where block into declarations with a type, and those@@ -664,7 +637,7 @@ -- Elaborate those with a type *before* RHS, those without *after* let (wbefore, wafter) = sepBlocks wb - logElab 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter+ logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter mapM_ (rec_elabDecl info EAll winfo) wbefore -- Now build the RHS, using the type of the LHS as the goal. i <- getIState -- new implicits from where block@@ -1068,9 +1041,18 @@ lhs_arity = arity toplhs - updateApp wtm@(PWithApp fcw tm warg) = + currentFn fname (PAlternative _ _ as)+ | Just tm <- getApp as = tm+ where getApp (tm@(PApp _ (PRef _ _ f) _) : as)+ | f == fname = Just tm+ getApp (_ : as) = getApp as+ getApp [] = Nothing+ currentFn _ tm = tm++ updateApp wtm@(PWithApp fcw tm_in warg) = + let tm = currentFn fname tm_in in case matchClause ist toplhs tm of- Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level"))+ Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level ")) Right mvars -> let ns = map (keepMvar (map fst mvars) fcw) ns_in ns' = map (keepMvar (map fst mvars) fcw) ns_in'
src/Idris/Elab/Data.hs view
@@ -216,8 +216,8 @@ mkLazy (PPi pl n nfc ty sc) = let ty' = if getTyName ty- then PApp fc (PRef fc [] (sUN "Lazy'"))- [pexp (PRef fc [] (sUN "LazyCodata")),+ then PApp fc (PRef fc [] (sUN "Delayed"))+ [pexp (PRef fc [] (sUN "Infinite")), pexp ty] else ty in PPi pl n nfc ty' (mkLazy sc)
src/Idris/Elab/Instance.hs view
@@ -55,15 +55,17 @@ [(Name, Docstring (Either Err PTerm))] -> ElabWhat -> -- phase FC -> [(Name, PTerm)] -> -- constraints+ [Name] -> -- parent dictionary names (optionally) Accessibility -> FnOpts -> Name -> -- the class FC -> -- precise location of class name [PTerm] -> -- class parameters (i.e. instance)+ [(Name, PTerm)] -> -- Extra arguments in scope (e.g. instance in where block) PTerm -> -- full instance type Maybe Name -> -- explicit name [PDecl] -> Idris ()-elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do+elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do ist <- getIState (n, ci) <- case lookupCtxtName n (idris_classes ist) of [c] -> return c@@ -79,7 +81,8 @@ let emptyclass = null (class_methods ci) when (what /= EDefns) $ do- nty <- elabType' True info syn doc argDocs fc totopts iname NoFC t+ nty <- elabType' True info syn doc argDocs fc totopts iname NoFC + (piBindp expl_param pextra t) -- if the instance type matches any of the instances we have already, -- and it's not a named instance, then it's overlapping, so report an error case expn of@@ -88,6 +91,9 @@ addInstance intInst True n iname Just _ -> addInstance intInst False n iname when (what /= ETypes && (not (null ds && not emptyclass))) $ do+ -- Add the parent implementation names to the privileged set+ oldOpen <- addOpenImpl parents+ let ips = zip (class_params ci) ps let ns = case n of NS n ns' -> ns'@@ -101,17 +107,31 @@ ist <- getIState let pnames = nub $ map pname (concat (nub wparams)) ++ concatMap (namesIn [] ist) ps+ let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci) undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances+ + ist <- getIState+ -- Bring variables in instance head into scope when building the+ -- dictionary+ let headVars = nub $ concatMap getHeadVars ps+ let (headVarTypes, ty)+ = case lookupTyExact iname (tt_ctxt ist) of+ Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)+ _ -> (zip headVars (repeat Placeholder), Erased)+ logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty+ let all_meths = map (nsroot . fst) (class_methods ci)- let mtys = map (\ (n, (op, t)) ->+ let mtys = map (\ (n, (inj, op, t)) -> let t_in = substMatchesShadow ips pnames t- mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))+ mnamemap = + map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))+ (map (toImp fc) headVars))) all_meths t' = substMatchesShadow mnamemap pnames t_in in (decorate ns iname n,- op, coninsert cs t', t'))+ op, coninsert cs pextra t', t')) (class_methods ci) logElab 3 (show (mtys, ips)) logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))@@ -119,38 +139,63 @@ logElab 3 ("After defaults: " ++ show ds_defs ++ "\n") let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs logElab 1 ("Reordered: " ++ show ds' ++ "\n")+ mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci)) mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds') let wbTys = map mkTyDecl mtys- let wbVals = map (decorateid (decorate ns iname)) ds'+ let wbVals_orig = map (decorateid (decorate ns iname)) ds'+ ist <- getIState+ let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig let wb = wbTys ++ wbVals+ logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys) logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++ show (concat (nub wparams)) - -- Bring variables in instance head into scope- let headVars = nub $ mapMaybe (\p -> case p of- PRef _ _ n ->- case lookupTy n (tt_ctxt ist) of- [] -> Just n- _ -> Nothing- _ -> Nothing) ps--- let lhs = PRef fc iname- let lhs = PApp fc (PRef fc [] iname)- (map (\n -> pimp n (PRef fc [] n) True) headVars)++ let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars++ let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra) let rhs = PApp fc (PRef fc [] (instanceCtorName ci))- (map (pexp . mkMethApp) mtys)+ (map (pexp . (mkMethApp lhsImps)) mtys) - logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ show lhs ++ " " ++ show headVars+ logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars logElab 5 $ "Instance RHS " ++ show rhs - let idecls = [PClauses fc totopts iname- [PClause fc iname lhs [] rhs wb]]- logElab 1 (show idecls) push_estack iname True+ logElab 3 ("Method types: " ++ show wbTys)+ logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)+ logElab 3 ("Method bodies: " ++ show wbVals)++ let idecls = [PClauses fc totopts iname+ [PClause fc iname lhs [] rhs []]]++ mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys) mapM_ (rec_elabDecl info EAll info) idecls++ ctxt <- getContext+ let ifn_ty = case lookupTyExact iname ctxt of+ Just t -> t+ Nothing -> error "Can't happen (interface constructor)"+ let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of+ Just t -> t+ Nothing -> []+ let prop_params = getParamsInType ist [] ifn_is ifn_ty++ logElab 3 $ "Propagating parameters to methods: " + ++ show (iname, prop_params)++ let wbVals' = map (addParams prop_params) wbVals++ mapM_ (rec_elabDecl info EAll info) wbVals'+ + mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')+ pop_estack- ist <- getIState++ setOpenImpl oldOpen+-- totalityCheckBlock+ checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist)) addIBC (IBCInstance intInst (isNothing expn) n iname) @@ -166,10 +211,13 @@ Just m -> sNS (SN (sInstanceN n' (map show ps'))) m Just nm -> nm - substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps t expn ds)- = PInstance doc argDocs syn fc cs acc opts n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds+ substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)+ = PInstance doc argDocs syn fc cs parents acc opts n nfc + (map (substMatchesShadow ips pnames) ps) + pextra+ (substMatchesShadow ips pnames t) expn ds - isOverlapping i (PInstance doc argDocs syn _ _ _ _ n nfc ps t expn _)+ isOverlapping i (PInstance doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _) = case lookupCtxtName n (idris_classes i) of [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in case lookupTy iname (tt_ctxt i) of@@ -226,8 +274,15 @@ map snd (filter (\(i, _) -> i `elem` dets) a') keepDets dets t = t - mkMethApp (n, _, _, ty)- = lamBind 0 ty (papp fc (PRef fc [] n) (methArgs 0 ty))+ methName (n, _, _, _) = n+ toExp n = pexp (PRef fc [] n) ++ mkMethApp ps (n, _, _, ty) + = lamBind 0 ty (papp fc (PRef fc [] n) + (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))+ where+ needed is p = pname p `elem` map pname is+ lamBind i (PPi (Constraint _ _) _ _ _ sc) sc' = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc') lamBind i (PPi _ n _ ty sc) sc'@@ -254,8 +309,10 @@ _ -> return ps' getWParams (_ : ps) = getWParams ps - decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns- decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns+ decorate ns iname (NS (UN nm) s)+ = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns+ decorate ns iname nm + = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n NoFC@@ -265,10 +322,14 @@ conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x) conbind [] x = x - coninsert :: [(Name, PTerm)] -> PTerm -> PTerm- coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)- coninsert cs sc = conbind cs sc+ extrabind :: [(Name, PTerm)] -> PTerm -> PTerm+ extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)+ extrabind [] x = x + coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm+ coninsert cs ex (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)+ coninsert cs ex sc = conbind cs (extrabind ex sc)+ -- Reorder declarations to be in the same order as defined in the -- class declaration (important so that we insert default definitions -- in the right place, and so that dependencies between methods are@@ -314,6 +375,100 @@ clauseFor m iname ns (PClauses _ _ m' _) = decorate ns iname m == decorate ns iname m' clauseFor m iname ns _ = False+ +getHeadVars :: PTerm -> [Name]+getHeadVars (PRef _ _ n) | implicitable n = [n]+getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)+getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r+getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t+getHeadVars _ = []++-- Implicitly bind variables from the instance head in method types+impBind :: [(Name, PTerm)] -> PDecl -> PDecl+impBind vs (PTy d ds syn fc opts n fc' t)+ = PTy d ds syn fc opts n fc' + (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)+ where+ doImpBind [] ty = ty+ doImpBind ((n, argty) : ns) ty + = PPi impl n NoFC argty (doImpBind ns ty)++ boundIn (PPi _ n _ _ sc) = n : boundIn sc+ boundIn _ = []++getTypeIn :: IState -> Name -> Type -> PTerm+getTypeIn ist n (Bind x b sc)+ | n == x = delab ist (binderTy b)+ | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)+getTypeIn ist n tm = Placeholder++toImp fc n = pimp n (PRef fc [] n) True++-- Propagate class parameters to method bodies, if they're not already +-- there, and they are needed (i.e. appear in method's type)+addParams :: [Name] -> PDecl -> PDecl+addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)+ where+ addCParams (PClause fc n lhs ws rhs wb)+ = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb+ addCParams (PWith fc n lhs ws sc pn ds)+ = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn + (map (addParams ps) ds)+ addCParams c = c++ addTmParams ps (PRef fc hls n) + = PApp fc (PRef fc hls n) (map (toImp fc) ps)+ addTmParams ps (PApp fc ap@(PRef fc' hls n) args)+ = PApp fc ap (mergePs (map (toImp fc) ps) args)+ addTmParams ps tm = tm++ mergePs [] args = args+ mergePs (p : ps) args+ | isImplicit p,+ pname p `notElem` map pname args+ = p : mergePs ps args+ where+ isImplicit (PExp{}) = False+ isImplicit _ = True+ mergePs (p : ps) args+ = mergePs ps args++ -- Don't propagate a parameter if the name is rebound explicitly+ dropPs :: [Name] -> [Name] -> [Name]+ dropPs ns = filter (\x -> x `notElem` ns)++addParams ps d = d++-- Check a given method definition is injective, if the class info+-- says it needs to be.+-- Takes originally written decl and the one with name decoration, so+-- we know which name to look up.+checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] -> + (PDecl, PDecl) -> Idris ()+checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)+ | Just (True, _, _) <- clookup n ns+ = do ist <- getIState+ case lookupDefExact elabn (tt_ctxt ist) of+ Just (CaseOp _ _ _ _ _ cdefs) ->+ checkInjectiveCase ist (snd (cases_compiletime cdefs))+ where+ checkInjectiveCase ist (STerm tm) + = checkInjectiveApp ist (fst (unApply tm))+ checkInjectiveCase _ _ = notifail++ checkInjectiveApp ist (P (TCon _ _) n _) = return ()+ checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()+ checkInjectiveApp ist (P Ref n _) + | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()+ checkInjectiveApp ist (P Ref n _) = notifail+ checkInjectiveApp _ _ = notifail++ notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))++ clookup n [] = Nothing+ clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d+ | otherwise = Nothing+checkInjectiveDef fc ns _ = return() checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris () checkInjectiveArgs fc n ds Nothing = return ()
src/Idris/Elab/Term.hs view
@@ -85,7 +85,7 @@ mapM_ (\n -> when (n `elem` hs) $ do focus n g <- goal- try (resolveTC' True False 10 g fn ist)+ try (resolveTC' True True 10 g fn ist) (movelast n)) ivs ivs <- get_instances hs <- get_holes@@ -313,13 +313,13 @@ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),- ht == txt "Lazy'" = notDelay orig+ ht == txt "Delayed" = notDelay orig forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),- ht == txt "Lazy'" = notDelay orig+ ht == txt "Delayed" = notDelay orig forceErr orig env (InfiniteUnify _ t _) | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),- ht == txt "Lazy'" = notDelay orig+ ht == txt "Delayed" = notDelay orig forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t forceErr orig env (At _ t) = forceErr orig env t@@ -482,7 +482,7 @@ return $ pruneByType env tc (unDelay ty) ist as unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,- l == txt "Lazy'" = unDelay arg+ l == txt "Delayed" = unDelay arg | otherwise = t isAmbiguous (CantResolveAlts _) = delayok@@ -1400,7 +1400,7 @@ let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty) let tries = [mkDelay env t, t] case tyh of- P _ (UN l) _ | l == txt "Lazy'"+ P _ (UN l) _ | l == txt "Delayed" -> return (PAlternative [] FirstSuccess tries) _ -> return t where@@ -1630,7 +1630,8 @@ ctxt = tt_ctxt ist -- Get the function at the head of the alternative and see if it's- -- a plausible match against the goal type. Keep if so.+ -- a plausible match against the goal type. Keep if so. Also keep if+ -- there is a possible coercion to the goal type. headIs var f (PRef _ _ f') = typeHead var f f' headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg]) | l == txt "Delay" = headIs var f (getTm arg)@@ -1652,6 +1653,7 @@ (V _, _) -> isPlausible ist var env n ty _ -> matching (getRetTy ty') goalty + || isCoercion (getRetTy ty') goalty -- May be useful to keep for debugging purposes for a bit: -- let res = matching (getRetTy ty') goalty in -- traceWhen (not res)@@ -1678,6 +1680,30 @@ matching (TType _) (TType _) = True matching (UType _) (UType _) = True matching l r = l == r++ -- Return whether there is a possible coercion between the return type+ -- of an alternative and the goal type+ isCoercion rty gty | (P _ r _, _) <- unApply rty+ = not (null (getCoercionsBetween r gty))+ isCoercion _ _ = False+ + getCoercionsBetween :: Name -> Type -> [Name]+ getCoercionsBetween r goal+ = let cs = getCoercionsTo ist goal in+ findCoercions r cs+ where findCoercions t [] = []+ findCoercions t (n : ns) =+ let ps = case lookupTy n (tt_ctxt ist) of+ [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in+ [n | any useR as]+ _ -> [] in+ ps ++ findCoercions t ns++ useR ty = + case unApply (getRetTy ty) of+ (P _ t _, _) -> t == r+ _ -> False+ pruneByType _ t _ _ as = as
src/Idris/Elab/Utils.hs view
@@ -426,3 +426,27 @@ displayImpWarning (fc, n) = iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n" ++ "\tDid you mean to refer to " ++ show n ++ "?"++propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm+propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)+ = PApp fc (PRef fc hls n) (addP t args)+ where addP (Bind n _ sc) (t : ts)+ | Placeholder <- getTm t,+ n `elem` ps,+ not (n `elem` bound)+ = t { getTm = PPatvar NoFC n } : addP sc ts+ addP (Bind n _ sc) (t : ts) = t : addP sc ts+ addP _ ts = ts+propagateParams i ps t bound (PApp fc ap args)+ = PApp fc (propagateParams i ps t bound ap) args+propagateParams i ps t bound (PRef fc hls n)+ = case lookupCtxt n (idris_implicits i) of+ [is] -> let ps' = filter (isImplicit is) ps in+ PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')+ _ -> PRef fc hls n+ where isImplicit [] n = False+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True+ isImplicit (_ : is) n = isImplicit is n+propagateParams i ps t bound x = x++
src/Idris/ElabDecls.hs view
@@ -239,6 +239,11 @@ pblock i = map (expandParamsD False i id ns (concatMap tldeclared ps)) ps +elabDecl' what info (POpenInterfaces f ns ds)+ = do open <- addOpenImpl ns+ mapM_ (elabDecl' what info) ds+ setOpenImpl open+ elabDecl' what info (PNamespace n nfc ps) = do mapM_ (elabDecl' what ninfo) ps let ns = reverse (map T.pack newNS)@@ -251,9 +256,9 @@ | what /= EDefns = do logElab 1 $ "Elaborating class " ++ show n elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd-elabDecl' what info (PInstance doc argDocs s f cs acc fnopts n nfc ps t expn ds)+elabDecl' what info (PInstance doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds) = do logElab 1 $ "Elaborating instance " ++ show n- elabInstance info s doc argDocs what f cs acc fnopts n nfc ps t expn ds+ elabInstance info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn) = do logElab 1 $ "Elaborating record " ++ show name elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
src/Idris/IBC.hs view
@@ -40,7 +40,7 @@ import Codec.Archive.Zip ibcVersion :: Word16-ibcVersion = 138+ibcVersion = 143 -- When IBC is being loaded - we'll load different things (and omit different -- structures/definitions) depending on which phase we're in@@ -95,6 +95,7 @@ ibc_deprecated :: ![(Name, String)], ibc_defs :: ![(Name, Def)], ibc_total :: ![(Name, Totality)],+ ibc_injective :: ![(Name, Injectivity)], ibc_access :: ![(Name, Accessibility)], ibc_fragile :: ![(Name, String)] }@@ -104,7 +105,7 @@ !-} initIBC :: IBCFile-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] []+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] hasValidIBCVersion :: FilePath -> Idris Bool hasValidIBCVersion fp = do@@ -197,6 +198,7 @@ makeEntry "ibc_deprecated" (ibc_deprecated i), makeEntry "ibc_defs" (ibc_defs i), makeEntry "ibc_total" (ibc_total i),+ makeEntry "ibc_injective" (ibc_injective i), makeEntry "ibc_access" (ibc_access i), makeEntry "ibc_fragile" (ibc_fragile i)] @@ -300,6 +302,7 @@ ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f } ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f } ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }+ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f } ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f } ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f } ibc i (IBCLineApp fp l t) f@@ -394,6 +397,7 @@ processDeprecate archive processDefs archive processTotal archive+ processInjective archive processAccess reexp phase archive processFragile archive @@ -718,6 +722,11 @@ ds <- getEntry [] "ibc_total" ar mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds +processInjective :: Archive -> Idris ()+processInjective ar = do+ ds <- getEntry [] "ibc_injective" ar+ mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setInjective n a (tt_ctxt i) })) ds+ processTotalityCheckError :: Archive -> Idris () processTotalityCheckError ar = do es <- getEntry [] "ibc_totcheckfail" ar@@ -1371,7 +1380,7 @@ put x10 put x11 put x12- PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ->+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 -> do putWord8 8 put x1 put x2@@ -1386,6 +1395,8 @@ put x11 put x12 put x13+ put x14+ put x15 PDSL x1 x2 -> do putWord8 9 put x1 put x2@@ -1427,6 +1438,10 @@ put x1 put x2 put x3+ POpenInterfaces x1 x2 x3 -> do putWord8 18+ put x1+ put x2+ put x3 get = do i <- getWord8 case i of@@ -1502,7 +1517,9 @@ x11 <- get x12 <- get x13 <- get- return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)+ x14 <- get+ x15 <- get+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) 9 -> do x1 <- get x2 <- get return (PDSL x1 x2)@@ -1542,6 +1559,10 @@ x2 <- get x3 <- get return (PRunElabDecl x1 x2 x3)+ 18 -> do x1 <- get+ x2 <- get+ x3 <- get+ return (POpenInterfaces x1 x2 x3) _ -> error "Corrupted binary data for PDecl'" instance Binary t => Binary (ProvideWhat' t) where@@ -1570,7 +1591,7 @@ _ -> error "Corrupted binary data for Using" instance Binary SyntaxInfo where- put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _ _)+ put (Syn x1 x2 x3 x4 _ _ x5 x6 x7 _ _ x8 _ _ _) = do put x1 put x2 put x3@@ -1578,6 +1599,7 @@ put x5 put x6 put x7+ put x8 get = do x1 <- get x2 <- get@@ -1586,7 +1608,8 @@ x5 <- get x6 <- get x7 <- get- return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True True)+ x8 <- get+ return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True True) instance (Binary t) => Binary (PClause' t) where put x@@ -2438,13 +2461,25 @@ instance Binary Codegen where put x = case x of- Via str -> do putWord8 0- put str+ Via ir str -> do putWord8 0+ put ir+ put str Bytecode -> putWord8 1 get = do i <- getWord8 case i of 0 -> do x1 <- get- return (Via x1)+ x2 <- get+ return (Via x1 x2) 1 -> return Bytecode _ -> error "Corrupted binary data for Codegen"++instance Binary IRFormat where+ put x = case x of+ IBCFormat -> putWord8 0+ JSONFormat -> putWord8 1+ get = do i <- getWord8+ case i of+ 0 -> return IBCFormat+ 1 -> return JSONFormat+ _ -> error "Corrupted binary data for IRFormat"
src/Idris/Parser.hs view
@@ -213,6 +213,7 @@ where declBody :: Bool -> IdrisParser [PDecl] declBody b = try (instance_ True syn)+ <|> try (openInterface syn) <|> declBody' b <|> using_ syn <|> params syn@@ -337,9 +338,9 @@ (map (updateNs ns) ds) (updateRecCon ns cname) cdocs- updateNs ns (PInstance docs pdocs s fc cs acc opts cn fc' ps ity ni ds)- = PInstance docs pdocs s fc cs acc opts (updateB ns cn) fc'- ps ity (fmap (updateB ns) ni)+ updateNs ns (PInstance docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)+ = PInstance docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'+ ps pextra ity (fmap (updateB ns) ni) (map (updateNs ns) ds) updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds) updateNs ns (PProvider docs s fc fc' pw n)@@ -594,18 +595,12 @@ do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do pushIndent (doc, argDocs) <- docstring syn- ist <- get- let initOpts = if default_total ist- then [TotalFn]- else []- opts <- fnOpts initOpts- acc <- accessibility- opts' <- fnOpts opts+ (opts, acc) <- fnOpts (n_in, nfc) <- fnName let n = expandNS syn n_in fc <- getFC lchar ':'- return (doc, argDocs, fc, opts', n, nfc, acc))+ return (doc, argDocs, fc, opts, n, nfc, acc)) ty <- typeExpr (allowImp syn) terminator -- If it's a top level function, note the accessibility@@ -633,10 +628,40 @@ | otherwise = return True fixityOK _ = return True -{-| Parses function options given initial options+{-| Parses a series of function and accessbility options @-FnOpts ::= 'total'+FnOpts ::= FnOpt* Accessibility FnOpt*+@+ -}+fnOpts :: IdrisParser ([FnOpt], Accessibility)+fnOpts = do+ opts <- many fnOpt+ acc <- accessibility+ opts' <- many fnOpt+ let allOpts = opts ++ opts'+ let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]+ opts'' <- addDefaultTotality (nub existingTotality) allOpts+ return (opts'', acc)+ where prettyTot TotalFn = "total"+ prettyTot PartialFn = "partial"+ prettyTot CoveringFn = "covering"+ addDefaultTotality [] opts = do+ ist <- get+ case default_total ist of+ DefaultCheckingTotal -> return (TotalFn:opts)+ DefaultCheckingCovering -> return (CoveringFn:opts)+ DefaultCheckingPartial -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary+ addDefaultTotality [tot] opts = return opts+ -- Should really be a semantics error instead of a parser error+ addDefaultTotality (tot1:tot2:tots) opts =+ fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)+++{-| Parses a function option++@+FnOpt ::= 'total' | 'partial' | 'covering' | 'implicit'@@ -659,37 +684,31 @@ ; @ -}--- FIXME: Check compatability for function options (i.e. partal/total)------ Issue #1574 on the issue tracker.--- https://github.com/idris-lang/Idris-dev/issues/1574-fnOpts :: [FnOpt] -> IdrisParser [FnOpt]-fnOpts opts- = do reservedHL "total"; fnOpts (TotalFn : opts)- <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))- <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))- <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;- fnOpts (CExport c : opts)- <|> do try (lchar '%' *> reserved "no_implicit");- fnOpts (NoImplicit : opts)- <|> do try (lchar '%' *> reserved "inline");- fnOpts (Inlinable : opts)- <|> do try (lchar '%' *> reserved "assert_total");- fnOpts (AssertTotal : opts)- <|> do try (lchar '%' *> reserved "error_handler");- fnOpts (ErrorHandler : opts)- <|> do try (lchar '%' *> reserved "error_reverse");- fnOpts (ErrorReverse : opts)- <|> do try (lchar '%' *> reserved "reflection");- fnOpts (Reflection : opts)- <|> do try (lchar '%' *> reserved "hint");- fnOpts (AutoHint : opts)- <|> do lchar '%'; reserved "specialise";- lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'- fnOpts (Specialise ns : opts)- <|> do reservedHL "implicit"; fnOpts (Implicit : opts)- <|> return opts- <?> "function modifier"+fnOpt :: IdrisParser FnOpt+fnOpt = do reservedHL "total"; return TotalFn+ <|> do reservedHL "partial"; return PartialFn+ <|> do reservedHL "covering"; return CoveringFn+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;+ return $ CExport c+ <|> do try (lchar '%' *> reserved "no_implicit");+ return NoImplicit+ <|> do try (lchar '%' *> reserved "inline");+ return Inlinable+ <|> do try (lchar '%' *> reserved "assert_total");+ return AssertTotal+ <|> do try (lchar '%' *> reserved "error_handler");+ return ErrorHandler+ <|> do try (lchar '%' *> reserved "error_reverse");+ return ErrorReverse+ <|> do try (lchar '%' *> reserved "reflection");+ return Reflection+ <|> do try (lchar '%' *> reserved "hint");+ return AutoHint+ <|> do lchar '%'; reserved "specialise";+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';+ return $ Specialise ns+ <|> do reservedHL "implicit"; return Implicit+ <?> "function modifier" where nameTimes :: IdrisParser (Name, Maybe Int) nameTimes = do n <- fst <$> fnName t <- option Nothing (do reds <- fmap fst natural@@ -711,12 +730,7 @@ ext <- ppostDecl return (doc, ext) ist <- get- let initOpts = if default_total ist- then [TotalFn]- else []- opts <- fnOpts initOpts- acc <- accessibility- opts' <- fnOpts opts+ (opts, acc) <- fnOpts (n_in, nfc) <- fnName let n = expandNS syn n_in lchar ':'@@ -724,7 +738,7 @@ fc <- getFC terminator addAcc n acc- return (PPostulate ext doc syn fc nfc opts' n ty)+ return (PPostulate ext doc syn fc nfc opts n ty) <?> "postulate" where ppostDecl = do fc <- reservedHL "postulate"; return False <|> do lchar '%'; reserved "extern"; return True@@ -767,6 +781,26 @@ return [PParams fc ns' (concat ds)] <?> "parameters declaration" +{- | Parses an open block++-}++openInterface :: SyntaxInfo -> IdrisParser [PDecl]+openInterface syn =+ do reservedHL "using"+ reservedHL "implementation"+ fc <- getFC+ ns <- sepBy1 fnName (lchar ',')++ openBlock+ ds <- many (decl syn)+ closeBlock+ return [POpenInterfaces fc (map fst ns) (concat ds)]+ <?> "open interface declaration"++++ {- | Parses a mutual declaration (for mutually recursive functions) @@@ -843,7 +877,10 @@ ist <- get let cd' = annotate syn ist cd - ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)+ ds <- many (notEndBlock >> try (instance_ True syn)+ <|> do x <- data_ syn+ return [x]+ <|> fnDecl syn) closeBlock return (cn, cd', concat ds) <?> "class block"@@ -919,15 +956,8 @@ instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl] instance_ kwopt syn = do ist <- get- let initOpts = if default_total ist- then [TotalFn]- else []- (doc, argDocs) <- docstring syn- opts <- fnOpts initOpts- acc <- accessibility- opts' <- fnOpts opts-+ (opts, acc) <- fnOpts if kwopt then optional instanceKeyword else do instanceKeyword return (Just ())@@ -940,8 +970,9 @@ args <- many (simpleExpr syn) let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args) let t = bindList (PPi constraint) cs sc+ pnames <- instanceUsing ds <- instanceBlock syn- return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]+ return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds] <?> "implementation declaration" where instanceName :: IdrisParser Name instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'@@ -954,6 +985,12 @@ fc <- getFC parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.") + instanceUsing :: IdrisParser [Name]+ instanceUsing = do reservedHL "using"+ ns <- sepBy1 fnName (lchar ',')+ return (map fst ns)+ <|> return []+ -- | Parse a docstring docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm),@@ -1013,7 +1050,7 @@ t <- typeExpr (disallowImp syn) return (UImplicit x t)) <|> do c <- fst <$> fnName- xs <- some (fst <$> fnName)+ xs <- many (fst <$> fnName) return (UConstraint c xs) <?> "using declaration" @@ -1201,13 +1238,12 @@ return $ PWith fc n capp wargs wval pn withs) <|> do pushIndent (n_in, nfc) <- fnName; let n = expandNS syn n_in- cargs <- many (constraintArg syn) fc <- getFC args <- many (try (implicitArg (syn { inPattern = True } ))+ <|> try (constraintArg (syn { inPattern = True })) <|> (fmap pexp (argExpr syn))) wargs <- many (wExpr syn)- let capp = PApp fc (PRef nfc [nfc] n)- (cargs ++ args)+ let capp = PApp fc (PRef nfc [nfc] n) args (do r <- rhs syn n ist <- get let ctxt = tt_ctxt ist@@ -1288,7 +1324,7 @@ -} codegen_ :: IdrisParser Codegen codegen_ = do n <- fst <$> identifier- return (Via (map toLower n))+ return (Via IBCFormat (map toLower n)) <|> do reserved "Bytecode"; return Bytecode <?> "code generation language" @@ -1343,6 +1379,10 @@ return [PDirective (DHide n)] <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName [] return [PDirective (DFreeze n)]+ -- injectivity assertins are intended for debugging purposes+ -- only, and won't be documented/could be removed at any point+ <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName+ return [PDirective (DInjective n)] <|> do try (lchar '%' *> reserved "access") acc <- accessibility ist <- get@@ -1396,14 +1436,15 @@ {- | Parses a totality @-Totality ::= 'partial' | 'total'+Totality ::= 'partial' | 'total' | 'covering' @ -}-totality :: IdrisParser Bool+totality :: IdrisParser DefaultTotality totality- = do reservedHL "total"; return True- <|> do reservedHL "partial"; return False+ = do reservedHL "total"; return DefaultCheckingTotal+ <|> do reservedHL "partial"; return DefaultCheckingPartial+ <|> do reservedHL "covering"; return DefaultCheckingCovering {- | Parses a type provider @@ -1768,10 +1809,15 @@ -- Redo totality check for deferred names let deftots = idris_defertotcheck i- logLvl 1 $ "Totality checking " ++ show deftots+ logLvl 2 $ "Totality checking " ++ show deftots mapM_ (\x -> do tot <- getTotality x case tot of- Total _ -> setTotality x Unchecked+ Total _ ->+ do let opts = case lookupCtxtExact x (idris_flags i) of+ Just os -> os+ Nothing -> []+ when (AssertTotal `notElem` opts) $+ setTotality x Unchecked _ -> return ()) (map snd deftots) mapM_ buildSCG deftots mapM_ checkDeclTotality deftots
src/Idris/Parser/Data.hs view
@@ -204,18 +204,21 @@ fc <- getFC (tyn_in, nfc) <- fnName (do try (lchar ':')- popIndent ty <- typeExpr (allowImp syn) let tyn = expandNS syn tyn_in- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do reservedHL "where" cons <- indentedBlock (constructor syn) accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)- return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do- args <- many (fst <$> name)+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))+ terminator+ return d) <|> (do+ args <- many (do notEndApp+ x <- fst <$> name+ return x) let ty = bindArgs (map (const (PType fc)) args) (PType fc) let tyn = expandNS syn tyn_in- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do+ d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do try (lchar '=') <|> do reservedHL "where" let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data " let n = show tyn_in ++ " "@@ -228,13 +231,14 @@ let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..." fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3] cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")- terminator let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args) cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) -> do let cty = bindArgs cargs conty return (doc, argDocs, x, xfc, cty, cfc, fs)) cons accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')- return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons')))+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))+ terminator+ return d) <?> "data type declaration" where mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
src/Idris/Parser/Expr.hs view
@@ -36,12 +36,18 @@ -- | Allow implicit type declarations allowImp :: SyntaxInfo -> SyntaxInfo-allowImp syn = syn { implicitAllowed = True }+allowImp syn = syn { implicitAllowed = True,+ constraintAllowed = False } -- | Disallow implicit type declarations disallowImp :: SyntaxInfo -> SyntaxInfo-disallowImp syn = syn { implicitAllowed = False }+disallowImp syn = syn { implicitAllowed = False,+ constraintAllowed = False } +-- | Allow scoped constraint arguments+allowConstr :: SyntaxInfo -> SyntaxInfo+allowConstr syn = syn { constraintAllowed = True }+ {-| Parses an expression as a whole @ FullExpr ::= Expr EOF_t;@@ -327,7 +333,7 @@ @ -} caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)-caseOption syn = do lhs <- expr (syn { inPattern = True })+caseOption syn = do lhs <- expr (disallowImp (syn { inPattern = True })) r <- impossible <|> symbol "=>" *> expr syn return (lhs, r) <?> "case option"@@ -432,7 +438,7 @@ <|> do lchar '_'; return Placeholder <?> "expression" -{- |Parses an expression in braces+{- |Parses an expression in parentheses @ Bracketed ::= '(' Bracketed' @@@ -477,8 +483,8 @@ Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l, pexp (PRef fc0 [] (sMN 1000 "ARG"))]))- <|> do l <- expr syn- bracketedExpr syn open l+ <|> do l <- expr (allowConstr syn)+ bracketedExpr (allowConstr syn) open l @@ -891,7 +897,7 @@ -} typeExpr :: SyntaxInfo -> IdrisParser PTerm typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []- sc <- expr syn+ sc <- expr (allowConstr syn) return (bindList (PPi constraint) cs sc) <?> "type signature" @@ -916,13 +922,13 @@ -} lambda :: SyntaxInfo -> IdrisParser PTerm lambda syn = do lchar '\\' <?> "lambda expression"- ((do xt <- try $ tyOptDeclList syn+ ((do xt <- try $ tyOptDeclList (disallowImp syn) fc <- getFC sc <- lambdaTail return (bindList (PLam fc) xt sc)) <|> (do ps <- sepBy (do fc <- getFC- e <- simpleExpr (syn { inPattern = True })+ e <- simpleExpr (disallowImp (syn { inPattern = True })) return (fc, e)) (lchar ',') sc <- lambdaTail@@ -1055,7 +1061,7 @@ explicitPi opts st syn = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')') binder <- bindsymbol opts st syn- sc <- expr syn+ sc <- expr (allowConstr syn) return (bindList (PPi binder) xt sc) autoImplicit opts st syn@@ -1064,7 +1070,7 @@ xt <- typeDeclList syn lchar '}' symbol "->"- sc <- expr syn+ sc <- expr (allowConstr syn) highlightP kw AnnKeyword return (bindList (PPi (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)@@ -1078,7 +1084,7 @@ xt <- typeDeclList syn lchar '}' symbol "->"- sc <- expr syn+ sc <- expr (allowConstr syn) highlightP kw AnnKeyword return (bindList (PPi (TacImp [] Dynamic script)) xt sc) @@ -1096,6 +1102,14 @@ return (bindList (PPi im) xt (bindList (PPi cl) cs sc)) +constraintPi opts st syn =+ do cs <- constraintList1 syn+ sc <- expr syn+ if implicitAllowed syn+ then return (bindList (PPi constraint) cs sc)+ else return (bindList (PPi (Imp opts st False (Just (Impl True False)) True))+ cs sc)+ implicitPi opts st syn = autoImplicit opts st syn <|> defaultImplicit opts st syn@@ -1114,7 +1128,10 @@ st <- static explicitPi opts st syn <|> try (do lchar '{'; implicitPi opts st syn)- <|> unboundPi opts st syn+ <|> if constraintAllowed syn + then try (constraintPi opts st syn)+ <|> unboundPi opts st syn+ else unboundPi opts st syn <?> "dependent type signature" {- | Parses Possible Options for Pi Expressions@@ -1152,9 +1169,9 @@ return [(defname, NoFC, t)]) <?> "type constraint list" where nexpr = try (do (n, fc) <- name; lchar ':'- e <- expr syn+ e <- expr (disallowImp syn) return (n, fc, e))- <|> do e <- expr syn+ <|> do e <- expr (disallowImp syn) return (defname, NoFC, e) defname = sMN 0 "constraint"
src/Idris/Parser/Helpers.hs view
@@ -687,11 +687,12 @@ fcOf :: PDecl -> FC fcOf (PClauses fc _ _ _) = fc collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds+collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds') = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'-collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')- = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'+collect (PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')+ = PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds' collect (d : ds) = d : collect ds collect [] = []
src/Idris/ProofSearch.hs view
@@ -339,25 +339,37 @@ -- | Resolve interfaces. This will only pick up 'normal' implementations, never -- named implementations (which is enforced by 'findInstances'). resolveTC :: Bool -- ^ using default Int- -> Bool -- ^ allow metavariables in the goal+ -> Bool -- ^ allow open implementations -> Int -- ^ depth -> Term -- ^ top level goal, for error messages -> Name -- ^ top level function name, to prevent loops -> (PTerm -> ElabD ()) -- ^ top level elaborator -> IState -> ElabD ()-resolveTC def mvok depth top fn elab ist- = do hs <- get_holes- resTC' [] def hs depth top fn elab ist+resolveTC def openOK depth top fn elab ist+ = do hs <- get_holes+ resTC' [] def openOK hs depth top fn elab ist -resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve interface"-resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True-resTC' tcs defaultOn topholes depth topg fn elab ist+resTC' tcs def openOK topholes 0 topg fn elab ist = fail $ "Can't resolve interface"+resTC' tcs def openOK topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True+resTC' tcs defaultOn openOK topholes depth topg fn elab ist = do compute- g <- goal+ if openOK+ then try' (resolveOpen (idris_openimpls ist))+ resolveNormal+ True+ else resolveNormal++ where+ -- try all the Open implementations first+ resolveOpen open = do t <- goal+ blunderbuss t depth [] open++ resolveNormal = do -- Resolution can proceed only if there is something concrete in the -- determining argument positions. Keep track of the holes in the -- non-determining position, because it's okay for 'trivial' to solve -- those holes and no others.+ g <- goal let (argsok, okholePos) = case tcArgsOK g topholes of Nothing -> (False, []) Just hs -> (True, hs)@@ -380,9 +392,9 @@ try' (trivialTCs okholes elab ist) (do addDefault t tc ttypes let stk = map fst (filter snd $ elab_stack ist)- let insts = findInstances ist t+ let insts = idris_openimpls ist ++ findInstances ist t blunderbuss t depth stk (stk ++ insts)) True- where+ -- returns Just hs if okay, where hs are holes which are okay in the -- goal, or Nothing if not okay to proceed tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn@@ -491,7 +503,7 @@ let got = fst (unApply (getRetTy t)) let depth' = if tc' `elem` tcs then depth - 1 else depth- resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)+ resTC' (got : tcs) defaultOn openOK topholes depth' topg fn elab ist) (filter (\ (x, y) -> not x) (zip (map fst imps) args)) -- if there's any arguments left, we've failed to resolve hs <- get_holes
src/Idris/REPL.hs view
@@ -903,8 +903,8 @@ fixClauses :: PDecl' t -> PDecl' t fixClauses (PClauses fc opts _ css@(clause:cs)) = PClauses fc opts (getClauseName clause) css- fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName decls) =- PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName (map fixClauses decls)+ fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =+ PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls) fixClauses decl = decl process fn (Undefine names) = undefine names@@ -1249,7 +1249,6 @@ [pexp $ PRef fc [] mainname]) return (Just m') ir <- compile codegen f m- i <- getIState runIO $ generate codegen (fst (head (idris_imported i))) ir where fc = fileFC "main"@@ -1688,7 +1687,7 @@ Object else Executable xs -> last xs let cgn = case opt getCodegen opts of- [] -> Via "c"+ [] -> Via IBCFormat "c" xs -> last xs let cgFlags = opt getCodegenArgs opts @@ -1703,7 +1702,7 @@ let port = getPort opts when (DefaultTotal `elem` opts) $ do i <- getIState- putIState (i { default_total = True })+ putIState (i { default_total = DefaultCheckingTotal }) tty <- runIO $ isATTY setColourise $ not quiet && last (tty : opt getColour opts)
src/Idris/REPL/Parser.hs view
@@ -358,13 +358,13 @@ cmd_compile :: String -> P.IdrisParser (Either String Command) cmd_compile name = do- let defaultCodegen = Via "c"+ let defaultCodegen = Via IBCFormat "c" let codegenOption :: P.IdrisParser Codegen codegenOption = do let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode viaCodegen = do x <- fst <$> P.identifier- return (Via (map toLower x))+ return (Via IBCFormat (map toLower x)) bytecodeCodegen <|> viaCodegen let hasOneArg = do
src/Idris/TypeSearch.hs view
@@ -92,8 +92,8 @@ matcher = matchTypesBulk istate maxScore ty1 -typeFromDef :: (Def, b, c, d) -> Maybe Type-typeFromDef (def, _, _, _) = get def where+typeFromDef :: (Def, i, b, c, d) -> Maybe Type+typeFromDef (def, _, _, _, _) = get def where get :: Def -> Maybe Type get (Function ty _) = Just ty get (TyDecl _ ty) = Just ty@@ -101,10 +101,10 @@ get (CaseOp _ ty _ _ _ _) = Just ty get _ = Nothing --- Replace all occurences of `Lazy' s t` with `t` in a type+-- Replace all occurences of `Delayed s t` with `t` in a type unLazy :: Type -> Type unLazy typ = case typ of- App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty+ App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Delayed" -> unLazy ty Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty) App s t1 t2 -> App s (unLazy t1) (unLazy t2) Proj ty i -> Proj (unLazy ty) i
src/Util/DynamicLinker.hs view
@@ -7,7 +7,7 @@ import Foreign.LibFFI import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr) import System.Directory-#ifndef WINDOWS+#ifndef mingw32_HOST_OS import System.Posix.DynamicLinker import System.FilePath.Posix ((</>)) #else@@ -19,16 +19,14 @@ #endif hostDynamicLibExt :: String-#ifdef LINUX+#if defined(linux_HOST_OS) || defined(freebsd_HOST_OS) \+ || defined(dragonfly_HOST_OS) || defined(openbsd_HOST_OS) \+ || defined(netbsd_HOST_OS) hostDynamicLibExt = "so"-#elif MACOSX+#elif defined(darwin_HOST_OS) hostDynamicLibExt = "dylib"-#elif WINDOWS+#elif defined(mingw32_HOST_OS) hostDynamicLibExt = "dll"-#elif FREEBSD-hostDynamicLibExt = "so"-#elif DRAGONFLY-hostDynamicLibExt = "so" #else hostDynamicLibExt = error $ unwords [ "Undefined file extension for dynamic libraries"@@ -61,7 +59,7 @@ map ("."</>) names ++ [d </> f | d <- cwd:dirs, f <- names] return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found -#ifndef WINDOWS+#ifndef mingw32_HOST_OS tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib) tryLoadLib dirs lib = do filename <- libFileName dirs lib handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]
− test/classes001/ClassName.idr
@@ -1,49 +0,0 @@-module ClassName--||| A fancy shower with a constructor-||| @ a the thing to be shown-interface MyShow a where- ||| Build a MyShow- constructor MkMyShow- ||| The shower- ||| @ x will become a string- myShow : (x : a) -> String--twiceAString : MyShow a => a -> String-twiceAString x = myShow x ++ myShow x--implementation MyShow Integer where- myShow x = show x--badShow : MyShow Integer-badShow = MkMyShow (const "hej")--test1 : twiceAString 2 = "22"-test1 = Refl--test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"-test2 = Refl---||| Parent interface fun-interface MyMagma a where- constructor MkMyMagma- total op : a -> a -> a--||| Semigroup-interface MyMagma a => MySemigroup a where- constructor MkMySemigroup- total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z--implementation [addition] MyMagma Nat where- op = plus--additionS : MySemigroup Nat-additionS = MkMySemigroup @{addition} plusAssociative--doIt : MySemigroup a => a -> List a -> a-doIt x [] = x-doIt x (y :: xs) = doIt (x `op` y) xs--test : Nat-test = doIt @{additionS} 22 [1,2,3,4]
− test/classes001/expected
@@ -1,29 +0,0 @@-Interface MyShow- A fancy shower with a constructor--Parameters:- a -- the thing to be shown--Methods:- myShow : MyShow a => (x : a) -> String- The shower- - The function is Total-Implementation constructor:- MkMyShow : (myShow : a -> String) -> MyShow a- Build a MyShow- Arguments:- (implicit) a : Type -- the thing to be shown- - myShow : a -> String -- The shower- -Implementations:- MyShow Integer-MkMyShow : (myShow : a -> String) -> MyShow a- Build a MyShow- Arguments:- (implicit) a : Type -- the thing to be shown- - myShow : a -> String -- The shower- - The function is Total
− test/classes001/input
@@ -1,2 +0,0 @@-:doc MyShow-:doc MkMyShow
− test/classes001/run
@@ -1,3 +0,0 @@-#!/usr/bin/env bash-${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input-rm -f bounded001 *.ibc
+ test/directives002/directives002.idr view
@@ -0,0 +1,14 @@+module directives002++%access export+%default covering++loop : ()+loop = loop+ +namespace Main+ total+ main : IO ()+ main = do+ pure loop+ putStrLn $ "Hello World"
+ test/directives002/expected view
@@ -0,0 +1,2 @@+directives002.idr:12:3:+directives002.Main.main is possibly not total due to: directives002.loop
+ test/directives002/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ directives002.idr --check --nocolour++rm -f directives002 *.ibc
+ test/interfaces001/ClassName.idr view
@@ -0,0 +1,49 @@+module ClassName++||| A fancy shower with a constructor+||| @ a the thing to be shown+interface MyShow a where+ ||| Build a MyShow+ constructor MkMyShow+ ||| The shower+ ||| @ x will become a string+ myShow : (x : a) -> String++twiceAString : MyShow a => a -> String+twiceAString x = myShow x ++ myShow x++implementation MyShow Integer where+ myShow x = show x++badShow : MyShow Integer+badShow = MkMyShow (const "hej")++test1 : twiceAString 2 = "22"+test1 = Refl++test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"+test2 = Refl+++||| Parent interface fun+interface MyMagma a where+ constructor MkMyMagma+ total op : a -> a -> a++||| Semigroup+interface MyMagma a => MySemigroup a where+ constructor MkMySemigroup+ total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z++implementation [addition] MyMagma Nat where+ op = plus++additionS : MySemigroup Nat+additionS = MkMySemigroup @{addition} plusAssociative++doIt : MySemigroup a => a -> List a -> a+doIt x [] = x+doIt x (y :: xs) = doIt (x `op` y) xs++test : Nat+test = doIt @{additionS} 22 [1,2,3,4]
+ test/interfaces001/expected view
@@ -0,0 +1,29 @@+Interface MyShow+ A fancy shower with a constructor++Parameters:+ a -- the thing to be shown++Methods:+ myShow : MyShow a => (x : a) -> String+ The shower+ + The function is Total+Implementation constructor:+ MkMyShow : (myShow : a -> String) -> MyShow a+ Build a MyShow+ Arguments:+ (implicit) a : Type -- the thing to be shown+ + myShow : a -> String -- The shower+ +Implementations:+ MyShow Integer+MkMyShow : (myShow : a -> String) -> MyShow a+ Build a MyShow+ Arguments:+ (implicit) a : Type -- the thing to be shown+ + myShow : a -> String -- The shower+ + The function is Total
+ test/interfaces001/input view
@@ -0,0 +1,2 @@+:doc MyShow+:doc MkMyShow
+ test/interfaces001/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input+rm -f *.ibc
+ test/interfaces002/expected view
@@ -0,0 +1,1 @@+41
+ test/interfaces002/interfaces002.idr view
@@ -0,0 +1,39 @@+import Data.Vect++interface ArrayM where+ Array : (n : Nat) -> (a : Type) -> Type+ + create : (n : Nat) -> a -> Array n a++ lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a+ upd : a -> (i : Nat) -> (prf : LT i n) -> Array n a -> Array n a++using (ArrayM)+ sumArrayHelp : Num a => (k : Nat) -> LT k (S n) -> Array n a -> a+ sumArrayHelp Z x y = 0+ sumArrayHelp (S k) (LTESucc prf) y + = lkp k prf y + sumArrayHelp k (lteSuccRight prf) y++ sumArray : Array n Int -> Int+ sumArray {n} x = sumArrayHelp n lteRefl x++implementation ArrayM where+ Array = Vect ++ create n x = replicate n x++ lkp Z (LTESucc x) (y :: xs) = y+ lkp (S k) (LTESucc x) (y :: xs) = lkp k x xs++ upd val Z (LTESucc p) (_ :: xs) = val :: xs + upd val (S k) (LTESucc p) (x :: xs) = x :: upd val k p xs++-- using (ArrayM as vectArray)++testSum : Array n Int -> Int+testSum = sumArray ++main : IO ()+main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))++
+ test/interfaces002/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces002.idr -o interfaces002+./interfaces002+rm -f interfaces002 *.ibc
+ test/interfaces003/expected view
@@ -0,0 +1,2 @@+10+9
+ test/interfaces003/interfaces003.idr view
@@ -0,0 +1,22 @@+interface NumMod where+ number : Bool -> Int++implementation [Five] NumMod where+ number b = 5++foo : NumMod => Int+foo = number True + number False++Increment : Int -> NumMod -> NumMod+Increment inc x = AddOne+ where+ foo : NumMod+ foo = x++ implementation [AddOne] NumMod where+ number x = if x then number@{foo} x + inc else inc++using implementation Five+ main : IO ()+ main = do printLn foo + printLn (foo @{Increment 2 Five})
+ test/interfaces003/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces003.idr -o interfaces003+./interfaces003+rm -f interfaces003 *.ibc
+ test/interfaces004/expected view
@@ -0,0 +1,4 @@+12+36+True+False
+ test/interfaces004/interfaces004.idr view
@@ -0,0 +1,35 @@++[PlusNatSemi] Semigroup Nat where+ (<+>) x y = x + y++[MultNatSemi] Semigroup Nat where+ (<+>) x y = x * y++[PlusNatMonoid] Monoid Nat using PlusNatSemi where+ neutral = 0++[MultNatMonoid] Monoid Nat using MultNatSemi where+ neutral = 1++test : Monoid a => a -> a+test x = x <+> x <+> neutral++[CmpLess] Ord Int where+ compare x y = if (x == y) then EQ else+ if (boolOp prim__sltInt x y) then GT else LT++foo : Int -> Int -> Bool+foo x y = x < y++using implementation CmpLess+ foo' : Int -> Int -> Bool+ foo' x y = x < y++using implementation PlusNatMonoid+ main : IO ()+ main = do printLn (test (the Nat 6))+ printLn (test @{MultNatMonoid} 6)+ + printLn (foo 3 4)+ printLn (foo' 3 4)+
+ test/interfaces004/run view
@@ -0,0 +1,4 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces004.idr -o interfaces004+./interfaces004+rm -f interfaces004 *.ibc
+ test/interfaces005/expected view
@@ -0,0 +1,7 @@+interfaces005a.idr:18:3:+Set.TreeSet.Set must be defined by a type or data constructor+No such variable TreeSet+interfaces005b.idr:4:11:+Data definitions not allowed in a class declaration+interfaces005b.idr:18:3:SetSig is not an interface+No such variable TreeSet
+ test/interfaces005/interfaces005.idr view
@@ -0,0 +1,53 @@+module Set+ +public export+interface SetSig a where+ data SetT : Type -> Type++ new : SetT a+ insert : a -> SetT a -> SetT a+ member : a -> SetT a -> Bool++Set : (a : Type) -> SetSig a => Type+Set (a) @{sig} = SetT @{sig} a++data Tree a = Leaf | Node (Tree a) a (Tree a)++mkTree : Type -> Type+mkTree = Tree++namespace TreeSet+ export+ [TreeSet] Ord a => SetSig a where++ SetT = Tree ++ new = Leaf++ insert x Leaf = Node Leaf x Leaf+ insert x (Node l val r) = case compare x val of+ LT => Node (insert x l) val r+ EQ => Node l val r+ GT => Node l val (insert x r)++ member x Leaf = False+ member x (Node l val r) = case compare x val of+ LT => member x l+ EQ => True+ GT => member x r++using implementation TreeSet++ test : Set Nat+ test = insert 3 $ + insert 2 $ + insert 7 $ + insert 3 $ + insert 4 $ + insert 5 new ++ foo : Bool+ foo = member 6 test++ bar : Bool+ bar = member 3 test
+ test/interfaces005/interfaces005a.idr view
@@ -0,0 +1,50 @@+module Set+ +public export+interface SetSig a where+ data Set : Type -> Type++ new : Set a+ insert : a -> Set a -> Set a+ member : a -> Set a -> Bool++data Tree a = Leaf | Node (Tree a) a (Tree a)++mkTree : Type -> Type+mkTree = Tree++namespace TreeSet+ export+ [TreeSet] Ord a => SetSig a where++ Set = mkTree ++ new = Leaf++ insert x Leaf = Node Leaf x Leaf+ insert x (Node l val r) = case compare x val of+ LT => Node (insert x l) val r+ EQ => Node l val r+ GT => Node l val (insert x r)++ member x Leaf = False+ member x (Node l val r) = case compare x val of+ LT => member x l+ EQ => True+ GT => member x r++using implementation TreeSet++ test : Set @{TreeSet {a=Nat}} Nat+ test = insert 3 $ + insert 2 $ + insert 7 $ + insert 3 $ + insert 4 $ + insert 5 new ++ foo : Bool+ foo = member 6 test++ bar : Bool+ bar = member 3 test
+ test/interfaces005/interfaces005b.idr view
@@ -0,0 +1,50 @@+module Set+ +public export+interface SetSig a where+ data Set : Type -> Type where MkSet : List a -> Set a++ new : Set a+ insert : a -> Set a -> Set a+ member : a -> Set a -> Bool++data Tree a = Leaf | Node (Tree a) a (Tree a)++mkTree : Type -> Type+mkTree = Tree++namespace TreeSet+ export+ [TreeSet] Ord a => SetSig a where++ Set = Tree ++ new = Leaf++ insert x Leaf = Node Leaf x Leaf+ insert x (Node l val r) = case compare x val of+ LT => Node (insert x l) val r+ EQ => Node l val r+ GT => Node l val (insert x r)++ member x Leaf = False+ member x (Node l val r) = case compare x val of+ LT => member x l+ EQ => True+ GT => member x r++using implementation TreeSet++ test : Set @{TreeSet {a=Nat}} Nat+ test = insert 3 $ + insert 2 $ + insert 7 $ + insert 3 $ + insert 4 $ + insert 5 new ++ foo : Bool+ foo = member 6 test++ bar : Bool+ bar = member 3 test
+ test/interfaces005/run view
@@ -0,0 +1,5 @@+#!/usr/bin/env bash+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005.idr --check+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005a.idr --check+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005b.idr --check+rm -rf *.ibc
test/reg072/expected view
@@ -6,7 +6,7 @@ Type mismatch between x = x (Type of Refl) and- negate 0.0 = 0.0 (Expected type)+ (-0.0) = 0.0 (Expected type) Specifically: Type mismatch between