1
1
mirror of https://github.com/anoma/juvix.git synced 2025-01-05 22:46:08 +03:00

Fix generation of wildcards in RecordPattern (#2802)

- Closes #2801
This commit is contained in:
Jan Mas Rovira 2024-06-04 18:28:25 +02:00 committed by GitHub
parent 371f8f2258
commit 44cdd8404b
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 12 additions and 2 deletions

View File

@ -1251,7 +1251,11 @@ goRecordPattern r = do
mkPatterns :: Sem r [Internal.PatternArg]
mkPatterns = do
sig <- asks (fromJust . HashMap.lookup (constr ^. Internal.nameId) . (^. S.infoConstructorSigs))
sig <-
asks $
fromJust
. HashMap.lookup (constr ^. Internal.nameId)
. (^. S.infoConstructorSigs)
let maxIdx = length (sig ^. recordNames) - 1
args <- IntMap.toAscList <$> byIndex
execOutputList (go maxIdx 0 args)
@ -1265,8 +1269,9 @@ goRecordPattern r = do
output arg'
go maxIdx (idx + 1) args'
| otherwise = do
v <- Internal.freshVar loc ("x" <> show idx)
v <- Internal.freshVar loc ("gen_" <> show idx)
output (Internal.patternArgFromVar Internal.Explicit v)
go maxIdx (idx + 1) args
goAxiom :: (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, Builtins, NameIdGen, Reader S.InfoTable] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef
goAxiom a = do

View File

@ -6,6 +6,11 @@ type Pair (A B : Type) :=
snd : B
};
type T := t;
partialMatch : Pair T T -> T
| mypair@mkPair@{snd := t} := t;
swap {A B : Type} : Pair A B -> Pair B A
| mkPair@{fst := c1; snd := c2} := mkPair c2 c1;