Term.builtin/derived/ref smart constructors now take annotations.

This commit is contained in:
Paul Chiusano 2018-07-18 11:16:10 -04:00
parent 5b38f58a23
commit edd0e84e70
4 changed files with 13 additions and 13 deletions

View File

@ -57,7 +57,7 @@ builtinTerms = builtinTerms' ++
Term.constructor r i) Term.constructor r i)
builtinTerms' :: forall v. Var v => [(v, Term v)] builtinTerms' :: forall v. Var v => [(v, Term v)]
builtinTerms' = (toSymbol &&& Term.ref) <$> Map.keys (builtins @v) builtinTerms' = (toSymbol &&& Term.ref()) <$> Map.keys (builtins @v)
builtinTypes :: forall v. Var v => [(v, Type v)] builtinTypes :: forall v. Var v => [(v, Type v)]

View File

@ -180,17 +180,17 @@ var = ABT.annotatedVar
var' :: Var v => Text -> Term' vt v var' :: Var v => Text -> Term' vt v
var' = var() . ABT.v' var' = var() . ABT.v'
derived :: Ord v => Hash -> Term' vt v derived :: Ord v => a -> Hash -> AnnotatedType2 vt at v a
derived = ref . Reference.Derived derived a = ref a . Reference.Derived
derived' :: Ord v => Text -> Maybe (Term' vt v) derived' :: Ord v => Text -> Maybe (Term' vt v)
derived' base58 = derived <$> Hash.fromBase58 base58 derived' base58 = derived () <$> Hash.fromBase58 base58
ref :: Ord v => Reference -> AnnotatedType2 vt at v () ref :: Ord v => a -> Reference -> AnnotatedType2 vt at v a
ref r = ABT.tm (Ref r) ref a r = ABT.tm' a (Ref r)
builtin :: Ord v => Text -> AnnotatedType2 vt at v () builtin :: Ord v => a -> Text -> AnnotatedType2 vt at v a
builtin n = ref (Reference.Builtin n) builtin a n = ref a (Reference.Builtin n)
float :: Ord v => Double -> Term' vt v float :: Ord v => Double -> Term' vt v
float d = ABT.tm (Float d) float d = ABT.tm (Float d)

View File

@ -712,7 +712,7 @@ synthesize e = scope ("synth: " ++ show e) $ go (minimize' e)
abilities <- getAbilities abilities <- getAbilities
t <- scope "let1 closed" $ synthesizeClosed' abilities decls binding t <- scope "let1 closed" $ synthesizeClosed' abilities decls binding
v' <- ABT.freshen e freshenVar v' <- ABT.freshen e freshenVar
e <- pure $ ABT.bind e (Term.builtin (Var.name v') `Term.ann` t) e <- pure $ ABT.bind e (Term.builtin() (Var.name v') `Term.ann` t)
synthesize e synthesize e
--go (Term.Let1' binding e) = do --go (Term.Let1' binding e) = do
-- -- literally just convert to a lambda application and call synthesize! -- -- literally just convert to a lambda application and call synthesize!
@ -891,8 +891,8 @@ synthesizeApp ft arg = scope ("synthesizeApp: " ++ show ft ++ ", " ++ show arg)
-- also rename Vector -> Sequence -- also rename Vector -> Sequence
desugarVector :: Var v => [Term v] -> Term v desugarVector :: Var v => [Term v] -> Term v
desugarVector ts = case ts of desugarVector ts = case ts of
[] -> Term.ann (Term.builtin "Vector.empty") (Type.forall'() ["a"] va) [] -> Term.ann (Term.builtin() "Vector.empty") (Type.forall'() ["a"] va)
hd : tl -> (Term.builtin "Vector.prepend" `Term.ann` prependT) `Term.app` hd `Term.app` desugarVector tl hd : tl -> (Term.builtin() "Vector.prepend" `Term.ann` prependT) `Term.app` hd `Term.app` desugarVector tl
where prependT = Type.forall'() ["a"] (Type.arrow() (Type.v' "a") (Type.arrow() va va)) where prependT = Type.forall'() ["a"] (Type.arrow() (Type.v' "a") (Type.arrow() va va))
va = Type.app() (Type.vector()) (Type.v' "a") va = Type.app() (Type.vector()) (Type.v' "a")
@ -901,7 +901,7 @@ annotateRefs :: (Applicative f, Ord v)
-> Term v -> Term v
-> Noted f (Term v) -> Noted f (Term v)
annotateRefs synth term = ABT.visit f term where annotateRefs synth term = ABT.visit f term where
f (Term.Ref' h) = Just (Term.ann (Term.ref h) <$> (ABT.vmap TypeVar.Universal <$> synth h)) f (Term.Ref' h) = Just (Term.ann (Term.ref() h) <$> (ABT.vmap TypeVar.Universal <$> synth h))
f _ = Nothing f _ = Nothing
synthesizeClosed synthesizeClosed

View File

@ -537,7 +537,7 @@ synthesize e = withinSynthesize e $ go (minimize' e)
t <- synthesizeClosed' abilities binding t <- synthesizeClosed' abilities binding
v' <- ABT.freshen e freshenVar v' <- ABT.freshen e freshenVar
-- note: `Ann' (Ref' _) t` synthesizes to `t` -- note: `Ann' (Ref' _) t` synthesizes to `t`
e <- pure $ ABT.bindInheritAnnotation e (Term.ann' () (Term.builtin (Var.name v')) t) e <- pure $ ABT.bindInheritAnnotation e (Term.ann' () (Term.builtin() (Var.name v')) t)
synthesize e synthesize e
go (Term.Let1' binding e) = do go (Term.Let1' binding e) = do
-- literally just convert to a lambda application and call synthesize! -- literally just convert to a lambda application and call synthesize!