Skip to content

Commit

Permalink
TypedExpr: nits in the JSON printer
Browse files Browse the repository at this point in the history
  • Loading branch information
@zoep
zoep committed Oct 10, 2023
1 parent 079f55c commit f644ee6
Showing 1 changed file with 64 additions and 36 deletions.
100 changes: 64 additions & 36 deletions src/Syntax/TimeAgnostic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -352,24 +352,24 @@ instance Timable StorageRef where
-- It was difficult to construct a function with type:
-- `InvPredicate t -> Either (Exp Bool Timed,Exp Bool Timed) (Exp Bool Untimed)`
instance ToJSON (Act Timed) where
toJSON (Act storages contracts) = object [ "kind" .= String "Program"
toJSON (Act storages contracts) = object [ "kind" .= String "Act"
, "store" .= storeJSON storages
, "contracts" .= toJSON contracts ]

instance ToJSON (Act Untimed) where
toJSON (Act storages contracts) = object [ "kind" .= String "Program"
toJSON (Act storages contracts) = object [ "kind" .= String "Act"
, "store" .= storeJSON storages
, "contracts" .= toJSON contracts ]

instance ToJSON (Contract Timed) where
toJSON (Contract ctor behv) = object [ "kind" .= String "Contract"
, "constructor" .= toJSON ctor
, "behaviors" .= toJSON behv ]
, "constructor" .= toJSON ctor
, "behaviours" .= toJSON behv ]

instance ToJSON (Contract Untimed) where
toJSON (Contract ctor behv) = object [ "kind" .= String "Contract"
, "constructor" .= toJSON ctor
, "behaviors" .= toJSON behv ]
, "constructor" .= toJSON ctor
, "behaviours" .= toJSON behv ]


storeJSON :: Store -> Value
Expand All @@ -379,7 +379,7 @@ storeJSON storages = object [ "kind" .= String "Storages"
instance ToJSON (Constructor Timed) where
toJSON Constructor{..} = object [ "kind" .= String "Constructor"
, "contract" .= _cname
, "interface" .= (String . pack $ show _cinterface)
, "interface" .= toJSON _cinterface
, "preConditions" .= toJSON _cpreconditions
, "postConditions" .= toJSON _cpostconditions
, "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
Expand All @@ -388,7 +388,7 @@ instance ToJSON (Constructor Timed) where
instance ToJSON (Constructor Untimed) where
toJSON Constructor{..} = object [ "kind" .= String "Constructor"
, "contract" .= _cname
, "interface" .= (String . pack $ show _cinterface)
, "interface" .= toJSON _cinterface
, "preConditions" .= toJSON _cpreconditions
, "postConditions" .= toJSON _cpostconditions
, "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
Expand All @@ -398,13 +398,26 @@ instance ToJSON (Behaviour t) where
toJSON Behaviour{..} = object [ "kind" .= String "Behaviour"
, "name" .= _name
, "contract" .= _contract
, "interface" .= (String . pack $ show _interface)
, "interface" .= toJSON _interface
, "preConditions" .= toJSON _preconditions
, "case" .= toJSON _caseconditions
, "postConditions" .= toJSON _postconditions
, "stateUpdates" .= toJSON _stateUpdates
, "returns" .= toJSON _returns ]

instance ToJSON Interface where
toJSON (Interface x decls) = object [ "kind" .= String "Interface"
, "id" .= pack (show x)
, "args" .= toJSON decls
]

instance ToJSON Decl where
toJSON (Decl abitype x) = object [ "kind" .= String "Declaration"
, "id" .= pack (show x)
, "abitype" .= pack (show abitype)
]


invariantJSON :: ToJSON pred => Invariant t -> pred -> Value
invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant"
, "predicate" .= toJSON predicate
Expand All @@ -413,8 +426,8 @@ invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant"
, "contract" .= _icontract ]

instance ToJSON (Rewrite t) where
toJSON (Constant a) = object [ "Constant" .= toJSON a ]
toJSON (Rewrite a) = object [ "Rewrite" .= toJSON a ]
toJSON (Constant a) = object [ "constant" .= toJSON a ]
toJSON (Rewrite a) = object [ "rewrite" .= toJSON a ]

instance ToJSON (StorageLocation t) where
toJSON (Loc _ a) = object [ "location" .= toJSON a ]
Expand All @@ -423,26 +436,33 @@ instance ToJSON (StorageUpdate t) where
toJSON (Update _ a b) = object [ "location" .= toJSON a ,"value" .= toJSON b ]

instance ToJSON (TStorageItem a t) where
toJSON (Item t _ a) = object [ "sort" .= pack (show t)
, "item" .= toJSON a ]
toJSON (Item t _ a) = object [ "item" .= toJSON a
, "type" .= show t
]

instance ToJSON (StorageRef t) where
toJSON (SVar _ c x) = object [ "var" .= String (pack c <> "." <> pack x) ]
toJSON (SVar _ c x) = object [ "kind" .= pack "SVar"
, "svar" .= pack x
, "contract" .= pack c ]
toJSON (SMapping _ e xs) = mapping e xs
toJSON (SField _ e _ x) = field e x
toJSON (SField _ e c x) = field e c x

mapping :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
mapping a b = object [ "symbol" .= pack "lookup"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [toJSON a, toJSON b]) ]
mapping a b = object [ "kind" .= pack "Mapping"
, "indexes" .= toJSON b
, "reference" .= toJSON a]

field :: (ToJSON a1) => a1 -> Id -> Id -> Value
field a c x = object [ "kind" .= pack "Field"
, "field" .= pack x
, "contract" .= pack c
, "reference" .= toJSON a
]

field :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
field a b = object [ "symbol" .= pack "select"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [toJSON a, toJSON b]) ]

instance ToJSON (TypedExp t) where
toJSON (TExp typ a) = object [ "sort" .= pack (show typ)
toJSON (TExp typ a) = object [ "kind" .= pack "TypedExpr"
, "sort" .= pack (show typ)
, "expression" .= toJSON a ]

instance ToJSON (Exp a t) where
Expand All @@ -451,14 +471,15 @@ instance ToJSON (Exp a t) where
toJSON (Exp _ a b) = symbol "^" a b
toJSON (Mul _ a b) = symbol "*" a b
toJSON (Div _ a b) = symbol "/" a b
toJSON (LitInt _ a) = toJSON $ show a
toJSON (LitInt _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "int" ]
toJSON (IntMin _ a) = toJSON $ show $ intmin a
toJSON (IntMax _ a) = toJSON $ show $ intmax a
toJSON (UIntMin _ a) = toJSON $ show $ uintmin a
toJSON (UIntMax _ a) = toJSON $ show $ uintmax a
toJSON (InRange _ a b) = object [ "symbol" .= pack ("inrange" <> show a)
, "arity" .= Data.Aeson.Types.Number 1
, "args" .= Array (fromList [toJSON b]) ]
toJSON (InRange _ a b) = object [ "symbol" .= pack "inrange"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [String (pack $ show a), toJSON b]) ]
toJSON (IntEnv _ a) = String $ pack $ show a
toJSON (ITE _ a b c) = object [ "symbol" .= pack "ite"
, "arity" .= Data.Aeson.Types.Number 3
Expand All @@ -472,7 +493,8 @@ instance ToJSON (Exp a t) where
toJSON (Eq _ _ a b) = symbol "==" a b
toJSON (LEQ _ a b) = symbol "<=" a b
toJSON (GEQ _ a b) = symbol ">=" a b
toJSON (LitBool _ a) = String $ pack $ show a
toJSON (LitBool _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "bool" ]
toJSON (Neg _ a) = object [ "symbol" .= pack "not"
, "arity" .= Data.Aeson.Types.Number 1
, "args" .= Array (fromList [toJSON a]) ]
Expand All @@ -481,18 +503,24 @@ instance ToJSON (Exp a t) where
toJSON (Slice _ s a b) = object [ "symbol" .= pack "slice"
, "arity" .= Data.Aeson.Types.Number 3
, "args" .= Array (fromList [toJSON s, toJSON a, toJSON b]) ]
toJSON (ByStr _ a) = toJSON a
toJSON (ByLit _ a) = String . pack $ show a
toJSON (ByEnv _ a) = String . pack $ show a

toJSON (TEntry _ t a) = object [ fromString (show t) .= toJSON a ]
toJSON (Var _ _ _ a) = toJSON a
toJSON (ByStr _ a) = object [ "bytestring" .= toJSON a
, "type" .= pack "bool" ]
toJSON (ByLit _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "bytestring" ]
toJSON (ByEnv _ a) = object [ "ethEnv" .= pack (show a)
, "type" .= pack "bytestring" ]
toJSON (TEntry _ t a) = object [ "entry" .= toJSON a
, "timing" .= show t ]
toJSON (Var _ t _ a) = object [ "var" .= toJSON a
, "type" .= show t ]
toJSON (Create _ f xs) = object [ "symbol" .= pack "create"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ]
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ]

toJSON v = error $ "todo: json ast for: " <> show v



symbol :: (ToJSON a1, ToJSON a2) => String -> a1 -> a2 -> Value
symbol s a b = object [ "symbol" .= pack s
, "arity" .= Data.Aeson.Types.Number 2
Expand Down

0 comments on commit f644ee6

Please sign in to comment.