Merge branch 'main' into issue-2766-hint-not-listed-as-a-pragma

CHANGELOG_NEXT.md

@@ -18,6 +18,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * The `idris2 --help pragma` command now outputs the `%hint` pragma.
 
+* The `idris2 --init` command now ensures that package names are
+  valid Idris2 identifiers.
+
 ### Building/Packaging changes
 
 * The Nix flake's `buildIdris` function now returns a set with `executable` and
@@ -76,9 +79,6 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun`
   and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`.
 
-* Totality checking will now look under data constructors, so `Just xs` will
-  be considered smaller than `Just (x :: xs)`.
-
 * LHS of `with`-applications are parsed as `PWithApp` instead of `PApp`. As a
   consequence, `IWithApp` appears in `TTImp` values in elaborator scripts instead
   of `IApp`, as it should have been.

libs/base/Language/Reflection/TT.idr

@@ -170,6 +170,12 @@ data Name = NS Namespace Name -- name in a namespace
 
 %name Name nm
 
+%nameLit fromName
+
+public export
+fromName : Name -> Name
+fromName nm = nm
+
 export
 dropNS : Name -> Name
 dropNS (NS _ n) = dropNS n

libs/base/Language/Reflection/TTImp.idr

@@ -222,6 +222,18 @@ mutual
 
   %name Decl decl
 
+%TTImpLit fromTTImp
+
+public export
+fromTTImp : TTImp -> TTImp
+fromTTImp s = s
+
+%declsLit fromDecls
+
+public export
+fromDecls : List Decl -> List Decl
+fromDecls decls = decls
+
 public export
 getFC : TTImp -> FC
 getFC (IVar fc _)                = fc

libs/linear/System/Concurrency/Session.idr

@@ -186,7 +186,7 @@ end : LinearIO io => Channel End -@ L io ()
 end (MkChannel _ _ _) = do
   pure ()
 
-||| Given a session, create a bidirectional communiaction channel and
+||| Given a session, create a bidirectional communication channel and
 ||| return its two endpoints
 export
 makeChannel :

src/Core/Termination/CallGraph.idr

@@ -1,13 +1,11 @@
 module Core.Termination.CallGraph
 
-import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env
 import Core.Normalise
 import Core.Value
 
-import Libraries.Data.IntMap
 import Libraries.Data.SparseMatrix
 
 import Data.String
@@ -136,100 +134,56 @@ mutual
                     else pure $ Ref fc Func n
         conIfGuarded tm = pure tm
 
-  knownOr : Core SizeChange -> Core SizeChange -> Core SizeChange
-  knownOr x y = case !x of Unknown => y; _ => x
+  knownOr : SizeChange -> Lazy SizeChange -> SizeChange
+  knownOr Unknown y = y
+  knownOr x _ = x
 
-  plusLazy : Core SizeChange -> Core SizeChange -> Core SizeChange
-  plusLazy x y = case !x of Smaller => pure Smaller; x => pure $ x |+| !y
+  plusLazy : SizeChange -> Lazy SizeChange -> SizeChange
+  plusLazy Smaller _ = Smaller
+  plusLazy x y = x |+| y
 
   -- Return whether first argument is structurally smaller than the second.
-  sizeCompare : {auto defs : Defs} ->
-                Term vars -> -- RHS: term we're checking
+  sizeCompare : Term vars -> -- RHS: term we're checking
                 Term vars -> -- LHS: argument it might be smaller than
-                Core SizeChange
+                SizeChange
 
-  sizeCompareCon : {auto defs : Defs} -> Term vars -> Term vars -> Core Bool
-  sizeCompareTyCon : {auto defs : Defs} -> Term vars -> Term vars -> Bool
-  sizeCompareConArgs : {auto defs : Defs} -> Term vars -> List (Term vars) -> Core Bool
-  sizeCompareApp : {auto defs : Defs} -> Term vars -> Term vars -> Core SizeChange
+  sizeCompareCon : Term vars -> Term vars -> Bool
+  sizeCompareConArgs : Term vars -> List (Term vars) -> Bool
+  sizeCompareApp : Term vars -> Term vars -> SizeChange
 
   sizeCompare s (Erased _ (Dotted t)) = sizeCompare s t
-  sizeCompare _ (Erased _ _) = pure Unknown -- incomparable!
+  sizeCompare _ (Erased _ _) = Unknown -- incomparable!
   -- for an as pattern, it's smaller if it's smaller than either part
   sizeCompare s (As _ _ p t)
       = knownOr (sizeCompare s p) (sizeCompare s t)
   sizeCompare (As _ _ p s) t
       = knownOr (sizeCompare p t) (sizeCompare s t)
-  -- if they're both metas, let sizeEq check if they're the same
-  sizeCompare s@(Meta _ _ _ _) t@(Meta _ _ _ _) = pure (if sizeEq s t then Same else Unknown)
-  -- otherwise try to expand RHS meta
-  sizeCompare s@(Meta n _ i args) t = do
-    Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) | _ => pure Unknown
-    let (PMDef _ [] (STerm _ tm) _ _) = definition gdef | _ => pure Unknown
-    tm <- substMeta (embed tm) args zero []
-    sizeCompare tm t
-    where
-      substMeta : {0 drop, vs : _} ->
-                  Term (drop ++ vs) -> List (Term vs) ->
-                  SizeOf drop -> SubstEnv drop vs ->
-                  Core (Term vs)
-      substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env
-          = substMeta sc as (suc drop) (a :: env)
-      substMeta (Bind bfc n (Let _ c val ty) sc) as drop env
-          = substMeta (subst val sc) as drop env
-      substMeta rhs [] drop env = pure (substs drop env rhs)
-      substMeta rhs _ _ _ = throw (InternalError ("Badly formed metavar solution \{show n}"))
-
   sizeCompare s t
-     = if sizeCompareTyCon s t then pure Same
-       else if !(sizeCompareCon s t)
-          then pure Smaller
-          else knownOr (sizeCompareApp s t) (pure $ if sizeEq s t then Same else Unknown)
-
-  -- consider two types the same size
-  sizeCompareTyCon s t =
-    let (f, args) = getFnArgs t in
-    let (g, args') = getFnArgs s in
-    case f of
-      Ref _ (TyCon _ _) cn => case g of
-        Ref _ (TyCon _ _) cn' => cn == cn'
-        _ => False
-      _ => False
+     = if sizeCompareCon s t
+          then Smaller
+          else knownOr (sizeCompareApp s t) (if sizeEq s t then Same else Unknown)
 
   sizeCompareCon s t
       = let (f, args) = getFnArgs t in
         case f of
-             Ref _ (DataCon t a) cn =>
-                -- if s is smaller or equal to an arg, then it is smaller than t
-                if !(sizeCompareConArgs s args) then pure True
-                else let (g, args') = getFnArgs s in
-                    case g of
-                        Ref _ (DataCon t' a') cn' =>
-                                -- if s is a matching DataCon, applied to same number of args,
-                                -- no Unknown args, and at least one Smaller
-                                if cn == cn' && length args == length args'
-                                  then do
-                                       sizes <- traverse (uncurry sizeCompare) (zip args' args)
-                                       pure $ Smaller == foldl (|*|) Same sizes
-                                  else pure False
-                        _ => pure $ False
-             _ => pure False
-
-  sizeCompareConArgs s [] = pure False
+             Ref _ (DataCon t a) cn => sizeCompareConArgs s args
+             _ => False
+
+  sizeCompareConArgs s [] = False
   sizeCompareConArgs s (t :: ts)
-      = case !(sizeCompare s t) of
+      = case sizeCompare s t of
           Unknown => sizeCompareConArgs s ts
-          _ => pure True
+          _ => True
 
   sizeCompareApp (App _ f _) t = sizeCompare f t
-  sizeCompareApp _ t = pure Unknown
+  sizeCompareApp _ t = Unknown
 
-  sizeCompareAsserted : {auto defs : Defs} -> Maybe (Term vars) -> Term vars -> Core SizeChange
+  sizeCompareAsserted : Maybe (Term vars) -> Term vars -> SizeChange
   sizeCompareAsserted (Just s) t
-      = pure $ case !(sizeCompare s t) of
+      = case sizeCompare s t of
           Unknown => Unknown
           _ => Smaller
-  sizeCompareAsserted Nothing _ = pure Unknown
+  sizeCompareAsserted Nothing _ = Unknown
 
   -- if the argument is an 'assert_smaller', return the thing it's smaller than
   asserted : Name -> Term vars -> Maybe (Term vars)
@@ -246,9 +200,9 @@ mutual
   mkChange : Defs -> Name ->
              (pats : List (Term vars)) ->
              (arg : Term vars) ->
-             Core (List SizeChange)
+             List SizeChange
   mkChange defs aSmaller pats arg
-    = traverse (\p => plusLazy (sizeCompareAsserted (asserted aSmaller arg) p) (sizeCompare arg p)) pats
+    = map (\p => plusLazy (sizeCompareAsserted (asserted aSmaller arg) p) (sizeCompare arg p)) pats
 
   -- Given a name of a case function, and a list of the arguments being
   -- passed to it, update the pattern list so that it's referring to the LHS
@@ -356,7 +310,7 @@ mutual
               (do scs <- traverse (findSC defs env g pats) args
                   pure ([MkSCCall fn
                            (fromListList
-                                !(traverse (mkChange defs aSmaller pats) args))
+                                (map (mkChange defs aSmaller pats) args))
                            fc]
                            ++ concat scs))
 

src/Idris/Package.idr

@@ -903,7 +903,8 @@ processPackage : {auto c : Ref Ctxt Defs} ->
 processPackage opts (cmd, mfile)
     = withCtxt . withSyn . withROpts $ case cmd of
         Init =>
-          do pkg <- coreLift interactive
+          do Just pkg <- coreLift interactive
+               | Nothing => coreLift (exitWith (ExitFailure 1))
              let fp = fromMaybe (pkg.name ++ ".ipkg") mfile
              False <- coreLift (exists fp)
                | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists"))

src/Idris/Package/Init.idr

@@ -12,6 +12,7 @@ import Idris.Package.Types
 import System.Directory
 import Control.App.FileIO
 
+import Libraries.Text.Lexer
 import Libraries.Utils.Path
 import Libraries.System.Directory.Tree
 
@@ -67,9 +68,11 @@ prompt p = putStr p >> fflush stdout >> getLine
 
 export
 covering
-interactive : IO PkgDesc
+interactive : IO (Maybe PkgDesc)
 interactive = do
-  pname    <- prompt "Package name: "
+  pname <- prompt "Package name: "
+  let True = checkPackageName $ fastUnpack pname
+    | False => pure Nothing
   pauthors <- prompt "Package authors: "
   poptions <- prompt "Package options: "
   psource  <- prompt "Source directory: "
@@ -81,11 +84,32 @@ interactive = do
         , modules   := modules
         , sourcedir := sourcedir
         } (initPkgDesc (fromMaybe "project" (mstring pname)))
-  pure pkg
+  pure $ Just pkg
 
   where
 
     mstring : String -> Maybe String
     mstring str = case trim str of
       "" => Nothing
       str => Just str
+
+    isIdentStart : Char -> Bool
+    isIdentStart '_' = True
+    isIdentStart x   = isUpper x ||
+                       isAlpha x ||
+                       x > chr 160
+
+    isIdentTrailing : List Char -> Bool
+    isIdentTrailing []      = True
+    isIdentTrailing (x::xs) = case isAlphaNum x ||
+                                   x > chr 160  ||
+                                   x == '-'     ||
+                                   x == '_'     ||
+                                   x == '\'' of
+                                False => False
+                                True  => isIdentTrailing xs
+
+    checkPackageName : List Char -> Bool
+    checkPackageName []      = True
+    checkPackageName (x::xs) = isIdentStart x &&
+                               isIdentTrailing xs

tests/idris2/reflection/reflection020/FromDecls.idr

@@ -6,8 +6,6 @@ import FromTTImp
 
 %language ElabReflection
 
-%declsLit fromDecls
-
 record NatDecl where
     constructor MkNatDecl
     var : String

tests/idris2/reflection/reflection020/FromName.idr

@@ -2,8 +2,6 @@ import Language.Reflection
 
 %language ElabReflection
 
-%nameLit fromName
-
 data MyName = MkMyName String
 
 myName : Name -> Elab MyName

tests/idris2/reflection/reflection020/FromTTImp.idr

@@ -2,8 +2,6 @@ import Language.Reflection
 
 %language ElabReflection
 
-%TTImpLit fromTTImp
-
 public export
 data NatExpr : Type where
      Plus : NatExpr -> NatExpr -> NatExpr

tests/idris2/reg/reg054/Issue3354.idr

@@ -0,0 +1,12 @@
+import Data.Fin
+
+covering
+g : Fin 64 -> Unit
+g FZ      = ()
+g (FS i') = g $ weaken i'
+
+
+total
+g' : Fin 64 -> Unit
+g' FZ        = ()
+g' i@(FS i') = g' $ assert_smaller i $ weaken i'

tests/idris2/reg/reg054/expected

@@ -0,0 +1 @@
+1/1: Building Issue3354 (Issue3354.idr)

tests/idris2/reg/reg054/run

@@ -0,0 +1,2 @@
+. ../../../testutils.sh
+check Issue3354.idr

tests/idris2/total/total004/expected

@@ -6,7 +6,7 @@ Main> Main.bar is total
 Main> Main.swapR is total
 Main> Main.loopy is possibly not terminating due to recursive path Main.loopy
 Main> Main.foom is total
-Main> Main.pfoom is total
+Main> Main.pfoom is possibly not terminating due to recursive path Main.pfoom
 Main> Main.even is total
 Main> Main.vtrans is possibly not terminating due to recursive path Main.vtrans -> Main.vtrans
 Main> Main.GTree is total