Skip to content

Commit

Permalink
fix: maxID looks at type ids (#1109)
Browse files Browse the repository at this point in the history
  • Loading branch information
brprice committed Aug 10, 2023
2 parents e603e61 + 5cce9ab commit e3f2d18
Showing 1 changed file with 20 additions and 8 deletions.
28 changes: 20 additions & 8 deletions primer/test/Tests/Action.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@
module Tests.Action where

import Foreword
import Prelude (error)

import Data.Data (Data)
import Data.Generics.Uniplate.Data (universe)
import Hedgehog hiding (
Action,
Property,
Var,
property,
)
import Optics (maximumOf)
import Primer.Action (
Action (..),
ActionError (CaseBindsClash, NameCapture),
Expand All @@ -23,15 +23,17 @@ import Primer.Builtins.DSL (listOf)
import Primer.Core (
Expr,
Expr' (..),
HasID,
ID (..),
Kind' (KType),
Meta (Meta),
Pattern (PatCon, PatPrim),
PrimCon (PrimChar),
TmVarRef (LocalVarRef),
Type' (TEmptyHole, TForall),
getID,
)
import Primer.Core.DSL
import Primer.Core.Utils (exprIDs)
import Primer.Gen.Core.Raw (
evalExprGen,
genExpr,
Expand All @@ -57,11 +59,21 @@ import Primer.Zipper (
import Tasty (Property, property)
import Test.Tasty.HUnit (Assertion, assertFailure, (@?=))

-- Note: 'unsafeMaximum' is partial, but we believe that 'maxID' itself is
-- safe due to the fact that 'universe x' always contains at least
-- `x`.
maxID :: (HasID a, Data a) => a -> ID
maxID = unsafeMaximum . map getID . universe
-- Note: the 'fromMaybe' will only ever see a 'Just' (i.e. could be replaced
-- with 'fromJust'), since 'exprIDs' will always target at least one ID (namely,
-- the ID at the root)
maxID :: Expr -> ID
maxID e = fromMaybe (getID e) $ maximumOf exprIDs e

unit_maxID :: Assertion
unit_maxID =
let m :: ID -> Meta (Maybe a)
m i = Meta i Nothing Nothing
h = EmptyHole . m
expr a b c d e f = App (m a) (h b) (APP (m c) (h d) $ TForall (m e) "a" (KType ()) (TEmptyHole $ m f))
in for_ (permutations [0 .. 5]) $ \case
[a, b, c, d, e, f] -> maxID (expr a b c d e f) @?= 5
_ -> error "impossible"

tasty_ConstructVar_succeeds_on_hole_when_in_scope :: Property
tasty_ConstructVar_succeeds_on_hole_when_in_scope = property $ do
Expand Down

0 comments on commit e3f2d18

Please sign in to comment.