correct specialisation signature

anoma · Oct 3, 2023 · dd63c7b · dd63c7b
1 parent b70fb05
commit dd63c7b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -109,7 +109,7 @@ data AxiomInfo = AxiomInfo
   }
 
 data SpecialisationInfo = SpecialisationInfo
-  { _specSignature :: [Node],
+  { _specSignature :: ([Node], [Int]),
     _specSymbol :: Symbol
   }
 

diff --git a/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs b/src/Juvix/Compiler/Core/Transformation/Optimize/SpecializeArgs.hs
@@ -98,7 +98,6 @@ convertNode = dmapLRM go
                     filter
                       ( \argNum ->
                           argNum <= argsNum
-                            && argNum <= length args'
                             && isSpecializable tab (args' !! (argNum - 1))
                             && isArgSpecializable tab _identSymbol argNum
                       )
@@ -145,9 +144,13 @@ convertNode = dmapLRM go
                       eassert (length lams == argsNum)
                       eassert (length args' == argsNum)
                       eassert (argsNum <= length tyargs)
-                      let specSig = selectSpecargs specargs args'
+                      -- assumption: all type variables are at the front
+                      eassert (not $ any (isTypeConstr tab) (drop tyargsNum tyargs))
+                      -- the specialisation signature: the values we specialise the arguments by
+                      let specSigArgs = selectSpecargs specargs args'
+                          specSig = (specSigArgs, specargs)
                       if
-                          | all isClosed specSig ->
+                          | all isClosed specSigArgs ->
                               case find ((== specSig) . (^. specSignature)) (lookupSpecialisationInfo tab _identSymbol) of
                                 Just SpecialisationInfo {..} ->
                                   return $