From 2029605a3cb982f8043d1fc2dbaf2e675f2fb4fb Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 21 Aug 2020 15:38:29 -0700 Subject: [PATCH 1/6] Implement primitive `foldl` and `foldl'` operations. Reimplement `foldr` and add `foldr'` in terms of the left folds. --- lib/Cryptol.cry | 25 +++- src/Cryptol/Eval/Concrete.hs | 7 + src/Cryptol/Eval/Generic.hs | 50 +++++++ src/Cryptol/Eval/SBV.hs | 3 + src/Cryptol/Eval/What4.hs | 3 + tests/issues/T146.icry.stdout | 16 +-- tests/issues/issue226.icry.stdout | 2 + tests/issues/issue290v2.icry.stdout | 4 +- tests/issues/issue723.icry.stdout | 4 +- tests/regression/instance.icry.stdout | 180 +++++++++++++------------- 10 files changed, 187 insertions(+), 107 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index a4c2ac1c4..5bfaca22d 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -1028,9 +1028,14 @@ map f xs = [f x | x <- xs] * * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3 */ -foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a -foldl f acc xs = ys ! 0 - where ys = [acc] # [f a x | a <- ys | x <- xs] +primitive foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + +/** + * Functional left fold, with strict evaluation of the accumulator value. + * + * foldl' (+) 0 [1,2,3] = ((0 + 1) + 2) + 3 + */ +primitive foldl' : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a /** * Functional right fold. @@ -1038,8 +1043,18 @@ foldl f acc xs = ys ! 0 * foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3)) */ foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b -foldr f acc xs = ys ! 0 - where ys = [acc] # [f x a | a <- ys | x <- reverse xs] +foldr f acc xs = foldl g acc (reverse xs) + where g b a = f a b + +/** + * Functional right fold, with strict evaluation of the accumulator value. + * + * foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3)) + */ +foldr' : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b +foldr' f acc xs = foldl' g acc (reverse xs) + where g b a = f a b + /** * Compute the sum of the values in the sequence. diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index eaa2c6e76..a1795e72d 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -298,6 +298,13 @@ primTable eOpts = let sym = Concrete in updatePrim sym updateBack_word updateBack) -- Misc + , ("foldl" , {-# SCC "Prelude::foldl" #-} + foldlV sym) + + , ("foldl'" , {-# SCC "Prelude::foldl'" #-} + foldl'V sym) + + , ("parmap" , {-# SCC "Prelude::parmap" #-} parmapV sym) diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 3764e0fcc..9a82b5622 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -8,6 +8,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE BlockArguments #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Safe #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -1909,6 +1910,55 @@ mergeSeqMap sym c x y = iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i) + +foldlV :: Backend sym => sym -> GenValue sym +foldlV sym = + ilam $ \_n -> + tlam $ \_a -> + tlam $ \_b -> + lam $ \f -> pure $ + lam $ \z -> pure $ + lam $ \v -> + v >>= \case + VSeq n m -> go0 f z (enumerateSeqMap n m) + VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym =<< wv) + _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"] + where + go0 _f a [] = a + go0 f a bs = + do f' <- fromVFun <$> f + go1 f' a bs + + go1 _f a [] = a + go1 f a (b:bs) = + do f' <- fromVFun <$> (f a) + go1 f (f' b) bs + +foldl'V :: Backend sym => sym -> GenValue sym +foldl'V sym = + ilam $ \_n -> + tlam $ \_a -> + tlam $ \_b -> + lam $ \f -> pure $ + lam $ \z -> pure $ + lam $ \v -> + v >>= \case + VSeq n m -> go0 f z (enumerateSeqMap n m) + VWord _n wv -> go0 f z . map (pure . VBit) =<< (enumerateWordValue sym =<< wv) + _ -> panic "Cryptol.Eval.Generic.foldlV" ["Expected finite sequence"] + where + go0 _f a [] = a + go0 f a bs = + do f' <- fromVFun <$> f + a' <- a + go1 f' a' bs + + go1 _f a [] = pure a + go1 f a (b:bs) = + do f' <- fromVFun <$> (f (pure a)) + a' <- f' b + go1 f a' bs + -------------------------------------------------------------------------------- -- Experimental parallel primitives diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index ecc5e6998..1cb2596af 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -494,6 +494,9 @@ primTable = let sym = SBV in , ("fromZ" , fromZV sym) + , ("foldl" , foldlV sym) + , ("foldl'" , foldl'V sym) + , ("parmap" , parmapV sym) -- {at,len} (fin len) => [len][8] -> at diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index 262ceeb9e..f3c32d1d1 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -157,6 +157,9 @@ primTable w4sym = let sym = What4 w4sym in -- Misc + , ("foldl" , foldlV sym) + , ("foldl'" , foldl'V sym) + , ("parmap" , parmapV sym) , ("fromZ" , fromZV sym) diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index d978cbe6d..2cbcf37b8 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,14 +3,14 @@ Loading module Cryptol Loading module Main [error] at T146.cry:1:18--6:10: - The type ?fv`959 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`943 + The type ?fv`952 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`936 where - ?fv`959 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`943 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`952 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 + fv`936 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: - The type ?fv`961 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`943 + The type ?fv`954 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`936 where - ?fv`961 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`943 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`954 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 + fv`936 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 421b572bf..726f76a1d 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -129,7 +129,9 @@ Symbols False : Bit floor : {a} (Round a) => a -> Integer foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b fraction : {m, n, r, a} (FLiteral m n r a) => a fromInteger : {a} (Ring a) => Integer -> a fromThenTo : diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index b00af3cc8..937a207ba 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`940 == 1 + • n`933 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`940 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`933 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index 7803526dc..8f59c99dd 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`940 + • k == n`933 arising from matching types at issue723.cry:7:17--7:19 where - n`940 is signature variable 'n' at issue723.cry:1:6--1:7 + n`933 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index 63f3ff374..987c2c97b 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Z ?n`1180) + • Logic (Z ?n`1173) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1180 is type wildcard (_) at :1:15--1:16 + ?n`1173 is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -50,14 +50,14 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Float ?n`1194 ?n`1195) + • Logic (Float ?n`1187 ?n`1188) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1194 is type wildcard (_) at :1:19--1:20 - ?n`1195 is type wildcard (_) at :1:21--1:22 + ?n`1187 is type wildcard (_) at :1:19--1:20 + ?n`1188 is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: Unsolvable constraints: @@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Z ?n`1218) + • Integral (Z ?n`1211) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1218' is not an integral type. + • Reason: Type 'Z ?n`1211' is not an integral type. where - ?n`1218 is type wildcard (_) at :1:8--1:9 + ?n`1211 is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1221 -> ?a`1222) + • Integral (?a`1214 -> ?a`1215) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1221 -> ?a`1222' is not an integral type. + • Reason: Type '?a`1214 -> ?a`1215' is not an integral type. where - ?a`1221 is type wildcard (_) at :1:7--1:8 - ?a`1222 is type wildcard (_) at :1:12--1:13 + ?a`1214 is type wildcard (_) at :1:7--1:8 + ?a`1215 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: Unsolvable constraints: @@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1221, ?a`1222) + • Integral (?a`1214, ?a`1215) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1221, ?a`1222)' is not an integral type. + • Reason: Type '(?a`1214, ?a`1215)' is not an integral type. where - ?a`1221 is type wildcard (_) at :1:7--1:8 - ?a`1222 is type wildcard (_) at :1:10--1:11 + ?a`1214 is type wildcard (_) at :1:7--1:8 + ?a`1215 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: Unsolvable constraints: @@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral {x : ?a`1221, y : ?a`1222} + • Integral {x : ?a`1214, y : ?a`1215} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1221, y : ?a`1222}' is not an integral type. + • Reason: Type '{x : ?a`1214, y : ?a`1215}' is not an integral type. where - ?a`1221 is type wildcard (_) at :1:11--1:12 - ?a`1222 is type wildcard (_) at :1:18--1:19 + ?a`1214 is type wildcard (_) at :1:11--1:12 + ?a`1215 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1221 ?n`1222) + • Integral (Float ?n`1214 ?n`1215) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1221 ?n`1222' is not an integral type. + • Reason: Type 'Float ?n`1214 ?n`1215' is not an integral type. where - ?n`1221 is type wildcard (_) at :1:12--1:13 - ?n`1222 is type wildcard (_) at :1:14--1:15 + ?n`1214 is type wildcard (_) at :1:12--1:13 + ?n`1215 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -187,35 +187,35 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (Z ?n`1222) + • Field (Z ?n`1215) arising from use of expression recip at :1:1--1:6 • Reason: Type 'Z' does not support field operations. where - ?n`1222 is type wildcard (_) at :1:10--1:11 + ?n`1215 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Field ([?n`1222]?a`1223) + • Field ([?n`1215]?a`1216) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1222 is type wildcard (_) at :1:9--1:10 - ?a`1223 is type wildcard (_) at :1:11--1:12 + ?n`1215 is type wildcard (_) at :1:9--1:10 + ?a`1216 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1222 -> ?a`1223) + • Field (?a`1215 -> ?a`1216) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1222 is type wildcard (_) at :1:9--1:10 - ?a`1223 is type wildcard (_) at :1:14--1:15 + ?a`1215 is type wildcard (_) at :1:9--1:10 + ?a`1216 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -227,14 +227,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1222, ?a`1223) + • Field (?a`1215, ?a`1216) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1222 is type wildcard (_) at :1:9--1:10 - ?a`1223 is type wildcard (_) at :1:12--1:13 + ?a`1215 is type wildcard (_) at :1:9--1:10 + ?a`1216 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -246,14 +246,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field {x : ?a`1222, y : ?a`1223} + • Field {x : ?a`1215, y : ?a`1216} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1222 is type wildcard (_) at :1:13--1:14 - ?a`1223 is type wildcard (_) at :1:20--1:21 + ?a`1215 is type wildcard (_) at :1:13--1:14 + ?a`1216 is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m @@ -276,35 +276,35 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (Z ?n`1226) + • Round (Z ?n`1219) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1226 is type wildcard (_) at :1:10--1:11 + ?n`1219 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1226]?a`1227) + • Round ([?n`1219]?a`1220) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1226 is type wildcard (_) at :1:9--1:10 - ?a`1227 is type wildcard (_) at :1:11--1:12 + ?n`1219 is type wildcard (_) at :1:9--1:10 + ?a`1220 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1226 -> ?a`1227) + • Round (?a`1219 -> ?a`1220) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1226 is type wildcard (_) at :1:9--1:10 - ?a`1227 is type wildcard (_) at :1:14--1:15 + ?a`1219 is type wildcard (_) at :1:9--1:10 + ?a`1220 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -316,14 +316,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1226, ?a`1227) + • Round (?a`1219, ?a`1220) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1226 is type wildcard (_) at :1:9--1:10 - ?a`1227 is type wildcard (_) at :1:12--1:13 + ?a`1219 is type wildcard (_) at :1:9--1:10 + ?a`1220 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -335,14 +335,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round {x : ?a`1226, y : ?a`1227} + • Round {x : ?a`1219, y : ?a`1220} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1226 is type wildcard (_) at :1:13--1:14 - ?a`1227 is type wildcard (_) at :1:20--1:21 + ?a`1219 is type wildcard (_) at :1:13--1:14 + ?a`1220 is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -352,14 +352,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • Eq (?a`1237 -> ?a`1238) + • Eq (?a`1230 -> ?a`1231) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1237 is type wildcard (_) at :1:8--1:9 - ?a`1238 is type wildcard (_) at :1:13--1:14 + ?a`1230 is type wildcard (_) at :1:8--1:9 + ?a`1231 is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -373,25 +373,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (Z ?n`1251) + • Cmp (Z ?n`1244) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1251 is type wildcard (_) at :1:8--1:9 + ?n`1244 is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (?a`1254 -> ?a`1255) + • Cmp (?a`1247 -> ?a`1248) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1254 is type wildcard (_) at :1:7--1:8 - ?a`1255 is type wildcard (_) at :1:12--1:13 + ?a`1247 is type wildcard (_) at :1:7--1:8 + ?a`1248 is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -426,25 +426,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Z ?n`1265) + • SignedCmp (Z ?n`1258) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1265 is type wildcard (_) at :1:9--1:10 + ?n`1258 is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (?a`1268 -> ?a`1269) + • SignedCmp (?a`1261 -> ?a`1262) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1268 is type wildcard (_) at :1:8--1:9 - ?a`1269 is type wildcard (_) at :1:13--1:14 + ?a`1261 is type wildcard (_) at :1:8--1:9 + ?a`1262 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,24 +454,24 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1276 ?n`1277) + • SignedCmp (Float ?n`1269 ?n`1270) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1276 is type wildcard (_) at :1:13--1:14 - ?n`1277 is type wildcard (_) at :1:15--1:16 + ?n`1269 is type wildcard (_) at :1:13--1:14 + ?n`1270 is type wildcard (_) at :1:15--1:16 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 Bit + • Literal ?val`1269 Bit arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type 'Bit' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1269 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Ambiguous numeric type: type argument 'val' of 'number' @@ -484,60 +484,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1283 (?a`1284 -> ?a`1285) + • Literal ?val`1276 (?a`1277 -> ?a`1278) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1284 -> ?a`1285' does not support integer literals. + • Reason: Type '?a`1277 -> ?a`1278' does not support integer literals. where - ?val`1283 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1284 is type wildcard (_) at :1:15--1:16 - ?a`1285 is type wildcard (_) at :1:20--1:21 + ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1277 is type wildcard (_) at :1:15--1:16 + ?a`1278 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1283 () + • Literal ?val`1276 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1283 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1283 (?a`1284, ?a`1285) + • Literal ?val`1276 (?a`1277, ?a`1278) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1284, ?a`1285)' does not support integer literals. + • Reason: Type '(?a`1277, ?a`1278)' does not support integer literals. where - ?val`1283 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1284 is type wildcard (_) at :1:16--1:17 - ?a`1285 is type wildcard (_) at :1:19--1:20 + ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1277 is type wildcard (_) at :1:16--1:17 + ?a`1278 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1283 {} + • Literal ?val`1276 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1283 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1283 {x : ?a`1284, y : ?a`1285} + • Literal ?val`1276 {x : ?a`1277, y : ?a`1278} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1284, - y : ?a`1285}' does not support integer literals. + • Reason: Type '{x : ?a`1277, + y : ?a`1278}' does not support integer literals. where - ?val`1283 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1284 is type wildcard (_) at :1:20--1:21 - ?a`1285 is type wildcard (_) at :1:27--1:28 + ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1277 is type wildcard (_) at :1:20--1:21 + ?a`1278 is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i From 6feeafa74f4608e2ffd17cccab4caf7416fa20ef Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 2 Sep 2020 13:07:50 -0700 Subject: [PATCH 2/6] Add `seq` and `deepseq` primitives, and rewrite some prelude functions to use stricter variants. Add an `Eq` constraint to `parmap` to mirror the restriction on `deepseq`. --- lib/Cryptol.cry | 51 +++++++- src/Cryptol/Eval/Concrete.hs | 16 +++ src/Cryptol/Eval/SBV.hs | 16 +++ src/Cryptol/Eval/What4.hs | 16 +++ tests/issues/T146.icry.stdout | 16 +-- tests/issues/issue226.icry.stdout | 6 +- tests/issues/issue290v2.icry.stdout | 4 +- tests/issues/issue723.icry.stdout | 4 +- tests/regression/instance.icry.stdout | 180 +++++++++++++------------- 9 files changed, 201 insertions(+), 108 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 5bfaca22d..a16be1f62 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -928,14 +928,46 @@ pmod x y = if y == 0 then 0/0 else last zs /** * Parallel map. The given function is applied to each element in the * given finite seqeuence, and the results are computed in parallel. + * The values in the resulting sequence are reduced to normal form, + * as is done with the deepseq operation. + * + * The Eq constraint restricts this operation to types + * where reduction to normal form makes sense. * * This function is experimental. */ -primitive parmap : {a, b, n} (fin n) => (a -> b) -> [n]a -> [n]b +primitive parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b // Utility operations ----------------------------------------------------------------- +/** + * A strictness-increasing operation. The first operand + * is reduced to weak head normal form before returning + * the second argument. + */ +primitive seq : {a, b} a -> b -> b + +/** + * A strictness-increasing operation. The first operand + * is reduced to normal form before evaluating the second + * argument. Unlike seq, this operation will fully evaluate + * all structural and sequence types down to base types. + * + * The Eq constraint restricts this operation to types + * where reduction to normal form makes sense. + */ +primitive deepseq : {a, b} Eq a => a -> b -> b + +/** + * Reduce to normal form. + * + * The Eq constraint restricts this operation to types + * where reduction to normal form makes sense. + */ +rnf : {a} Eq a => a -> a +rnf x = deepseq x x + /** * Raise a run-time error with the given message. * This function can be called at any type. @@ -1009,13 +1041,13 @@ or xs = zero != xs * Conjunction after applying a predicate to all elements. */ all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit -all f xs = and (map f xs) +all f xs = foldl' (/\) True (map f xs) /** * Disjunction after applying a predicate to all elements. */ any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit -any f xs = or (map f xs) +any f xs = foldl' (\/) False (map f xs) /** * Map a function over a sequence. @@ -1032,6 +1064,7 @@ primitive foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a /** * Functional left fold, with strict evaluation of the accumulator value. + * The accumulator is reduced to weak head normal form at each step. * * foldl' (+) 0 [1,2,3] = ((0 + 1) + 2) + 3 */ @@ -1048,6 +1081,7 @@ foldr f acc xs = foldl g acc (reverse xs) /** * Functional right fold, with strict evaluation of the accumulator value. + * The accumulator is reduced to weak head normal form at each step. * * foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3)) */ @@ -1055,12 +1089,19 @@ foldr' : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b foldr' f acc xs = foldl' g acc (reverse xs) where g b a = f a b - /** * Compute the sum of the values in the sequence. */ sum : {n, a} (fin n, Ring a) => [n]a -> a -sum xs = foldl (+) (fromInteger 0) xs +sum xs = foldl' (+) (fromInteger 0) xs + + +/** + * Compute the product of the values in the sequence. + */ +product : {n, a} (fin n, Ring a) => [n]a -> a +product xs = foldl' (*) (fromInteger 1) xs + /** * Scan left is like a foldl that also emits the intermediate values. diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index a1795e72d..fb794f4df 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -305,6 +305,22 @@ primTable eOpts = let sym = Concrete in foldl'V sym) + , ("seq" , {-# SCC "Prelude::seq" #-} + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- x + y) + + , ("deepseq" , {-# SCC "Prelude::deepseq" #-} + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- forceValue =<< x + y) + , ("parmap" , {-# SCC "Prelude::parmap" #-} parmapV sym) diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index 1cb2596af..4d199d625 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -497,6 +497,22 @@ primTable = let sym = SBV in , ("foldl" , foldlV sym) , ("foldl'" , foldl'V sym) + , ("seq" , + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- x + y) + + , ("deepseq" , + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- forceValue =<< x + y) + , ("parmap" , parmapV sym) -- {at,len} (fin len) => [len][8] -> at diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index f3c32d1d1..1f3b51e8d 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -160,6 +160,22 @@ primTable w4sym = let sym = What4 w4sym in , ("foldl" , foldlV sym) , ("foldl'" , foldl'V sym) + , ("seq" , + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- x + y) + + , ("deepseq" , + tlam $ \_a -> + tlam $ \_b -> + lam $ \x -> pure $ + lam $ \y -> + do _ <- forceValue =<< x + y) + , ("parmap" , parmapV sym) , ("fromZ" , fromZV sym) diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 2cbcf37b8..ba9539246 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,14 +3,14 @@ Loading module Cryptol Loading module Main [error] at T146.cry:1:18--6:10: - The type ?fv`952 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`936 + The type ?fv`982 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`966 where - ?fv`952 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`936 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`982 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 + fv`966 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: - The type ?fv`954 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`936 + The type ?fv`984 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`966 where - ?fv`954 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`936 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`984 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 + fv`966 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 726f76a1d..a53cc4c5b 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -122,6 +122,7 @@ Symbols ceiling : {a} (Round a) => a -> Integer complement : {a} (Logic a) => a -> a curry : {a, b, c} ((a, b) -> c) -> a -> b -> c + deepseq : {a, b} (Eq a) => a -> b -> b demote : {val, rep} (Literal val rep) => rep drop : {front, back, a} (fin front) => [front + back]a -> [back]a elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit @@ -164,22 +165,25 @@ Symbols negate : {a} (Ring a) => a -> a number : {val, rep} (Literal val rep) => rep or : {n} (fin n) => [n] -> Bit - parmap : {a, b, n} (fin n) => (a -> b) -> [n]a -> [n]b + parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u] pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] + product : {n, a} (fin n, Ring a) => [n]a -> a random : {a} [256] -> a ratio : Integer -> Integer -> Rational recip : {a} (Field a) => a -> a repeat : {n, a} a -> [n]a reverse : {n, a} (fin n) => [n]a -> [n]a + rnf : {a} (Eq a) => a -> a roundAway : {a} (Round a) => a -> Integer roundToEven : {a} (Round a) => a -> Integer sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit + seq : {a, b} a -> b -> b sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 937a207ba..60a77563b 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`933 == 1 + • n`963 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`933 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`963 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index 8f59c99dd..6e753d463 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`933 + • k == n`963 arising from matching types at issue723.cry:7:17--7:19 where - n`933 is signature variable 'n' at issue723.cry:1:6--1:7 + n`963 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index 987c2c97b..c61947d04 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Z ?n`1173) + • Logic (Z ?n`1203) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1173 is type wildcard (_) at :1:15--1:16 + ?n`1203 is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -50,14 +50,14 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Float ?n`1187 ?n`1188) + • Logic (Float ?n`1217 ?n`1218) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1187 is type wildcard (_) at :1:19--1:20 - ?n`1188 is type wildcard (_) at :1:21--1:22 + ?n`1217 is type wildcard (_) at :1:19--1:20 + ?n`1218 is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: Unsolvable constraints: @@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Z ?n`1211) + • Integral (Z ?n`1241) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1211' is not an integral type. + • Reason: Type 'Z ?n`1241' is not an integral type. where - ?n`1211 is type wildcard (_) at :1:8--1:9 + ?n`1241 is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1214 -> ?a`1215) + • Integral (?a`1244 -> ?a`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1214 -> ?a`1215' is not an integral type. + • Reason: Type '?a`1244 -> ?a`1245' is not an integral type. where - ?a`1214 is type wildcard (_) at :1:7--1:8 - ?a`1215 is type wildcard (_) at :1:12--1:13 + ?a`1244 is type wildcard (_) at :1:7--1:8 + ?a`1245 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: Unsolvable constraints: @@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1214, ?a`1215) + • Integral (?a`1244, ?a`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1214, ?a`1215)' is not an integral type. + • Reason: Type '(?a`1244, ?a`1245)' is not an integral type. where - ?a`1214 is type wildcard (_) at :1:7--1:8 - ?a`1215 is type wildcard (_) at :1:10--1:11 + ?a`1244 is type wildcard (_) at :1:7--1:8 + ?a`1245 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: Unsolvable constraints: @@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral {x : ?a`1214, y : ?a`1215} + • Integral {x : ?a`1244, y : ?a`1245} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1214, y : ?a`1215}' is not an integral type. + • Reason: Type '{x : ?a`1244, y : ?a`1245}' is not an integral type. where - ?a`1214 is type wildcard (_) at :1:11--1:12 - ?a`1215 is type wildcard (_) at :1:18--1:19 + ?a`1244 is type wildcard (_) at :1:11--1:12 + ?a`1245 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1214 ?n`1215) + • Integral (Float ?n`1244 ?n`1245) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1214 ?n`1215' is not an integral type. + • Reason: Type 'Float ?n`1244 ?n`1245' is not an integral type. where - ?n`1214 is type wildcard (_) at :1:12--1:13 - ?n`1215 is type wildcard (_) at :1:14--1:15 + ?n`1244 is type wildcard (_) at :1:12--1:13 + ?n`1245 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -187,35 +187,35 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (Z ?n`1215) + • Field (Z ?n`1245) arising from use of expression recip at :1:1--1:6 • Reason: Type 'Z' does not support field operations. where - ?n`1215 is type wildcard (_) at :1:10--1:11 + ?n`1245 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Field ([?n`1215]?a`1216) + • Field ([?n`1245]?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1215 is type wildcard (_) at :1:9--1:10 - ?a`1216 is type wildcard (_) at :1:11--1:12 + ?n`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1215 -> ?a`1216) + • Field (?a`1245 -> ?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1215 is type wildcard (_) at :1:9--1:10 - ?a`1216 is type wildcard (_) at :1:14--1:15 + ?a`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -227,14 +227,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1215, ?a`1216) + • Field (?a`1245, ?a`1246) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1215 is type wildcard (_) at :1:9--1:10 - ?a`1216 is type wildcard (_) at :1:12--1:13 + ?a`1245 is type wildcard (_) at :1:9--1:10 + ?a`1246 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -246,14 +246,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field {x : ?a`1215, y : ?a`1216} + • Field {x : ?a`1245, y : ?a`1246} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1215 is type wildcard (_) at :1:13--1:14 - ?a`1216 is type wildcard (_) at :1:20--1:21 + ?a`1245 is type wildcard (_) at :1:13--1:14 + ?a`1246 is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m @@ -276,35 +276,35 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (Z ?n`1219) + • Round (Z ?n`1249) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1219 is type wildcard (_) at :1:10--1:11 + ?n`1249 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1219]?a`1220) + • Round ([?n`1249]?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1219 is type wildcard (_) at :1:9--1:10 - ?a`1220 is type wildcard (_) at :1:11--1:12 + ?n`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1219 -> ?a`1220) + • Round (?a`1249 -> ?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1219 is type wildcard (_) at :1:9--1:10 - ?a`1220 is type wildcard (_) at :1:14--1:15 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -316,14 +316,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1219, ?a`1220) + • Round (?a`1249, ?a`1250) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1219 is type wildcard (_) at :1:9--1:10 - ?a`1220 is type wildcard (_) at :1:12--1:13 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -335,14 +335,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round {x : ?a`1219, y : ?a`1220} + • Round {x : ?a`1249, y : ?a`1250} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1219 is type wildcard (_) at :1:13--1:14 - ?a`1220 is type wildcard (_) at :1:20--1:21 + ?a`1249 is type wildcard (_) at :1:13--1:14 + ?a`1250 is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -352,14 +352,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • Eq (?a`1230 -> ?a`1231) + • Eq (?a`1260 -> ?a`1261) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1230 is type wildcard (_) at :1:8--1:9 - ?a`1231 is type wildcard (_) at :1:13--1:14 + ?a`1260 is type wildcard (_) at :1:8--1:9 + ?a`1261 is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -373,25 +373,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (Z ?n`1244) + • Cmp (Z ?n`1274) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1244 is type wildcard (_) at :1:8--1:9 + ?n`1274 is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (?a`1247 -> ?a`1248) + • Cmp (?a`1277 -> ?a`1278) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1247 is type wildcard (_) at :1:7--1:8 - ?a`1248 is type wildcard (_) at :1:12--1:13 + ?a`1277 is type wildcard (_) at :1:7--1:8 + ?a`1278 is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -426,25 +426,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Z ?n`1258) + • SignedCmp (Z ?n`1288) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1258 is type wildcard (_) at :1:9--1:10 + ?n`1288 is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (?a`1261 -> ?a`1262) + • SignedCmp (?a`1291 -> ?a`1292) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1261 is type wildcard (_) at :1:8--1:9 - ?a`1262 is type wildcard (_) at :1:13--1:14 + ?a`1291 is type wildcard (_) at :1:8--1:9 + ?a`1292 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,24 +454,24 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1269 ?n`1270) + • SignedCmp (Float ?n`1299 ?n`1300) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1269 is type wildcard (_) at :1:13--1:14 - ?n`1270 is type wildcard (_) at :1:15--1:16 + ?n`1299 is type wildcard (_) at :1:13--1:14 + ?n`1300 is type wildcard (_) at :1:15--1:16 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1269 Bit + • Literal ?val`1299 Bit arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type 'Bit' does not support integer literals. where - ?val`1269 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1299 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Ambiguous numeric type: type argument 'val' of 'number' @@ -484,60 +484,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 (?a`1277 -> ?a`1278) + • Literal ?val`1306 (?a`1307 -> ?a`1308) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1277 -> ?a`1278' does not support integer literals. + • Reason: Type '?a`1307 -> ?a`1308' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1277 is type wildcard (_) at :1:15--1:16 - ?a`1278 is type wildcard (_) at :1:20--1:21 + ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1307 is type wildcard (_) at :1:15--1:16 + ?a`1308 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 () + • Literal ?val`1306 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 (?a`1277, ?a`1278) + • Literal ?val`1306 (?a`1307, ?a`1308) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1277, ?a`1278)' does not support integer literals. + • Reason: Type '(?a`1307, ?a`1308)' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1277 is type wildcard (_) at :1:16--1:17 - ?a`1278 is type wildcard (_) at :1:19--1:20 + ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1307 is type wildcard (_) at :1:16--1:17 + ?a`1308 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 {} + • Literal ?val`1306 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1276 {x : ?a`1277, y : ?a`1278} + • Literal ?val`1306 {x : ?a`1307, y : ?a`1308} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1277, - y : ?a`1278}' does not support integer literals. + • Reason: Type '{x : ?a`1307, + y : ?a`1308}' does not support integer literals. where - ?val`1276 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1277 is type wildcard (_) at :1:20--1:21 - ?a`1278 is type wildcard (_) at :1:27--1:28 + ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1307 is type wildcard (_) at :1:20--1:21 + ?a`1308 is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i From d70ac55b5dbe2cc98d9976369b536bb76b51cf62 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 2 Sep 2020 14:59:05 -0700 Subject: [PATCH 3/6] Force `parmap` to have `deepseq` behavior on each element of the sequence. --- src/Cryptol/Eval/Generic.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 9a82b5622..d261bd7c5 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -1990,7 +1990,12 @@ sparkParMap :: SeqMap sym -> SEval sym (SeqMap sym) sparkParMap sym f n m = - finiteSeqMap sym <$> mapM (sSpark sym . f) (enumerateSeqMap n m) + finiteSeqMap sym <$> mapM (sSpark sym . g) (enumerateSeqMap n m) + where + g x = + do z <- sDelay sym Nothing (f x) + forceValue =<< z + z -------------------------------------------------------------------------------- -- Floating Point Operations From 858e20c752fa334843aae6e53bb74fef2e254a42 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 3 Sep 2020 10:40:43 -0700 Subject: [PATCH 4/6] Minor cleanup. Remove some stray changes that snuck in. --- src/Cryptol/Eval/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/Eval/Monad.hs b/src/Cryptol/Eval/Monad.hs index 0991ec01b..219554fec 100644 --- a/src/Cryptol/Eval/Monad.hs +++ b/src/Cryptol/Eval/Monad.hs @@ -250,7 +250,7 @@ unDelay tv = case res of -- In this case, we claim the thunk. Update the state to indicate -- that we are working on it. - Unforced nm backup -> writeTVar tv (UnderEvaluation tid backup) + Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup) -- In this case, the thunk is already being evaluated. If it is -- under evaluation by this thread, we have to run the backup computation, From de3bcd72873d3e6bc3c7065c5efe5dd5a95d3eda Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 14 Sep 2020 11:03:58 -0700 Subject: [PATCH 5/6] Update rational properties regression test to use What4 backend. This works around SBV8.7/CVC1.7 compatiblity issues, and has a side effect of completing the QOrdCompatible proof, which was previously returning UNKNOWN. --- tests/regression/rational_properties.icry | 6 ++---- tests/regression/rational_properties.icry.stdout | 10 +++------- 2 files changed, 5 insertions(+), 11 deletions(-) diff --git a/tests/regression/rational_properties.icry b/tests/regression/rational_properties.icry index a0356d3c6..8d8699c9c 100644 --- a/tests/regression/rational_properties.icry +++ b/tests/regression/rational_properties.icry @@ -2,10 +2,8 @@ :check -:set prover=cvc4 +:set prover=w4-cvc4 :prove -:set prover=z3 - -:prove Qdense +:set prover=w4-z3 :prove QordTrans diff --git a/tests/regression/rational_properties.icry.stdout b/tests/regression/rational_properties.icry.stdout index 2fbd8c41b..bfc35cd3d 100644 --- a/tests/regression/rational_properties.icry.stdout +++ b/tests/regression/rational_properties.icry.stdout @@ -74,8 +74,7 @@ Testing... Passed 100 tests. :prove QordEquiv2 Q.E.D. :prove QordTrans - Unknown. - Reason: incomplete + Solver returned UNKNOWN :prove QordIrreflexive Q.E.D. :prove QordExclusive @@ -83,13 +82,11 @@ Testing... Passed 100 tests. :prove Qtrichotomy Q.E.D. :prove QordCompatible - Unknown. - Reason: incomplete + Q.E.D. :prove QordPositive Q.E.D. :prove Qdense - Unknown. - Reason: incomplete + Q.E.D. :prove intDivDown Q.E.D. :prove floorCorrect1 @@ -101,4 +98,3 @@ Testing... Passed 100 tests. :prove ceilingCorrect2 Q.E.D. Q.E.D. -Q.E.D. From e79786edb02af0ca7333a7b15acf3bb01a96f76f Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 14 Sep 2020 12:41:38 -0700 Subject: [PATCH 6/6] Remove `seq` and change `foldl'` to always perform normal-form evaluation. The extra flexability aforded by WHNF evaluation is mostly just confusing, I think. --- lib/Cryptol.cry | 21 +-- src/Cryptol/Eval/Concrete.hs | 9 -- src/Cryptol/Eval/Generic.hs | 10 +- src/Cryptol/Eval/SBV.hs | 8 -- src/Cryptol/Eval/What4.hs | 8 -- tests/issues/T146.icry.stdout | 16 +-- tests/issues/issue226.icry.stdout | 9 +- tests/issues/issue290v2.icry.stdout | 4 +- tests/issues/issue723.icry.stdout | 4 +- tests/regression/instance.icry.stdout | 180 +++++++++++++------------- 10 files changed, 119 insertions(+), 150 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index a16be1f62..2ea57c632 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -941,18 +941,10 @@ primitive parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b // Utility operations ----------------------------------------------------------------- -/** - * A strictness-increasing operation. The first operand - * is reduced to weak head normal form before returning - * the second argument. - */ -primitive seq : {a, b} a -> b -> b - /** * A strictness-increasing operation. The first operand * is reduced to normal form before evaluating the second - * argument. Unlike seq, this operation will fully evaluate - * all structural and sequence types down to base types. + * argument. * * The Eq constraint restricts this operation to types * where reduction to normal form makes sense. @@ -1064,11 +1056,12 @@ primitive foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a /** * Functional left fold, with strict evaluation of the accumulator value. - * The accumulator is reduced to weak head normal form at each step. + * The accumulator is reduced to normal form at each step. The Eq constraint + * restricts the accumulator to types where reduction to normal form makes sense. * * foldl' (+) 0 [1,2,3] = ((0 + 1) + 2) + 3 */ -primitive foldl' : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a +primitive foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a /** * Functional right fold. @@ -1085,21 +1078,21 @@ foldr f acc xs = foldl g acc (reverse xs) * * foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3)) */ -foldr' : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b +foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b foldr' f acc xs = foldl' g acc (reverse xs) where g b a = f a b /** * Compute the sum of the values in the sequence. */ -sum : {n, a} (fin n, Ring a) => [n]a -> a +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, Ring a) => [n]a -> a +product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a product xs = foldl' (*) (fromInteger 1) xs diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs index fb794f4df..2a0a2731f 100644 --- a/src/Cryptol/Eval/Concrete.hs +++ b/src/Cryptol/Eval/Concrete.hs @@ -304,15 +304,6 @@ primTable eOpts = let sym = Concrete in , ("foldl'" , {-# SCC "Prelude::foldl'" #-} foldl'V sym) - - , ("seq" , {-# SCC "Prelude::seq" #-} - tlam $ \_a -> - tlam $ \_b -> - lam $ \x -> pure $ - lam $ \y -> - do _ <- x - y) - , ("deepseq" , {-# SCC "Prelude::deepseq" #-} tlam $ \_a -> tlam $ \_b -> diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index d261bd7c5..f25cec699 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -1950,13 +1950,15 @@ foldl'V sym = go0 _f a [] = a go0 f a bs = do f' <- fromVFun <$> f - a' <- a + a' <- sDelay sym Nothing a + forceValue =<< a' go1 f' a' bs - go1 _f a [] = pure a + go1 _f a [] = a go1 f a (b:bs) = - do f' <- fromVFun <$> (f (pure a)) - a' <- f' b + do f' <- fromVFun <$> (f a) + a' <- sDelay sym Nothing (f' b) + forceValue =<< a' go1 f a' bs -------------------------------------------------------------------------------- diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs index 4d199d625..93c859b14 100644 --- a/src/Cryptol/Eval/SBV.hs +++ b/src/Cryptol/Eval/SBV.hs @@ -497,14 +497,6 @@ primTable = let sym = SBV in , ("foldl" , foldlV sym) , ("foldl'" , foldl'V sym) - , ("seq" , - tlam $ \_a -> - tlam $ \_b -> - lam $ \x -> pure $ - lam $ \y -> - do _ <- x - y) - , ("deepseq" , tlam $ \_a -> tlam $ \_b -> diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index 1f3b51e8d..2183471dd 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -160,14 +160,6 @@ primTable w4sym = let sym = What4 w4sym in , ("foldl" , foldlV sym) , ("foldl'" , foldl'V sym) - , ("seq" , - tlam $ \_a -> - tlam $ \_b -> - lam $ \x -> pure $ - lam $ \y -> - do _ <- x - y) - , ("deepseq" , tlam $ \_a -> tlam $ \_b -> diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index ba9539246..1daea171a 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,14 +3,14 @@ Loading module Cryptol Loading module Main [error] at T146.cry:1:18--6:10: - The type ?fv`982 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`966 + The type ?fv`980 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`964 where - ?fv`982 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`966 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`980 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 + fv`964 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: - The type ?fv`984 is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`966 + The type ?fv`982 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`964 where - ?fv`984 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`966 is signature variable 'fv' at T146.cry:11:10--11:12 + ?fv`982 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 + fv`964 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index a53cc4c5b..497e0c6df 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -130,9 +130,9 @@ Symbols False : Bit floor : {a} (Round a) => a -> Integer foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a - foldl' : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a + foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b - foldr' : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b + foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b fraction : {m, n, r, a} (FLiteral m n r a) => a fromInteger : {a} (Ring a) => Integer -> a fromThenTo : @@ -170,7 +170,7 @@ Symbols pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v] pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)] - product : {n, a} (fin n, Ring a) => [n]a -> a + product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a random : {a} [256] -> a ratio : Integer -> Integer -> Rational recip : {a} (Field a) => a -> a @@ -183,14 +183,13 @@ Symbols scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit - seq : {a, b} a -> b -> b sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m] split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a splitAt : {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a) - sum : {n, a} (fin n, Ring a) => [n]a -> a + sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a True : Bit tail : {n, a} [1 + n]a -> [n]a take : {front, back, a} (fin front) => [front + back]a -> [front]a diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 60a77563b..f75f9157c 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`963 == 1 + • n`961 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`963 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`961 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index 6e753d463..05985f1d3 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`963 + • k == n`961 arising from matching types at issue723.cry:7:17--7:19 where - n`963 is signature variable 'n' at issue723.cry:1:6--1:7 + n`961 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index c61947d04..33e7391b6 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Z ?n`1203) + • Logic (Z ?n`1201) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1203 is type wildcard (_) at :1:15--1:16 + ?n`1201 is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -50,14 +50,14 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Float ?n`1217 ?n`1218) + • Logic (Float ?n`1215 ?n`1216) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1217 is type wildcard (_) at :1:19--1:20 - ?n`1218 is type wildcard (_) at :1:21--1:22 + ?n`1215 is type wildcard (_) at :1:19--1:20 + ?n`1216 is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: Unsolvable constraints: @@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Z ?n`1241) + • Integral (Z ?n`1239) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1241' is not an integral type. + • Reason: Type 'Z ?n`1239' is not an integral type. where - ?n`1241 is type wildcard (_) at :1:8--1:9 + ?n`1239 is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1244 -> ?a`1245) + • Integral (?a`1242 -> ?a`1243) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1244 -> ?a`1245' is not an integral type. + • Reason: Type '?a`1242 -> ?a`1243' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:7--1:8 - ?a`1245 is type wildcard (_) at :1:12--1:13 + ?a`1242 is type wildcard (_) at :1:7--1:8 + ?a`1243 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: Unsolvable constraints: @@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1244, ?a`1245) + • Integral (?a`1242, ?a`1243) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1244, ?a`1245)' is not an integral type. + • Reason: Type '(?a`1242, ?a`1243)' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:7--1:8 - ?a`1245 is type wildcard (_) at :1:10--1:11 + ?a`1242 is type wildcard (_) at :1:7--1:8 + ?a`1243 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: Unsolvable constraints: @@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral {x : ?a`1244, y : ?a`1245} + • Integral {x : ?a`1242, y : ?a`1243} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1244, y : ?a`1245}' is not an integral type. + • Reason: Type '{x : ?a`1242, y : ?a`1243}' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:11--1:12 - ?a`1245 is type wildcard (_) at :1:18--1:19 + ?a`1242 is type wildcard (_) at :1:11--1:12 + ?a`1243 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1244 ?n`1245) + • Integral (Float ?n`1242 ?n`1243) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1244 ?n`1245' is not an integral type. + • Reason: Type 'Float ?n`1242 ?n`1243' is not an integral type. where - ?n`1244 is type wildcard (_) at :1:12--1:13 - ?n`1245 is type wildcard (_) at :1:14--1:15 + ?n`1242 is type wildcard (_) at :1:12--1:13 + ?n`1243 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -187,35 +187,35 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (Z ?n`1245) + • Field (Z ?n`1243) arising from use of expression recip at :1:1--1:6 • Reason: Type 'Z' does not support field operations. where - ?n`1245 is type wildcard (_) at :1:10--1:11 + ?n`1243 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Field ([?n`1245]?a`1246) + • Field ([?n`1243]?a`1244) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:11--1:12 + ?n`1243 is type wildcard (_) at :1:9--1:10 + ?a`1244 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1245 -> ?a`1246) + • Field (?a`1243 -> ?a`1244) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:14--1:15 + ?a`1243 is type wildcard (_) at :1:9--1:10 + ?a`1244 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -227,14 +227,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1245, ?a`1246) + • Field (?a`1243, ?a`1244) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:12--1:13 + ?a`1243 is type wildcard (_) at :1:9--1:10 + ?a`1244 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -246,14 +246,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field {x : ?a`1245, y : ?a`1246} + • Field {x : ?a`1243, y : ?a`1244} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:13--1:14 - ?a`1246 is type wildcard (_) at :1:20--1:21 + ?a`1243 is type wildcard (_) at :1:13--1:14 + ?a`1244 is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m @@ -276,35 +276,35 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (Z ?n`1249) + • Round (Z ?n`1247) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1249 is type wildcard (_) at :1:10--1:11 + ?n`1247 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1249]?a`1250) + • Round ([?n`1247]?a`1248) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:11--1:12 + ?n`1247 is type wildcard (_) at :1:9--1:10 + ?a`1248 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1249 -> ?a`1250) + • Round (?a`1247 -> ?a`1248) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:14--1:15 + ?a`1247 is type wildcard (_) at :1:9--1:10 + ?a`1248 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -316,14 +316,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1249, ?a`1250) + • Round (?a`1247, ?a`1248) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:12--1:13 + ?a`1247 is type wildcard (_) at :1:9--1:10 + ?a`1248 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -335,14 +335,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round {x : ?a`1249, y : ?a`1250} + • Round {x : ?a`1247, y : ?a`1248} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:13--1:14 - ?a`1250 is type wildcard (_) at :1:20--1:21 + ?a`1247 is type wildcard (_) at :1:13--1:14 + ?a`1248 is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -352,14 +352,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • Eq (?a`1260 -> ?a`1261) + • Eq (?a`1258 -> ?a`1259) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1260 is type wildcard (_) at :1:8--1:9 - ?a`1261 is type wildcard (_) at :1:13--1:14 + ?a`1258 is type wildcard (_) at :1:8--1:9 + ?a`1259 is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -373,25 +373,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (Z ?n`1274) + • Cmp (Z ?n`1272) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1274 is type wildcard (_) at :1:8--1:9 + ?n`1272 is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (?a`1277 -> ?a`1278) + • Cmp (?a`1275 -> ?a`1276) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1277 is type wildcard (_) at :1:7--1:8 - ?a`1278 is type wildcard (_) at :1:12--1:13 + ?a`1275 is type wildcard (_) at :1:7--1:8 + ?a`1276 is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -426,25 +426,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Z ?n`1288) + • SignedCmp (Z ?n`1286) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1288 is type wildcard (_) at :1:9--1:10 + ?n`1286 is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (?a`1291 -> ?a`1292) + • SignedCmp (?a`1289 -> ?a`1290) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1291 is type wildcard (_) at :1:8--1:9 - ?a`1292 is type wildcard (_) at :1:13--1:14 + ?a`1289 is type wildcard (_) at :1:8--1:9 + ?a`1290 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,24 +454,24 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1299 ?n`1300) + • SignedCmp (Float ?n`1297 ?n`1298) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1299 is type wildcard (_) at :1:13--1:14 - ?n`1300 is type wildcard (_) at :1:15--1:16 + ?n`1297 is type wildcard (_) at :1:13--1:14 + ?n`1298 is type wildcard (_) at :1:15--1:16 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1299 Bit + • Literal ?val`1297 Bit arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type 'Bit' does not support integer literals. where - ?val`1299 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1297 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Ambiguous numeric type: type argument 'val' of 'number' @@ -484,60 +484,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1306 (?a`1307 -> ?a`1308) + • Literal ?val`1304 (?a`1305 -> ?a`1306) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1307 -> ?a`1308' does not support integer literals. + • Reason: Type '?a`1305 -> ?a`1306' does not support integer literals. where - ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1307 is type wildcard (_) at :1:15--1:16 - ?a`1308 is type wildcard (_) at :1:20--1:21 + ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1305 is type wildcard (_) at :1:15--1:16 + ?a`1306 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1306 () + • Literal ?val`1304 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1306 (?a`1307, ?a`1308) + • Literal ?val`1304 (?a`1305, ?a`1306) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1307, ?a`1308)' does not support integer literals. + • Reason: Type '(?a`1305, ?a`1306)' does not support integer literals. where - ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1307 is type wildcard (_) at :1:16--1:17 - ?a`1308 is type wildcard (_) at :1:19--1:20 + ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1305 is type wildcard (_) at :1:16--1:17 + ?a`1306 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1306 {} + • Literal ?val`1304 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1306 {x : ?a`1307, y : ?a`1308} + • Literal ?val`1304 {x : ?a`1305, y : ?a`1306} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1307, - y : ?a`1308}' does not support integer literals. + • Reason: Type '{x : ?a`1305, + y : ?a`1306}' does not support integer literals. where - ?val`1306 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1307 is type wildcard (_) at :1:20--1:21 - ?a`1308 is type wildcard (_) at :1:27--1:28 + ?val`1304 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1305 is type wildcard (_) at :1:20--1:21 + ?a`1306 is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i