fix order of arguments

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

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
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
@@ -27,6 +27,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 {..} ->