import Data.Bits ((.&.), shiftL, (.|.))
import Prelude ( (++), (+), (==), Show, show, Char )
-{-
+dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc)
+
nat2int :: Nat -> Prelude.Int
nat2int O = 0
nat2int (S x) = 1 + (nat2int x)
outputableToString :: Outputable -> String
outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
--}
+
Class EqDecidable (T:Type) :=
{ eqd_type := T
; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
-; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _))
}.
Coercion eqd_type : EqDecidable >-> Sortclass.
(* extracts the Name from a CoreVar *)
Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
-Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
- Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
-
Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *)
Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ].
Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ].
(* the magic wired-in name for the modal type elimination form *)
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
-(* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
- | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
- => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None
- | _ => None
-end.
-Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar :=
-match ce with
- | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
- => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None
- | _ => None
-end.
-
Generalizable All Variables.
Require Import Preamble.
Require Import General.
+Require Import Coq.Lists.List.
Require Import HaskGeneral.
Require Import HaskLiterals.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
+Require Import HaskWeakVars.
Require Import HaskWeak.
+Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar".
+
+(* detects our crude Core-encoding of modal type introduction/elimination forms *)
+Definition isBrak (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
+ match coreVarToWeakVar v with
+ | WExprVar _ => None
+ | WTypeVar tv => Some tv
+ | WCoerVar _ => None
+ end else None
+ | _ => None
+end.
+Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
+ match coreVarToWeakVar v with
+ | WExprVar _ => None
+ | WTypeVar tv => Some tv
+ | WCoerVar _ => None
+ end else None
+ | _ => None
+end.
+
+Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
+ let (t1,t2) := coreCoercionKind cc
+ in weakCoercion t1 t2 cc.
+
Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
match ce with
| CoreELit lit => OK (WELit lit)
| CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
| CoreEType t => Error "encountered CoreEType in a position where an Expr should have been"
- | CoreECast e co => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co)
+ | CoreECast e co => coreExprToWeakExpr e >>= fun e' =>
+ OK (WECast e' (coreCoercionToWeakCoercion co))
- | CoreEVar v => match coreVarSort v with
- | CoreExprVar _ => OK (WEVar v)
- | CoreTypeVar _ => Error "found a type variable inside an EVar!"
- | CoreCoerVar _ => Error "found a coercion variable inside an EVar!"
+ | CoreEVar v => match coreVarToWeakVar v with
+ | WExprVar ev => OK (WEVar ev)
+ | WTypeVar _ => Error "found a type variable inside an EVar!"
+ | WCoerVar _ => Error "found a coercion variable inside an EVar!"
end
| CoreEApp e1 e2 => match isBrak e1 with
end
end
- | CoreELam v e => match coreVarSort v with
- | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam v e')
- | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e')
- | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e')
+ | CoreELam v e => match coreVarToWeakVar v with
+ | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e')
+ | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
+ | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
end
- | CoreELet (CoreNonRec v ve) e => match coreVarSort v with
- | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' =>
- coreExprToWeakExpr e >>= fun e' => OK (WELet v ve' e')
- | CoreTypeVar _ => match e with
+ | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with
+ | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
+ coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e')
+ | WTypeVar _ => match e with
| CoreEType t => Error "saw a type-let"
| _ => Error "saw (ELet <tyvar> e) where e!=EType"
end
- | CoreCoerVar _ => Error "saw an (ELet <coercionVar>)"
+ | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
end
| CoreELet (CoreRec rb) e =>
- ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) :=
+ ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
match cel with
| nil => OK nil
| (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
- match coreVarSort v' with
- | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t')
- | CoreTypeVar _ => Error "found a type variable in a recursive let"
- | CoreCoerVar _ => Error "found a coercion variable in a recursive let"
+ match coreVarToWeakVar v' with
+ | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
+ | WTypeVar _ => Error "found a type variable in a recursive let"
+ | WCoerVar _ => Error "found a coercion variable in a recursive let"
end
end) rb) >>= fun rb' =>
coreExprToWeakExpr e >>= fun e' =>
OK (WELetRec (unleaves' rb') e')
| CoreECase e v tbranches alts =>
+ match coreVarToWeakVar v with
+ | WTypeVar _ => Error "found a type variable in a case"
+ | WCoerVar _ => Error "found a coercion variable in a case"
+ | WExprVar ev =>
coreExprToWeakExpr e
>>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
match te' with
| TyConApp _ tc lt =>
((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
- : ???(list (AltCon*list CoreVar*WeakExpr)) :=
+ : ???(list (AltCon*list WeakVar*WeakExpr)) :=
match branches with
| nil => OK nil
| (mkTriple alt vars e)::rest =>
- mkBranches rest
- >>= fun rest' =>
+ mkBranches rest >>= fun rest' =>
coreExprToWeakExpr e >>= fun e' =>
match alt with
| DEFAULT => OK ((DEFAULT,nil,e')::rest')
| LitAlt lit => OK ((LitAlt lit,nil,e')::rest')
- | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),vars,e')::rest')
+ | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')
end
end) alts)
>>= fun branches => coreExprToWeakExpr e
>>= fun scrutinee =>
list2vecOrError lt _ >>= fun lt' =>
- OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches)))
+ OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches)))
| _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
end
+ end
end.
Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)).
Instance CoreNameEqDecidable : EqDecidable CoreName :=
{ eqd_dec := coreName_eq
-; eqd_dec_reflexive := coreName_eq_refl
}.
Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ].
Extract Inductive PredType =>
"TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ].
-Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
-
-Definition haskLiteralToCoreType lit : CoreType :=
- TyConApp (haskLiteralToTyCon lit) nil.
-
-Inductive CoreVarSort : Type :=
-| CoreExprVar : CoreType -> CoreVarSort
-| CoreTypeVar : Kind -> CoreVarSort
-| CoreCoerVar : CoreType * CoreType -> CoreVarSort.
-
-Variable coreVarSort : CoreVar -> CoreVarSort. Extract Inlined Constant coreVarSort => "coreVarSort".
-
Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString".
Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString".
Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString".
Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType.
Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+
+Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)).
+ Extract Inlined Constant coretype_eq_dec => "Type.coreEqType".
+ Instance CoreTypeEqDecidable : EqDecidable CoreType.
+ apply Build_EqDecidable.
+ apply coretype_eq_dec.
+ Defined.
+
+Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)".
Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)).
Instance CoreVarEqDecidable : EqDecidable CoreVar :=
{ eqd_dec := coreVar_eq
-; eqd_dec_reflexive := coreVar_eq_refl
+(*; eqd_dec_reflexive := coreVar_eq_refl*)
}.
Notation "'★'" := KindType.
Notation "a ⇛ b" := (KindTypeFunction a b).
+Instance KindEqDecidable : EqDecidable Kind.
+ apply Build_EqDecidable.
+ induction v1.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; auto.
+ destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto;
+ right; intro; subst; inversion H; subst; apply n; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ destruct v2; try (right; intro q; inversion q; fail) ; left ; auto.
+ Defined.
+
Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString".
Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString".
Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString".
Extract Inlined Constant tyCon_eq => "(==)".
Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)).
Extract Inlined Constant dataCon_eq => "(==)".
-Axiom tyCon_eq_reflexive : forall `(tc:TyCon n), (tyCon_eq tc tc) = (left _ (refl_equal tc)).
-Axiom dataCon_eq_reflexive : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)).
-
-Instance TyConEqDecidable {n} : EqDecidable (TyCon n) :=
-{ eqd_dec := tyCon_eq
-; eqd_dec_reflexive := tyCon_eq_reflexive
-}.
-
-Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) :=
-{ eqd_dec := dataCon_eq
-; eqd_dec_reflexive := dataCon_eq_reflexive
-}.
+Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := { eqd_dec := tyCon_eq }.
+Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := { eqd_dec := dataCon_eq }.
-(*
-Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)).
-Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
-Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end.
-(* the type of the scrutinee in a case branch *)
-Require Import Coq.Arith.EqNat.
-Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}.
- intros.
- destruct H.
- exists x; omega.
- Defined.
-Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n.
- induction n.
- apply vec_nil.
- apply vec_cons.
- exists n; omega.
- apply (vec_map (bump _)); auto.
- Defined.
-Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)).
- set (hv1 _ (vecOfNats _)) as hv1'.
- set (hv2 _ (vecOfNats _)) as hv2'.
- destruct hv1' as [hv1_n hv1_pf].
- destruct hv2' as [hv2_n hv2_pf].
- clear hv1_pf.
- clear hv2_pf.
- set (eq_nat_decide hv1_n hv2_n) as dec.
- destruct dec.
- left. admit.
- right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl.
- Defined.
-(* equality on levels is decidable *)
-Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2))
- := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2.
-*)
Generalizable All Variables.
Require Import Preamble.
Require Import General.
+Require Import Coq.Lists.List.
Require Import HaskGeneral.
Require Import HaskLiterals.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
+Require Import HaskCoreTypes.
+Require Import HaskWeakVars.
Inductive WeakExpr :=
-| WEVar : CoreVar -> WeakExpr
-| WELit : HaskLiteral -> WeakExpr
-| WELet : CoreVar -> WeakExpr -> WeakExpr -> WeakExpr
-| WELetRec : Tree ??(CoreVar * WeakExpr) -> WeakExpr -> WeakExpr
-| WECast : WeakExpr -> CoreCoercion -> WeakExpr
-| WENote : Note -> WeakExpr -> WeakExpr
-| WEApp : WeakExpr -> WeakExpr -> WeakExpr
-| WETyApp : WeakExpr -> CoreType -> WeakExpr
-| WECoApp : WeakExpr -> CoreCoercion -> WeakExpr
-| WELam : CoreVar -> WeakExpr -> WeakExpr
-| WETyLam : CoreVar -> WeakExpr -> WeakExpr
-| WECoLam : CoreVar -> WeakExpr -> WeakExpr
-| WEBrak : CoreVar -> WeakExpr -> WeakExpr
-| WEEsc : CoreVar -> WeakExpr -> WeakExpr
+| WEVar : WeakExprVar -> WeakExpr
+| WELit : HaskLiteral -> WeakExpr
+| WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr
+| WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr
+| WECast : WeakExpr -> WeakCoercion -> WeakExpr
+| WENote : Note -> WeakExpr -> WeakExpr
+| WEApp : WeakExpr -> WeakExpr -> WeakExpr
+| WETyApp : WeakExpr -> CoreType -> WeakExpr
+| WECoApp : WeakExpr -> WeakCoercion -> WeakExpr
+| WELam : WeakExprVar -> WeakExpr -> WeakExpr
+| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
+| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
+| WEBrak : WeakTypeVar -> WeakExpr -> WeakExpr
+| WEEsc : WeakTypeVar -> WeakExpr -> WeakExpr
| WECase : forall (scrutinee:WeakExpr)
(tbranches:CoreType)
{n:nat}(tc:TyCon n)
(type_params:vec CoreType n)
- (alts : Tree ??(AltCon*list CoreVar*WeakExpr)),
+ (alts : Tree ??(AltCon*list WeakVar*WeakExpr)),
WeakExpr.
-(* calculate the free CoreVar's in a WeakExpr *)
-Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar :=
+(* calculate the free WeakVar's in a WeakExpr *)
+Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
match me with
| WELit _ => nil
| WEVar cv => cv::nil
| WEEsc ec e => getWeakExprFreeVars e
| WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
| WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2)
- | WELam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
- | WETyLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
- | WECoLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e)
+ | WELam cv e => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
+ | WETyLam cv e => getWeakExprFreeVars e
+ | WECoLam cv e => getWeakExprFreeVars e
(* the messy fixpoints below are required by Coq's termination conditions *)
| WECase scrutinee tbranches n tc type_params alts =>
mergeDistinctLists (getWeakExprFreeVars scrutinee) (
- ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list CoreVar*WeakExpr)) {struct alts} : list CoreVar :=
+ ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) {struct alts} : list WeakExprVar :=
match alts with
| T_Leaf None => nil
| T_Leaf (Some (DEFAULT,_,e)) => getWeakExprFreeVars e
| T_Leaf (Some (LitAlt lit,_,e)) => getWeakExprFreeVars e
- | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e)) => removeFromDistinctList' vars (getWeakExprFreeVars e)
+ | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e)) => removeFromDistinctList'
+ (General.filter (map (fun v => match v with
+ | WExprVar ev => Some ev
+ | WTypeVar _ => None
+ | WCoerVar _ => None
+ end) vars))
+ (getWeakExprFreeVars e)
| T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2)
end) alts))
- | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) :=
+ | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) :=
match mlr with
| T_Leaf None => cvl
| T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl
| T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl)
end) mlr (mergeDistinctLists (getWeakExprFreeVars e)
- ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) :=
+ ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
match mlr with
| T_Leaf None => nil
| T_Leaf (Some (cv,e)) => getWeakExprFreeVars e
end) mlr))
end.
-(* wrap lambdas around an expression until it has no free variables *)
+(* wrap lambdas around an expression until it has no free expression variables *)
Definition makeClosedExpression : WeakExpr -> WeakExpr :=
- fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) :=
+ fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) :=
match cvl with
| nil => me
| cv::cvl' => WELam cv (closeExpression me cvl')
end) me (getWeakExprFreeVars me).
(* messy first-order capture-avoiding substitution on CoreType's *)
-Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) :=
+Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType :=
match te with
| TyVarTy tv' => if eqd_dec tv tv' then tsubst else te
- | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
+ | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
| FunTy t1 t2 => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)
- | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
+ | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst)
| PredTy (EqPred t1 t2) => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst))
| PredTy (IParam ip ty) => PredTy (IParam ip (replaceCoreVar ty tv tsubst))
| PredTy (ClassP _ c lt) => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) :=
(* calculate the CoreType of a WeakExpr *)
Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
match ce with
- | WEVar v => match coreVarSort v with
- | CoreExprVar t => OK t
- | CoreTypeVar _ => Error "found tyvar in expression"
- | CoreCoerVar _ => Error "found coercion variable in expression"
- end
+ | WEVar (weakExprVar v t) => OK t
| WELit lit => OK (haskLiteralToCoreType lit)
| WEApp e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' =>
match t' with
- | FunTy t1 t2 => OK t2
| (TyConApp 2 tc (t1::t2::nil)) =>
if (tyCon_eq tc ArrowTyCon)
then OK t2
- else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
- | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp")
+ else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
+ | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
end
| WETyApp e t => coreTypeOfWeakExpr e >>= fun te =>
match te with
- | ForAllTy v ct => match coreVarSort v with
- | CoreExprVar _ => Error "found an expression variable inside an forall-type!"
- | CoreTypeVar _ => OK (replaceCoreVar ct v t)
- | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!"
- end
- | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp")
+ | ForAllTy v ct => OK (replaceCoreVar ct v t)
+ | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
end
| WECoApp e co => coreTypeOfWeakExpr e >>= fun te =>
match te with
- | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3
| TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) =>
if (tyCon_eq tc ArrowTyCon)
then OK t3
- else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
- | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp")
+ else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
+ | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
end
- | WELam ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with
- | CoreExprVar vt => OK (FunTy vt t')
- | CoreTypeVar _ => Error "found a type variable in a WELam!"
- | CoreCoerVar _ => Error "found a coercion variable in a WELam!"
- end
- | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t')
- | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with
- | CoreExprVar vt => Error "found an expression variable in a WECoLam!"
- | CoreTypeVar _ => Error "found a type variable in a WECoLam!"
- | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t')
- end
+ | WELam (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil))
+ | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end
+ | WECoLam (weakCoerVar cv φ₁ φ₂) e =>
+ coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil))
| WELet ev ve e => coreTypeOfWeakExpr e
| WELetRec rb e => coreTypeOfWeakExpr e
| WENote n e => coreTypeOfWeakExpr e
- | WECast e co => OK (snd (coreCoercionKind co))
+ | WECast e (weakCoercion t1 t2 _) => OK t2
| WECase scrutinee tbranches n tc type_params alts => OK tbranches
- | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil))
- | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' =>
+ | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+ OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
+ | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
match t' with
| (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
if (tyCon_eq tc hetMetCodeTypeTyCon)
- then if eqd_dec ec ec' then OK t''
+ then if eqd_dec ecc ec' then OK t''
else Error "level mismatch in escapification"
else Error "ill-typed escapification"
| _ => Error "ill-typed escapification"
- end
+ end end
end.
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskWeakVars: types and variables for HaskWeak *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import HaskGeneral.
+Require Import HaskLiterals.
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+
+Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
+
+Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion.
+
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar.
+
+Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar.
+
+Inductive WeakVar : Type :=
+| WExprVar : WeakExprVar -> WeakVar
+| WTypeVar : WeakTypeVar -> WeakVar
+| WCoerVar : WeakCoerVar -> WeakVar.
+
+Definition haskLiteralToCoreType lit : CoreType :=
+ TyConApp (haskLiteralToTyCon lit) nil.
+
+Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt.
+
+Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType.
+
+(* EqDecidable instances for all of the above *)
+Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar.
+ apply Build_EqDecidable.
+ intros.
+ destruct v1 as [cv1 k1].
+ destruct v2 as [cv2 k2].
+ destruct (eqd_dec cv1 cv2); subst.
+ destruct (eqd_dec k1 k2); subst.
+ left; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ Defined.
+
+Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar.
+ apply Build_EqDecidable.
+ intros.
+ destruct v1 as [cv1 t1a t1b].
+ destruct v2 as [cv2 t2a t2b].
+ destruct (eqd_dec cv1 cv2); subst.
+ destruct (eqd_dec t1a t2a); subst.
+ destruct (eqd_dec t1b t2b); subst.
+ left; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ Defined.
+
+Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar.
+ apply Build_EqDecidable.
+ intros.
+ destruct v1 as [cv1 k1].
+ destruct v2 as [cv2 k2].
+ destruct (eqd_dec cv1 cv2); subst.
+ destruct (eqd_dec k1 k2); subst.
+ left; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ right; intro; apply n; inversion H; subst; auto.
+ Defined.
+
+Instance WeakVarEqDecidable : EqDecidable WeakVar.
+ apply Build_EqDecidable.
+ induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto;
+ destruct (eqd_dec w w0); subst.
+ left; auto.
+ right; intro X; apply n; inversion X; auto.
+ left; auto.
+ right; intro X; apply n; inversion X; auto.
+ left; auto.
+ right; intro X; apply n; inversion X; auto.
+ Defined.
+
+
+
+
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
+Require Import HaskWeakVars.
Require Import HaskWeak.
Require Import HaskCoreToWeak.
Require Import HaskStrongTypes.
projects / coq-hetmet.git / commitdiff