X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction.v;fp=src%2FExtraction.v;h=43d404fa98169f42ca0c61e7eb48f160d9a205f1;hp=66a69dac1d2225211fef67900791b03215935cf2;hb=4359342db4052c77b802ce256856df71387e7a62;hpb=2a887b5df62e3202c859c953d83918872bda31e4 diff --git a/src/Extraction.v b/src/Extraction.v index 66a69da..43d404f 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -1,9 +1,9 @@ (* need this or the Haskell extraction fails *) Set Printing Width 1300000. -Require Import Coq.Lists.List. Require Import Coq.Strings.Ascii. Require Import Coq.Strings.String. +Require Import Coq.Lists.List. Require Import Preamble. Require Import General. @@ -25,7 +25,7 @@ Require Import HaskProof. Require Import HaskCoreToWeak. Require Import HaskWeakToStrong. Require Import HaskStrongToProof. -(*Require Import HaskProofToStrong.*) +Require Import HaskProofToStrong. Require Import HaskProofToLatex. Require Import HaskStrongToWeak. Require Import HaskWeakToCore. @@ -33,13 +33,14 @@ Require Import HaskWeakToCore. 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 vec => "([])" [ "([])" "(:)" ].*) -(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*) -Extract Inlined Constant map => "Prelude.map". -Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. +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" ]. @@ -47,10 +48,9 @@ Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive unit => "()" [ "()" ]. Extract Inlined Constant string_dec => "(==)". Extract Inlined Constant ascii_dec => "(==)". -Extract Inductive string => "Prelude.String" [ "[]" "(:)" ]. (* adapted from ExtrOcamlString.v *) -Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'". +Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'". Extract Constant zero => "'\000'". Extract Constant one => "'\001'". Extract Constant shift => "shiftAscii". @@ -58,10 +58,10 @@ 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))". + 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. @@ -116,6 +116,7 @@ Section core2proof. eol+++"\end{document}"+++ eol. + Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := addErrorMessage ("input CoreSyn: " +++ ce) (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) ( @@ -162,6 +163,124 @@ Section core2proof. 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 = ★). + admit. + 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) ( @@ -173,13 +292,18 @@ Section core2proof. ((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) -*) - )))))))). + + (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 @@ -212,6 +336,7 @@ Section core2proof. end. End core2proof. - +(*Set Extraction Optimize.*) +(*Set Extraction AutoInline.*) Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.