Merge pull request #866 from GaloisInc/rework-semantics

Reformulate evaluation semantics
GaloisInc · Sep 2, 2020 · 8bfad53 · 8bfad53
2 parents 4729596 + 04bd633
commit 8bfad53
Show file tree

Hide file tree

Showing 15 changed files with 830 additions and 797 deletions.
diff --git a/docs/Semantics.pdf b/docs/Semantics.pdf
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
@@ -138,9 +138,10 @@ evalExpr sym env expr = case expr of
      e' <- eval e
      evalSel sym e' sel
 
-  ESet e sel v -> {-# SCC "evalExpr->ESet" #-}
+  ESet ty e sel v -> {-# SCC "evalExpr->ESet" #-}
     do e' <- eval e
-       evalSetSel sym e' sel (eval v)
+       let tyv = evalValType (envTypes env) ty
+       evalSetSel sym tyv e' sel (eval v)
 
   EIf c t f -> {-# SCC "evalExpr->EIf" #-} do
      b <- fromVBit <$> eval c
@@ -584,14 +585,15 @@ evalSel sym val sel = case sel of
                               , show vdoc ]
 {-# SPECIALIZE evalSetSel ::
   ConcPrims =>
-  Concrete ->
+  Concrete -> TValue ->
   GenValue Concrete -> Selector -> SEval Concrete (GenValue Concrete) -> SEval Concrete (GenValue Concrete)
   #-}
 evalSetSel :: forall sym.
   EvalPrims sym =>
   sym ->
+  TValue ->
   GenValue sym -> Selector -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
-evalSetSel sym e sel v =
+evalSetSel sym _tyv e sel v =
   case sel of
     TupleSel n _  -> setTuple n
     RecordSel n _ -> setRecord n