From 7c65f3efaa960ef86595d63af54d7002ea908932 Mon Sep 17 00:00:00 2001 From: LeitMoth Date: Fri, 19 Jul 2024 17:39:55 -0500 Subject: [PATCH] fix term equality bug, I just had things backwards --- src/Disco/Exhaustiveness.hs | 25 +++++++++-------- src/Disco/Exhaustiveness/Constraint.hs | 39 ++++---------------------- src/Disco/Exhaustiveness/TypeInfo.hs | 2 +- 3 files changed, 20 insertions(+), 46 deletions(-) diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 51217784..fa225d12 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -73,7 +73,7 @@ allSame :: (Eq a) => [a] -> Bool allSame [] = True allSame (x : xs) = all (x ==) xs --- TODO: explain. this was a pain +-- TODO(colin): explain. this was a pain desugarTuplePats :: [APattern] -> APattern desugarTuplePats [] = error "Found empty tuple, what happened?" desugarTuplePats [p] = p @@ -85,7 +85,8 @@ desugarMatch var pat = do case pat of (APWild _) -> return [] (APVar ty name) -> do - return $ [(var, GHerebyBe $ TI.TypedVar (name, TI.extractRelevant ty))] + let newAlias = TI.TypedVar (name, TI.extractRelevant ty) + return $ [(newAlias, GWasOriginally var)] (APNat _ nat) -> return [(var, GMatch (TI.natural nat) [])] (APUnit) -> return [(var, GMatch TI.unit [])] (APBool b) -> return [(var, GMatch (TI.bool b) [])] @@ -104,7 +105,7 @@ desugarMatch var pat = do (APTup ty [_, _]) -> error $ "Tuple type that wasn't a pair???: " ++ show ty (APTup _ sugary) -> desugarMatch var (desugarTuplePats sugary) (APList _ subs) -> do - -- TODO: review, will this be a problem like tuples? + -- TODO(colin): review, will this be a problem like tuples? let types = map (TI.extractRelevant . Ty.getType) subs when (not . allSame $ types) @@ -113,7 +114,7 @@ desugarMatch var pat = do guards <- sequence $ zipWith desugarMatch vars subs return $ (var, (GMatch (TI.list types) vars)) : concat guards (APCons _ subHead subTail) -> do - -- TODO: review, will this be a problem like tuples? + -- TODO(colin): review, will this be a problem like tuples? let typeHead = (TI.extractRelevant . Ty.getType) subHead let typeTail = (TI.extractRelevant . Ty.getType) subTail varHead <- TI.newVar typeHead @@ -122,7 +123,7 @@ desugarMatch var pat = do guardsTail <- desugarMatch varTail subTail let guardCons = (var, (GMatch (TI.cons typeHead typeTail) [varHead, varTail])) return $ [guardCons] ++ guardsHead ++ guardsTail - -- TODO: consider the rest of the patterns + -- TODO(colin): consider the rest of the patterns -- (APAdd) e -> return [] @@ -136,7 +137,7 @@ type Guard = (TI.TypedVar, GuardConstraint) data GuardConstraint where GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint - GHerebyBe :: TI.TypedVar -> GuardConstraint + GWasOriginally :: TI.TypedVar -> GuardConstraint deriving (Show, Eq) data Literal where @@ -148,7 +149,7 @@ data Literal where data LitCond where LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond LitNot :: TI.DataCon -> LitCond - LitHerebyBe :: TI.TypedVar -> LitCond + LitWasOriginally :: TI.TypedVar -> LitCond deriving (Show, Eq, Ord) data Ant where @@ -163,8 +164,8 @@ ua nrefs gdt = case gdt of (n1, u1) <- ua nrefs t1 (n2, u2) <- ua n1 t2 return (n2, ABranch u1 u2) - Guarded (x, GHerebyBe z) t -> do - n <- addLitMulti nrefs $ LitCond (x, LitHerebyBe z) + Guarded (y, GWasOriginally x) t -> do + n <- addLitMulti nrefs $ LitCond (y, LitWasOriginally x) ua n t Guarded (x, (GMatch dc args)) t -> do n <- addLitMulti nrefs $ LitCond (x, LitMatch dc args) @@ -187,8 +188,8 @@ addLiteral (context, constraints) flit = case flit of F -> MaybeT $ pure Nothing T -> return (context, constraints) LitCond (x, c) -> case c of - LitHerebyBe z -> - (context `C.addVars` [z], constraints) `C.addConstraint` (x, C.CHerebyBe z) + LitWasOriginally z -> + (context `C.addVars` [x], constraints) `C.addConstraint` (x, C.CWasOriginally z) LitMatch dc args -> (context `C.addVars` args, constraints) `C.addConstraint` (x, C.CMatch dc args) LitNot dc -> @@ -208,7 +209,7 @@ joinComma = foldr1 (join ", ") joinSpace :: [String] -> String joinSpace = foldr1 (join " ") --- TODO: maybe fully print out tuples even if they have wildcars in the middle? +-- TODO(colin): maybe fully print out tuples even if they have wildcars in the middle? -- e.g. (1,_,_) instead of just (1,_) prettyInhab :: InhabPat -> String prettyInhab (IPNot []) = "_" diff --git a/src/Disco/Exhaustiveness/Constraint.hs b/src/Disco/Exhaustiveness/Constraint.hs index 34d97bd9..646c97d6 100644 --- a/src/Disco/Exhaustiveness/Constraint.hs +++ b/src/Disco/Exhaustiveness/Constraint.hs @@ -19,7 +19,7 @@ addVars (Context ctx) vars = Context (ctx ++ vars) data Constraint where CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint CNot :: TI.DataCon -> Constraint - CHerebyBe :: TI.TypedVar -> Constraint + CWasOriginally :: TI.TypedVar -> Constraint deriving (Show, Eq, Ord) posMatch :: [Constraint] -> Maybe (TI.DataCon, [TI.TypedVar]) @@ -36,7 +36,7 @@ type ConstraintFor = (TI.TypedVar, Constraint) lookupVar :: TI.TypedVar -> [ConstraintFor] -> TI.TypedVar lookupVar x = foldr getNextId x where - getNextId (x', CHerebyBe y) | x' == x = const y + getNextId (x', CWasOriginally y) | x' == x = const y getNextId _ = id alistLookup :: (Eq a) => a -> [(a, b)] -> [b] @@ -47,33 +47,6 @@ onVar x cs = alistLookup (lookupVar x cs) cs type NormRefType = (Context, [ConstraintFor]) -{- - TODO: fix this! -FIXME: big bug! - -in haskell, look at this: - -thing :: (Int, Bool) -> () -thing (n,True) = () -thing (0,n) = () - -haskell reports (p, False) uncovered where p is one of {0} - -but our solver just responds with (_, False) uncovered. -Its dropping the info about the 0!!! - -This is present in my test implementation, -I just didn't discover it until now :[ - -Clue discovered! -If we swap these like this: -thing (0,n) = unit -thing (n,True) = unit -Our solver actually gets this right! - -This is a good clue to start with --} - addConstraints :: (Members '[Fresh] r) => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType addConstraints = foldM addConstraint @@ -91,7 +64,7 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of Just args' -> addConstraints nref - (zipWith (\a b -> (a, CHerebyBe b)) args args') + (zipWith (\a b -> (a, CWasOriginally b)) args args') Nothing -> return added --- Equation (11) CNot _ -> do @@ -99,7 +72,7 @@ addConstraintHelper nref@(ctx, cns) cf@(origX, c) = case c of guard inh -- ensure that origX is still inhabited, as per I2 return added -- Equation (14) - CHerebyBe y -> do + CWasOriginally y -> do let origY = lookupVar y cns if origX == origY then return nref @@ -130,7 +103,7 @@ conflictsWith c = case c of CNot k -> \case (CMatch k' _) | k == k' -> True -- 11a _ -> False - CHerebyBe _ -> const False + CWasOriginally _ -> const False -- Search for a MatchDataCon that is matching on k specifically -- (there should be at most one, see I4 in section 3.4) @@ -151,7 +124,7 @@ substituteVarIDs y x = map (\(var, c) -> (subst var, c)) -- if a variable in the context has a resolvable type, there must be at least one constructor -- which can be instantiated without contradiction of the refinement type -- This function tests if this is true --- NOTE: we may eventually have type constraints +-- NOTE(colin): we may eventually have type constraints -- and we would need to worry pulling them from nref here inhabited :: (Members '[Fresh] r) => NormRefType -> TI.TypedVar -> Sem r Bool inhabited n var = case TI.tyDataCons . TI.getType $ var of diff --git a/src/Disco/Exhaustiveness/TypeInfo.hs b/src/Disco/Exhaustiveness/TypeInfo.hs index 42f4a016..e4804b85 100644 --- a/src/Disco/Exhaustiveness/TypeInfo.hs +++ b/src/Disco/Exhaustiveness/TypeInfo.hs @@ -98,7 +98,7 @@ extractRelevant t = Type {tyIdent = t, tyDataCons = Nothing} -- extractRelevant ty = error $ "Bad type in exhaust" ++ show ty --- TODO: should these really just be blank names? +-- TODO(colin): should these really just be blank names? newName :: (Member Fresh r) => Sem r (Name ATerm) newName = fresh $ s2n ""