--import TcType
--import CoreFVs
--import CoreUtils
---import MkCore
--import Var
--import BasicTypes
--import Bag
--import SrcLoc
--import Data.List
+import qualified MkCore
import qualified TysWiredIn
import qualified TysPrim
import qualified Outputable
Unset Extraction Optimize.
Unset Extraction AutoInline.
-Definition coqCoreToStringPass (s:CoreExpr CoreVar) : string
+Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string
:= "FIXME".
(*
Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar
Require Import HaskCoreVars.
(* this type must extract to EXACTLY match TypeRep.Type *)
-Inductive CoreExpr (b:Type) :=
-| CoreEVar : CoreVar -> CoreExpr b
-| CoreELit : HaskLiteral -> CoreExpr b
-| CoreEApp : CoreExpr b -> CoreExpr b -> CoreExpr b
-| CoreELam : b -> CoreExpr b -> CoreExpr b
-| CoreELet : CoreBind b -> CoreExpr b -> CoreExpr b
-| CoreECase : CoreExpr b -> b -> CoreType -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
-| CoreECast : CoreExpr b -> CoreCoercion -> CoreExpr b
-| CoreENote : Note -> CoreExpr b -> CoreExpr b
-| CoreEType : CoreType -> CoreExpr b
-with CoreBind (b:Type) :=
-| CoreNonRec : b -> CoreExpr b -> CoreBind b
-| CoreRec : list (b * CoreExpr b) -> CoreBind b.
+Inductive CoreExpr {b:Type} :=
+| CoreEVar : CoreVar -> CoreExpr
+| CoreELit : HaskLiteral -> CoreExpr
+| CoreEApp : CoreExpr -> CoreExpr -> CoreExpr
+| CoreELam : b -> CoreExpr -> CoreExpr
+| CoreELet : CoreBind -> CoreExpr -> CoreExpr
+| CoreECase : CoreExpr -> b -> CoreType -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
+| CoreECast : CoreExpr -> CoreCoercion -> CoreExpr
+| CoreENote : Note -> CoreExpr -> CoreExpr
+| CoreEType : CoreType -> CoreExpr
+with CoreBind {b:Type} :=
+| CoreNonRec : b -> CoreExpr -> CoreBind
+| CoreRec : list (b * CoreExpr ) -> CoreBind.
Extract Inductive CoreExpr =>
"CoreSyn.Expr" [
"CoreSyn.Var"
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 :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
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
+ | WTypeVar tv => Some (tv,tbody)
| WCoerVar _ => None
end else None
| _ => None
end.
-Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
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
+ | WTypeVar tv => Some (tv,tbody)
| WCoerVar _ => None
end else None
| _ => None
let (t1,t2) := coreCoercionKind cc
in weakCoercion t1 t2 cc.
-Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
+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')
end
| CoreEApp e1 e2 => match isBrak e1 with
- | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
+ | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e' t)
| None => match isEsc e1 with
- | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
+ | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e' t)
| None => coreExprToWeakExpr e1 >>= fun e1' =>
match e2 with
| CoreEType t => OK (WETyApp e1' t)
end
| CoreELet (CoreRec rb) e =>
- ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
+ ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
match cel with
| nil => OK nil
| (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
>>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
match te' with
| TyConApp _ tc lt =>
- ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
+ ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
: ???(list (AltCon*list WeakVar*WeakExpr)) :=
match branches with
| nil => OK nil
| WELam : WeakExprVar -> WeakExpr -> WeakExpr
| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
-| WEBrak : WeakTypeVar -> WeakExpr -> WeakExpr
-| WEEsc : WeakTypeVar -> WeakExpr -> WeakExpr
+
+(* the CoreType argument is used only when going back from Weak to Core; it lets us dodge a possibly-failing type calculation *)
+| WEBrak : WeakTypeVar -> WeakExpr -> CoreType -> WeakExpr
+| WEEsc : WeakTypeVar -> WeakExpr -> CoreType -> WeakExpr
+
+(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
| WECase : forall (scrutinee:WeakExpr)
(tbranches:CoreType)
{n:nat}(tc:TyCon n)
| WENote n e => getWeakExprFreeVars e
| WETyApp e t => getWeakExprFreeVars e
| WECoApp e co => getWeakExprFreeVars e
- | WEBrak ec e => getWeakExprFreeVars e
- | WEEsc ec e => getWeakExprFreeVars e
+ | WEBrak ec e _ => getWeakExprFreeVars e
+ | 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 _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
| WENote n e => coreTypeOfWeakExpr e
| WECast e (weakCoercion t1 t2 _) => OK t2
| WECase scrutinee tbranches n tc type_params alts => OK tbranches
- | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+
+ (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
+ | 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 _ =>
+ | 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)