| /dports/security/hs-cryptol/cryptol-2.11.0/src/Cryptol/TypeCheck/Solver/ |
| H A D | Class.hs | 72 TCon (TError {}) _ -> Unsolvable
75 TCon (TC TCBit) [] -> SolvedIf []
113 TCon (TError {}) _ -> Unsolvable
116 TCon (TC TCBit) [] -> SolvedIf []
153 TCon (TError {}) _ -> Unsolvable
165 TCon (TC TCBit) [] -> Unsolvable
222 TCon (TC TCSeq) [n, elTy] ->
467 TCon (TC TCRational) [] ->
470 TCon (TC TCFloat) [e,p]
508 TCon (TC TCFloat) [e,p]
[all …]
|
| H A D | Utils.hs | 27 TCon (TF TCAdd) [t1,t2] ->
33 TCon _ _ -> [] -- XXX: we could do some distributivity etc
51 TCon (TF TCAdd) [t1,t2] ->
54 TCon (TC (TCNum 0)) [] -> return (k, t2)
56 TCon (TC (TCNum k)) [] -> guard (k > 0) >> return (k, tNum (0::Int))
57 TCon {} -> Nothing
70 TCon (TF TCMul) [t1,t2] ->
73 TCon (TC (TCNum k)) [] -> guard (k > 1) >> return (k, tNum (1::Int))
74 TCon {} -> Nothing
|
| H A D | Selector.hs | 79 TCon (TC TCSeq) [len,el] -> liftSeq len el
80 TCon (TC TCFun) [t1,t2] -> liftFun t1 t2
86 TCon (TC (TCTuple m)) ts ->
90 TCon (TC TCSeq) [len,el] -> liftSeq len el
91 TCon (TC TCFun) [t1,t2] -> liftFun t1 t2
96 (ListSel n _, TCon (TC TCSeq) [l,t])
113 return (TCon (TC TCFun) [t1,t2'])
150 TCon (TC TCSeq) [len,el]
154 TCon (TC TCFun) [t1,t2]
170 TCon _ [_,eli] ->
[all …]
|
| /dports/security/hs-cryptol/cryptol-2.11.0/src/Cryptol/TypeCheck/ |
| H A D | SimpleSolver.hs | 45 TCon (PC PTrue) [] -> SolvedIf []
46 TCon (PC PAnd) [l,r] -> SolvedIf [l,r]
48 TCon (PC PZero) [ty] -> solveZeroInst ty
49 TCon (PC PLogic) [ty] -> solveLogicInst ty
50 TCon (PC PRing) [ty] -> solveRingInst ty
51 TCon (PC PField) [ty] -> solveFieldInst ty
53 TCon (PC PRound) [ty] -> solveRoundInst ty
55 TCon (PC PEq) [ty] -> solveEqInst ty
56 TCon (PC PCmp) [ty] -> solveCmpInst ty
63 TCon (PC PPrime) [ty] -> cryIsPrime ctxt ty
[all …]
|
| H A D | Type.hs | 7 , module Cryptol.TypeCheck.TCon
24 import Cryptol.TypeCheck.TCon
102 data Type = TCon !TCon ![Type] constructor
290 TCon x xs == TCon y ys = x == y && xs == ys function
307 (TCon x xs, TCon y ys) -> compare (x,xs) (y,ys)
677 tf1 f x = TCon (TF f) [x]
746 pEq t = TCon (PC PEq) [t]
749 pCmp t = TCon (PC PCmp) [t]
769 pTrue = TCon (PC PTrue) []
969 TCon (TC tc) ts ->
[all …]
|
| H A D | SimpType.hs | 23 TCon tc ts -> tCon tc (map go ts)
28 tCon :: TCon -> [Type] -> Type
45 _ -> TCon tc ts
46 _ -> TCon tc ts
115 , TCon (TF TCAdd) [a,b] <- tNoUser x
146 mulK n t | TCon (TF TCMul) [a,b] <- t'
150 | TCon (TF TCDiv) [a,b] <- t'
249 | TCon (TF TCMin) [a,b] <- t'
267 | TCon (TF TCAdd) [a,b] <- t'
272 | TCon (TF TCSub) [a,b] <- t'
[all …]
|
| H A D | Unify.hs | 59 mgu (TCon (TC tc1) ts1) (TCon (TC tc2) ts2)
62 mgu (TCon (TF f1) ts1) (TCon (TF f2) ts2)
66 | TCon (TF _) _ <- t1, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2]) function
67 | TCon (TF _) _ <- t2, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2]) function
|
| H A D | Sanity.hs | 67 TCon tc ts ->
240 TCon (TC TCFun) [ a, b ]
280 TCon (TC (TCTuple sz)) ts ->
288 TCon (TC TCSeq) [s,elT] ->
290 return (TCon (TC TCSeq) [s,res])
292 TCon (TC TCFun) [a,b] ->
328 TCon (TC TCSeq) [ n, elT ] ->
334 TCon (TC (TCNum m)) []
371 TCon tc1 ts1 -> case other of
372 TCon tc2 ts2
[all …]
|
| H A D | TypePat.hs | 42 tcon :: TCon -> ([Type] -> a) -> Pat Type a
44 TCon c ts | f == c -> return (p ts)
76 TCon (TC (TCNum n)) _ -> return n
150 TCon (TC (TCTuple _)) ts -> return ts
192 TCon (TError (_ :-> k1) ) _ | k == k1 -> return ()
|
| H A D | TCon.hs | 2 module Cryptol.TypeCheck.TCon where
16 infixPrimTy :: TCon -> Maybe (Ident,Fixity)
40 builtInType :: M.Name -> Maybe TCon
123 instance HasKind TCon where
194 data TCon = TC TC | PC PC | TF TFun | TError Kind type
294 instance PP TCon where
|
| H A D | TypeMap.hs | 119 , tcon :: Map TCon (List TypeMap a)
137 TCon c ts -> lookupTM ts <=< lookupTM c . tcon
146 TCon c ts -> m { tcon = alterTM c (updSub ts f) (tcon m) } function
153 [ (TCon c ts, v) | (c,m1) <- toListTM (tcon m)
175 (\ts a -> f (TCon c ts) a) l) (tcon m)
|
| /dports/devel/hs-hoogle/hoogle-5.0.18.2/src/Input/ |
| H A D | Item.hs | 44 rnf (TCon x y) = rnf x `seq` rnf y
56 put (TCon x y) = put (0 :: Word8) >> put x >> put y
68 f (TVar x xs) = f $ TCon x xs
69 f (TCon x []) = x
70 f (TCon x xs) = "(" ++ unwords (x : map f xs) ++ ")"
209 ty (TyForall _ _ _ x) = TCon "\\/" [ty x]
210 ty x@TyFun{} = TCon "->" $ tyFun x
212 ty (TyList _ x) = TCon "[]" [ty x]
213 ty (TyParArray _ x) = TCon "[::]" [ty x]
215 TCon a b -> TCon a (b ++ [ty y])
[all …]
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/Treeless/ |
| H A D | AsPatterns.hs | 31 _ -> pure $ mkTApp (TCon c) vs
32 | otherwise = pure $ mkTApp (TCon c) vs
51 …TCon{} -> tApp t [] -- need to recover nullary constructors as well (to make deep @-patterns wor…
72 tApp (TCon c) vs = lookupAsPattern c vs
|
| H A D | Simplify.hs | 106 t@TCon{} -> pure t
151 conView (TCon c) = Just (c, [])
207 | TApp TCon{} _ <- u = mkTApp v vs
218 k >= 2^64, Just trueCon <- true = TCon trueCon
222 , Just falseCon <- false = if k < j then TCon trueCon else TCon falseCon
233 , Just falseCon <- false = if k >= j then TCon trueCon else TCon falseCon
298 operations TCon{} = 0
327 isTrue (TCon c) = Just c == true
330 isFalse (TCon c) = Just c == false
393 pruneBoolGuards d (b@(TAGuard (TCon c) _) : bs)
[all …]
|
| H A D | Builtin.hs | 80 TCon c | isZero c -> tInt 0
98 TApp (TCon s) [e] | isSuc s ->
104 TApp (TCon c) [e]
163 t@TCon{} -> t
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/MAlonzo/ |
| H A D | Coerce.hs | 29 TCon{} -> return $ TCoerce t
56 TCon{} -> return t
74 funArity (TCon q) = erasedArity q
|
| /dports/security/hs-cryptol/cryptol-2.11.0/src/Cryptol/Eval/ |
| H A D | Type.hs | 132 TCon (TC c) ts ->
157 TCon (TF f) ts -> Left $ evalTF f (map num ts)
158 TCon (PC p) _ -> evalPanic "evalType" ["invalid predicate symbol", show p]
159 TCon (TError _) ts -> evalPanic "evalType"
213 ty = TCon (TF f) (map tNat' vs)
|
| /dports/devel/hs-hoogle/hoogle-5.0.18.2/src/Output/ |
| H A D | Types.hs | 47 … inst <- pure $ Map.fromListWith (+) [(fromIString x,1) | (_, IInstance (Sig _ [TCon x _])) <- xs]
90 tys -> [ qq { sigTy = init tys ++ [TCon maybeCtor [last tys]] } ]
97 [TCon n _] -> n
100 s = strPack <$> Sig { sigCtx = [], sigTy = [TCon c []] }
169 g (TCon x xs) = TCon (con x) $ map g xs
175 …let sigNames (Sig ctx typ) = nubOrd [strCons '~' x | Ctx x _ <- ctx] ++ nubOrd [x | TCon x _ <- un…
500 TCon n [] | n == arrow -> TyCon n [] -- empty function type?!
501 TCon n tys | n == arrow -> TyFun (map toTy (init tys)) (toTy $ last tys)
502 TCon n tys -> TyCon n (map toTy tys)
|
| /dports/security/hs-cryptol/cryptol-2.11.0/src/Cryptol/TypeCheck/Solver/Numeric/ |
| H A D | Fin.hs | 36 TCon (TC tc) []
40 TCon (TF f) ts ->
|
| /dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/_cabal_deps/haskell-src-exts-1.23.1/tests/examples/ |
| H A D | GadtRecordFields.hs | 4 TCon :: { field1 :: Int, field2 :: Bool } -> Ty
|
| H A D | GadtRecordFields.hs.prettyprinter.golden | 4 TCon :: {field1 :: Int, field2 :: Bool} -> Ty
|
| /dports/devel/hs-hoogle/hoogle-5.0.18.2/_cabal_deps/haskell-src-exts-1.23.0/tests/examples/ |
| H A D | GadtRecordFields.hs | 4 TCon :: { field1 :: Int, field2 :: Bool } -> Ty
|
| H A D | GadtRecordFields.hs.prettyprinter.golden | 4 TCon :: {field1 :: Int, field2 :: Bool} -> Ty
|
| /dports/www/hs-postgrest/postgrest-8.0.0/_cabal_deps/haskell-src-exts-1.23.1/tests/examples/ |
| H A D | GadtRecordFields.hs | 4 TCon :: { field1 :: Int, field2 :: Bool } -> Ty
|
| H A D | GadtRecordFields.hs.prettyprinter.golden | 4 TCon :: {field1 :: Int, field2 :: Bool} -> Ty
|