From: Adam Megacz Date: Mon, 28 Mar 2011 00:20:22 +0000 (-0700) Subject: Merge branch 'master' of http://git.megacz.com/coq-hetmet X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=ddac2a6a7301788326cd9107965e59fc0804daad;hp=e2be3300379a5c0e1397c33f7b983a5259c5f51b Merge branch 'master' of git.megacz.com/coq-hetmet Conflicts: src/Extraction-prefix.hs --- diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 56322c9..fbe22cb 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -35,13 +35,6 @@ import qualified GHC.Base import qualified System.IO import qualified System.IO.Unsafe -{- -- used for extracting strings WITHOUT the patch for Coq -bin2ascii = - (\ b0 b1 b2 b3 b4 b5 b6 b7 -> - let f b i = if b then 1 `shiftL` i else 0 - in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) --} - getTyConTyVars :: TyCon.TyCon -> [Var.TyVar] getTyConTyVars tc = if TyCon.isFunTyCon tc @@ -58,7 +51,6 @@ 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 (\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 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) @@ -85,7 +77,6 @@ nat2int (S x) = 1 + (nat2int x) natToString :: Nat -> Prelude.String natToString n = show (nat2int n) --- only needs to sanitize characters which might appear in Haskell identifiers sanitizeForLatex :: Prelude.String -> Prelude.String sanitizeForLatex [] = [] sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x) @@ -108,10 +99,15 @@ coreKindToKind k = else if (Coercion.isArgTypeKind k) then KindStar else if (Coercion.isUbxTupleKind k) then KindStar else if (Coercion.isOpenTypeKind k) then KindStar +-- +-- The "subkinding" in GHC is not dealt with in System FC, and dealing +-- with it is not actually as simple as you'd think. +-- -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType -- else if (Coercion.isOpenTypeKind k) then KindOpenType -- else if (Coercion.isArgTypeKind k) then KindArgType -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple +-- else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " @@ -119,10 +115,6 @@ coreKindToKind k = outputableToString :: Outputable.Outputable a => a -> Prelude.String outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) --- I'm leaving this here (commented out) in case I ever need it again) ---checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool ---checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) - coreViewDeep :: Type.Type -> Type.Type coreViewDeep t = case t of @@ -197,3 +189,14 @@ trace msg x = System.IO.Unsafe.unsafePerformIO $ trace msg x = System.IO.Unsafe.unsafePerformIO $ (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x) -} + +{- -- used for extracting strings WITHOUT the patch for Coq +bin2ascii = + (\ b0 b1 b2 b3 b4 b5 b6 b7 -> + let f b i = if b then 1 `shiftL` i else 0 + in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) +-} + +-- I'm leaving this here (commented out) in case I ever need it again) +--checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool +--checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index dbeb3cc..2f0856f 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -62,7 +62,7 @@ Extract Inlined Constant string_dec => "(==)". Extract Inlined Constant ascii_dec => "(==)". (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". +Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq". Extract Constant zero => "'\000'". Extract Constant one => "'\001'". Extract Constant shift => "shiftAscii". diff --git a/src/PreCategory.v b/src/PreCategory.v deleted file mode 100644 index 7418261..0000000 --- a/src/PreCategory.v +++ /dev/null @@ -1,93 +0,0 @@ -(*********************************************************************************************************************************) -(* SemiCategory: *) -(* *) -(* Same as a category, but without identity maps. See *) -(* *) -(* http://ncatlab.org/nlab/show/semicategory *) -(* *) -(*********************************************************************************************************************************) - -Generalizable All Variables. -Require Import Preamble. -Require Import General. - -Class SemiCategory (Ob:Type)(Hom:Ob->Ob->Type) := -{ semi_hom := Hom -; semi_ob := Ob -; semi_comp : forall {a}{b}{c}, Hom a b -> Hom b c -> Hom a c -; semi_eqv : forall a b, (Hom a b) -> (Hom a b) -> Prop -; semi_eqv_equivalence : forall a b, Equivalence (semi_eqv a b) -; semi_comp_respects : forall a b c, Proper (semi_eqv a b ==> semi_eqv b c ==> semi_eqv a c) (@semi_comp _ _ _) -; semi_associativity : - forall `(f:Hom a b)`(g:Hom b c)`(h:Hom c d), semi_eqv _ _ (semi_comp (semi_comp f g) h) (semi_comp f (semi_comp g h)) -}. -Coercion semi_ob : SemiCategory >-> Sortclass. - -Notation "a ~-> b" := (@semi_hom _ _ _ a b) (at level 70). -Notation "f ~-~ g" := (@semi_eqv _ _ _ _ _ f g) (at level 54). -Notation "f >>->> g" := (@semi_comp _ _ _ _ _ _ f g) (at level 45). - -Add Parametric Relation (Ob:Type)(Hom:Ob->Ob->Type)(C:SemiCategory Ob Hom)(a b:Ob) : (semi_hom a b) (semi_eqv a b) - reflexivity proved by (@Equivalence_Reflexive _ _ (semi_eqv_equivalence a b)) - symmetry proved by (@Equivalence_Symmetric _ _ (semi_eqv_equivalence a b)) - transitivity proved by (@Equivalence_Transitive _ _ (semi_eqv_equivalence a b)) - as parametric_relation_semi_eqv. - Add Parametric Morphism `(c:SemiCategory Ob Hom)(a b c:Ob) : (@semi_comp _ _ _ a b c) - with signature (semi_eqv _ _ ==> semi_eqv _ _ ==> semi_eqv _ _) as parametric_morphism_semi_comp. - intros. - apply semi_comp_respects; auto. - Defined. - -Class SemiFunctor -`( c1 : SemiCategory ) -`( c2 : SemiCategory ) -( fobj : c1 -> c2 ) := -{ semifunctor_fobj := fobj -; semi_fmor : forall {a b}, (a~->b) -> (fobj a)~->(fobj b) -; semi_fmor_respects : forall a b (f f':a~->b), (f ~-~ f') -> (semi_fmor f ~-~ semi_fmor f') -; semi_fmor_preserves_comp : forall `(f:a~->b)`(g:b~->c), (semi_fmor f) >>->> (semi_fmor g) ~-~ semi_fmor (f >>->> g) -}. -Implicit Arguments semi_fmor [[Ob][Hom][c1][Ob0][Hom0][c2][fobj][a][b]]. - - (* register "fmor" so we can rewrite through it *) - Implicit Arguments semi_fmor [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ]. - Implicit Arguments semi_fmor_respects [ Ob Hom Ob0 Hom0 c1 c2 fobj a b ]. - Implicit Arguments semi_fmor_preserves_comp [ Ob Hom Ob0 Hom0 c1 c2 fobj a b c ]. - Notation "F \- f" := (semi_fmor F f) (at level 20) : category_scope. - Add Parametric Morphism `(C1:SemiCategory)`(C2:SemiCategory) - (Fobj:C1->C2) - (F:SemiFunctor C1 C2 Fobj) - (a b:C1) - : (@semi_fmor _ _ C1 _ _ C2 Fobj F a b) - with signature ((@semi_eqv C1 _ C1 a b) ==> (@semi_eqv C2 _ C2 (Fobj a) (Fobj b))) as parametric_morphism_semi_fmor'. - intros; apply (@semi_fmor_respects _ _ C1 _ _ C2 Fobj F a b x y); auto. - Defined. - Coercion semifunctor_fobj : SemiFunctor >-> Funclass. - -Definition semifunctor_comp - `(C1:SemiCategory) - `(C2:SemiCategory) - `(C3:SemiCategory) - `(F:@SemiFunctor _ _ C1 _ _ C2 Fobj)`(G:@SemiFunctor _ _ C2 _ _ C3 Gobj) : SemiFunctor C1 C3 (Gobj ○ Fobj). - intros. apply (Build_SemiFunctor _ _ _ _ _ _ _ (fun a b m => semi_fmor G (semi_fmor F m))). - intros. - setoid_rewrite H. - reflexivity. - intros. - setoid_rewrite semi_fmor_preserves_comp; auto. - setoid_rewrite semi_fmor_preserves_comp; auto. - reflexivity. - Defined. -Notation "f >>>–>>> g" := (@semifunctor_comp _ _ _ _ _ _ _ _ _ _ f _ g) (at level 20) : category_scope. - -Class IsomorphicSemiCategories `(C:SemiCategory)`(D:SemiCategory) := -{ isc_f_obj : C -> D -; isc_g_obj : D -> C -; isc_f : SemiFunctor C D isc_f_obj -; isc_g : SemiFunctor D C isc_g_obj -; isc_forward : forall a b (f:a~->b), semi_fmor isc_f (semi_fmor isc_g f) ~-~ f -}. -; isc_backward : isc_g >>>> isc_f ~~~~ functor_id D -}. - -