Restore logging sequence

idris-lang · Oct 31, 2024 · db2677c · db2677c
1 parent 211b9c7
commit db2677c
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 5 deletions.
diff --git a/src/Core/Normalise/Quote.idr b/src/Core/Normalise/Quote.idr
@@ -95,7 +95,8 @@ mutual
                     Env Term free -> SnocList (FC, Closure free) ->
                     Core (SnocList (FC, Term (free ++ bound)))
   quoteArgsWithFC q opts defs bounds env
-      = traverse (quoteArgWithFC q opts defs bounds env)
+      -- [Note] Restore logging sequence
+      = map reverse . traverse (quoteArgWithFC q opts defs bounds env) . reverse
 
   quoteHead : {auto c : Ref Ctxt Defs} ->
               {bound, free : _} ->

diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
@@ -877,7 +877,8 @@ mutual
            let args = if isLin margs' then cast margs else cast margs ++ margs'
            logC "unify.hole" 10
                    (do args' <- traverse (evalArg empty) args
-                       qargs <- traverse (quote empty env) args'
+                       -- [Note] Restore logging sequence
+                       qargs <- map reverse $ traverse (quote empty env) (reverse args')
                        qtm <- quote empty env tmnf
                        pure $ "Unifying: " ++ show !(toFullNames mname) ++ " " ++ show !(traverse toFullNames $ toList qargs) ++
                               " with " ++ show !(toFullNames qtm)) -- first attempt, try 'empty', only try 'defs' when on 'retry'?

diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr
@@ -225,12 +225,14 @@ mutual
   mightMatch defs (NBind _ _ _ _) (NBind _ _ _ _) = pure Poly -- lambdas might match
   mightMatch defs (NTCon _ n t a args) (NTCon _ n' t' a' args')
       = if n == n'
-           then do amatch <- mightMatchArgs defs (map snd args) (map snd args')
+           -- [Note] Restore logging sequence
+           then do amatch <- mightMatchArgs defs (reverse $ map snd args) (reverse $ map snd args')
                    if amatch then pure Concrete else pure NoMatch
            else pure NoMatch
   mightMatch defs (NDCon _ n t a args) (NDCon _ n' t' a' args')
       = if t == t'
-           then do amatch <- mightMatchArgs defs (map snd args) (map snd args')
+           -- [Note] Restore logging sequence
+           then do amatch <- mightMatchArgs defs (reverse $ map snd args) (reverse $ map snd args')
                    if amatch then pure Concrete else pure NoMatch
            else pure NoMatch
   mightMatch defs (NPrimVal _ x) (NPrimVal _ y)

diff --git a/src/TTImp/PartialEval.idr b/src/TTImp/PartialEval.idr
@@ -517,7 +517,9 @@ mutual
                     Env Term free -> SnocList (FC, Closure free) ->
                     Core (SnocList (FC, Term (free ++ bound)))
   quoteArgsWithFC q defs bounds env terms
-      = pure $ zip (map fst terms) !(quoteArgs q defs bounds env (map snd terms))
+           -- [Note] Restore logging sequence
+      = do let rev_terms = reverse terms
+           pure . reverse $ zip (map fst rev_terms) !(quoteArgs q defs bounds env (map snd rev_terms))
 
   quoteHead : {bound, free : _} ->
               {auto c : Ref Ctxt Defs} ->