Skip to content
Permalink
Browse files

Split `Blank` up into `Recorded` and non-recorded portion, this lets …

…us give a more precise type for `SolvedBlank` notes

Also changed naming - `blank` is a noop in the typechecker, `placeholder` is like GHC holes, and `resolve` is used for type-directed term resolution
  • Loading branch information...
pchiusano committed Aug 1, 2018
1 parent f23ca96 commit 0566c26561bc8132371c95fe5105e22c51502ce9
@@ -1,10 +1,17 @@
module Unison.Blank where

data Blank loc
-- An expression that has not been filled in, has type `forall a . a`.
= Placeholder
-- A user-provided typed hole
| Remember loc String
loc :: Recorded loc -> loc
loc (Placeholder loc _) = loc
loc (Resolve loc _) = loc

data Recorded loc
-- A user-provided named placeholder
= Placeholder loc String
-- A name to be resolved with type-directed name resolution.
| Resolve loc String
deriving (Show, Eq, Ord)

data Blank loc = Blank | Recorded (Recorded loc)
deriving (Show, Eq, Ord)


@@ -146,7 +146,7 @@ insertTerm at ctx = do
Term (E.Vector' vs) -> do
i <- listToMaybe [i | Index i <- [last at]]
let v2 = E.vector'() ((E.vmap ABT.Bound <$> Vector.take (i+1) vs) `mappend`
Vector.singleton (E.placeholder ()) `mappend`
Vector.singleton (E.blank ()) `mappend`
(E.vmap ABT.Bound <$> Vector.drop (i+1) vs))
asTerm =<< set (Term v2)
_ -> Nothing -- todo - allow other types of insertions, like \x -> y to \x x2 -> y
@@ -29,7 +29,7 @@ import GHC.Generics
import Prelude.Extras (Eq1(..), Show1(..))
import Text.Show
import qualified Unison.ABT as ABT
import Unison.Blank
import qualified Unison.Blank as B
import Unison.Hash (Hash)
import qualified Unison.Hash as Hash
import Unison.Hashable (Hashable1, accumulateToken)
@@ -55,7 +55,7 @@ data F typeVar typeAnn patternAnn a
| Float Double
| Boolean Bool
| Text Text
| Blank (Blank typeAnn)
| Blank (B.Blank typeAnn)
| Ref Reference
-- First argument identifies the data type,
-- second argument identifies the constructor
@@ -225,14 +225,14 @@ uint64 a d = ABT.tm' a (UInt64 d)
text :: Ord v => a -> Text -> AnnotatedTerm2 vt at ap v a
text a = ABT.tm' a . Text

placeholder :: Ord v => a -> AnnotatedTerm2 vt at ap v a
placeholder a = ABT.tm' a (Blank Placeholder)
blank :: Ord v => a -> AnnotatedTerm2 vt at ap v a
blank a = ABT.tm' a (Blank B.Blank)

remember :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a
remember a s = ABT.tm' a . Blank $ Remember a s
placeholder :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a
placeholder a s = ABT.tm' a . Blank $ B.Recorded (B.Placeholder a s)

resolve :: Ord v => a -> String -> AnnotatedTerm2 vt a ap v a
resolve a s = ABT.tm' a . Blank $ Resolve a s
resolve a s = ABT.tm' a . Blank $ B.Recorded (B.Resolve a s)

constructor :: Ord v => a -> Reference -> Int -> AnnotatedTerm2 vt at ap v a
constructor a ref n = ABT.tm' a (Constructor ref n)
@@ -444,11 +444,11 @@ instance Var v => Hashable1 (F v a p) where
Float n -> [tag 66, Hashable.Double n]
Boolean b -> [tag 67, accumulateToken b]
Text t -> [tag 68, accumulateToken t]
Blank b ->
tag 1 : case b of
Placeholder -> [tag 0]
Remember _ s -> [tag 1, Hashable.Text (Text.pack s)]
Resolve _ s -> [tag 2, Hashable.Text (Text.pack s)]
Blank b -> tag 1 :
case b of
B.Blank -> [tag 0]
B.Recorded (B.Placeholder _ s) -> [tag 1, Hashable.Text (Text.pack s)]
B.Recorded (B.Resolve _ s) -> [tag 2, Hashable.Text (Text.pack s)]
Ref (Reference.Builtin name) -> [tag 2, accumulateToken name]
Ref (Reference.Derived _) -> error "handled above, but GHC can't figure this out"
App a a2 -> [tag 3, hashed (hash a), hashed (hash a2)]
@@ -523,9 +523,9 @@ instance (Var v, Show p, Show a0, Show a) => Show (F v a0 p a) where
go _ (Vector vs) = showListWith (showsPrec 0) (Vector.toList vs)
go _ (Blank b) =
case b of
Placeholder -> s"_"
Remember _ r -> s("_" ++ r)
Resolve _ r -> s r
B.Blank -> s"_"
B.Recorded (B.Placeholder _ r) -> s("_" ++ r)
B.Recorded (B.Resolve _ r) -> s r
go _ (Ref r) = showsPrec 0 r
go _ (Let b body) = showParen True (s"let " <> showsPrec 0 b <> s" in " <> showsPrec 0 body)
go _ (LetRec bs body) = showParen True (s"let rec" <> showsPrec 0 bs <> s" in " <> showsPrec 0 body)
@@ -186,8 +186,8 @@ boolean :: Var v => TermP v
boolean = ((\t -> Term.boolean (ann t) True) <$> reserved "true") <|>
((\t -> Term.boolean (ann t) False) <$> reserved "false")

remember :: Var v => TermP v
remember = (\t -> Term.remember (ann t) (L.payload t)) <$> blank
placeholder :: Var v => TermP v
placeholder = (\t -> Term.placeholder (ann t) (L.payload t)) <$> blank

vector :: Var v => TermP v -> TermP v
vector p = f <$> reserved "[" <*> elements <*> reserved "]"
@@ -198,7 +198,7 @@ vector p = f <$> reserved "[" <*> elements <*> reserved "]"
termLeaf :: forall v. Var v => TermP v
termLeaf =
asum [hashLit, prefixTerm, text, number, boolean,
tupleOrParenthesizedTerm, remember, vector term]
tupleOrParenthesizedTerm, placeholder, vector term]

and = label "and" $ f <$> reserved "and" <*> termLeaf <*> termLeaf
where f kw x y = Term.and (ann kw <> ann y) x y
@@ -202,7 +202,7 @@ universal :: Ord v => v -> Type (TypeVar b v)
universal v = ABT.var (TypeVar.Universal v)

existentialp :: Ord v => a -> v -> AnnotatedType (TypeVar (Blank x) v) a
existentialp a v = existential' a Placeholder v
existentialp a v = existential' a Blank v

existential' :: Ord v => a -> Blank x -> v -> AnnotatedType (TypeVar (Blank x) v) a
existential' a blank v = ABT.annotatedVar a (TypeVar.Existential blank v)
Oops, something went wrong.

1 comment on commit 0566c26

@pchiusano

This comment has been minimized.

Copy link
Member Author

commented on 0566c26 Aug 1, 2018

@runarorama previously we had data Blank loc = Placeholder | Remember loc String | Resolve loc String which was awkward because when the typechecker records a SolvedBlank note, it should only be one of Remember or Resolve. So I split up the Blank type.

Also did some bikeshedding on names, got rid of remember, it's now called placeholder, and blank is the same meaning as before, the dummy term which is ignored during typechecking.

Please sign in to comment.
You can’t perform that action at this time.