From 743099bc348cfa97fb4d94c7e7ae3e53d2717e87 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:17:55 -0700 Subject: [PATCH] split Extraction.v so most can be compiled with -dont-load-proofs --- Makefile | 1 + src/Extraction.v | 344 +------------------------------------------------ src/ExtractionMain.v | 349 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 352 insertions(+), 342 deletions(-) create mode 100644 src/ExtractionMain.v diff --git a/Makefile b/Makefile index b8851aa..2d65894 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,7 @@ default: build/CoqPass.hs build/CoqPass.hs: $(allfiles) make build/Makefile.coq + cd build; make -f Makefile.coq OPTS=-dont-load-proofs ExtractionMain.vo cd build; make -f Makefile.coq Extraction.vo cat src/Extraction-prefix.hs > build/CoqPass.hs cat build/Extraction.hs | grep -v '^module' | grep -v '^import' >> build/CoqPass.hs diff --git a/src/Extraction.v b/src/Extraction.v index 82b0543..eb13e2b 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -1,351 +1,11 @@ (*********************************************************************************************************************************) -(* Extraction: *) -(* *) -(* This module is the "top level" for extraction *) -(* *) +(* ExtractionMain: just the "Extract" command *) (*********************************************************************************************************************************) (* need this or the Haskell extraction fails *) Set Printing Width 1300000. +Require Import ExtractionMain. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. - -Require Import Preamble. -Require Import General. - -Require Import NaturalDeduction. -Require Import NaturalDeductionToLatex. - -Require Import HaskKinds. -Require Import HaskLiteralsAndTyCons. -Require Import HaskCoreVars. -Require Import HaskCoreTypes. -Require Import HaskCore. -Require Import HaskWeakVars. -Require Import HaskWeakTypes. -Require Import HaskWeak. -Require Import HaskStrongTypes. -Require Import HaskStrong. -Require Import HaskProof. -Require Import HaskCoreToWeak. -Require Import HaskWeakToStrong. -Require Import HaskStrongToProof. -Require Import HaskProofToLatex. -Require Import HaskStrongToWeak. -Require Import HaskWeakToCore. -Require Import HaskProofToStrong. - -Require Import HaskProofCategory. -Require Import HaskStrongCategory. -Require Import ReificationsEquivalentToGeneralizedArrows. - -Open Scope string_scope. -Extraction Language Haskell. - -(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*) -(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) -(*Extract Inlined Constant map => "Prelude.map".*) - -(* I try to reuse Haskell types mostly to get the "deriving Show" aspect *) -Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. -Extract Inductive list => "([])" [ "([])" "(:)" ]. -Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. -Extract Inductive prod => "(,)" [ "(,)" ]. -Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. -Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. -Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. -Extract Inductive unit => "()" [ "()" ]. -Extract Inlined Constant string_dec => "(==)". -Extract Inlined Constant ascii_dec => "(==)". - -(* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => "shiftAscii". - -Unset Extraction Optimize. -Unset Extraction AutoInline. - -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 Γ : TypeEnv := nil. - - Definition Δ : CoercionEnv Γ := nil. - - Definition φ : TyVarResolver Γ := - fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)). - (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*) - - 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 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} % 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=200in,centering]{geometry}"+++eol+++ - "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++ - "\begin{document}"+++eol+++ - "\begin{preview}"+++eol. - - Definition footer : string := - 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 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 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 useUniqueSupply {T}(ut:UniqM T) : ???T := - match ut with - uniqM f => - f uniqueSupply >>= fun x => OK (snd x) - end. - - Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }. - intros. - induction ln. - exists O. - intros. - inversion H. - destruct IHln as [n pf]. - exists (plus (S n) a). - intros. - destruct H. - omega. - fold (@In _ n' ln) in H. - set (pf n' H) as q. - omega. - Defined. - - Definition FreshNat : @FreshMonad nat. - refine {| FMT := fun T => nat -> prod nat T - ; FMT_fresh := _ - |}. - Focus 2. - intros. - refine ((S H),_). - set (larger tl) as q. - destruct q as [n' pf]. - exists n'. - intros. - set (pf _ H0) as qq. - omega. - - refine {| returnM := fun a (v:a) => _ |}. - intro n. exact (n,v). - intros. - set (X H) as q. - destruct q as [n' v]. - set (X0 v n') as q'. - exact q'. - Defined. - - Definition unFresh {T} : @FreshM _ FreshNat T -> T. - intros. - destruct X. - exact O. - apply t. - Defined. - - Definition env := ★::nil. - Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _). - Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]]. - eapply nd_comp. - eapply nd_comp. - eapply nd_rule. - apply RVar. - eapply nd_rule. - eapply (RURule _ _ _ _ (RuCanL _ _)) . - eapply nd_rule. - eapply RLam. - Defined. -(* - Definition TInt : HaskType nil ★. - assert (tyConKind' intPrimTyCon = ★). - rewrite <- H. - unfold HaskType; intros. - apply TCon. - Defined. - - Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]]. - apply nd_rule. - apply RVar. - Defined. - - Definition idtype := - HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))). - - Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]]. - eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ]. - apply idproof0. - Defined. -*) -(* - 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 τ => - addErrorMessage ("HaskType: " +++ τ) - ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => - (let haskProof := @expr2proof _ _ _ _ _ _ e - in (* insert HaskProof-to-HaskProof manipulations here *) - (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof)) - >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e')) -(* - >>= fun e' => - Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e')) - *) -) -)))))))). -(* Error "X").*) -(* - strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply - (projT2 e') - INil - >>= fun q => Error (toString q) - ))))))))). -*) -*) - - 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 => - - (addErrorMessage ("HaskStrong...") - (let haskProof := @expr2proof _ _ _ _ _ _ e - in (* insert HaskProof-to-HaskProof manipulations here *) - OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) - >>= fun e' => - (snd e') >>= fun e'' => - strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply - (projT2 e'') INil - >>= fun q => - OK (weakExprToCoreExpr q) - )))))))))). - - 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. (*Set Extraction Optimize.*) (*Set Extraction AutoInline.*) Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore. diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v new file mode 100644 index 0000000..59183c9 --- /dev/null +++ b/src/ExtractionMain.v @@ -0,0 +1,349 @@ +(*********************************************************************************************************************************) +(* ExtractionMain: *) +(* *) +(* This module is the "top level" for extraction *) +(* *) +(*********************************************************************************************************************************) + +Require Import Coq.Strings.Ascii. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. + +Require Import Preamble. +Require Import General. + +Require Import NaturalDeduction. +Require Import NaturalDeductionToLatex. + +Require Import HaskKinds. +Require Import HaskLiteralsAndTyCons. +Require Import HaskCoreVars. +Require Import HaskCoreTypes. +Require Import HaskCore. +Require Import HaskWeakVars. +Require Import HaskWeakTypes. +Require Import HaskWeak. +Require Import HaskStrongTypes. +Require Import HaskStrong. +Require Import HaskProof. +Require Import HaskCoreToWeak. +Require Import HaskWeakToStrong. +Require Import HaskStrongToProof. +Require Import HaskProofToLatex. +Require Import HaskStrongToWeak. +Require Import HaskWeakToCore. +Require Import HaskProofToStrong. + +Require Import HaskProofCategory. +(* +Require Import HaskStrongCategory. +Require Import ReificationsEquivalentToGeneralizedArrows. +Require Import ProgrammingLanguage. +*) + +Open Scope string_scope. +Extraction Language Haskell. + +(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*) +(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) +(*Extract Inlined Constant map => "Prelude.map".*) + +(* I try to reuse Haskell types mostly to get the "deriving Show" aspect *) +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inlined Constant string_dec => "(==)". +Extract Inlined Constant ascii_dec => "(==)". + +(* adapted from ExtrOcamlString.v *) +Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => "shiftAscii". + +Unset Extraction Optimize. +Unset Extraction AutoInline. + +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 Γ : TypeEnv := nil. + + Definition Δ : CoercionEnv Γ := nil. + + Definition φ : TyVarResolver Γ := + fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)). + (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*) + + 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 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} % 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=200in,centering]{geometry}"+++eol+++ + "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++ + "\begin{document}"+++eol+++ + "\begin{preview}"+++eol. + + Definition footer : string := + eol+++"\end{preview}"+++ + eol+++"\end{document}"+++ + eol. + + + Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := Error "Temporarily Disabled". +(* + 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 _ => false) τ 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 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 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 useUniqueSupply {T}(ut:UniqM T) : ???T := + match ut with + uniqM f => + f uniqueSupply >>= fun x => OK (snd x) + end. + + Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }. + intros. + induction ln. + exists O. + intros. + inversion H. + destruct IHln as [n pf]. + exists (plus (S n) a). + intros. + destruct H. + omega. + fold (@In _ n' ln) in H. + set (pf n' H) as q. + omega. + Defined. + + Definition FreshNat : @FreshMonad nat. + refine {| FMT := fun T => nat -> prod nat T + ; FMT_fresh := _ + |}. + Focus 2. + intros. + refine ((S H),_). + set (larger tl) as q. + destruct q as [n' pf]. + exists n'. + intros. + set (pf _ H0) as qq. + omega. + + refine {| returnM := fun a (v:a) => _ |}. + intro n. exact (n,v). + intros. + set (X H) as q. + destruct q as [n' v]. + set (X0 v n') as q'. + exact q'. + Defined. + + Definition unFresh {T} : @FreshM _ FreshNat T -> T. + intros. + destruct X. + exact O. + apply t. + Defined. + + Definition env := ★::nil. + Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _). + Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]]. + eapply nd_comp. + eapply nd_comp. + eapply nd_rule. + apply RVar. + eapply nd_rule. + eapply (RURule _ _ _ _ (RuCanL _ _)) . + eapply nd_rule. + eapply RLam. + Defined. +(* + Definition TInt : HaskType nil ★. + assert (tyConKind' intPrimTyCon = ★). + rewrite <- H. + unfold HaskType; intros. + apply TCon. + Defined. + + Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]]. + apply nd_rule. + apply RVar. + Defined. + + Definition idtype := + HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))). + + Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]]. + eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ]. + apply idproof0. + Defined. +*) +(* + 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 τ => + addErrorMessage ("HaskType: " +++ τ) + ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => + (let haskProof := @expr2proof _ _ _ _ _ _ e + in (* insert HaskProof-to-HaskProof manipulations here *) + (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof)) + >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e')) +(* + >>= fun e' => + Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e')) + *) +) +)))))))). +(* Error "X").*) +(* + strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e') + INil + >>= fun q => Error (toString q) + ))))))))). +*) +*) + + 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 => + + (addErrorMessage ("HaskStrong...") + (let haskProof := @expr2proof _ _ _ _ _ _ e + in (* insert HaskProof-to-HaskProof manipulations here *) + OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => + (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => + OK (weakExprToCoreExpr q) + )))))))))). + + 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. -- 1.7.10.4