X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=8ee03d8474fea93f88a157916399c13d9f993a1d;hp=3dec80feda126a9b9ff5217689b037de9d275477;hb=7b4102f909b03506dc1d7a30d3bd0dc057439b98;hpb=f7a6e08c97cae1c1b278c18a1904eadec4e5f010 diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 3dec80f..8ee03d8 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -47,8 +47,13 @@ getTyConTyVars tc = then [] else TyCon.tyConTyVars tc +cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering +cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT +cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT +cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1 + sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x +sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x -- to do: this could be moved into Coq coreVarToWeakVar :: Var.Var -> WeakVar