mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-21 07:17:25 +03:00
Term and type are now monomorphic, polymorphism over literals and constraints wasn’t buying much
This commit is contained in:
Paul Chiusano
parent
83e6548633
commit
e44938ee14
25
src/Main.hs
25
src/Main.hs
@ -1,39 +1,30 @@
|
||||
module Main where
|
||||
|
||||
import Unison.Syntax.Term as E
|
||||
import Unison.Syntax.Term.Examples
|
||||
|
||||
import Unison.Syntax.Type as T
|
||||
import Unison.Type.Context as C
|
||||
import Unison.Type.Note as N
|
||||
import Unison.Syntax.Var as V
|
||||
|
||||
expr :: E.Term () a
|
||||
identity :: E.Term
|
||||
identity = E.lam1 $ \x -> x
|
||||
|
||||
expr :: E.Term
|
||||
expr = identity
|
||||
|
||||
identityAnn = E.Ann identity (forall1 $ \x -> T.Arrow x x)
|
||||
-- (subst t' v (T.Universal v'))
|
||||
|
||||
unit :: E.Term () a
|
||||
unit = E.Lit ()
|
||||
|
||||
synthLit :: () -> ()
|
||||
synthLit = id
|
||||
|
||||
showType :: Either N.Note (T.Type () ()) -> String
|
||||
showType :: Either N.Note T.Type -> String
|
||||
showType (Left err) = show err
|
||||
showType (Right a) = show a
|
||||
|
||||
showCtx :: Context () () -> String
|
||||
showCtx = show
|
||||
|
||||
idType :: Type () ()
|
||||
idType :: Type
|
||||
idType = forall1 $ \x -> x
|
||||
|
||||
substIdType :: Type () () -> Type () ()
|
||||
substIdType :: Type -> Type
|
||||
substIdType (Forall v t) = subst t v (T.Universal (V.decr V.bound1))
|
||||
|
||||
main :: IO ()
|
||||
-- main = putStrLn . show $ (idType, substIdType idType)
|
||||
-- main = putStrLn . showCtx . snd $ extendUniversal C.empty
|
||||
main = putStrLn . showType $ C.synthesizeClosed synthLit identityAnn
|
||||
main = putStrLn . showType $ C.synthesizeClosed identityAnn
|
||||
|
||||
@ -4,6 +4,7 @@ import Control.Applicative
|
||||
import Unison.Edit.Term.Action
|
||||
import qualified Unison.Edit.Term.Path as P
|
||||
import qualified Unison.Syntax.Term as E
|
||||
import qualified Unison.Syntax.Term.Literal as EL
|
||||
import qualified Unison.Syntax.Var as V
|
||||
|
||||
-- data Edit e = Edit [(Path, Action e)]
|
||||
@ -11,14 +12,14 @@ import qualified Unison.Syntax.Var as V
|
||||
-- but when applying an edit, have to pick a context
|
||||
-- context is just a function, which editing target must be applied to
|
||||
|
||||
apply :: (l -> Either (Primop l t) (E.Term l t))
|
||||
-> Action (E.Term l t) -> P.Path -> E.Term l t -> Maybe (E.Term l t)
|
||||
apply :: (EL.Literal -> Either Primop E.Term)
|
||||
-> Action E.Term -> P.Path -> E.Term -> Maybe E.Term
|
||||
apply expandLit f loc e = go f where
|
||||
go Abstract = abstract loc e
|
||||
go Step = step expandLit loc e
|
||||
go _ = undefined
|
||||
|
||||
abstract :: P.Path -> E.Term l t -> Maybe (E.Term l t)
|
||||
abstract :: P.Path -> E.Term -> Maybe E.Term
|
||||
abstract loc e =
|
||||
let v = V.decr V.bound1 -- unused
|
||||
in do
|
||||
@ -28,16 +29,16 @@ abstract loc e =
|
||||
|
||||
|
||||
-- data Eval l = Eval {
|
||||
-- step :: forall t. l -> Either (Primop l) (E.Term l t),
|
||||
-- whnf :: forall t. E.Term l t -> Maybe (E.Term l t), -- fail if expr not closed
|
||||
-- hnf :: forall t. E.Term l t -> Maybe (E.Term l t), -- ditto
|
||||
-- step :: forall t. l -> Either (Primop l) Term,
|
||||
-- whnf :: forall t. E.Term -> Maybe Term, -- fail if expr not closed
|
||||
-- hnf :: forall t. E.Term -> Maybe Term, -- ditto
|
||||
-- }
|
||||
data Primop l t = Primop !Int ([E.Term l t] -> E.Term l t)
|
||||
data Primop = Primop !Int ([E.Term] -> E.Term)
|
||||
|
||||
step :: (l -> Either (Primop l t) (E.Term l t))
|
||||
step :: (EL.Literal -> Either Primop E.Term)
|
||||
-> P.Path
|
||||
-> E.Term l t
|
||||
-> Maybe (E.Term l t)
|
||||
-> E.Term
|
||||
-> Maybe E.Term
|
||||
step expandLit loc e = do
|
||||
(e', wrap) <- E.stripAnn <$> P.at loc e
|
||||
pure . wrap $ case e' of
|
||||
|
||||
@ -10,7 +10,7 @@ data E
|
||||
|
||||
newtype Path = Path [E]
|
||||
|
||||
at :: Path -> E.Term l c -> Maybe (E.Term l c)
|
||||
at :: Path -> E.Term -> Maybe E.Term
|
||||
at (Path []) e = Just e
|
||||
at (Path (h:t)) e = go h e where
|
||||
go _ (E.Var _) = Nothing
|
||||
@ -21,7 +21,7 @@ at (Path (h:t)) e = go h e where
|
||||
go Body (E.Lam body) = at (Path t) body
|
||||
go _ _ = Nothing
|
||||
|
||||
set :: E.Term l c -> Path -> E.Term l c -> Maybe (E.Term l c)
|
||||
set :: E.Term -> Path -> E.Term -> Maybe E.Term
|
||||
set e (Path []) _ = Just e
|
||||
set e (Path (h:t)) ctx = go h ctx where
|
||||
go _ (E.Var _) = Nothing
|
||||
@ -32,7 +32,7 @@ set e (Path (h:t)) ctx = go h ctx where
|
||||
go Body (E.Lam body) = E.Lam <$> set e (Path t) body
|
||||
go _ _ = Nothing
|
||||
|
||||
modify :: (E.Term l c -> E.Term l c) -> Path -> E.Term l c -> Maybe (E.Term l c)
|
||||
modify :: (E.Term -> E.Term) -> Path -> E.Term -> Maybe E.Term
|
||||
modify f loc e = do
|
||||
x <- at loc e
|
||||
set (f x) loc e
|
||||
|
||||
@ -1,25 +0,0 @@
|
||||
module Unison.Language.Term (Term, hash, hashes) where
|
||||
|
||||
import qualified Unison.Language.Type as T
|
||||
import qualified Unison.Syntax.Hash as H
|
||||
import qualified Unison.Syntax.Term as ST
|
||||
import qualified Unison.Language.Term.Literal as L
|
||||
|
||||
-- | A term in the Unison language
|
||||
type Term = ST.Term L.Literal T.Type
|
||||
|
||||
-- | Computes the nameless hash of the given term
|
||||
hash :: Term -> H.Hash
|
||||
hash e = H.term hashLit T.hash e
|
||||
|
||||
-- | Computes the nameless hash of the given terms, where
|
||||
-- the terms may have mutual dependencies
|
||||
hashes :: [Term] -> [H.Hash]
|
||||
hashes e = H.terms hashLit T.hash e
|
||||
|
||||
hashLit :: L.Literal -> H.Hash
|
||||
hashLit (L.Hash h) = h
|
||||
hashLit (L.Number n) = H.zero `H.append` H.hashDouble n
|
||||
hashLit (L.String s) = H.one `H.append` H.hashText s
|
||||
hashLit (L.Vector vec) = H.two `H.append` go vec where
|
||||
go vec = error "todo: hashLit vector"
|
||||
@ -1,28 +0,0 @@
|
||||
module Unison.Language.Type (Type, hash, hashes) where
|
||||
|
||||
import qualified Unison.Syntax.Type as ST
|
||||
import qualified Unison.Syntax.Hash as H
|
||||
import qualified Unison.Language.Type.Literal as L
|
||||
|
||||
-- | A type in the Unison language
|
||||
type Type = ST.Type L.Literal ()
|
||||
|
||||
-- | Computes the nameless hash of the given type
|
||||
hash :: Type -> H.Hash
|
||||
hash t = H.typ hashLit hashConstraint t
|
||||
|
||||
-- | Computes the nameless hash of the given types, where
|
||||
-- the types may have mutual dependencies
|
||||
hashes :: [Type] -> [H.Hash]
|
||||
hashes ts = H.types hashLit hashConstraint ts
|
||||
|
||||
-- private
|
||||
|
||||
hashLit :: L.Literal -> H.Hash
|
||||
hashLit (L.Hash h) = h
|
||||
hashLit L.Number = H.zero
|
||||
hashLit L.String = H.one
|
||||
hashLit L.Vector = H.two
|
||||
|
||||
hashConstraint :: () -> H.Hash
|
||||
hashConstraint _ = H.zero
|
||||
@ -2,7 +2,7 @@ module Unison.Node.Panel where
|
||||
|
||||
import qualified Data.Map as M
|
||||
import Unison.Node.Metadata as D
|
||||
import Unison.Language.Layout as L
|
||||
import Unison.Syntax.Layout as L
|
||||
|
||||
-- | Represents a view of a collection of Unison types in @t@ and
|
||||
-- terms in @e@, with hashes of type @k@. This structure can in principle be
|
||||
|
||||
@ -1,10 +1 @@
|
||||
module Unison.Syntax (
|
||||
module Unison.Syntax.Term,
|
||||
module Unison.Syntax.Literal
|
||||
) where
|
||||
|
||||
import Unison.Syntax.Term
|
||||
import Unison.Syntax.Literal
|
||||
|
||||
x :: Int
|
||||
x = 2
|
||||
module Unison.Syntax where
|
||||
|
||||
@ -1,14 +1,11 @@
|
||||
module Unison.Syntax.Hash (
|
||||
Hash,
|
||||
append, finalize, hashDouble, hashText,
|
||||
zero, one, two, three,
|
||||
term, terms, typ, types) where
|
||||
zero, one, two, three) where
|
||||
|
||||
import Data.Word (Word8)
|
||||
import qualified Data.ByteString as B
|
||||
import qualified Data.Text as T
|
||||
import Unison.Syntax.Term as E
|
||||
import Unison.Syntax.Type as T
|
||||
|
||||
-- | Hash which uniquely identifies a Unison type or term
|
||||
newtype Hash = Hash B.ByteString deriving (Eq,Show,Ord)
|
||||
@ -25,33 +22,6 @@ hashText = error "todo: hashText"
|
||||
finalize :: Hash -> B.ByteString
|
||||
finalize (Hash bs) = bs
|
||||
|
||||
-- | Compute a `Hash` for the given `Term`
|
||||
term :: (l -> Hash)
|
||||
-> (t -> Hash)
|
||||
-> E.Term l t
|
||||
-> Hash
|
||||
term hashLit hashTyp e = error "todo: Hash.term"
|
||||
|
||||
-- | Compute a `Hash` for a mutually recursive list of terms
|
||||
terms :: (l -> Hash)
|
||||
-> (t -> Hash)
|
||||
-> [E.Term l t]
|
||||
-> [Hash]
|
||||
terms hashLit hashTyp es = error "todo: Hash.terms"
|
||||
|
||||
typ :: (l -> Hash)
|
||||
-> (c -> Hash)
|
||||
-> T.Type l c
|
||||
-> Hash
|
||||
typ hashLit hashConstraint t = error "todo: Hash.typ"
|
||||
|
||||
-- | Compute a `Hash` for a mutually recursive list of types
|
||||
types :: (l -> Hash)
|
||||
-> (c -> Hash)
|
||||
-> [T.Type l c]
|
||||
-> [Hash]
|
||||
types hashLit hashConstraint ts = error "todo: Hash.types"
|
||||
|
||||
word8 :: Word8 -> Hash
|
||||
word8 byte = Hash (B.singleton byte)
|
||||
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
module Unison.Language.Layout where
|
||||
module Unison.Syntax.Layout where
|
||||
|
||||
import Unison.Language.Layout.Style
|
||||
import Unison.Syntax.Layout.Style
|
||||
import Data.Text
|
||||
|
||||
{-
|
||||
@ -31,4 +31,3 @@ data Layout k
|
||||
| Vertical [Layout k] -- ^ Vertical flow, each child takes up its preferred space
|
||||
| Class Text (Layout k) -- ^ Attach a "class" attribute to this 'Layout'
|
||||
| Id Text (Layout k) -- ^ Attach an "id" attribute to this 'Layout'
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
module Unison.Language.Layout.Style where
|
||||
module Unison.Syntax.Layout.Style where
|
||||
|
||||
import Data.Text
|
||||
|
||||
@ -1,4 +0,0 @@
|
||||
module Unison.Syntax.Literal where
|
||||
|
||||
data Literal = Int Int
|
||||
deriving (Eq,Ord,Show,Read)
|
||||
@ -6,18 +6,22 @@
|
||||
module Unison.Syntax.Term where
|
||||
|
||||
import Control.Applicative
|
||||
import qualified Data.Text as Txt
|
||||
import Unison.Syntax.Var as V
|
||||
import qualified Unison.Syntax.Hash as H
|
||||
import qualified Unison.Syntax.Type as T
|
||||
import qualified Unison.Syntax.Term.Literal as L
|
||||
|
||||
-- | Terms with literals in `l` and type annotations in `t`
|
||||
data Term l t
|
||||
-- | Terms in the Unison language
|
||||
data Term
|
||||
= Var V.Var
|
||||
| Lit l
|
||||
| App (Term l t) (Term l t)
|
||||
| Ann (Term l t) t
|
||||
| Lam (Term l t)
|
||||
| Lit L.Literal
|
||||
| App Term Term
|
||||
| Ann Term T.Type
|
||||
| Lam Term
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
abstract :: V.Var -> Term l t -> Term l t
|
||||
abstract :: V.Var -> Term -> Term
|
||||
abstract v = go V.bound1 where
|
||||
go _ l@(Lit _) = l
|
||||
go n (App f arg) = App (go n f) (go n arg)
|
||||
@ -26,17 +30,17 @@ abstract v = go V.bound1 where
|
||||
go n (Ann e t) = Ann (go n e) t
|
||||
go n (Lam body) = Lam (go (V.succ n) body)
|
||||
|
||||
ap1 :: Term l t -> Term l t -> Maybe (Term l t)
|
||||
ap1 :: Term -> Term -> Maybe Term
|
||||
ap1 (Lam body) t = Just (subst1 body t)
|
||||
ap1 _ _ = Nothing
|
||||
|
||||
bound1 :: Term l t
|
||||
bound1 :: Term
|
||||
bound1 = Var V.bound1
|
||||
|
||||
collect :: Applicative f
|
||||
=> (V.Var -> f (Term l t))
|
||||
-> Term l t
|
||||
-> f (Term l t)
|
||||
=> (V.Var -> f Term)
|
||||
-> Term
|
||||
-> f Term
|
||||
collect f = go where
|
||||
go e = case e of
|
||||
Var v -> f v
|
||||
@ -45,17 +49,17 @@ collect f = go where
|
||||
Ann e' t -> Ann <$> go e' <*> pure t
|
||||
Lam body -> Lam <$> go body
|
||||
|
||||
lam1 :: (Term l t -> Term l t) -> Term l t
|
||||
lam1 :: (Term -> Term) -> Term
|
||||
lam1 f = let v = V.decr V.bound1 -- unused
|
||||
in Lam . abstract v . f $ Var v
|
||||
|
||||
lam2 :: (Term l t -> Term l t -> Term l t) -> Term l t
|
||||
lam2 :: (Term -> Term -> Term) -> Term
|
||||
lam2 f =
|
||||
let v = V.decr V.bound1 -- unused
|
||||
v2 = V.decr v
|
||||
in Lam (abstract v (Lam (abstract v2 $ f (Var v) (Var v2))))
|
||||
|
||||
lam3 :: (Term l t -> Term l t -> Term l t -> Term l t) -> Term l t
|
||||
lam3 :: (Term -> Term -> Term -> Term) -> Term
|
||||
lam3 f =
|
||||
let v = V.decr V.bound1 -- unused
|
||||
v2 = V.decr v
|
||||
@ -63,7 +67,7 @@ lam3 f =
|
||||
in Lam (abstract v (Lam (abstract v2 (Lam (abstract v3 $ f (Var v) (Var v2) (Var v3))))))
|
||||
|
||||
-- subst1 f x
|
||||
subst1 :: Term l t -> Term l t -> Term l t
|
||||
subst1 :: Term -> Term -> Term
|
||||
subst1 = go V.bound1 where
|
||||
go ind body e = case body of
|
||||
Var v | v == ind -> e
|
||||
@ -73,21 +77,46 @@ subst1 = go V.bound1 where
|
||||
Ann body' t -> Ann (go ind body' e) t
|
||||
Lam body' -> Lam (go (V.succ ind) body' e)
|
||||
|
||||
vars :: Term l t -> [V.Var]
|
||||
vars :: Term -> [V.Var]
|
||||
vars e = getConst $ collect (\v -> Const [v]) e
|
||||
|
||||
stripAnn :: Term l t -> (Term l t, Term l t -> Term l t)
|
||||
stripAnn :: Term -> (Term, Term -> Term)
|
||||
stripAnn (Ann e t) = (e, \e' -> Ann e' t)
|
||||
stripAnn e = (e, id)
|
||||
|
||||
-- arguments 'f x y z' == '[x, y, z]'
|
||||
arguments :: Term l t -> [Term l t]
|
||||
arguments :: Term -> [Term]
|
||||
arguments (App f x) = arguments f ++ [x]
|
||||
arguments _ = []
|
||||
|
||||
betaReduce :: Term l t -> Term l t
|
||||
betaReduce :: Term -> Term
|
||||
betaReduce (App (Lam f) arg) = subst1 f arg
|
||||
betaReduce e = e
|
||||
|
||||
applyN :: Term l t -> [Term l t] -> Term l t
|
||||
applyN :: Term -> [Term] -> Term
|
||||
applyN f = foldl App f
|
||||
|
||||
number :: Double -> Term
|
||||
number n = Lit (L.Number n)
|
||||
|
||||
string :: String -> Term
|
||||
string s = Lit (L.String (Txt.pack s))
|
||||
|
||||
text :: Txt.Text -> Term
|
||||
text s = Lit (L.String s)
|
||||
|
||||
-- | Computes the nameless hash of the given term
|
||||
hash :: Term -> H.Hash
|
||||
hash e = error "todo: Term.hash"
|
||||
|
||||
-- | Computes the nameless hash of the given terms, where
|
||||
-- the terms may have mutual dependencies
|
||||
hashes :: [Term] -> [H.Hash]
|
||||
hashes e = error "todo: Term.hashes"
|
||||
|
||||
hashLit :: L.Literal -> H.Hash
|
||||
hashLit (L.Hash h) = h
|
||||
hashLit (L.Number n) = H.zero `H.append` H.hashDouble n
|
||||
hashLit (L.String s) = H.one `H.append` H.hashText s
|
||||
hashLit (L.Vector vec) = H.two `H.append` go vec where
|
||||
go vec = error "todo: hashLit vector"
|
||||
|
||||
@ -1,6 +0,0 @@
|
||||
module Unison.Syntax.Term.Examples where
|
||||
|
||||
import Unison.Syntax.Term
|
||||
|
||||
identity :: Term l t
|
||||
identity = lam1 $ \x -> x
|
||||
@ -1,4 +1,4 @@
|
||||
module Unison.Language.Term.Literal where
|
||||
module Unison.Syntax.Term.Literal where
|
||||
|
||||
import Data.Text
|
||||
import Data.Vector.Unboxed as V
|
||||
@ -9,3 +9,4 @@ data Literal
|
||||
| Number Double
|
||||
| String Text
|
||||
| Vector (V.Vector Double)
|
||||
deriving (Eq,Ord,Show)
|
||||
@ -10,32 +10,28 @@ module Unison.Syntax.Type where
|
||||
|
||||
import Control.Applicative
|
||||
import qualified Data.Set as S
|
||||
import qualified Unison.Syntax.Var as V
|
||||
import qualified Unison.Syntax.Hash as H
|
||||
import qualified Unison.Syntax.Kind as K
|
||||
import qualified Unison.Syntax.Type.Literal as L
|
||||
import qualified Unison.Syntax.Var as V
|
||||
|
||||
-- constructor is private not exported
|
||||
data Monotype l c = Monotype { getPolytype :: Type l c }
|
||||
deriving instance (Eq l, Eq c) => Eq (Monotype l c)
|
||||
deriving instance (Ord l, Ord c) => Ord (Monotype l c)
|
||||
instance (Show l, Show c) => Show (Monotype l c) where
|
||||
data Monotype = Monotype { getPolytype :: Type } deriving (Eq,Ord)
|
||||
instance Show Monotype where
|
||||
show (Monotype t) = show t
|
||||
|
||||
-- | Types with literals in `l` and constraints in `c`
|
||||
data Type l c
|
||||
= Unit l
|
||||
| Arrow (Type l c) (Type l c)
|
||||
data Type
|
||||
= Unit L.Literal
|
||||
| Arrow Type Type
|
||||
| Universal V.Var
|
||||
| Existential V.Var
|
||||
| Ann (Type l c) K.Kind
|
||||
| Constrain (Type l c) c
|
||||
| Forall V.Var (Type l c) -- | ^ `DeBruijn 1` is bounded by nearest enclosing `Forall`, `DeBruijn 2` by next enclosing `Forall`, etc
|
||||
| Ann Type K.Kind
|
||||
| Constrain Type () -- todo: constraint language
|
||||
| Forall V.Var Type -- ^ `DeBruijn 1` is bounded by nearest enclosing `Forall`, `DeBruijn 2` by next enclosing `Forall`, etc
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
|
||||
deriving instance (Eq l, Eq c) => Eq (Type l c)
|
||||
deriving instance (Ord l, Ord c) => Ord (Type l c)
|
||||
deriving instance (Show l, Show c) => Show (Type l c)
|
||||
|
||||
trav :: Applicative f => (V.Var -> f V.Var) -> Type l c -> f (Type l c)
|
||||
trav :: Applicative f => (V.Var -> f V.Var) -> Type -> f Type
|
||||
trav _ (Unit l) = pure (Unit l)
|
||||
trav f (Arrow i o) = Arrow <$> trav f i <*> trav f o
|
||||
trav f (Universal v) = Universal <$> f v
|
||||
@ -44,7 +40,7 @@ trav f (Ann t k) = Ann <$> trav f t <*> pure k
|
||||
trav f (Constrain t c) = Constrain <$> trav f t <*> pure c
|
||||
trav f (Forall v fn) = Forall <$> f v <*> trav f fn
|
||||
|
||||
monotype :: Type l c -> Maybe (Monotype l c)
|
||||
monotype :: Type -> Maybe Monotype
|
||||
monotype t = Monotype <$> go t where
|
||||
go (Unit l) = pure (Unit l)
|
||||
go (Arrow i o) = Arrow <$> go i <*> go o
|
||||
@ -54,7 +50,7 @@ monotype t = Monotype <$> go t where
|
||||
go (Constrain t' c) = Constrain <$> go t' <*> pure c
|
||||
go _ = Nothing
|
||||
|
||||
abstract :: V.Var -> Type l c -> Type l c
|
||||
abstract :: V.Var -> Type -> Type
|
||||
abstract v = go V.bound1 where
|
||||
go _ u@(Unit _) = u
|
||||
go n (Arrow i o) = Arrow (go n i) (go n o)
|
||||
@ -67,38 +63,38 @@ abstract v = go V.bound1 where
|
||||
go n (Forall v' fn) = Forall v' (go (V.succ n) fn)
|
||||
|
||||
-- | Type variable which is bound by the nearest enclosing `Forall`
|
||||
bound1 :: Type l c
|
||||
bound1 :: Type
|
||||
bound1 = Universal V.bound1
|
||||
|
||||
-- | HOAS syntax for `Forall` constructor:
|
||||
-- `forall1 $ \x -> Arrow x x`
|
||||
forall1 :: (Type l c -> Type l c) -> Type l c
|
||||
forall1 :: (Type -> Type) -> Type
|
||||
forall1 f = forallN 1 $ \[x] -> f x
|
||||
|
||||
-- | HOAS syntax for `Forall` constructor:
|
||||
-- `forall2 $ \x y -> Arrow (Arrow x y) (Arrow x y)`
|
||||
forall2 :: (Type l c -> Type l c -> Type l c) -> Type l c
|
||||
forall2 :: (Type -> Type -> Type) -> Type
|
||||
forall2 f = forallN 2 $ \[x,y] -> f x y
|
||||
|
||||
-- | HOAS syntax for `Forall` constructor:
|
||||
-- `forall2 $ \x y z -> Arrow (Arrow x y z) (Arrow x y z)`
|
||||
forall3 :: (Type l c -> Type l c -> Type l c -> Type l c) -> Type l c
|
||||
forall3 :: (Type -> Type -> Type -> Type) -> Type
|
||||
forall3 f = forallN 3 $ \[x,y,z] -> f x y z
|
||||
|
||||
-- | HOAS syntax for `Forall` constructor:
|
||||
-- `forallN 3 $ \[x,y,z] -> Arrow x (Arrow y z)`
|
||||
forallN :: Int -> ([Type l c] -> Type l c) -> Type l c
|
||||
forallN :: Int -> ([Type] -> Type) -> Type
|
||||
forallN n f | n > 0 =
|
||||
let vars = take n (tail $ iterate V.decr V.bound1)
|
||||
inner = f (map Universal vars)
|
||||
in foldr (\v body -> Forall V.bound1 (abstract v body)) inner vars
|
||||
forallN n _ | otherwise = error $ "forallN " ++ show n
|
||||
|
||||
subst1 :: Type l c -> Type l c -> Type l c
|
||||
subst1 :: Type -> Type -> Type
|
||||
subst1 fn arg = subst fn V.bound1 arg
|
||||
|
||||
-- | mnemonic `subst fn var=arg`
|
||||
subst :: Type l c -> V.Var -> Type l c -> Type l c
|
||||
subst :: Type -> V.Var -> Type -> Type
|
||||
subst fn var arg = case fn of
|
||||
Unit l -> Unit l
|
||||
Arrow i o -> Arrow (subst i var arg) (subst o var arg)
|
||||
@ -111,7 +107,7 @@ subst fn var arg = case fn of
|
||||
Forall v fn' -> Forall v (subst fn' (V.succ var) arg)
|
||||
|
||||
-- | The set of unbound variables in this type
|
||||
freeVars :: Type l c -> S.Set V.Var
|
||||
freeVars :: Type -> S.Set V.Var
|
||||
freeVars t = case t of
|
||||
Unit _ -> S.empty
|
||||
Arrow i o -> S.union (freeVars i) (freeVars o)
|
||||
@ -120,3 +116,9 @@ freeVars t = case t of
|
||||
Ann fn _ -> freeVars fn
|
||||
Constrain fn _ -> freeVars fn
|
||||
Forall v fn -> S.delete v (freeVars fn)
|
||||
|
||||
hash :: Type -> H.Hash
|
||||
hash _ = error "todo: Type.hash"
|
||||
|
||||
hashes :: [Type] -> H.Hash
|
||||
hashes _ = error "todo: Type.hashes"
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
module Unison.Language.Type.Literal where
|
||||
module Unison.Syntax.Type.Literal where
|
||||
|
||||
import Unison.Syntax.Hash as H
|
||||
|
||||
@ -8,3 +8,4 @@ data Literal
|
||||
| Number
|
||||
| String
|
||||
| Vector
|
||||
deriving (Eq,Ord,Show)
|
||||
@ -11,42 +11,43 @@ import qualified Data.Set as S
|
||||
import Unison.Syntax.Type as T
|
||||
import qualified Unison.Syntax.Term as Term
|
||||
import Unison.Syntax.Term (Term)
|
||||
import qualified Unison.Syntax.Type.Literal as TL
|
||||
import qualified Unison.Syntax.Term.Literal as EL
|
||||
import Unison.Syntax.Var as V
|
||||
import Unison.Type.Context.Element as E
|
||||
import Unison.Type.Note
|
||||
import Debug.Trace
|
||||
|
||||
-- | An ordered algorithmic context
|
||||
-- Context variables will be negative, while 'normal' DeBruijn
|
||||
-- will be positive, so we don't generally need to worry about
|
||||
-- getting accidental collisions when applying a context to
|
||||
-- a type
|
||||
data Context l c = Context V.Var [Element l c]
|
||||
data Context = Context V.Var [Element]
|
||||
|
||||
instance (Show l, Show c) => Show (Context l c) where
|
||||
instance Show Context where
|
||||
show (Context n es) = "Context (" ++ show n ++ ") " ++ show (reverse es)
|
||||
|
||||
empty :: Context l c
|
||||
empty :: Context
|
||||
empty = Context bound0 []
|
||||
|
||||
bound0 :: V.Var
|
||||
bound0 = V.decr V.bound1
|
||||
|
||||
context :: [Element l c] -> Context l c
|
||||
context :: [Element] -> Context
|
||||
context xs =
|
||||
let ctx = reverse xs
|
||||
v = fromMaybe bound0 (currentVar ctx)
|
||||
in Context v ctx
|
||||
|
||||
append :: Context l c -> Context l c -> Context l c
|
||||
append :: Context -> Context -> Context
|
||||
append (Context n1 ctx1) (Context n2 ctx2) =
|
||||
let n12 = V.minv n1 n2
|
||||
in Context n12 (ctx2 ++ ctx1)
|
||||
|
||||
fresh :: Context l c -> V.Var
|
||||
fresh :: Context -> V.Var
|
||||
fresh (Context n _) = V.decr n
|
||||
|
||||
fresh3 :: Context l c -> (V.Var, V.Var, V.Var)
|
||||
fresh3 :: Context -> (V.Var, V.Var, V.Var)
|
||||
fresh3 (Context n _) = (a,b,c) where
|
||||
a = V.decr n
|
||||
b = fresh' a
|
||||
@ -56,28 +57,28 @@ fresh' :: V.Var -> V.Var
|
||||
fresh' = V.decr
|
||||
|
||||
-- | Add an element onto the end of this `Context`
|
||||
extend :: Element l c -> Context l c -> Context l c
|
||||
extend :: Element -> Context -> Context
|
||||
extend e ctx = ctx `append` context [e]
|
||||
|
||||
-- | Extend this `Context` with a single universally quantified variable,
|
||||
-- guaranteed to be fresh
|
||||
extendUniversal :: Context l c -> (V.Var, Context l c)
|
||||
extendUniversal :: Context -> (V.Var, Context)
|
||||
extendUniversal (Context n ctx) =
|
||||
let v = V.decr n in (v, Context v (E.Universal v : ctx))
|
||||
|
||||
-- | Extend this `Context` with a single existentially quantified variable,
|
||||
-- guaranteed to be fresh
|
||||
extendExistential :: Context l c -> (V.Var, Context l c)
|
||||
extendExistential :: Context -> (V.Var, Context)
|
||||
extendExistential (Context n ctx) =
|
||||
let v = V.decr n in (v, Context v (E.Universal v : ctx))
|
||||
|
||||
-- | Extend this `Context` with a marker variable, guaranteed to be fresh
|
||||
extendMarker :: Context l c -> (V.Var, Context l c)
|
||||
extendMarker :: Context -> (V.Var, Context)
|
||||
extendMarker (Context n ctx) =
|
||||
let v = V.decr n in (v, Context v ([E.Existential v, E.Marker v] ++ ctx))
|
||||
|
||||
-- | Delete up to and including the given `Element`
|
||||
retract :: Element l c -> Context l c -> Context l c
|
||||
retract :: Element -> Context -> Context
|
||||
retract m (Context _ ctx) =
|
||||
let ctx' = tail (dropWhile (go m) ctx)
|
||||
n' = fromMaybe bound0 (currentVar ctx') -- ok to recycle our variable supply
|
||||
@ -87,55 +88,55 @@ retract m (Context _ ctx) =
|
||||
go _ _ = True
|
||||
in Context n' ctx'
|
||||
|
||||
universals :: Context l c -> [V.Var]
|
||||
universals :: Context -> [V.Var]
|
||||
universals (Context _ ctx) = [v | E.Universal v <- ctx]
|
||||
|
||||
markers :: Context l c -> [V.Var]
|
||||
markers :: Context -> [V.Var]
|
||||
markers (Context _ ctx) = [v | Marker v <- ctx]
|
||||
|
||||
existentials :: Context l c -> [V.Var]
|
||||
existentials :: Context -> [V.Var]
|
||||
existentials (Context _ ctx) = ctx >>= go where
|
||||
go (E.Existential v) = [v]
|
||||
go (E.Solved v _) = [v]
|
||||
go _ = []
|
||||
|
||||
solved :: Context l c -> [(V.Var, Monotype l c)]
|
||||
solved :: Context -> [(V.Var, Monotype)]
|
||||
solved (Context _ ctx) = [(v, sa) | Solved v sa <- ctx]
|
||||
|
||||
unsolved :: Context l c -> [V.Var]
|
||||
unsolved :: Context -> [V.Var]
|
||||
unsolved (Context _ ctx) = [v | E.Existential v <- ctx]
|
||||
|
||||
replace :: Element l c -> Context l c -> Context l c -> Context l c
|
||||
replace :: Element -> Context -> Context -> Context
|
||||
replace e focus ctx = let (l,r) = breakAt e ctx in l `append` focus `append` r
|
||||
|
||||
breakAt :: Element l c -> Context l c -> (Context l c, Context l c)
|
||||
breakAt :: Element -> Context -> (Context, Context)
|
||||
breakAt m (Context _ xs) =
|
||||
let (r, l) = break (=== m) xs
|
||||
in (context (reverse $ drop 1 l), context $ reverse r)
|
||||
|
||||
-- | ordered Γ α β = True <=> Γ[α^][β^]
|
||||
ordered :: Context l c -> V.Var -> V.Var -> Bool
|
||||
ordered :: Context -> V.Var -> V.Var -> Bool
|
||||
ordered ctx v v2 = v `elem` existentials (retract (E.Existential v2) ctx)
|
||||
|
||||
-- | solve (ΓL,α^,ΓR) α τ = (ΓL,α = τ,ΓR)
|
||||
-- If the given existential variable exists in the context,
|
||||
-- we solve it to the given monotype, otherwise return `Nothing`
|
||||
solve :: Context l c -> V.Var -> Monotype l c -> Maybe (Context l c)
|
||||
solve :: Context -> V.Var -> Monotype -> Maybe Context
|
||||
solve ctx v t | wellformedType ctxL (getPolytype t) = Just ctx'
|
||||
| otherwise = Nothing
|
||||
where (ctxL,ctxR) = breakAt (E.Existential v) ctx
|
||||
ctx' = ctxL `append` context [E.Solved v t] `append` ctxR
|
||||
|
||||
bindings :: Context l c -> [(V.Var, Type l c)]
|
||||
bindings :: Context -> [(V.Var, Type)]
|
||||
bindings (Context _ ctx) = [(v,a) | E.Ann v a <- ctx]
|
||||
|
||||
lookupType :: Context l c -> V.Var -> Maybe (Type l c)
|
||||
lookupType :: Context -> V.Var -> Maybe Type
|
||||
lookupType ctx v = lookup v (bindings ctx)
|
||||
|
||||
vars :: Context l c -> [V.Var]
|
||||
vars :: Context -> [V.Var]
|
||||
vars = fmap fst . bindings
|
||||
|
||||
allVars :: [Element l c] -> [V.Var]
|
||||
allVars :: [Element] -> [V.Var]
|
||||
allVars ctx = ctx >>= go where
|
||||
go (E.Solved v _) = [v]
|
||||
go (E.Ann v _) = [v]
|
||||
@ -145,12 +146,12 @@ allVars ctx = ctx >>= go where
|
||||
|
||||
-- TODO: I suspect this can get away with just examining first few elements
|
||||
-- perhaps up to first marker
|
||||
currentVar :: [Element l c] -> Maybe V.Var
|
||||
currentVar :: [Element] -> Maybe V.Var
|
||||
currentVar ctx | L.null ctx = Nothing
|
||||
currentVar ctx | otherwise = Just $ minimum (allVars ctx)
|
||||
|
||||
-- | Check that the type is well formed wrt the given `Context`
|
||||
wellformedType :: Context l c -> Type l c -> Bool
|
||||
wellformedType :: Context -> Type -> Bool
|
||||
wellformedType c t = case t of
|
||||
T.Unit _ -> True
|
||||
T.Universal v -> v `elem` universals c
|
||||
@ -167,7 +168,7 @@ wellformedType c t = case t of
|
||||
-- mentioned in either `Ann` or `Solved` elements must be
|
||||
-- wellformed with respect to the prefix of the context
|
||||
-- leading up to these elements.
|
||||
wellformed :: Context l c -> Bool
|
||||
wellformed :: Context -> Bool
|
||||
wellformed ctx = all go (zipTail ctx) where
|
||||
go (E.Universal v, ctx') = v `notElem` universals ctx'
|
||||
go (E.Existential v, ctx') = v `notElem` existentials ctx'
|
||||
@ -175,12 +176,12 @@ wellformed ctx = all go (zipTail ctx) where
|
||||
go (E.Ann v t, ctx') = v `notElem` vars ctx' && wellformedType ctx' t
|
||||
go (Marker v, ctx') = v `notElem` vars ctx' && v `notElem` existentials ctx'
|
||||
|
||||
zipTail :: Context l c -> [(Element l c, Context l c)]
|
||||
zipTail :: Context -> [(Element, Context)]
|
||||
zipTail (Context n ctx) = zip ctx (map (Context n) $ tail (tails ctx))
|
||||
|
||||
-- invariant is that both input types will have been fully freshened
|
||||
-- before being passed to apply
|
||||
apply :: Context l c -> Type l c -> Type l c
|
||||
apply :: Context -> Type -> Type
|
||||
apply ctx t = case t of
|
||||
T.Universal _ -> t
|
||||
T.Unit _ -> t
|
||||
@ -193,7 +194,7 @@ apply ctx t = case t of
|
||||
|
||||
-- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
|
||||
-- This may have the effect of altering the context.
|
||||
subtype :: (Eq l, Show l, Show c) => Context l c -> Type l c -> Type l c -> Either Note (Context l c)
|
||||
subtype :: Context -> Type -> Type -> Either Note Context
|
||||
subtype ctx tx ty = scope (show tx++" <: "++show ty) (go tx ty) where -- Rules from figure 9
|
||||
go (Unit l) (Unit l2) | l == l2 = pure ctx -- `Unit`
|
||||
go t1@(T.Universal v1) t2@(T.Universal v2) -- `Var`
|
||||
@ -224,7 +225,7 @@ subtype ctx tx ty = scope (show tx++" <: "++show ty) (go tx ty) where -- Rules f
|
||||
-- | Instantiate the given existential such that it is
|
||||
-- a subtype of the given type, updating the context
|
||||
-- in the process.
|
||||
instantiateL :: Context l c -> V.Var -> Type l c -> Either Note (Context l c)
|
||||
instantiateL :: Context -> V.Var -> Type -> Either Note Context
|
||||
instantiateL ctx v t = case monotype t >>= solve ctx v of
|
||||
Just ctx' -> pure ctx' -- InstLSolve
|
||||
Nothing -> case t of
|
||||
@ -249,7 +250,7 @@ instantiateL ctx v t = case monotype t >>= solve ctx v of
|
||||
-- | Instantiate the given existential such that it is
|
||||
-- a subtype of the given type, updating the context
|
||||
-- in the process.
|
||||
instantiateR :: Context l c -> Type l c -> V.Var -> Either Note (Context l c)
|
||||
instantiateR :: Context -> Type -> V.Var -> Either Note Context
|
||||
instantiateR ctx t v = case monotype t >>= solve ctx v of
|
||||
Just ctx' -> pure ctx' -- InstRSolve
|
||||
Nothing -> case t of
|
||||
@ -274,54 +275,52 @@ instantiateR ctx t v = case monotype t >>= solve ctx v of
|
||||
_ -> Left $ note "could not instantiate right"
|
||||
|
||||
-- | Check that under the given context, `e` has type `t`,
|
||||
-- updating the context in the process. Parameterized on
|
||||
-- a function for synthesizing the type of a literal, `l`.
|
||||
check :: (Eq l', Show l', Show l, Show c)
|
||||
=> (l -> l')
|
||||
-> Context l' c
|
||||
-> Term l (Type l' c)
|
||||
-> Type l' c
|
||||
-> Either Note (Context l' c)
|
||||
check synthLit ctx e t | wellformedType ctx t = scope ((show e) ++ ": " ++ show t) $ go e t where
|
||||
go (Term.Lit l) (T.Unit l') | synthLit l == l' = pure ctx -- 1I
|
||||
-- updating the context in the process.
|
||||
check :: Context -> Term -> Type -> Either Note Context
|
||||
check ctx e t | wellformedType ctx t = scope ((show e) ++ ": " ++ show t) $ go e t where
|
||||
-- go (Term.Lit l) (T.Unit l') | synthLit l == l' = pure ctx -- 1I
|
||||
go _ (T.Forall x body) = -- ForallI
|
||||
let (x', ctx') = extendUniversal ctx
|
||||
in retract (E.Universal x') <$> check synthLit ctx' e (T.subst body x (T.Universal x'))
|
||||
in retract (E.Universal x') <$> check ctx' e (T.subst body x (T.Universal x'))
|
||||
go (Term.Lam body) (T.Arrow i o) = -- =>I
|
||||
let x' = fresh ctx
|
||||
v = Term.Var x'
|
||||
ctx' = extend (E.Ann x' i) ctx
|
||||
body' = Term.subst1 body v
|
||||
in retract (E.Ann x' i) <$> check synthLit ctx' body' o
|
||||
in retract (E.Ann x' i) <$> check ctx' body' o
|
||||
go _ _ = do -- Sub
|
||||
(a, ctx') <- synthesize synthLit ctx e
|
||||
(a, ctx') <- synthesize ctx e
|
||||
subtype ctx' (apply ctx' a) (apply ctx' t)
|
||||
check _ _ _ _ = Left $ note "type not well formed wrt context"
|
||||
check _ _ _ = Left $ note "type not well formed wrt context"
|
||||
|
||||
-- | Infer the type of a literal
|
||||
synthLit :: EL.Literal -> Type
|
||||
synthLit lit = T.Unit $ case lit of
|
||||
EL.Hash h -> TL.Hash h
|
||||
EL.Number _ -> TL.Number
|
||||
EL.String _ -> TL.String
|
||||
EL.Vector _ -> TL.Vector
|
||||
|
||||
-- | Synthesize the type of the given term, updating the context
|
||||
-- in the process. Parameterized on a function for synthesizing
|
||||
-- the type of a literal, `l`.
|
||||
synthesize :: (Show c, Show l', Eq l', Show l)
|
||||
=> (l -> l')
|
||||
-> Context l' c
|
||||
-> Term l (Type l' c)
|
||||
-> Either Note (Type l' c, Context l' c)
|
||||
synthesize synthLit ctx e = scope (show e ++ " =>") $ go e where
|
||||
synthesize :: Context -> Term -> Either Note (Type, Context)
|
||||
synthesize ctx e = scope (show e ++ " =>") $ go e where
|
||||
go (Term.Var v) = case lookupType ctx v of -- Var
|
||||
Nothing -> Left $ note "type not in scope"
|
||||
Just t -> pure (t, ctx)
|
||||
go (Term.Ann e' t) = (,) t <$> check synthLit ctx e' t -- Anno
|
||||
go (Term.Lit l) = pure (T.Unit $ synthLit l, ctx) -- 1I=>
|
||||
go (Term.Ann e' t) = (,) t <$> check ctx e' t -- Anno
|
||||
go (Term.Lit l) = pure (synthLit l, ctx) -- 1I=>
|
||||
go (Term.App f arg) = do -- ->E
|
||||
(ft, ctx') <- synthesize synthLit ctx f
|
||||
synthesizeApp synthLit ctx' (apply ctx' ft) arg
|
||||
(ft, ctx') <- synthesize ctx f
|
||||
synthesizeApp ctx' (apply ctx' ft) arg
|
||||
go (Term.Lam body) = -- ->I=> (Full Damas Milner rule)
|
||||
let (arg, i, o) = fresh3 ctx
|
||||
ctxTl = context [E.Marker i, E.Existential i, E.Existential o,
|
||||
E.Ann arg (T.Existential i)]
|
||||
freshVars = tail $ iterate fresh' o
|
||||
in do
|
||||
ctx' <- check synthLit (ctx `append` ctxTl)
|
||||
ctx' <- check (ctx `append` ctxTl)
|
||||
(Term.subst1 body (Term.Var arg))
|
||||
(T.Existential o)
|
||||
pure $ let
|
||||
@ -338,31 +337,24 @@ synthesize synthLit ctx e = scope (show e ++ " =>") $ go e where
|
||||
-- | Synthesize the type of the given term, `arg` given that a function of
|
||||
-- the given type `ft` is being applied to `arg`. Update the conext in
|
||||
-- the process.
|
||||
synthesizeApp :: (Eq l', Show l', Show l, Show c)
|
||||
=> (l -> l')
|
||||
-> Context l' c
|
||||
-> Type l' c
|
||||
-> Term l (Type l' c)
|
||||
-> Either Note (Type l' c, Context l' c)
|
||||
synthesizeApp synthLit ctx ft arg = go ft where
|
||||
synthesizeApp :: Context -> Type -> Term -> Either Note (Type, Context)
|
||||
synthesizeApp ctx ft arg = go ft where
|
||||
go (T.Forall x body) = let x' = fresh ctx -- Forall1App
|
||||
in synthesizeApp synthLit
|
||||
(ctx `append` context [E.Existential x'])
|
||||
in synthesizeApp (ctx `append` context [E.Existential x'])
|
||||
(T.subst body x (T.Existential x'))
|
||||
arg
|
||||
go (T.Arrow i o) = (,) o <$> check synthLit ctx arg i -- ->App
|
||||
go (T.Arrow i o) = (,) o <$> check ctx arg i -- ->App
|
||||
go (T.Existential a) = -- a^App
|
||||
let i = fresh ctx
|
||||
o = fresh' i
|
||||
soln = Monotype (T.Arrow (T.Existential i) (T.Existential o))
|
||||
ctxMid = context [E.Existential o, E.Existential i, E.Solved a soln]
|
||||
in (,) (T.Existential o) <$>
|
||||
check synthLit (replace (E.Existential a) ctxMid ctx)
|
||||
check (replace (E.Existential a) ctxMid ctx)
|
||||
arg
|
||||
(T.Existential i)
|
||||
go _ = Left $ note "unable to synthesize type of application"
|
||||
|
||||
synthesizeClosed :: (Show l', Eq l', Show l, Show c)
|
||||
=> (l -> l') -> Term l (Type l' c) -> Either Note (Type l' c)
|
||||
synthesizeClosed synthLit term = go <$> synthesize synthLit (context []) term
|
||||
synthesizeClosed :: Term -> Either Note Type
|
||||
synthesizeClosed term = go <$> synthesize (context []) term
|
||||
where go (t, ctx) = apply ctx t
|
||||
|
||||
@ -12,53 +12,53 @@ import qualified Unison.Syntax.Type as T
|
||||
import qualified Unison.Syntax.Var as V
|
||||
|
||||
-- | Elements of an algorithmic context
|
||||
data Element l c where
|
||||
Universal :: V.Var -> Element l c -- | ^ `v` is universally quantified
|
||||
Existential :: V.Var -> Element l c -- | ^ `v` existential and unsolved
|
||||
Solved :: V.Var -> T.Monotype l c -> Element l c -- | ^ `v` is solved to some monotype
|
||||
Ann :: V.Var -> T.Type l c -> Element l c -- | ^ `v` has type `a`, which may be quantified
|
||||
Marker :: V.Var -> Element l c -- | ^ used for scoping
|
||||
data Element where
|
||||
Universal :: V.Var -> Element -- | ^ `v` is universally quantified
|
||||
Existential :: V.Var -> Element -- | ^ `v` existential and unsolved
|
||||
Solved :: V.Var -> T.Monotype -> Element -- | ^ `v` is solved to some monotype
|
||||
Ann :: V.Var -> T.Type -> Element -- | ^ `v` has type `a`, which may be quantified
|
||||
Marker :: V.Var -> Element -- | ^ used for scoping
|
||||
|
||||
instance (Show l, Show c) => Show (Element l c) where
|
||||
instance Show Element where
|
||||
show (Universal v) = show v
|
||||
show (Existential v) = "^"++show v
|
||||
show (Solved v t) = "^"++show v++"="++show t
|
||||
show (Ann v t) = show v++":"++show t
|
||||
show (Marker v) = "|"++show v++"|"
|
||||
|
||||
(===) :: Element l c -> Element l c -> Bool
|
||||
(===) :: Element -> Element -> Bool
|
||||
Existential v === Existential v2 | v == v2 = True
|
||||
Universal v === Universal v2 | v == v2 = True
|
||||
Marker v === Marker v2 | v == v2 = True
|
||||
_ === _ = False
|
||||
|
||||
(!==) :: Element l c -> Element l c -> Bool
|
||||
(!==) :: Element -> Element -> Bool
|
||||
e1 !== e2 = not (e1 === e2)
|
||||
|
||||
_Universal :: Simple Prism (Element l c) V.Var
|
||||
_Universal :: Simple Prism Element V.Var
|
||||
_Universal = prism Universal go where
|
||||
go (Universal v) = Right v
|
||||
go e = Left e
|
||||
|
||||
_Existential :: Simple Prism (Element l c) V.Var
|
||||
_Existential :: Simple Prism Element V.Var
|
||||
_Existential = prism Existential go where
|
||||
go (Existential v) = Right v
|
||||
go e = Left e
|
||||
|
||||
_Solved :: Simple Prism (Element l c) (V.Var, T.Monotype l c)
|
||||
_Solved :: Simple Prism Element (V.Var, T.Monotype)
|
||||
_Solved = prism (uncurry Solved) go where
|
||||
go (Solved v t) = Right (v, t)
|
||||
go e = Left e
|
||||
|
||||
_Ann :: Simple Prism (Element l c) (V.Var, T.Type l c)
|
||||
_Ann :: Simple Prism Element (V.Var, T.Type)
|
||||
_Ann = prism (uncurry Ann) go where
|
||||
go (Ann v t) = Right (v, t)
|
||||
go e = Left e
|
||||
|
||||
_Marker :: Simple Prism (Element l c) V.Var
|
||||
_Marker :: Simple Prism Element V.Var
|
||||
_Marker = prism Marker go where
|
||||
go (Marker v) = Right v
|
||||
go e = Left e
|
||||
|
||||
deriving instance (Ord l, Ord c) => Ord (Element l c)
|
||||
deriving instance (Eq l, Eq c) => Eq (Element l c)
|
||||
deriving instance Ord Element
|
||||
deriving instance Eq Element
|
||||
|
||||
10
unison.cabal
10
unison.cabal
@ -52,12 +52,6 @@ library
|
||||
Unison.Edit.Term.Path
|
||||
Unison.Edit.Term.Edit
|
||||
Unison.Edit.Type.Path
|
||||
Unison.Language.Layout
|
||||
Unison.Language.Layout.Style
|
||||
Unison.Language.Term
|
||||
Unison.Language.Term.Literal
|
||||
Unison.Language.Type
|
||||
Unison.Language.Type.Literal
|
||||
Unison.Node
|
||||
Unison.Node.Implementations.State
|
||||
Unison.Node.Metadata
|
||||
@ -66,10 +60,10 @@ library
|
||||
Unison.Syntax.Hash
|
||||
Unison.Syntax.Index
|
||||
Unison.Syntax.Kind
|
||||
Unison.Syntax.Literal
|
||||
Unison.Syntax.Term
|
||||
Unison.Syntax.Term.Examples
|
||||
Unison.Syntax.Term.Literal
|
||||
Unison.Syntax.Type
|
||||
Unison.Syntax.Type.Literal
|
||||
Unison.Syntax.Var
|
||||
Unison.Type.Context
|
||||
Unison.Type.Context.Element
|
||||
|
||||
Loading…
Reference in New Issue
Block a user