mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-23 08:18:04 +03:00
modify type smart constructors to set annotations
This commit is contained in:
parent
591317fff4
commit
a4a1f6973c
@ -50,11 +50,11 @@ focus1 e = ABT.Path go' where
|
||||
go Fn (Term (E.App' fn arg)) =
|
||||
Just (Term fn, \fn -> Term <$> (E.app <$> asTerm fn <*> pure (w arg)), [])
|
||||
go Fn (Type (T.App' fn arg)) =
|
||||
Just (Type fn, \fn -> Type <$> (T.app <$> asType fn <*> pure (wt arg)), [])
|
||||
Just (Type fn, \fn -> Type <$> (T.app() <$> asType fn <*> pure (wt arg)), [])
|
||||
go Arg (Term (E.App' fn arg)) =
|
||||
Just (Term arg, \arg -> Term <$> (E.app (w fn) <$> asTerm arg), [])
|
||||
go Arg (Type (T.App' fn arg)) =
|
||||
Just (Type arg, \arg -> Type <$> (T.app (wt fn) <$> asType arg), [])
|
||||
Just (Type arg, \arg -> Type <$> (T.app() (wt fn) <$> asType arg), [])
|
||||
go Body (Term (E.LamNamed' v body)) = Just (Term body, \t -> Term . set <$> asTerm t, [v]) where
|
||||
set body = ABT.tm (E.Lam (ABT.absr v body))
|
||||
go Body (Term (E.Let1Named' v b body)) = Just (Term body, \t -> Term . set <$> asTerm t, [v]) where
|
||||
@ -81,7 +81,7 @@ focus1 e = ABT.Path go' where
|
||||
go Bound (Term (E.Let1Named' v b body)) =
|
||||
Just (Var v, \v -> (\v -> Term $ E.let1 [(v,w b)] (w body)) <$> asVar v, [])
|
||||
go Bound (Type (T.ForallNamed' v body)) =
|
||||
Just (Var v, \v -> Type <$> (T.forall <$> asVar v <*> pure (wt body)), [])
|
||||
Just (Var v, \v -> Type <$> (T.forall() <$> asVar v <*> pure (wt body)), [])
|
||||
go (Index i) (Term (E.Vector' vs)) | i < Vector.length vs && i >= 0 =
|
||||
Just (Term (vs `Vector.unsafeIndex` i),
|
||||
\e -> (\e -> Term $ E.vector' $ fmap w vs // [(i,e)]) <$> asTerm e,
|
||||
@ -91,8 +91,8 @@ focus1 e = ABT.Path go' where
|
||||
set _ = Nothing
|
||||
go Annotation (Term (E.Ann' e t)) = Just (Type t, \t -> Term . E.ann (w e) <$> asType t, [])
|
||||
go Body (Term (E.Ann' body t)) = Just (Term body, \body -> Term . flip E.ann (wt t) <$> asTerm body, [])
|
||||
go Input (Type (T.Arrow' i o)) = Just (Type i, \i -> Type <$> (T.arrow <$> asType i <*> pure (wt o)), [])
|
||||
go Output (Type (T.Arrow' i o)) = Just (Type o, \o -> Type . T.arrow (wt i) <$> asType o, [])
|
||||
go Input (Type (T.Arrow' i o)) = Just (Type i, \i -> Type <$> (T.arrow() <$> asType i <*> pure (wt o)), [])
|
||||
go Output (Type (T.Arrow' i o)) = Just (Type o, \o -> Type . T.arrow() (wt i) <$> asType o, [])
|
||||
go _ _ = Nothing
|
||||
|
||||
type Path = [PathElement]
|
||||
|
@ -351,8 +351,10 @@ alias = do
|
||||
TypeParser.Aliases s <- get
|
||||
let s' = (fn, apply)
|
||||
apply args | length args <= length params = ABT.substs (params `zip` args) body
|
||||
apply args = apply (take n args) `Type.apps` drop n args
|
||||
apply args = apply (take n args) `Type.apps` (addUnit <$> drop n args)
|
||||
apply args = apply (take n args) `Type.apps` (addUnit <$> drop n args)
|
||||
n = length params
|
||||
addUnit a = ((), a)
|
||||
set (TypeParser.Aliases (s':s))
|
||||
|
||||
-- bindings :: Var v => Parser (S v) [(v, Term v)]
|
||||
|
@ -25,6 +25,7 @@ import qualified Unison.Hashable as Hashable
|
||||
import qualified Unison.Kind as K
|
||||
import qualified Unison.Reference as Reference
|
||||
import qualified Unison.TypeVar as TypeVar
|
||||
import qualified Unison.Var as Var
|
||||
|
||||
-- | Base functor for types in the Unison language
|
||||
data F a
|
||||
@ -117,65 +118,66 @@ isArrow _ = False
|
||||
|
||||
-- some smart constructors
|
||||
|
||||
infixr 7 -->
|
||||
(-->) :: Ord v => Type v -> Type v -> Type v
|
||||
(-->) = arrow
|
||||
vector :: Ord v => a -> AnnotatedType v a
|
||||
vector a = builtin a "Sequence"
|
||||
|
||||
vector :: Ord v => Type v
|
||||
vector = builtin "Sequence"
|
||||
-- vectorOf :: Ord v => a -> AnnotatedType v a -> Type v
|
||||
-- vectorOf a t = vector `app` t
|
||||
|
||||
vectorOf :: Ord v => Type v -> Type v
|
||||
vectorOf t = vector `app` t
|
||||
ref :: Ord v => a -> Reference -> AnnotatedType v a
|
||||
ref a = ABT.tm' a . Ref
|
||||
|
||||
ref :: Ord v => Reference -> Type v
|
||||
ref = ABT.tm . Ref
|
||||
builtin :: Ord v => a -> Text -> AnnotatedType v a
|
||||
builtin a = ref a . Reference.Builtin
|
||||
|
||||
builtin :: Ord v => Text -> Type v
|
||||
builtin = ref . Reference.Builtin
|
||||
int64 :: Ord v => a -> AnnotatedType v a
|
||||
int64 a = builtin a "Int64"
|
||||
|
||||
int64 :: Ord v => Type v
|
||||
int64 = builtin "Int64"
|
||||
uint64 :: Ord v => a -> AnnotatedType v a
|
||||
uint64 a = builtin a "UInt64"
|
||||
|
||||
uint64 :: Ord v => Type v
|
||||
uint64 = builtin "UInt64"
|
||||
float :: Ord v => a -> AnnotatedType v a
|
||||
float a = builtin a "Float"
|
||||
|
||||
float :: Ord v => Type v
|
||||
float = builtin "Float"
|
||||
boolean :: Ord v => a -> AnnotatedType v a
|
||||
boolean a = builtin a "Boolean"
|
||||
|
||||
boolean :: Ord v => Type v
|
||||
boolean = builtin "Boolean"
|
||||
text :: Ord v => a -> AnnotatedType v a
|
||||
text a = builtin a "Text"
|
||||
|
||||
text :: Ord v => Type v
|
||||
text = builtin "Text"
|
||||
stream :: Ord v => a -> AnnotatedType v a
|
||||
stream a = builtin a "Stream"
|
||||
|
||||
stream :: Ord v => Type v
|
||||
stream = builtin "Stream"
|
||||
app :: Ord v => a -> AnnotatedType v a -> AnnotatedType v a -> AnnotatedType v a
|
||||
app a f arg = ABT.tm' a (App f arg)
|
||||
|
||||
-- `f x y z` means `((f x) y) z` and the annotation paired with `y` is the one
|
||||
-- meant for `app (f x) y`
|
||||
apps :: Ord v => AnnotatedType v a -> [(a, AnnotatedType v a)] -> AnnotatedType v a
|
||||
apps f params = foldl' go f params where
|
||||
go f (a,t) = app a f t
|
||||
|
||||
arrow :: Ord v => a -> AnnotatedType v a -> AnnotatedType v a -> AnnotatedType v a
|
||||
arrow a i o = ABT.tm' a (Arrow i o)
|
||||
|
||||
ann :: Ord v => a -> AnnotatedType v a -> K.Kind -> AnnotatedType v a
|
||||
ann a e t = ABT.tm' a (Ann e t)
|
||||
|
||||
forall :: Ord v => a -> v -> AnnotatedType v a -> AnnotatedType v a
|
||||
forall a v body = ABT.tm' a (Forall (ABT.abs' a v body))
|
||||
|
||||
iff :: Var v => Type v
|
||||
iff = forall aa $ arrows [boolean, a, a] a
|
||||
iff = forall () aa $ arrows (f <$> [boolean(), a, a]) a
|
||||
where aa = ABT.v' "a"
|
||||
a = var aa
|
||||
a = var () aa
|
||||
f x = ((), x)
|
||||
|
||||
andor :: Ord v => Type v
|
||||
andor = arrows [boolean, boolean] boolean
|
||||
andor = arrows (f <$> [boolean(), boolean()]) $ boolean()
|
||||
where f x = ((), x)
|
||||
|
||||
app :: Ord v => Type v -> Type v -> Type v
|
||||
app f arg = ABT.tm (App f arg)
|
||||
|
||||
apps :: Ord v => Type v -> [Type v] -> Type v
|
||||
apps f = foldl' app f
|
||||
|
||||
arrow :: Ord v => Type v -> Type v -> Type v
|
||||
arrow i o = ABT.tm (Arrow i o)
|
||||
|
||||
ann :: Ord v => Type v -> K.Kind -> Type v
|
||||
ann e t = ABT.tm (Ann e t)
|
||||
|
||||
forall :: Ord v => v -> Type v -> Type v
|
||||
forall v body = ABT.tm (Forall (ABT.abs v body))
|
||||
|
||||
var :: Ord v => v -> Type v
|
||||
var = ABT.var
|
||||
var :: Ord v => a -> v -> AnnotatedType v a
|
||||
var = ABT.annotatedVar
|
||||
|
||||
existential :: Ord v => v -> Type (TypeVar v)
|
||||
existential v = ABT.var (TypeVar.Existential v)
|
||||
@ -192,24 +194,28 @@ universal' a v = ABT.annotatedVar a (TypeVar.Universal v)
|
||||
v' :: Var v => Text -> Type v
|
||||
v' s = ABT.var (ABT.v' s)
|
||||
|
||||
forall' :: Var v => [Text] -> Type v -> Type v
|
||||
forall' vs body = foldr forall body (map ABT.v' vs)
|
||||
forall' :: Var v => a -> [Text] -> AnnotatedType v a -> AnnotatedType v a
|
||||
forall' a vs body = foldr (forall a) body (Var.named <$> vs)
|
||||
|
||||
foralls :: Var v => [v] -> Type v -> Type v
|
||||
foralls vs body = foldr forall body vs
|
||||
foralls :: Var v => a -> [v] -> AnnotatedType v a -> AnnotatedType v a
|
||||
foralls a vs body = foldr (forall a) body vs
|
||||
|
||||
arrows :: Ord v => [Type v] -> Type v -> Type v
|
||||
arrows ts result = foldr arrow result ts
|
||||
-- Note: `a -> b -> c` parses as `a -> (b -> c)`
|
||||
-- the annotation associated with `b` will be the annotation for the `b -> c`
|
||||
-- node
|
||||
arrows :: Ord v => [(a, AnnotatedType v a)] -> AnnotatedType v a -> AnnotatedType v a
|
||||
arrows ts result = foldr go result ts where
|
||||
go (a,t) result = arrow a t result
|
||||
|
||||
-- The types of effectful computations
|
||||
effect :: Ord v => [Type v] -> Type v -> Type v
|
||||
effect es (Effect' fs t) = ABT.tm (Effect (es ++ fs) t)
|
||||
effect es t = ABT.tm (Effect es t)
|
||||
effect :: Ord v => a -> [AnnotatedType v a] -> AnnotatedType v a -> AnnotatedType v a
|
||||
effect a es (Effect' fs t) = ABT.tm' a (Effect (es ++ fs) t)
|
||||
effect a es t = ABT.tm' a (Effect es t)
|
||||
|
||||
-- The types of first-class effect values
|
||||
-- which get deconstructed in effect handlers.
|
||||
effectV :: Ord v => Type v -> Type v -> Type v
|
||||
effectV e t = apps (builtin "Effect") [e, t]
|
||||
effectV :: Ord v => a -> (a, AnnotatedType v a) -> (a, AnnotatedType v a) -> AnnotatedType v a
|
||||
effectV builtinA e t = apps (builtin builtinA "Effect") [e, t]
|
||||
|
||||
-- Strips effects from a type. E.g. `{e} a` becomes `a`.
|
||||
stripEffect :: AnnotatedType v a -> ([AnnotatedType v a], AnnotatedType v a)
|
||||
@ -219,12 +225,12 @@ stripEffect t = ([], t)
|
||||
-- The type of the flipped function application operator:
|
||||
-- `(a -> (a -> b) -> b)`
|
||||
flipApply :: Var v => Type v -> Type v
|
||||
flipApply t = forall b $ arrow (arrow t (var b)) (var b)
|
||||
flipApply t = forall() b $ arrow() (arrow() t (var() b)) (var() b)
|
||||
where b = ABT.fresh t (ABT.v' "b")
|
||||
|
||||
-- | Bind all free variables with an outer `forall`.
|
||||
generalize :: Ord v => Type v -> Type v
|
||||
generalize t = foldr forall t $ Set.toList (ABT.freeVars t)
|
||||
generalize :: Ord v => AnnotatedType v a -> AnnotatedType v a
|
||||
generalize t = foldr (forall (ABT.annotation t)) t $ Set.toList (ABT.freeVars t)
|
||||
|
||||
instance Hashable1 F where
|
||||
hash1 hashCycle hash e =
|
||||
|
@ -66,15 +66,15 @@ effect = do
|
||||
es <- sepBy (token (string ",")) valueType
|
||||
token_ $ string "}"
|
||||
t <- valueTypeLeaf
|
||||
pure (Type.effect es t)
|
||||
pure (Type.effect() es t)
|
||||
|
||||
tupleOrParenthesized :: Ord v => TypeP v -> TypeP v
|
||||
tupleOrParenthesized rec =
|
||||
parenthesized $ go <$> sepBy (token $ string ",") rec where
|
||||
go [t] = t
|
||||
go types = foldr pair unit types
|
||||
pair t1 t2 = Type.builtin "Pair" `Type.app` t1 `Type.app` t2
|
||||
unit = Type.builtin "()"
|
||||
pair t1 t2 = Type.app() (Type.app() (Type.builtin() "Pair") t1) t2
|
||||
unit = Type.builtin() "()"
|
||||
|
||||
-- "TypeA TypeB TypeC"
|
||||
app :: Ord v => TypeP v -> TypeP v
|
||||
@ -82,14 +82,14 @@ app rec = get >>= \(Aliases aliases) -> do
|
||||
(hd:tl) <- some rec
|
||||
pure $ case hd of
|
||||
Type.Var' v -> case lookup v aliases of
|
||||
Nothing -> foldl' Type.app hd tl
|
||||
Nothing -> foldl' (Type.app()) hd tl
|
||||
Just apply -> apply tl
|
||||
_ -> foldl' Type.app hd tl
|
||||
_ -> foldl' (Type.app()) hd tl
|
||||
|
||||
-- valueType ::= ... | Arrow valueType computationType
|
||||
arrow :: Var v => TypeP v -> TypeP v
|
||||
arrow rec = do
|
||||
t <- foldr1 Type.arrow <$> sepBy1 (token (string "->")) (effect <|> rec)
|
||||
t <- foldr1 (Type.arrow()) <$> sepBy1 (token (string "->")) (effect <|> rec)
|
||||
case t of
|
||||
Type.Arrow' (Type.Effect' _ _) _ -> fail "effect to the left of an ->"
|
||||
_ -> pure t
|
||||
@ -101,7 +101,7 @@ forall rec = do
|
||||
vars <- some $ token varName
|
||||
_ <- token (char '.')
|
||||
t <- rec
|
||||
pure $ Type.forall' (fmap Text.pack vars) t
|
||||
pure $ Type.forall'() (fmap Text.pack vars) t
|
||||
|
||||
varName :: Parser s String
|
||||
varName = do
|
||||
|
@ -371,6 +371,21 @@ extendMarker loc v = do
|
||||
notMember :: Var v => v -> Set (TypeVar v) -> Bool
|
||||
notMember v s = Set.notMember (TypeVar.Universal v) s && Set.notMember (TypeVar.Existential v) s
|
||||
|
||||
-- | Replace any existentials with their solution in the context
|
||||
apply :: Var v => Context v loc -> Type v loc -> Type v loc
|
||||
apply ctx t = _todo
|
||||
--case t of
|
||||
-- Type.Universal' _ -> t
|
||||
-- Type.Ref' _ -> t
|
||||
-- Type.Existential' v ->
|
||||
-- maybe t (\(Type.Monotype t') -> apply ctx t') (lookup v (solved ctx))
|
||||
-- Type.Arrow' i o -> Type.arrow (apply ctx i) (apply ctx o)
|
||||
-- Type.App' x y -> Type.app (apply ctx x) (apply ctx y)
|
||||
-- Type.Ann' v k -> Type.ann (apply ctx v) k
|
||||
-- Type.Effect' es t -> Type.effect (map (apply ctx) es) (apply ctx t)
|
||||
-- Type.ForallNamed' v t' -> Type.forall v (apply ctx t')
|
||||
-- _ -> error $ "Match error in Context.apply: " ++ show t
|
||||
--
|
||||
-- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
|
||||
-- This may have the effect of altering the context.
|
||||
subtype :: forall v loc . (Eq loc, Var v) => loc -> Type v loc -> Type v loc -> M v loc ()
|
||||
@ -418,8 +433,6 @@ subtype loc tx ty = withinSubtype tx ty $
|
||||
es2' = map (apply ctx) es2
|
||||
_abilityCheck' es2' es1'
|
||||
go _ _ _ = fail "not a subtype"
|
||||
apply = _todoApply
|
||||
|
||||
|
||||
-- abilityCheck' :: Var v => [Type v] -> [Type v] -> M v ()
|
||||
-- abilityCheck' ambient requested = do
|
||||
|
Loading…
Reference in New Issue
Block a user