diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 2fab17d03..e2439123c 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -3,6 +3,8 @@ module Prelude import public Builtin import public PrimIO +%default total + {- The Prelude is minimal (since it is effectively part of the language specification, this seems to be desirable - we should, nevertheless, aim to diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 9c0d9fe76..6a661e90e 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -30,7 +30,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 30 +ttcVersion = 31 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 2c9427a39..4ab7f1059 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -215,6 +215,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu unsetFlag fc impName BlockedHint setFlag fc impName TCInline + -- it's the methods we're interested in, not the implementation + setFlag fc impName (SetTotal PartialOK) -- 4. (TODO: Order method bodies to be in declaration order, in -- case of dependencies) @@ -274,7 +276,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu -- inserted in the right place mkMethField : List (Name, RigCount, RawImp) -> List (Name, List (Name, RigCount, PiInfo RawImp)) -> - (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> RawImp + (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp mkMethField methImps fldTys (topn, n, upds, c, treq, ty) = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys)) imps = map fst methImps in @@ -315,8 +317,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu topMethType : List (Name, RawImp) -> Name -> List (Name, RigCount, RawImp) -> List String -> List Name -> List Name -> - (Name, RigCount, TotalReq, (Bool, RawImp)) -> - Core ((Name, Name, List (String, String), RigCount, TotalReq, RawImp), + (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) -> + Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp), List (Name, RawImp)) topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in)) = do -- Get the specialised type by applying the method to the @@ -357,17 +359,18 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu topMethTypes : List (Name, RawImp) -> Name -> List (Name, RigCount, RawImp) -> List String -> List Name -> List Name -> - List (Name, RigCount, TotalReq, (Bool, RawImp)) -> - Core (List (Name, Name, List (String, String), RigCount, TotalReq, RawImp)) + List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) -> + Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp)) topMethTypes upds impName methImps impsp pnames allmeths [] = pure [] topMethTypes upds impName methImps impsp pnames allmeths (m :: ms) = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms pure (m' :: ms') - mkTopMethDecl : (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> ImpDecl + mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl mkTopMethDecl (mn, n, upds, c, treq, mty) - = IClaim fc c vis (Totality treq :: opts_in) (MkImpTy fc n mty) + = let opts = maybe opts_in (\t => Totality t :: opts_in) treq in + IClaim fc c vis opts (MkImpTy fc n mty) -- Given the method type (result of topMethType) return the mapping from -- top level method name to current implementation's method name @@ -418,7 +421,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu "Implementation body can only contain definitions") addTransform : Name -> List (Name, Name) -> - (Name, RigCount, TotalReq, Bool, RawImp) -> + (Name, RigCount, Maybe TotalReq, Bool, RawImp) -> Core () addTransform iname ns (top, _, _, _, ty) = do log 3 $ "Adding transform for " ++ show top ++ " : " ++ show ty ++ diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 6121a44ae..d3db2020c 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -243,9 +243,9 @@ updateIfaceSyn iname cn ps cs ms ds findSetTotal (_ :: xs) = findSetTotal xs totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) -> - Core (Name, RigCount, TotalReq, (Bool, RawImp)) + Core (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) totMeth (n, c, opts, t) - = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts) + = do let treq = findSetTotal opts pure (n, c, treq, t) export diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index dd41b8c88..8ced5d47b 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -503,7 +503,7 @@ record IFaceInfo where iconstructor : Name params : List Name parents : List RawImp - methods : List (Name, RigCount, TotalReq, Bool, RawImp) + methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp) -- ^ name, whether a data method, and desugared type (without constraint) defaults : List (Name, List ImpClause) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index de9ee019d..1afc480dd 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -328,7 +328,7 @@ mutual export Show ImpDecl where - show (IClaim _ _ _ _ ty) = show ty + show (IClaim _ _ _ opts ty) = show opts ++ " " ++ show ty show (IData _ _ d) = show d show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")" show (IParameters _ ps ds)