[termination] implement lexical order search

app/Main.hs

@@ -278,8 +278,18 @@ go c = do
       let callMap = T.buildCallMap a
           opts' = A.defaultOptions
           completeGraph = T.completeCallGraph callMap
+          recBehav = map T.recursiveBehaviour (T.reflexiveEdges completeGraph)
       A.printPrettyCode opts' completeGraph
       putStrLn ""
+      forM_ recBehav $ \r -> do
+        -- M.printPrettyCodeDefault (r ^. T.recBehaviourFunction)
+        A.printPrettyCode A.defaultOptions r
+        putStrLn ""
+        case T.findOrder r of
+          Nothing -> putStrLn " Fails the termination checking"
+          Just (T.LexicoOrder k) -> putStrLn (" Terminates with order " <> show k)
+        putStrLn ""
+
 
 
 main :: IO ()

src/MiniJuvix/Termination/CallGraph.hs

@@ -74,3 +74,67 @@ completeCallGraph cm = CompleteCallGraph (go startingEdges)
   edgesUnion = HashMap.union
   edgesCount :: Edges -> Int
   edgesCount = HashMap.size
+
+reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
+reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
+  where
+  reflexive :: Edge -> Maybe ReflexiveEdge
+  reflexive e
+   | e ^. edgeFrom == e ^. edgeTo = Just $ ReflexiveEdge (e ^.edgeFrom) (e ^. edgeMatrices)
+   | otherwise = Nothing
+
+callMatrixDiag :: CallMatrix -> [Rel]
+callMatrixDiag m = [ col i r | (i, r) <- zip [0 :: Int ..] m]
+  where
+  col i (CallRow row) = case row of
+    Nothing -> RNothing
+    Just (j, r')
+      | i == j -> RJust r'
+      | otherwise -> RJust r'
+
+recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
+recursiveBehaviour re =
+  RecursiveBehaviour (re ^. redgeFun)
+  (map callMatrixDiag (re ^. redgeMatrices))
+
+findOrder :: RecursiveBehaviour -> Maybe LexicoOrder
+findOrder rb
+  | null b0 = impossible
+  | otherwise = LexicoOrder <$> listToMaybe (mapMaybe isLexicoOrder allPerms)
+  where
+  isLexicoOrder :: [Int] -> Maybe [Int]
+  isLexicoOrder = go startB
+    where
+    go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
+    go [] _ = Just []
+    go b perm = case perm of
+      [] -> Nothing
+      (p0 : ptail)
+        | Just r <- find (isLess . snd . (!! p0)) b,
+          all (notNothing . snd . (!! p0)) b,
+          Just perm' <- go (b' p0) (map pred ptail)
+          -> Just (fst (r !! p0) : perm')
+        | otherwise -> Nothing
+      where
+      b' i = map r' (filter (not . isLess . snd . (!!i)) b)
+        where
+        r' r = case splitAt i r of
+          (x, y) -> x ++ drop 1 y
+  notNothing r = case r of
+    RNothing -> False
+    _ -> True
+  isLess = (RJust RLe ==)
+  b0 = rb ^. recBehaviourMatrix
+  allPerms = case nonEmpty startB of
+    -- Nothing -> []
+    Nothing -> impossible -- temporary
+    Just s -> permutations [0 .. length (head s) - 1]
+  indexed = map (zip [0 :: Int ..] . take minLength) b0
+    where
+    minLength =  minimum (map length b0)
+  -- | removes columns that don't have at least one ≺ in them
+  removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
+  -- TODO fix.
+  -- removeUselessColumns = transpose . filter (any (isLess . snd) ) . transpose
+  removeUselessColumns = id
+  startB = removeUselessColumns indexed

src/MiniJuvix/Termination/Types.hs

@@ -7,7 +7,7 @@ module MiniJuvix.Termination.Types (
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language as A
 import qualified Data.HashMap.Strict as HashMap
-import Prettyprinter
+import Prettyprinter as PP
 import MiniJuvix.Termination.Types.SizeRelation
 import MiniJuvix.Syntax.Abstract.Pretty.Base
 
@@ -42,13 +42,23 @@ data Edge = Edge {
 newtype CompleteCallGraph = CompleteCallGraph Edges
 
 data ReflexiveEdge = ReflexiveEdge {
-  _redgeMatrix :: CallMatrix,
-  _redgeFun :: A.FunctionName
+  _redgeFun :: A.FunctionName,
+  _redgeMatrices :: [CallMatrix]
   }
 
+data RecursiveBehaviour = RecursiveBehaviour
+  {
+    _recBehaviourFunction :: A.FunctionName,
+    _recBehaviourMatrix :: [[Rel]]
+  }
+
+newtype LexicoOrder = LexicoOrder [Int]
+
 makeLenses ''FunCall
 makeLenses ''Edge
 makeLenses ''CallMap
+makeLenses ''RecursiveBehaviour
+makeLenses ''ReflexiveEdge
 
 instance PrettyCode FunCall where
   ppCode :: forall r. Members '[Reader Options] r => FunCall -> Sem r (Doc Ann)
@@ -123,3 +133,11 @@ instance PrettyCode CompleteCallGraph where
   ppCode (CompleteCallGraph edges) = do
     es <- vsep2 <$> mapM ppCode (toList edges)
     return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
+
+instance PrettyCode RecursiveBehaviour where
+  ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
+  ppCode (RecursiveBehaviour f m) = do
+    f' <- ppSCode f
+    let m' = vsep (map (PP.list . map pretty) m)
+    return $ pretty ("Recursive behaviour of " :: Text)  <> f' <> colon <> line
+      <> indent 2 (align m')

src/MiniJuvix/Termination/Types/SizeRelation.hs

@@ -7,10 +7,12 @@ import Prettyprinter
 data Rel =
   RJust Rel'
   | RNothing
+  deriving stock (Eq, Show)
 
 data Rel' =
   REq
   | RLe
+  deriving stock (Eq, Show)
 
 toRel :: Rel' -> Rel
 toRel = RJust

tests/positive/Termination/Data/List.mjuvix

@@ -49,11 +49,11 @@ take : (a : Type) → ℕ → List a → List a;
 take a (suc n) (∷ _ x xs) ≔ ∷ a x (take a n xs);
 take a _ _ ≔ nil a;
 
-import Data.Ord;
-open Data.Ord;
+-- import Data.Ord;
+-- open Data.Ord;
 
-import Data.Product;
-open Data.Product;
+-- import Data.Product;
+-- open Data.Product;
 
 -- splitAt : (a : Type) → ℕ → List a → List a;
 -- splitAt a _ (nil _) ≔ nil a , nil a;