GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-07 08:19:12 +03:00
Code Issues Projects Releases Wiki Activity

Add a new constructor for updating records to the intermediate language.

Browse Source
This commit is contained in:
Iavor Diatchki 2019-02-12 16:24:08 -08:00
parent 895f69f1c3
commit ea7f95e37d
6 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Cryptol/IR/FreeVars.hs
View File

@ -103,6 +103,7 @@ instance FreeVars Expr where
ETuple es -> freeVars es
ERec fs -> freeVars (map snd fs)
ESel e _ -> freeVars e
ESet e _ v -> freeVars [e,v]
EIf e1 e2 e3 -> freeVars [e1,e2,e3]
EComp t1 t2 e mss -> freeVars [t1,t2] <> rmVals (defs mss) (freeVars e)
<> mconcat (map fvsArm mss)

1
src/Cryptol/Transform/AddModParams.hs
View File

@ -233,6 +233,7 @@ instance Inst Expr where
ETuple es -> ETuple (inst ps es)
ERec fs -> ERec [ (f,inst ps e) | (f,e) <- fs ]
ESel e s -> ESel (inst ps e) s
ESet e s v -> ESet (inst ps e) s (inst ps v)
EIf e1 e2 e3 -> EIf (inst ps e1) (inst ps e2) (inst ps e3)
EComp t1 t2 e ms -> EComp (inst ps t1) (inst ps t2)

1
src/Cryptol/Transform/MonoValues.hs
View File

@ -184,6 +184,7 @@ rewE rews = go
ERec fs -> ERec <$> (forM fs $ \(f,e) -> do e1 <- go e
return (f,e1))
ESel e s -> ESel <$> go e <*> return s
ESet e s v -> ESet <$> go e <*> return s <*> go v
EIf e1 e2 e3 -> EIf <$> go e1 <*> go e2 <*> go e3
EComp len t e mss -> EComp len t <$> go e <*> mapM (mapM (rewM rews)) mss

1
src/Cryptol/Transform/Specialize.hs
View File

@ -77,6 +77,7 @@ specializeExpr expr =
ETuple es -> ETuple <$> traverse specializeExpr es
ERec fs -> ERec <$> traverse (traverseSnd specializeExpr) fs
ESel e s -> ESel <$> specializeExpr e <*> pure s
ESet e s v -> ESet <$> specializeExpr e <*> pure s <*> specializeExpr v
EIf e1 e2 e3 -> EIf <$> specializeExpr e1 <*> specializeExpr e2 <*> specializeExpr e3
EComp len t e mss -> EComp len t <$> specializeExpr e <*> traverse (traverse specializeMatch) mss
-- Bindings within list comprehensions always have monomorphic types.

3
src/Cryptol/TypeCheck/AST.hs
View File

@ -105,6 +105,7 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements)
| ETuple [Expr] -- ^ Tuple value
| ERec [(Ident,Expr)] -- ^ Record value
| ESel Expr Selector -- ^ Elimination for tuple/record/list
| ESet Expr Selector Expr -- ^ Change the value of a field.
| EIf Expr Expr Expr -- ^ If-then-else
| EComp Type Type Expr [[Match]]
@ -210,6 +211,8 @@ instance PP (WithNames Expr) where
ESel e sel -> ppWP 4 e <+> text "." <.> pp sel
ESet e sel v -> braces (pp e <+> "|" <+> pp sel <+> "=" <+> pp v)
EIf e1 e2 e3 -> optParens (prec > 0)
$ sep [ text "if" <+> ppW e1
, text "then" <+> ppW e2

3
src/Cryptol/TypeCheck/Parseable.hs
View File

@ -34,6 +34,9 @@ instance ShowParseable Expr where
showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es)
showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides)
showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s)
showParseable (ESet e s v) = parens (text "ESet" <+>
showParseable e <+> showParseable s
<+> showParseable v)
showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c $$ showParseable t $$ showParseable f)
showParseable (EComp _ _ e mss) = parens (text "EComp" $$ showParseable e $$ showParseable mss)
showParseable (EVar n) = parens (text "EVar" <+> showParseable n)