From d9ea06807ffa8277bed66e13693d4020cdb803d3 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 27 Oct 2023 13:36:18 -0700 Subject: [PATCH 1/3] Fixes #1584 --- src/Cryptol/Eval.hs | 34 ++++++++++++++-------------------- 1 file changed, 14 insertions(+), 20 deletions(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 4b7d7e85d..f3c381b1f 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -53,7 +53,7 @@ import Cryptol.ModuleSystem.Name import Cryptol.Parser.Position import Cryptol.Parser.Selector(ppSelector) import Cryptol.TypeCheck.AST -import Cryptol.TypeCheck.Solver.InfNat(Nat'(..)) +import Cryptol.TypeCheck.Solver.InfNat(Nat'(..),nMul) import Cryptol.Utils.Ident import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP @@ -708,23 +708,23 @@ branchEnvs :: ListEnv sym -> [Match] -> SEval sym (ListEnv sym) -branchEnvs sym env matches = snd <$> foldM (evalMatch sym) (1, env) matches +branchEnvs sym env matches = snd <$> foldM (evalMatch sym) (Nat 1, env) matches {-# SPECIALIZE evalMatch :: (?range :: Range, ConcPrims) => Concrete -> - (Integer, ListEnv Concrete) -> + (Nat', ListEnv Concrete) -> Match -> - SEval Concrete (Integer, ListEnv Concrete) + SEval Concrete (Nat', ListEnv Concrete) #-} -- | Turn a match into the list of environments it represents. evalMatch :: (?range :: Range, EvalPrims sym) => sym -> - (Integer, ListEnv sym) -> + (Nat', ListEnv sym) -> Match -> - SEval sym (Integer, ListEnv sym) + SEval sym (Nat', ListEnv sym) evalMatch sym (lsz, lenv) m = seq lsz $ case m of -- many envs @@ -733,7 +733,7 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of -- Select from a sequence of finite length. This causes us to 'stutter' -- through our previous choices `nLen` times. Nat nLen -> do - vss <- memoMap sym (Nat lsz) $ indexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr + vss <- memoMap sym lsz $ indexSeqMap $ \i -> evalExpr sym (evalListEnv lenv i) expr let stutter xs = \i -> xs (i `div` nLen) let lenv' = lenv { leVars = fmap stutter (leVars lenv) } let vs i = do let (q, r) = i `divMod` nLen @@ -742,27 +742,21 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of VSeq _ xs' -> lookupSeqMap xs' r VStream xs' -> lookupSeqMap xs' r _ -> evalPanic "evalMatch" ["Not a list value"] - return (lsz * nLen, bindVarList n vs lenv') + return (nMul lsz len, bindVarList n vs lenv') - -- Select from a sequence of infinite length. Note that this means we - -- will never need to backtrack into previous branches. Thus, we can convert - -- `leVars` elements of the comprehension environment into `leStatic` elements - -- by selecting out the 0th element. + {- Select from a sequence of infinite length. Note that only the + first generator in a sequence of generators may have infinite length, + so we can just evaluate it once an forall (i.e., it does not change + on each loop iteration, as it may happen in the finite case). -} Inf -> do - let allvars = IntMap.union (fmap (Right . ($ 0)) (leVars lenv)) (leStatic lenv) - let lenv' = lenv { leVars = IntMap.empty - , leStatic = allvars - } - let env = EvalEnv allvars (leTypes lenv) + let env = EvalEnv (leStatic lenv) (leTypes lenv) xs <- evalExpr sym env expr let vs i = case xs of VWord _ w -> VBit <$> indexWordValue sym w i VSeq _ xs' -> lookupSeqMap xs' i VStream xs' -> lookupSeqMap xs' i _ -> evalPanic "evalMatch" ["Not a list value"] - -- Selecting from an infinite list effectively resets the length of the - -- list environment, so return 1 as the length - return (1, bindVarList n vs lenv') + return (Inf, bindVarList n vs lenv) where len = evalNumType (leTypes lenv) l From b8ef2b630a87e0877fe714e2c8a544f14c3531ff Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 30 Oct 2023 09:51:38 -0700 Subject: [PATCH 2/3] Fix a typo --- src/Cryptol/Eval.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index f3c381b1f..a706c2d35 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -746,7 +746,7 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of {- Select from a sequence of infinite length. Note that only the first generator in a sequence of generators may have infinite length, - so we can just evaluate it once an forall (i.e., it does not change + so we can just evaluate it once an for all (i.e., it does not change on each loop iteration, as it may happen in the finite case). -} Inf -> do let env = EvalEnv (leStatic lenv) (leTypes lenv) From d8223c129cfd1153acb627cc09972493a0d2f4f5 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 30 Oct 2023 09:51:52 -0700 Subject: [PATCH 3/3] Add a test --- tests/issues/T1584.icry | 1 + tests/issues/T1584.icry.stdout | 2 ++ 2 files changed, 3 insertions(+) create mode 100644 tests/issues/T1584.icry create mode 100644 tests/issues/T1584.icry.stdout diff --git a/tests/issues/T1584.icry b/tests/issues/T1584.icry new file mode 100644 index 000000000..1bf229b0f --- /dev/null +++ b/tests/issues/T1584.icry @@ -0,0 +1 @@ +take`{5} [ x+y | x <- [(0:Integer)...], y <- [1] ] diff --git a/tests/issues/T1584.icry.stdout b/tests/issues/T1584.icry.stdout new file mode 100644 index 000000000..933c3095b --- /dev/null +++ b/tests/issues/T1584.icry.stdout @@ -0,0 +1,2 @@ +Loading module Cryptol +[1, 2, 3, 4, 5]