From f7839231f73aada908d6d64edfdbbef043b74b18 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 18 Dec 2024 14:14:28 +0000 Subject: [PATCH] Add hole solving but not for nats --- brat/Brat/Checker.hs | 29 +++- brat/Brat/Checker/Helpers.hs | 5 + brat/Brat/Checker/Monad.hs | 16 ++ brat/Brat/Checker/SolveHoles.hs | 160 ++++++++++++++++++ brat/Brat/Checker/SolvePatterns.hs | 38 +---- brat/Brat/Elaborator.hs | 1 + brat/Brat/Error.hs | 3 +- brat/Brat/Eval.hs | 58 +++++-- brat/Brat/Lexer/Flat.hs | 1 + brat/Brat/Lexer/Token.hs | 2 + brat/Brat/Parser.hs | 1 + brat/Brat/Syntax/Common.hs | 2 +- brat/Brat/Syntax/Concrete.hs | 1 + brat/Brat/Syntax/Core.hs | 3 + brat/Brat/Syntax/Raw.hs | 3 + brat/Brat/Unelaborator.hs | 2 + brat/brat.cabal | 1 + brat/examples/infer.brat | 8 + brat/test/golden/error/remaining_hopes.brat | 5 + .../golden/error/remaining_hopes.brat.golden | 8 + 20 files changed, 292 insertions(+), 55 deletions(-) create mode 100644 brat/Brat/Checker/SolveHoles.hs create mode 100644 brat/examples/infer.brat create mode 100644 brat/test/golden/error/remaining_hopes.brat create mode 100644 brat/test/golden/error/remaining_hopes.brat.golden diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index ffee325f..3b317be0 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -25,6 +25,7 @@ import Prelude hiding (filter) import Brat.Checker.Helpers import Brat.Checker.Monad import Brat.Checker.Quantity +import Brat.Checker.SolveHoles (typeEq) import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve) import Brat.Checker.Types import Brat.Constructors @@ -659,7 +660,13 @@ check' (Of n e) ((), unders) = case ?my of (elems, unders, rightUnders) <- getVecs len unders pure ((tgt, el):elems, (tgt, ty):unders, rightUnders) getVecs _ unders = pure ([], [], unders) - +check' Hope ((), (NamedPort hope _, ty):unders) = case (?my, ty) of + (Braty, Left _k) -> do + fc <- req AskFC + req (ANewHope hope fc) + pure (((), ()), ((), unders)) + (Braty, Right _ty) -> typeErr "Can only infer kinded things with !" + (Kerny, _) -> typeErr "Won't infer kernel typed !" check' tm _ = error $ "check' " ++ show tm @@ -1124,7 +1131,7 @@ run :: VEnv -> Namespace -> Checking a -> Either Error (a, ([TypedHole], Store, Graph)) -run ve initStore ns m = +run ve initStore ns m = do let ctx = Ctx { globalVEnv = ve , store = initStore -- TODO: fill with default constructors @@ -1132,5 +1139,19 @@ run ve initStore ns m = , kconstructors = kernelConstructors , typeConstructors = defaultTypeConstructors , aliasTable = M.empty - } in - (\(a,ctx,(holes, graph)) -> (a, (holes, store ctx, graph))) <$> handler (localNS ns m) ctx mempty + , hopes = M.empty + } + (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty + let tyMap = typeMap $ store ctx + -- If the `hopes` set has any remaining holes with kind Nat, we need to abort. + -- Even though we didn't need them for typechecking problems, our runtime + -- behaviour depends on the values of the holes, which we can't account for. + case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap (InEnd e)) (hopes ctx) of + [] -> pure (a, (holes, store ctx, graph)) + -- Just use the FC of the first hole while we don't have the capacity to + -- show multiple error locations + hs@((_,fc):_) -> Left $ Err (Just fc) (RemainingNatHopes (show . fst <$> hs)) + where + isNatKinded tyMap e = case tyMap M.! e of + EndType Braty (Left Nat) -> True + _ -> False diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index f58ac827..d792a0a4 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -492,3 +492,8 @@ runArith (NumValue upl grol) Pow (NumValue upr gror) -- 2^(2^k * upr) + 2^(2^k * upr) * (full(2^(k + k') * mono)) = pure $ NumValue (upl ^ upr) (StrictMonoFun (StrictMono (l * upr) (Full (StrictMono (k + k') mono)))) runArith _ _ _ = Nothing + +buildConst :: SimpleTerm -> Val Z -> Checking Src +buildConst tm ty = do + (_, _, [(out,_)], _) <- next "buildConst" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + pure out diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index e993711b..cb9fd015 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -50,12 +50,16 @@ data CtxEnv = CtxEnv , locals :: VEnv } +type Hopes = M.Map InPort FC + data Context = Ctx { globalVEnv :: VEnv , store :: Store , constructors :: ConstructorMap Brat , kconstructors :: ConstructorMap Kernel , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)] , aliasTable :: M.Map QualName Alias + -- All the ends here should be targets + , hopes :: Hopes } data CheckingSig ty where @@ -89,6 +93,9 @@ data CheckingSig ty where AskVEnv :: CheckingSig CtxEnv Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () + ANewHope :: InPort -> FC -> CheckingSig () + AskHopes :: CheckingSig Hopes + RemoveHope :: InPort -> CheckingSig () localAlias :: (QualName, Alias) -> Checking v -> Checking v localAlias _ (Ret v) = Ret v @@ -267,6 +274,15 @@ handler (Req s k) ctx g M.lookup tycon tbl handler (k args) ctx g + ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g + + AskHopes -> handler (k (hopes ctx)) ctx g + + RemoveHope e -> let hset = hopes ctx in + if M.member e hset + then handler (k ()) (ctx { hopes = M.delete e hset }) g + else Left (dumbErr (InternalError ("Trying to remove Hope not in set: " ++ show e))) + type Checking = Free CheckingSig instance Semigroup a => Semigroup (Checking a) where diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs new file mode 100644 index 00000000..8711006a --- /dev/null +++ b/brat/Brat/Checker/SolveHoles.hs @@ -0,0 +1,160 @@ +module Brat.Checker.SolveHoles (typeEq) where + +import Brat.Checker.Helpers (buildConst) +import Brat.Checker.Monad +import Brat.Checker.Types (kindForMode) +import Brat.Error (ErrorMsg(..)) +import Brat.Eval +import Brat.Syntax.Common +import Brat.Syntax.Simple (SimpleTerm(..)) +import Brat.Syntax.Value +import Control.Monad.Freer +import Bwd +import Hasochism +import Util (zipSameLength) + +import Data.Bifunctor (second) +import Data.Foldable (sequenceA_) +import Data.Functor +import qualified Data.Map as M +import Data.Type.Equality (TestEquality(..), (:~:)(..)) + +-- External interface to typeEq' for closed values only. +typeEq :: String -- String representation of the term for error reporting + -> TypeKind -- The kind we're comparing at + -> Val Z -- Expected + -> Val Z -- Actual + -> Checking () +typeEq str = typeEq' str (Zy :* S0 :* S0) + +-- Demand that two things are equal, we're allowed to solve variables in the +-- hope set to make this true. +-- Raises a user error if the vals cannot be made equal. +typeEq' :: String -- String representation of the term for error reporting + -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n + -> TypeKind -- The kind we're comparing at + -> Val n -- Expected + -> Val n -- Actual + -> Checking () +typeEq' str stuff@(_ny :* _ks :* sems) k exp act = do + hopes <- req AskHopes + exp <- sem sems exp + act <- sem sems act + typeEqEta str stuff hopes k exp act + +isNumVar :: Sem -> Maybe SVar +isNumVar (SNum (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v))))) = Just v +isNumVar _ = Nothing + +-- Presumes that the hope set and the two `Sem`s are up to date. +typeEqEta :: String -- String representation of the term for error reporting + -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n + -> Hopes -- A map from the hope set to corresponding FCs + -> TypeKind -- The kind we're comparing at + -> Sem -- Expected + -> Sem -- Actual + -> Checking () +typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do + -- Higher kinded things + let nextSem = semLvl lvy + let xz = B0 :< nextSem + exp <- applySem exp xz + act <- applySem act xz + typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopes (TypeFor m ks) exp act +-- Not higher kinded - check for flex terms +-- (We don't solve under binders for now, so we only consider Zy here) +-- 1. "easy" flex cases +typeEqEta _tm (Zy :* _ks :* _sems) hopes k (SApp (SPar (InEnd e)) B0) act + | M.member e hopes = solveHope k e act +typeEqEta _tm (Zy :* _ks :* _sems) hopes k exp (SApp (SPar (InEnd e)) B0) + | M.member e hopes = solveHope k e exp +typeEqEta _ (Zy :* _ :* _) hopes Nat exp act + | Just (SPar (InEnd e)) <- isNumVar exp, M.member e hopes = solveHope Nat e act + | Just (SPar (InEnd e)) <- isNumVar act, M.member e hopes = solveHope Nat e exp +-- 2. harder cases, neither is in the hope set, so we can't define it ourselves +typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do + exp <- quote ny exp + act <- quote ny act + case [e | (VApp (VPar (InEnd e)) _) <- [exp,act], M.member e hopes] of + [] -> typeEqRigid tm stuff k exp act + [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined + _es -> error "TODO: must wait for one or the other to become more defined" + +-- This will update the `hopes` set, potentially invalidating things that have +-- been eval'd. +-- The Sem is closed, for now. +solveHope :: TypeKind -> InPort -> Sem -> Checking () +solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of + Right () -> do + defineEnd (InEnd hope) v + dangling <- case (k, v) of + (Nat, VNum _v) -> err $ Unimplemented "Nat hope solving" [] + (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum" + _ -> buildConst Unit TUnit + req (Wire (end dangling, kindType k, hope)) + req (RemoveHope hope) + Left msg -> case v of + VApp (VPar (InEnd end)) B0 | hope == end -> pure () + -- TODO: Not all occurrences are toxic. The end could be in an argument + -- to a hoping variable which isn't used. + -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1. + _ -> err msg + +typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking () +typeEqs _ _ [] [] [] = pure () +typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = typeEqs tm stuff ks exps acts <* typeEq' tm stuff k exp act +typeEqs _ _ _ _ _ = typeErr "arity mismatch" + +typeEqRow :: Modey m + -> String -- The term we complain about in errors + -> (Ny :* Stack Z TypeKind :* Stack Z Sem) lv -- Next available level, the kinds of existing levels + -> Ro m lv top0 + -> Ro m lv top1 + -> Either ErrorMsg (Some ((Ny :* Stack Z TypeKind :* Stack Z Sem) -- The new stack of kinds and fresh level + :* ((:~:) top0 :* (:~:) top1)) -- Proofs both input rows have same length (quantified over by Some) + ,[Checking ()] -- subproblems to run in parallel + ) +typeEqRow _ _ stuff R0 R0 = pure (Some (stuff :* (Refl :* Refl)), []) +typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> second + ((:) (typeEq' tm stuff (kindForMode m) ty1 ty2)) +typeEqRow m tm (ny :* kz :* semz) (REx (_,k1) ro1) (REx (_,k2) ro2) | k1 == k2 = typeEqRow m tm (Sy ny :* (kz :<< k1) :* (semz :<< semLvl ny)) ro1 ro2 +typeEqRow _ _ _ _ _ = Left $ TypeErr "Mismatched rows" + +-- Calls to typeEqRigid *must* start with rigid types to ensure termination +typeEqRigid :: String -- String representation of the term for error reporting + -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n + -> TypeKind -- The kind we're comparing at + -> Val n -- Expected + -> Val n -- Actual + -> Checking () +typeEqRigid tm (_ :* _ :* semz) Nat exp act = do + -- TODO: What if there's hope in the numbers? + exp <- sem semz exp + act <- sem semz act + if getNum exp == getNum act + then pure () + else err $ TypeMismatch tm (show exp) (show act) +typeEqRigid tm stuff@(_ :* kz :* _) (TypeFor m []) (VApp f args) (VApp f' args') | f == f' = + svKind f >>= \case + TypeFor m' ks | m == m' -> typeEqs tm stuff (snd <$> ks) (args <>> []) (args' <>> []) + -- pattern should always match + _ -> err $ InternalError "quote gave a surprising result" + where + svKind (VPar e) = kindOf (VPar e) + svKind (VInx n) = pure $ proj kz n +typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' = + req (TLup (m, c)) >>= \case + Just ks -> typeEqs tm lvkz (snd <$> ks) args args' + Nothing -> err $ TypeErr $ "Type constructor " ++ show c + ++ " undefined " ++ " at kind " ++ show (TypeFor m []) +typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 = do + probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg + (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd + sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized +typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1) + | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of + Nothing -> typeErr "Mismatched sum lengths" + Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat) + where + eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1) +typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index d9034655..362bfea5 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -19,7 +19,6 @@ import Hasochism import Control.Monad (unless) import Data.Bifunctor (first) -import Data.Foldable (for_, traverse_) import qualified Data.Map as M import Data.Maybe (fromJust) import Data.Type.Equality ((:~:)(..), testEquality) @@ -78,7 +77,7 @@ solve my ((src, Lit tm):p) = do (Braty, Left Nat) | Num n <- tm -> do unless (n >= 0) $ typeErr "Negative Nat kind" - unifyNum (nConstant (fromIntegral n)) (nVar (VPar (ExEnd (end src)))) + unifyNum (nConstant (fromIntegral n)) (nVar (VPar (toEnd src))) (Braty, Right ty) -> do throwLeft (simpleCheck Braty ty tm) _ -> typeErr $ "Literal " ++ show tm ++ " isn't valid at this type" @@ -97,7 +96,7 @@ solve my ((src, PCon c abs):p) = do -- Special case for 0, so that we can call `unifyNum` instead of pattern -- matching using what's returned from `natConstructors` PrefixName [] "zero" -> do - unifyNum (nVar (VPar (ExEnd (end src)))) nZero + unifyNum (nVar (VPar (toEnd src))) nZero p <- argProblems [] (normaliseAbstractor abs) p (tests, sol) <- solve my p pure ((src, PrimLitTest (Num 0)):tests, sol) @@ -108,7 +107,7 @@ solve my ((src, PCon c abs):p) = do (REx ("inner", Nat) R0) unifyNum (nVar (VPar (ExEnd (end src)))) - (relationToInner (nVar (VPar (ExEnd (end dangling))))) + (relationToInner (nVar (VPar (toEnd dangling)))) p <- argProblems [dangling] (normaliseAbstractor abs) p (tests, sol) <- solve my p -- When we get @-patterns, we shouldn't drop this anymore @@ -199,38 +198,7 @@ instantiateMeta e val = do defineEnd e val --- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding --- We can have bogus failures here because we're not normalising under lambdas --- N.B. the value argument is normalised. -doesntOccur :: End -> Val n -> Either ErrorMsg () -doesntOccur e (VNum nv) = for_ (getNumVar nv) (collision e) where - getNumVar :: NumVal (VVar n) -> Maybe End - getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of - Linear v -> case v of - VPar e -> Just e - _ -> Nothing - Full sm -> getNumVar (numValue sm) - getNumVar _ = Nothing -doesntOccur e (VApp var args) = case var of - VPar e' -> collision e e' *> traverse_ (doesntOccur e) args - _ -> pure () -doesntOccur e (VCon _ args) = traverse_ (doesntOccur e) args -doesntOccur e (VLam body) = doesntOccur e body -doesntOccur e (VFun my (ins :->> outs)) = case my of - Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs - Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs -doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows - -collision :: End -> End -> Either ErrorMsg () -collision e v | e == v = Left . UnificationError $ - show e ++ " is cyclic" - | otherwise = pure () - -doesntOccurRo :: Modey m -> End -> Ro m i j -> Either ErrorMsg () -doesntOccurRo _ _ R0 = pure () -doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro -doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro -- Need to keep track of which way we're solving - which side is known/unknown -- Things which are dynamically unknown must be Tgts - information flows from Srcs diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index da34e09b..5a4ed219 100644 --- a/brat/Brat/Elaborator.hs +++ b/brat/Brat/Elaborator.hs @@ -91,6 +91,7 @@ elaborate (WC fc x) = do elaborate' :: Flat -> Either Error SomeRaw' elaborate' (FVar x) = pure $ SomeRaw' (RVar x) +elaborate' FHope = pure $ SomeRaw' RHope elaborate' (FArith op a b) = do (SomeRaw a) <- elaborate a (SomeRaw b) <- elaborate b diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs index f34dba14..fc8a841f 100644 --- a/brat/Brat/Error.hs +++ b/brat/Brat/Error.hs @@ -83,6 +83,7 @@ data ErrorMsg -- The argument is the row of unused connectors | ThunkLeftOvers String | ThunkLeftUnders String + | RemainingNatHopes [String] instance Show ErrorMsg where show (TypeErr x) = "Type error: " ++ x @@ -166,7 +167,7 @@ instance Show ErrorMsg where show UnreachableBranch = "Branch cannot be reached" show (ThunkLeftOvers overs) = "Expected function to address all inputs, but " ++ overs ++ " wasn't used" show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders - + show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":((" " ++) <$> hs)) data Error = Err { fc :: Maybe FC , msg :: ErrorMsg diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index 52fff0e8..f9ae33d3 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -4,22 +4,27 @@ module Brat.Eval (EvMode(..) ,ValPat(..) ,NumPat(..) ,apply + ,applySem ,eval ,sem + ,semLvl + ,doesntOccur ,evalCTy ,eqTest + ,getNum ,kindEq + ,kindOf ,kindType ,numVal - ,typeEq + ,quote ) where import Brat.Checker.Monad import Brat.Checker.Types (EndType(..), kindForMode) import Brat.Error (ErrorMsg(..)) import Brat.QualName (plain) -import Brat.Syntax.Value import Brat.Syntax.Common +import Brat.Syntax.Value import Control.Monad.Freer (req) import Bwd import Hasochism @@ -29,6 +34,7 @@ import Data.Bifunctor (second) import Data.Functor import Data.Kind (Type) import Data.Type.Equality (TestEquality(..), (:~:)(..)) +import Data.Foldable (traverse_) kindType :: TypeKind -> Val Z kindType Nat = TNat @@ -191,14 +197,8 @@ kindOf (VPar e) = req (TypeOf e) >>= \case Kerny -> show ty kindOf (VInx n) = case n of {} --- We should have made sure that the two values share the given kind -typeEq :: String -- String representation of the term for error reporting - -> TypeKind -- The kind we're comparing at - -> Val Z -- Expected - -> Val Z -- Actual - -> Checking () -typeEq str k exp act = eqTest str k exp act >>= throwLeft - +-------- for SolvePatterns usage: not allowed to solve hopes, +-- and if pattern insoluble, it's not a type error (it's a "pattern match case unreachable") eqTest :: String -- String representation of the term for error reporting -> TypeKind -- The kind we're comparing at -> Val Z -- Expected @@ -256,10 +256,7 @@ eqWorker tm lvkz (TypeFor _ []) (SSum m0 stk0 rs0) (SSum m1 stk1 rs1) Just rs -> traverse eqVariant rs <&> sequence_ where eqVariant (Some r0, Some r1) = eqRowTest m0 tm lvkz (stk0,r0) (stk1,r1) <&> dropRight -eqWorker tm _ _ s0 s1 = do - v0 <- quote Zy s0 - v1 <- quote Zy s1 - pure . Left $ TypeMismatch tm (show v0) (show v1) +eqWorker tm _ _ v0 v1 = pure . Left $ TypeMismatch tm (show v0) (show v1) -- Type rows have bot0,bot1 dangling de Bruijn indices, which we instantiate with -- de Bruijn levels. As we go under binders in these rows, we add to the scope's @@ -300,3 +297,36 @@ eqTests tm lvkz = go Left e -> pure $ Left e go _ us vs = pure . Left . TypeErr $ "Arity mismatch in type constructor arguments:\n " ++ show us ++ "\n " ++ show vs + +-- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding +-- We can have bogus failures here because we're not normalising under lambdas +-- N.B. the value argument is normalised. +doesntOccur :: End -> Val n -> Either ErrorMsg () +doesntOccur e (VNum nv) = traverse_ (collision e) (getNumVar nv) + where + getNumVar :: NumVal (VVar n) -> Maybe End + getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of + Linear v -> case v of + VPar e -> Just e + _ -> Nothing + Full sm -> getNumVar (numValue sm) + getNumVar _ = Nothing +doesntOccur e (VApp var args) = case var of + VPar e' -> collision e e' *> traverse_ (doesntOccur e) args + _ -> pure () +doesntOccur e (VCon _ args) = traverse_ (doesntOccur e) args +doesntOccur e (VLam body) = doesntOccur e body +doesntOccur e (VFun my (ins :->> outs)) = case my of + Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs + Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs +doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows + +collision :: End -> End -> Either ErrorMsg () +collision e v | e == v = Left . UnificationError $ + show e ++ " is cyclic" + | otherwise = pure () + +doesntOccurRo :: Modey m -> End -> Ro m i j -> Either ErrorMsg () +doesntOccurRo _ _ R0 = pure () +doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro +doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro diff --git a/brat/Brat/Lexer/Flat.hs b/brat/Brat/Lexer/Flat.hs index 1f41d5ba..30fd6f62 100644 --- a/brat/Brat/Lexer/Flat.hs +++ b/brat/Brat/Lexer/Flat.hs @@ -87,6 +87,7 @@ tok = try (char '(' $> LParen) <|> try (string "-" $> Minus) <|> try (string "$" $> Dollar) <|> try (string "|" $> Pipe) + <|> try (string "!" $> Bang) <|> try (K <$> try keyword) <|> try qualified <|> Ident <$> ident diff --git a/brat/Brat/Lexer/Token.hs b/brat/Brat/Lexer/Token.hs index d5f8842b..80dca83b 100644 --- a/brat/Brat/Lexer/Token.hs +++ b/brat/Brat/Lexer/Token.hs @@ -43,6 +43,7 @@ data Tok | Dollar | Underscore | Pipe + | Bang | Cons | Snoc | ConcatEqEven @@ -88,6 +89,7 @@ instance Show Tok where show Dollar = "$" show Underscore = "_" show Pipe = "|" + show Bang = "!" show Cons = ",-" show Snoc = "-," show ConcatEqEven = "=,=" diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 494f193b..087a406a 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -515,6 +515,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr] <|> var <|> match Underscore $> FUnderscore <|> match Pipe $> FIdentity + <|> match Bang $> FHope cnoun :: Parser Flat -> Parser (WC (Raw 'Chk 'Noun)) diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs index dacd8d1b..622c598d 100644 --- a/brat/Brat/Syntax/Common.hs +++ b/brat/Brat/Syntax/Common.hs @@ -111,7 +111,7 @@ instance Eq ty => Eq (TypeRowElem ty) where Anon ty == Anon ty' = ty == ty' data TypeKind = TypeFor Mode [(PortName, TypeKind)] | Nat | Row - deriving (Eq, Show) + deriving (Eq, Ord, Show) pattern Star, Dollar :: [(PortName, TypeKind)] -> TypeKind pattern Star ks = TypeFor Brat ks diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs index d2d567f6..3e07bb44 100644 --- a/brat/Brat/Syntax/Concrete.hs +++ b/brat/Brat/Syntax/Concrete.hs @@ -22,6 +22,7 @@ type FEnv = ([FDecl], [RawAlias]) data Flat = FVar QualName + | FHope | FApp (WC Flat) (WC Flat) | FJuxt (WC Flat) (WC Flat) | FThunk (WC Flat) diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs index d3c30cff..c9dbd046 100644 --- a/brat/Brat/Syntax/Core.hs +++ b/brat/Brat/Syntax/Core.hs @@ -49,6 +49,7 @@ data Term :: Dir -> Kind -> Type where Pull :: [PortName] -> WC (Term Chk k) -> Term Chk k Var :: QualName -> Term Syn Noun -- Look up in noun (value) env Identity :: Term Syn UVerb + Hope :: Term Chk Noun Arith :: ArithOp -> WC (Term Chk Noun) -> WC (Term Chk Noun) -> Term Chk Noun Of :: WC (Term Chk Noun) -> WC (Term d Noun) -> Term d Noun @@ -113,8 +114,10 @@ instance Show (Term d k) where ,"of" ,bracket POf e ] + show (Var x) = show x show Identity = "|" + show Hope = "!" -- Nested applications should be bracketed too, hence 4 instead of 3 show (fun :$: arg) = bracket PApp fun ++ ('(' : show arg ++ ")") show (tm ::: ty) = bracket PAnn tm ++ " :: " ++ show ty diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs index ca26fa79..62934f1b 100644 --- a/brat/Brat/Syntax/Raw.hs +++ b/brat/Brat/Syntax/Raw.hs @@ -71,6 +71,7 @@ data Raw :: Dir -> Kind -> Type where RPull :: [PortName] -> WC (Raw Chk k) -> Raw Chk k RVar :: QualName -> Raw Syn Noun RIdentity :: Raw Syn UVerb + RHope :: Raw Chk Noun RArith :: ArithOp -> WC (Raw Chk Noun) -> WC (Raw Chk Noun) -> Raw Chk Noun ROf :: WC (Raw Chk Noun) -> WC (Raw d Noun) -> Raw d Noun (:::::) :: WC (Raw Chk Noun) -> [RawIO] -> Raw Syn Noun @@ -102,6 +103,7 @@ instance Show (Raw d k) where = unwords ["let", show abs, "=", show xs, "in", show body] show (RNHole name) = '?':name show (RVHole name) = '?':name + show RHope = "!" show (RSimple tm) = show tm show RPass = show "pass" show REmpty = "()" @@ -201,6 +203,7 @@ instance (Kindable k) => Desugarable (Raw d k) where -- TODO: holes need to know their arity for type checking desugar' (RNHole strName) = NHole . (strName,) <$> freshM strName desugar' (RVHole strName) = VHole . (strName,) <$> freshM strName + desugar' RHope = pure Hope desugar' RPass = pure Pass desugar' (RSimple simp) = pure $ Simple simp desugar' REmpty = pure Empty diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs index 51d85041..5ff57492 100644 --- a/brat/Brat/Unelaborator.hs +++ b/brat/Brat/Unelaborator.hs @@ -38,6 +38,7 @@ unelab _ _ (Con c args) = FCon c (unelab Chky Nouny <$> args) unelab _ _ (C (ss :-> ts)) = FFn (toRawRo ss :-> toRawRo ts) unelab _ _ (K cty) = FKernel $ fmap (\(p, ty) -> Named p (toRaw ty)) cty unelab _ _ Identity = FIdentity +unelab _ _ Hope = FHope unelab _ _ FanIn = FFanIn unelab _ _ FanOut = FFanOut @@ -67,6 +68,7 @@ toRaw (Con c args) = RCon c (toRaw <$> args) toRaw (C (ss :-> ts)) = RFn (toRawRo ss :-> toRawRo ts) toRaw (K cty) = RKernel $ (\(p, ty) -> Named p (toRaw ty)) <$> cty toRaw Identity = RIdentity +toRaw Hope = RHope toRaw FanIn = RFanIn toRaw FanOut = RFanOut diff --git a/brat/brat.cabal b/brat/brat.cabal index 58a29efa..a7d22664 100644 --- a/brat/brat.cabal +++ b/brat/brat.cabal @@ -66,6 +66,7 @@ library Brat.Checker.Helpers, Brat.Checker.Helpers.Nodes, Brat.Checker.Monad, + Brat.Checker.SolveHoles, Brat.Checker.SolvePatterns, Brat.Checker.Types, Brat.Compile.Hugr, diff --git a/brat/examples/infer.brat b/brat/examples/infer.brat new file mode 100644 index 00000000..e10ee44e --- /dev/null +++ b/brat/examples/infer.brat @@ -0,0 +1,8 @@ +map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y) +map(_, _, _, []) = [] +map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs) + +-- TODO: Make BRAT solve for the # kinded args +mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n) +mapVec(_, _, _, _, []) = [] +mapVec(_, _, f, succ(n), x ,- xs) = f(x) ,- mapVec(!, !, f, n, xs) diff --git a/brat/test/golden/error/remaining_hopes.brat b/brat/test/golden/error/remaining_hopes.brat new file mode 100644 index 00000000..164b8190 --- /dev/null +++ b/brat/test/golden/error/remaining_hopes.brat @@ -0,0 +1,5 @@ +f(n :: #) -> Nat +f(n) = n + +g :: Nat +g = f(!) diff --git a/brat/test/golden/error/remaining_hopes.brat.golden b/brat/test/golden/error/remaining_hopes.brat.golden new file mode 100644 index 00000000..80d15436 --- /dev/null +++ b/brat/test/golden/error/remaining_hopes.brat.golden @@ -0,0 +1,8 @@ +Error in test/golden/error/remaining_hopes.brat on line 5: +g = f(!) + ^^^ + + Expected to work out values for these holes: + In checking_check_defs_1_g_1_Eval 0 + +