X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=224d70b54f624160c7013dfd97a1638a51a3d9bf;hp=2ee78b2223952536632ce1ce45f8db96e9bba0da;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=b096aab78240e38ff69c120367e65be60cbc54f5

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 2ee78b2..224d70b 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -21,7 +21,6 @@ Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Const
 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
-(* TODO: might be a better idea to panic here than simply drop things that look wrong *)
 Definition dataConExTyVars cdc :=
   filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
   Opaque dataConExTyVars.
@@ -79,27 +78,25 @@ Section Raw.
   Inductive RawCoercionKind : Type :=
     mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
 
-  Section CV.
-
-    (* the PHOAS type which stands for coercion variables of System FC *)
-    
-
-    (* Figure 7: γ, δ *)
-    Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
-(*
-    | CoVar          : CV                                           -> RawHaskCoer (* g      *)
-    | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
-    | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
-    | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
-    | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
-    | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
-    | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
-    | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
-    | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
-    | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
-    | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
-*)
-  End CV.
+  (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
+  Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
+  (*  
+   *  This has been disabled until we manage to reconcile SystemFC's
+   *  coercions with what GHC actually implements (they are not the
+   *  same!)
+   *  
+  | CoVar          : CV                                           -> RawHaskCoer (* g      *)
+  | CoType         : RawHaskType                                  -> RawHaskCoer (* τ      *)
+  | CoApp          : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* γ γ    *)
+  | CoAppT         : RawHaskCoer -> RawHaskType                   -> RawHaskCoer (* γ@v    *)
+  | CoCFApp        : ∀ n, CoFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* C   γⁿ *)
+  | CoTFApp        : ∀ n, TyFunConst n -> vec RawHaskCoer n       -> RawHaskCoer (* S_n γⁿ *)
+  | CoAll          : Kind  -> (TV -> RawHaskCoer)                 -> RawHaskCoer (* ∀a:κ.γ *)
+  | CoSym          : RawHaskCoer                                  -> RawHaskCoer (* sym    *)
+  | CoComp         : RawHaskCoer -> RawHaskCoer                   -> RawHaskCoer (* ◯      *)
+  | CoLeft         : RawHaskCoer                                  -> RawHaskCoer (* left   *)
+  | CoRight        : RawHaskCoer                                  -> RawHaskCoer (* right  *).
+  *)
 End Raw.
 
 Implicit Arguments TCon   [ [TV] ].
@@ -294,13 +291,6 @@ Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ
   apply weakCK.
   apply IHκ.
   Defined.
-(*
-Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
-  match κ as K return list (HaskCoercionKind (app K Γ)) with
-  | nil => hck
-  | _   => map weakCK' hck
-  end.
-*)
 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
   map weakCK' hck.
 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
@@ -309,10 +299,6 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T
   forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
   := fun TV ite tv => (f TV (weakITE ite) tv).
 
-(* I keep mixing up left/right folds *)
-(* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
-(*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
-
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->
   HaskType Γ (fold_right KindArrow ★ lk) ->
@@ -492,7 +478,9 @@ end.
 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
   compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
 
-(* This is not provable in Coq's logic because the Coq function space
+(* The PHOAS axioms
+ * 
+ * This is not provable in Coq's logic because the Coq function space
  * is "too big" - although its only definable inhabitants are Coq
  * functions, it is not provable in Coq that all function space
  * inhabitants are definable (i.e. there are no "exotic" inhabitants).