clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

[coq-hetmet.git] / src / HaskWeakToCore.v

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 7d0fac4..290d634 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -8,33 +8,59 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.

+Require Import HaskCoreToWeak.

 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 

-Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
-  Extract Inlined Constant mkCoreLet => "sortAlts".
+Variable sortAlts  : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@triple CoreAltCon a b).
+  Extract Inlined Constant sortAlts => "sortAlts".

   Implicit Arguments sortAlts [[a][b]].
 
   Implicit Arguments sortAlts [[a][b]].
 

-Variable trustMeCoercion           : CoreCoercion.
-  Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
+Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
+    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".

 
 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
 
 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 

-Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-   fun _ => trustMeCoercion.
+Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon :=
+  match wa with
+  | WeakDataAlt cdc => DataAlt cdc
+  | WeakLitAlt  lit => LitAlt lit
+  | WeakDEFAULT     => DEFAULT
+  end.
+
+Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
+  match wt with
+    | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
+    | WAppTy  t1 t2                   => match (weakTypeToCoreType t1) with
+                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
+                                           | t1'             => AppTy t1' (weakTypeToCoreType t2)
+                                         end
+    | WTyCon    tc                    => TyConApp tc nil
+    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType lt)
+    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType lt))
+    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType ty))
+    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
+    | WFunTyCon                       => TyConApp ArrowTyCon nil
+    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
+    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
+                                            (weakTypeToCoreType t3)
+  end.

 
 

+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).

 
 

-  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=

   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit

@@ -59,17 +85,23 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
                                                      (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)
                                                      (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)

+  | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)

   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)

-  | WECase  vscrut e tbranches tc types alts  =>
-                                            CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
+  | WECase  vscrut escrut tbranches tc types alts  =>
+                                            CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)

                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 

-                                                  ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+                                                  ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>
                                                 match alts with
                                                   | T_Leaf None              => nil
                                                   | T_Branch b1 b2           => app (mkCaseBranches b1) (mkCaseBranches b2)
                                                   | T_Leaf (Some (ac,tvars,cvars,evars,e)) =>

-                                                    (mkTriple (ac:AltCon)
+                                                    (mkTriple (weakAltConToCoreAltCon ac)

                                                       (app (app 
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
                                                       (app (app 
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))

@@ -87,6 +119,10 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
                                                (weakExprToCoreExpr e)
   end.
 
                                                (weakExprToCoreExpr e)
   end.
 

+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).

 
 

+Instance weakExprToString : ToString WeakExpr  :=
+  { toString := fun we => toString (weakExprToCoreExpr we) }.