GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 11:22:33 +03:00
Code Issues Projects Releases Wiki Activity

Remove evaluator cases that should not occur.

Browse Source 
These are translated away in the solver.
This commit is contained in:
Iavor Diatchki 2017-12-22 11:24:44 -08:00
parent c481fbc6e8
commit 7bf0fa8222
2 changed files with 1 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Cryptol/Eval.hs
View File

@ -417,9 +417,6 @@ evalSel val sel = case sel of
tupleSel n v =
case v of
VTuple vs -> vs !! n
VSeq w vs -> VSeq w <$> mapSeqMap (tupleSel n) vs
VStream vs -> VStream <$> mapSeqMap (tupleSel n) vs
VFun f -> return $ VFun (\x -> tupleSel n =<< f x)
_ -> do vdoc <- ppValue defaultPPOpts v
evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in tuple selection"
@ -428,9 +425,6 @@ evalSel val sel = case sel of
recordSel n v =
case v of
VRecord {} -> lookupRecord n v
VSeq w vs -> VSeq w <$> mapSeqMap (recordSel n) vs
VStream vs -> VStream <$> mapSeqMap (recordSel n) vs
VFun f -> return $ VFun (\x -> recordSel n =<< f x)
_ -> do vdoc <- ppValue defaultPPOpts v
evalPanic "Cryptol.Eval.evalSel"
[ "Unexpected value in record selection"

8
src/Cryptol/Eval/Reference.lhs
View File

@ -321,9 +321,7 @@ assigns values to those variables.
Selectors
---------
Apply the the given selector form to the given value. This function
pushes tuple and record selections pointwise down into sequences and
functions.
Apply the the given selector form to the given value.
> evalSel :: Value -> Selector -> Value
> evalSel val sel =
@ -335,15 +333,11 @@ functions.
> tupleSel n v =
> case v of
> VTuple vs -> vs !! n
> VList vs -> VList (map (tupleSel n) vs)
> VFun f -> VFun (\x -> tupleSel n (f x))
> _ -> evalPanic "evalSel"
> ["Unexpected value in tuple selection."]
> recordSel n v =
> case v of
> VRecord _ -> lookupRecord n v
> VList vs -> VList (map (recordSel n) vs)
> VFun f -> VFun (\x -> recordSel n (f x))
> _ -> evalPanic "evalSel"
> ["Unexpected value in record selection."]
> listSel n v =