1
1
mirror of https://github.com/anoma/juvix.git synced 2024-09-11 16:26:33 +03:00

Fix minor issue with ==% for type equality (#1780)

This commit is contained in:
Jonathan Cubides 2023-01-27 19:34:25 +01:00 committed by GitHub
parent 384653f630
commit 6d49c9c9f1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 10 additions and 7 deletions

View File

@ -162,6 +162,7 @@ juvix-format: $(TOFORMAT)
$(TOFORMAT): %:
@echo "Formatting $@"
@juvix dev scope $@ --with-comments > $@.tmp
@echo "" >> $@.tmp
@mv $@.tmp $@
@echo "Typechecking formatted $@"
@juvix typecheck $@ --only-errors

View File

@ -285,11 +285,8 @@ infix 4 ===
(===) :: (IsExpression a, IsExpression b) => a -> b -> Bool
a === b = (toExpression a ==% toExpression b) mempty
infix 4 ==%
-- TODO: make it symmetric
(==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
(==%) a b free =
leftEq :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
leftEq a b free =
isRight
. run
. runError @Text
@ -297,6 +294,11 @@ infix 4 ==%
. evalState (mempty @(HashMap Name Name))
$ matchExpressions (toExpression a) (toExpression b)
infix 4 ==%
(==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
(==%) a b free = leftEq a b free || leftEq b a free
infixl 9 @@
(@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression

View File

@ -13,7 +13,7 @@ registerTrace f = do
b <- freshVar "b"
let freeVars = HashSet.fromList [a, b]
unless
(((u <>--> u <>--> a --> b --> b) ==% ftype) freeVars)
((ftype ==% (u <>--> u <>--> a --> b --> b)) freeVars)
(error "trace must be of type {A : Type} -> {B : Type} -> A -> B -> B")
registerBuiltin BuiltinTrace (f ^. axiomName)
@ -25,6 +25,6 @@ registerFail f = do
let freeVars = HashSet.fromList [a]
string_ <- getBuiltinName (getLoc f) BuiltinString
unless
(((u <>--> string_ --> a) ==% ftype) freeVars)
((ftype ==% (u <>--> string_ --> a)) freeVars)
(error "fail must be of type {A : Type} -> String -> A")
registerBuiltin BuiltinFail (f ^. axiomName)