Merge branch 'main' into builtin-cons-names

CHANGELOG_NEXT.md

@@ -281,6 +281,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Refactored `Uninhabited` implementation for `Data.List.Elem`, `Data.List1.Elem`, `Data.SnocList.Elem` and `Data.Vect.Elem`
   so it can be used for homogeneous (`===`) and heterogeneous (`~=~`) equality.
 
+* Added `System.Concurrency.channelGetNonBlocking` for the chez backend.
+
+* Added `System.Concurrency.channelGetWithTimeout` for the chez backend.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
@@ -322,7 +326,6 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`
 
-
 #### Test
 
 * Replaced `Requirement` data type with a new record that can be used to create

libs/base/System/Concurrency.idr

@@ -72,19 +72,15 @@ data Condition : Type where [external]
 %foreign "scheme,racket:blodwen-make-cv"
          "scheme,chez:blodwen-make-condition"
 prim__makeCondition : PrimIO Condition
-
 %foreign "scheme,racket:blodwen-cv-wait"
          "scheme,chez:blodwen-condition-wait"
 prim__conditionWait : Condition -> Mutex -> PrimIO ()
-
 %foreign "scheme,chez:blodwen-condition-wait-timeout"
 --         "scheme,racket:blodwen-cv-wait-timeout"
 prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()
-
 %foreign "scheme,racket:blodwen-cv-signal"
          "scheme,chez:blodwen-condition-signal"
 prim__conditionSignal : Condition -> PrimIO ()
-
 %foreign "scheme,racket:blodwen-cv-broadcast"
          "scheme,chez:blodwen-condition-broadcast"
 prim__conditionBroadcast : Condition -> PrimIO ()
@@ -187,6 +183,10 @@ data Channel : Type -> Type where [external]
 prim__makeChannel : PrimIO (Channel a)
 %foreign "scheme:blodwen-channel-get"
 prim__channelGet : Channel a -> PrimIO a
+%foreign "scheme,chez:blodwen-channel-get-non-blocking"
+prim__channelGetNonBlocking : Channel a -> PrimIO (Maybe a)
+%foreign "scheme,chez:blodwen-channel-get-with-timeout"
+prim__channelGetWithTimeout : Channel a -> Int -> PrimIO (Maybe a)
 %foreign "scheme:blodwen-channel-put"
 prim__channelPut : Channel a -> a -> PrimIO ()
 
@@ -208,6 +208,23 @@ export
 channelGet : HasIO io => (chan : Channel a) -> io a
 channelGet chan = primIO (prim__channelGet chan)
 
+||| Non-blocking version of channelGet (chez backend).
+|||
+||| @ chan the channel to receive on
+partial
+export
+channelGetNonBlocking : HasIO io => (chan : Channel a) -> io (Maybe a)
+channelGetNonBlocking chan = primIO (prim__channelGetNonBlocking chan)
+
+||| Timeout version of channelGet (chez backend).
+|||
+||| @ chan the channel to receive on
+||| @ milliseconds how many milliseconds to wait until timeout
+partial
+export
+channelGetWithTimeout : HasIO io => (chan : Channel a) -> (milliseconds : Nat) -> io (Maybe a)
+channelGetWithTimeout chan milliseconds = primIO (prim__channelGetWithTimeout chan (cast milliseconds))
+
 ||| Puts a value on the given channel.
 |||
 ||| @ chan the `Channel` to send the value over

libs/linear/System/Concurrency/Linear.idr

@@ -8,6 +8,17 @@ export
 fork1 : L IO () -@ L IO ThreadID
 fork1 act = liftIO1 $ fork $ LIO.run act
 
+||| Run a computation concurrently to the current thread.
+||| This returns a receiver for the value.
+export
+concurrently : L IO a -@ L1 IO (L IO a)
+concurrently act = do
+  ch <- makeChannel
+  _ <- fork1 $ do
+    x <- act
+    channelPut ch x
+  pure1 $ channelGet ch
+
 ||| Run a computation concurrently to the current thread.
 ||| This returns a receiver for the value. A typical usage
 ||| pattern is showcased by the implementation of `par1`:

libs/papers/Language/IntrinsicTyping/Krivine.idr

@@ -522,13 +522,15 @@ namespace Machine
   public export
   vlam0 : (eq : ctx = []) -> (tr : Trace (Lam sc) env ctx) -> tr ~=~ Machine.Done {sc, env}
   vlam0 eq Done = Refl
+  vlam0 eq (Beta {arg = Element _ _, ctx = Element _ _} _) impossible
 
   public export
   vlamS : {0 env : ValidEnv g} -> {0 arg : ValidClosed a} ->
           {0 sc : Term (a :: g) b} -> {0 ctx' : ValidEvalContext b c} ->
           (eq : ctx = ValidEvalContext.(::) arg ctx') ->
           (tr : Trace (Lam sc) env ctx) ->
           (tr' : Trace sc (arg :: env) ctx' ** tr ~=~ Machine.Beta {sc, arg, env} tr')
+  vlamS {arg = (Element _ _)} {ctx' = (Element _ _)} eq Done impossible
   vlamS eq (Beta tr) with 0 (fst (biinjective @{CONS} eq))
     _ | Refl with 0 (snd (biinjective @{CONS} eq))
       _ | Refl = (tr ** Refl)

src/Compiler/Scheme/Chez.idr

@@ -94,7 +94,9 @@ schHeader chez libs whole
     (import (chezscheme))
     (case (machine-type)
       [(i3fb ti3fb a6fb ta6fb) #f]
-      [(i3le ti3le a6le ta6le tarm64le) (load-shared-object "libc.so.6")]
+      [(i3le ti3le a6le ta6le tarm64le)
+         (with-exception-handler (lambda(x) (load-shared-object "libc.so"))
+            (lambda () (load-shared-object "libc.so.6")))]
       [(i3osx ti3osx a6osx ta6osx tarm64osx tppc32osx tppc64osx) (load-shared-object "libc.dylib")]
       [(i3nt ti3nt a6nt ta6nt) (load-shared-object "msvcrt.dll")]
       [else (load-shared-object "libc.so")])

src/Core/Binary.idr

@@ -29,7 +29,8 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2025_02_05_00
+ttcVersion = 2025_02_09_00
+
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Case/Util.idr

@@ -20,7 +20,7 @@ getCons : {auto c : Ref Ctxt Defs} ->
 getCons defs (NTCon _ tn _ _ _)
     = case !(lookupDefExact tn (gamma defs)) of
            Just (TCon _ _ _ _ _ _ cons _) =>
-                do cs' <- traverse addTy cons
+                do cs' <- traverse addTy (fromMaybe [] cons)
                    pure (catMaybes cs')
            _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
   where

src/Core/Context.idr

@@ -585,9 +585,9 @@ HasNames Def where
       fullNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(full gam env),
                           !(full gam lhs), !(full gam rhs)))
-  full gam (TCon t a ps ds u ms cs det)
+  full gam (TCon t a ps ds u ms mcs det)
       = pure $ TCon t a ps ds u !(traverse (full gam) ms)
-                                !(traverse (full gam) cs) det
+                                !(traverseOpt (traverse (full gam)) mcs) det
   full gam (BySearch c d def)
       = pure $ BySearch c d !(full gam def)
   full gam (Guess tm b cs)
@@ -603,9 +603,9 @@ HasNames Def where
       resolvedNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(resolved gam env),
                           !(resolved gam lhs), !(resolved gam rhs)))
-  resolved gam (TCon t a ps ds u ms cs det)
+  resolved gam (TCon t a ps ds u ms mcs det)
       = pure $ TCon t a ps ds u !(traverse (resolved gam) ms)
-                                !(traverse (resolved gam) cs) det
+                                !(traverseOpt (traverse (full gam)) mcs) det
   resolved gam (BySearch c d def)
       = pure $ BySearch c d !(resolved gam def)
   resolved gam (Guess tm b cs)

src/Core/Context/Context.idr

@@ -101,7 +101,7 @@ data Def : Type where
            (detpos : List Nat) -> -- determining arguments
            (flags : TypeFlags) -> -- should 'auto' implicits check
            (mutwith : List Name) ->
-           (datacons : List Name) ->
+           (datacons : Maybe (List Name)) ->
            (detagabbleBy : Maybe (List Nat)) ->
                     -- argument positions which can be used for
                     -- detagging, if it's possible (to check if it's

src/Core/Context/Data.idr

@@ -104,7 +104,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
                             (TCon tag arity
                                   paramPositions
                                   allPos
-                                  defaultFlags [] (map name datacons) Nothing)
+                                  defaultFlags [] (Just $ map name datacons) Nothing)
          (idx, gam') <- addCtxt tyn tydef (gamma defs)
          gam'' <- addDataConstructors 0 datacons gam'
          put Ctxt ({ gamma := gam'' } defs)

src/Core/Context/Pretty.idr

@@ -57,7 +57,7 @@ namespace Raw
           ([ "tag:" <++> byShow tag
            , "arity:" <++> byShow arity
            , "parameter positions:" <++> byShow ps
-           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
   prettyDef (ExternDef arity) =
@@ -109,7 +109,7 @@ namespace Resugared
           ([ "tag:" <++> byShow tag
            , "arity:" <++> byShow arity
            , "parameter positions:" <++> byShow ps
-           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
   prettyDef (ExternDef arity) = pure $

src/Core/Coverage.idr

@@ -24,20 +24,21 @@ conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool
 conflictMatch [] = False
 conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
   where
-    clash : Term vars -> Term vars -> Bool
+    data ClashResult = Distinct | Same | Incomparable
+
+    clash : Term vars -> Term vars -> ClashResult
     clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
-        = t /= t'
+        = if t /= t' then Distinct else Same
     clash (Ref _ (TyCon t _) _) (Ref _ (TyCon t' _) _)
-        = t /= t'
-    clash (PrimVal _ c) (PrimVal _ c')
-      = c /= c'
-    clash (Ref _ t _) (PrimVal _ _) = isJust (isCon t)
-    clash (PrimVal _ _) (Ref _ t _) = isJust (isCon t)
-    clash (Ref _ t _) (TType _ _) = isJust (isCon t)
-    clash (TType _ _) (Ref _ t _) = isJust (isCon t)
-    clash (TType _ _) (PrimVal _ _) = True
-    clash (PrimVal _ _) (TType _ _) = True
-    clash _ _ = False
+        = if t /= t' then Distinct else Same
+    clash (PrimVal _ c) (PrimVal _ c') = if  c /= c' then Distinct else Same
+    clash (Ref _ t _) (PrimVal _ _) = if isJust (isCon t) then Distinct else Incomparable
+    clash (PrimVal _ _) (Ref _ t _) = if isJust (isCon t) then Distinct else Incomparable
+    clash (Ref _ t _) (TType _ _)   = if isJust (isCon t) then Distinct else Incomparable
+    clash (TType _ _) (Ref _ t _)   = if isJust (isCon t) then Distinct else Incomparable
+    clash (TType _ _) (PrimVal _ _) = Distinct
+    clash (PrimVal _ _) (TType _ _) = Distinct
+    clash _ _ = Incomparable
 
     findN : Nat -> Term vars -> Bool
     findN i (Local _ _ i' _) = i == i'
@@ -60,7 +61,10 @@ conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
     conflictTm tm tm'
         = let (f, args) = getFnArgs tm
               (f', args') = getFnArgs tm' in
-          clash f f' || any (uncurry conflictTm) (zip args args')
+          case clash f f' of
+            Distinct => True
+            Incomparable => False
+            Same => (any (uncurry conflictTm) (zip args args'))
 
     conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
     conflictArgs n tm [] = False
@@ -107,13 +111,12 @@ conflict defs env nfty n
       conflictNF i t (NBind fc x b sc)
           -- invent a fresh name, in case a user has bound the same name
           -- twice somehow both references appear in the result  it's unlikely
-          -- put posslbe
+          -- put possible
           = let x' = MN (show x) i in
                 conflictNF (i + 1) t
                        !(sc defs (toClosure defaultOpts [] (Ref fc Bound x')))
       conflictNF i nf (NApp _ (NRef Bound n) [])
-          = do empty <- clearDefs defs
-               pure (Just [(n, !(quote empty env nf))])
+          = pure (Just [(n, !(quote defs env nf))])
       conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
           = if t == t'
                then conflictArgs i (map snd args) (map snd args')
@@ -138,7 +141,8 @@ isEmpty defs env (NTCon fc n t a args)
   = do Just nty <- lookupDefExact n (gamma defs)
          | _ => pure False
        case nty of
-            TCon _ _ _ _ flags _ cons _
+            TCon _ _ _ _ flags _ Nothing _ => pure False
+            TCon _ _ _ _ flags _ (Just cons) _
                  => if not (external flags)
                        then allM (conflict defs env (NTCon fc n t a args)) cons
                        else pure False

src/Core/Termination/Positivity.idr

@@ -166,6 +166,7 @@ calcPositive loc n
          logC "totality.positivity" 6 $ do pure $ "Calculating positivity: " ++ show !(toFullNames n)
          case !(lookupDefTyExact n (gamma defs)) of
               Just (TCon _ _ _ _ _ tns dcons _, ty) =>
+                  let dcons = fromMaybe [] dcons in
                   case !(totRefsIn defs ty) of
                        IsTerminating =>
                             do log "totality.positivity" 30 $

src/Idris/Doc/String.idr

@@ -424,7 +424,7 @@ getDocsForName fc n config
            TCon _ _ _ _ _ _ cons _ =>
              do let tot = catMaybes [ showTotal (totality d)
                                     , pure (showVisible (collapseDefault $ visibility d))]
-                cdocs <- traverse (getDConDoc <=< toFullNames) cons
+                cdocs <- traverse (getDConDoc <=< toFullNames) (fromMaybe [] cons)
                 cdoc <- case cdocs of
                   [] => pure (Just "data", [])
                   [doc] =>

src/TTImp/Elab/App.idr

@@ -394,7 +394,7 @@ mutual
                 | Nothing => pure Nothing
                 let (TCon _ _ _ _ _ _ datacons _) = gdef.definition
                 | _ => pure Nothing
-                pure (Just (length datacons))
+                pure (length <$> datacons)
         else pure Nothing
       countConstructors _ = pure Nothing
 

src/TTImp/Elab/Record.idr

@@ -79,7 +79,7 @@ toRHS fc r = snd (toRHS' fc r)
 findConName : Defs -> Name -> Core (Maybe Name)
 findConName defs tyn
     = case !(lookupDefExact tyn (gamma defs)) of
-           Just (TCon _ _ _ _ _ _ [con] _) => pure (Just con)
+           Just (TCon _ _ _ _ _ _ (Just [con]) _) => pure (Just con)
            _ => pure Nothing
 
 findFieldsAndTypeArgs : {auto c : Ref Ctxt Defs} ->

src/TTImp/Elab/RunElab.idr

@@ -311,7 +311,7 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
              Just (TCon _ _ _ _ _ _ cons _) <-
                      lookupDefExact cn (gamma defs)
                  | _ => failWith defs $ show cn ++ " is not a type"
-             scriptRet cons
+             scriptRet $ fromMaybe [] cons
     elabCon defs "GetReferredFns" [n]
         = do dn <- reify defs !(evalClosure defs n)
              Just def <- lookupCtxtExact dn (gamma defs)

src/TTImp/Interactive/CaseSplit.idr

@@ -110,7 +110,7 @@ findCons n lhs
                                                ("Not a type constructor " ++
                                                   show res)))
                              pure (OK (fn, !(toFullNames tyn),
-                                           !(traverse toFullNames cons)))
+                                           !(traverse toFullNames $ fromMaybe [] cons)))
 
 findAllVars : Term vars -> List Name
 findAllVars (Bind _ x (PVar _ _ _ _) sc)

src/TTImp/Interactive/ExprSearch.idr

@@ -688,7 +688,7 @@ tryIntermediateRec fc rig opts hints env ty topty (Just rd)
         = isSingleCon defs !(sc defs (toClosure defaultOpts []
                                               (Erased fc Placeholder)))
     isSingleCon defs (NTCon _ n _ _ _)
-        = do Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n (gamma defs)
+        = do Just (TCon _ _ _ _ _ _ (Just [con]) _) <- lookupDefExact n (gamma defs)
                   | _ => pure False
              pure True
     isSingleCon _ _ = pure False

src/TTImp/Interactive/Intro.idr

@@ -50,7 +50,7 @@ parameters
     let TCon _ _ _ _ _ _ cs _ = definition gdef
       | _ => pure []
     let gty = gnf env ty
-    ics <- for cs $ \ cons => do
+    ics <- for (fromMaybe [] cs) $ \ cons => do
       Just gdef <- lookupCtxtExact cons (gamma defs)
         | _ => pure Nothing
       let nargs = lengthExplicitPi $ fst $ snd $ underPis (-1) [] (type gdef)

src/TTImp/ProcessBuiltin.idr

@@ -154,7 +154,7 @@ isNatural fc n = do
         | Nothing => undefinedName EmptyFC n
     let TCon _ _ _ _ _ _ cons _ = gdef.definition
         | _ => pure False
-    consDefs <- getConsGDef fc cons
+    consDefs <- getConsGDef fc (fromMaybe [] cons)
     pure $ all hasNatFlag consDefs
   where
     isNatFlag : DefFlag -> Bool
@@ -225,7 +225,7 @@ processBuiltinNatural fc name = do
     let TCon _ _ _ _ _ _ dcons _ = gdef.definition
         | def => throw $ GenericMsg fc
             $ "Expected a type constructor, found " ++ showDefType def ++ "."
-    cons <- getConsGDef fc dcons
+    cons <- getConsGDef fc (fromMaybe [] dcons)
     checkNatCons ds.gamma cons n fc
 
 ||| Check a `%builtin NaturalToInteger` pragma is correct.

src/TTImp/ProcessData.idr

@@ -426,7 +426,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)
 
          -- Add the type constructor as a placeholder
          tidx <- addDef n (newDef fc n linear vars fullty def_vis
-                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] Nothing Nothing))
          addMutData (Resolved tidx)
          defs <- get Ctxt
          traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)
@@ -499,7 +499,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
                       _ => pure $ mbtot <|> declTot
 
                     case definition ndef of
-                      TCon _ _ _ _ _ mw [] _ => case mfullty of
+                      TCon _ _ _ _ flags mw Nothing _ => case mfullty of
                         Nothing => pure (mw, vis, tot, type ndef)
                         Just fullty =>
                             do ok <- convert defs [] fullty (type ndef)
@@ -516,7 +516,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
          -- Add the type constructor as a placeholder while checking
          -- data constructors
          tidx <- addDef n (newDef fc n linear vars fullty (specified vis)
-                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] Nothing Nothing))
          case vis of
               Private => pure ()
               _ => do addHashWithNames n

src/TTImp/ProcessDef.idr

@@ -1118,7 +1118,9 @@ processDef opts nest env fc n_in cs_in
                               pure (Just rtm))
                (\err => do defs <- get Ctxt
                            if not !(recoverableErr defs err)
-                              then pure Nothing
+                              then do
+                                log "declare.def.impossible" 5 "impossible because \{show err}"
+                                pure Nothing
                               else pure (Just tm))
       where
         closeEnv : Defs -> NF [] -> Core ClosedTerm