cryptol 2.12.0 → 2.13.0

raw patch · 48 files changed

+844/−456 lines, 48 filesdep +arithmoidep +ghc-bignumdep ~basedep ~base-compatdep ~sbvnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: arithmoi, ghc-bignum

Dependency ranges changed: base, base-compat, sbv, what4

API changes (from Hackage documentation)

Files

• CHANGES.md +40/−1
• cryptol.cabal +14/−8
• cryptol/OptParser.hs +0/−1
• lib/Cryptol.cry +19/−37
• lib/Cryptol/Reference.cry +30/−0
• src/Cryptol/AES.hs +4/−2
• src/Cryptol/Backend/Concrete.hs +5/−6
• src/Cryptol/Backend/Monad.hs +2/−2
• src/Cryptol/Backend/SBV.hs +4/−3
• src/Cryptol/Backend/What4.hs +5/−4
• src/Cryptol/Eval.hs +3/−3
• src/Cryptol/Eval/Concrete.hs +2/−2
• src/Cryptol/Eval/Env.hs +1/−1
• src/Cryptol/Eval/Generic.hs +43/−2
• src/Cryptol/Eval/Reference.lhs +10/−8
• src/Cryptol/IR/FreeVars.hs +1/−1
• src/Cryptol/ModuleSystem/Base.hs +29/−26
• src/Cryptol/ModuleSystem/Env.hs +3/−3
• src/Cryptol/ModuleSystem/Interface.hs +1/−1
• src/Cryptol/ModuleSystem/Monad.hs +1/−1
• src/Cryptol/ModuleSystem/Name.hs +3/−2
• src/Cryptol/ModuleSystem/NamingEnv.hs +2/−0
• src/Cryptol/ModuleSystem/Renamer/Monad.hs +1/−1
• src/Cryptol/Parser/Layout.hs +4/−2
• src/Cryptol/Parser/NoInclude.hs +5/−3
• src/Cryptol/Parser/NoPat.hs +4/−2
• src/Cryptol/Parser/ParserUtils.hs +8/−5
• src/Cryptol/PrimeEC.hs +110/−166
• src/Cryptol/REPL/Command.hs +16/−5
• src/Cryptol/REPL/Monad.hs +3/−3
• src/Cryptol/Symbolic/SBV.hs +4/−1
• src/Cryptol/Transform/MonoValues.hs +5/−4
• src/Cryptol/Transform/Specialize.hs +3/−0
• src/Cryptol/TypeCheck/CheckModuleInstance.hs +2/−0
• src/Cryptol/TypeCheck/Error.hs +43/−32
• src/Cryptol/TypeCheck/Infer.hs +55/−43
• src/Cryptol/TypeCheck/Instantiate.hs +2/−1
• src/Cryptol/TypeCheck/Kind.hs +4/−1
• src/Cryptol/TypeCheck/Monad.hs +29/−19
• src/Cryptol/TypeCheck/Sanity.hs +2/−2
• src/Cryptol/TypeCheck/SimpType.hs +2/−0
• src/Cryptol/TypeCheck/SimpleSolver.hs +4/−1
• src/Cryptol/TypeCheck/Solver/Numeric.hs +1/−7
• src/Cryptol/TypeCheck/Solver/Selector.hs +8/−5
• src/Cryptol/TypeCheck/Type.hs +1/−0
• src/Cryptol/TypeCheck/TypePat.hs +24/−0
• src/Cryptol/TypeCheck/Unify.hs +127/−39
• src/GHC/Num/Compat.hs +155/−0

@@ -1,3 +1,42 @@+# 2.13.0++## Language changes++* Update the implementation of the Prelude function `sortBy` to use+  a merge sort instead of an insertion sort. This improves the both+  asymptotic and observed performance on sorting tasks.++## UI improvements++* "Type mismatch" errors now show a context giving more information+  about the location of the error.   The context is shown when the+  part of the types match, but then some nested types do not.+  For example, when mathching `{ a : [8], b : [8] }` with+  `{ a : [8], b : [16] }` the error will be `8` does not match `16`+  and the context will be `{ b : [ERROR] _ }` indicating that the+  error is in the length of the sequence of field `b`.++## Bug fixes++* The What4 backend now properly supports Boolector 3.2.2 or later.++* Make error message locations more precise in some cases (issue #1299).++* Make `:reload` behave as expected after loading a module with `:module`+  (issue #1313).++* Make `include` paths work as expected when nested within another `include`+  (issue #1321).++* Fix a panic that occurred when loading dependencies before `include`s are+  resolved (issue #1330).++* Closed issues #1098, #1280, and #1347.++* Merged pull requests #1233, #1300, #1301, #1302, #1303, #1305, #1306, #1307,+  #1308, #1311, #1312, #1317, #1319, #1323, #1326, #1331, #1333, #1336, #1337,+  #1338, #1342, #1346, #1348, and #1349.+ # 2.12.0  ## Language changes@@ -43,7 +82,7 @@   can be combined into a single line by separating them with `;`,   which is necessary for stating a signature together with a   definition, etc.-  + * There is a new `:set path` REPL option that provides an alternative to   `CRYPTOLPATH` for controlling where to search for imported modules   (issue #631).

@@ -1,6 +1,6 @@ Cabal-version:       2.4 Name:                cryptol-Version:             2.12.0+Version:             2.13.0 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD-3-Clause@@ -9,7 +9,7 @@ Maintainer:          cryptol@galois.com Homepage:            http://www.cryptol.net/ Bug-reports:         https://github.com/GaloisInc/cryptol/issues-Copyright:           2013-2020 Galois Inc.+Copyright:           2013-2021 Galois Inc. Category:            Language Build-type:          Simple extra-source-files:  bench/data/*.cry@@ -26,7 +26,7 @@   type:     git   location: https://github.com/GaloisInc/cryptol.git   -- add a tag on release branches-  tag:      2.12.0+  tag:      2.13.0   flag static@@ -40,9 +40,10 @@ library   Default-language:     Haskell2010-  Build-depends:       base              >= 4.8 && < 5,+  Build-depends:       base              >= 4.9 && < 5,+                       arithmoi          >= 0.12,                        async             >= 2.2 && < 2.3,-                       base-compat       >= 0.6 && < 0.12,+                       base-compat       >= 0.6 && < 0.13,                        bv-sized          >= 1.0 && < 1.1,                        bytestring        >= 0.10,                        array             >= 0.4,@@ -56,7 +57,6 @@                        ghc-prim,                        GraphSCC          >= 1.0.4,                        heredoc           >= 0.2,-                       integer-gmp       >= 1.0 && < 1.1,                        libBF             >= 0.6 && < 0.7,                        MemoTrie          >= 0.6 && < 0.7,                        monad-control     >= 1.0,@@ -64,7 +64,7 @@                        parameterized-utils >= 2.0.2,                        prettyprinter     >= 1.7.0,                        process           >= 1.2,-                       sbv               >= 8.6 && < 8.17,+                       sbv               >= 8.10 && < 9.1,                        simple-smt        >= 0.9.7,                        stm               >= 2.4,                        strict,@@ -74,8 +74,13 @@                        mtl               >= 2.2.1,                        time              >= 1.6.0.1,                        panic             >= 0.3,-                       what4             >= 1.2 && < 1.3+                       what4             >= 1.3 && < 1.4 +  if impl(ghc >= 9.0)+    build-depends:     ghc-bignum        >= 1.0 && < 1.3+  else+    build-depends:     integer-gmp       >= 1.0 && < 1.1+   Build-tool-depends:  alex:alex, happy:happy   hs-source-dirs:      src @@ -201,6 +206,7 @@   Other-modules:       Cryptol.Parser.LexerUtils,                        Cryptol.Parser.ParserUtils,                        Cryptol.Prelude,+                       GHC.Num.Compat,                        Paths_cryptol,                        GitRev 

@@ -9,7 +9,6 @@  module OptParser where -import Data.Monoid (Endo(..)) import Data.Semigroup  import Prelude ()

@@ -915,14 +915,9 @@  * given update pairs.  */ updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a-updates xs0 idxs vals = xss!0- where-   xss = [ xs0 ] #-         [ update xs i b-         | xs <- xss-         | i  <- idxs-         | b  <- vals-         ]+updates xs0 idxs vals = foldl upd xs0 (zip idxs vals)+  where+    upd xs (i,b) = update xs i b  /**  * Perform a series of updates to a sequence.  The first argument is@@ -932,14 +927,9 @@  * given update pairs.  */ updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a-updatesEnd xs0 idxs vals = xss!0- where-   xss = [ xs0 ] #-         [ updateEnd xs i b-         | xs  <- xss-         | i   <- idxs-         | b   <- vals-         ]+updatesEnd xs0 idxs vals = foldl upd xs0 (zip idxs vals)+  where+    upd xs (i,b) = updateEnd xs i b  /**  * Produce a sequence using a generating function.@@ -964,18 +954,16 @@  * pair of elements that are equivalent according to the order relation.  */ sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a-sortBy le vs =-  if `n == (0 : Integer) then vs-  else drop`{1 - min 1 n} (insertBy (vs@0) (sortBy le (drop`{min 1 n} vs)))+sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0   where-    insertBy : {k} (fin k) => a -> [k]a -> [k+1]a-    insertBy x0 ys = xys.0 # [last xs]-      where-        xs : [k+1]a-        xs = [x0] # xys.1-        xys : [k](a, a)-        xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]-+    xs' = if `(n/2)  == 1 then xs else sortBy le xs+    ys' = if `(n/^2) == 1 then ys else sortBy le ys+    zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)+             | j == `(n/^2)       then (xs'@i, i+1, j  )+             | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )+            else                       (ys'@j, i  , j+1)+          | (_, i, j) <- [ (undefined, 0, 0) ] # zs+          ]  // GF_2^n polynomial computations ------------------------------------------- @@ -1159,27 +1147,22 @@ sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a sum xs = foldl' (+) (fromInteger 0) xs - /**  * Compute the product of the values in the sequence.  */ product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a product xs = foldl' (*) (fromInteger 1) xs - /**  * Scan left is like a foldl that also emits the intermediate values.  */-scanl : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b-scanl f acc xs = ys-  where ys = [acc] # [f a x | a <- ys | x <- xs]+primitive scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a  /**  * Scan right is like a foldr that also emits the intermediate values.  */-scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b-scanr f acc xs = reverse ys-  where ys = [acc] # [f x a | a <- ys | x <- reverse xs]+scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1+n]b+scanr f acc xs = reverse (scanl (\a b -> f b a) acc (reverse xs))  /**  * Repeat a value.@@ -1222,5 +1205,4 @@  * list of successive function applications.  */ iterate : {a} (a -> a) -> a -> [inf]a-iterate f x = xs-  where xs = [x] # [ f v | v <- xs ]+iterate f z = scanl (\x _ -> f x) z (zero:[inf]())

@@ -44,3 +44,33 @@     powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]      zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]++/**+ * Functional left fold.+ *+ * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3+ *+ * Reference implementation.+ */+foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a+foldl f z bs = last (scanl f z bs)++/**+ * Scan left is like a foldl that also emits the intermediate values.+ *+ * Reference implementation.+ */+scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a+scanl f z bs = as+  where+    as = [z] # [ f a b | a <- as | b <- bs ]++/**+ * Map a function iteratively over a seed value, producing an infinite+ * list of successive function applications.+ *+ * Reference implementation.+ */+iterate : {a} (a -> a) -> a -> [inf]a+iterate f z = xs+  where xs = [z] # [ f x | x <- xs ]

@@ -294,8 +294,10 @@           subWordRcon :: Word32 -> GF28 -> Word32          subWordRcon w rc = fromBytes [a `xor` rc, b, c, d]-            where [a, b, c, d] = map sbox $ toBytes w-+            where (a, b, c, d) =+                    case map sbox $ toBytes w of+                      [a', b', c', d'] -> (a', b', c', d')+                      bs -> error $ "Unexpected list length in keyExpansionWords: " ++ show (length bs)  -- | Definition of round-constants, as specified in Section 5.2 of the AES standard. --   We only need up to the 11th value for AES-128, and fewer than that for AES-192

@@ -40,7 +40,7 @@ import Data.Ratio import Numeric (showIntAtBase) import qualified LibBF as FP-import qualified GHC.Integer.GMP.Internals as Integer+import qualified GHC.Num.Compat as Integer  import qualified Cryptol.Backend.Arch as Arch import qualified Cryptol.Backend.FloatHelpers as FP@@ -340,11 +340,10 @@   -- NB: under the precondition that `m` is prime,   -- the only values for which no inverse exists are   -- congruent to 0 modulo m.-  znRecip sym m x-    | r == 0    = raiseError sym DivideByZero-    | otherwise = pure r-   where-     r = Integer.recipModInteger x m+  znRecip sym m x =+    case Integer.integerRecipMod x m of+      Just r  -> integerLit sym r+      Nothing -> raiseError sym DivideByZero    znPlus  _ = liftBinIntMod (+)   znMinus _ = liftBinIntMod (-)

@@ -383,13 +383,13 @@   {-# INLINE fmap #-}  instance Applicative Eval where-  pure  = return+  pure  = Ready   (<*>) = ap   {-# INLINE pure #-}   {-# INLINE (<*>) #-}  instance Monad Eval where-  return = Ready+  return = pure   (>>=)  = evalBind   {-# INLINE return #-}   {-# INLINE (>>=) #-}

@@ -38,7 +38,7 @@ import           Data.Bits (bit, complement) import           Data.List (foldl') -import qualified GHC.Integer.GMP.Internals as Integer+import qualified GHC.Num.Compat as Integer  import Data.SBV.Dynamic as SBV import qualified Data.SBV.Internals as SBV@@ -429,8 +429,9 @@ sModRecip sym m x   -- If the input is concrete, evaluate the answer   | Just xi <- svAsInteger x-  = let r = Integer.recipModInteger xi m-     in if r == 0 then raiseError sym DivideByZero else integerLit sym r+  = case Integer.integerRecipMod xi m of+      Just r  -> integerLit sym r+      Nothing -> raiseError sym DivideByZero    -- If the input is symbolic, create a new symbolic constant   -- and assert that it is the desired multiplicitive inverse.

@@ -28,7 +28,7 @@ import           Data.Parameterized.NatRepr import           Data.Parameterized.Some -import qualified GHC.Integer.GMP.Internals as Integer+import qualified GHC.Num.Compat as Integer  import qualified What4.Interface as W4 import qualified What4.SWord as SW@@ -341,7 +341,7 @@   wordMult   sym x y = liftIO (SW.bvMul (w4 sym) x y)   wordNegate sym x   = liftIO (SW.bvNeg (w4 sym) x)   wordLg2    sym x   = sLg2 (w4 sym) x- +   wordShiftLeft   sym x y = w4bvShl (w4 sym) x y   wordShiftRight  sym x y = w4bvLshr (w4 sym) x y   wordRotateLeft  sym x y = w4bvRol (w4 sym) x y@@ -668,8 +668,9 @@ sModRecip sym m x   -- If the input is concrete, evaluate the answer   | Just xi <- W4.asInteger x-  = let r = Integer.recipModInteger xi m-     in if r == 0 then raiseError sym DivideByZero else integerLit sym r+  = case Integer.integerRecipMod xi m of+      Just r  -> integerLit sym r+      Nothing -> raiseError sym DivideByZero    -- If the input is symbolic, create a new symbolic constant   -- and assert that it is the desired multiplicitive inverse.

@@ -550,7 +550,7 @@     , leTypes  = mempty     } -  mappend l r = l <> r+  mappend = (<>)  toListEnv :: GenEvalEnv sym -> ListEnv sym toListEnv e =@@ -566,7 +566,7 @@ --   locations. evalListEnv :: ListEnv sym -> Integer -> GenEvalEnv sym evalListEnv (ListEnv vm st tm) i =-    let v = fmap (Right . ($i)) vm+    let v = fmap (Right . ($ i)) vm      in EvalEnv{ envVars = IntMap.union v st                , envTypes = tm                }@@ -664,7 +664,7 @@       -- `leVars` elements of the comprehension environment into `leStatic` elements       -- by selecting out the 0th element.       Inf -> do-        let allvars = IntMap.union (fmap (Right . ($0)) (leVars lenv)) (leStatic lenv)+        let allvars = IntMap.union (fmap (Right . ($ 0)) (leVars lenv)) (leStatic lenv)         let lenv' = lenv { leVars   = IntMap.empty                          , leStatic = allvars                          }

@@ -250,9 +250,9 @@   ]  toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint-toProjectivePoint v = PrimeEC.ProjectivePoint <$> f "x" <*> f "y" <*> f "z"+toProjectivePoint v = PrimeEC.toProjectivePoint <$> f "x" <*> f "y" <*> f "z"   where-   f nm = PrimeEC.integerToBigNat . fromVInteger <$> lookupRecord nm v+   f nm = fromVInteger <$> lookupRecord nm v  fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value fromProjectivePoint (PrimeEC.ProjectivePoint x y z) =

@@ -48,7 +48,7 @@     { envVars       = IntMap.empty     , envTypes      = mempty     }-  mappend l r = l <> r+  mappend = (<>)  ppEnv :: Backend sym => sym -> PPOpts -> GenEvalEnv sym -> SEval sym Doc ppEnv sym opts env = brackets . fsep <$> mapM bind (IntMap.toList (envVars env))

@@ -21,6 +21,8 @@ {-# LANGUAGE BangPatterns #-}  {-# OPTIONS_GHC -fno-warn-orphans #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.Eval.Generic where  import qualified Control.Exception as X@@ -35,7 +37,7 @@ import Data.Ratio ((%))  import Cryptol.TypeCheck.AST-import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul)+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd) import Cryptol.Backend import Cryptol.Backend.Concrete (Concrete(..)) import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )@@ -1814,6 +1816,40 @@        go1 f a' bs  +-- scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a+scanlV :: forall sym. Backend sym => sym -> Prim sym+scanlV sym =+  PNumPoly \n ->+  PTyPoly  \a ->+  PTyPoly  \_b ->+  PFun     \f ->+  PFun     \z ->+  PStrict  \v ->+  PPrim+    do sm <- case v of+            VSeq _ m   -> scan n f z m+            VWord _ wv -> scan n f z (VBit <$> asBitsMap sym wv)+            VStream m  -> scan n f z m+            _ -> panic "Cryptol.Eval.Generic.scanlV" ["Expected sequence"]+       mkSeq sym (nAdd (Nat 1) n) a sm++ where+  scan :: Nat' ->+          SEval sym (GenValue sym) ->+          SEval sym (GenValue sym) ->+          (SeqMap sym (GenValue sym)) ->+          SEval sym (SeqMap sym (GenValue sym))+  scan n f z m =+    do (result, fill) <- sDeclareHole sym "scanl"+       fill $ memoMap sym (nAdd (Nat 1) n) $ indexSeqMap $ \i ->+         if i == 0 then z+         else+           do r <- result+              f'  <- fromVFun sym <$> f+              f'' <- fromVFun sym <$> f' (lookupSeqMap r (i-1))+              f'' (lookupSeqMap m (i-1))+       result+ -- Random Values ---------------------------------------------------------------  {-# SPECIALIZE randomV ::@@ -1830,7 +1866,9 @@       -- unpack the seed into four Word64s       let mask64 = 0xFFFFFFFFFFFFFFFF           unpack s = fromInteger (s .&. mask64) : unpack (s `shiftR` 64)-          [a, b, c, d] = take 4 (unpack seed)+          (a, b, c, d) = case take 4 (unpack seed) of+                           [a', b', c', d'] -> (a', b', c', d')+                           _ -> error "randomV: impossible (infinite seed is finite)"       in fst $ gen 100 $ seedTFGen (a, b, c, d)  --------------------------------------------------------------------------------@@ -2199,6 +2237,9 @@    , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}                     foldl'V sym)++  , ("scanl"      , {-# SCC "Prelude::scanl" #-}+                    scanlV sym)    , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}                     PTyPoly \_a ->

@@ -31,7 +31,7 @@ > import qualified Data.Text as T (pack) > import LibBF (BigFloat) > import qualified LibBF as FP-> import qualified GHC.Integer.GMP.Internals as Integer+> import qualified GHC.Num.Compat as Integer > > import Cryptol.ModuleSystem.Name (asPrim) > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)@@ -259,7 +259,7 @@ >     { envVars  = mempty >     , envTypes = mempty >     }->   mappend l r = l <> r+>   mappend = (<>) > > -- | Bind a variable in the evaluation environment. > bindVar :: (Name, E Value) -> Env -> Env@@ -1331,8 +1331,10 @@ > ratRecip x = pure (recip x) > > zRecip :: Integer -> Integer -> E Integer-> zRecip m x = if r == 0 then cryError DivideByZero else pure r->    where r = Integer.recipModInteger x m+> zRecip m x =+>   case Integer.integerRecipMod x m of+>     Just r  -> pure r+>     Nothing -> cryError DivideByZero > > zDiv :: Integer -> Integer -> Integer -> E Integer > zDiv m x y = f <$> zRecip m y@@ -1554,17 +1556,17 @@ > > signedShiftRV :: Value > signedShiftRV =->   VNumPoly $ \(Nat n) -> pure $+>   VNumPoly $ \n -> pure $ >   VPoly $ \ix -> pure $ >   VFun $ \v -> pure $ >   VFun $ \x -> >   do amt <- cryToInteger ix x->      pure $ generateV (Nat n) $ \i ->+>      pure $ generateV n $ \i -> >        do vs <- fromVList <$> v >           if i < amt then->             indexFront (Nat n) vs 0+>             indexFront n vs 0 >           else->             indexFront (Nat n) vs (i - amt)+>             indexFront n vs (i - amt)  Indexing --------

@@ -32,7 +32,7 @@                 , tyParams  = Set.empty                 } -  mappend d1 d2 = d1 <> d2+  mappend = (<>)    mconcat ds = Deps { valDeps   = Set.unions (map valDeps ds)                     , tyDeps    = Set.unions (map tyDeps  ds)

@@ -117,6 +117,7 @@  -- Parsing --------------------------------------------------------------------- +-- | Parse a module and expand includes parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName) parseModule path = do   getBytes <- getByteReader@@ -149,8 +150,26 @@               }    case P.parseModule cfg txt of-    Right pm -> let fp = fingerprint bytes-                in fp `seq` return (fp, pm)+    Right pm ->+      do let fp = fingerprint bytes+         pm1 <- case path of+                  InFile p ->+                    do r <- getByteReader+                       mb <- io (removeIncludesModule r p pm)+                       case mb of+                         Right ok -> pure ok+                         Left err -> noIncludeErrors err++                  {- We don't do "include" resolution for in-memory files+                     because at the moment the include resolution pass requires+                     the path to the file to be known---this is used when+                     looking for other inlcude files.  This could be+                     generalized, but we can do it once we have a concrete use+                     case as it would help guide the design. -}+                  InMem {} -> pure pm++         fp `seq` return (fp, pm1)+     Left err -> moduleParseError path err  @@ -210,7 +229,7 @@        ("Loading module " ++ pretty (P.thing (P.mName pm)))  -     (nameEnv,tcmod) <- checkModule isrc path pm+     (nameEnv,tcmod) <- checkModule isrc pm      tcm <- optionalInstantiate tcmod       -- extend the eval env, unless a functor.@@ -387,19 +406,17 @@                   [ "Unable to find the prelude" ]  -- | Load a module, be it a normal module or a functor instantiation.-checkModule ::-  ImportSource -> ModulePath -> P.Module PName ->-  ModuleM (R.NamingEnv, T.Module)-checkModule isrc path m =+checkModule :: ImportSource -> P.Module PName -> ModuleM (R.NamingEnv, T.Module)+checkModule isrc m =   case P.mInstance m of-    Nothing -> checkSingleModule T.tcModule isrc path m+    Nothing -> checkSingleModule T.tcModule isrc m     Just fmName ->       do mbtf <- getLoadedMaybe (thing fmName)          case mbtf of            Just tf ->              do renThis <- io $ newIORef (lmNamingEnv tf)                 let how = T.tcModuleInst renThis (lmModule tf)-                (_,m') <- checkSingleModule how isrc path m+                (_,m') <- checkSingleModule how isrc m                 newEnv <- io $ readIORef renThis                 pure (newEnv,m')            Nothing -> panic "checkModule"@@ -409,35 +426,21 @@ -- | Typecheck a single module.  If the module is an instantiation -- of a functor, then this just type-checks the instantiating parameters. -- See 'checkModule'+-- Note: we assume that @include@s have already been processed checkSingleModule ::   Act (P.Module Name) T.Module {- ^ how to check -} ->   ImportSource                 {- ^ why are we loading this -} ->-  ModulePath                   {- path -} ->   P.Module PName               {- ^ module to check -} ->   ModuleM (R.NamingEnv,T.Module)-checkSingleModule how isrc path m = do+checkSingleModule how isrc m = do    -- check that the name of the module matches expectations   let nm = importedModule isrc   unless (notParamInstModName nm == thing (P.mName m))          (moduleNameMismatch nm (mName m)) -  -- remove includes first; we only do this for actual files.-  -- it is less clear what should happen for in-memory things, and since-  -- this is a more-or-less obsolete feature, we are just not doing-  -- ot for now.-  e   <- case path of-           InFile p -> do-             r <- getByteReader-             io (removeIncludesModule r p m)-           InMem {} -> pure (Right m)--  nim <- case e of-           Right nim  -> return nim-           Left ierrs -> noIncludeErrors ierrs-   -- remove pattern bindings-  npm <- noPat nim+  npm <- noPat m    -- rename everything   renMod <- renameModule npm

@@ -260,8 +260,8 @@                  Just c -> dynModContext me <> c                  Nothing -> panic "focusedEnv"                               [ "Focused modules not loaded: " ++ show (pp fm) ]-   + -- Loaded Modules --------------------------------------------------------------  -- | The location of a module@@ -318,7 +318,7 @@   mempty = LoadedModules { lmLoadedModules = []                          , lmLoadedParamModules = []                          }-  mappend l r = l <> r+  mappend = (<>)  data LoadedModule = LoadedModule   { lmName              :: ModName@@ -419,7 +419,7 @@     , deTySyns = mempty     , deEnv    = mempty     }-  mappend de1 de2 = de1 <> de2+  mappend = (<>)  -- | Build 'IfaceDecls' that correspond to all of the bindings in the -- dynamic environment.

@@ -146,7 +146,7 @@  instance Monoid IfaceDecls where   mempty      = IfaceDecls Map.empty Map.empty Map.empty Map.empty Map.empty-  mappend l r = l <> r+  mappend     = (<>)   mconcat ds  = IfaceDecls     { ifTySyns   = Map.unions (map ifTySyns   ds)     , ifNewtypes = Map.unions (map ifNewtypes ds)

@@ -339,7 +339,7 @@  instance Monad m => Monad (ModuleT m) where   {-# INLINE return #-}-  return x      = ModuleT (return x)+  return        = pure    {-# INLINE (>>=) #-}   m >>= f       = ModuleT (unModuleT m >>= unModuleT . f)

@@ -10,6 +10,7 @@  {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -183,12 +184,12 @@ instance PPName Name where   ppNameFixity n = nameFixity n -  ppInfixName n @ Name { .. }+  ppInfixName n@Name { .. }     | isInfixIdent nIdent = ppName n     | otherwise           = panic "Name" [ "Non-infix name used infix"                                          , show nIdent ] -  ppPrefixName n @ Name { .. } = optParens (isInfixIdent nIdent) (ppName n)+  ppPrefixName n@Name { .. } = optParens (isInfixIdent nIdent) (ppName n)   -- | Pretty-print a name with its source location information.

@@ -17,6 +17,8 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE OverloadedStrings #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.ModuleSystem.NamingEnv where  import Data.List (nub)

@@ -104,7 +104,7 @@  instance Monad RenameM where   {-# INLINE return #-}-  return x      = RenameM (return x)+  return        = pure    {-# INLINE (>>=) #-}   m >>= k       = RenameM (unRenameM m >>= unRenameM . k)

@@ -36,7 +36,7 @@      - The implicit layout block is ended by:           * a token than is less indented that the block, or-          * `)`, `}`, `]`, or +          * `)`, `}`, `]`, or           * ',' but only if there is an outer paren block           block's column.     - When an implicit layout block ends, we insert a "virtual end block"@@ -141,7 +141,9 @@       curTok : go stack lastVirt False advanceTokens      where-    curTok : advanceTokens = tokens+    (curTok, advanceTokens) = case tokens of+                                (curTok' : advanceTokens') -> (curTok', advanceTokens')+                                [] -> error "layout: Unexpected empty list of tokens"     curTokTy               = tokenType (thing curTok)     curRange               = srcRange curTok     curLoc                 = from curRange

@@ -116,11 +116,11 @@   fmap = liftM  instance A.Applicative NoIncM where-  pure = return+  pure x = M (pure x)   (<*>) = ap  instance Monad NoIncM where-  return x = M (return x)+  return   = pure   m >>= f  = M (unM m >>= unM . f)  instance Fail.MonadFail NoIncM where@@ -196,7 +196,9 @@   case parseProgramWith (defaultConfig { cfgSource = thing lf, cfgPreProc = guessPreProc (thing lf) }) source of      Right prog -> do-      Program ds <- withIncPath (thing lf) (noIncludeProgram prog)+      Program ds <-+        do path <- fromIncPath (thing lf)+           withIncPath path (noIncludeProgram prog)       return ds      Left err -> M (raise [IncludeParseError err])

@@ -565,9 +565,11 @@               deriving (Show,Generic, NFData)  instance Functor NoPatM where fmap = liftM-instance Applicative NoPatM where pure = return; (<*>) = ap+instance Applicative NoPatM where+  pure x = M (pure x)+  (<*>) = ap instance Monad NoPatM where-  return x  = M (return x)+  return    = pure   M x >>= k = M (x >>= unM . k)  -- | Pick a new name, to be used when desugaring patterns.

@@ -13,6 +13,8 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE OverloadedStrings #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.Parser.ParserUtils where  import Data.Maybe(fromMaybe)@@ -151,11 +153,11 @@   fmap = liftM  instance Applicative ParseM where-  pure  = return+  pure a = P (\_ _ s -> Right (a,s))   (<*>) = ap  instance Monad ParseM where-  return a  = P (\_ _ s -> Right (a,s))+  return    = pure   m >>= k   = P (\cfg p s1 -> case unP m cfg p s1 of                             Left e       -> Left e                             Right (a,s2) -> unP (k a) cfg p s2)@@ -382,7 +384,7 @@ eFromToBy r e1 e2 e3 isStrictBound =   case (asETyped e1, asETyped e2, asETyped e3) of     (Just (e1', t), Nothing, Nothing) -> eFromToByTyped r e1' e2 e3 (Just t) isStrictBound-    (Nothing, Just (e2', t), Nothing) -> eFromToByTyped r e1 e2' e3 (Just t) isStrictBound   +    (Nothing, Just (e2', t), Nothing) -> eFromToByTyped r e1 e2' e3 (Just t) isStrictBound     (Nothing, Nothing, Just (e3', t)) -> eFromToByTyped r e1 e2 e3' (Just t) isStrictBound     (Nothing, Nothing, Nothing)       -> eFromToByTyped r e1 e2 e3 Nothing isStrictBound     _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."]@@ -400,7 +402,7 @@ eFromToDownBy r e1 e2 e3 isStrictBound =   case (asETyped e1, asETyped e2, asETyped e3) of     (Just (e1', t), Nothing, Nothing) -> eFromToDownByTyped r e1' e2 e3 (Just t) isStrictBound-    (Nothing, Just (e2', t), Nothing) -> eFromToDownByTyped r e1 e2' e3 (Just t) isStrictBound   +    (Nothing, Just (e2', t), Nothing) -> eFromToDownByTyped r e1 e2' e3 (Just t) isStrictBound     (Nothing, Nothing, Just (e3', t)) -> eFromToDownByTyped r e1 e2 e3' (Just t) isStrictBound     (Nothing, Nothing, Nothing)       -> eFromToDownByTyped r e1 e2 e3 Nothing isStrictBound     _ -> errorMessage r ["A sequence enumeration may have at most one element type annotation."]@@ -575,7 +577,8 @@  -- NOTE: The list of patterns is reversed! mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName-mkProperty f ps e = DBind Bind { bName       = f+mkProperty f ps e = at (f,e) $+                    DBind Bind { bName       = f                                , bParams     = reverse ps                                , bDef        = at e (Located emptyRange (DExpr e))                                , bSignature  = Nothing

@@ -18,16 +18,27 @@ -- in order to speed up the basic modular arithmetic operations. ----------------------------------------------------------------------------- {-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE UnboxedTuples #-} +#if __GLASGOW_HASKELL__ >= 900+-- On GHC 9.0 or later—that is, when building with ghc-bignum—BigNum# is an+-- unlifted type, so we need UnliftedNewtypes to declare a newtype on top of+-- it. On older versions of GHC, BigNat# is simply a synonym for BigNat. BigNat+-- is lifted, so declaring a newtype on top of it works out of the box.+{-# LANGUAGE UnliftedNewtypes #-}+#endif+ module Cryptol.PrimeEC   ( PrimeModulus   , primeModulus   , ProjectivePoint(..)-  , integerToBigNat-  , Integer.bigNatToInteger+  , toProjectivePoint+  , BN.integerToBigNat+  , BN.bigNatToInteger    , ec_double   , ec_add_nonzero@@ -36,10 +47,9 @@   ) where  -import           GHC.Integer.GMP.Internals (BigNat)-import qualified GHC.Integer.GMP.Internals as Integer-import           GHC.Prim-import           Data.Bits+import           GHC.Num.Compat (BigNat#)+import qualified GHC.Num.Compat as BN+import           GHC.Exts  import Cryptol.TypeCheck.Solver.InfNat (widthInteger) import Cryptol.Utils.Panic@@ -48,173 +58,103 @@ --   homogenous coordinates. data ProjectivePoint =   ProjectivePoint-  { px :: !BigNat-  , py :: !BigNat-  , pz :: !BigNat+  { px :: !BigNat#+  , py :: !BigNat#+  , pz :: !BigNat#   } ++toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint+toProjectivePoint x y z =+  ProjectivePoint (BN.integerToBigNat x) (BN.integerToBigNat y) (BN.integerToBigNat z)+ -- | The projective "point at infinity", which represents the zero element --   of the ECC group. zro :: ProjectivePoint-zro = ProjectivePoint Integer.oneBigNat Integer.oneBigNat Integer.zeroBigNat---- | Coerce an integer value to a @BigNat@.  This operation only really makes---   sense for nonnegative values, but this condition is not checked.-integerToBigNat :: Integer -> BigNat-integerToBigNat (Integer.S# i)  = Integer.wordToBigNat (int2Word# i)-integerToBigNat (Integer.Jp# b) = b-integerToBigNat (Integer.Jn# b) = b+zro = ProjectivePoint (BN.oneBigNat (# #)) (BN.oneBigNat (# #)) (BN.zeroBigNat (# #))  -- | Simple newtype wrapping the @BigNat@ value of the --   modulus of the underlying field Z p.  This modulus --   is required to be prime.-newtype PrimeModulus = PrimeModulus { primeMod :: BigNat }+newtype PrimeModulus = PrimeModulus { primeMod :: BigNat# }   -- | Inject an integer value into the @PrimeModulus@ type. --   This modulus is required to be prime. primeModulus :: Integer -> PrimeModulus-primeModulus = PrimeModulus . integerToBigNat+primeModulus x = PrimeModulus (BN.integerToBigNat x) {-# INLINE primeModulus #-}  --- Barrett reduction replaces a division by the modulus with--- two multiplications and some shifting, masking, and additions--- (and some fairly negligible pre-processing). For the size of--- moduli we are working with for ECC, this does not appear to be--- a performance win.  Even for largest NIST curve (P-521) Barrett--- reduction is about 20% slower than naive modular reduction.--- Smaller curves are worse WRT the baseline.---- {-# INLINE primeModulus #-}--- primeModulus :: Integer -> PrimeModulus--- primeModulus = untrie modulusParameters---- data PrimeModulus = PrimeModulus---   { primeMod :: !Integer---   , barrettInverse :: !Integer---   , barrettK       :: !Int---   , barrettMask    :: !Integer---   }---  deriving (Show, Eq)---- {-# NOINLINE modulusParameters #-}--- modulusParameters :: Integer :->: PrimeModulus--- modulusParameters = trie computeModulusParameters---- computeModulusParameters :: Integer -> PrimeModulus--- computeModulusParameters p = PrimeModulus p inv k mask---   where---   k = fromInteger w----   b :: Integer---   b = 2 ^ (64::Int)----   -- w is the number of 64-bit words required to express p---   w = (widthInteger p + 63) `div` 64----   mask = b^(k+1) - 1----   -- inv = floor ( b^(2*k) / p )---   inv = b^(2*k) `div` p---- barrettReduction :: PrimeModulus -> Integer -> Integer--- barrettReduction p x = go r3---   where---     m    = primeMod p---     k    = barrettK p---     inv  = barrettInverse p---     mask = barrettMask p----     -- q1 <- floor (x / b^(k-1))---     q1 = x `shiftR` (64 * (k-1))----     -- q2 <- q1 * floor ( b^(2*k) / m )---     q2 = q1 * inv----     -- q3 <- floor (q2 / b^(k+1))---     q3 = q2 `shiftR` (64 * (k+1))----     -- r1 <- x mod b^(k+1)---     r1 = x .&. mask----     -- r2 <- (q3 * m) mod b^(k+1)---     r2 = (q3 * m) .&. mask----     -- r3 <- r1 - r2---     r3 = r1 - r2----     -- up to 2 multiples of m must be removed---     go z = if z > m then go (z - m) else z- -- | Modular addition of two values.  The inputs are --   required to be in reduced form, and will output --   a value in reduced form.-mod_add :: PrimeModulus -> BigNat -> BigNat -> BigNat-mod_add p !x !y =-    case Integer.isNullBigNat# rmp of-      0# -> rmp-      _  -> r-  where r = Integer.plusBigNat x y-        rmp = Integer.minusBigNat r (primeMod p)+mod_add :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#+mod_add p x y =+  let r = BN.bigNatAdd x y in+  case BN.bigNatSub r (primeMod p) of+    (# (# #) | #) -> r+    (# | rmp #)   -> rmp  -- | Compute the "half" value of a modular integer.  For a given input @x@ --   this is a value @y@ such that @y+y == x@.  Such values must exist --   in @Z p@ when @p > 2@.  The input @x@ is required to be in reduced form, --   and will output a value in reduced form.-mod_half :: PrimeModulus -> BigNat -> BigNat-mod_half p !x = if Integer.testBitBigNat x 0# then qodd else qeven+mod_half :: PrimeModulus -> BigNat# -> BigNat#+mod_half p x = if BN.testBitBigNat x 0# then qodd else qeven   where-  qodd  = (Integer.plusBigNat x (primeMod p)) `Integer.shiftRBigNat` 1#-  qeven = x `Integer.shiftRBigNat` 1#+  qodd  = (BN.bigNatAdd x (primeMod p)) `BN.shiftRBigNat` 1#+  qeven = x `BN.shiftRBigNat` 1#  -- | Compute the modular multiplication of two input values.  Currently, this --   uses naive modular reduction, and does not require the inputs to be in --   reduced form.  The output is in reduced form.-mod_mul :: PrimeModulus -> BigNat -> BigNat -> BigNat-mod_mul p !x !y = (Integer.timesBigNat x y) `Integer.remBigNat` (primeMod p)+mod_mul :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#+mod_mul p x y = (BN.bigNatMul x y) `BN.bigNatRem` (primeMod p)  -- | Compute the modular difference of two input values.  The inputs are --   required to be in reduced form, and will output a value in reduced form.-mod_sub :: PrimeModulus -> BigNat -> BigNat -> BigNat-mod_sub p !x !y = mod_add p x (Integer.minusBigNat (primeMod p) y)+mod_sub :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#+mod_sub p x y =+  case BN.bigNatSub (primeMod p) y of+    (# | y' #) -> mod_add p x y'+    (# (# #) | #) -> x -- BOGUS!  -- | Compute the modular square of an input value @x@; that is, @x*x@. --   The input is not required to be in reduced form, and the output --   will be in reduced form.-mod_square :: PrimeModulus -> BigNat -> BigNat-mod_square p !x = Integer.sqrBigNat x `Integer.remBigNat` primeMod p+mod_square :: PrimeModulus -> BigNat# -> BigNat#+mod_square p x = BN.bigNatSqr x `BN.bigNatRem` primeMod p  -- | Compute the modular scalar multiplication @2x = x+x@. --   The input is required to be in reduced form and the output --   will be in reduced form.-mul2 :: PrimeModulus -> BigNat -> BigNat-mul2 p !x =-    case Integer.isNullBigNat# rmp of-      0# -> rmp-      _  -> r- where-   r = x `Integer.shiftLBigNat` 1#-   rmp = Integer.minusBigNat r (primeMod p)+mul2 :: PrimeModulus -> BigNat# -> BigNat#+mul2 p x =+  let r = x `BN.shiftLBigNat` 1# in+  case BN.bigNatSub r (primeMod p) of+    (# (# #) | #) -> r+    (# | rmp #)   -> rmp  -- | Compute the modular scalar multiplication @3x = x+x+x@. --   The input is required to be in reduced form and the output --   will be in reduced form.-mul3 :: PrimeModulus -> BigNat -> BigNat-mul3 p x = mod_add p x $! mul2 p x+mul3 :: PrimeModulus -> BigNat# -> BigNat#+mul3 p x = mod_add p x (mul2 p x)  -- | Compute the modular scalar multiplication @4x = x+x+x+x@. --   The input is required to be in reduced form and the output --   will be in reduced form.-mul4 :: PrimeModulus -> BigNat -> BigNat-mul4 p x = mul2 p $! mul2 p x+mul4 :: PrimeModulus -> BigNat# -> BigNat#+mul4 p x = mul2 p (mul2 p x)  -- | Compute the modular scalar multiplication @8x = x+x+x+x+x+x+x+x@. --   The input is required to be in reduced form and the output --   will be in reduced form.-mul8 :: PrimeModulus -> BigNat -> BigNat-mul8 p x = mul2 p $! mul4 p x+mul8 :: PrimeModulus -> BigNat# -> BigNat#+mul8 p x = mul2 p (mul4 p x) + -- | Compute the elliptic curve group doubling operation. --   In other words, if @S@ is a projective point on a curve, --   this operation computes @S+S@ in the ECC group.@@ -225,7 +165,7 @@ --   reflected across the x axis. ec_double :: PrimeModulus -> ProjectivePoint -> ProjectivePoint ec_double p (ProjectivePoint sx sy sz) =-    if Integer.isZeroBigNat sz then zro else ProjectivePoint r18 r23 r13+    if BN.bigNatIsZero sz then zro else ProjectivePoint r18 r23 r13    where   r7  = mod_square p sz                   {-  7: t4 <- (t3)^2  -}@@ -250,22 +190,25 @@ --   case for adding points which might be the identity. ec_add :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_add p s t-  | Integer.isZeroBigNat (pz s) = t-  | Integer.isZeroBigNat (pz t) = s+  | BN.bigNatIsZero (pz s) = t+  | BN.bigNatIsZero (pz t) = s   | otherwise = ec_add_nonzero p s t {-# INLINE ec_add #-}  + -- | Compute the elliptic curve group subtraction operation, including the special --   cases for subtracting points which might be the identity. ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_sub p s t = ec_add p s u-  where u = t{ py = Integer.minusBigNat (primeMod p) (py t) }+  where u = case BN.bigNatSub (primeMod p) (py t) of+              (# | y' #)    -> t{ py = y' }+              (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))] {-# INLINE ec_sub #-}   ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint-ec_negate p s = s{ py = Integer.minusBigNat (primeMod p) (py s) }+ec_negate p s = s{ py = BN.bigNatSubUnsafe (primeMod p) (py s) } {-# INLINE ec_negate #-}  -- | Compute the elliptic curve group addition operation@@ -280,8 +223,8 @@ --   which instead computes a tangent line to @S@ . ec_add_nonzero :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) =-    if Integer.isZeroBigNat r13 then-      if Integer.isZeroBigNat r14 then+    if BN.bigNatIsZero r13 then+      if BN.bigNatIsZero r14 then         ec_double p s       else         zro@@ -289,7 +232,7 @@       ProjectivePoint r32 r37 r27    where-  tNormalized = Integer.eqBigNat tz Integer.oneBigNat+  tNormalized = BN.bigNatIsOne tz    tz2 = mod_square p tz   tz3 = mod_mul p tz tz2@@ -328,17 +271,17 @@ --   be added many times. ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint ec_normalize p s@(ProjectivePoint x y z)-  | Integer.eqBigNat z Integer.oneBigNat = s-  | otherwise = ProjectivePoint x' y' Integer.oneBigNat+  | BN.bigNatIsOne z = s+  | otherwise = ProjectivePoint x' y' (BN.oneBigNat (# #))  where   m = primeMod p -  l  = Integer.recipModBigNat z m-  l2 = Integer.sqrBigNat l-  l3 = Integer.timesBigNat l l2+  l  = BN.recipModBigNat z m+  l2 = BN.bigNatSqr l+  l3 = BN.bigNatMul l l2 -  x' = (Integer.timesBigNat x l2) `Integer.remBigNat` m-  y' = (Integer.timesBigNat y l3) `Integer.remBigNat` m+  x' = (BN.bigNatMul x l2) `BN.bigNatRem` m+  y' = (BN.bigNatMul y l3) `BN.bigNatRem` m   -- | Given an integer @k@ and a projective point @S@, compute@@ -348,30 +291,31 @@ ec_mult p d s   | d == 0    = zro   | d == 1    = s-  | Integer.isZeroBigNat (pz s) = zro+  | BN.bigNatIsZero (pz s) = zro   | otherwise =       case m of-        0# -> panic "ec_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))]+        0# -> panic "ec_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))]         _  -> go m zro   where    s' = ec_normalize p s    h  = 3*d -   d' = integerToBigNat d-   h' = integerToBigNat h+   d' = BN.integerToBigNat d+   h' = BN.integerToBigNat h     m = case widthInteger h of-         Integer.S# mint -> mint+         BN.IS mint -> mint          _ -> 0# +   go :: Int# -> ProjectivePoint -> ProjectivePoint    go i !r      | tagToEnum# (i ==# 0#) = r      | otherwise = go (i -# 1#) r'      where-      h_i = Integer.testBitBigNat h' i-      d_i = Integer.testBitBigNat d' i+      h_i = BN.testBitBigNat h' i+      d_i = BN.testBitBigNat d' i        r' = if h_i then              if d_i then r2 else ec_add p r2 s'@@ -395,26 +339,26 @@   (ProjectivePoint, ProjectivePoint, ProjectivePoint, ProjectivePoint) normalizeForTwinMult p s t      -- S == 0 && T == 0-   | Integer.isZeroBigNat a && Integer.isZeroBigNat b =+   | BN.bigNatIsZero a && BN.bigNatIsZero b =         (zro, zro, zro, zro)       -- S == 0 && T != 0-   | Integer.isZeroBigNat a =+   | BN.bigNatIsZero a =         let tnorm = ec_normalize p t          in (zro, tnorm, tnorm, ec_negate p tnorm)       -- T == 0 && S != 0-   | Integer.isZeroBigNat b =+   | BN.bigNatIsZero b =         let snorm = ec_normalize p s          in (snorm, zro, snorm, snorm)       -- S+T == 0, both != 0-   | Integer.isZeroBigNat c =+   | BN.bigNatIsZero c =         let snorm = ec_normalize p s          in (snorm, ec_negate p snorm, zro, ec_double p snorm)       -- S-T == 0, both != 0-   | Integer.isZeroBigNat d =+   | BN.bigNatIsZero d =         let snorm = ec_normalize p s          in (snorm, snorm, ec_double p snorm, zro) @@ -441,7 +385,7 @@    abcd = mod_mul p a bcd -  e = Integer.recipModBigNat abcd m+  e = BN.recipModBigNat abcd m    a_inv = mod_mul p e bcd   b_inv = mod_mul p e acd@@ -460,11 +404,11 @@   d_inv2 = mod_square p d_inv   d_inv3 = mod_mul p d_inv d_inv2 -  s'   = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) Integer.oneBigNat-  t'   = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) Integer.oneBigNat+  s'   = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) (BN.oneBigNat (# #))+  t'   = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) (BN.oneBigNat (# #)) -  spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) Integer.oneBigNat-  smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) Integer.oneBigNat+  spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) (BN.oneBigNat (# #))+  smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) (BN.oneBigNat (# #))   -- | Given an integer @j@ and a projective point @S@, together with@@ -477,52 +421,52 @@   Integer -> ProjectivePoint ->   Integer -> ProjectivePoint ->   ProjectivePoint-ec_twin_mult p (integerToBigNat -> d0) s (integerToBigNat -> d1) t =+ec_twin_mult p (BN.integerToBigNat -> d0) s (BN.integerToBigNat -> d1) t =    case m of-     0# -> panic "ec_twin_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))]+     0# -> panic "ec_twin_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))]      _  -> go m init_c0 init_c1 zro   where   (s',t',spt',smt') = normalizeForTwinMult p s t -  m = case max 4 (widthInteger (Integer.bigNatToInteger (primeMod p))) of-        Integer.S# mint -> mint+  m = case max 4 (widthInteger (BN.bigNatToInteger (primeMod p))) of+        BN.IS mint -> mint         _ -> 0# -- if `m` doesn't fit into an Int, should be impossible    init_c0 = C False False (tst d0 (m -# 1#)) (tst d0 (m -# 2#)) (tst d0 (m -# 3#)) (tst d0 (m -# 4#))   init_c1 = C False False (tst d1 (m -# 1#)) (tst d1 (m -# 2#)) (tst d1 (m -# 3#)) (tst d1 (m -# 4#))    tst x i-    | tagToEnum# (i >=# 0#) = Integer.testBitBigNat x i+    | isTrue# (i >=# 0#) = BN.testBitBigNat x i     | otherwise = False    f i =-    if tagToEnum# (i <# 18#) then-      if tagToEnum# (i <# 12#) then-        if tagToEnum# (i <# 4#) then+    if isTrue# (i <# 18#) then+      if isTrue# (i <# 12#) then+        if isTrue# (i <# 4#) then           12#         else           14#       else-        if tagToEnum# (i <# 14#) then+        if isTrue# (i <# 14#) then           12#         else           10#     else-      if tagToEnum# (i <# 22#) then+      if isTrue# (i <# 22#) then         9#       else-        if tagToEnum# (i <# 24#) then+        if isTrue# (i <# 24#) then           11#         else           12# -  go !k !c0 !c1 !r = if tagToEnum# (k <# 0#) then r else go (k -# 1#) c0' c1' r'+  go !k !c0 !c1 !r = if isTrue# (k <# 0#) then r else go (k -# 1#) c0' c1' r'     where       h0  = cStateToH c0       h1  = cStateToH c1-      u0  = if tagToEnum# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#)-      u1  = if tagToEnum# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#)+      u0  = if isTrue# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#)+      u1  = if isTrue# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#)       c0' = cStateUpdate u0 c0 (tst d0 (k -# 5#))       c1' = cStateUpdate u1 c1 (tst d1 (k -# 5#)) @@ -571,4 +515,4 @@ cStateUpdate u (C _ c1 c2 c3 c4 c5) e =   case u of     0# -> C c1 c2 c3 c4 c5 e-    _  -> C (complement c1) c2 c3 c4 c5 e+    _  -> C (not c1) c2 c3 c4 c5 e

@@ -14,6 +14,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RecordWildCards #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.REPL.Command (     -- * Commands     Command(..), CommandDescr(..), CommandBody(..), CommandExitCode(..)@@ -1124,9 +1126,18 @@ moduleCmd modString   | null modString = return ()   | otherwise      = do-      case parseModName modString of-        Just m  -> loadHelper (M.loadModuleByName m)-        Nothing -> rPutStrLn "Invalid module name."+    case parseModName modString of+      Just m+        | M.isParamInstModName m -> loadHelper (M.loadModuleByName m)+        | otherwise  ->+          do mpath <- liftModuleCmd (M.findModule m)+             case mpath of+               M.InFile file ->+                 do setEditPath file+                    setLoadedMod LoadedModule { lName = Just m, lPath = mpath }+                    loadHelper (M.loadModuleByPath file)+               M.InMem {} -> loadHelper (M.loadModuleByName m)+      Nothing -> rPutStrLn "Invalid module name."  loadPrelude :: REPL () loadPrelude  = moduleCmd $ show $ pp M.preludeName@@ -1246,7 +1257,7 @@   noInfo nameEnv name =     case M.nameInfo name of       M.Declared m _ ->-                      rPrint $runDoc nameEnv ("Name defined in module" <+> pp m)+                      rPrint $ runDoc nameEnv ("Name defined in module" <+> pp m)       M.Parameter  -> rPutStrLn "// No documentation is available."  @@ -1330,7 +1341,7 @@          return $            do rPutStrLn "" -              let property +              let property                     | P.PragmaProperty `elem` ifDeclPragmas = [text "property"]                     | otherwise                             = []               rPrint $ runDoc nameEnv

@@ -218,7 +218,7 @@   | detailedPrompt = withEdit ++ "> "   | otherwise      = modLn ++ "> "   where-  detailedPrompt = False+  detailedPrompt = id False    modLn   =     case lName =<< eLoadedMod rw of@@ -266,13 +266,13 @@  instance Applicative REPL where   {-# INLINE pure #-}-  pure = return+  pure x = REPL (\_ -> pure x)   {-# INLINE (<*>) #-}   (<*>) = ap  instance Monad REPL where   {-# INLINE return #-}-  return x = REPL (\_ -> return x)+  return = pure    {-# INLINE (>>=) #-}   m >>= f = REPL $ \ref -> do

@@ -420,7 +420,10 @@   mkTevs prims result = do     -- It's a bit fragile, but the value of the safety predicate seems     -- to always be the first value in the model assignment list.-    let Right (_, (safetyCV : cvs)) = SBV.getModelAssignment result+    let (safetyCV, cvs) =+          case SBV.getModelAssignment result of+            Right (_, (safetyCV' : cvs')) -> (safetyCV', cvs')+            _ -> error "processResults: SBV.getModelAssignment failure"         safety = SBV.cvToBool safetyCV         (vs, _) = parseValues ts cvs         mdl = computeModel prims ts vs

@@ -84,9 +84,10 @@ import Cryptol.TypeCheck.AST hiding (splitTApp) -- XXX: just use this one import Cryptol.TypeCheck.TypeMap import Cryptol.Utils.Ident(Namespace(..))-import Data.List(sortBy,groupBy)+import Data.List(sortBy) import Data.Either(partitionEithers) import Data.Map (Map)+import qualified Data.List.NonEmpty as NE import MonadLib hiding (mapM)  import Prelude ()@@ -224,7 +225,7 @@     NonRecursive d -> NonRecursive <$> rewD rews d     Recursive ds ->       do let (leave,rew) = partitionEithers (map consider ds)-             rewGroups   = groupBy sameTParams+             rewGroups   = NE.groupBy sameTParams                          $ sortBy compareTParams rew          ds1 <- mapM (rewD rews) leave          ds2 <- mapM rewSame rewGroups@@ -243,10 +244,10 @@                      else Left d    rewSame ds =-     do new <- forM ds $ \(d,_,_,e) ->+     do new <- forM (NE.toList ds) $ \(d,_,_,e) ->                  do x <- newName                     return (d, x, e)-        let (_,tps,props,_) : _ = ds+        let (_,tps,props,_) NE.:| _ = ds             tys            = map (TVar . tpVar) tps             proofNum       = length props             addRew (d,x,_) = insertTM (dName d,tys,proofNum) x

@@ -1,3 +1,6 @@+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+ -- | -- Module      :  Cryptol.Transform.Specialize -- Copyright   :  (c) 2013-2016 Galois, Inc.

@@ -1,4 +1,6 @@ {-# Language OverloadedStrings #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.CheckModuleInstance (checkModuleInstance) where  import           Data.Map ( Map )

@@ -1,6 +1,8 @@ {-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-} {-# Language OverloadedStrings #-} {-# Language Safe #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.Error where  import qualified Data.IntMap as IntMap@@ -16,6 +18,7 @@ import Cryptol.TypeCheck.Type import Cryptol.TypeCheck.InferTypes import Cryptol.TypeCheck.Subst+import Cryptol.TypeCheck.Unify(Path,isRootPath) import Cryptol.ModuleSystem.Name(Name) import Cryptol.Utils.Ident(Ident) import Cryptol.Utils.RecordMap@@ -52,7 +55,7 @@  -- | Should the first error suppress the next one. subsumes :: (Range,Error) -> (Range,Error) -> Bool-subsumes (_,NotForAll _ x _) (_,NotForAll _ y _) = x == y+subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y subsumes (r1,KindMismatch {}) (r2,err) =   case err of     KindMismatch {} -> r1 == r2@@ -84,10 +87,10 @@               | RecursiveTypeDecls [Name]                 -- ^ The type synonym declarations are recursive -              | TypeMismatch TypeSource Type Type+              | TypeMismatch TypeSource Path Type Type                 -- ^ Expected type, inferred type -              | RecursiveType TypeSource Type Type+              | RecursiveType TypeSource Path Type Type                 -- ^ Unification results in a recursive type                | UnsolvedGoals [Goal]@@ -105,11 +108,11 @@                 -- ^ Type wild cards are not allowed in this context                 -- (e.g., definitions of type synonyms). -              | TypeVariableEscaped TypeSource Type [TParam]+              | TypeVariableEscaped TypeSource Path Type [TParam]                 -- ^ Unification variable depends on quantified variables                 -- that are not in scope. -              | NotForAll TypeSource TVar Type+              | NotForAll TypeSource Path TVar Type                 -- ^ Quantified type variables (of kind *) need to                 -- match the given type, so it does not work for all types. @@ -222,15 +225,15 @@       TooManyTySynParams {}     -> err       TooFewTyParams {}         -> err       RecursiveTypeDecls {}     -> err-      TypeMismatch src t1 t2    -> TypeMismatch src !$ (apSubst su t1) !$ (apSubst su t2)-      RecursiveType src t1 t2   -> RecursiveType src !$ (apSubst su t1) !$ (apSubst su t2)+      TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)+      RecursiveType src pa t1 t2   -> RecursiveType src pa !$ (apSubst su t1) !$ (apSubst su t2)       UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs       UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs       UnsolvedDelayedCt g       -> UnsolvedDelayedCt !$ (apSubst su g)       UnexpectedTypeWildCard    -> err-      TypeVariableEscaped src t xs ->-                                 TypeVariableEscaped src !$ (apSubst su t) .$ xs-      NotForAll src x t         -> NotForAll src x !$ (apSubst su t)+      TypeVariableEscaped src pa t xs ->+                                 TypeVariableEscaped src pa !$ (apSubst su t) .$ xs+      NotForAll src pa x t        -> NotForAll src pa x !$ (apSubst su t)       TooManyPositionalTypeParams -> err       CannotMixPositionalAndNamedTypeParams -> err @@ -258,15 +261,15 @@       TooManyTySynParams {}     -> Set.empty       TooFewTyParams {}         -> Set.empty       RecursiveTypeDecls {}     -> Set.empty-      TypeMismatch _ t1 t2      -> fvs (t1,t2)-      RecursiveType _ t1 t2     -> fvs (t1,t2)+      TypeMismatch _ _ t1 t2    -> fvs (t1,t2)+      RecursiveType _ _ t1 t2   -> fvs (t1,t2)       UnsolvedGoals gs          -> fvs gs       UnsolvableGoals gs        -> fvs gs       UnsolvedDelayedCt g       -> fvs g       UnexpectedTypeWildCard    -> Set.empty-      TypeVariableEscaped _ t xs-> fvs t `Set.union`+      TypeVariableEscaped _ _ t xs-> fvs t `Set.union`                                             Set.fromList (map TVBound xs)-      NotForAll _ x t             -> Set.insert x (fvs t)+      NotForAll _ _ x t             -> Set.insert x (fvs t)       TooManyPositionalTypeParams -> Set.empty       CannotMixPositionalAndNamedTypeParams -> Set.empty       UndefinedTypeParameter {}             -> Set.empty@@ -308,13 +311,13 @@   ppPrec _ (WithNames err names) =     case err of -      RecursiveType src t1 t2 ->+      RecursiveType src pa t1 t2 ->         addTVarsDescsAfter names err $         nested "Matching would result in an infinite type." $-          vcat [ "The type: " <+> ppWithNames names t1-               , "occurs in:" <+> ppWithNames names t2-               , "When checking" <+> pp src-               ]+          vcat ( [ "The type: " <+> ppWithNames names t1+                 , "occurs in:" <+> ppWithNames names t2+                 ] ++ ppCtxt pa +++                 [ "When checking" <+> pp src ] )        UnexpectedTypeWildCard ->         addTVarsDescsAfter names err $@@ -357,13 +360,14 @@         nested "Recursive type declarations:"                (commaSep $ map nm ts) -      TypeMismatch src t1 t2 ->+      TypeMismatch src pa t1 t2 ->         addTVarsDescsAfter names err $         nested "Type mismatch:" $         vcat $           [ "Expected type:" <+> ppWithNames names t1           , "Inferred type:" <+> ppWithNames names t2           ] ++ mismatchHint t1 t2+            ++ ppCtxt pa             ++ ["When checking" <+> pp src]        UnsolvableGoals gs -> explainUnsolvable names gs@@ -389,22 +393,24 @@           nested "while validating user-specified signature" $           ppWithNames names g -      TypeVariableEscaped src t xs ->+      TypeVariableEscaped src pa t xs ->         addTVarsDescsAfter names err $         nested ("The type" <+> ppWithNames names t <+>                                         "is not sufficiently polymorphic.") $-          vcat [ "It cannot depend on quantified variables:" <+>-                     (commaSep (map (ppWithNames names) xs))-               , "When checking" <+> pp src-               ]+          vcat ( [ "It cannot depend on quantified variables:" <+>+                       (commaSep (map (ppWithNames names) xs))+                 ] ++ ppCtxt pa+                   ++ [ "When checking" <+> pp src ]+               ) -      NotForAll src x t ->+      NotForAll src pa x t ->         addTVarsDescsAfter names err $         nested "Inferred type is not sufficiently polymorphic." $-          vcat [ "Quantified variable:" <+> ppWithNames names x-               , "cannot match type:"   <+> ppWithNames names t-               , "When checking" <+> pp src-               ]+          vcat ( [ "Quantified variable:" <+> ppWithNames names x+                 , "cannot match type:"   <+> ppWithNames names t+                 ] ++ ppCtxt pa+                   ++ [ "When checking" <+> pp src ]+               )        BadParameterKind tp k ->         addTVarsDescsAfter names err $@@ -479,8 +485,11 @@      noUni = Set.null (Set.filter isFreeTV (fvs err)) +    ppCtxt pa = if isRootPath pa then [] else [ "Context:" <+> pp pa ]  ++ explainUnsolvable :: NameMap -> [Goal] -> Doc explainUnsolvable names gs =   addTVarsDescsAfter names gs (bullets (map explain gs))@@ -497,7 +506,9 @@     case tNoUser (goal g) of       TCon (PC pc) ts ->         let tys = [ backticks (ppWithNames names t) | t <- ts ]-            doc1 : _ = tys+            doc1 = case tys of+                     (doc1' : _) -> doc1'+                     [] -> error "explainUnsolvable: Expected TCon to have at least one argument"             custom msg = hang msg                             2 (text "arising from" $$                                pp (goalSource g)   $$@@ -563,7 +574,7 @@            PValidFloat ->             case ts of-              ~[e,p] -> +              ~[e,p] ->                 custom (hang "Unsupported floating point parameters:"                            2 ("exponent =" <+> ppWithNames names e $$                               "precision =" <+> ppWithNames names p))

@@ -15,6 +15,8 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE Safe #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.Infer   ( checkE   , checkSigB@@ -44,6 +46,7 @@                                         checkParameterConstraints) import           Cryptol.TypeCheck.Instantiate import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)+import           Cryptol.TypeCheck.Unify(rootPath) import           Cryptol.Utils.Ident import           Cryptol.Utils.Panic(panic) import           Cryptol.Utils.RecordMap@@ -58,7 +61,7 @@ import           Data.Ratio(numerator,denominator) import           Data.Traversable(forM) import           Data.Function(on)-import           Control.Monad(zipWithM,unless,foldM,forM_)+import           Control.Monad(zipWithM,unless,foldM,forM_,mplus)   @@ -247,13 +250,14 @@      P.ETuple es ->       do etys <- expectTuple (length es) tGoal-         let mkTGoal n t = WithSource t (TypeOfTupleField n)-         es'  <- zipWithM checkE es (zipWith mkTGoal [1..] etys)+         let mkTGoal n t e = WithSource t (TypeOfTupleField n) (getLoc e)+         es'  <- zipWithM checkE es (zipWith3 mkTGoal [1..] etys es)          return (ETuple es')      P.ERecord fs ->       do es  <- expectRec fs tGoal-         let checkField f (e,t) = checkE e (WithSource t (TypeOfRecordField f))+         let checkField f (e,t) =+                checkE e (WithSource t (TypeOfRecordField f) (getLoc e))          es' <- traverseRecordMap checkField es          return (ERec es') @@ -262,19 +266,19 @@     P.ESel e l ->       do let src = selSrc l          t <- newType src KType-         e' <- checkE e (WithSource t src)+         e' <- checkE e (WithSource t src (getLoc expr))          f <- newHasGoal l t (twsType tGoal)          return (hasDoSelect f e')      P.EList [] ->       do (len,a) <- expectSeq tGoal-         expectFin 0 (WithSource len LenOfSeq)+         expectFin 0 (WithSource len LenOfSeq (getLoc expr))          return (EList [] a)      P.EList es ->       do (len,a) <- expectSeq tGoal-         expectFin (length es) (WithSource len LenOfSeq)-         let checkElem e = checkE e (WithSource a TypeOfSeqElement)+         expectFin (length es) (WithSource len LenOfSeq (getLoc expr))+         let checkElem e = checkE e (WithSource a TypeOfSeqElement (getLoc e))          es' <- mapM checkElem es          return (EList es' a) @@ -378,11 +382,12 @@          (len,a) <- expectSeq tGoal           inferred <- smallest ts-         ctrs <- unify (WithSource len LenOfSeq) inferred+         ctrs <- unify (WithSource len LenOfSeq (getLoc expr)) inferred          newGoals CtComprehension ctrs           ds     <- combineMaps dss-         e'     <- withMonoTypes ds (checkE e (WithSource a TypeOfSeqElement))+         e'     <- withMonoTypes ds (checkE e+                                (WithSource a TypeOfSeqElement (getLoc e)))          return (EComp len a e' mss')       where       -- the renamer should have made these checks already?@@ -407,12 +412,13 @@     P.EApp e1 e2 ->       do let argSrc = TypeOfArg noArgDescr          t1  <- newType argSrc  KType-         e1' <- checkE e1 (WithSource (tFun t1 (twsType tGoal)) FunApp)-         e2' <- checkE e2 (WithSource t1 argSrc)+         e1' <- checkE e1+                  (WithSource (tFun t1 (twsType tGoal)) FunApp (getLoc e1))+         e2' <- checkE e2 (WithSource t1 argSrc (getLoc e2))          return (EApp e1' e2')      P.EIf e1 e2 e3 ->-      do e1'      <- checkE e1 (WithSource tBit TypeOfIfCondExpr)+      do e1'      <- checkE e1 (WithSource tBit TypeOfIfCondExpr (getLoc e1))          e2'      <- checkE e2 tGoal          e3'      <- checkE e3 tGoal          return (EIf e1' e2' e3')@@ -423,7 +429,7 @@      P.ETyped e t ->       do tSig <- checkTypeOfKind t KType-         e' <- checkE e (WithSource tSig TypeFromUserAnnotation)+         e' <- checkE e (WithSource tSig TypeFromUserAnnotation (getLoc expr))          checkHasType tSig tGoal          return e' @@ -465,28 +471,28 @@      Just e ->       do e1 <- checkE e tGoal-         foldM doUpd e1 fs+         fst <$> foldM doUpd (e1, getLoc e) fs    where-  doUpd e (P.UpdField how sels v) =+  doUpd (e,eloc) (P.UpdField how sels v) =     case sels of       [l] ->         case how of           P.UpdSet ->             do let src = selSrc s                ft <- newType src KType-               v1 <- checkE v (WithSource ft src)+               v1 <- checkE v (WithSource ft src eloc)                d  <- newHasGoal s (twsType tGoal) ft-               pure (hasDoSet d e v1)+               pure (hasDoSet d e v1, eloc `rCombMaybe` getLoc v)           P.UpdFun ->              do let src = selSrc s                 ft <- newType src KType-                v1 <- checkE v (WithSource (tFun ft ft) src)+                v1 <- checkE v (WithSource (tFun ft ft) src eloc)                 -- XXX: ^ may be used a different src?                 d  <- newHasGoal s (twsType tGoal) ft                 tmp <- newParamName NSValue (packIdent "rf")                 let e' = EVar tmp-                pure $ hasDoSet d e' (EApp v1 (hasDoSelect d e'))+                pure ( hasDoSet d e' (EApp v1 (hasDoSelect d e'))                        `EWhere`                        [  NonRecursive                           Decl { dName        = tmp@@ -497,6 +503,7 @@                                , dFixity      = Nothing                                , dDoc         = Nothing                                } ]+                      , eloc `rCombMaybe` getLoc v )          where s = thing l       _ -> panic "checkRecUpd/doUpd" [ "Expected exactly 1 field label"@@ -505,11 +512,11 @@   expectSeq :: TypeWithSource -> InferM (Type,Type)-expectSeq tGoal@(WithSource ty src) =+expectSeq tGoal@(WithSource ty src rng) =   case ty of      TUser _ _ ty' ->-         expectSeq (WithSource ty' src)+         expectSeq (WithSource ty' src rng)      TCon (TC TCSeq) [a,b] ->          return (a,b)@@ -521,7 +528,7 @@      _ ->       do tys@(a,b) <- genTys-         recordError (TypeMismatch src ty (tSeq a b))+         recordErrorLoc rng (TypeMismatch src rootPath ty (tSeq a b))          return tys   where   genTys =@@ -531,11 +538,11 @@   expectTuple :: Int -> TypeWithSource -> InferM [Type]-expectTuple n tGoal@(WithSource ty src) =+expectTuple n tGoal@(WithSource ty src rng) =   case ty of      TUser _ _ ty' ->-         expectTuple n (WithSource ty' src)+         expectTuple n (WithSource ty' src rng)      TCon (TC (TCTuple n')) tys | n == n' ->          return tys@@ -547,7 +554,7 @@      _ ->       do tys <- genTys-         recordError (TypeMismatch src ty (tTuple tys))+         recordErrorLoc rng (TypeMismatch src rootPath ty (tTuple tys))          return tys    where@@ -558,11 +565,11 @@   RecordMap Ident (Range, a) ->   TypeWithSource ->   InferM (RecordMap Ident (a, Type))-expectRec fs tGoal@(WithSource ty src) =+expectRec fs tGoal@(WithSource ty src rng) =   case ty of      TUser _ _ ty' ->-         expectRec fs (WithSource ty' src)+         expectRec fs (WithSource ty' src rng)      TRec ls       | Right r <- zipRecords (\_ (_rng,v) t -> (v,t)) fs ls -> pure r@@ -577,16 +584,16 @@          case ty of            TVar TVFree{} -> do ps <- unify tGoal (TRec tys)                                newGoals CtExactType ps-           _ -> recordError (TypeMismatch src ty (TRec tys))+           _ -> recordErrorLoc rng (TypeMismatch src rootPath ty (TRec tys))          return res   expectFin :: Int -> TypeWithSource -> InferM ()-expectFin n tGoal@(WithSource ty src) =+expectFin n tGoal@(WithSource ty src rng) =   case ty of      TUser _ _ ty' ->-         expectFin n (WithSource ty' src)+         expectFin n (WithSource ty' src rng)      TCon (TC (TCNum n')) [] | toInteger n == n' ->          return ()@@ -594,7 +601,7 @@     _ -> newGoals CtExactType =<< unify tGoal (tNum n)  expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)-expectFun mbN n (WithSource ty0 src)  = go [] n ty0+expectFun mbN n (WithSource ty0 src rng)  = go [] n ty0   where    go tys arity ty@@ -612,9 +619,10 @@              res  <- newType TypeOfRes KType              case ty of                TVar TVFree{} ->-                  do ps <- unify (WithSource ty src) (foldr tFun res args)+                  do ps <- unify (WithSource ty src rng) (foldr tFun res args)                      newGoals CtExactType  ps-               _ -> recordError (TypeMismatch src ty (foldr tFun res args))+               _ -> recordErrorLoc rng+                        (TypeMismatch src rootPath ty (foldr tFun res args))              return (reverse tys ++ args, res)      | otherwise =@@ -641,9 +649,11 @@   do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ]       (tys,tRes) <- expectFun fun (length ps) tGoal-     largs      <- sequence (zipWith checkP ps (zipWith WithSource tys descs))+     let srcs = zipWith3 WithSource tys descs (map getLoc ps)+     largs      <- sequence (zipWith checkP ps srcs)      let ds = Map.fromList [ (thing x, x { thing = t }) | (x,t) <- zip largs tys ]-     e1         <- withMonoTypes ds (checkE e (WithSource tRes TypeOfRes))+     e1 <- withMonoTypes ds+              (checkE e (WithSource tRes TypeOfRes (twsRange tGoal)))       let args = [ (thing x, t) | (x,t) <- zip largs tys ]      return (foldr (\(x,t) b -> EAbs x t b) e1 args)@@ -658,11 +668,12 @@                    return a  checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)-checkP p tGoal@(WithSource _ src) =+checkP p tGoal@(WithSource _ src rng0) =   do (x, t) <- inferP p      ps <- unify tGoal (thing t)-     let rng   = fromMaybe emptyRange (getLoc p)-     let mkErr = recordError . UnsolvedGoals . (:[])+     let rngMb = getLoc p `mplus` rng0+         rng   = fromMaybe emptyRange rngMb+     let mkErr = recordErrorLoc rngMb . UnsolvedGoals . (:[])                                                    . Goal (CtPattern src) rng      mapM_ mkErr ps      return (Located (srcRange t) x)@@ -679,7 +690,7 @@      P.PTyped p t ->       do tSig <- checkTypeOfKind t KType-         ln   <- checkP p (WithSource tSig TypeFromUserAnnotation)+         ln   <- checkP p (WithSource tSig TypeFromUserAnnotation (getLoc t))          return (thing ln, ln { thing = tSig })      _ -> tcPanic "inferP" [ "Unexpected pattern:", show pat ]@@ -691,7 +702,8 @@ inferMatch (P.Match p e) =   do (x,t) <- inferP p      n     <- newType LenOfCompGen KNum-     e'    <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp)+     e'    <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp+                                   (getLoc e))      return (From x n (thing t) e', x, t, n)  inferMatch (P.MatchLet b)@@ -943,7 +955,7 @@      P.DExpr e ->       do let nm = thing (P.bName b)-         let tGoal = WithSource t (DefinitionOf nm)+         let tGoal = WithSource t (DefinitionOf nm) (getLoc b)          e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal          let f = thing (P.bName b)          return Decl { dName = f@@ -975,7 +987,7 @@   withTParams as $   do (e1,cs0) <- collectGoals $                 do let nm = thing (P.bName b)-                       tGoal = WithSource t0 (DefinitionOf nm)+                       tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)                    e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal                    addGoals validSchema                    () <- simplifyAllConstraints  -- XXX: using `asmps` also?

@@ -205,5 +205,6 @@     | Set.notMember tp bounds = return []     | otherwise = let a   = tpVar tp                       src = tvarDesc (tvInfo a)-                  in unify (WithSource (TVar a) src) ty+                      rng = Just (tvarSource (tvInfo a))+                  in unify (WithSource (TVar a) src rng) ty 

@@ -8,6 +8,8 @@  {-# LANGUAGE RecursiveDo #-} {-# LANGUAGE Safe #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.Kind   ( checkType   , checkSchema@@ -302,7 +304,8 @@     do let ty = tpVar (mtpParam a)        (ts1,k1) <- appTy ts (kindOf ty)        case k of-         Just ks | ks /= k1 -> kRecordError $ KindMismatch Nothing ks k1+         Just ks+           | ks /= k1 -> kRecordError (KindMismatch Nothing ks k1)          _ -> return ()         unless (null ts1) $

@@ -45,7 +45,8 @@ import           Cryptol.TypeCheck.AST import           Cryptol.TypeCheck.Subst import           Cryptol.TypeCheck.Interface(genIface)-import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))+import           Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)+                                        , Path, rootPath) import           Cryptol.TypeCheck.InferTypes import           Cryptol.TypeCheck.Error( Warning(..),Error(..)                                         , cleanupErrors, computeFreeVarNames@@ -292,11 +293,11 @@   fmap f (IM m) = IM (fmap f m)  instance A.Applicative InferM where-  pure  = return+  pure x = IM (pure x)   (<*>) = ap  instance Monad InferM where-  return x      = IM (return x)+  return        = pure   IM m >>= f    = IM (m >>= unIM . f)  instance Fail.MonadFail InferM where@@ -331,12 +332,21 @@  -- | Report an error. recordError :: Error -> InferM ()-recordError e =-  do r <- case e of-            AmbiguousSize d _ -> return (tvarSource d)-            _ -> curRange+recordError = recordErrorLoc Nothing++-- | Report an error.+recordErrorLoc :: Maybe Range -> Error -> InferM ()+recordErrorLoc rng e =+  do r <- case rng of+            Just r  -> pure r+            Nothing -> case e of+                         AmbiguousSize d _ -> return (tvarSource d)+                         _                 -> curRange      IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s } +++ recordWarning :: Warning -> InferM () recordWarning w =   unless ignore $@@ -549,23 +559,23 @@  -- | Record that the two types should be syntactically equal. unify :: TypeWithSource -> Type -> InferM [Prop]-unify (WithSource t1 src) t2 =+unify (WithSource t1 src rng) t2 =   do t1' <- applySubst t1      t2' <- applySubst t2-     let ((su1, ps), errs) = runResult (mgu t1' t2')+     let ((su1, ps), errs) = runResult (doMGU t1' t2')      extendSubst su1-     let toError :: UnificationError -> Error-         toError err =+     let toError :: (Path,UnificationError) -> Error+         toError (pa,err) =            case err of-             UniTypeLenMismatch _ _ -> TypeMismatch src t1' t2'-             UniTypeMismatch s1 s2  -> TypeMismatch src s1 s2+             UniTypeLenMismatch _ _ -> TypeMismatch src rootPath t1' t2'+             UniTypeMismatch s1 s2  -> TypeMismatch src pa s1 s2              UniKindMismatch k1 k2  -> KindMismatch (Just src) k1 k2-             UniRecursive x t       -> RecursiveType src (TVar x) t-             UniNonPolyDepends x vs -> TypeVariableEscaped src (TVar x) vs-             UniNonPoly x t         -> NotForAll src x t+             UniRecursive x t       -> RecursiveType src pa (TVar x) t+             UniNonPolyDepends x vs -> TypeVariableEscaped src pa (TVar x) vs+             UniNonPoly x t         -> NotForAll src pa x t      case errs of        [] -> return ps-       _  -> do mapM_ (recordError . toError) errs+       _  -> do mapM_ (recordErrorLoc rng . toError) errs                 return []  -- | Apply the accumulated substitution to something with free type variables.@@ -958,11 +968,11 @@   fmap f (KM m) = KM (fmap f m)  instance A.Applicative KindM where-  pure  = return+  pure x = KM (pure x)   (<*>) = ap  instance Monad KindM where-  return x      = KM (return x)+  return        = pure   KM m >>= k    = KM (m >>= unKM . k)  instance Fail.MonadFail KindM where

@@ -472,11 +472,11 @@   fmap = liftM  instance A.Applicative TcM where-  pure  = return+  pure a = TcM (pure a)   (<*>) = ap  instance Monad TcM where-  return a    = TcM (return a)+  return      = pure   TcM m >>= f = TcM (do a <- m                         let TcM m1 = f a                         m1)

@@ -1,4 +1,6 @@ {-# LANGUAGE PatternGuards #-}+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.SimpType where  import Control.Applicative((<|>))

@@ -34,7 +34,10 @@    where   dbg msg x-    | False     = ppTrace msg x+      -- Change `False` to `True` below to enable extra tracing. Note that+      -- this is written with an extraneous `id` expression to suppress+      -- pattern-match coverage checking warnings in this one case.+    | id False  = ppTrace msg x     | otherwise = x  

@@ -9,8 +9,7 @@ import           Data.List (sortBy) import           Data.MemoTrie -import qualified GHC.Integer.GMP.Internals as Integer-+import Math.NumberTheory.Primes.Testing (isPrime)  import Cryptol.Utils.Patterns import Cryptol.TypeCheck.Type hiding (tMul)@@ -78,11 +77,6 @@ {-# NOINLINE primeTable #-} primeTable :: Integer :->: Bool primeTable = trie isPrime-  where-    isPrime i =-      case Integer.testPrimeInteger i 25# of-        0# -> False-        _  -> True  cryIsPrime :: Ctxt -> Type -> Solved cryIsPrime _varInfo ty =

@@ -8,6 +8,7 @@ {-# LANGUAGE PatternGuards, Safe #-} module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where +import Cryptol.Parser.Position(Range) import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.InferTypes import Cryptol.TypeCheck.Monad( InferM, unify, newGoals@@ -41,8 +42,8 @@      return (tSeq (tNum n) elems)  -improveSelector :: Selector -> Type -> InferM Bool-improveSelector sel outerT =+improveSelector :: Maybe Range -> Selector -> Type -> InferM Bool+improveSelector rng sel outerT =   case sel of     RecordSel _ mb -> cvt recordType mb     TupleSel  _ mb -> cvt tupleType  mb@@ -50,7 +51,7 @@   where   cvt _ Nothing   = return False   cvt f (Just a)  = do ty <- f a-                       ps <- unify (WithSource outerT (selSrc sel)) ty+                       ps <- unify (WithSource outerT (selSrc sel) rng) ty                        newGoals CtExactType ps                        newT <- applySubst outerT                        return (newT /= outerT)@@ -117,13 +118,15 @@ tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved tryHasGoal has   | TCon (PC (PHas sel)) [ th, ft ] <- goal (hasGoal has) =-    do imped     <- improveSelector sel th+    do let rng = Just (goalRange (hasGoal has))+       imped     <- improveSelector rng sel th        outerT    <- tNoUser `fmap` applySubst th        mbInnerT  <- solveSelector sel outerT        case mbInnerT of          Nothing -> return (imped, False)          Just innerT ->-           do newGoals CtExactType =<< unify (WithSource innerT (selSrc sel)) ft+           do newGoals CtExactType =<<+                                  unify (WithSource innerT (selSrc sel) rng) ft               oT <- applySubst outerT               iT <- applySubst innerT               sln <- mkSelSln sel oT iT

@@ -231,6 +231,7 @@ data TypeWithSource = WithSource   { twsType   :: Type   , twsSource :: TypeSource+  , twsRange  :: !(Maybe Range)   }  

@@ -1,3 +1,5 @@+-- See Note [-Wincomplete-uni-patterns and irrefutable patterns]+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module Cryptol.TypeCheck.TypePat   ( aInf, aNat, aNat' @@ -193,4 +195,26 @@                     _                                     -> mzero  +{-+Note [-Wincomplete-uni-patterns and irrefutable patterns]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Various parts of Cryptol use irrefutable patterns in functions that assume that+their arguments have particular shapes. For example, the `ar1 ~[a] = a`+function in this module uses an irrefutable pattern because it assumes the+invariant that the argument list will have exactly one element. This lets ar1+be slightly lazier when evaluated. +Unfortunately, this use of irrefutable patterns is at odds with the+-Wincomplete-uni-patterns warning. At present, -Wincomplete-uni-patterns will+produce a warning for any irrefutable pattern that does not cover all possible+data constructors. While we could rewrite functions like `ar1` to explicitly+provide a fall-through case, that would change its strictness properties. As+a result, we simply disable -Wincomplete-uni-patterns warnings in each part+of Cryptol that uses irrefutable patterns.++Arguably, -Wincomplete-uni-patterns shouldn't be producing warnings for+irrefutable patterns at all. GHC issue #14800+(https://gitlab.haskell.org/ghc/ghc/-/issues/14800) proposes this idea.+If that issue is fixed in the future, we may want to reconsider whether we want+to disable -Wincomplete-uni-patterns.+-}

@@ -8,13 +8,20 @@  {-# LANGUAGE Safe #-} {-# LANGUAGE PatternGuards, ViewPatterns #-}-{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-}+{-# LANGUAGE BlockArguments, OverloadedStrings #-} module Cryptol.TypeCheck.Unify where +import Control.DeepSeq(NFData)+import GHC.Generics(Generic)+ import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst import Cryptol.Utils.RecordMap+import Cryptol.Utils.Ident(Ident)+import Cryptol.ModuleSystem.Name(nameIdent) +import Cryptol.TypeCheck.PP import Control.Monad.Writer (Writer, writer, runWriter) import qualified Data.Set as Set @@ -25,9 +32,9 @@ -- on bound variables. type MGU = (Subst,[Prop]) -type Result a = Writer [UnificationError] a+type Result a = Writer [(Path,UnificationError)] a -runResult :: Result a -> (a, [UnificationError])+runResult :: Result a -> (a, [(Path,UnificationError)]) runResult = runWriter  data UnificationError@@ -38,31 +45,56 @@   | UniNonPolyDepends TVar [TParam]   | UniNonPoly TVar Type -uniError :: UnificationError -> Result MGU-uniError e = writer (emptyMGU, [e])+uniError :: Path -> UnificationError -> Result MGU+uniError p e = writer (emptyMGU, [(p,e)])  +newtype Path = Path [PathElement]+  deriving (Show,Generic,NFData)++data PathElement =+    TConArg     TC      Int+  | TNewtypeArg Newtype Int+  | TRecArg     Ident+  deriving (Show,Generic,NFData)++rootPath :: Path+rootPath = Path []++isRootPath :: Path -> Bool+isRootPath (Path xs) = null xs++extPath :: Path -> PathElement -> Path+extPath (Path xs) x = Path (x : xs)++ emptyMGU :: MGU emptyMGU = (emptySubst, []) -mgu :: Type -> Type -> Result MGU+doMGU :: Type -> Type -> Result MGU+doMGU t1 t2 = mgu rootPath t1 t2 -mgu (TUser c1 ts1 _) (TUser c2 ts2 _)+mgu :: Path -> Type -> Type -> Result MGU++mgu _ (TUser c1 ts1 _) (TUser c2 ts2 _)   | c1 == c2 && ts1 == ts2  = return emptyMGU -mgu (TVar x) t        = bindVar x t-mgu t (TVar x)        = bindVar x t+mgu p (TVar x) t     = bindVar p x t+mgu p t (TVar x)     = bindVar p x t -mgu (TUser _ _ t1) t2 = mgu t1 t2-mgu t1 (TUser _ _ t2) = mgu t1 t2+mgu p (TUser _ _ t1) t2 = mgu p t1 t2+mgu p t1 (TUser _ _ t2) = mgu p t1 t2 -mgu (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)-  | tc1 == tc2 = mguMany ts1 ts2+mgu p (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)+  | tc1 == tc2 =+    let paths = [ extPath p (TConArg tc1 i) | i <- [ 0 .. ] ]+    in mguMany p paths ts1 ts2 -mgu (TCon (TF f1) ts1) (TCon (TF f2) ts2)+mgu _ (TCon (TF f1) ts1) (TCon (TF f2) ts2)   | f1 == f2 && ts1 == ts2  = return emptyMGU -mgu t1 t2+-- XXX: here we loose the information about where the constarint came from+mgu _ t1 t2   | TCon (TF _) _ <- t1, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])   | TCon (TF _) _ <- t2, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2])   where@@ -71,58 +103,114 @@    isNum = k1 == KNum -mgu (TRec fs1) (TRec fs2)-  | fieldSet fs1 == fieldSet fs2 = mguMany (recordElements fs1) (recordElements fs2)+mgu p (TRec fs1) (TRec fs2)+  | fieldSet fs1 == fieldSet fs2 =+    let paths = [ extPath p (TRecArg i) | (i,_) <- canonicalFields fs1 ]+    in mguMany p paths (recordElements fs1) (recordElements fs2) -mgu (TNewtype ntx xs) (TNewtype nty ys)-  | ntx == nty = mguMany xs ys+mgu p (TNewtype ntx xs) (TNewtype nty ys)+  | ntx == nty =+    let paths = [ extPath p (TNewtypeArg ntx i) | i <- [ 0 .. ] ]+    in mguMany p paths xs ys -mgu t1 t2-  | not (k1 == k2)  = uniError $ UniKindMismatch k1 k2-  | otherwise       = uniError $ UniTypeMismatch t1 t2+mgu p t1 t2+  | not (k1 == k2)  = uniError p $ UniKindMismatch k1 k2+  | otherwise       = uniError p $ UniTypeMismatch t1 t2   where   k1 = kindOf t1   k2 = kindOf t2  -mguMany :: [Type] -> [Type] -> Result MGU-mguMany [] [] = return emptyMGU-mguMany (t1 : ts1) (t2 : ts2) =-  do (su1,ps1) <- mgu t1 t2-     (su2,ps2) <- mguMany (apSubst su1 ts1) (apSubst su1 ts2)+-- XXX: could pass the path to the lists themselvs+mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU+mguMany _ _ [] [] = return emptyMGU+mguMany p (p1:ps) (t1 : ts1) (t2 : ts2) =+  do (su1,ps1) <- mgu p1 t1 t2+     (su2,ps2) <- mguMany p ps (apSubst su1 ts1) (apSubst su1 ts2)      return (su2 @@ su1, ps1 ++ ps2)-mguMany t1 t2 = uniError $ UniTypeLenMismatch (length t1) (length t2)+mguMany p _ t1 t2 = uniError p $ UniTypeLenMismatch (length t1) (length t2)+-- XXX: I think by this point the types should have been kind checked,+-- so there should be no mismatches with the lengths...  -bindVar :: TVar -> Type -> Result MGU+bindVar :: Path -> TVar -> Type -> Result MGU -bindVar x (tNoUser -> TVar y)+bindVar _ x (tNoUser -> TVar y)   | x == y                      = return emptyMGU -bindVar v@(TVBound {}) (tNoUser -> TVar v1@(TVFree {})) = bindVar v1 (TVar v)+bindVar p v@(TVBound {})+          (tNoUser -> TVar v1@(TVFree {})) = bindVar p v1 (TVar v) -bindVar v@(TVBound {}) t+bindVar p v@(TVBound {}) t   | k == kindOf t = if k == KNum                        then return (emptySubst, [TVar v =#= t])-                       else uniError $ UniNonPoly v t-  | otherwise     = uniError $ UniKindMismatch k (kindOf t)+                       else uniError p $ UniNonPoly v t+  | otherwise     = uniError p $ UniKindMismatch k (kindOf t)   where k = kindOf v -bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))+bindVar _ x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))   | xscope `Set.isProperSubsetOf` yscope, xk == yk =     return (uncheckedSingleSubst y (TVar x), [])     -- In this case, we can add the reverse binding y ~> x to the     -- substitution, but the instantiation x ~> y would be forbidden     -- because it would allow y to escape from its scope. -bindVar x t =+bindVar p x t =   case singleSubst x t of     Left SubstRecursive-      | kindOf x == KType -> uniError $ UniRecursive x t+      | kindOf x == KType -> uniError p $ UniRecursive x t       | otherwise -> return (emptySubst, [TVar x =#= t])     Left (SubstEscaped tps) ->-      uniError $ UniNonPolyDepends x tps+      uniError p $ UniNonPolyDepends x tps     Left (SubstKindMismatch k1 k2) ->-      uniError $ UniKindMismatch k1 k2+      uniError p $ UniKindMismatch k1 k2     Right su ->       return (su, [])+++--------------------------------------------------------------------------------++ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc+ppPathEl el prec k =+  case el of+    TRecArg l -> braces (pp l <+> ":" <+> k 0 <.> comma <+> "…")++    TConArg tc n ->+      case tc of++       TCSeq -> optParens (prec > 4)+                if n == 0 then brackets (k 0) <+> "_"+                          else brackets "_" <+> (k 4)++       TCFun -> optParens (prec > 1)+                if n == 0 then k 2 <+> "->" <+> "_"+                          else "_" <+> "->" <+> k 1++       TCTuple i  -> parens (commaSep (before ++ [k 0] ++ after))+          where before = replicate n "_"+                after  = replicate (i - n - 1) "_"++       _ -> justPrefix (kindArity (kindOf tc)) (pp tc) n++    TNewtypeArg nt n ->+      justPrefix (length (ntParams nt)) (pp (nameIdent (ntName nt))) n++  where+  justPrefix arity fun n =+    optParens (prec > 3) (fun <+> hsep (before ++ [k 5] ++ after))+    where before = replicate n "_"+          after  = replicate (arity - n - 1) "_"++  kindArity ki =+    case ki of+      _ :-> k1 -> 1 + kindArity k1+      _        -> 0++instance PP Path where+  ppPrec prec0 (Path ps0) = go (reverse ps0) prec0+    where+    go ps prec =+      case ps of+        []       -> "ERROR"+        p : more -> ppPathEl p prec (go more)+

@@ -0,0 +1,155 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE UnboxedSums #-}+{-# LANGUAGE UnboxedTuples #-}++-- |+-- Module      :  GHC.Num.Compat+-- Description :  Defines numeric compatibility shims that work with both+--                ghc-bignum (GHC 9.0+) and integer-gmp (older GHCs).+-- Copyright   :  (c) 2021 Galois, Inc.+-- License     :  BSD3+-- Maintainer  :  cryptol@galois.com+-- Stability   :  provisional+-- Portability :  portable+module GHC.Num.Compat+  ( -- * BigNat#+    BigNat#+  , bigNatAdd+  , bigNatIsOne+  , bigNatIsZero+  , bigNatMul+  , bigNatRem+  , bigNatSqr+  , bigNatSub+  , bigNatSubUnsafe+  , oneBigNat+  , recipModBigNat+  , shiftLBigNat+  , shiftRBigNat+  , testBitBigNat+  , zeroBigNat++    -- * Integer+  , Integer(IS, IP, IN)+  , integerRecipMod++    -- * Conversions+  , bigNatToInteger+  , integerToBigNat+  ) where++#if defined(MIN_VERSION_ghc_bignum)+import           GHC.Num.BigNat (BigNat#, bigNatAdd, bigNatIsOne, bigNatIsZero, bigNatMul, bigNatRem, bigNatSqr, bigNatSub, bigNatSubUnsafe)+import qualified GHC.Num.Backend as BN+import qualified GHC.Num.BigNat as BN+import           GHC.Num.Integer (Integer(IS, IP, IN))+import qualified GHC.Num.Integer as Integer+import           GHC.Exts++-- | Coerce a @BigNat#@ to an integer value.+bigNatToInteger :: BigNat# -> Integer+bigNatToInteger = Integer.integerFromBigNat#++-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@.+--+-- PRECONDITION: @m@ must be strictly positive.+integerRecipMod :: Integer -> Integer -> Maybe Integer+integerRecipMod x y =+  case Integer.integerRecipMod# x (Integer.integerToNaturalClamp y) of+    (# r | #)  -> Just (toInteger r)+    (# | () #) -> Nothing++-- | Coerce an integer value to a @BigNat#@.  This operation only really makes+--   sense for nonnegative values, but this condition is not checked.+integerToBigNat :: Integer -> BigNat#+integerToBigNat = Integer.integerToBigNatClamp#++-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk.+oneBigNat :: (# #) -> BigNat#+oneBigNat _ = BN.bigNatFromWord# 1##++recipModBigNat :: BigNat# -> BigNat# -> BigNat#+recipModBigNat = BN.sbignat_recip_mod 0#++shiftLBigNat :: BigNat# -> Int# -> BigNat#+shiftLBigNat bn i = BN.bigNatShiftL# bn (int2Word# i)++shiftRBigNat :: BigNat# -> Int# -> BigNat#+shiftRBigNat bn i = BN.bigNatShiftR# bn (int2Word# i)++testBitBigNat :: BigNat# -> Int# -> Bool+testBitBigNat bn i = isTrue# (BN.bigNatTestBit# bn (int2Word# i))++-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk.+zeroBigNat :: (# #) -> BigNat#+zeroBigNat _ = BN.bigNatFromWord# 0##+#else+import           GHC.Integer.GMP.Internals (bigNatToInteger, recipModBigNat, shiftLBigNat, shiftRBigNat, testBitBigNat)+import qualified GHC.Integer.GMP.Internals as GMP+import           GHC.Exts++type BigNat# = GMP.BigNat++{-# COMPLETE IS, IP, IN #-}++pattern IS :: Int# -> Integer+pattern IS i = GMP.S# i++pattern IP :: ByteArray# -> Integer+pattern IP ba = GMP.Jp# (GMP.BN# ba)++pattern IN :: ByteArray# -> Integer+pattern IN ba = GMP.Jn# (GMP.BN# ba)++bigNatAdd :: BigNat# -> BigNat# -> BigNat#+bigNatAdd = GMP.plusBigNat++bigNatIsOne :: BigNat# -> Bool+bigNatIsOne bn = GMP.eqBigNat bn GMP.oneBigNat++bigNatIsZero :: BigNat# -> Bool+bigNatIsZero = GMP.isZeroBigNat++bigNatMul :: BigNat# -> BigNat# -> BigNat#+bigNatMul = GMP.timesBigNat++bigNatRem :: BigNat# -> BigNat# -> BigNat#+bigNatRem = GMP.remBigNat++bigNatSqr :: BigNat# -> BigNat#+bigNatSqr = GMP.sqrBigNat++bigNatSub :: BigNat# -> BigNat# -> (# (# #) | BigNat# #)+bigNatSub x y =+  case GMP.isNullBigNat# res of+    0# -> (# | res #)+    _  -> (# (# #) | #)+  where+    res = GMP.minusBigNat x y++bigNatSubUnsafe :: BigNat# -> BigNat# -> BigNat#+bigNatSubUnsafe = GMP.minusBigNat++integerToBigNat :: Integer -> BigNat#+integerToBigNat (GMP.S# i)  = GMP.wordToBigNat (int2Word# i)+integerToBigNat (GMP.Jp# b) = b+integerToBigNat (GMP.Jn# b) = b++-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@.+--+-- PRECONDITION: @m@ must be strictly positive.+integerRecipMod :: Integer -> Integer -> Maybe Integer+integerRecipMod x y+  | res == 0  = Nothing+  | otherwise = Just res+  where+    res = GMP.recipModInteger x y++oneBigNat :: (##) -> BigNat#+oneBigNat _ = GMP.oneBigNat++zeroBigNat :: (##) -> BigNat#+zeroBigNat _ = GMP.zeroBigNat+#endif