Add the 'Appendable' super-type and add hints for new number functions.
This commit is contained in:
parent
79e465c9e0
commit
0a4010e7da
3 changed files with 33 additions and 15 deletions
|
@ -43,11 +43,11 @@ lineTypes = [ numScheme (\n -> listOf (pairOf n) ==> line) "line"
|
|||
, "customLine" -: listOf int ==> color ==> line ==> form
|
||||
] ++ hasType (color ==> line ==> form) ["solid","dashed","dotted"]
|
||||
|
||||
shapes = [ numScheme (\n -> listOf (pairOf n) ==> pairOf n ==> shape) "polygon"
|
||||
shapes = [ twoNums (\n m -> listOf (pairOf n) ==> pairOf m ==> shape) "polygon"
|
||||
, "filled" -: color ==> shape ==> form
|
||||
, "outlined" -: color ==> shape ==> form
|
||||
, "customOutline" -: listOf int ==> color ==> shape ==> form
|
||||
] ++ map (numScheme (\n -> n ==> n ==> pairOf n ==> shape)) [ "ngon"
|
||||
] ++ map (twoNums (\n m -> n ==> n ==> pairOf m ==> shape)) [ "ngon"
|
||||
, "rect"
|
||||
, "oval" ]
|
||||
|
||||
|
@ -130,6 +130,9 @@ concreteSignals =
|
|||
binop t = t ==> t ==> t
|
||||
numScheme t name = (name, Forall [0] [VarT 0 :<: number] (t (VarT 0)))
|
||||
timeScheme name t = (name, Forall [0] [VarT 0 :<: time] (t (VarT 0)))
|
||||
twoNums f name =
|
||||
(,) name . Forall [0,1] [ VarT 0 :<: number, VarT 1 :<: number ] $
|
||||
f (VarT 0) (VarT 1)
|
||||
|
||||
math =
|
||||
map (numScheme (\t -> t ==> binop t)) ["clamp"] ++
|
||||
|
@ -137,7 +140,10 @@ math =
|
|||
[ numScheme (\t -> t ==> t) "abs" ] ++
|
||||
hasType (binop float) [ "/", "logBase" ] ++
|
||||
hasType (binop int) ["rem","div","mod"] ++
|
||||
hasType (float ==> float) ["sin","cos","tan","asin","acos","atan","sqrt"]
|
||||
hasType (float ==> float) ["sin","cos","tan","asin","acos","atan","sqrt"] ++
|
||||
hasType float ["pi","e"] ++
|
||||
hasType (int ==> float) ["toFloat","castIntToFloat"] ++
|
||||
hasType (float ==> int) ["round","floor","ceiling","truncate"]
|
||||
|
||||
bools =
|
||||
[ "not" -: bool ==> bool ] ++
|
||||
|
@ -163,7 +169,7 @@ funcs =
|
|||
, "." -:: (b ==> c) ==> (a ==> b) ==> (a ==> c)
|
||||
, "$" -:: (a ==> b) ==> a ==> b
|
||||
, ":" -:: a ==> listOf a ==> listOf a
|
||||
, "++" -:: a ==> a ==> a
|
||||
, (,) "++" . Forall [0,1] [ VarT 0 :<: appendable (VarT 1) ] $ VarT 0 ==> VarT 0 ==> VarT 0
|
||||
, "Cons" -:: a ==> listOf a ==> listOf a
|
||||
, "Nil" -:: listOf a
|
||||
, "Just" -:: a ==> maybeOf a
|
||||
|
@ -184,19 +190,22 @@ lists =
|
|||
, "scanl1" -:: (a ==> a ==> a) ==> listOf a ==> a
|
||||
, "forall" -:: (a ==> bool) ==> listOf a ==> bool
|
||||
, "exists" -:: (a ==> bool) ==> listOf a ==> bool
|
||||
, "concat" -:: listOf (listOf a) ==> listOf a
|
||||
, "reverse" -:: listOf a ==> listOf a
|
||||
, "take" -:: int ==> listOf a ==> listOf a
|
||||
, "drop" -:: int ==> listOf a ==> listOf a
|
||||
, "partition" -:: (a ==> bool) ==> listOf a ==> tupleOf [listOf a,listOf a]
|
||||
, "intersperse" -:: a ==> listOf a ==> listOf a
|
||||
, "intercalate" -:: listOf a ==> listOf(listOf a) ==> listOf a
|
||||
, "zip" -:: listOf a ==>listOf b ==>listOf(tupleOf [a,b])
|
||||
, "map" -:: (a ==> b) ==> listOf a ==> listOf b
|
||||
, "foldr" -:: (a ==> b ==> b) ==> b ==> listOf a ==> b
|
||||
, "foldl" -:: (a ==> b ==> b) ==> b ==> listOf a ==> b
|
||||
, "scanl" -:: (a ==> b ==> b) ==> b ==> listOf a ==> listOf b
|
||||
, "concatMap" -:: (a ==> listOf b) ==> listOf a ==> listOf b
|
||||
, (,) "concat" . Forall [0,1] [ VarT 0 :<: appendable (VarT 1) ] $
|
||||
listOf (VarT 0) ==> VarT 0
|
||||
, (,) "concatMap" . Forall [0,1,2] [ VarT 0 :<: appendable (VarT 1) ] $
|
||||
(VarT 2 ==> VarT 0) ==> listOf (VarT 2) ==> VarT 0
|
||||
, (,) "intercalate" . Forall [0,1] [ VarT 0 :<: appendable (VarT 1) ] $
|
||||
VarT 0 ==> listOf (VarT 0) ==> VarT 0
|
||||
, "zipWith" -:: (a ==> b ==> c) ==> listOf a ==> listOf b ==> listOf c
|
||||
] ++ map (numScheme (\n -> listOf n ==> n)) [ "sum", "product"
|
||||
, "maximum", "minimum" ]
|
||||
|
|
|
@ -31,10 +31,10 @@ number = SuperType "Number" (Set.fromList [ int, float ])
|
|||
char = tipe "Char"
|
||||
bool = tipe "Bool"
|
||||
|
||||
string = tipe "String"
|
||||
string = listOf char -- tipe "String"
|
||||
text = tipe "Text"
|
||||
|
||||
time = SuperType "Time" (Set.fromList [ int, float ])
|
||||
time = SuperType "Time" (Set.fromList [ int, float, tipe "Number" ])
|
||||
|
||||
element = tipe "Element"
|
||||
direction = tipe "Direction"
|
||||
|
@ -49,6 +49,7 @@ tupleOf ts = ADT ("Tuple" ++ show (length ts)) ts
|
|||
maybeOf t = ADT "Maybe" [t]
|
||||
pairOf t = tupleOf [t,t]
|
||||
point = pairOf int
|
||||
appendable t = SuperType "Appendable" (Set.fromList [ string, text, listOf t ])
|
||||
|
||||
jsBool = tipe "JSBool"
|
||||
jsNumber = tipe "JSNumber"
|
||||
|
@ -72,7 +73,8 @@ instance Show Type where
|
|||
case t of
|
||||
{ LambdaT t1@(LambdaT _ _) t2 -> parens (show t1) ++ " -> " ++ show t2
|
||||
; LambdaT t1 t2 -> show t1 ++ " -> " ++ show t2
|
||||
; VarT x -> show x
|
||||
; VarT x -> 't' : show x
|
||||
; ADT "List" [ADT "Char" []] -> "String"
|
||||
; ADT "List" [tipe] -> "[" ++ show tipe ++ "]"
|
||||
; ADT name cs ->
|
||||
if isTupleString name
|
||||
|
|
|
@ -30,8 +30,9 @@ solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =
|
|||
solver ((VarT x :=: t) : cs) subs =
|
||||
solver (map (cSub x t) cs) . map (second $ tSub x t) $ (x,t):subs
|
||||
solver ((t :=: VarT x) : cs) subs = solver ((VarT x :=: t) : cs) subs
|
||||
solver ((t1 :=: t2) : cs) subs =
|
||||
if t1 /= t2 then uniError t1 t2 else solver cs subs
|
||||
solver ((t1 :=: t2) : cs) subs
|
||||
| t1 == t2 = solver cs subs
|
||||
| otherwise = uniError t1 t2
|
||||
|
||||
-------- subtypes --------
|
||||
|
||||
|
@ -43,11 +44,18 @@ solver (c@(VarT x :<: SuperType n ts) : cs) subs
|
|||
solver ((t@(ADT n1 []) :<: st@(SuperType n2 ts)) : cs) subs
|
||||
| n1 == n2 || Set.member t ts = solver cs subs
|
||||
| otherwise = return . Left $ "Type error: " ++ show t ++
|
||||
" is not a subtype of " ++ show st
|
||||
" is not a " ++ show st
|
||||
solver ((t@(ADT "List" [_]) :<: st@(SuperType n' ts')) : cs) subs
|
||||
| any f (Set.toList ts') = solver cs subs
|
||||
| otherwise = return . Left $ "Type error: " ++ show t ++
|
||||
" is not a " ++ show st
|
||||
where f (ADT "List" [VarT _]) = True
|
||||
f _ = False
|
||||
|
||||
solver ((t :<: st@(SuperType n ts)) : cs) subs
|
||||
| Set.member t ts = solver cs subs
|
||||
| otherwise = return . Left $ "Type error: " ++ show t ++
|
||||
" is not a subtype of " ++ show st
|
||||
" is not a " ++ show st
|
||||
|
||||
solver ((t1 :<<: Forall xs cs' t2) : cs) subs = do
|
||||
pairs <- mapM (\x -> liftM ((,) x . VarT) guid) xs
|
||||
|
@ -63,7 +71,6 @@ cSub k v (t :<<: poly) = force $ tSub k v t :<<: poly
|
|||
tSub k v t@(VarT x) = if k == x then v else t
|
||||
tSub k v (LambdaT t1 t2) = force $ LambdaT (tSub k v t1) (tSub k v t2)
|
||||
tSub k v (ADT name ts) = ADT name (map (force . tSub k v) ts)
|
||||
tSub _ _ t = t
|
||||
|
||||
uniError t1 t2 =
|
||||
return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2
|
||||
|
|
Loading…
Reference in a new issue