mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-23 16:28:02 +03:00
Debugging letrec typechecking
This commit is contained in:
parent
19c20553f1
commit
d03e48a77b
@ -393,7 +393,7 @@ subtract _ t1s t2s =
|
|||||||
instance (Show1 f, Var v) => Show (Term f v a) where
|
instance (Show1 f, Var v) => Show (Term f v a) where
|
||||||
-- annotations not shown
|
-- annotations not shown
|
||||||
showsPrec p (Term _ _ out) = case out of
|
showsPrec p (Term _ _ out) = case out of
|
||||||
Var v -> (Text.unpack (Var.shortName v) ++)
|
Var v -> (show v ++)
|
||||||
Cycle body -> showsPrec p body
|
Cycle body -> showsPrec p body
|
||||||
Abs v body -> showParen True $ (Text.unpack (Var.shortName v) ++) . showString ". " . showsPrec p body
|
Abs v body -> showParen True $ (Text.unpack (Var.shortName v) ++) . showString ". " . showsPrec p body
|
||||||
Tm f -> showsPrec1 p f
|
Tm f -> showsPrec1 p f
|
||||||
|
@ -250,7 +250,7 @@ lam'' vs body = foldr lam body vs
|
|||||||
-- | Smart constructor for let rec blocks. Each binding in the block may
|
-- | Smart constructor for let rec blocks. Each binding in the block may
|
||||||
-- reference any other binding in the block in its body (including itself),
|
-- reference any other binding in the block in its body (including itself),
|
||||||
-- and the output expression may also reference any binding in the block.
|
-- and the output expression may also reference any binding in the block.
|
||||||
letRec :: Ord v => [(v,Term v)] -> Term v -> Term v
|
letRec :: Ord v => [(v, Term' vt v)] -> Term' vt v -> Term' vt v
|
||||||
letRec [] e = e
|
letRec [] e = e
|
||||||
letRec bindings e = ABT.cycle (foldr ABT.abs z (map fst bindings))
|
letRec bindings e = ABT.cycle (foldr ABT.abs z (map fst bindings))
|
||||||
where
|
where
|
||||||
|
@ -13,7 +13,7 @@ underlying (Universal v) = v
|
|||||||
underlying (Existential v) = v
|
underlying (Existential v) = v
|
||||||
|
|
||||||
instance Show v => Show (TypeVar v) where
|
instance Show v => Show (TypeVar v) where
|
||||||
show (Universal v) = show v
|
show (Universal v) = "@" ++ show v
|
||||||
show (Existential v) = "'" ++ show v
|
show (Existential v) = "'" ++ show v
|
||||||
|
|
||||||
instance Var v => Var (TypeVar v) where
|
instance Var v => Var (TypeVar v) where
|
||||||
|
@ -6,7 +6,7 @@ import Data.Maybe
|
|||||||
import Data.Set (Set)
|
import Data.Set (Set)
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
import qualified Unison.ABT as ABT
|
import qualified Unison.ABT as ABT
|
||||||
import Unison.Term (Term)
|
import Unison.Term (Term')
|
||||||
import qualified Unison.Term as Term
|
import qualified Unison.Term as Term
|
||||||
import Unison.Var (Var)
|
import Unison.Var (Var)
|
||||||
|
|
||||||
@ -63,7 +63,7 @@ components' freeVars bs =
|
|||||||
--
|
--
|
||||||
-- Gets rid of the let rec and replaces it with an ordinary `let`, such
|
-- Gets rid of the let rec and replaces it with an ordinary `let`, such
|
||||||
-- that `id` is suitably generalized.
|
-- that `id` is suitably generalized.
|
||||||
minimize :: Var v => Term v -> Maybe (Term v)
|
minimize :: Var v => Term' vt v -> Maybe (Term' vt v)
|
||||||
minimize (Term.LetRecNamed' bs e) = case components bs of
|
minimize (Term.LetRecNamed' bs e) = case components bs of
|
||||||
[_single] -> Nothing
|
[_single] -> Nothing
|
||||||
cs -> Just $ foldr mklet e cs where
|
cs -> Just $ foldr mklet e cs where
|
||||||
@ -73,5 +73,5 @@ minimize (Term.LetRecNamed' bs e) = case components bs of
|
|||||||
mklet cycle e = Term.letRec cycle e
|
mklet cycle e = Term.letRec cycle e
|
||||||
minimize _ = Nothing
|
minimize _ = Nothing
|
||||||
|
|
||||||
minimize' :: Var v => Term v -> Term v
|
minimize' :: Var v => Term' vt v -> Term' vt v
|
||||||
minimize' term = fromMaybe term (minimize term)
|
minimize' term = fromMaybe term (minimize term)
|
||||||
|
@ -42,6 +42,7 @@ import qualified Unison.Term as Term
|
|||||||
import qualified Unison.Type as Type
|
import qualified Unison.Type as Type
|
||||||
import Unison.TypeVar (TypeVar)
|
import Unison.TypeVar (TypeVar)
|
||||||
import qualified Unison.TypeVar as TypeVar
|
import qualified Unison.TypeVar as TypeVar
|
||||||
|
import Unison.Typechecker.Components (minimize')
|
||||||
import Unison.Var (Var)
|
import Unison.Var (Var)
|
||||||
import qualified Unison.Var as Var
|
import qualified Unison.Var as Var
|
||||||
-- uncomment for debugging
|
-- uncomment for debugging
|
||||||
@ -67,10 +68,10 @@ data Element v
|
|||||||
|
|
||||||
instance Var v => Show (Element v) where
|
instance Var v => Show (Element v) where
|
||||||
show (Var v) = case v of
|
show (Var v) = case v of
|
||||||
TypeVar.Universal v -> Text.unpack (Var.shortName v)
|
TypeVar.Universal x -> "@" <> show x
|
||||||
TypeVar.Existential v -> "'"++Text.unpack (Var.shortName v)
|
TypeVar.Existential x -> "'" ++ show x
|
||||||
show (Solved v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t
|
show (Solved v t) = "'"++Text.unpack (Var.shortName v)++" = "++show t
|
||||||
show (Ann v t) = Text.unpack (Var.shortName v)++" : "++show t
|
show (Ann v t) = Text.unpack (Var.shortName v) ++ " : " ++ show t
|
||||||
show (Marker v) = "|"++Text.unpack (Var.shortName v)++"|"
|
show (Marker v) = "|"++Text.unpack (Var.shortName v)++"|"
|
||||||
|
|
||||||
(===) :: Eq v => Element v -> Element v -> Bool
|
(===) :: Eq v => Element v -> Element v -> Bool
|
||||||
@ -546,7 +547,9 @@ instantiateR t v = getContext >>= \ctx -> case Type.monotype t >>= solve ctx v o
|
|||||||
setContext $ ctx `append` context [Marker x', Existential x']
|
setContext $ ctx `append` context [Marker x', Existential x']
|
||||||
instantiateR (ABT.bind body (Type.existential x')) v
|
instantiateR (ABT.bind body (Type.existential x')) v
|
||||||
modifyContext (retract (Marker x'))
|
modifyContext (retract (Marker x'))
|
||||||
_ -> fail $ "could not instantiate right " ++ show t
|
_ -> do
|
||||||
|
logContext ("failed: instantiateR " <> show t <> " " <> show v)
|
||||||
|
fail $ "could not instantiate right " ++ show t
|
||||||
|
|
||||||
withEffects :: [Type v] -> M v a -> M v a
|
withEffects :: [Type v] -> M v a -> M v a
|
||||||
withEffects abilities' m =
|
withEffects abilities' m =
|
||||||
@ -593,7 +596,7 @@ check e t = getContext >>= \ctx -> scope ("check: " ++ show e ++ ": " ++ show
|
|||||||
a <- synthesize e; ctx <- getContext
|
a <- synthesize e; ctx <- getContext
|
||||||
subtype (apply ctx a) (apply ctx t)
|
subtype (apply ctx a) (apply ctx t)
|
||||||
(as, t') = Type.stripEffect t
|
(as, t') = Type.stripEffect t
|
||||||
in withEffects as $ go e t'
|
in withEffects as $ go (minimize' e) t'
|
||||||
else
|
else
|
||||||
scope ("context: " ++ show ctx) .
|
scope ("context: " ++ show ctx) .
|
||||||
scope ("term: " ++ show e) .
|
scope ("term: " ++ show e) .
|
||||||
@ -618,6 +621,7 @@ annotateLetRecBindings letrec = do
|
|||||||
-- annotate each term variable w/ corresponding existential
|
-- annotate each term variable w/ corresponding existential
|
||||||
-- [marker e1, 'e1, 'e2, ... v1 : 'e1, v2 : 'e2 ...]
|
-- [marker e1, 'e1, 'e2, ... v1 : 'e1, v2 : 'e2 ...]
|
||||||
appendContext $ context (Marker e1 : map Existential es ++ zipWith Ann vs (map Type.existential es))
|
appendContext $ context (Marker e1 : map Existential es ++ zipWith Ann vs (map Type.existential es))
|
||||||
|
logContext "annotating letrec bindings"
|
||||||
-- check each `bi` against `ei`; sequencing resulting contexts
|
-- check each `bi` against `ei`; sequencing resulting contexts
|
||||||
Foldable.traverse_ (\(e,(_,binding)) -> check binding (Type.existential e)) (zip es bindings)
|
Foldable.traverse_ (\(e,(_,binding)) -> check binding (Type.existential e)) (zip es bindings)
|
||||||
-- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`;
|
-- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`;
|
||||||
@ -632,7 +636,8 @@ annotateLetRecBindings letrec = do
|
|||||||
-- | Synthesize the type of the given term, updating the context in the process.
|
-- | Synthesize the type of the given term, updating the context in the process.
|
||||||
-- | Figure 11 from the paper
|
-- | Figure 11 from the paper
|
||||||
synthesize :: Var v => Term v -> M v (Type v)
|
synthesize :: Var v => Term v -> M v (Type v)
|
||||||
synthesize e = scope ("synth: " ++ show e) $ logContext "synthesize" >> go e where
|
synthesize e = scope ("synth: " ++ show e) $ go (minimize' e)
|
||||||
|
where
|
||||||
go :: Var v => Term v -> M v (Type v)
|
go :: Var v => Term v -> M v (Type v)
|
||||||
go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var
|
go (Term.Var' v) = getContext >>= \ctx -> case lookupType ctx v of -- Var
|
||||||
Nothing -> fail $ "type not known for term var: " ++ Text.unpack (Var.name v)
|
Nothing -> fail $ "type not known for term var: " ++ Text.unpack (Var.name v)
|
||||||
@ -838,7 +843,7 @@ synthesizeApp ft arg = scope ("synthesizeApp: " ++ show ft ++ " " ++ show arg) $
|
|||||||
ambientEs <- getAbilities
|
ambientEs <- getAbilities
|
||||||
o <$ check arg (Type.effect ambientEs i)
|
o <$ check arg (Type.effect ambientEs i)
|
||||||
go (Type.Existential' a) = do -- a^App
|
go (Type.Existential' a) = do -- a^App
|
||||||
[i,o] <- traverse freshenVar [a, ABT.v' "o"]
|
[i,o] <- traverse freshenVar [ABT.v' "i", ABT.v' "o"]
|
||||||
let soln = Type.Monotype (Type.existential i `Type.arrow` Type.existential o)
|
let soln = Type.Monotype (Type.existential i `Type.arrow` Type.existential o)
|
||||||
let ctxMid = context [Existential o, Existential i, Solved a soln]
|
let ctxMid = context [Existential o, Existential i, Solved a soln]
|
||||||
modifyContext' $ replace (Existential a) ctxMid
|
modifyContext' $ replace (Existential a) ctxMid
|
||||||
|
@ -24,7 +24,7 @@ import qualified Data.Set as Set
|
|||||||
-- info attached to `v` values may participate in the `Eq` or `Ord` instances,
|
-- info attached to `v` values may participate in the `Eq` or `Ord` instances,
|
||||||
-- it is 'just' metadata.
|
-- it is 'just' metadata.
|
||||||
--
|
--
|
||||||
class (Eq v, Ord v) => Var v where
|
class (Show v, Eq v, Ord v) => Var v where
|
||||||
named :: Text -> v
|
named :: Text -> v
|
||||||
rename :: Text -> v -> v
|
rename :: Text -> v -> v
|
||||||
name :: v -> Text
|
name :: v -> Text
|
||||||
|
@ -125,6 +125,17 @@ test = scope "typechecker" . tests $
|
|||||||
|r12 : UInt64
|
|r12 : UInt64
|
||||||
|r12 = (x -> x) 64
|
|r12 = (x -> x) 64
|
||||||
|
|
|
|
||||||
|
|id : forall a . a -> a
|
||||||
|
|id x = x
|
||||||
|
|
|
||||||
|
|r13 : (UInt64, Text)
|
||||||
|
|r13 = let
|
||||||
|
| id = ((x -> x): forall a . a -> a)
|
||||||
|
| (id 10, id "foo")
|
||||||
|
|
|
||||||
|
|r14 : (forall a . a -> a) -> (UInt64, Text)
|
||||||
|
|r14 id = (id 10, id "foo")
|
||||||
|
|
|
||||||
|() |]
|
|() |]
|
||||||
|
|
||||||
, checks [r|effect Abort where
|
, checks [r|effect Abort where
|
||||||
@ -156,7 +167,19 @@ test = scope "typechecker" . tests $
|
|||||||
|bork = u -> 1 +_UInt64 (Abort.Abort ())
|
|bork = u -> 1 +_UInt64 (Abort.Abort ())
|
||||||
|
|
|
|
||||||
|() |]
|
|() |]
|
||||||
, checks [r|--State effect
|
, checks [r|--State1 effect
|
||||||
|
|effect State se2 where
|
||||||
|
| put : ∀ se . se -> {State se} ()
|
||||||
|
| get : ∀ se . () -> {State se} se
|
||||||
|
|
|
||||||
|
|state woot eff = case eff of
|
||||||
|
| { State.get () -> k } -> handle state woot in k woot
|
||||||
|
| { State.put snew -> k } -> handle (state snew) in (k ())
|
||||||
|
| { a } -> (woot, a)
|
||||||
|
|
|
||||||
|
|()
|
||||||
|
|]
|
||||||
|
, checks [r|--State2 effect
|
||||||
|effect State se2 where
|
|effect State se2 where
|
||||||
| put : ∀ se . se -> {State se} ()
|
| put : ∀ se . se -> {State se} ()
|
||||||
| get : ∀ se . () -> {State se} se
|
| get : ∀ se . () -> {State se} se
|
||||||
@ -165,13 +188,13 @@ test = scope "typechecker" . tests $
|
|||||||
|state woot eff = case eff of
|
|state woot eff = case eff of
|
||||||
| { State.get () -> k } -> handle (state woot) in (k woot)
|
| { State.get () -> k } -> handle (state woot) in (k woot)
|
||||||
| { State.put snew -> k } -> handle (state snew) in (k ())
|
| { State.put snew -> k } -> handle (state snew) in (k ())
|
||||||
| { a } -> (woot, a)
|
|
||||||
|
|
|
|
||||||
|ex : (UInt64, UInt64)
|
|()
|
||||||
|ex = handle (state 42) in State.get ()
|
|
||||||
|
|
|
||||||
|ex
|
|
||||||
|]
|
|]
|
||||||
|
|
||||||
|
--ex : (UInt64, UInt64)
|
||||||
|
--ex = handle (state 42) in State.get ()
|
||||||
|
|
||||||
]
|
]
|
||||||
where c tm typ = scope tm . expect $ check (stripMargin tm) typ
|
where c tm typ = scope tm . expect $ check (stripMargin tm) typ
|
||||||
bombs s = scope s (expect . not . fileTypechecks $ s)
|
bombs s = scope s (expect . not . fileTypechecks $ s)
|
||||||
|
Loading…
Reference in New Issue
Block a user