wip cli

anoma · Sep 5, 2024 · c8b8c2c · c8b8c2c
1 parent 83dba28
commit c8b8c2c
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 22 deletions.
diff --git a/app/Commands/Dev/InstanceTermination/Options.hs b/app/Commands/Dev/InstanceTermination/Options.hs
@@ -26,4 +26,4 @@ parseInstanceTerminationCommand =
         minfo =
           info
             (Calls <$> parseCalls)
-            (progDesc "Compute the calls table of a .juvix file")
+            (progDesc "Compute the instance constraints table of a .juvix file")
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -591,9 +591,22 @@ checkResolveInstanceHoles ::
   Sem r (NonEmpty MutualStatement)
 checkResolveInstanceHoles s = do
   (holes, stmts :: NonEmpty MutualStatement) <- runOutputList s
-  infos <- mapM getInstanceInfo (stmts ^.. each . _StatementFunction . filtered isInstance)
-  checkInstanceTermination infos
+  checkInstanceTermination (MutualBlock stmts)
   resolveInstanceHoles holes stmts
+
+mutualBlockInstanceCallMap ::
+  ( Members
+      '[ Reader InfoTable,
+         Error TypeCheckerError,
+         Inference
+       ]
+      r
+  ) =>
+  MutualBlock ->
+  Sem r ([InstanceInfo], CallMap' InstanceParam)
+mutualBlockInstanceCallMap stmts = do
+  instances <- mapM getInstanceInfo (stmts ^.. mutualStatements . each . _StatementFunction . filtered isInstance)
+  (instances,) . mkInstanceCallMap <$> mapWithM checkInstanceConstraints instances
   where
     isInstance :: FunctionDef -> Bool
     isInstance f = case f ^. funDefIsInstanceCoercion of
@@ -602,19 +615,30 @@ checkResolveInstanceHoles s = do
         IsInstanceCoercionInstance -> True
         IsInstanceCoercionCoercion -> False
 
--- {Show a} : Show (List a)
+    mkInstanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam
+    mkInstanceCallMap l = run (execCallMapBuilder (forM l (uncurry addInstance)))
+      where
+        addInstance :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> [InstanceApp] -> Sem r ()
+        addInstance i = mapM_ (addConstraint i)
+
+        addConstraint :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> InstanceApp -> Sem r ()
+        addConstraint InstanceInfo {..} InstanceApp {..} = do
+          let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs
+          addCall _instanceInfoInductive c
+
 checkInstanceTermination ::
   ( Members
       '[ Reader InfoTable,
-         Error TypeCheckerError
+         Error TypeCheckerError,
+         Inference
        ]
       r
   ) =>
-  [InstanceInfo] ->
+  MutualBlock ->
   Sem r ()
-checkInstanceTermination instances = do
+checkInstanceTermination stmts = do
   -- TODO remove later calls to checkInstanceConstraints
-  cm :: CallMap' InstanceParam <- mkInstanceCallMap <$> mapWithM checkInstanceConstraints instances
+  (instances, cm :: CallMap' InstanceParam) <- mutualBlockInstanceCallMap stmts
   forM_ (mapWith findOrder (callMapRecursiveBehaviour cm)) $ \(recBehav, morder) -> case morder of
     Just {} -> return ()
     Nothing ->
@@ -623,17 +647,6 @@ checkInstanceTermination instances = do
           TraitNotTerminatingNew
             { _traitNotTerminatingNew = nonEmpty' [i | i <- instances, i ^. instanceInfoInductive == recBehav ^. recursiveBehaviourFun]
             }
-  where
-    mkInstanceCallMap :: [(InstanceInfo, [InstanceApp])] -> CallMap' InstanceParam
-    mkInstanceCallMap l = run (execCallMapBuilder (forM l (uncurry addInstance)))
-      where
-        addInstance :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> [InstanceApp] -> Sem r ()
-        addInstance i = mapM_ (addConstraint i)
-
-        addConstraint :: (Members '[CallMapBuilder' InstanceParam] r) => InstanceInfo -> InstanceApp -> Sem r ()
-        addConstraint InstanceInfo {..} InstanceApp {..} = do
-          let c :: FunCall' InstanceParam = mkFunCall cmpInstanceParam _instanceAppHead _instanceInfoParams _instanceAppArgs
-          addCall _instanceInfoInductive c
 
 resolveInstanceHoles ::
   forall a r.

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -513,16 +513,16 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
 
 runInferenceDefs ::
   (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) =>
-  Sem (Inference ': r) (NonEmpty funDef) ->
-  Sem r (NonEmpty funDef)
+  Sem (Inference ': r) funDef ->
+  Sem r funDef
 runInferenceDefs a = do
   (finalState, expr) <- runInferenceState iniState a
   (subs, idens) <- closeState finalState
   idens' <- mapM (subsHoles subs) (idens ^. typesTable)
   stash' <- mapM (subsHoles subs) (finalState ^. inferenceFunctionsStash)
   forM_ stash' registerFunctionDef
   addIdenTypes (TypesTable idens')
-  mapM (subsHoles subs) expr
+  subsHoles subs expr
 
 runInferenceDef ::
   (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) =>