From fec6dc4863296b2e96a42aac5e240bdd7a5e2f16 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 8 Nov 2024 16:07:10 +0000 Subject: [PATCH 01/35] Add holes(!) --- brat/Brat/Checker.hs | 40 +++-- brat/Brat/Checker/Helpers.hs | 16 +- brat/Brat/Checker/Monad.hs | 35 +++++ brat/Brat/Checker/SolveHoles.hs | 234 +++++++++++++++++++++++++++++ brat/Brat/Checker/SolvePatterns.hs | 163 ++++++++++---------- brat/Brat/Checker/Types.hs | 5 + brat/Brat/Elaborator.hs | 1 + brat/Brat/Error.hs | 4 + brat/Brat/Eval.hs | 68 ++++++--- brat/Brat/FC.hs | 6 +- brat/Brat/Lexer/Flat.hs | 1 + brat/Brat/Lexer/Token.hs | 2 + brat/Brat/Load.hs | 4 +- 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/Syntax/Value.hs | 4 +- brat/Control/Monad/Freer.hs | 51 ++++++- brat/brat.cabal | 1 + brat/examples/infer.brat | 7 + brat/test/Test/Util.hs | 3 +- 23 files changed, 533 insertions(+), 122 deletions(-) create mode 100644 brat/Brat/Checker/SolveHoles.hs create mode 100644 brat/examples/infer.brat diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index d243476b..dbd7924a 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -24,6 +24,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 @@ -114,13 +115,13 @@ checkWire Braty (WC fc tm) outputs (dangling, o) (hungry, u) = localFC fc $ do let ot = binderToValue Braty o let ut = binderToValue Braty u if outputs - then typeEq (show tm) (Star []) ot ut - else typeEq (show tm) (Star []) ut ot + then typeEq (show tm) (Zy :* S0 :* S0) (Star []) ot ut + else typeEq (show tm) (Zy :* S0 :* S0) (Star []) ut ot wire (dangling, ot, hungry) checkWire Kerny (WC fc tm) outputs (dangling, ot) (hungry, ut) = localFC fc $ do if outputs - then typeEq (show tm) (Dollar []) ot ut - else typeEq (show tm) (Dollar []) ut ot + then typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ot ut + else typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ut ot wire (dangling, ot, hungry) checkIO :: forall m d k exp act . (CheckConstraints m k, ?my :: Modey m) @@ -545,7 +546,7 @@ check' FanIn (overs, ((tgt, ty):unders)) = do let k = case my of Kerny -> Dollar [] Braty -> Star [] - typeEq (show FanIn) k elTy (binderToValue my overTy) + typeEq (show FanIn) (Zy :* S0 :* S0) k elTy (binderToValue my overTy) let tailTy = TVec elTy (VNum (nConstant (n - 1))) (_, [(hungryHead, _), (hungryTail, tailTy)], [(danglingResult, _)], _) <- anext "faninNodes" (Constructor (plain "cons")) (S0, Some (Zy :* S0)) ((RPr ("head", elTy) (RPr ("tail", tailTy) R0)) :: Ro m Z Z) @@ -649,7 +650,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 ((), ((tgt, ty):unders)) = case (?my, ty) of + (Braty, Left _k) -> do + fc <- req AskFC + req (ANewHope (toEnd tgt, 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 @@ -1115,10 +1122,9 @@ abstractEndz ez = changeVar (ParToInx (AddZ (stackLen ez)) ez) run :: VEnv -> Store - -> Namespace -> Checking a -> Either Error (a, ([TypedHole], Store, Graph)) -run ve initStore ns m = +run ve initStore m = do let ctx = Ctx { globalVEnv = ve , store = initStore -- TODO: fill with default constructors @@ -1126,5 +1132,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 + , hopeSet = M.empty + } + (a,ctx,(holes, graph)) <- handler m ctx mempty + let tyMap = typeMap $ store ctx + -- If the hopeSet 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 e) (hopeSet 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 f05a54b9..816bc5c0 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -20,7 +20,7 @@ module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig ,evalSrcRow, evalTgtRow )-} where -import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows) +import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows, defineEnd) import Brat.Checker.Types import Brat.Error (ErrorMsg(..)) import Brat.Eval (eval, EvMode(..), kindType) @@ -391,10 +391,10 @@ valueToBinder Braty = Right valueToBinder Kerny = id defineSrc :: Src -> Val Z -> Checking () -defineSrc src v = req (Define (ExEnd (end src)) v) +defineSrc src v = defineEnd (ExEnd (end src)) v defineTgt :: Tgt -> Val Z -> Checking () -defineTgt tgt v = req (Define (InEnd (end tgt)) v) +defineTgt tgt v = defineEnd (InEnd (end tgt)) v declareSrc :: Src -> Modey m -> BinderType m -> Checking () declareSrc src my ty = req (Declare (ExEnd (end src)) my ty) @@ -508,3 +508,13 @@ 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 + +buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src) +buildArithOp op = do + (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) + pure ((lhs, rhs), out) + +buildConst :: SimpleTerm -> Val Z -> Checking Src +buildConst tm ty = do + (_, _, [(out,_)], _) <- next "" (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 b8a5b6b6..a69afdd8 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -18,6 +18,7 @@ import Control.Monad.Freer import Control.Monad.Fail () import Data.List (intercalate) import qualified Data.Map as M +import qualified Data.Set as S -- import Debug.Trace @@ -50,12 +51,16 @@ data CtxEnv = CtxEnv , locals :: VEnv } +type HopeSet = M.Map End FC + data Context = Ctx { globalVEnv :: VEnv , store :: Store , constructors :: ConstructorMap Brat , kconstructors :: ConstructorMap Kernel , typeConstructors :: M.Map (Mode, UserName) [(PortName, TypeKind)] , aliasTable :: M.Map UserName Alias + -- All the ends here should be targets + , hopeSet :: HopeSet } data CheckingSig ty where @@ -89,6 +94,8 @@ data CheckingSig ty where AskVEnv :: CheckingSig CtxEnv Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () + ANewHope :: (End, FC) -> CheckingSig () + AskHopeSet :: CheckingSig HopeSet localAlias :: (UserName, Alias) -> Checking v -> Checking v localAlias _ (Ret v) = Ret v @@ -267,6 +274,31 @@ handler (Req s k) ctx g M.lookup tycon tbl handler (k args) ctx g + ANewHope (e, fc) -> handler (k ()) (ctx { hopeSet = M.insert e fc (hopeSet ctx) }) g + + AskHopeSet -> handler (k (hopeSet ctx)) ctx g + +howStuck :: Val n -> Stuck +howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e) +howStuck (VLam bod) = howStuck bod +howStuck (VCon _ _) = Unstuck +howStuck (VFun _ _) = Unstuck +howStuck (VSum _ _) = Unstuck +-- Numbers are likely to cause problems. +-- Whether they are stuck or not depends on the question we're asking! +howStuck (VNum (NumValue 0 gro)) = howStuckGro gro + where + howStuckGro Constant0 = Unstuck + howStuckGro (StrictMonoFun f) = howStuckSM f + + howStuckSM (StrictMono 0 mono) = howStuckMono mono + howStuckSM _ = AwaitingAny mempty + + howStuckMono (Full sm) = howStuckSM sm + howStuckMono (Linear (VPar e)) = AwaitingAny (S.singleton e) -- ALAN was VHop + howStuckMono (Linear _) = AwaitingAny mempty +howStuck _ = AwaitingAny mempty + type Checking = Free CheckingSig instance Semigroup a => Semigroup (Checking a) where @@ -315,3 +347,6 @@ localNS ns (Req (Fresh str) k) = let (name, root) = fresh str ns in localNS ns (Req (SplitNS str) k) = let (subSpace, newRoot) = split str ns in localNS newRoot (k subSpace) localNS ns (Req c k) = Req c (localNS ns . k) + +defineEnd :: End -> Val Z -> Checking () +defineEnd e v = req (Define e v) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs new file mode 100644 index 00000000..877b614d --- /dev/null +++ b/brat/Brat/Checker/SolveHoles.hs @@ -0,0 +1,234 @@ +module Brat.Checker.SolveHoles (typeEq, buildNatVal, buildNum, invertNatVal) where + +import Brat.Checker.Monad +import Brat.Checker.Types (kindForMode) +import Brat.Checker.Helpers (buildArithOp, buildConst, next) +import Brat.Error (ErrorMsg(..)) +import Brat.Eval +import Brat.Graph (NodeType(..)) +import Brat.Syntax.Common +import Brat.Syntax.Simple (SimpleTerm(..)) +import Brat.Syntax.Value +import Control.Monad.Freer +import Bwd +import Hasochism +import Util (zip_same_length) + +import Data.Foldable (traverse_) +import Data.Functor +import qualified Data.Map as M +import Data.Type.Equality (TestEquality(..), (:~:)(..)) + +-- 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 AskHopeSet + 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 + -> HopeSet -- The hope set + -> TypeKind -- The kind we're comparing at + -> Sem -- Expected + -> Sem -- Actual + -> Checking () +typeEqEta tm (lvy :* kz :* sems) hopeSet (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)) hopeSet (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) +-- "easy" flex cases +typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k (SApp (SPar e) B0) act + | M.member e hopeSet = solveHope k e act +typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0) + | M.member e hopeSet = solveHope k e exp +typeEqEta _ (Zy :* _ :* _) hopeSet Nat exp act + | Just (SPar e) <- isNumVar exp, M.member e hopeSet = solveHope Nat e act + | Just (SPar e) <- isNumVar act, M.member e hopeSet = solveHope Nat e exp +typeEqEta tm stuff@(ny :* _ks :* _sems) hopeSet k exp act = do + exp <- quote ny exp + act <- quote ny act + case [e | (VApp (VPar e) _) <- [exp,act], M.member e hopeSet] of + [] -> typeEqRigid tm stuff k exp act + _es -> error "TODO" +-- uhhh +-- Yield(AwaitingAny $ S.fromList es) (\_ -> typeEq tm stuff k exp act) + +-- This will update the hopeSet, potentially invalidating things that have been eval'd +-- The Sem is closed, for now. +-- TODO: This needs to update the BRAT graph with the solution. +solveHope :: TypeKind -> End -> Sem -> Checking () +solveHope k e v = quote Zy v >>= \v -> case doesntOccur e v of + Right () -> do + defineEnd e v + dangling <- case (k, v) of + (Nat, VNum v) -> buildNatVal v + (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum" + _ -> buildConst Unit TUnit + let InEnd i = e + req $ Wire (end dangling, kindType k, i) + pure () + Left msg -> case v of + VApp (VPar e') B0 | e == e' -> 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 <&> \(res, probs) -> (res, (typeEq tm stuff (kindForMode m) ty1 ty2):probs) +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 + traverse_ id 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 zip_same_length rs0 rs1 of + Nothing -> typeErr "Mismatched sum lengths" + Just rs -> traverse eqVariant rs >>= (traverse_ id . 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) + +wire :: (Src, Val Z, Tgt) -> Checking () +wire (src, ty, tgt) = req $ Wire (end src, ty, end tgt) + +buildNum :: Integer -> Checking Src +buildNum n = buildConst (Num (fromIntegral n)) TNat + + +buildNatVal :: NumVal (VVar Z) -> Checking Src +buildNatVal nv@(NumValue n gro) = case n of + 0 -> buildGro gro + n -> do + nDangling <- buildNum n + ((lhs,rhs),out) <- buildArithOp Add + src <- buildGro gro + wire (nDangling, TNat, lhs) + wire (src, TNat, rhs) + pure out + where + buildGro :: Fun00 (VVar Z) -> Checking Src + buildGro Constant0 = buildNum 0 + buildGro (StrictMonoFun sm) = buildSM sm + + buildSM :: StrictMono (VVar Z) -> Checking Src + buildSM (StrictMono k mono) = do + -- Calculate 2^k as `factor` + two <- buildNum 2 + kDangling <- buildNum k + ((lhs,rhs),factor) <- buildArithOp Pow + wire (two, TNat, lhs) + wire (kDangling, TNat, rhs) + -- Multiply mono by 2^k + ((lhs,rhs),out) <- buildArithOp Mul + monoDangling <- buildMono mono + wire (factor, TNat, lhs) + wire (monoDangling, TNat, rhs) + pure out + + buildMono :: Monotone (VVar Z) -> Checking Src + buildMono (Linear (VPar (ExEnd e))) = pure $ NamedPort e "numval" + buildMono (Full sm) = do + -- Calculate 2^n as `outPlus1` + two <- buildNum 2 + dangling <- buildSM sm + ((lhs,rhs),outPlus1) <- buildArithOp Pow + wire (two, TNat, lhs) + wire (dangling, TNat, rhs) + -- Then subtract 1 + one <- buildNum 1 + ((lhs,rhs),out) <- buildArithOp Sub + wire (outPlus1, TNat, lhs) + wire (one, TNat, rhs) + pure out + buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv + +invertNatVal :: Src -> NumVal a -> Checking Src +invertNatVal src (NumValue up gro) = case up of + 0 -> invertGro src gro + _ -> do + ((lhs,rhs),out) <- buildArithOp Sub + upSrc <- buildNum up + wire (src, TNat, lhs) + wire (upSrc, TNat, rhs) + invertGro out gro + where + invertGro _ Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" + invertGro src (StrictMonoFun sm) = invertSM src sm + + invertSM src (StrictMono k mono) = case k of + 0 -> invertMono src mono + _ -> do + divisor <- buildNum (2 ^ k) + ((lhs,rhs),out) <- buildArithOp Div + wire (src, TNat, lhs) + wire (divisor, TNat, rhs) + invertMono out mono + + invertMono src (Linear _) = pure src + invertMono src (Full sm) = do + (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) + wire (src, TNat, llufTgt) + invertSM llufSrc sm diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 272915a3..0e38aea6 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -2,6 +2,7 @@ module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve) import Brat.Checker.Monad import Brat.Checker.Helpers +import Brat.Checker.SolveHoles (buildNatVal, buildNum, invertNatVal) import Brat.Checker.Types (EndType(..)) import Brat.Constructors import Brat.Constructors.Patterns @@ -19,7 +20,6 @@ import Hasochism import Control.Monad (unless) import Data.Bifunctor (first) -import Data.Foldable (traverse_) import qualified Data.Map as M import Data.Maybe (fromJust) import Data.Type.Equality ((:~:)(..), testEquality) @@ -141,6 +141,9 @@ solveConstructor :: EvMode m ) solveConstructor my src (c, abs) ty p = do (CArgs pats _ patRo argRo, (tycon, tyargs)) <- lookupConstructor my c ty + -- Create a row of hypothetical kinds which contextualise the arguments to the + -- constructor. + -- These need to be Tgts because we don't know how to compute them dynamically/ (_, _, _, stuff) <- next "type_args" Hypo (S0, Some (Zy :* S0)) patRo R0 (node, _, patArgWires, _) <- let ?my = my in anext "val_args" Hypo stuff R0 argRo trackM ("Constructor " ++ show c ++ "; type " ++ show ty) @@ -148,6 +151,8 @@ solveConstructor my src (c, abs) ty p = do Some (_ :* patEnds) -> do trackM (show pats) trackM (show patEnds) + -- Match the patterns for `c` against the ends of the Hypo node, to + -- produce the terms that we're interested in let (lhss, leftovers) = patVals pats (stkList patEnds) unless (null leftovers) $ error "There's a bug in the constructor table" tyArgKinds <- tlup (Brat, tycon) @@ -188,47 +193,44 @@ unify l k r = do -- the whole `Problem`. (l, r, _) -> err . UnificationError $ "Can't unify " ++ show l ++ " with " ++ show r +-- Solve a metavariable statically - don't do anything dynamic instantiateMeta :: End -> Val Z -> Checking () instantiateMeta e val = do throwLeft (doesntOccur e val) - req (Define 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) = case getNumVar nv of - Just e' -> collision e e' - _ -> pure () + defineEnd e val + +-- Make the dynamic wiring for a metavariable. This only needs to happen for +-- numbers because they have nontrivial runtime behaviour. +computeMeta :: End -> NumVal (VVar Z) -> Checking () +computeMeta e nv = case (e, vars nv) of + (ExEnd src, [VPar (InEnd tgt)]) -> do + src <- invertNatVal (NamedPort src "") nv + wire (src, TNat, NamedPort tgt "") + + -- Both targets, we need to create the thing that they both derive from + (InEnd tgt1, [VPar (InEnd tgt2)]) -> do + (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0)) + (REx ("n", Nat) R0) (REx ("n", Nat) R0) + defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt)))) + defineTgt (NamedPort tgt2 "") (VNum (nVar (VPar (toEnd idSrc)))) + wire (idSrc, TNat, NamedPort tgt2 "") + let _nv' = fmap (const (VPar (toEnd idSrc))) nv + src1 <- buildNatVal nv + wire (src1, TNat, NamedPort tgt1 "") + + -- RHS is constant or Src, wire it into tgt + (InEnd tgt, _) -> do + src <- buildNatVal nv + wire (src, TNat, NamedPort tgt "") + + -- do nothing + _ -> pure () 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 + vars :: NumVal a -> [a] + vars = foldMap pure +-- 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 unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking () unifyNum (NumValue lup lgro) (NumValue rup rgro) | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro) @@ -246,10 +248,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking () lhsMono (Linear v) num = case v of - VPar e -> instantiateMeta e (VNum num) - _ -> case num of -- our only hope is to instantiate the RHS - NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar (ExEnd e))))) -> instantiateMeta (toEnd e) (VNum (nVar v)) - _ -> err . UnificationError $ "Couldn't instantiate variable " ++ show v + VPar e -> instantiateMeta e (VNum num) *> computeMeta e num lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm')))) = lhsStrictMono sm (NumValue 0 (StrictMonoFun sm')) lhsMono m@(Full _) (NumValue 0 gro) = lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m))) @@ -261,6 +260,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) demand0 (NumValue 0 Constant0) = pure () demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of Linear (VPar e) -> instantiateMeta e (VNum (nConstant 0)) + *> computeMeta e (nConstant 0) Full sm -> demand0 (NumValue 0 (StrictMonoFun sm)) _ -> err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0" demand0 n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0" @@ -270,9 +270,21 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- 2^k * x -- = 2^k * (y + 1) -- = 2^k + 2^k * y - demandSucc (StrictMono k (Linear (VPar (ExEnd out)))) = do - y <- mkPred out + demandSucc sm@(StrictMono k (Linear (VPar (ExEnd x)))) = do + ySrc <- invertNatVal (NamedPort x "") (NumValue 1 (StrictMonoFun sm)) + let y = nVar (VPar (toEnd ySrc)) + instantiateMeta (ExEnd x) (VNum (nPlus 1 y)) + pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y + + demandSucc (StrictMono k (Linear (VPar (InEnd x)))) = do + one <- buildNum 1 + ((lhs,rhs),out) <- buildArithOp Add + wire (one, TNat, rhs) + wire (out, TNat, NamedPort x "") + let y = nVar (VPar (toEnd lhs)) + instantiateMeta (InEnd x) (VNum (nPlus 1 y)) pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y + -- 2^k * full(n + 1) -- = 2^k * (1 + 2 * full(n)) -- = 2^k + 2^(k + 1) * full(n) @@ -291,53 +303,48 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) evenGro Constant0 = pure Constant0 evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of Linear (VPar (ExEnd out)) -> do - half <- mkHalf out + half <- invertNatVal (NamedPort out "") (NumValue 0 (StrictMonoFun (StrictMono 1 (Linear ())))) + instantiateMeta (ExEnd out) (VNum (n2PowTimes 1 (nVar (VPar (toEnd half))))) pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd half))))) - Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even" + Linear (VPar (InEnd tgt)) -> do + twoSrc <- buildNum 2 + ((halfTgt,twoTgt),outSrc) <- buildArithOp Mul + wire (twoSrc, TNat, twoTgt) + wire (outSrc, TNat, NamedPort tgt "") + let _half = nVar (VPar (toEnd halfTgt)) + instantiateMeta (InEnd tgt) (VNum (n2PowTimes 1 (nVar (VPar (toEnd halfTgt))))) + pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd halfTgt))))) Full sm -> StrictMonoFun sm <$ demand0 (NumValue 0 (StrictMonoFun sm)) evenGro (StrictMonoFun (StrictMono n mono)) = pure (StrictMonoFun (StrictMono (n - 1) mono)) -- Check a numval is odd, and return its rounded down half oddGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z)) oddGro (StrictMonoFun (StrictMono 0 mono)) = case mono of - Linear (VPar (ExEnd out)) -> mkPred out >>= demandEven - Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even" + Linear (VPar (ExEnd out)) -> do + -- compute (/2) . (-1) + halfSrc <- invertNatVal (NamedPort out "") (NumValue 1 (StrictMonoFun (StrictMono 1 (Linear ())))) + instantiateMeta (ExEnd out) (VNum (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd halfSrc)))))) + pure (nVar (VPar (toEnd halfSrc))) + Linear (VPar (InEnd tgt)) -> do + twoSrc <- buildNum 2 + ((flooredHalfTgt, twoTgt), doubleSrc) <- buildArithOp Mul + wire (twoSrc, TNat, twoTgt) + + oneSrc <- buildNum 1 + ((doubleTgt, oneTgt), addOut) <- buildArithOp Add + wire (oneSrc, TNat, oneTgt) + wire (doubleSrc, TNat, doubleTgt) + wire (addOut, TNat, NamedPort tgt "") + + instantiateMeta (InEnd tgt) (VNum (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd flooredHalfTgt)))))) + pure (nVar (VPar (toEnd flooredHalfTgt))) + -- full(n + 1) = 1 + 2 * full(n) -- hence, full(n) is the rounded down half Full sm -> nFull <$> demandSucc sm oddGro _ = err . UnificationError $ "Can't force " ++ show n ++ " to be even" - -- Add dynamic logic to compute half of a variable. - mkHalf :: OutPort -> Checking Src - mkHalf out = do - (_, [], [(const2,_)], _) <- next "const2" (Const (Num 2)) (S0, Some (Zy :* S0)) - R0 - (RPr ("value", TNat) R0) - (_, [(lhs,_),(rhs,_)], [(half,_)], _) <- next "div2" (ArithNode Div) (S0, Some (Zy :* S0)) - (RPr ("left", TNat) (RPr ("right", TNat) R0)) - (RPr ("out", TNat) R0) - wire (NamedPort out "numerator", TNat, lhs) - wire (const2, TNat, rhs) - req $ Define (toEnd out) (VNum (n2PowTimes 1 (nVar (VPar (toEnd half))))) - pure half - - - -- Add dynamic logic to compute the predecessor of a variable, and return that - -- predecessor. - -- The variable must be a non-zero nat!! - mkPred :: OutPort -> Checking (NumVal (VVar Z)) - mkPred out = do - (_, [], [(const1,_)], _) <- next "const1" (Const (Num 1)) (S0, Some (Zy :* S0)) - R0 - (RPr ("value", TNat) R0) - (_, [(lhs,_),(rhs,_)], [(pred,_)], _) <- next "minus1" (ArithNode Sub) (S0, Some (Zy :* S0)) - (RPr ("left", TNat) (RPr ("right", TNat) R0)) - (RPr ("out", TNat) R0) - wire (NamedPort out "", TNat, lhs) - wire (const1, TNat, rhs) - req $ Define (ExEnd out) (VNum (nPlus 1 (nVar (VPar (toEnd pred))))) - pure (nVar (VPar (toEnd pred))) - +-- The variable must be a non-zero nat!! patVal :: ValPat -> [End] -> (Val Z, [End]) -- Nat variables will only be found in a `NumPat`, not a `ValPat` patVal VPVar (e:es) = (VApp (VPar e) B0, es) diff --git a/brat/Brat/Checker/Types.hs b/brat/Brat/Checker/Types.hs index e2ff5594..2428c83f 100644 --- a/brat/Brat/Checker/Types.hs +++ b/brat/Brat/Checker/Types.hs @@ -9,6 +9,7 @@ module Brat.Checker.Types (Overs, Unders ,emptyEnv ,TypedHole(..), HoleTag(..), HoleData(..) ,initStore + ,kindForMode ) where import Brat.Checker.Quantity @@ -111,3 +112,7 @@ initStore = Store M.empty M.empty instance Semigroup Store where (Store ks vs) <> (Store ks' vs') = Store (ks <> ks') (vs <> vs') + +kindForMode :: Modey m -> TypeKind +kindForMode Braty = Star [] +kindForMode Kerny = Dollar [] diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs index d5024802..751e0503 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 32cea48a..5027978a 100644 --- a/brat/Brat/Error.hs +++ b/brat/Brat/Error.hs @@ -82,6 +82,8 @@ data ErrorMsg -- The argument is the row of unused connectors | ThunkLeftOvers String | ThunkLeftUnders String + -- TODO: Add file context here + | RemainingNatHopes [String] instance Show ErrorMsg where show (TypeErr x) = "Type error: " ++ x @@ -165,7 +167,9 @@ 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:":indent (indent hs)) +indent = fmap (" " ++) data Error = Err { fc :: Maybe FC , msg :: ErrorMsg diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index 7d434d80..2bea55d5 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -4,23 +4,28 @@ 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(..)) +import Brat.Checker.Types (EndType(..), kindForMode) import Brat.Error (ErrorMsg(..)) -import Brat.Syntax.Value import Brat.Syntax.Common +import Brat.Syntax.Value import Brat.UserName (plain) -import Control.Monad.Freer (req) +import Control.Monad.Freer import Bwd import Hasochism import Util (zip_same_length) @@ -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 @@ -275,9 +272,7 @@ eqRowTest :: Modey m )) eqRowTest _ _ lvkz (stk0, R0) (stk1, R0) = pure $ Right (Some lvkz, stk0, stk1) eqRowTest m tm lvkz (stk0, RPr (_, ty0) r0) (stk1, RPr (_, ty1) r1) = do - let k = case m of - Braty -> Star [] - Kerny -> Dollar [] + let k = kindForMode m ty0 <- sem stk0 ty0 ty1 <- sem stk1 ty1 eqWorker tm lvkz k ty0 ty1 >>= \case @@ -302,3 +297,38 @@ 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) = case getNumVar nv of + Just e' -> collision e e' + _ -> pure () + 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/FC.hs b/brat/Brat/FC.hs index 958df5d1..ab50a96f 100644 --- a/brat/Brat/FC.hs +++ b/brat/Brat/FC.hs @@ -2,11 +2,7 @@ module Brat.FC where data Pos = Pos { line :: Int , col :: Int - } deriving Eq - -instance Show Pos where - show (Pos { .. }) = show line ++ ":" ++ show col - + } deriving (Eq, Show) instance Ord Pos where compare (Pos l c) (Pos l' c') | l == l' = compare c c' diff --git a/brat/Brat/Lexer/Flat.hs b/brat/Brat/Lexer/Flat.hs index 311e1b47..0ab238e3 100644 --- a/brat/Brat/Lexer/Flat.hs +++ b/brat/Brat/Lexer/Flat.hs @@ -88,6 +88,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 33ddbad6..59adea6c 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/Load.hs b/brat/Brat/Load.hs index 0e16e288..7d2c0747 100644 --- a/brat/Brat/Load.hs +++ b/brat/Brat/Load.hs @@ -138,7 +138,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS -- * A map from names to VDecls (aka an Env) -- * Some overs and outs?? let (globalNS, newRoot) = split "globals" ns - (entries, (_holes, kcStore, kcGraph)) <- run venv initStore globalNS $ + (entries, (_holes, kcStore, kcGraph)) <- run venv initStore $ localNS globalNS $ withAliases aliases $ forM decls $ \d -> localFC (fnLoc d) $ do let name = PrefixName pre (fnName d) (thing, ins :->> outs, sig, prefix) <- case (fnLocality d) of @@ -160,7 +160,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS let vdecls = map fst entries -- Now generate environment mapping usernames to nodes in the graph venv <- pure $ venv <> M.fromList [(name, overs) | ((name, _), (_, overs)) <- entries] - ((), (holes, newEndData, graph)) <- run venv kcStore newRoot $ withAliases aliases $ do + ((), (holes, newEndData, graph)) <- run venv kcStore $ localNS newRoot $ withAliases aliases $ do remaining <- "check_defs" -! foldM checkDecl' to_define vdecls pure $ assert (M.null remaining) () -- all to_defines were defined pure (venv, oldDecls <> vdecls, holes, oldEndData <> newEndData, kcGraph <> graph) diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs index 0c605e5a..11418ae5 100644 --- a/brat/Brat/Parser.hs +++ b/brat/Brat/Parser.hs @@ -513,6 +513,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 95d217c6..dbaa8f84 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 fd6f9ed7..3a28d926 100644 --- a/brat/Brat/Syntax/Concrete.hs +++ b/brat/Brat/Syntax/Concrete.hs @@ -22,6 +22,7 @@ type FEnv = ([FDecl], [RawAlias]) data Flat = FVar UserName + | 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 2b45872a..2cdad6a2 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 :: UserName -> 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 126cd815..9c415935 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 :: UserName -> 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/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs index c3b1e9cb..2967de69 100644 --- a/brat/Brat/Syntax/Value.hs +++ b/brat/Brat/Syntax/Value.hs @@ -51,6 +51,8 @@ data Inx :: N -> Type where VZ :: Inx (S n) VS :: Inx n -> Inx (S n) +deriving instance Eq (Inx n) + instance Show (Inx n) where show = show . toNat where @@ -144,7 +146,7 @@ deriving instance Show (VVar n) instance Eq (VVar n) where (VPar e0) == (VPar e1) = e0 == e1 - (VInx _) == (VInx _) = error "tried to compare VInxs" + (VInx i) == (VInx i') = i == i' _ == _ = False -- More syntactic, called "Term" elsewhere in literature (not in BRAT) diff --git a/brat/Control/Monad/Freer.hs b/brat/Control/Monad/Freer.hs index ebb1e310..34e35732 100644 --- a/brat/Control/Monad/Freer.hs +++ b/brat/Control/Monad/Freer.hs @@ -1,7 +1,42 @@ -module Control.Monad.Freer (Free(..), req) where +module Control.Monad.Freer where import Control.Monad ((>=>)) import Data.Kind (Type) +import qualified Data.Map as M +import qualified Data.Set as S + +import Brat.Syntax.Port + +-- A mapping of metavars to metavars, for a single problem: +-- * e -> Unstuck means e has been solved +-- * e -> Awaiting es means the problem's been transferred +-- * e not in news means no change to e +newtype News = News (M.Map End Stuck) + +updateEnd :: News -> End -> Stuck +updateEnd (News m) e = case M.lookup e m of + Nothing -> AwaitingAny (S.singleton e) + Just s -> s + +-- The RHS of the operation is the newer news +-- Invariant: The domains of these Newses are disjoint +instance Semigroup News where + (News m1) <> n2@(News m2) = News (m2 `M.union` (M.map (/// n2) m1)) + +instance Monoid News where + mempty = News M.empty + +data Stuck + = Unstuck + | AwaitingAny (S.Set End) + deriving Show + +instance Semigroup Stuck where + (AwaitingAny es1) <> (AwaitingAny es2) = AwaitingAny (S.union es1 es2) + _ <> _ = Unstuck + +instance Monoid Stuck where + mempty = AwaitingAny S.empty data Free (sig :: Type -> Type) (v :: Type) where Ret :: v -> Free sig v @@ -11,6 +46,20 @@ instance Functor (Free sig) where fmap f (Ret v) = Ret (f v) fmap f (Req sig k) = Req sig (fmap f . k) +class NewsWatcher t where + (///) :: t -> News -> t + +instance NewsWatcher Stuck where + Unstuck /// _ = Unstuck + (AwaitingAny es) /// n = foldMap (updateEnd n) es + +instance NewsWatcher (News -> t) where + f /// n = f . (n <>) + +instance NewsWatcher (Free sig v) where + Ret v /// _ = Ret v + Req sig k /// n = Req sig $ \v -> k v /// n + instance Applicative (Free sig) where pure = Ret (Ret f) <*> ma = fmap f ma diff --git a/brat/brat.cabal b/brat/brat.cabal index 7dc81789..424ae447 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..dacdb0a7 --- /dev/null +++ b/brat/examples/infer.brat @@ -0,0 +1,7 @@ +map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y) +map(_, _, _, []) = [] +map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs) + +mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n) +mapVec(_, _, _, _, []) = [] +mapVec(_, _, f, _, x ,- xs) = f(x) ,- mapVec(!, !, f, !, xs) diff --git a/brat/test/Test/Util.hs b/brat/test/Test/Util.hs index 1f50d9cc..a2a170c6 100644 --- a/brat/test/Test/Util.hs +++ b/brat/test/Test/Util.hs @@ -5,14 +5,13 @@ import Brat.Checker.Monad import Brat.Checker.Types (initStore, emptyEnv) import Brat.Error import Brat.FC -import Brat.Naming import qualified Data.Set as S import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.ExpectedFailure -runEmpty m = run emptyEnv initStore root m +runEmpty m = run emptyEnv initStore m assertChecking :: Checking a -> Assertion assertChecking m = case runEmpty $ localFC (FC (Pos 0 0) (Pos 0 0)) m of From 3c1f4ece0802febf3d9e7be3afe8c118fe0d0d3d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 8 Nov 2024 16:16:35 +0000 Subject: [PATCH 02/35] WIP: Merge better nat solving --- brat/Brat/Checker/SolveHoles.hs | 34 +++++----- brat/Brat/Checker/SolvePatterns.hs | 102 +++++++++++++++-------------- 2 files changed, 71 insertions(+), 65 deletions(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 877b614d..e77289aa 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -158,6 +158,7 @@ buildNum :: Integer -> Checking Src buildNum n = buildConst (Num (fromIntegral n)) TNat +-- Generate wiring to produce a dynamic instance of the numval argument buildNatVal :: NumVal (VVar Z) -> Checking Src buildNatVal nv@(NumValue n gro) = case n of 0 -> buildGro gro @@ -205,30 +206,33 @@ buildNatVal nv@(NumValue n gro) = case n of pure out buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv -invertNatVal :: Src -> NumVal a -> Checking Src -invertNatVal src (NumValue up gro) = case up of - 0 -> invertGro src gro +invertNatVal :: NumVal (VVar Z) -> Checking Tgt +invertNatVal (NumValue up gro) = case up of + 0 -> invertGro gro _ -> do ((lhs,rhs),out) <- buildArithOp Sub upSrc <- buildNum up - wire (src, TNat, lhs) wire (upSrc, TNat, rhs) - invertGro out gro + tgt <- invertGro gro + wire (out, TNat, tgt) + pure lhs where - invertGro _ Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" - invertGro src (StrictMonoFun sm) = invertSM src sm + invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" + invertGro (StrictMonoFun sm) = invertSM sm - invertSM src (StrictMono k mono) = case k of - 0 -> invertMono src mono + invertSM (StrictMono k mono) = case k of + 0 -> invertMono mono _ -> do divisor <- buildNum (2 ^ k) ((lhs,rhs),out) <- buildArithOp Div - wire (src, TNat, lhs) + tgt <- invertMono mono + wire (out, TNat, tgt) wire (divisor, TNat, rhs) - invertMono out mono + pure lhs - invertMono src (Linear _) = pure src - invertMono src (Full sm) = do + invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval") + invertMono (Full sm) = do (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) - wire (src, TNat, llufTgt) - invertSM llufSrc sm + tgt <- invertSM sm + wire (llufSrc, TNat, tgt) + pure llufTgt diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 0e38aea6..52103e2d 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -2,7 +2,7 @@ module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve) import Brat.Checker.Monad import Brat.Checker.Helpers -import Brat.Checker.SolveHoles (buildNatVal, buildNum, invertNatVal) +import Brat.Checker.SolveHoles (buildNatVal, invertNatVal) import Brat.Checker.Types (EndType(..)) import Brat.Constructors import Brat.Constructors.Patterns @@ -104,6 +104,7 @@ solve my ((src, PCon c abs):p) = do (tests, sol) <- solve my p pure ((src, PrimLitTest (Num 0)):tests, sol) _ -> case M.lookup c natConstructors of + -- This `relationToInner` is very sus - it doesn't do any wiring! Just (Just _, relationToInner) -> do (node, [], kids@[(dangling, _)], _) <- next "unpacked_nat" Hypo (S0, Some (Zy :* S0)) R0 -- we don't need to wire the src in; we just need the inner stuff @@ -194,18 +195,28 @@ unify l k r = do (l, r, _) -> err . UnificationError $ "Can't unify " ++ show l ++ " with " ++ show r -- Solve a metavariable statically - don't do anything dynamic +-- Once a metavariable is solved, we expect to not see it again in a normal form. instantiateMeta :: End -> Val Z -> Checking () instantiateMeta e val = do throwLeft (doesntOccur e val) defineEnd e val --- Make the dynamic wiring for a metavariable. This only needs to happen for +-- Solve a Nat kinded metavariable. Unlike `instantiateMeta`, this function also +-- makes the dynamic wiring for a metavariable. This only needs to happen for -- numbers because they have nontrivial runtime behaviour. -computeMeta :: End -> NumVal (VVar Z) -> Checking () -computeMeta e nv = case (e, vars nv) of - (ExEnd src, [VPar (InEnd tgt)]) -> do - src <- invertNatVal (NamedPort src "") nv - wire (src, TNat, NamedPort tgt "") +-- +-- We assume that the caller has done the occurs check and rules out trivial equations. +solveNumMeta :: End -> NumVal (VVar Z) -> Checking () +solveNumMeta e nv = case (e, vars nv) of + -- Compute the thing that the rhs should be based on the src, and instantiate src to that + -- TODO: sus that we're not using `tgt`?? + (ExEnd src, [VPar (InEnd _tgt)]) -> do + -- Compute the value of the `tgt` variable from the known `src` value by inverting nv + tgtSrc <- invertNatVal nv + defineSrc (NamedPort src "") (VNum (nVar (VPar (toEnd tgtSrc)))) + wire (NamedPort src "", TNat, tgtSrc) + + (ExEnd src, _) -> defineSrc (NamedPort src "") (VNum nv) -- Both targets, we need to create the thing that they both derive from (InEnd tgt1, [VPar (InEnd tgt2)]) -> do @@ -214,23 +225,24 @@ computeMeta e nv = case (e, vars nv) of defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt)))) defineTgt (NamedPort tgt2 "") (VNum (nVar (VPar (toEnd idSrc)))) wire (idSrc, TNat, NamedPort tgt2 "") - let _nv' = fmap (const (VPar (toEnd idSrc))) nv - src1 <- buildNatVal nv + let nv' = fmap (const (VPar (toEnd idSrc))) nv + src1 <- buildNatVal nv' + defineTgt (NamedPort tgt1 "") (VNum nv') wire (src1, TNat, NamedPort tgt1 "") -- RHS is constant or Src, wire it into tgt (InEnd tgt, _) -> do src <- buildNatVal nv + defineTgt (NamedPort tgt "") (VNum nv) wire (src, TNat, NamedPort tgt "") - -- do nothing - _ -> pure () where vars :: NumVal a -> [a] vars = foldMap pure -- 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 +-- ...But we don't need to do any wiring here, right? unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking () unifyNum (NumValue lup lgro) (NumValue rup rgro) | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro) @@ -247,8 +259,9 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) lhsStrictMono (StrictMono (n - 1) mono) num lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking () - lhsMono (Linear v) num = case v of - VPar e -> instantiateMeta e (VNum num) *> computeMeta e num + lhsMono (Linear v) (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v')))) | v == v' = pure () + lhsMono (Linear (VPar e)) num = throwLeft (doesntOccur e (VNum num)) *> + solveNumMeta e num lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm')))) = lhsStrictMono sm (NumValue 0 (StrictMonoFun sm')) lhsMono m@(Full _) (NumValue 0 gro) = lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m))) @@ -259,8 +272,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) demand0 :: NumVal (VVar Z) -> Checking () demand0 (NumValue 0 Constant0) = pure () demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of - Linear (VPar e) -> instantiateMeta e (VNum (nConstant 0)) - *> computeMeta e (nConstant 0) + Linear (VPar e) -> solveNumMeta e (nConstant 0) Full sm -> demand0 (NumValue 0 (StrictMonoFun sm)) _ -> err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0" demand0 n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0" @@ -270,20 +282,18 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- 2^k * x -- = 2^k * (y + 1) -- = 2^k + 2^k * y - demandSucc sm@(StrictMono k (Linear (VPar (ExEnd x)))) = do + demandSucc _sm@(StrictMono _k (Linear (VPar (ExEnd _x)))) = error "Todo..." {-do + -- This is sus because we don't have any tgt? ySrc <- invertNatVal (NamedPort x "") (NumValue 1 (StrictMonoFun sm)) let y = nVar (VPar (toEnd ySrc)) - instantiateMeta (ExEnd x) (VNum (nPlus 1 y)) + solveNumMeta (ExEnd x) (nPlus 1 y) pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y + -} - demandSucc (StrictMono k (Linear (VPar (InEnd x)))) = do - one <- buildNum 1 - ((lhs,rhs),out) <- buildArithOp Add - wire (one, TNat, rhs) - wire (out, TNat, NamedPort x "") - let y = nVar (VPar (toEnd lhs)) - instantiateMeta (InEnd x) (VNum (nPlus 1 y)) - pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y + demandSucc sm@(StrictMono k (Linear (VPar (InEnd weeEnd)))) = do + bigEnd <- invertNatVal (NumValue 1 (StrictMonoFun sm)) + solveNumMeta (toEnd bigEnd) (NumValue 0 (StrictMonoFun sm)) + pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (InEnd weeEnd))) -- 2^k * full(n + 1) -- = 2^k * (1 + 2 * full(n)) @@ -303,16 +313,13 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) evenGro Constant0 = pure Constant0 evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of Linear (VPar (ExEnd out)) -> do - half <- invertNatVal (NamedPort out "") (NumValue 0 (StrictMonoFun (StrictMono 1 (Linear ())))) - instantiateMeta (ExEnd out) (VNum (n2PowTimes 1 (nVar (VPar (toEnd half))))) + half <- invertNatVal (NumValue 0 (StrictMonoFun (StrictMono 1 mono))) + solveNumMeta (ExEnd out) (n2PowTimes 1 (nVar (VPar (toEnd half)))) pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd half))))) Linear (VPar (InEnd tgt)) -> do - twoSrc <- buildNum 2 - ((halfTgt,twoTgt),outSrc) <- buildArithOp Mul - wire (twoSrc, TNat, twoTgt) - wire (outSrc, TNat, NamedPort tgt "") - let _half = nVar (VPar (toEnd halfTgt)) - instantiateMeta (InEnd tgt) (VNum (n2PowTimes 1 (nVar (VPar (toEnd halfTgt))))) + halfTgt <- buildNatVal (NumValue 0 (StrictMonoFun (StrictMono 1 (Linear (VPar (toEnd tgt)))))) + let half = nVar (VPar (toEnd halfTgt)) + solveNumMeta (InEnd tgt) (n2PowTimes 1 half) pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd halfTgt))))) Full sm -> StrictMonoFun sm <$ demand0 (NumValue 0 (StrictMonoFun sm)) evenGro (StrictMonoFun (StrictMono n mono)) = pure (StrictMonoFun (StrictMono (n - 1) mono)) @@ -320,24 +327,19 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- Check a numval is odd, and return its rounded down half oddGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z)) oddGro (StrictMonoFun (StrictMono 0 mono)) = case mono of - Linear (VPar (ExEnd out)) -> do + -- TODO: Why aren't we using `out`?? + Linear (VPar (ExEnd _out)) -> do -- compute (/2) . (-1) - halfSrc <- invertNatVal (NamedPort out "") (NumValue 1 (StrictMonoFun (StrictMono 1 (Linear ())))) - instantiateMeta (ExEnd out) (VNum (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd halfSrc)))))) - pure (nVar (VPar (toEnd halfSrc))) - Linear (VPar (InEnd tgt)) -> do - twoSrc <- buildNum 2 - ((flooredHalfTgt, twoTgt), doubleSrc) <- buildArithOp Mul - wire (twoSrc, TNat, twoTgt) - - oneSrc <- buildNum 1 - ((doubleTgt, oneTgt), addOut) <- buildArithOp Add - wire (oneSrc, TNat, oneTgt) - wire (doubleSrc, TNat, doubleTgt) - wire (addOut, TNat, NamedPort tgt "") - - instantiateMeta (InEnd tgt) (VNum (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd flooredHalfTgt)))))) - pure (nVar (VPar (toEnd flooredHalfTgt))) + doubTgt <- invertNatVal (NumValue 1 (StrictMonoFun (StrictMono 1 mono))) + let [VPar (InEnd halfTgt)] = foldMap pure mono + solveNumMeta (toEnd doubTgt) (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd halfTgt))))) + pure (nVar (VPar (toEnd halfTgt))) + Linear (VPar (InEnd weeTgt)) -> do + -- compute (/2) . (-1) + bigTgt <- invertNatVal (NumValue 1 (StrictMonoFun (StrictMono 1 (Linear (VPar (toEnd weeTgt)))))) + let flooredHalf = nVar (VPar (toEnd weeTgt)) + solveNumMeta (toEnd bigTgt) (nPlus 1 (n2PowTimes 1 flooredHalf)) + pure flooredHalf -- full(n + 1) = 1 + 2 * full(n) -- hence, full(n) is the rounded down half From 0f7d13d4569d3ed005e8c260f2c1d9f397c1978c Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 8 Nov 2024 17:02:15 +0000 Subject: [PATCH 03/35] Revert `run` namespacing changes --- brat/Brat/Checker.hs | 5 +++-- brat/Brat/Load.hs | 4 ++-- brat/test/Test/Util.hs | 3 ++- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index dbd7924a..d98e26c1 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -1122,9 +1122,10 @@ abstractEndz ez = changeVar (ParToInx (AddZ (stackLen ez)) ez) run :: VEnv -> Store + -> Namespace -> Checking a -> Either Error (a, ([TypedHole], Store, Graph)) -run ve initStore m = do +run ve initStore ns m = do let ctx = Ctx { globalVEnv = ve , store = initStore -- TODO: fill with default constructors @@ -1134,7 +1135,7 @@ run ve initStore m = do , aliasTable = M.empty , hopeSet = M.empty } - (a,ctx,(holes, graph)) <- handler m ctx mempty + (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty let tyMap = typeMap $ store ctx -- If the hopeSet has any remaining holes with kind Nat, we need to abort. -- Even though we didn't need them for typechecking problems, our runtime diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs index 7d2c0747..0e16e288 100644 --- a/brat/Brat/Load.hs +++ b/brat/Brat/Load.hs @@ -138,7 +138,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS -- * A map from names to VDecls (aka an Env) -- * Some overs and outs?? let (globalNS, newRoot) = split "globals" ns - (entries, (_holes, kcStore, kcGraph)) <- run venv initStore $ localNS globalNS $ + (entries, (_holes, kcStore, kcGraph)) <- run venv initStore globalNS $ withAliases aliases $ forM decls $ \d -> localFC (fnLoc d) $ do let name = PrefixName pre (fnName d) (thing, ins :->> outs, sig, prefix) <- case (fnLocality d) of @@ -160,7 +160,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS let vdecls = map fst entries -- Now generate environment mapping usernames to nodes in the graph venv <- pure $ venv <> M.fromList [(name, overs) | ((name, _), (_, overs)) <- entries] - ((), (holes, newEndData, graph)) <- run venv kcStore $ localNS newRoot $ withAliases aliases $ do + ((), (holes, newEndData, graph)) <- run venv kcStore newRoot $ withAliases aliases $ do remaining <- "check_defs" -! foldM checkDecl' to_define vdecls pure $ assert (M.null remaining) () -- all to_defines were defined pure (venv, oldDecls <> vdecls, holes, oldEndData <> newEndData, kcGraph <> graph) diff --git a/brat/test/Test/Util.hs b/brat/test/Test/Util.hs index a2a170c6..1f50d9cc 100644 --- a/brat/test/Test/Util.hs +++ b/brat/test/Test/Util.hs @@ -5,13 +5,14 @@ import Brat.Checker.Monad import Brat.Checker.Types (initStore, emptyEnv) import Brat.Error import Brat.FC +import Brat.Naming import qualified Data.Set as S import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.ExpectedFailure -runEmpty m = run emptyEnv initStore m +runEmpty m = run emptyEnv initStore root m assertChecking :: Checking a -> Assertion assertChecking m = case runEmpty $ localFC (FC (Pos 0 0) (Pos 0 0)) m of From a53435bf8581cfafd2c1d4f41e3d15897741ae57 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 26 Nov 2024 09:41:05 +0000 Subject: [PATCH 04/35] Add defines --- brat/Brat/Checker/SolveHoles.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index e77289aa..48828766 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -2,11 +2,12 @@ module Brat.Checker.SolveHoles (typeEq, buildNatVal, buildNum, invertNatVal) whe import Brat.Checker.Monad import Brat.Checker.Types (kindForMode) -import Brat.Checker.Helpers (buildArithOp, buildConst, next) +import Brat.Checker.Helpers (buildArithOp, buildConst, defineSrc, defineTgt, next) import Brat.Error (ErrorMsg(..)) import Brat.Eval import Brat.Graph (NodeType(..)) import Brat.Syntax.Common +import Brat.Syntax.Port (ToEnd(..)) import Brat.Syntax.Simple (SimpleTerm(..)) import Brat.Syntax.Value import Control.Monad.Freer @@ -168,6 +169,7 @@ buildNatVal nv@(NumValue n gro) = case n of src <- buildGro gro wire (nDangling, TNat, lhs) wire (src, TNat, rhs) + defineSrc out (VNum (nPlus n (nVar (VPar (toEnd src))))) pure out where buildGro :: Fun00 (VVar Z) -> Checking Src @@ -187,6 +189,7 @@ buildNatVal nv@(NumValue n gro) = case n of monoDangling <- buildMono mono wire (factor, TNat, lhs) wire (monoDangling, TNat, rhs) + defineSrc out (VNum (n2PowTimes k (nVar (VPar (toEnd monoDangling))))) pure out buildMono :: Monotone (VVar Z) -> Checking Src @@ -203,6 +206,7 @@ buildNatVal nv@(NumValue n gro) = case n of ((lhs,rhs),out) <- buildArithOp Sub wire (outPlus1, TNat, lhs) wire (one, TNat, rhs) + defineSrc out (VNum (nFull (nVar (VPar (toEnd dangling))))) pure out buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv @@ -215,6 +219,7 @@ invertNatVal (NumValue up gro) = case up of wire (upSrc, TNat, rhs) tgt <- invertGro gro wire (out, TNat, tgt) + defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd out))))) pure lhs where invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" @@ -228,6 +233,7 @@ invertNatVal (NumValue up gro) = case up of tgt <- invertMono mono wire (out, TNat, tgt) wire (divisor, TNat, rhs) + defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd out))))) pure lhs invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval") @@ -235,4 +241,5 @@ invertNatVal (NumValue up gro) = case up of (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) tgt <- invertSM sm wire (llufSrc, TNat, tgt) + defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd llufSrc))))) pure llufTgt From fec32638f55b460c9518dbded3ba835788662950 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 26 Nov 2024 17:42:07 +0000 Subject: [PATCH 05/35] rename some variables --- brat/Brat/Checker/SolvePatterns.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 52103e2d..0eac19aa 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -219,16 +219,16 @@ solveNumMeta e nv = case (e, vars nv) of (ExEnd src, _) -> defineSrc (NamedPort src "") (VNum nv) -- Both targets, we need to create the thing that they both derive from - (InEnd tgt1, [VPar (InEnd tgt2)]) -> do + (InEnd bigTgt, [VPar (InEnd weeTgt)]) -> do (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt)))) - defineTgt (NamedPort tgt2 "") (VNum (nVar (VPar (toEnd idSrc)))) - wire (idSrc, TNat, NamedPort tgt2 "") + defineTgt (NamedPort weeTgt "") (VNum (nVar (VPar (toEnd idSrc)))) + wire (idSrc, TNat, NamedPort weeTgt "") let nv' = fmap (const (VPar (toEnd idSrc))) nv - src1 <- buildNatVal nv' - defineTgt (NamedPort tgt1 "") (VNum nv') - wire (src1, TNat, NamedPort tgt1 "") + bigSrc <- buildNatVal nv' + defineTgt (NamedPort bigTgt "") (VNum nv') + wire (bigSrc, TNat, NamedPort bigTgt "") -- RHS is constant or Src, wire it into tgt (InEnd tgt, _) -> do From c8cb33fd94d7aec243871bd1206db76b32c7d286 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 10:23:57 +0000 Subject: [PATCH 06/35] drive-by: Give everything created with anext a label --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 12 ++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index d98e26c1..9e45f784 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -476,7 +476,7 @@ check' (Simple tm) ((), ((hungry, ty):unders)) = do case (?my, ty, tm) of -- The only SimpleType that checks against a kind is a Nat (Braty, Left Nat, Num n) -> do - (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0) let val = VNum (nConstant (fromIntegral n)) defineSrc dangling val @@ -487,7 +487,7 @@ check' (Simple tm) ((), ((hungry, ty):unders)) = do _ -> do let vty = biType @m ty throwLeft $ simpleCheck ?my vty tm - (_, _, [(dangling, _)], _) <- anext @m "" (Const tm) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- anext @m "const" (Const tm) (S0,Some (Zy :* S0)) R0 (RPr ("value", vty) R0) wire (dangling, vty, hungry) pure (((), ()), ((), unders)) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 816bc5c0..03cae948 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -261,7 +261,7 @@ getThunks _ [] = pure ([], [], []) getThunks Braty row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectorise >>= \case (src, VFun Braty (ss :->> ts)) -> do (node, unders, overs, _) <- let ?my = Braty in - anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts + anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') -- These shouldn't happen @@ -269,7 +269,7 @@ getThunks Braty row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectori v -> typeErr $ "Force called on non-thunk: " ++ show v getThunks Kerny row@((src, Right ty):rest) = ((src,) <$> eval S0 ty) >>= vectorise >>= \case (src, VFun Kerny (ss :->> ts)) -> do - (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts + (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Kerny rest pure (node:nodes, unders <> unders', overs <> overs') (_, VFun _ _) -> err $ ExpectedThunk (showMode Kerny) (showRow row) @@ -278,7 +278,7 @@ getThunks Braty ((src, Left (Star args)):rest) = do (node, unders, overs) <- case bwdStack (B0 <>< args) of Some (_ :* stk) -> do let (ri,ro) = kindArgRows stk - (node, unders, overs, _) <- next "" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro + (node, unders, overs, _) <- next "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro pure (node, unders, overs) (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') @@ -355,7 +355,7 @@ vectorise (src, ty) = do let weak1 = changeVar (Thinning (ThDrop ThNull)) vecFun <- vectorisedFun len my cty (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <- - next "" MapFun (S0, Some (Zy :* S0)) + next "MapFun" MapFun (S0, Some (Zy :* S0)) (REx ("len", Nat) (RPr ("value", weak1 ty) R0)) (RPr ("vector", weak1 vecFun) R0) defineTgt lenTgt (VNum len) @@ -511,10 +511,10 @@ runArith _ _ _ = Nothing buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src) buildArithOp op = do - (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) + (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) pure ((lhs, rhs), out) buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do - (_, _, [(out,_)], _) <- next "" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out From 5b2cb452e961fcc9270561b1d9965364e660c973 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 10:25:16 +0000 Subject: [PATCH 07/35] Replace define -> instantiate --- brat/Brat/Checker/SolvePatterns.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 0eac19aa..2cd778c9 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -213,27 +213,27 @@ solveNumMeta e nv = case (e, vars nv) of (ExEnd src, [VPar (InEnd _tgt)]) -> do -- Compute the value of the `tgt` variable from the known `src` value by inverting nv tgtSrc <- invertNatVal nv - defineSrc (NamedPort src "") (VNum (nVar (VPar (toEnd tgtSrc)))) + instantiateMeta (ExEnd src) (VNum (nVar (VPar (toEnd tgtSrc)))) wire (NamedPort src "", TNat, tgtSrc) - (ExEnd src, _) -> defineSrc (NamedPort src "") (VNum nv) + (ExEnd src, _) -> instantiateMeta (ExEnd src) (VNum nv) -- Both targets, we need to create the thing that they both derive from (InEnd bigTgt, [VPar (InEnd weeTgt)]) -> do (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt)))) - defineTgt (NamedPort weeTgt "") (VNum (nVar (VPar (toEnd idSrc)))) + instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc)))) wire (idSrc, TNat, NamedPort weeTgt "") let nv' = fmap (const (VPar (toEnd idSrc))) nv bigSrc <- buildNatVal nv' - defineTgt (NamedPort bigTgt "") (VNum nv') + instantiateMeta (InEnd bigTgt) (VNum nv') wire (bigSrc, TNat, NamedPort bigTgt "") -- RHS is constant or Src, wire it into tgt (InEnd tgt, _) -> do src <- buildNatVal nv - defineTgt (NamedPort tgt "") (VNum nv) + instantiateMeta (InEnd tgt) (VNum nv) wire (src, TNat, NamedPort tgt "") where From ed531aeb100b030d3732d1b69dd27f18973b262f Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 10:27:17 +0000 Subject: [PATCH 08/35] Define targets instead of sources (fixes unified.brat) --- brat/Brat/Checker/SolveHoles.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 48828766..06342828 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -219,7 +219,7 @@ invertNatVal (NumValue up gro) = case up of wire (upSrc, TNat, rhs) tgt <- invertGro gro wire (out, TNat, tgt) - defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd out))))) + defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd tgt))))) pure lhs where invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" @@ -233,7 +233,7 @@ invertNatVal (NumValue up gro) = case up of tgt <- invertMono mono wire (out, TNat, tgt) wire (divisor, TNat, rhs) - defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd out))))) + defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd tgt))))) pure lhs invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval") @@ -241,5 +241,5 @@ invertNatVal (NumValue up gro) = case up of (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) tgt <- invertSM sm wire (llufSrc, TNat, tgt) - defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd llufSrc))))) + defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd tgt))))) pure llufTgt From c48da2cc1610c122c32313ac06ffc7a4341b0e90 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 11:00:38 +0000 Subject: [PATCH 09/35] fix: Dodgy demandSucc logic --- brat/Brat/Checker/SolvePatterns.hs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 2cd778c9..254923b8 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -289,11 +289,15 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) solveNumMeta (ExEnd x) (nPlus 1 y) pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y -} - - demandSucc sm@(StrictMono k (Linear (VPar (InEnd weeEnd)))) = do - bigEnd <- invertNatVal (NumValue 1 (StrictMonoFun sm)) - solveNumMeta (toEnd bigEnd) (NumValue 0 (StrictMonoFun sm)) - pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (InEnd weeEnd))) + -- 2^k * x + -- = 2^k * (y + 1) + -- = 2^k + 2^k * y + -- Hence, the predecessor is (2^k - 1) + (2^k * y) + demandSucc _sm@(StrictMono k (Linear (VPar (InEnd x)))) = do + (_, [(y,_)], _, _) <- anext "y" Hypo (S0, Some (Zy :* S0)) (REx ("", Nat) R0) R0 + yPlus1 <- invertNatVal (nPlus 1 (nVar (VPar (InEnd (end y))))) + solveNumMeta (InEnd x) (nVar (VPar (InEnd (end yPlus1)))) + pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (InEnd (end y)))) -- 2^k * full(n + 1) -- = 2^k * (1 + 2 * full(n)) From 95a4c2d14e2375f0ca3084914a31afd6d2400685 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 11:45:18 +0000 Subject: [PATCH 10/35] Define tgts to respective srcs in invertNatVal --- brat/Brat/Checker/SolveHoles.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 06342828..eda95a98 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -219,6 +219,7 @@ invertNatVal (NumValue up gro) = case up of wire (upSrc, TNat, rhs) tgt <- invertGro gro wire (out, TNat, tgt) + defineTgt tgt (VNum (nVar (VPar (toEnd out)))) defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd tgt))))) pure lhs where @@ -233,6 +234,7 @@ invertNatVal (NumValue up gro) = case up of tgt <- invertMono mono wire (out, TNat, tgt) wire (divisor, TNat, rhs) + defineTgt tgt (VNum (nVar (VPar (toEnd out)))) defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd tgt))))) pure lhs @@ -241,5 +243,6 @@ invertNatVal (NumValue up gro) = case up of (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) tgt <- invertSM sm wire (llufSrc, TNat, tgt) + defineTgt tgt (VNum (nVar (VPar (toEnd llufSrc)))) defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd tgt))))) pure llufTgt From 37ef790c752454ec74ed85571a248dfccd2b4d2d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 11:45:40 +0000 Subject: [PATCH 11/35] Allow hopes to be removed from the set --- brat/Brat/Checker/Monad.hs | 6 ++++++ brat/Brat/Checker/SolveHoles.hs | 13 +++++++------ 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index a69afdd8..735340b0 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -96,6 +96,7 @@ data CheckingSig ty where Define :: End -> Val Z -> CheckingSig () ANewHope :: (End, FC) -> CheckingSig () AskHopeSet :: CheckingSig HopeSet + RemoveHope :: End -> CheckingSig () localAlias :: (UserName, Alias) -> Checking v -> Checking v localAlias _ (Ret v) = Ret v @@ -278,6 +279,11 @@ handler (Req s k) ctx g AskHopeSet -> handler (k (hopeSet ctx)) ctx g + RemoveHope e -> let hset = hopeSet ctx in + if M.member e hset + then handler (k ()) (ctx { hopeSet = M.delete e hset }) g + else (Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e)))) + howStuck :: Val n -> Stuck howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e) howStuck (VLam bod) = howStuck bod diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index eda95a98..1e0e8d37 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -77,22 +77,23 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopeSet k exp act = do -- The Sem is closed, for now. -- TODO: This needs to update the BRAT graph with the solution. solveHope :: TypeKind -> End -> Sem -> Checking () -solveHope k e v = quote Zy v >>= \v -> case doesntOccur e v of +solveHope k hope@(InEnd i) v = quote Zy v >>= \v -> case doesntOccur hope v of Right () -> do - defineEnd e v + defineEnd hope v dangling <- case (k, v) of (Nat, VNum v) -> buildNatVal v (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum" _ -> buildConst Unit TUnit - let InEnd i = e - req $ Wire (end dangling, kindType k, i) - pure () + req (Wire (end dangling, kindType k, i)) + req (RemoveHope hope) Left msg -> case v of - VApp (VPar e') B0 | e == e' -> pure () + VApp (VPar 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 +solveHope _ hope@(ExEnd _) _ = err . InternalError $ + "solveHope: Hope was a src: " ++ show hope typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking () typeEqs _ _ [] [] [] = pure () From cebc93b29f03af5359dec4219226cb2b4327607d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 11:53:16 +0000 Subject: [PATCH 12/35] Cleanup Error.hs --- brat/Brat/Error.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs index 5027978a..ed1d1b1d 100644 --- a/brat/Brat/Error.hs +++ b/brat/Brat/Error.hs @@ -82,7 +82,6 @@ data ErrorMsg -- The argument is the row of unused connectors | ThunkLeftOvers String | ThunkLeftUnders String - -- TODO: Add file context here | RemainingNatHopes [String] instance Show ErrorMsg where @@ -167,9 +166,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:":indent (indent hs)) - -indent = fmap (" " ++) + show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":((" " ++) <$> hs)) data Error = Err { fc :: Maybe FC , msg :: ErrorMsg From c6e7c3c975ac17207a628dbfd39fd3a3b3c4cb8d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 11:59:58 +0000 Subject: [PATCH 13/35] Add golden file for unsolved hope error --- brat/test/golden/error/remaining_hopes.brat | 5 +++++ brat/test/golden/error/remaining_hopes.brat.golden | 8 ++++++++ 2 files changed, 13 insertions(+) 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/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 + + From 4e776cc8c9e48a50fb90e975756dd64e3f86bc49 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 12:08:13 +0000 Subject: [PATCH 14/35] XFAIL infer.brat because we don't compile `Pow` --- brat/test/Test/Compile/Hugr.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs index 11de7093..ef24aa26 100644 --- a/brat/test/Test/Compile/Hugr.hs +++ b/brat/test/Test/Compile/Hugr.hs @@ -38,6 +38,7 @@ nonCompilingExamples = expectedCheckingFails ++ expectedParsingFails ++ ,"fanout" -- Contains Selectors ,"vectorise" -- Generates MapFun nodes which aren't implemented yet ,"batcher-merge-sort" -- Generates MapFun nodes which aren't implemented yet + ,"infer" -- Generates `Pow` nodes which aren't implemented yet -- Victims of #13 ,"arith" ,"cqcconf" From 541f35ab1d6038ac4805a47e250549860f874b3b Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 12:22:36 +0000 Subject: [PATCH 15/35] Apply lints --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 4 ++-- brat/Brat/Checker/Monad.hs | 2 +- brat/Brat/Checker/SolveHoles.hs | 14 ++++++++------ brat/Brat/Eval.hs | 4 +--- brat/Control/Monad/Freer.hs | 2 +- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 21541b85..40983c9b 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -660,7 +660,7 @@ 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 ((), ((tgt, ty):unders)) = case (?my, ty) of +check' Hope ((), (tgt, ty):unders) = case (?my, ty) of (Braty, Left _k) -> do fc <- req AskFC req (ANewHope (toEnd tgt, fc)) @@ -731,7 +731,7 @@ checkBody fnName body cty = do NoLhs tm -> pure (tm, (fcOf tm, fcOf tm)) Clauses (c :| cs) -> do fc <- req AskFC - pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c)) + pure (WC fc (Lambda c cs), bimap fcOf fcOf c) Undefined -> err (InternalError "Checking undefined clause") ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do (((), ()), leftovers) <- check tm conns diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 182cc083..882a787c 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -380,10 +380,10 @@ valueToBinder Braty = Right valueToBinder Kerny = id defineSrc :: Src -> Val Z -> Checking () -defineSrc src v = defineEnd (ExEnd (end src)) v +defineSrc src = defineEnd (ExEnd (end src)) defineTgt :: Tgt -> Val Z -> Checking () -defineTgt tgt v = defineEnd (InEnd (end tgt)) v +defineTgt tgt = defineEnd (InEnd (end tgt)) declareSrc :: Src -> Modey m -> BinderType m -> Checking () declareSrc src my ty = req (Declare (ExEnd (end src)) my ty) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index b2b1a1d3..b42fe61b 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -282,7 +282,7 @@ handler (Req s k) ctx g RemoveHope e -> let hset = hopeSet ctx in if M.member e hset then handler (k ()) (ctx { hopeSet = M.delete e hset }) g - else (Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e)))) + else Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e))) howStuck :: Val n -> Stuck howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 59286905..adebc80e 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -15,7 +15,8 @@ import Bwd import Hasochism import Util (zipSameLength) -import Data.Foldable (traverse_) +import Data.Bifunctor (second) +import Data.Foldable (sequenceA_) import Data.Functor import qualified Data.Map as M import Data.Type.Equality (TestEquality(..), (:~:)(..)) @@ -106,11 +107,12 @@ typeEqRow :: Modey m -> 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) + :* ((:~:) 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 <&> \(res, probs) -> (res, (typeEq tm stuff (kindForMode m) ty1 ty2):probs) +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" @@ -144,13 +146,13 @@ typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' = 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 - traverse_ id probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized + 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 >>= (traverse_ id . concat) + Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat) where - eqVariant (Some r0, Some r1) = throwLeft $ (snd <$> typeEqRow m0 tm lvkz r0 r1) + eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1) typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1) wire :: (Src, Val Z, Tgt) -> Checking () diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs index bc991ec4..f9ae33d3 100644 --- a/brat/Brat/Eval.hs +++ b/brat/Brat/Eval.hs @@ -302,9 +302,7 @@ eqTests tm lvkz = go -- 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) = case getNumVar nv of - Just e' -> collision e e' - _ -> pure () +doesntOccur e (VNum nv) = traverse_ (collision e) (getNumVar nv) where getNumVar :: NumVal (VVar n) -> Maybe End getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of diff --git a/brat/Control/Monad/Freer.hs b/brat/Control/Monad/Freer.hs index 34e35732..2fb24058 100644 --- a/brat/Control/Monad/Freer.hs +++ b/brat/Control/Monad/Freer.hs @@ -21,7 +21,7 @@ updateEnd (News m) e = case M.lookup e m of -- The RHS of the operation is the newer news -- Invariant: The domains of these Newses are disjoint instance Semigroup News where - (News m1) <> n2@(News m2) = News (m2 `M.union` (M.map (/// n2) m1)) + (News m1) <> n2@(News m2) = News (m2 `M.union` M.map (/// n2) m1) instance Monoid News where mempty = News M.empty From 8ad05de5ca9b0d398c329ae2081b8b5afddb831a Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Wed, 27 Nov 2024 12:28:04 +0000 Subject: [PATCH 16/35] Revert "drive-by: Give everything created with anext a label" This reverts commit c8cb33fd94d7aec243871bd1206db76b32c7d286. --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 12 ++++++------ brat/test/golden/error/remaining_hopes.brat.golden | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 40983c9b..4f56f1ba 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -486,7 +486,7 @@ check' (Simple tm) ((), (hungry, ty):unders) = do case (?my, ty, tm) of -- The only SimpleType that checks against a kind is a Nat (Braty, Left Nat, Num n) -> do - (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0) let val = VNum (nConstant (fromIntegral n)) defineSrc dangling val @@ -497,7 +497,7 @@ check' (Simple tm) ((), (hungry, ty):unders) = do _ -> do let vty = biType @m ty throwLeft $ simpleCheck ?my vty tm - (_, _, [(dangling, _)], _) <- anext @m "const" (Const tm) (S0,Some (Zy :* S0)) + (_, _, [(dangling, _)], _) <- anext @m "" (Const tm) (S0,Some (Zy :* S0)) R0 (RPr ("value", vty) R0) wire (dangling, vty, hungry) pure (((), ()), ((), unders)) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 882a787c..b6812e79 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -250,7 +250,7 @@ getThunks _ [] = pure ([], [], []) getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Braty (ss :->> ts)) -> do (node, unders, overs, _) <- let ?my = Braty in - anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts + anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') -- These shouldn't happen @@ -258,7 +258,7 @@ getThunks Braty row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) v -> typeErr $ "Force called on non-thunk: " ++ show v getThunks Kerny row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case (src, VFun Kerny (ss :->> ts)) -> do - (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts + (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts (nodes, unders', overs') <- getThunks Kerny rest pure (node:nodes, unders <> unders', overs <> overs') (_, VFun _ _) -> err $ ExpectedThunk (showMode Kerny) (showRow row) @@ -267,7 +267,7 @@ getThunks Braty ((src, Left (Star args)):rest) = do (node, unders, overs) <- case bwdStack (B0 <>< args) of Some (_ :* stk) -> do let (ri,ro) = kindArgRows stk - (node, unders, overs, _) <- next "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro + (node, unders, overs, _) <- next "" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro pure (node, unders, overs) (nodes, unders', overs') <- getThunks Braty rest pure (node:nodes, unders <> unders', overs <> overs') @@ -344,7 +344,7 @@ vectorise (src, ty) = do let weak1 = changeVar (Thinning (ThDrop ThNull)) vecFun <- vectorisedFun len my cty (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <- - next "MapFun" MapFun (S0, Some (Zy :* S0)) + next "" MapFun (S0, Some (Zy :* S0)) (REx ("len", Nat) (RPr ("value", weak1 ty) R0)) (RPr ("vector", weak1 vecFun) R0) defineTgt lenTgt (VNum len) @@ -499,10 +499,10 @@ runArith _ _ _ = Nothing buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src) buildArithOp op = do - (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) + (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) pure ((lhs, rhs), out) buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do - (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + (_, _, [(out,_)], _) <- next "" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out diff --git a/brat/test/golden/error/remaining_hopes.brat.golden b/brat/test/golden/error/remaining_hopes.brat.golden index 80d15436..49009d3a 100644 --- a/brat/test/golden/error/remaining_hopes.brat.golden +++ b/brat/test/golden/error/remaining_hopes.brat.golden @@ -3,6 +3,6 @@ g = f(!) ^^^ Expected to work out values for these holes: - In checking_check_defs_1_g_1_Eval 0 + In checking_check_defs_1_g_1_ 0 From 0cef0d3065fa10c0d88ad20b37396690747b06cb Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Thu, 28 Nov 2024 09:33:52 +0000 Subject: [PATCH 17/35] drive-by: Give labels to more `next` calls --- brat/Brat/Checker.hs | 4 ++-- brat/Brat/Checker/Helpers.hs | 4 ++-- brat/Brat/Load.hs | 2 +- brat/test/golden/graph/cons.brat.graph | 8 ++++---- brat/test/golden/graph/kernel.brat.graph | 4 ++-- brat/test/golden/graph/vec.brat.graph | 4 ++-- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 40983c9b..adcc002b 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -806,7 +806,7 @@ kindCheck ((hungry, k@(TypeFor m [])):unders) (Con c arg) = req (TLup (m, c)) >> -- the thing we *do* define kindOut as (_, argUnders, [(kindOut,_)], (_ :<< _va, _)) <- - next "" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0) + next "aliasargs" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0) -- arg is a juxtaposition (args, emptyUnders) <- kindCheck (second (\(Left k) -> k) <$> argUnders) (unWC arg) ensureEmpty "alias args" emptyUnders @@ -876,7 +876,7 @@ kindCheck unders (Emb (WC fc (Var v))) = localFC fc $ vlup v >>= f unders f _ (x:_) = err $ InternalError $ "Kindchecking a row which contains " ++ show x -- TODO: Add other operations on numbers kindCheck ((hungry, Nat):unders) (Simple (Num n)) | n >= 0 = do - (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0) + (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0) let value = VNum (nConstant (fromIntegral n)) defineTgt hungry value defineSrc dangling value diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index b2c5574b..713a10b3 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -499,10 +499,10 @@ runArith _ _ _ = Nothing buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src) buildArithOp op = do - (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) + (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0) pure ((lhs, rhs), out) buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do - (_, _, [(out,_)], _) <- next "" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs index 026996d5..b6897fd1 100644 --- a/brat/Brat/Load.hs +++ b/brat/Brat/Load.hs @@ -115,7 +115,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do loadAlias :: TypeAlias -> Checking (QualName, Alias) loadAlias (TypeAlias fc name args body) = localFC fc $ do - (_, [(hhungry, Left k)], _, _) <- next "" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0 + (_, [(hhungry, Left k)], _, _) <- next "aliasargs" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0 let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args ([v], unders) <- kindCheck [(hhungry, k)] $ Th (WC fc (Lambda (abs, WC fc body) [])) ensureEmpty "loadAlias unders" unders diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph index a9dcaf65..cc61c7b8 100644 --- a/brat/test/golden/graph/cons.brat.graph +++ b/brat/test/golden/graph/cons.brat.graph @@ -6,12 +6,12 @@ Nodes: (check_defs_1_two_const_1,BratNode (Const 1) [] [("value",Int)]) (check_defs_1_two_const_3,BratNode (Const 2) [] [("value",Int)]) (check_defs_1_two_nil_4,BratNode (Constructor nil) [] [("value",Vec(Int, 0))]) -(globals__3,BratNode (Const 2) [] [("value",Nat)]) -(globals__8,BratNode (Const 3) [] [("value",Nat)]) (globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (globals_Int_7,BratNode (Constructor Int) [] [("value",[])]) (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) +(globals_const_3,BratNode (Const 2) [] [("value",Nat)]) +(globals_const_8,BratNode (Const 3) [] [("value",Nat)]) (globals_decl_4_two,BratNode Id [("a1",Vec(Int, 2))] [("a1",Vec(Int, 2))]) (globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))]) @@ -27,6 +27,6 @@ Wires: (Ex globals_Int_7 0,[],In globals_Vec_6 0) (Ex globals_Vec_1 0,[],In globals___kca_two 0) (Ex globals_Vec_6 0,[],In globals___kca_three_5 0) -(Ex globals__3 0,Nat,In globals_Vec_1 1) -(Ex globals__8 0,Nat,In globals_Vec_6 1) +(Ex globals_const_3 0,Nat,In globals_Vec_1 1) +(Ex globals_const_8 0,Nat,In globals_Vec_6 1) (Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_1_cons 1) diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph index 9544c538..26ad580e 100644 --- a/brat/test/golden/graph/kernel.brat.graph +++ b/brat/test/golden/graph/kernel.brat.graph @@ -13,12 +13,12 @@ Nodes: (check_defs_1_id3_thunk/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)]) (check_defs_1_id3_thunk/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] []) (check_defs_1_id3_thunk_thunk_2,BratNode (Box (fromList []) check_defs_1_id3_thunk/in check_defs_1_id3_thunk/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) -(globals__8,BratNode (Const 3) [] [("value",Nat)]) (globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])]) (globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])]) (globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])]) (globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])]) (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) +(globals_const_8,BratNode (Const 3) [] [("value",Nat)]) (globals_decl_9_id3,BratNode Id [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })] [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })]) Wires: @@ -39,4 +39,4 @@ Wires: (Ex globals_Qubit_4 0,[],In globals___kcr__1 2) (Ex globals_Qubit_7 0,[],In globals_Vec_6 0) (Ex globals_Vec_6 0,[],In globals___kcr__5 0) -(Ex globals__8 0,Nat,In globals_Vec_6 1) +(Ex globals_const_8 0,Nat,In globals_Vec_6 1) diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph index 137a9bf8..844bd6c8 100644 --- a/brat/test/golden/graph/vec.brat.graph +++ b/brat/test/golden/graph/vec.brat.graph @@ -6,9 +6,9 @@ Nodes: (check_defs_1_xs_const_3,BratNode (Const 1) [] [("value",Int)]) (check_defs_1_xs_const_5,BratNode (Const 2) [] [("value",Int)]) (check_defs_1_xs_nil_6,BratNode (Constructor nil) [] [("value",Vec(Int, 0))]) -(globals__3,BratNode (Const 3) [] [("value",Nat)]) (globals_Int_2,BratNode (Constructor Int) [] [("value",[])]) (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])]) +(globals_const_3,BratNode (Const 3) [] [("value",Nat)]) (globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))]) Wires: @@ -21,4 +21,4 @@ Wires: (Ex check_defs_1_xs_nil_6 0,Vec(Int, 0),In check_defs_1_xs_cons_4 1) (Ex globals_Int_2 0,[],In globals_Vec_1 0) (Ex globals_Vec_1 0,[],In globals___kca_xs 0) -(Ex globals__3 0,Nat,In globals_Vec_1 1) +(Ex globals_const_3 0,Nat,In globals_Vec_1 1) From c4ebd8c07cb59634806881cb822f76d8962b99c1 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 13:33:51 +0000 Subject: [PATCH 18/35] [cleanup] Remove News datatype from this PR --- brat/Brat/Checker/Monad.hs | 22 ---------------- brat/Control/Monad/Freer.hs | 51 +------------------------------------ 2 files changed, 1 insertion(+), 72 deletions(-) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index b42fe61b..76a556a8 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -18,7 +18,6 @@ import Control.Monad.Freer import Control.Monad.Fail () import Data.List (intercalate) import qualified Data.Map as M -import qualified Data.Set as S -- import Debug.Trace @@ -284,27 +283,6 @@ handler (Req s k) ctx g then handler (k ()) (ctx { hopeSet = M.delete e hset }) g else Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e))) -howStuck :: Val n -> Stuck -howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e) -howStuck (VLam bod) = howStuck bod -howStuck (VCon _ _) = Unstuck -howStuck (VFun _ _) = Unstuck -howStuck (VSum _ _) = Unstuck --- Numbers are likely to cause problems. --- Whether they are stuck or not depends on the question we're asking! -howStuck (VNum (NumValue 0 gro)) = howStuckGro gro - where - howStuckGro Constant0 = Unstuck - howStuckGro (StrictMonoFun f) = howStuckSM f - - howStuckSM (StrictMono 0 mono) = howStuckMono mono - howStuckSM _ = AwaitingAny mempty - - howStuckMono (Full sm) = howStuckSM sm - howStuckMono (Linear (VPar e)) = AwaitingAny (S.singleton e) -- ALAN was VHop - howStuckMono (Linear _) = AwaitingAny mempty -howStuck _ = AwaitingAny mempty - type Checking = Free CheckingSig instance Semigroup a => Semigroup (Checking a) where diff --git a/brat/Control/Monad/Freer.hs b/brat/Control/Monad/Freer.hs index 2fb24058..ebb1e310 100644 --- a/brat/Control/Monad/Freer.hs +++ b/brat/Control/Monad/Freer.hs @@ -1,42 +1,7 @@ -module Control.Monad.Freer where +module Control.Monad.Freer (Free(..), req) where import Control.Monad ((>=>)) import Data.Kind (Type) -import qualified Data.Map as M -import qualified Data.Set as S - -import Brat.Syntax.Port - --- A mapping of metavars to metavars, for a single problem: --- * e -> Unstuck means e has been solved --- * e -> Awaiting es means the problem's been transferred --- * e not in news means no change to e -newtype News = News (M.Map End Stuck) - -updateEnd :: News -> End -> Stuck -updateEnd (News m) e = case M.lookup e m of - Nothing -> AwaitingAny (S.singleton e) - Just s -> s - --- The RHS of the operation is the newer news --- Invariant: The domains of these Newses are disjoint -instance Semigroup News where - (News m1) <> n2@(News m2) = News (m2 `M.union` M.map (/// n2) m1) - -instance Monoid News where - mempty = News M.empty - -data Stuck - = Unstuck - | AwaitingAny (S.Set End) - deriving Show - -instance Semigroup Stuck where - (AwaitingAny es1) <> (AwaitingAny es2) = AwaitingAny (S.union es1 es2) - _ <> _ = Unstuck - -instance Monoid Stuck where - mempty = AwaitingAny S.empty data Free (sig :: Type -> Type) (v :: Type) where Ret :: v -> Free sig v @@ -46,20 +11,6 @@ instance Functor (Free sig) where fmap f (Ret v) = Ret (f v) fmap f (Req sig k) = Req sig (fmap f . k) -class NewsWatcher t where - (///) :: t -> News -> t - -instance NewsWatcher Stuck where - Unstuck /// _ = Unstuck - (AwaitingAny es) /// n = foldMap (updateEnd n) es - -instance NewsWatcher (News -> t) where - f /// n = f . (n <>) - -instance NewsWatcher (Free sig v) where - Ret v /// _ = Ret v - Req sig k /// n = Req sig $ \v -> k v /// n - instance Applicative (Free sig) where pure = Ret (Ret f) <*> ma = fmap f ma From 991e0dc42b57fd9aff0b2e190e6e5e45100e1193 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 13:35:20 +0000 Subject: [PATCH 19/35] Update brat/Brat/Checker/Monad.hs Co-authored-by: Alan Lawrence --- brat/Brat/Checker/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index 76a556a8..c63e41da 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -281,7 +281,7 @@ handler (Req s k) ctx g RemoveHope e -> let hset = hopeSet ctx in if M.member e hset then handler (k ()) (ctx { hopeSet = M.delete e hset }) g - else Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e))) + else Left (dumbErr (InternalError ("Trying to remove Hope not in set: " ++ show e))) type Checking = Free CheckingSig From f82f25c5dfb0291a664db759e24cfcece42ab0fd Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 13:54:21 +0000 Subject: [PATCH 20/35] refactor: Move Nat building code to Helpers --- brat/Brat/Checker/Helpers.hs | 93 ++++++++++++++++++++++++++++ brat/Brat/Checker/SolveHoles.hs | 99 +----------------------------- brat/Brat/Checker/SolvePatterns.hs | 1 - 3 files changed, 94 insertions(+), 99 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index a52629bb..0141c69e 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -506,3 +506,96 @@ buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out + +buildNum :: Integer -> Checking Src +buildNum n = buildConst (Num (fromIntegral n)) TNat + +-- Generate wiring to produce a dynamic instance of the numval argument +-- N.B. In these functions, we wire using Req, rather than the `wire` function +-- because we don't want it to do any extra evaluation. +buildNatVal :: NumVal (VVar Z) -> Checking Src +buildNatVal nv@(NumValue n gro) = case n of + 0 -> buildGro gro + n -> do + nDangling <- buildNum n + ((lhs,rhs),out) <- buildArithOp Add + src <- buildGro gro + req $ Wire (end nDangling, TNat, end lhs) + req $ Wire (end src, TNat, end rhs) + defineSrc out (VNum (nPlus n (nVar (VPar (toEnd src))))) + pure out + where + buildGro :: Fun00 (VVar Z) -> Checking Src + buildGro Constant0 = buildNum 0 + buildGro (StrictMonoFun sm) = buildSM sm + + buildSM :: StrictMono (VVar Z) -> Checking Src + buildSM (StrictMono k mono) = do + -- Calculate 2^k as `factor` + two <- buildNum 2 + kDangling <- buildNum k + ((lhs,rhs),factor) <- buildArithOp Pow + req $ Wire (end two, TNat, end lhs) + req $ Wire (end kDangling, TNat, end rhs) + -- Multiply mono by 2^k + ((lhs,rhs),out) <- buildArithOp Mul + monoDangling <- buildMono mono + req $ Wire (end factor, TNat, end lhs) + req $ Wire (end monoDangling, TNat, end rhs) + defineSrc out (VNum (n2PowTimes k (nVar (VPar (toEnd monoDangling))))) + pure out + + buildMono :: Monotone (VVar Z) -> Checking Src + buildMono (Linear (VPar (ExEnd e))) = pure $ NamedPort e "numval" + buildMono (Full sm) = do + -- Calculate 2^n as `outPlus1` + two <- buildNum 2 + dangling <- buildSM sm + ((lhs,rhs),outPlus1) <- buildArithOp Pow + req $ Wire (end two, TNat, end lhs) + req $ Wire (end dangling, TNat, end rhs) + -- Then subtract 1 + one <- buildNum 1 + ((lhs,rhs),out) <- buildArithOp Sub + req $ Wire (end outPlus1, TNat, end lhs) + req $ Wire (end one, TNat, end rhs) + defineSrc out (VNum (nFull (nVar (VPar (toEnd dangling))))) + pure out + buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv + +invertNatVal :: NumVal (VVar Z) -> Checking Tgt +invertNatVal (NumValue up gro) = case up of + 0 -> invertGro gro + _ -> do + ((lhs,rhs),out) <- buildArithOp Sub + upSrc <- buildNum up + req $ Wire (end upSrc, TNat, end rhs) + tgt <- invertGro gro + req $ Wire (end out, TNat, end tgt) + defineTgt tgt (VNum (nVar (VPar (toEnd out)))) + defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd tgt))))) + pure lhs + where + invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" + invertGro (StrictMonoFun sm) = invertSM sm + + invertSM (StrictMono k mono) = case k of + 0 -> invertMono mono + _ -> do + divisor <- buildNum (2 ^ k) + ((lhs,rhs),out) <- buildArithOp Div + tgt <- invertMono mono + req $ Wire (end out, TNat, end tgt) + req $ Wire (end divisor, TNat, end rhs) + defineTgt tgt (VNum (nVar (VPar (toEnd out)))) + defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd tgt))))) + pure lhs + + invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval") + invertMono (Full sm) = do + (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) + tgt <- invertSM sm + req $ Wire (end llufSrc, TNat, end tgt) + defineTgt tgt (VNum (nVar (VPar (toEnd llufSrc)))) + defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd tgt))))) + pure llufTgt diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index adebc80e..a584e134 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -2,12 +2,10 @@ module Brat.Checker.SolveHoles (typeEq, buildNatVal, buildNum, invertNatVal) whe import Brat.Checker.Monad import Brat.Checker.Types (kindForMode) -import Brat.Checker.Helpers (buildArithOp, buildConst, defineSrc, defineTgt, next) +import Brat.Checker.Helpers (buildConst, buildNatVal, buildNum, invertNatVal) import Brat.Error (ErrorMsg(..)) import Brat.Eval -import Brat.Graph (NodeType(..)) import Brat.Syntax.Common -import Brat.Syntax.Port (ToEnd(..)) import Brat.Syntax.Simple (SimpleTerm(..)) import Brat.Syntax.Value import Control.Monad.Freer @@ -154,98 +152,3 @@ typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1) 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) - -wire :: (Src, Val Z, Tgt) -> Checking () -wire (src, ty, tgt) = req $ Wire (end src, ty, end tgt) - -buildNum :: Integer -> Checking Src -buildNum n = buildConst (Num (fromIntegral n)) TNat - - --- Generate wiring to produce a dynamic instance of the numval argument -buildNatVal :: NumVal (VVar Z) -> Checking Src -buildNatVal nv@(NumValue n gro) = case n of - 0 -> buildGro gro - n -> do - nDangling <- buildNum n - ((lhs,rhs),out) <- buildArithOp Add - src <- buildGro gro - wire (nDangling, TNat, lhs) - wire (src, TNat, rhs) - defineSrc out (VNum (nPlus n (nVar (VPar (toEnd src))))) - pure out - where - buildGro :: Fun00 (VVar Z) -> Checking Src - buildGro Constant0 = buildNum 0 - buildGro (StrictMonoFun sm) = buildSM sm - - buildSM :: StrictMono (VVar Z) -> Checking Src - buildSM (StrictMono k mono) = do - -- Calculate 2^k as `factor` - two <- buildNum 2 - kDangling <- buildNum k - ((lhs,rhs),factor) <- buildArithOp Pow - wire (two, TNat, lhs) - wire (kDangling, TNat, rhs) - -- Multiply mono by 2^k - ((lhs,rhs),out) <- buildArithOp Mul - monoDangling <- buildMono mono - wire (factor, TNat, lhs) - wire (monoDangling, TNat, rhs) - defineSrc out (VNum (n2PowTimes k (nVar (VPar (toEnd monoDangling))))) - pure out - - buildMono :: Monotone (VVar Z) -> Checking Src - buildMono (Linear (VPar (ExEnd e))) = pure $ NamedPort e "numval" - buildMono (Full sm) = do - -- Calculate 2^n as `outPlus1` - two <- buildNum 2 - dangling <- buildSM sm - ((lhs,rhs),outPlus1) <- buildArithOp Pow - wire (two, TNat, lhs) - wire (dangling, TNat, rhs) - -- Then subtract 1 - one <- buildNum 1 - ((lhs,rhs),out) <- buildArithOp Sub - wire (outPlus1, TNat, lhs) - wire (one, TNat, rhs) - defineSrc out (VNum (nFull (nVar (VPar (toEnd dangling))))) - pure out - buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv - -invertNatVal :: NumVal (VVar Z) -> Checking Tgt -invertNatVal (NumValue up gro) = case up of - 0 -> invertGro gro - _ -> do - ((lhs,rhs),out) <- buildArithOp Sub - upSrc <- buildNum up - wire (upSrc, TNat, rhs) - tgt <- invertGro gro - wire (out, TNat, tgt) - defineTgt tgt (VNum (nVar (VPar (toEnd out)))) - defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd tgt))))) - pure lhs - where - invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable" - invertGro (StrictMonoFun sm) = invertSM sm - - invertSM (StrictMono k mono) = case k of - 0 -> invertMono mono - _ -> do - divisor <- buildNum (2 ^ k) - ((lhs,rhs),out) <- buildArithOp Div - tgt <- invertMono mono - wire (out, TNat, tgt) - wire (divisor, TNat, rhs) - defineTgt tgt (VNum (nVar (VPar (toEnd out)))) - defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd tgt))))) - pure lhs - - invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval") - invertMono (Full sm) = do - (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0) - tgt <- invertSM sm - wire (llufSrc, TNat, tgt) - defineTgt tgt (VNum (nVar (VPar (toEnd llufSrc)))) - defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd tgt))))) - pure llufTgt diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 0032c0bd..ae1e9fb3 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -2,7 +2,6 @@ module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve) import Brat.Checker.Monad import Brat.Checker.Helpers -import Brat.Checker.SolveHoles (buildNatVal, invertNatVal) import Brat.Checker.Types (EndType(..)) import Brat.Constructors import Brat.Constructors.Patterns From f75ce8ce9960268c3f6410d10ae23ce3bcc721e1 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 13:55:26 +0000 Subject: [PATCH 21/35] refactor: Replace mkStaticNum with a call to buildNatVal --- brat/Brat/Checker/Helpers.hs | 48 +----------------------------------- 1 file changed, 1 insertion(+), 47 deletions(-) diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 0141c69e..7efd43f5 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -276,58 +276,12 @@ vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes ,CTy m Z -- The function type at the end ) vecLayers my (TVec ty (VNum n)) = do - src <- mkStaticNum n + src <- buildNatVal n first ((src, n):) <$> vecLayers my ty vecLayers Braty (VFun Braty cty) = pure ([], cty) vecLayers Kerny (VFun Kerny cty) = pure ([], cty) vecLayers my ty = typeErr $ "Expected a " ++ showMode my ++ "function or vector of functions, got " ++ show ty -mkStaticNum :: NumVal (VVar Z) -> Checking Src -mkStaticNum n@(NumValue c gro) = do - (_, [], [(constSrc,_)], _) <- next "const" (Const (Num (fromIntegral c))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0) - src <- case gro of - Constant0 -> pure constSrc - StrictMonoFun sm -> do - (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "add_const" (ArithNode Add) (S0, Some (Zy :* S0)) - (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) - (RPr ("value", TNat) R0) - smSrc <- mkStrictMono sm - wire (constSrc, TNat, lhs) - wire (smSrc, TNat, rhs) - pure src - defineSrc src (VNum n) - pure src - where - mkStrictMono :: StrictMono (VVar Z) -> Checking Src - mkStrictMono (StrictMono k mono) = do - (_, [], [(constSrc,_)], _) <- next "2^k" (Const (Num (2^k))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0) - (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "mult_const" (ArithNode Mul) (S0, Some (Zy :* S0)) - (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) - (RPr ("value", TNat) R0) - monoSrc <- mkMono mono - wire (constSrc, TNat, lhs) - wire (monoSrc, TNat, rhs) - pure src - - mkMono :: Monotone (VVar Z) -> Checking Src - mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono") - mkMono (Full sm) = do - (_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0) - (_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0)) - (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) - (RPr ("value", TNat) R0) - smSrc <- mkStrictMono sm - wire (twoSrc, TNat, lhs) - wire (smSrc, TNat, rhs) - - (_, [], [(oneSrc,_)], _) <- next "1" (Const (Num 1)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0) - (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "n-1" (ArithNode Sub) (S0, Some (Zy :* S0)) - (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) - (RPr ("value", TNat) R0) - wire (powSrc, TNat, lhs) - wire (oneSrc, TNat, rhs) - pure src - vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z) vectorise my (src, ty) = do (layers, cty) <- vecLayers my ty From da0860813e4c16968030e051b5d8dff9b7575a69 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 14:08:44 +0000 Subject: [PATCH 22/35] Revert changes to FC --- brat/Brat/FC.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/brat/Brat/FC.hs b/brat/Brat/FC.hs index ab50a96f..958df5d1 100644 --- a/brat/Brat/FC.hs +++ b/brat/Brat/FC.hs @@ -2,7 +2,11 @@ module Brat.FC where data Pos = Pos { line :: Int , col :: Int - } deriving (Eq, Show) + } deriving Eq + +instance Show Pos where + show (Pos { .. }) = show line ++ ":" ++ show col + instance Ord Pos where compare (Pos l c) (Pos l' c') | l == l' = compare c c' From 575474eae59cb3651feb70d0bc358e60420f4b3a Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 14:59:09 +0000 Subject: [PATCH 23/35] Apply suggestions from code review Co-authored-by: Alan Lawrence --- brat/Brat/Checker/SolveHoles.hs | 6 ++++-- brat/Brat/Checker/SolvePatterns.hs | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index a584e134..7b407df7 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -55,7 +55,7 @@ typeEqEta tm (lvy :* kz :* sems) hopeSet (TypeFor m ((_, k):ks)) exp act = do typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopeSet (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) --- "easy" flex cases +-- 1. "easy" flex cases typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k (SApp (SPar e) B0) act | M.member e hopeSet = solveHope k e act typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0) @@ -63,12 +63,14 @@ typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0) typeEqEta _ (Zy :* _ :* _) hopeSet Nat exp act | Just (SPar e) <- isNumVar exp, M.member e hopeSet = solveHope Nat e act | Just (SPar e) <- isNumVar act, M.member e hopeSet = 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) hopeSet k exp act = do exp <- quote ny exp act <- quote ny act case [e | (VApp (VPar e) _) <- [exp,act], M.member e hopeSet] of [] -> typeEqRigid tm stuff k exp act - _es -> error "TODO" + [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" -- uhhh -- Yield(AwaitingAny $ S.fromList es) (\_ -> typeEq tm stuff k exp act) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index ae1e9fb3..f57f2b96 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -222,7 +222,7 @@ solveNumMeta e nv = case (e, vars nv) of defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt)))) instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc)))) wire (idSrc, TNat, NamedPort weeTgt "") - let nv' = fmap (const (VPar (toEnd idSrc))) nv + let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace bigSrc <- buildNatVal nv' instantiateMeta (InEnd bigTgt) (VNum nv') wire (bigSrc, TNat, NamedPort bigTgt "") From c6555b95f0f6d43fbd4289e78cb955080632cb73 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 14:23:07 +0000 Subject: [PATCH 24/35] rename HopeSet -> Hopes --- brat/Brat/Checker.hs | 6 +++--- brat/Brat/Checker/Helpers.hs | 2 +- brat/Brat/Checker/Monad.hs | 14 +++++++------- brat/Brat/Checker/SolveHoles.hs | 29 +++++++++++++++-------------- 4 files changed, 26 insertions(+), 25 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 4e2310e7..ca20215f 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -1139,14 +1139,14 @@ run ve initStore ns m = do , kconstructors = kernelConstructors , typeConstructors = defaultTypeConstructors , aliasTable = M.empty - , hopeSet = M.empty + , hopes = M.empty } (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty let tyMap = typeMap $ store ctx - -- If the hopeSet has any remaining holes with kind Nat, we need to abort. + -- 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 e) (hopeSet ctx) of + case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap 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 diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs index 7efd43f5..36455224 100644 --- a/brat/Brat/Checker/Helpers.hs +++ b/brat/Brat/Checker/Helpers.hs @@ -458,7 +458,7 @@ buildArithOp op = do buildConst :: SimpleTerm -> Val Z -> Checking Src buildConst tm ty = do - (_, _, [(out,_)], _) <- next "const" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) + (_, _, [(out,_)], _) <- next "buildConst" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0) pure out buildNum :: Integer -> Checking Src diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index c63e41da..606fa889 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -50,7 +50,7 @@ data CtxEnv = CtxEnv , locals :: VEnv } -type HopeSet = M.Map End FC +type Hopes = M.Map End FC data Context = Ctx { globalVEnv :: VEnv , store :: Store @@ -59,7 +59,7 @@ data Context = Ctx { globalVEnv :: VEnv , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)] , aliasTable :: M.Map QualName Alias -- All the ends here should be targets - , hopeSet :: HopeSet + , hopes :: Hopes } data CheckingSig ty where @@ -94,7 +94,7 @@ data CheckingSig ty where Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () ANewHope :: (End, FC) -> CheckingSig () - AskHopeSet :: CheckingSig HopeSet + AskHopes :: CheckingSig Hopes RemoveHope :: End -> CheckingSig () localAlias :: (QualName, Alias) -> Checking v -> Checking v @@ -274,13 +274,13 @@ handler (Req s k) ctx g M.lookup tycon tbl handler (k args) ctx g - ANewHope (e, fc) -> handler (k ()) (ctx { hopeSet = M.insert e fc (hopeSet ctx) }) g + ANewHope (e, fc) -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g - AskHopeSet -> handler (k (hopeSet ctx)) ctx g + AskHopes -> handler (k (hopes ctx)) ctx g - RemoveHope e -> let hset = hopeSet ctx in + RemoveHope e -> let hset = hopes ctx in if M.member e hset - then handler (k ()) (ctx { hopeSet = M.delete e hset }) g + 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 diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 7b407df7..b5490738 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -29,7 +29,7 @@ typeEq :: String -- String representation of the term for error reporting -> Val n -- Actual -> Checking () typeEq str stuff@(_ny :* _ks :* sems) k exp act = do - hopes <- req AskHopeSet + hopes <- req AskHopes exp <- sem sems exp act <- sem sems act typeEqEta str stuff hopes k exp act @@ -41,40 +41,41 @@ 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 - -> HopeSet -- The hope set + -> 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) hopeSet (TypeFor m ((_, k):ks)) exp act = do +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)) hopeSet (TypeFor m ks) exp act + 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) hopeSet k (SApp (SPar e) B0) act - | M.member e hopeSet = solveHope k e act -typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0) - | M.member e hopeSet = solveHope k e exp -typeEqEta _ (Zy :* _ :* _) hopeSet Nat exp act - | Just (SPar e) <- isNumVar exp, M.member e hopeSet = solveHope Nat e act - | Just (SPar e) <- isNumVar act, M.member e hopeSet = solveHope Nat e exp +typeEqEta _tm (Zy :* _ks :* _sems) hopes k (SApp (SPar e) B0) act + | M.member e hopes = solveHope k e act +typeEqEta _tm (Zy :* _ks :* _sems) hopes k exp (SApp (SPar e) B0) + | M.member e hopes = solveHope k e exp +typeEqEta _ (Zy :* _ :* _) hopes Nat exp act + | Just (SPar e) <- isNumVar exp, M.member e hopes = solveHope Nat e act + | Just (SPar 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) hopeSet k exp act = do +typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do exp <- quote ny exp act <- quote ny act - case [e | (VApp (VPar e) _) <- [exp,act], M.member e hopeSet] of + case [e | (VApp (VPar 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" -- uhhh -- Yield(AwaitingAny $ S.fromList es) (\_ -> typeEq tm stuff k exp act) --- This will update the hopeSet, potentially invalidating things that have been eval'd +-- This will update the `hopes` set, potentially invalidating things that have +-- been eval'd. -- The Sem is closed, for now. -- TODO: This needs to update the BRAT graph with the solution. solveHope :: TypeKind -> End -> Sem -> Checking () From d077d4c9e40685f0969ce43f276b3d5bc9627e2d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 14:44:43 +0000 Subject: [PATCH 25/35] refactor: Make GHC enforce that Hopes are InPorts --- brat/Brat/Checker.hs | 6 +++--- brat/Brat/Checker/Monad.hs | 6 +++--- brat/Brat/Checker/SolveHoles.hs | 22 ++++++++++------------ 3 files changed, 16 insertions(+), 18 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index ca20215f..38f4bd21 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -660,10 +660,10 @@ 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 ((), (tgt, ty):unders) = case (?my, ty) of +check' Hope ((), ((NamedPort hope _, ty):unders)) = case (?my, ty) of (Braty, Left _k) -> do fc <- req AskFC - req (ANewHope (toEnd tgt, fc)) + req (ANewHope (hope, fc)) pure (((), ()), ((), unders)) (Braty, Right _ty) -> typeErr "Can only infer kinded things with !" (Kerny, _) -> typeErr "Won't infer kernel typed !" @@ -1146,7 +1146,7 @@ run ve initStore ns m = do -- 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 e) (hopes ctx) of + 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 diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index 606fa889..e8a003b7 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -50,7 +50,7 @@ data CtxEnv = CtxEnv , locals :: VEnv } -type Hopes = M.Map End FC +type Hopes = M.Map InPort FC data Context = Ctx { globalVEnv :: VEnv , store :: Store @@ -93,9 +93,9 @@ data CheckingSig ty where AskVEnv :: CheckingSig CtxEnv Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () - ANewHope :: (End, FC) -> CheckingSig () + ANewHope :: (InPort, FC) -> CheckingSig () AskHopes :: CheckingSig Hopes - RemoveHope :: End -> CheckingSig () + RemoveHope :: InPort -> CheckingSig () localAlias :: (QualName, Alias) -> Checking v -> Checking v localAlias _ (Ret v) = Ret v diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index b5490738..df3398b9 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -56,18 +56,18 @@ typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do -- 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 e) B0) act +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 e) B0) +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 e) <- isNumVar exp, M.member e hopes = solveHope Nat e act - | Just (SPar e) <- isNumVar act, M.member e hopes = solveHope Nat e exp + | 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 e) _) <- [exp,act], M.member e hopes] of + 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" @@ -78,24 +78,22 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do -- been eval'd. -- The Sem is closed, for now. -- TODO: This needs to update the BRAT graph with the solution. -solveHope :: TypeKind -> End -> Sem -> Checking () -solveHope k hope@(InEnd i) v = quote Zy v >>= \v -> case doesntOccur hope v of +solveHope :: TypeKind -> InPort -> Sem -> Checking () +solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of Right () -> do - defineEnd hope v + defineEnd (InEnd hope) v dangling <- case (k, v) of (Nat, VNum v) -> buildNatVal v (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum" _ -> buildConst Unit TUnit - req (Wire (end dangling, kindType k, i)) + req (Wire (end dangling, kindType k, hope)) req (RemoveHope hope) Left msg -> case v of - VApp (VPar end) B0 | hope == end -> pure () + 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 -solveHope _ hope@(ExEnd _) _ = err . InternalError $ - "solveHope: Hope was a src: " ++ show hope typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking () typeEqs _ _ [] [] [] = pure () From 741d896a3e29f299a85fb5ebc4cb9e90fa2d4461 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 14:45:43 +0000 Subject: [PATCH 26/35] refactor: Curry ANewHope --- brat/Brat/Checker.hs | 2 +- brat/Brat/Checker/Monad.hs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 38f4bd21..997381f2 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -663,7 +663,7 @@ check' (Of n e) ((), unders) = case ?my of check' Hope ((), ((NamedPort hope _, ty):unders)) = case (?my, ty) of (Braty, Left _k) -> do fc <- req AskFC - req (ANewHope (hope, fc)) + req (ANewHope hope fc) pure (((), ()), ((), unders)) (Braty, Right _ty) -> typeErr "Can only infer kinded things with !" (Kerny, _) -> typeErr "Won't infer kernel typed !" diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs index e8a003b7..cb9fd015 100644 --- a/brat/Brat/Checker/Monad.hs +++ b/brat/Brat/Checker/Monad.hs @@ -93,7 +93,7 @@ data CheckingSig ty where AskVEnv :: CheckingSig CtxEnv Declare :: End -> Modey m -> BinderType m -> CheckingSig () Define :: End -> Val Z -> CheckingSig () - ANewHope :: (InPort, FC) -> CheckingSig () + ANewHope :: InPort -> FC -> CheckingSig () AskHopes :: CheckingSig Hopes RemoveHope :: InPort -> CheckingSig () @@ -274,7 +274,7 @@ 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 + ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g AskHopes -> handler (k (hopes ctx)) ctx g From bb431eff7e55ea5d2852948f50eea6a92c354249 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 15:11:07 +0000 Subject: [PATCH 27/35] refactor: Expose only a simpler version of typeEq --- brat/Brat/Checker.hs | 10 +++++----- brat/Brat/Checker/SolveHoles.hs | 26 +++++++++++++++++--------- 2 files changed, 22 insertions(+), 14 deletions(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 997381f2..0239df22 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -125,13 +125,13 @@ checkWire Braty (WC fc tm) outputs (dangling, o) (hungry, u) = localFC fc $ do let ot = binderToValue Braty o let ut = binderToValue Braty u if outputs - then typeEq (show tm) (Zy :* S0 :* S0) (Star []) ot ut - else typeEq (show tm) (Zy :* S0 :* S0) (Star []) ut ot + then typeEq (show tm) (Star []) ot ut + else typeEq (show tm) (Star []) ut ot wire (dangling, ot, hungry) checkWire Kerny (WC fc tm) outputs (dangling, ot) (hungry, ut) = localFC fc $ do if outputs - then typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ot ut - else typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ut ot + then typeEq (show tm) (Dollar []) ot ut + else typeEq (show tm) (Dollar []) ut ot wire (dangling, ot, hungry) checkIO :: forall m d k exp act . (CheckConstraints m k, ?my :: Modey m) @@ -556,7 +556,7 @@ check' FanIn (overs, (tgt, ty):unders) = do let k = case my of Kerny -> Dollar [] Braty -> Star [] - typeEq (show FanIn) (Zy :* S0 :* S0) k elTy (binderToValue my overTy) + typeEq (show FanIn) k elTy (binderToValue my overTy) let tailTy = TVec elTy (VNum (nConstant (n - 1))) (_, [(hungryHead, _), (hungryTail, tailTy)], [(danglingResult, _)], _) <- anext "faninNodes" (Constructor (plain "cons")) (S0, Some (Zy :* S0)) (RPr ("head", elTy) (RPr ("tail", tailTy) R0) :: Ro m Z Z) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index df3398b9..376367bf 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -19,16 +19,24 @@ import Data.Functor import qualified Data.Map as M import Data.Type.Equality (TestEquality(..), (:~:)(..)) --- 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. +-- External interface to typeEq' for closed values only. 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 + -> Val Z -- Expected + -> Val Z -- Actual -> Checking () -typeEq str stuff@(_ny :* _ks :* sems) k exp act = do +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 @@ -97,7 +105,7 @@ solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of 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 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 @@ -111,7 +119,7 @@ typeEqRow :: Modey m ) 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)) + ((:) (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" From b846a622c2cae53fd960ac8f8782223e3fe8a5e0 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 15:13:11 +0000 Subject: [PATCH 28/35] cosmetic: Get rid of unused variable --- brat/Brat/Checker/SolvePatterns.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index f57f2b96..ca1f0ab6 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -289,7 +289,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- = 2^k * (y + 1) -- = 2^k + 2^k * y -- Hence, the predecessor is (2^k - 1) + (2^k * y) - demandSucc _sm@(StrictMono k (Linear (VPar (InEnd x)))) = do + demandSucc (StrictMono k (Linear (VPar (InEnd x)))) = do (_, [(y,_)], _, _) <- anext "y" Hypo (S0, Some (Zy :* S0)) (REx ("", Nat) R0) R0 yPlus1 <- invertNatVal (nPlus 1 (nVar (VPar (InEnd (end y))))) solveNumMeta (InEnd x) (nVar (VPar (InEnd (end yPlus1)))) From 8bee0d014fbcdba8d0f3a94d758ccb0dcade50b1 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 15:15:42 +0000 Subject: [PATCH 29/35] cleanup: Get rid of outdated comments --- brat/Brat/Checker/SolveHoles.hs | 3 --- brat/Brat/Checker/SolvePatterns.hs | 2 -- 2 files changed, 5 deletions(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index 376367bf..edd10f3c 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -79,13 +79,10 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do [] -> 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" --- uhhh --- Yield(AwaitingAny $ S.fromList es) (\_ -> typeEq tm stuff k exp act) -- This will update the `hopes` set, potentially invalidating things that have -- been eval'd. -- The Sem is closed, for now. --- TODO: This needs to update the BRAT graph with the solution. solveHope :: TypeKind -> InPort -> Sem -> Checking () solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of Right () -> do diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index ca1f0ab6..5e4e32a7 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -101,7 +101,6 @@ solve my ((src, PCon c abs):p) = do (tests, sol) <- solve my p pure ((src, PrimLitTest (Num 0)):tests, sol) _ -> case M.lookup c natConstructors of - -- This `relationToInner` is very sus - it doesn't do any wiring! Just (Just _, relationToInner) -> do (node, [], kids@[(dangling, _)], _) <- next "unpacked_nat" Hypo (S0, Some (Zy :* S0)) R0 -- we don't need to wire the src in; we just need the inner stuff @@ -206,7 +205,6 @@ instantiateMeta e val = do solveNumMeta :: End -> NumVal (VVar Z) -> Checking () solveNumMeta e nv = case (e, vars nv) of -- Compute the thing that the rhs should be based on the src, and instantiate src to that - -- TODO: sus that we're not using `tgt`?? (ExEnd src, [VPar (InEnd _tgt)]) -> do -- Compute the value of the `tgt` variable from the known `src` value by inverting nv tgtSrc <- invertNatVal nv From 631509ebe489f5a9fc3ca0b1c2841016025a3abe Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 15:42:41 +0000 Subject: [PATCH 30/35] Don't reexport nat building from SolveHoles --- brat/Brat/Checker/SolveHoles.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs index edd10f3c..801ec0fe 100644 --- a/brat/Brat/Checker/SolveHoles.hs +++ b/brat/Brat/Checker/SolveHoles.hs @@ -1,8 +1,8 @@ -module Brat.Checker.SolveHoles (typeEq, buildNatVal, buildNum, invertNatVal) where +module Brat.Checker.SolveHoles (typeEq, buildNum) where import Brat.Checker.Monad import Brat.Checker.Types (kindForMode) -import Brat.Checker.Helpers (buildConst, buildNatVal, buildNum, invertNatVal) +import Brat.Checker.Helpers (buildConst, buildNatVal, buildNum) import Brat.Error (ErrorMsg(..)) import Brat.Eval import Brat.Syntax.Common From 5a3ffd889640aa7fad9c70e743f9ed4f4496b2f1 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 15:52:23 +0000 Subject: [PATCH 31/35] [broken] New example --- brat/examples/unified.brat | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/brat/examples/unified.brat b/brat/examples/unified.brat index f04c167a..b4d86236 100644 --- a/brat/examples/unified.brat +++ b/brat/examples/unified.brat @@ -28,3 +28,7 @@ swapFront(X :: *, n :: #, Vec(X, n)) -> Vec(X, n) swapFront(_, _, []) = [] swapFront(_, _, [x]) = [x] swapFront(X, _, cons(x, cons(y, zs))) = cons(y, cons(x, zs)) + +mapAndConquer(X :: *, Y :: *, n :: #, f :: { X -> Y }, Vec(X, succ(n))) -> Vec(Y, succ(n)) +mapAndConquer(_, _, doub(n), f, xsl =, x ,= xsr) = mapAndConquer(!, !, !, f, xsl) =, f(x) ,= mapAndConquer(!, !, !, f, xsr) +mapAndConquer(_, _, succ(n), f, xsl =,= xsr) = mapAndConquer(!, !, !, f, xsl) =,= mapAndConquer(!, !, !, f, xsr) From 7286b0ced774164004f6c05c8c5b80eabf5ec539 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 17:11:00 +0000 Subject: [PATCH 32/35] refactor: Make better use of `toEnd` function --- brat/Brat/Checker/SolvePatterns.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index 5e4e32a7..e8308a08 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -77,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" @@ -96,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) @@ -107,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 @@ -289,9 +289,9 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- Hence, the predecessor is (2^k - 1) + (2^k * y) demandSucc (StrictMono k (Linear (VPar (InEnd x)))) = do (_, [(y,_)], _, _) <- anext "y" Hypo (S0, Some (Zy :* S0)) (REx ("", Nat) R0) R0 - yPlus1 <- invertNatVal (nPlus 1 (nVar (VPar (InEnd (end y))))) - solveNumMeta (InEnd x) (nVar (VPar (InEnd (end yPlus1)))) - pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (InEnd (end y)))) + yPlus1 <- invertNatVal (nPlus 1 (nVar (VPar (toEnd y)))) + solveNumMeta (InEnd x) (nVar (VPar (toEnd yPlus1))) + pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (toEnd y))) -- 2^k * full(n + 1) -- = 2^k * (1 + 2 * full(n)) From 787baedce4d07f50fe31e9051b44f6b904d918c5 Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Tue, 3 Dec 2024 17:12:19 +0000 Subject: [PATCH 33/35] Fill in the missing case for demandSucc --- brat/Brat/Checker/SolvePatterns.hs | 14 +++++++------- brat/examples/unified.brat | 9 ++++++--- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs index e8308a08..f9ed0b0d 100644 --- a/brat/Brat/Checker/SolvePatterns.hs +++ b/brat/Brat/Checker/SolvePatterns.hs @@ -276,13 +276,13 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro) -- 2^k * x -- = 2^k * (y + 1) -- = 2^k + 2^k * y - demandSucc _sm@(StrictMono _k (Linear (VPar (ExEnd _x)))) = error "Todo..." {-do - -- This is sus because we don't have any tgt? - ySrc <- invertNatVal (NamedPort x "") (NumValue 1 (StrictMonoFun sm)) - let y = nVar (VPar (toEnd ySrc)) - solveNumMeta (ExEnd x) (nPlus 1 y) - pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y - -} + demandSucc (StrictMono k (Linear (VPar (ExEnd x)))) = do + (_, [(yTgt, _)], [(ySrc, _)], _) <- + next "yId" Id (S0, Some (Zy :* S0)) (REx ("value", Nat) R0) (REx ("value", Nat) R0) + + defineSrc ySrc (VNum (nVar (VPar (toEnd yTgt)))) + instantiateMeta (ExEnd x) (VNum (nPlus 1 (nVar (VPar (toEnd yTgt))))) + pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (toEnd ySrc))) -- 2^k * x -- = 2^k * (y + 1) -- = 2^k + 2^k * y diff --git a/brat/examples/unified.brat b/brat/examples/unified.brat index b4d86236..cabab3e0 100644 --- a/brat/examples/unified.brat +++ b/brat/examples/unified.brat @@ -29,6 +29,9 @@ swapFront(_, _, []) = [] swapFront(_, _, [x]) = [x] swapFront(X, _, cons(x, cons(y, zs))) = cons(y, cons(x, zs)) -mapAndConquer(X :: *, Y :: *, n :: #, f :: { X -> Y }, Vec(X, succ(n))) -> Vec(Y, succ(n)) -mapAndConquer(_, _, doub(n), f, xsl =, x ,= xsr) = mapAndConquer(!, !, !, f, xsl) =, f(x) ,= mapAndConquer(!, !, !, f, xsr) -mapAndConquer(_, _, succ(n), f, xsl =,= xsr) = mapAndConquer(!, !, !, f, xsl) =,= mapAndConquer(!, !, !, f, xsr) +filled(X :: *, n :: #, Vec(X, full(n))) -> Vec(X, full(n)) +filled(_, n, xsl =, x ,= xsr) = xsl =, x ,= xsr + +-- mapAndConquer(X :: *, Y :: *, n :: #, f :: { X -> Y }, Vec(X, succ(n))) -> Vec(Y, succ(n)) +-- mapAndConquer(_, _, doub(n), f, xsl =, x ,= xsr) = mapAndConquer(!, !, n, f, xsl) =, f(x) ,= mapAndConquer(!, !, n, f, xsr) +-- mapAndConquer(_, _, succ(doub(n)), f, xsl =,= xsr) = mapAndConquer(!, !, n, f, xsl) =,= mapAndConquer(!, !, n, f, xsr) From ca5df296b6c53035436d2c94ee90de6556c2d66d Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 6 Dec 2024 10:55:29 +0000 Subject: [PATCH 34/35] fix: Add missing unelab cases --- brat/Brat/Unelaborator.hs | 2 ++ 1 file changed, 2 insertions(+) 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 From 837eeed54a1b761d2d38735e376a65d9cbc393da Mon Sep 17 00:00:00 2001 From: Craig Roy Date: Fri, 6 Dec 2024 11:03:11 +0000 Subject: [PATCH 35/35] lint: Redundant brackets --- brat/Brat/Checker.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs index 0239df22..3b317be0 100644 --- a/brat/Brat/Checker.hs +++ b/brat/Brat/Checker.hs @@ -660,7 +660,7 @@ 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 +check' Hope ((), (NamedPort hope _, ty):unders) = case (?my, ty) of (Braty, Left _k) -> do fc <- req AskFC req (ANewHope hope fc)