Skip to content

Commit

Permalink
Merge pull request #1797 from GaloisInc/bugfix/denormalize-cryptol-types
Browse files Browse the repository at this point in the history
Revert #1790
  • Loading branch information
mergify[bot] authored Jan 7, 2023
2 parents a63a2f4 + d768a02 commit b7f1b19
Show file tree
Hide file tree
Showing 4 changed files with 2 additions and 24 deletions.
6 changes: 2 additions & 4 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,6 @@ import qualified Cryptol.Eval.Value as V
import qualified Cryptol.Eval.Concrete as V
import Cryptol.Eval.Type (evalValType)
import qualified Cryptol.TypeCheck.AST as C
import qualified Cryptol.TypeCheck.SimpType as ST
import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst)
import qualified Cryptol.ModuleSystem.Name as C
(asPrim, asParamName, nameUnique, nameIdent, nameInfo, NameInfo(..))
Expand Down Expand Up @@ -231,11 +230,10 @@ importPC sc pc =
C.PFLiteral -> panic "importPC PFLiteral" []
C.PValidFloat -> panic "importPC PValidFloat" []

-- | Normalize according to Cryptol's rules, then translate size types to SAW
-- values of type Num and value types to SAW types of sort 0.
-- | Translate size types to SAW values of type Num, value types to SAW types of sort 0.
importType :: SharedContext -> Env -> C.Type -> IO Term
importType sc env ty =
case ST.tRebuild ty of
case ty of
C.TVar tvar ->
case tvar of
C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "TVFree"
Expand Down
7 changes: 0 additions & 7 deletions intTests/test_join_split/README.md

This file was deleted.

10 changes: 0 additions & 10 deletions intTests/test_join_split/join_split.saw

This file was deleted.

3 changes: 0 additions & 3 deletions intTests/test_join_split/test.sh

This file was deleted.

0 comments on commit b7f1b19

Please sign in to comment.