X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=077f7b509a22032859a83729226a7fc82b2620fe;hp=d5d66c0b7460b052e1fa28c9c52893aea810589e;hb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index d5d66c0..077f7b5 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -7,7 +7,9 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
+Require Import HaskCoreVars.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 
@@ -19,6 +21,8 @@ Inductive WeakAltCon :=
 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr
+
+(* TO DO: add a WEWhere and use the source location to detect which one the user used *)
 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr
@@ -49,3 +53,59 @@ Inductive WeakExpr :=
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 
+(*
+Fixpoint weakExprVarOccursFree (wvf:WeakExprVar)(we:WeakExpr) : bool :=
+  match we with
+  | WEVar   wv                           => if eqd_dec (wvf:CoreVar) (wv:CoreVar) then true else false
+  | WELit   lit                          => false
+  | WEApp   e1 e2                        => weakExprVarOccursFree wvf e1 || weakExprVarOccursFree wvf e2
+  | WETyApp e t                          => weakExprVarOccursFree wvf e
+  | WECoApp e co                         => weakExprVarOccursFree wvf e
+  | WENote  n e                          => weakExprVarOccursFree wvf e
+  | WELam   ev e                         => if eqd_dec (wvf:CoreVar) (ev:CoreVar) then false else weakExprVarOccursFree wvf e
+  | WETyLam tv e                         => weakExprVarOccursFree wvf e
+  | WECoLam cv e                         => weakExprVarOccursFree wvf e
+  | WECast  e co                         => weakExprVarOccursFree wvf e
+  | WEBrak  v wtv e t                    => weakExprVarOccursFree wvf e
+  | WEEsc   v wtv e t                    => weakExprVarOccursFree wvf e
+  | WECSP   v wtv e t                    => weakExprVarOccursFree wvf e
+  | WELet   v ebind ebody                => weakExprVarOccursFree wvf ebind
+                                            || if eqd_dec (wvf:CoreVar) (v:CoreVar) then false else weakExprVarOccursFree wvf ebody
+  | WECase  vs es tb tc tys alts         =>
+    if weakExprVarOccursFree wvf es
+      then true
+      else (fix weakExprVarOccursFreeBranches (alts:Tree ??(_)) : bool :=
+        match alts with
+          | T_Leaf None     => false
+          | T_Leaf (Some (_,_,_,v',e')) => 
+            if fold_left bor (map (fun v'':WeakExprVar => if eqd_dec (wvf:CoreVar) (v'':CoreVar) then true else false ) v') false
+              then false
+              else weakExprVarOccursFree wvf e'
+          | T_Branch b1 b2  => weakExprVarOccursFreeBranches b1 ||
+            weakExprVarOccursFreeBranches b2
+        end) alts
+  | WELetRec mlr e                       => false
+  end.
+
+(* some very simple-minded cleanups to produce "prettier" expressions *)
+Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr :=
+  match me with
+  | WEVar   wv                           => WEVar wv
+  | WELit   lit                          => WELit lit
+  | WEApp   e1 e2                        => WEApp        (simplifyWeakExpr e1) (simplifyWeakExpr e2)
+  | WETyApp e t                          => WETyApp      (simplifyWeakExpr e ) t
+  | WECoApp e co                         => CoreEApp     (simplifyWeakExpr e ) co
+  | WENote  n e                          => CoreENote n  (simplifyWeakExpr e )
+  | WELam   ev e                         => CoreELam  ev (simplifyWeakExpr e )
+  | WETyLam tv e                         => CoreELam  tv (simplifyWeakExpr e )
+  | WECoLam cv e                         => CoreELam  cv (simplifyWeakExpr e )
+  | WECast  e co                         => CoreECast    (simplifyWeakExpr e ) co
+  | WEBrak  v wtv e t                    => WEBrak v wtv (simplifyWeakExpr e ) t
+  | WEEsc   v wtv e t                    => WEEsc  v wtv (simplifyWeakExpr e ) t
+  | WECSP   v wtv e t                    => WECSP  v wtv (simplifyWeakExpr e ) t
+  | WELet   v ebind ebody                => WELet  v (simplifyWeakExpr ebind) (simplifyWeakExpr ebody)
+  | WECase  vs es tb tc tys alts         => WECase vs es tb tc tys (* FIXME alts *)
+  (* un-letrec-ify multi branch letrecs *)
+  | WELetRec mlr e                       => WELetRec mlr (simplifyWeakExpr e )
+  end.
+*)