X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=143be0b5324fd29cfb526e3cf479b3bdcacf1f95;hb=f7a6e08c97cae1c1b278c18a1904eadec4e5f010;hp=3798a36fa341888940a05b0c0c9b888ebfb8bdff;hpb=8efffc7368b5e54c42461f45a9708ff2828409a4;p=coq-hetmet.git

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 3798a36..143be0b 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -12,7 +12,6 @@ Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
-Require Import HaskWeakVars.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
@@ -70,6 +69,7 @@ Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
+  | EGlobal  Γ Δ ξ _ _                            => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
@@ -586,6 +586,7 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
+    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
@@ -631,6 +632,12 @@ Definition expr2proof  :
     end
 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 
+    destruct case_EGlobal.
+      apply nd_rule.
+      simpl.
+      destruct t as [t lev].
+      apply (RGlobal _ _ _ _ wev).
+
     destruct case_EVar.
       apply nd_rule.
       unfold mapOptionTree; simpl.
@@ -705,6 +712,7 @@ Definition expr2proof  :
       auto.
 
     destruct case_ENote.
+      destruct t.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.
@@ -783,16 +791,3 @@ Definition expr2proof  :
 
 End HaskStrongToProof.
 
-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
-| DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
-| DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
-  mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
-