1{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass, Safe #-}
2module Cryptol.TypeCheck.TCon where
3
4import qualified Data.Map as Map
5import GHC.Generics (Generic)
6import Control.DeepSeq
7
8import Cryptol.Parser.Selector
9import qualified Cryptol.ModuleSystem.Name as M
10import Cryptol.Utils.Fixity
11import Cryptol.Utils.Ident
12import Cryptol.Utils.PP
13
14-- | This is used for pretty prinitng.
15-- XXX: it would be nice to just rely in the info from the Prelude.
16infixPrimTy :: TCon -> Maybe (Ident,Fixity)
17infixPrimTy = \tc -> Map.lookup tc mp
18  where
19  mp = Map.fromList
20          [ tInfix "=="  PC PEqual    (n 20)
21          , tInfix "!="  PC PNeq      (n 20)
22          , tInfix ">="  PC PGeq      (n 30)
23          , tInfix  "+"  TF TCAdd     (l 80)
24          , tInfix  "-"  TF TCSub     (l 80)
25          , tInfix  "*"  TF TCMul     (l 90)
26          , tInfix  "/"  TF TCDiv     (l 90)
27          , tInfix  "%"  TF TCMod     (l 90)
28          , tInfix  "^^" TF TCExp     (r 95)
29          , tInfix  "/^" TF TCCeilDiv (l 90)
30          , tInfix  "%^" TF TCCeilMod (l 90)
31          ]
32
33  r x = Fixity { fAssoc = RightAssoc, fLevel = x }
34  l x = Fixity { fAssoc = LeftAssoc,  fLevel = x }
35  n x = Fixity { fAssoc = NonAssoc,   fLevel = x }
36
37  tInfix x mk tc f = (mk tc, (packIdent x, f))
38
39
40builtInType :: M.Name -> Maybe TCon
41builtInType nm =
42  case M.nameInfo nm of
43    M.Declared m _
44      | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
45      | m == floatName   -> Map.lookup (M.nameIdent nm) builtInFloat
46      | m == arrayName   -> Map.lookup (M.nameIdent nm) builtInArray
47    _ -> Nothing
48
49  where
50  x ~> y = (packIdent x, y)
51
52  -- Built-in types from Float.cry
53  builtInFloat = Map.fromList
54    [ "Float"             ~> TC TCFloat
55    , "ValidFloat"        ~> PC PValidFloat
56    ]
57
58  -- Built-in types from Cryptol.cry
59  builtInTypes = Map.fromList
60    [ -- Types
61      "inf"               ~> TC TCInf
62    , "Bit"               ~> TC TCBit
63    , "Integer"           ~> TC TCInteger
64    , "Rational"          ~> TC TCRational
65    , "Z"                 ~> TC TCIntMod
66
67      -- Predicate contstructors
68    , "=="                ~> PC PEqual
69    , "!="                ~> PC PNeq
70    , ">="                ~> PC PGeq
71    , "fin"               ~> PC PFin
72    , "prime"             ~> PC PPrime
73    , "Zero"              ~> PC PZero
74    , "Logic"             ~> PC PLogic
75    , "Ring"              ~> PC PRing
76    , "Integral"          ~> PC PIntegral
77    , "Field"             ~> PC PField
78    , "Round"             ~> PC PRound
79    , "Eq"                ~> PC PEq
80    , "Cmp"               ~> PC PCmp
81    , "SignedCmp"         ~> PC PSignedCmp
82    , "Literal"           ~> PC PLiteral
83    , "LiteralLessThan"   ~> PC PLiteralLessThan
84    , "FLiteral"          ~> PC PFLiteral
85
86    -- Type functions
87    , "+"                ~> TF TCAdd
88    , "-"                ~> TF TCSub
89    , "*"                ~> TF TCMul
90    , "/"                ~> TF TCDiv
91    , "%"                ~> TF TCMod
92    , "^^"               ~> TF TCExp
93    , "width"            ~> TF TCWidth
94    , "min"              ~> TF TCMin
95    , "max"              ~> TF TCMax
96    , "/^"               ~> TF TCCeilDiv
97    , "%^"               ~> TF TCCeilMod
98    , "lengthFromThenTo" ~> TF TCLenFromThenTo
99    ]
100
101  -- Built-in types from Array.cry
102  builtInArray = Map.fromList
103    [ "Array" ~> TC TCArray
104    ]
105
106
107
108
109--------------------------------------------------------------------------------
110
111infixr 5 :->
112
113-- | Kinds, classify types.
114data Kind   = KType
115            | KNum
116            | KProp
117            | Kind :-> Kind
118              deriving (Eq, Ord, Show, Generic, NFData)
119
120class HasKind t where
121  kindOf :: t -> Kind
122
123instance HasKind TCon where
124  kindOf (TC tc)      = kindOf tc
125  kindOf (PC pc)      = kindOf pc
126  kindOf (TF tf)      = kindOf tf
127  kindOf (TError k)   = k
128
129instance HasKind UserTC where
130  kindOf (UserTC _ k) = k
131
132instance HasKind TC where
133  kindOf tcon =
134    case tcon of
135      TCNum _   -> KNum
136      TCInf     -> KNum
137      TCBit     -> KType
138      TCInteger -> KType
139      TCRational -> KType
140      TCFloat   -> KNum :-> KNum :-> KType
141      TCIntMod  -> KNum :-> KType
142      TCArray   -> KType :-> KType :-> KType
143      TCSeq     -> KNum :-> KType :-> KType
144      TCFun     -> KType :-> KType :-> KType
145      TCTuple n -> foldr (:->) KType (replicate n KType)
146      TCAbstract x -> kindOf x
147
148instance HasKind PC where
149  kindOf pc =
150    case pc of
151      PEqual     -> KNum :-> KNum :-> KProp
152      PNeq       -> KNum :-> KNum :-> KProp
153      PGeq       -> KNum :-> KNum :-> KProp
154      PFin       -> KNum :-> KProp
155      PPrime     -> KNum :-> KProp
156      PHas _     -> KType :-> KType :-> KProp
157      PZero      -> KType :-> KProp
158      PLogic     -> KType :-> KProp
159      PRing      -> KType :-> KProp
160      PIntegral  -> KType :-> KProp
161      PField     -> KType :-> KProp
162      PRound     -> KType :-> KProp
163      PEq        -> KType :-> KProp
164      PCmp       -> KType :-> KProp
165      PSignedCmp -> KType :-> KProp
166      PLiteral   -> KNum :-> KType :-> KProp
167      PLiteralLessThan -> KNum :-> KType :-> KProp
168      PFLiteral  -> KNum :-> KNum :-> KNum :-> KType :-> KProp
169      PValidFloat -> KNum :-> KNum :-> KProp
170      PAnd       -> KProp :-> KProp :-> KProp
171      PTrue      -> KProp
172
173instance HasKind TFun where
174  kindOf tfun =
175    case tfun of
176      TCWidth   -> KNum :-> KNum
177
178      TCAdd     -> KNum :-> KNum :-> KNum
179      TCSub     -> KNum :-> KNum :-> KNum
180      TCMul     -> KNum :-> KNum :-> KNum
181      TCDiv     -> KNum :-> KNum :-> KNum
182      TCMod     -> KNum :-> KNum :-> KNum
183      TCExp     -> KNum :-> KNum :-> KNum
184      TCMin     -> KNum :-> KNum :-> KNum
185      TCMax     -> KNum :-> KNum :-> KNum
186      TCCeilDiv -> KNum :-> KNum :-> KNum
187      TCCeilMod -> KNum :-> KNum :-> KNum
188
189      TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
190
191
192
193-- | Type constants.
194data TCon   = TC TC | PC PC | TF TFun | TError Kind
195              deriving (Show, Eq, Ord, Generic, NFData)
196
197
198-- | Predicate symbols.
199-- If you add additional user-visible constructors, please update 'primTys'.
200data PC     = PEqual        -- ^ @_ == _@
201            | PNeq          -- ^ @_ /= _@
202            | PGeq          -- ^ @_ >= _@
203            | PFin          -- ^ @fin _@
204            | PPrime        -- ^ @prime _@
205
206            -- classes
207            | PHas Selector -- ^ @Has sel type field@ does not appear in schemas
208            | PZero         -- ^ @Zero _@
209            | PLogic        -- ^ @Logic _@
210            | PRing         -- ^ @Ring _@
211            | PIntegral     -- ^ @Integral _@
212            | PField        -- ^ @Field _@
213            | PRound        -- ^ @Round _@
214            | PEq           -- ^ @Eq _@
215            | PCmp          -- ^ @Cmp _@
216            | PSignedCmp    -- ^ @SignedCmp _@
217            | PLiteral      -- ^ @Literal _ _@
218            | PLiteralLessThan -- ^ @LiteralLessThan _ _@
219            | PFLiteral     -- ^ @FLiteral _ _ _@
220
221            | PValidFloat   -- ^ @ValidFloat _ _@ constraints on supported
222                            -- floating point representaitons
223
224            | PAnd          -- ^ This is useful when simplifying things in place
225            | PTrue         -- ^ Ditto
226              deriving (Show, Eq, Ord, Generic, NFData)
227
228-- | 1-1 constants.
229-- If you add additional user-visible constructors, please update 'primTys'.
230data TC     = TCNum Integer            -- ^ Numbers
231            | TCInf                    -- ^ Inf
232            | TCBit                    -- ^ Bit
233            | TCInteger                -- ^ Integer
234            | TCFloat                  -- ^ Float
235            | TCIntMod                 -- ^ @Z _@
236            | TCRational               -- ^ @Rational@
237            | TCArray                  -- ^ @Array _ _@
238            | TCSeq                    -- ^ @[_] _@
239            | TCFun                    -- ^ @_ -> _@
240            | TCTuple Int              -- ^ @(_, _, _)@
241            | TCAbstract UserTC        -- ^ An abstract type
242              deriving (Show, Eq, Ord, Generic, NFData)
243
244
245data UserTC = UserTC M.Name Kind
246              deriving (Show, Generic, NFData)
247
248instance Eq UserTC where
249  UserTC x _ == UserTC y _ = x == y
250
251instance Ord UserTC where
252  compare (UserTC x _) (UserTC y _) = compare x y
253
254
255
256
257
258
259-- | Built-in type functions.
260-- If you add additional user-visible constructors,
261-- please update 'primTys' in "Cryptol.Prims.Types".
262data TFun
263
264  = TCAdd                 -- ^ @ : Num -> Num -> Num @
265  | TCSub                 -- ^ @ : Num -> Num -> Num @
266  | TCMul                 -- ^ @ : Num -> Num -> Num @
267  | TCDiv                 -- ^ @ : Num -> Num -> Num @
268  | TCMod                 -- ^ @ : Num -> Num -> Num @
269  | TCExp                 -- ^ @ : Num -> Num -> Num @
270  | TCWidth               -- ^ @ : Num -> Num @
271  | TCMin                 -- ^ @ : Num -> Num -> Num @
272  | TCMax                 -- ^ @ : Num -> Num -> Num @
273  | TCCeilDiv             -- ^ @ : Num -> Num -> Num @
274  | TCCeilMod             -- ^ @ : Num -> Num -> Num @
275
276  -- Computing the lengths of explicit enumerations
277  | TCLenFromThenTo       -- ^ @ : Num -> Num -> Num -> Num@
278    -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@
279
280    deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData)
281
282
283
284--------------------------------------------------------------------------------
285-- Pretty printing
286
287instance PP Kind where
288  ppPrec p k = case k of
289    KType   -> char '*'
290    KNum    -> char '#'
291    KProp   -> text "Prop"
292    l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r])
293
294instance PP TCon where
295  ppPrec _ (TC tc)        = pp tc
296  ppPrec _ (PC tc)        = pp tc
297  ppPrec _ (TF tc)        = pp tc
298  ppPrec _ (TError _)     = "Error"
299
300
301instance PP PC where
302  ppPrec _ x =
303    case x of
304      PEqual     -> text "(==)"
305      PNeq       -> text "(/=)"
306      PGeq       -> text "(>=)"
307      PFin       -> text "fin"
308      PPrime     -> text "prime"
309      PHas sel   -> parens (ppSelector sel)
310      PZero      -> text "Zero"
311      PLogic     -> text "Logic"
312      PRing      -> text "Ring"
313      PIntegral  -> text "Integral"
314      PField     -> text "Field"
315      PRound     -> text "Round"
316      PEq        -> text "Eq"
317      PCmp       -> text "Cmp"
318      PSignedCmp -> text "SignedCmp"
319      PLiteral   -> text "Literal"
320      PLiteralLessThan -> text "LiteralLessThan"
321      PFLiteral  -> text "FLiteral"
322      PValidFloat -> text "ValidFloat"
323      PTrue      -> text "True"
324      PAnd       -> text "(&&)"
325
326instance PP TC where
327  ppPrec _ x =
328    case x of
329      TCNum n   -> integer n
330      TCInf     -> text "inf"
331      TCBit     -> text "Bit"
332      TCInteger -> text "Integer"
333      TCIntMod  -> text "Z"
334      TCRational -> text "Rational"
335      TCArray   -> text "Array"
336      TCFloat   -> text "Float"
337      TCSeq     -> text "[]"
338      TCFun     -> text "(->)"
339      TCTuple 0 -> text "()"
340      TCTuple 1 -> text "(one tuple?)"
341      TCTuple n -> parens $ hcat $ replicate (n-1) comma
342      TCAbstract u -> pp u
343
344instance PP UserTC where
345  ppPrec p (UserTC x _) = ppPrec p x
346
347instance PP TFun where
348  ppPrec _ tcon =
349    case tcon of
350      TCAdd             -> text "+"
351      TCSub             -> text "-"
352      TCMul             -> text "*"
353      TCDiv             -> text "/"
354      TCMod             -> text "%"
355      TCExp             -> text "^^"
356      TCWidth           -> text "width"
357      TCMin             -> text "min"
358      TCMax             -> text "max"
359      TCCeilDiv         -> text "/^"
360      TCCeilMod         -> text "%^"
361      TCLenFromThenTo   -> text "lengthFromThenTo"
362