fix ordering of arguments according to original type constructor

buzden · Jun 18, 2024 · 2098172 · 2098172
1 parent 9ef6e74
commit 2098172
Show file tree

Hide file tree

Showing 15 changed files with 65 additions and 49 deletions.
diff --git a/src/Deriving/DepTyCheck/Util/Fusion.idr b/src/Deriving/DepTyCheck/Util/Fusion.idr
@@ -118,7 +118,7 @@ record FusionDecl where
   splitDef    : Decl
   genFClaim   : Decl
   genRClaim   : Decl
-  genRDef     : Decl
+  genRDef     : Name -> Name -> Name -> Decl
 
 
 prepareConArgs : TTImp -> List TTImp
@@ -146,6 +146,17 @@ genFRhsClaim : Name -> List (Name, TTImp) -> TTImp
 genFRhsClaim n l = var `{Gen} .$ var `{MaybeEmpty} .$ genFDPair n l
 
 
+public export
+buildOrdering : Eq a => List (List a) -> List a
+buildOrdering l = go l [] where
+  go : List (List a) -> List a -> List a
+  go []     res = reverse res
+  go (h::t) res = go t (merge h res) where
+    merge : List a -> List a -> List a
+    merge []     res = res
+    merge (h::t) res = if (elem h res) then merge t res else merge t (h::res)
+
+
 deriveFusion : Vect (2 + n) (TypeInfo, List Name) -> Maybe FusionDecl
 deriveFusion l = do
   let typeNames = toList $ map ((.name) . fst) l
@@ -155,8 +166,8 @@ deriveFusion l = do
   let False = any isNothing typeArgs
     | True => Nothing
 
-  let uniqueArgs = nub $ (sortBy (comparing fst)) $ join $ catMaybes $ toList typeArgs -- arg types from type signature
-  let uniqueNames = nub $ sort $ join $ toList $ map snd l -- names from target type constructor
+  let uniqueNames = buildOrdering $ toList $ map snd l -- names from target type constructor
+  let uniqueArgs = nub $ (sortBy (comparing (\x => findIndex ((==) $ fst x) uniqueNames))) $ join $ catMaybes $ toList typeArgs -- arg types from type signature
 
   let True = length uniqueArgs == length uniqueNames  -- same parameter name could not be associated with different types
     | False => Nothing
@@ -192,7 +203,7 @@ deriveFusion l = do
                   toList (map (toList . (map (nameStr . (.name) . fst))) consComb)
                 else def splitName [impossibleClause (var splitName .$ implicitTrue)]
 
-  let stub = ILog Nothing
+  -- let stub = ILog Nothing
   let genFName = UN $ Basic ("gen" ++ (nameStr fusionTypeName))
   let genFClaim = export' genFName $
                     (MkArg MW ExplicitArg Nothing (var `{Fuel})) .->
@@ -202,18 +213,21 @@ deriveFusion l = do
                     (MkArg MW ExplicitArg Nothing (var `{Fuel})) .->
                     (var `{Gen} .$ var `{MaybeEmpty} .$ var `{Z})
 
+  let lambdaHelpName = "{lamc:0}"
+  let fuelHelpName = "fl"
+
   let fusedVarName = toLower $ nameStr fusionTypeName
   let typeVarNames = map (toLower . nameStr) typeNames
-  let genRDef = def
-                  `{genZ_ultimate} -- to pass a name of constructor
-                  [  var `{genZ_ultimate}
-                  .$ bindVar "fl"
+  let genRDef = \ultimateGenName, fusedGenName, originalConsName => def
+                  ultimateGenName
+                  [  var ultimateGenName
+                  .$ bindVar fuelHelpName
                   .= var `{(>>=)}
-                  .$ (var genFName .$ var `{fl})
+                  .$ (var fusedGenName .$ (var $ UN $ Basic fuelHelpName))
                   .$ (
-                      MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
+                      MkArg MW ExplicitArg (Just lambdaHelpName) implicitFalse
                       `lam` iCase {
-                        sc = var "{lamc:0}", -- to use a var with meaningful name
+                        sc = var lambdaHelpName,
                         ty = implicitFalse,
                         clauses =
                           [ genRMkDPair (bindVar fusedVarName) uniqueNames
@@ -223,7 +237,7 @@ deriveFusion l = do
                               clauses =
                                 [ (splitRhsDef (map bindVar typeVarNames))
                                 .= var `{pure}
-                                .$ foldConstructor (var `{MkZ}) (map var uniqueNames ++ map (var . UN . Basic) typeVarNames)
+                                .$ foldConstructor (var originalConsName) (map var uniqueNames ++ map (var . UN . Basic) typeVarNames)
                                 ]
                             }
                           ]
@@ -234,13 +248,22 @@ deriveFusion l = do
   Just (MkFusionDecl dataDecl claimDecl defDecl genFClaim genRClaim genRDef)
 
 
-declareFusion : Vect (2 + n) (TypeInfo, List Name) -> Elab (Maybe FusionDecl)
-declareFusion l = do
-  let derived = deriveFusion l
-  case derived of
-    Just fd => declare [fd.dataType, fd.splitClaim, fd.splitDef, fd.genFClaim, fd.genRClaim, fd.genRDef]
-    Nothing => declare []
-  pure $ derived
+-- checkDeclared : Elaboration m => List Decl -> m (List Decl)
+-- checkDeclared [] = pure []
+-- checkDeclared (x::xs) = do
+--   tail <- checkDeclared xs
+--   head <- case x of
+--     IClaim _ _ _ _ (MkTy _ _ n _) => getInfo' n
+--     IData _ _ _ (MkData _ n _ _ _) => getInfo' n
+--     IDef _ n _ => getInfo' n
+--     -- _ => pure []
+--   if null head then pure (x::tail) else pure tail
+
+
+-- declareFusion : Elaboration m => List Decl -> m ()
+-- declareFusion l = do
+--   notDeclaredYet <- checkDeclared l
+--   declare notDeclaredYet
 
 
 prepareArgsSolve : Arg -> (Name, List String)
@@ -271,14 +294,14 @@ runFusion x xArgs y yArgs = do
   xTI <- getInfo' x
   yTI <- getInfo' y
   let zipped = (xTI, xArgs) :: (yTI, yArgs) :: Nil
-  declareFusion zipped
+  pure $ deriveFusion zipped
 
 
 public export
 runFusionList : Vect (2 + n) (Name, List Name) -> Elab (Maybe FusionDecl)
 runFusionList l = do
   l' <- for l $ \(n, args) => (, args) <$> getInfo' n
-  declareFusion l'
+  pure $ deriveFusion l'
 
 
 public export
@@ -294,17 +317,14 @@ getSplit (Just fd) = [fd.splitClaim, fd.splitDef]
 
 
 public export
-getGen : Maybe FusionDecl -> List Decl
-getGen Nothing = []
-getGen (Just fd) = [fd.genFClaim, fd.genRClaim, fd.genRDef]
+getGen : Maybe FusionDecl -> Name -> Name -> Name -> List Decl
+getGen Nothing _ _ _ = []
+getGen (Just fd) n1 n2 n3 = [fd.genFClaim, fd.genRClaim, fd.genRDef n1 n2 n3]
 
 
 -- TODO: what happens with :doc
--- tests for order of dependent arguments
--- TODO: preserve order of args from left to right !!! IMPORTANT
 -- solveDeps should be compatible with fuse (not to group what couldn't be fused)
 -- TODO: declare fused type iff it does not exist (otherwise reuse)
 -- TODO: highlevel name conventions resolving (pure)
 -- TODO: remove declare stage from print tests (declare should be highlevel)
--- TODO: update to last compiler version and merge main
 -- TODO: GenSignature -> Con -> genZ_ultimate(?)
diff --git a/tests/derivation/utils/fusion/print/generator/001 one var match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/001 one var match/DerivedGen.idr
@@ -20,4 +20,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/002 two var ordered match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/002 two var ordered match/DerivedGen.idr
@@ -22,5 +22,5 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{m}, `{n}] `{Y} [`{m}, `{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
 
diff --git a/tests/derivation/utils/fusion/print/generator/003 two var unordered match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/003 two var unordered match/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{m}, `{n}] `{Y} [`{n}, `{m}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/004 var-const match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/004 var-const match/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/005 const-const match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/005 const-const match/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/006 const-const no match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/006 const-const no match/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/007 prim-prim match/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/007 prim-prim match/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{n}] `{Y} [`{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/008 non-shared var/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/008 non-shared var/DerivedGen.idr
@@ -21,4 +21,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusion `{X} [`{k}, `{m}] `{Y} [`{m}, `{n}]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXY} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/009 three types fusion/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/009 three types fusion/DerivedGen.idr
@@ -24,4 +24,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusionList [(`{X}, [`{n}]), (`{Y}, [`{n}]), (`{W}, [`{n}])]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXYW} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/generator/010 three types two args/DerivedGen.idr b/tests/derivation/utils/fusion/print/generator/010 three types two args/DerivedGen.idr
@@ -23,4 +23,4 @@ decl : Maybe FusionDecl
 decl = %runElab runFusionList [(`{X}, [`{k}, `{m}]), (`{Y}, [`{m}, `{n}]), (`{W}, [`{n}, `{k}])]
 
 main : IO ()
-main = putPretty $ getGen decl
+main = putPretty $ getGen decl `{genZ_ultimate} `{genXYW} `{MkZ}
diff --git a/tests/derivation/utils/fusion/print/merger/008 non-shared var/expected b/tests/derivation/utils/fusion/print/merger/008 non-shared var/expected
@@ -7,14 +7,14 @@
        emptyFC
        "XY"
        (Just
-          (    MkArg MW ExplicitArg (Just "k") type
-           .-> MkArg MW ExplicitArg (Just "m") type
+          (    MkArg MW ExplicitArg (Just "m") type
            .-> MkArg MW ExplicitArg (Just "n") type
+           .-> MkArg MW ExplicitArg (Just "k") type
            .-> type))
        []
        [ mkTy
            { name = "MkX_MkY"
-           , type = var "XY" .$ bindVar "k" .$ bindVar "m" .$ bindVar "n"
+           , type = var "XY" .$ bindVar "m" .$ bindVar "n" .$ bindVar "k"
            }
        ])
 ]
diff --git a/tests/derivation/utils/fusion/print/merger/010 three types two args/expected b/tests/derivation/utils/fusion/print/merger/010 three types two args/expected
@@ -7,14 +7,10 @@
        emptyFC
        "XYZ"
        (Just
-          (    MkArg MW ExplicitArg (Just "k") type
+          (    MkArg MW ExplicitArg (Just "n") type
            .-> MkArg MW ExplicitArg (Just "m") type
-           .-> MkArg MW ExplicitArg (Just "n") type
+           .-> MkArg MW ExplicitArg (Just "k") type
            .-> type))
        []
-       [ mkTy
-           { name = "MkX_MkY_MkZ"
-           , type = var "XYZ" .$ bindVar "k" .$ bindVar "m" .$ bindVar "n"
-           }
-       ])
+       [mkTy {name = "MkX_MkY_MkZ", type = var "XYZ" .$ bindVar "k"}])
 ]
diff --git a/tests/derivation/utils/fusion/print/splitter/008 non-shared var/expected b/tests/derivation/utils/fusion/print/splitter/008 non-shared var/expected
@@ -11,7 +11,7 @@
                  MW
                  ExplicitArg
                  Nothing
-                 (var "XY" .$ bindVar "k" .$ bindVar "m" .$ bindVar "n")
+                 (var "XY" .$ bindVar "m" .$ bindVar "n" .$ bindVar "k")
            .->    var "Builtin.Pair"
                .$ (var "X" .$ bindVar "m" .$ bindVar "n")
                .$ (var "Y" .$ bindVar "n" .$ bindVar "k")

diff --git a/tests/derivation/utils/fusion/print/splitter/010 three types two args/expected b/tests/derivation/utils/fusion/print/splitter/010 three types two args/expected
@@ -11,7 +11,7 @@
                  MW
                  ExplicitArg
                  Nothing
-                 (var "XYZ" .$ bindVar "k" .$ bindVar "m" .$ bindVar "n")
+                 (var "XYZ" .$ bindVar "n" .$ bindVar "m" .$ bindVar "k")
            .->    var "Builtin.Pair"
                .$ (var "X" .$ bindVar "n" .$ bindVar "m")
                .$ (   var "Builtin.Pair"