fix order of arguments

anoma · Sep 6, 2024 · 3977c4b · 3977c4b
1 parent 4c7e8a7
commit 3977c4b
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 5 deletions.
diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs
@@ -11,6 +11,7 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Data.TypedInstanceHole
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.SizeRelation
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
 import Juvix.Data.CodeAnn
@@ -64,6 +65,9 @@ instance PrettyCode SimpleLambda where
     v' <- ppCode (l ^. slambdaBinder . sbinderVar)
     return $ kwSimpleLambda <+> braces (v' <+> kwAssign <+> b')
 
+instance PrettyCode SizeRel' where
+  ppCode = return . annotate AnnKeyword . pretty
+
 instance PrettyCode Application where
   ppCode a = do
     l' <- ppLeftExpression appFixity (a ^. appLeft)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -635,7 +635,12 @@ mutualBlockInstanceCallMap stmts = do
 
         addConstraint :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> InstanceApp -> Sem r ()
         addConstraint InstanceInfo {..} InstanceApp {..} = do
-          let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs
+          let c :: FunCall' InstanceParam =
+                mkFunCall
+                  (flip cmpInstanceParam)
+                  _instanceAppHead
+                  _instanceInfoParams
+                  _instanceAppArgs
           addCall _instanceInfoInductive c
 
 checkInstanceTermination ::

diff --git a/...ix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs b/...ix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs
@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Tr
 where
 
 import Juvix.Compiler.Internal.Extra.InstanceInfo
+import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data.SizeRelation
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Options
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
@@ -27,6 +28,7 @@ checkTraitTermination InstanceApp {..} InstanceInfo {..} = do
       unless (any (checkStrictSubterm arg) _instanceInfoParams) $
         throw (ErrTraitNotTerminating (TraitNotTerminating (paramToExpression arg)))
 
+-- | Checks that p1 is a strict subterm of p2
 checkStrictSubterm :: InstanceParam -> InstanceParam -> Bool
 checkStrictSubterm p1 p2 = case p2 of
   InstanceParamApp InstanceApp {..} ->
@@ -41,7 +43,17 @@ checkSubterm :: InstanceParam -> InstanceParam -> Bool
 checkSubterm p1 p2 = p1 == p2 || checkStrictSubterm p1 p2
 
 cmpInstanceParam :: InstanceParam -> InstanceParam -> Maybe SizeRel'
-cmpInstanceParam l r
-  | checkStrictSubterm l r = Just RLe
-  | l == r = Just REq
-  | otherwise = Nothing
+cmpInstanceParam l r =
+  let res
+        | checkStrictSubterm l r = Just RLe
+        | l == r = Just REq
+        | otherwise = Nothing
+   in trace
+        ( "cmp "
+            <> ppTrace l
+            <> " <>? "
+            <> ppTrace r
+            <> " = "
+            <> ppTrace res
+        )
+        res