Skip to content

Commit

Permalink
Make the cryptol-remote-api build again.
Browse files Browse the repository at this point in the history
It looks like the code previously just a had a placeholder for
`newtypes`.  Now it sends a bit more info for nominal types, but
I am not sure that the rest of the code would handle these correctly.
  • Loading branch information
yav committed Jan 31, 2024
1 parent 684a85e commit c68ecfc
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 4 deletions.
2 changes: 1 addition & 1 deletion cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Original file line number Diff line number Diff line change
Expand Up @@ -617,7 +617,7 @@ readBack ty val =
TVTuple{} -> "tuple"
TVRec{} -> "record"
TVFun{} -> "fun"
TVNewtype nt _ _ -> identText $ nameIdent $ TC.ntName nt
TVNominal nt _ _ -> identText $ nameIdent $ TC.ntName nt
TVAbstract{} -> "abstract"


Expand Down
14 changes: 11 additions & 3 deletions cryptol-remote-api/src/CryptolServer/Data/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,10 @@ import Cryptol.Parser.Position (emptyRange)
import Cryptol.Parser.Selector (ppSelector)
import Cryptol.Utils.RecordMap (recordFromFields)
import Cryptol.TypeCheck.PP (NameMap, emptyNameMap, ppWithNames)
import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf)
import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..),
TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf,
NominalType(..), NominalTypeDef(..)
)
import Cryptol.Utils.Ident (mkIdent)
import Cryptol.Utils.PP (pp)
import Cryptol.Utils.RecordMap (canonicalFields)
Expand Down Expand Up @@ -213,8 +216,13 @@ instance JSON.ToJSON JSONType where
, "name" .= show (ppWithNames ns v)
]
convert (TUser _n _args def) = convert def
convert (TNewtype _nt _ts) =
JSON.object [ "type" .= T.pack "newtype" ]
convert (TNominal nt ts) =
JSON.object [ "type" .= case ntDef nt of
Struct {} -> T.pack "newtype"
Enum {} -> T.pack "enum"
, "name" .= show (pp (ntName nt))
, "arguments" .= map (JSONType ns) ts
]
convert (TRec fields) =
JSON.object
[ "type" .= T.pack "record"
Expand Down

0 comments on commit c68ecfc

Please sign in to comment.