X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction.v;h=82b05434263ca1fb6e754f08f89ea3a1a8e7b616;hp=542b5d49d7fc8d462a8666b19ad4722467951b80;hb=32436fdf380f7f2efc7a70896268509e7b3e0d6f;hpb=703bff3b209bd7d114b49cb736da8af167a4ec71

diff --git a/src/Extraction.v b/src/Extraction.v
index 542b5d4..82b0543 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -1,23 +1,57 @@
+(*********************************************************************************************************************************)
+(* Extraction:                                                                                                                   *)
+(*                                                                                                                               *)
+(*    This module is the "top level" for extraction                                                                              *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
 (* 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 Main.
+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 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" ].
@@ -25,27 +59,294 @@ 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"
-[
-"{- 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 => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Constant zero   => "'\000'".
+Extract Constant one    => "'\001'".
+Extract Constant shift  => "shiftAscii".
 
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string
-   := "FIXME".
+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 coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar
-   :=
+    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)
+                  ))))))))).
+*)
 *)
 
-Extraction "Extraction.hs" coqCoreToStringPass.
+    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.