X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FExtraction.v;h=66a69dac1d2225211fef67900791b03215935cf2;hb=f7a6e08c97cae1c1b278c18a1904eadec4e5f010;hp=22564a27cfc763c277161d11df897660bd2ed1f4;hpb=976b9bb93bf6ab296b3ac60dcdb4e87b1c665376;p=coq-hetmet.git diff --git a/src/Extraction.v b/src/Extraction.v index 22564a2..66a69da 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -12,7 +12,7 @@ Require Import NaturalDeduction. Require Import NaturalDeductionToLatex. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -27,7 +27,7 @@ Require Import HaskWeakToStrong. Require Import HaskStrongToProof. (*Require Import HaskProofToStrong.*) Require Import HaskProofToLatex. -(*Require Import HaskStrongToWeak.*) +Require Import HaskStrongToWeak. Require Import HaskWeakToCore. Open Scope string_scope. @@ -50,20 +50,24 @@ Extract Inlined Constant ascii_dec => "(==)". Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Prelude.Char" -[ -"{- If this appears, you're using Ascii internals. Please don't -} (\ b0 b1 b2 b3 b4 b5 b6 b7 -> let f b i = if b then 1 `shiftL` i else 0 in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))" -] -"{- If this appears, you're using Ascii internals. Please don't -} (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)". +Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'". +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => "shiftAscii". Unset Extraction Optimize. Unset Extraction AutoInline. -Axiom fail : forall {A}, string -> A. - Extract Inlined Constant fail => "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). @@ -72,57 +76,140 @@ Section core2proof. Definition Δ : CoercionEnv Γ := nil. - Definition φ : CoreVar->HaskTyVar Γ := - fun cv => (fun TV env => fail "unbound tyvar"). + Definition φ : TyVarResolver Γ := + 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 => fail ("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 ξ : WeakExprVar -> WeakType * list WeakTypeVar - := fun (v:WeakExprVar) => ((v:WeakType),nil). + Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ := + match coreVarToWeakVar cv with + | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with + | Error s => Prelude_error ("Error in top-level xi: " +++ s) + | OK t => t @@ nil + end + | WTypeVar _ => Prelude_error "top-level xi got a type variable" + | 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+++ - "\pdfpagewidth 50in"+++eol+++ - "\pdfpageheight 10in"+++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+++ - "\begin{document}"+++eol. + "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++ + "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++ + "\begin{document}"+++eol+++ + "\begin{preview}"+++eol. Definition footer : string := - eol+++"\end{document}"+++eol. - - Definition handleExpr (ce:@CoreExpr CoreVar) : string := - match coreExprToWeakExpr ce with - | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s) - | OK me => - match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with - | Indexed_Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) - | Indexed_OK τ e => match e with - | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s) - | OK e' => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer - end - end + eol+++"\end{preview}"+++ + eol+++"\end{document}"+++ + eol. + + 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 := - fold_left (fun x y => x+++eol+++eol+++y) (map handleBind lbinds) "". - - Definition coqPassCoreToCore (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := - lbinds. + header +++ + (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "") + +++ footer. + + + (* 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.