Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
- Context (hetmet_brak : WeakExprVar).
- Context (hetmet_esc : WeakExprVar).
- Context (uniqueSupply : UniqSupply).
+ Context (hetmet_brak : WeakExprVar).
+ Context (hetmet_esc : WeakExprVar).
+ Context (hetmet_kappa : WeakExprVar).
+ Context (hetmet_kappa_app : WeakExprVar).
+ Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
match ut with
(do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_kappa : WeakExprVar)
+ (hetmet_kappa_app : WeakExprVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+ Definition hetmet_kappa' := coreVarToWeakExprVarOrError hetmet_kappa.
+ Definition hetmet_kappa_app' := coreVarToWeakExprVarOrError hetmet_kappa_app.
Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString cex)
OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))))
: CoreM (list (@CoreBind CoreVar)) :=
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
do_skolemize
hetmet_brak
hetmet_esc
+ (*
+ hetmet_kappa
+ hetmet_kappa_app
+ *)
uniqueSupply
hetmet_PGArrow
hetmet_PGArrow_unit
Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+Variable hetmet_kappa_name : CoreName. Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name".
+Variable hetmet_kappa_app_name: CoreName.
+Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name".
Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
split_list lwt (length (fst (tyFunKind tf))) >>=
| _ => None
end.
+Definition isKappa (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3))
+ => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
+Definition isKappaApp (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3)) _)
+ => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
OK (WECSP v tv e' t')
- | None => coreExprToWeakExpr e1 >>= fun e1' =>
- match e2 with
- | CoreEType t =>
- coreTypeToWeakType t >>= fun t' =>
- OK (WETyApp e1' t')
- | _ => coreExprToWeakExpr e2
- >>= fun e2' => OK (WEApp e1' e2')
- end
- end
- end
+ | None =>
+ (*
+ if isKappa e1
+ then match e2 with
+ | CoreELam v e => match coreVarToWeakVar' v with
+ | OK (WExprVar ev) =>
+ coreExprToWeakExpr e >>= fun e' =>
+ OK (WEKappa ev e')
+ | _ => Error "bogus"
+ end
+ | _ => Error "bogus"
+ end
+ else if isKappaApp e1
+ then match e1 with
+ | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
+ coreExprToWeakExpr e1' >>= fun e1'' =>
+ coreExprToWeakExpr e2 >>= fun e2'' =>
+ OK (WEKappaApp e1'' e2'')
+ | _ => Error "bogus"
+ end
+ else
+ *)
+ coreExprToWeakExpr e1 >>= fun e1' =>
+ match e2 with
+ | CoreEType t =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WETyApp e1' t')
+ | _ => coreExprToWeakExpr e2
+ >>= fun e2' => OK (WEApp e1' e2')
+ end
+ end
+ end
end
| CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with
| TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
| TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
| TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
+ (*
+ | TKappa : RawHaskType (★ ⇛★ ⇛★ ) (* (~~>) *)
+ *)
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
Implicit Arguments TAll [ [TV] ].
Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
+(*Notation "t1 ~~~> t2" := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
(* Kind and Coercion Environments *)
| WETyApp : WeakExpr -> WeakType -> WeakExpr
| WECoApp : WeakExpr -> WeakCoercion -> WeakExpr
| WELam : WeakExprVar -> WeakExpr -> WeakExpr
+(*
+| WEKappa : WeakExprVar -> WeakExpr -> WeakExpr
+| WEKappaApp : WeakExpr -> WeakExpr -> WeakExpr
+*)
| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
(weakExprToCoreExpr e)::
nil)
(CoreEVar v)
+ (*
+ | WEKappa v e => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappa"
+ | WEKappaApp e1 e2 => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappaApp"
+ *)
| WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
| WECase vscrut escrut tbranches tc types alts =>
CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
| WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
| WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
| WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+(*
+ | WEKappaApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+ | WEKappa cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+*)
| WETyLam cv e => doesWeakVarOccur wev e
| WECoLam cv e => doesWeakVarOccur wev e
| WECase vscrut escrut tbranches tc avars alts =>