update more Term smart constructors to take an annotation

This commit is contained in:
Paul Chiusano 2018-07-18 11:24:05 -04:00
parent edd0e84e70
commit 0d918e4633
5 changed files with 29 additions and 32 deletions

View File

@ -146,7 +146,7 @@ insertTerm at ctx = do
Term (E.Vector' vs) -> do Term (E.Vector' vs) -> do
i <- listToMaybe [i | Index i <- [last at]] i <- listToMaybe [i | Index i <- [last at]]
let v2 = E.vector' ((E.vmap ABT.Bound <$> Vector.take (i+1) vs) `mappend` let v2 = E.vector' ((E.vmap ABT.Bound <$> Vector.take (i+1) vs) `mappend`
Vector.singleton E.blank `mappend` Vector.singleton (E.blank()) `mappend`
(E.vmap ABT.Bound <$> Vector.drop (i+1) vs)) (E.vmap ABT.Bound <$> Vector.drop (i+1) vs))
asTerm =<< set (Term v2) asTerm =<< set (Term v2)
_ -> Nothing -- todo - allow other types of insertions, like \x -> y to \x x2 -> y _ -> Nothing -- todo - allow other types of insertions, like \x -> y to \x x2 -> y

View File

@ -87,12 +87,12 @@ data F typeVar typeAnn a
deriving (Eq,Foldable,Functor,Generic,Generic1,Traversable) deriving (Eq,Foldable,Functor,Generic,Generic1,Traversable)
-- | Like `Term v`, but with an annotation of type `a` at every level in the tree -- | Like `Term v`, but with an annotation of type `a` at every level in the tree
type AnnotatedTerm v a = AnnotatedType2 v a v a type AnnotatedTerm v a = AnnotatedTerm2 v a v a
-- | Allow type variables and term variables to differ -- | Allow type variables and term variables to differ
type AnnotatedTerm' vt v a = AnnotatedType2 vt a v a type AnnotatedTerm' vt v a = AnnotatedTerm2 vt a v a
-- | Allow type variables, term variables, type annotations and term annotations -- | Allow type variables, term variables, type annotations and term annotations
-- to all differ -- to all differ
type AnnotatedType2 vt at v a = ABT.Term (F vt at) v a type AnnotatedTerm2 vt at v a = ABT.Term (F vt at) v a
-- | Terms are represented as ABTs over the base functor F, with variables in `v` -- | Terms are represented as ABTs over the base functor F, with variables in `v`
type Term v = AnnotatedTerm v () type Term v = AnnotatedTerm v ()
@ -174,44 +174,41 @@ fresh = ABT.fresh
-- some smart constructors -- some smart constructors
var :: a -> v -> AnnotatedType2 vt at v a var :: a -> v -> AnnotatedTerm2 vt at v a
var = ABT.annotatedVar 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 => a -> Hash -> AnnotatedType2 vt at v a derived :: Ord v => a -> Hash -> AnnotatedTerm2 vt at v a
derived a = ref a . 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 => a -> Reference -> AnnotatedType2 vt at v a ref :: Ord v => a -> Reference -> AnnotatedTerm2 vt at v a
ref a r = ABT.tm' a (Ref r) ref a r = ABT.tm' a (Ref r)
builtin :: Ord v => a -> Text -> AnnotatedType2 vt at v a builtin :: Ord v => a -> Text -> AnnotatedTerm2 vt at v a
builtin a n = ref a (Reference.Builtin n) builtin a n = ref a (Reference.Builtin n)
float :: Ord v => Double -> Term' vt v float :: Ord v => a -> Double -> AnnotatedTerm2 vt at v a
float d = ABT.tm (Float d) float a d = ABT.tm' a (Float d)
boolean :: Ord v => a -> Bool -> AnnotatedTerm' vt v a boolean :: Ord v => a -> Bool -> AnnotatedTerm2 vt at v a
boolean a b = ABT.tm' a (Boolean b) boolean a b = ABT.tm' a (Boolean b)
int64 :: Ord v => Int64 -> Term' vt v int64 :: Ord v => a -> Int64 -> AnnotatedTerm2 vt at v a
int64 d = ABT.tm (Int64 d) int64 a d = ABT.tm' a (Int64 d)
uint64 :: Ord v => Word64 -> Term' vt v uint64 :: Ord v => a -> Word64 -> AnnotatedTerm2 vt at v a
uint64 d = ABT.tm (UInt64 d) uint64 a d = ABT.tm' a (UInt64 d)
text :: Ord v => Text -> Term' vt v text :: Ord v => a -> Text -> AnnotatedTerm2 vt at v a
text = ABT.tm . Text text a = ABT.tm' a . Text
blank :: Ord v => Term' vt v blank :: Ord v => a -> AnnotatedTerm2 vt at v a
blank = ABT.tm Blank blank a = ABT.tm' a Blank
blank' :: Ord v => a -> AnnotatedTerm' vt v a
blank' a = ABT.tm' a Blank
app :: Ord v => Term' vt v -> Term' vt v -> Term' vt v app :: Ord v => Term' vt v -> Term' vt v -> Term' vt v
app f arg = ABT.tm (App f arg) app f arg = ABT.tm (App f arg)
@ -243,7 +240,7 @@ iff cond t f = ABT.tm (If cond t f)
ann :: Ord v => Term' vt v -> Type vt -> Term' vt v ann :: Ord v => Term' vt v -> Type vt -> Term' vt v
ann e t = ABT.tm (Ann e t) ann e t = ABT.tm (Ann e t)
ann' :: Ord v => a -> AnnotatedType2 vt at v a -> Type.AnnotatedType vt at -> AnnotatedType2 vt at v a ann' :: Ord v => a -> AnnotatedTerm2 vt at v a -> Type.AnnotatedType vt at -> AnnotatedTerm2 vt at v a
ann' a e t = ABT.tm' a (Ann e t) ann' a e t = ABT.tm' a (Ann e t)
vector :: Ord v => [Term' vt v] -> Term' vt v vector :: Ord v => [Term' vt v] -> Term' vt v

View File

@ -201,10 +201,10 @@ text' =
where ps = char '"' *> Unison.Parser.takeWhile "text literal" (/= '"') <* char '"' where ps = char '"' *> Unison.Parser.takeWhile "text literal" (/= '"') <* char '"'
text :: Ord v => Parser s (Term v) text :: Ord v => Parser s (Term v)
text = Term.text <$> text' text = Term.text() <$> text'
number :: Ord v => Parser s (Term v) number :: Ord v => Parser s (Term v)
number = number' Term.int64 Term.uint64 Term.float number = number' (Term.int64()) (Term.uint64()) (Term.float())
number' :: (Int64 -> a) -> (Word64 -> a) -> (Double -> a) -> Parser s a number' :: (Int64 -> a) -> (Word64 -> a) -> (Double -> a) -> Parser s a
number' i u f = token $ do number' i u f = token $ do
@ -237,7 +237,7 @@ hashLit = token (f =<< (mark *> hash))
hash = base64urlstring hash = base64urlstring
blank :: Ord v => TermP v blank :: Ord v => TermP v
blank = token (char '_') $> Term.blank blank = token (char '_') $> Term.blank()
vector :: Ord v => TermP v -> TermP v vector :: Ord v => TermP v -> TermP v
vector p = Term.vector <$> (lbracket *> elements <* rbracket) vector p = Term.vector <$> (lbracket *> elements <* rbracket)

View File

@ -151,7 +151,7 @@ check' term typ = join . Note.unnote $ check [] missing missingD term typ
-- this will check that `(f : forall a . a -> a) e` is well typed. -- this will check that `(f : forall a . a -> a) e` is well typed.
checkAdmissible' :: Var v => Term v -> Type v -> Either Note (Type v) checkAdmissible' :: Var v => Term v -> Type v -> Either Note (Type v)
checkAdmissible' term typ = checkAdmissible' term typ =
synthesize' (Term.blank `Term.ann` tweak typ `Term.app` term) synthesize' (Term.blank() `Term.ann` tweak typ `Term.app` term)
where where
tweak (Type.ForallNamed' v body) = Type.forall() v (tweak body) tweak (Type.ForallNamed' v body) = Type.forall() v (tweak body)
tweak t = Type.arrow() t t tweak t = Type.arrow() t t

View File

@ -826,16 +826,16 @@ checkCase scrutineeType outputType (Term.MatchCase pat guard rhs) =
-- Convert pattern to a Term -- Convert pattern to a Term
patTerm = evalState (patternToTerm pat) vs patTerm = evalState (patternToTerm pat) vs
newBody = Term.let1 [(Var.named "_", patTerm `Term.ann` scrutineeType)] rhs' newBody = Term.let1 [(Var.named "_", patTerm `Term.ann` scrutineeType)] rhs'
entireCase = foldr (\v t -> Term.let1 [(v, Term.blank)] t) newBody vs entireCase = foldr (\v t -> Term.let1 [(v, Term.blank())] t) newBody vs
in check entireCase outputType in check entireCase outputType
-- Make up a fake term for the pattern, that we can typecheck -- Make up a fake term for the pattern, that we can typecheck
patternToTerm :: Var v => Pattern -> State [v] (Term v) patternToTerm :: Var v => Pattern -> State [v] (Term v)
patternToTerm pat = case pat of patternToTerm pat = case pat of
Pattern.Boolean b -> pure $ Term.boolean() b Pattern.Boolean b -> pure $ Term.boolean() b
Pattern.Int64 n -> pure $ Term.int64 n Pattern.Int64 n -> pure $ Term.int64() n
Pattern.UInt64 n -> pure $ Term.uint64 n Pattern.UInt64 n -> pure $ Term.uint64() n
Pattern.Float n -> pure $ Term.float n Pattern.Float n -> pure $ Term.float() n
-- similar for other literals -- similar for other literals
Pattern.Constructor r cid pats -> do Pattern.Constructor r cid pats -> do
outputTerms <- traverse patternToTerm pats outputTerms <- traverse patternToTerm pats
@ -844,7 +844,7 @@ patternToTerm pat = case pat of
(h : t) <- get (h : t) <- get
put t put t
pure $ Term.var() h pure $ Term.var() h
Pattern.Unbound -> pure Term.blank Pattern.Unbound -> pure $ Term.blank()
Pattern.As p -> do Pattern.As p -> do
(h : t) <- get (h : t) <- get
put t put t