X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;h=8ee03d8474fea93f88a157916399c13d9f993a1d;hp=b144116e884a58a096e1ab3412690278853d171f;hb=7b4102f909b03506dc1d7a30d3bd0dc057439b98;hpb=c9a110c17f24f89f0375c3207b7c544e87a3cee8

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index b144116..8ee03d8 100644
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -1,11 +1,14 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 where
+import qualified Unique
+import qualified UniqSupply
 import qualified MkCore
 import qualified TysWiredIn
 import qualified TysPrim
 import qualified Outputable
 import qualified PrelNames
+import qualified OccName
 import qualified Name
 import qualified Literal
 import qualified Type
@@ -44,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
@@ -82,6 +90,11 @@ sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
 
+kindToCoreKind :: Kind -> TypeRep.Kind
+kindToCoreKind KindStar          = TypeRep.liftedTypeKind
+kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
+kindToCoreKind _                 = Prelude.error "kindToCoreKind does not know how to handle that"
+
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
   case Coercion.splitKindFunTy_maybe k of