@@ -6,6 +6,7 @@ import Control.Monad.State
66import Debug.Trace
77import qualified Data.Map as Map
88import Data.Char
9+import Data.List
910
1011{- The language has:
1112 * Full dependent types
@@ -405,4 +406,28 @@ weakenEnv env = wk (length env - 1) env
405406weakenTmEnv :: Int -> EnvTT n -> EnvTT n
406407weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
407408
409+orderPats :: Term -> Term
410+orderPats tm = op [] tm
411+ where
412+ op ps (Bind n (PVar t) sc) = op ((n, t) : ps) sc
413+ op ps sc = bindAll (map (\ (n, t) -> (n, PVar t)) (sortP ps)) sc
414+
415+ sortP ps = pick [] (reverse ps)
416+
417+ namesIn (P _ n _) = [n]
418+ namesIn (Bind n b t) = nub $ nb b ++ (namesIn t \\ [n])
419+ where nb (Let t v) = nub (namesIn t) ++ nub (namesIn v)
420+ nb (Guess t v) = nub (namesIn t) ++ nub (namesIn v)
421+ nb t = namesIn (binderTy t)
422+ namesIn (App f a) = nub (namesIn f ++ namesIn a)
423+ namesIn _ = []
424+
425+ pick acc [] = reverse acc
426+ pick acc ((n, t) : ps) = pick (insert n t acc) ps
427+
428+ insert n t [] = [(n, t)]
429+ insert n t ((n',t') : ps)
430+ | n `elem` (namesIn t' ++ concatMap namesIn (map snd ps))
431+ = (n', t') : insert n t ps
432+ | otherwise = (n,t):(n',t'):ps
408433