[ new ] --total cli flag

Author: gallais

CHANGELOG.md

@@ -65,6 +65,7 @@ filter p (x :: xs) with (p x)
 ### REPL/CLI/IDE mode changes
 
 * Added `--list-packages` CLI option.
+* Added `--total` CLI option.
 
 ### Library changes
 

src/Core/Binary.idr

@@ -17,6 +17,7 @@ import Core.UnifyState
 
 import Data.Buffer
 import Data.List
+import Data.String
 
 import System.File
 
@@ -31,7 +32,7 @@ import public Libraries.Utils.Binary
 ||| (Increment this when changing anything in the data format)
 export
 ttcVersion : Int
-ttcVersion = 61
+ttcVersion = 62
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
@@ -41,6 +42,7 @@ checkTTCVersion file ver exp
 record TTCFile extra where
   constructor MkTTCFile
   version : Int
+  totalReq : TotalReq
   sourceHash : String
   ifaceHash : Int
   importHashes : List (Namespace, Int)
@@ -93,14 +95,14 @@ HasNames (Name, Name, Bool) where
   resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
 
 HasNames e => HasNames (TTCFile e) where
-  full gam (MkTTCFile version sourceHash ifaceHash iHashes incData
+  full gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
                       pairnames rewritenames primnames
                       namedirectives cgdirectives trans
                       extra)
-      = pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
+      = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                          context userHoles
                          !(traverse (full gam) autoHints)
                          !(traverse (full gam) typeHints)
@@ -131,14 +133,14 @@ HasNames e => HasNames (TTCFile e) where
   -- I don't think we ever actually want to call this, because after we read
   -- from the file we're going to add them to learn what the resolved names
   -- are supposed to be! But for completeness, let's do it right.
-  resolved gam (MkTTCFile version sourceHash ifaceHash iHashes incData
+  resolved gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
                       pairnames rewritenames primnames
                       namedirectives cgdirectives trans
                       extra)
-      = pure $ MkTTCFile version sourceHash ifaceHash iHashes incData
+      = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
                          context userHoles
                          !(traverse (resolved gam) autoHints)
                          !(traverse (resolved gam) typeHints)
@@ -177,6 +179,7 @@ writeTTCFile b file_in
       = do file <- toFullNames file_in
            toBuf b "TT2"
            toBuf @{Wasteful} b (version file)
+           toBuf b (totalReq file)
            toBuf b (sourceHash file)
            toBuf b (ifaceHash file)
            toBuf b (importHashes file)
@@ -204,17 +207,20 @@ readTTCFile : TTC extra =>
 readTTCFile readall file as b
       = do hdr <- fromBuf b
            chunk <- get Bin
-           when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
+           when (hdr /= "TT2") $
+             corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
            ver <- fromBuf @{Wasteful} b
            checkTTCVersion file ver ttcVersion
+           totalReq <- fromBuf b
            sourceFileHash <- fromBuf b
            ifaceHash <- fromBuf b
            importHashes <- fromBuf b
            incData <- fromBuf b
            imp <- fromBuf b
            ex <- fromBuf b
            if not readall
-              then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
+              then pure (MkTTCFile ver totalReq
+                                   sourceFileHash ifaceHash importHashes
                                    incData [] [] [] [] []
                                    0 (mkNamespace "") [] Nothing
                                    Nothing
@@ -234,7 +240,8 @@ readTTCFile readall file as b
                  nds <- fromBuf b
                  cgds <- fromBuf b
                  trans <- fromBuf b
-                 pure (MkTTCFile ver sourceFileHash ifaceHash importHashes incData
+                 pure (MkTTCFile ver totalReq
+                                 sourceFileHash ifaceHash importHashes incData
                                  (map (replaceNS cns) defs) uholes
                                  autohs typehs imp nextv cns nns
                                  pns rws prims nds cgds trans ex)
@@ -278,9 +285,15 @@ writeToTTC extradata sourceFileName ttcFileName
          ust <- get UST
          gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs
          sourceHash <- hashFileWith defs.options.hashFn sourceFileName
-         log "ttc.write" 5 $ "Writing " ++ ttcFileName ++ " with source hash " ++ sourceHash ++ " and interface hash " ++ show (ifaceHash defs)
+         totalReq <- getDefaultTotalityOption
+         log "ttc.write" 5 $ unwords
+           [ "Writing", ttcFileName
+           , "with source hash", sourceHash
+           , "and interface hash", show (ifaceHash defs)
+           ]
          writeTTCFile bin
-                   (MkTTCFile ttcVersion (sourceHash) (ifaceHash defs) (importHashes defs)
+                   (MkTTCFile ttcVersion totalReq
+                              sourceHash (ifaceHash defs) (importHashes defs)
                               (incData defs)
                               gdefs
                               (keys (userHoles defs))
@@ -507,17 +520,38 @@ getImportHashes file b
          when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
          ver <- fromBuf @{Wasteful} b
          checkTTCVersion file ver ttcVersion
+         totalReq <- fromBuf {a = TotalReq} b
          sourceFileHash <- fromBuf {a = String} b
          interfaceHash <- fromBuf {a = Int} b
          fromBuf b
 
+export
+getTotalReq : String -> Ref Bin Binary -> Core TotalReq
+getTotalReq file b
+    = do hdr <- fromBuf {a = String} b
+         when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
+         ver <- fromBuf @{Wasteful} b
+         checkTTCVersion file ver ttcVersion
+         fromBuf b
+
+export
+readTotalReq : (fileName : String) -> -- file containing the module
+               Core (Maybe TotalReq)
+readTotalReq fileName
+    = do Right buffer <- coreLift $ readFromFile fileName
+            | Left err => pure Nothing
+         b <- newRef Bin buffer
+         catch (Just <$> getTotalReq fileName b)
+               (\err => pure Nothing)
+
 export
 getHashes : String -> Ref Bin Binary -> Core (String, Int)
 getHashes file b
     = do hdr <- fromBuf {a = String} b
          when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
          ver <- fromBuf @{Wasteful} b
          checkTTCVersion file ver ttcVersion
+         totReq <- fromBuf {a = TotalReq} b
          sourceFileHash <- fromBuf b
          interfaceHash <- fromBuf b
          pure (sourceFileHash, interfaceHash)
@@ -529,8 +563,7 @@ readHashes fileName
     = do Right buffer <- coreLift $ readFromFile fileName
             | Left err => pure ("", 0)
          b <- newRef Bin buffer
-         catch (do hashes <- getHashes fileName b
-                   pure hashes)
+         catch (getHashes fileName b)
                (\err => pure ("", 0))
 
 export

src/Core/Context.idr

@@ -1156,7 +1156,9 @@ clearCtxt
                             timings = timings defs } !initDefs)
   where
     resetElab : Options -> Options
-    resetElab = record { elabDirectives = defaultElab }
+    resetElab opts =
+      let tot = totalReq (session opts) in
+      record { elabDirectives = record { totality = tot } defaultElab } opts
 
 export
 getFieldNames : Context -> Namespace -> List Name
@@ -2559,6 +2561,12 @@ setSession sopts
     = do defs <- get Ctxt
          put Ctxt (record { options->session = sopts } defs)
 
+%inline
+export
+updateSession : {auto c : Ref Ctxt Defs} ->
+                (Session -> Session) -> Core ()
+updateSession f = setSession (f !getSession)
+
 export
 recordWarning : {auto c : Ref Ctxt Defs} -> Warning -> Core ()
 recordWarning w

src/Core/Core.idr

@@ -5,6 +5,7 @@ import Core.TT
 
 import Data.List
 import Data.List1
+import Data.String
 import Data.Vect
 
 import Libraries.Data.IMaybe

src/Core/Options.idr

@@ -144,6 +144,7 @@ public export
 record Session where
   constructor MkSessionOpts
   noprelude : Bool
+  totalReq : TotalReq
   nobanner : Bool
   findipkg : Bool
   codegen : CG
@@ -202,7 +203,6 @@ record Options where
   additionalCGs : List (String, CG)
   hashFn : String
 
-
 export
 availableCGs : Options -> List (String, CG)
 availableCGs o
@@ -228,7 +228,7 @@ defaultPPrint = MkPPOpts False True False
 
 export
 defaultSession : Session
-defaultSession = MkSessionOpts False False False Chez [] 1000 False False
+defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False False
                                defaultLogLevel False False Nothing Nothing
                                Nothing Nothing False 1 False True
                                False [] False False

src/Core/Options/Log.idr

@@ -129,6 +129,7 @@ knownTopics = [
     ("specialise", Nothing),
     ("totality", Nothing),
     ("totality.positivity", Nothing),
+    ("totality.requirement", Nothing),
     ("totality.termination", Nothing),
     ("totality.termination.calc", Nothing),
     ("totality.termination.guarded", Nothing),

src/Core/TT.idr

@@ -961,6 +961,16 @@ Eq TotalReq where
     (==) PartialOK PartialOK = True
     (==) _ _ = False
 
+||| Bigger means more requirements
+||| So if a definition was checked at b, it can be accepted at a <= b.
+export
+Ord TotalReq where
+  PartialOK <= _ = True
+  _ <= Total = True
+  a <= b = a == b
+
+  a < b = a <= b && a /= b
+
 export
 Show TotalReq where
     show Total = "total"

src/Core/TTC.idr

@@ -31,7 +31,6 @@ TTC ModuleIdent where
 export
 TTC VirtualIdent where
   toBuf b Interactive = tag 0
-
   fromBuf b =
     case !getTag of
       0 => pure Interactive

src/Idris/CommandLine.idr

@@ -157,7 +157,9 @@ data CLOpt
    ||| Generate bash completion info
   BashCompletion String String |
    ||| Generate bash completion script
-  BashCompletionScript String
+  BashCompletionScript String |
+   ||| Turn on %default total globally
+  Total
 
 ||| Extract the host and port to bind the IDE socket to
 export
@@ -242,6 +244,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Generate profile data when compiling, if supported"),
 
            optSeparator,
+           MkOpt ["--total"] [] [Total]
+              (Just "Require functions to be total by default"),
            MkOpt ["-Werror"] [] [WarningsAsErrors]
               (Just "Treat warnings as errors"),
            MkOpt ["-Wno-shadowing"] [] [IgnoreShadowingWarnings]