From 6621bf0a1ed844db5a520ed66591024ae631a7de Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 4 Jun 2024 16:35:11 +0200 Subject: [PATCH 1/2] fix generation of wildcards in RecordPattern --- src/Juvix/Compiler/Internal/Translation/FromConcrete.hs | 7 ++++++- tests/positive/RecordPattern.juvix | 5 +++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index eba5104bb8..5346abaa48 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -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) @@ -1267,6 +1271,7 @@ goRecordPattern r = do | otherwise = do v <- Internal.freshVar loc ("x" <> 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 diff --git a/tests/positive/RecordPattern.juvix b/tests/positive/RecordPattern.juvix index c23fd0be16..324b0e8795 100644 --- a/tests/positive/RecordPattern.juvix +++ b/tests/positive/RecordPattern.juvix @@ -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; From b98ab4ee9771300f8852f7d3f2e363f0c55c2a18 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 4 Jun 2024 16:38:43 +0200 Subject: [PATCH 2/2] change var name --- src/Juvix/Compiler/Internal/Translation/FromConcrete.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 5346abaa48..ad84213f96 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -1269,7 +1269,7 @@ 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