Require Import NaturalDeductionToLatex.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskCoreToWeak.
Require Import HaskWeakToStrong.
Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
+(*Require Import HaskProofToStrong.*)
Require Import HaskProofToLatex.
Require Import HaskStrongToWeak.
Require Import HaskWeakToCore.
Unset Extraction Optimize.
Unset Extraction AutoInline.
-Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
+
+Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
+Variable mkSystemName : Unique -> string -> nat -> Name.
+ Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
+Variable mkTyVar : Name -> Kind -> CoreVar.
+ Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
+Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
+ Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
+Variable mkExVar : Name -> CoreType -> CoreVar.
+ Extract Inlined Constant mkExVar => "Id.mkLocalId".
Section core2proof.
Context (ce:@CoreExpr CoreVar).
Definition Δ : CoercionEnv Γ := nil.
Definition φ : TyVarResolver Γ :=
- fun cv => (fun TV env => Prelude_error "unbound tyvar").
+ fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
(*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
- Definition ψ : CoreVar->HaskCoVar nil Δ
- := fun cv => Prelude_error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
+ Definition ψ : CoVarResolver Γ Δ :=
+ fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
(* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
match coreVarToWeakVar cv with
- | WExprVar wev => match weakTypeToType'' φ wev ★ with
+ | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
| Error s => Prelude_error ("Error in top-level xi: " +++ s)
| OK t => t @@ nil
end
| WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
end.
+
+ (* core-to-string (-dcoqpass) *)
+
Definition header : string :=
"\documentclass[9pt]{article}"+++eol+++
"\usepackage{amsmath}"+++eol+++
"\usepackage{amssymb}"+++eol+++
"\usepackage{proof}"+++eol+++
- "\usepackage{mathpartir}"+++eol+++
- "\usepackage{trfrac}"+++eol+++
+ "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
+ "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
"\def\code#1#2{\Box_{#1} #2}"+++eol+++
- "\usepackage[paperwidth=20in,centering]{geometry}"+++eol+++
+ "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
"\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
"\begin{document}"+++eol+++
"\begin{preview}"+++eol.
eol+++"\end{document}"+++
eol.
- Definition handleExpr (ce:@CoreExpr CoreVar) : string :=
- match coreExprToWeakExpr ce with
- | Error s => Prelude_error ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s)
- | OK we => match weakTypeOfWeakExpr we >>= fun t => weakTypeToType φ t with
- | Error s => Prelude_error ("unable to calculate HaskType of a HaskWeak expression because: " +++ s)
- | OK τ => match τ with
- | haskTypeOfSomeKind ★ τ' =>
- match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
- | Error s => Prelude_error ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
- | OK e' => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
- end
- | haskTypeOfSomeKind κ τ' =>
- Prelude_error ("encountered 'expression' of kind "+++κ+++" at top level (type "+++τ'
- +++"); shouldn't happen")
- end
- end
+ Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+ addErrorMessage ("HaskType: " +++ τ)
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+ OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
+ )))))))).
+
+ Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
+ match coreToStringExpr' ce with
+ | OK x => x
+ | Error s => Prelude_error s
end.
- Definition handleBind (bind:@CoreBind CoreVar) : string :=
- match bind with
- | CoreNonRec _ e => handleExpr e
- | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => handleExpr (snd x)) lbe) ""
+ Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
+ match binds with
+ | CoreNonRec _ e => coreToStringExpr e
+ | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
end.
Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
header +++
- (fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "")
+ (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
+++ footer.
- Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
- lbinds.
+
+ (* core-to-core (-fcoqpass) *)
+ Section CoreToCore.
+
+ Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
+ weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
+ Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
+ weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
+ 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).
+
+ Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+ (* insert HaskStrong-to-HaskStrong manipulations here *)
+ strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil
+ >>= fun q => OK (weakExprToCoreExpr q)
+(*
+ OK (weakExprToCoreExpr we)
+*)
+ )))))))).
+
+ Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
+ match coreToCoreExpr' ce with
+ | OK x => x
+ | Error s => Prelude_error s
+ end.
+
+ Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
+ match binds with
+ | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+ | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+ end.
+
+ Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+ map coreToCoreBind lbinds.
+
+ End CoreToCore.
+
+ Definition coqPassCoreToCore
+ (hetmet_brak : CoreVar)
+ (hetmet_esc : CoreVar)
+ (uniqueSupply : UniqSupply)
+ (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+ match coreVarToWeakVar hetmet_brak with
+ | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
+ | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
+ | _ => Prelude_error "IMPOSSIBLE"
+ end
+ | _ => Prelude_error "IMPOSSIBLE"
+ end.
End core2proof.
projects / coq-hetmet.git / blobdiff