projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
HaskProof: make the succedent level part of the judgment
[coq-hetmet.git]
/
src
/
HaskCoreToWeak.v
diff --git
a/src/HaskCoreToWeak.v
b/src/HaskCoreToWeak.v
index
1be33fd
..
ccd4973
100644
(file)
--- a/
src/HaskCoreToWeak.v
+++ b/
src/HaskCoreToWeak.v
@@
-4,10
+4,11
@@
Generalizable All Variables.
Require Import Preamble.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Coq.Lists.List.
Require Import Coq.Lists.List.
+Require Import General.
Require Import HaskKinds.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
@@
-28,6
+29,12
@@
Variable hetmet_brak_name : CoreName. Extract Inlined Constant he
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
+ split_list lwt (length (fst (tyFunKind tf))) >>=
+ fun argsrest =>
+ let (args,rest) := argsrest in
+ OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
+
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
match ct with
| TyVarTy cv => match coreVarToWeakVar cv with
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
match ct with
| TyVarTy cv => match coreVarToWeakVar cv with
@@
-44,7
+51,7
@@
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
| a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
end) lct)
in match tyConOrTyFun tc_ with
| a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
end) lct)
in match tyConOrTyFun tc_ with
- | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
+ | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
| inl tc => if eqd_dec tc ModalBoxTyCon
then match lct with
| ((TyVarTy ec)::tbody::nil) =>
| inl tc => if eqd_dec tc ModalBoxTyCon
then match lct with
| ((TyVarTy ec)::tbody::nil) =>
@@
-53,7
+60,7
@@
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
- | _ => Error ("mis-applied modal box tycon: " +++ ct)
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
@@
-68,9
+75,11
@@
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
coreTypeToWeakType' t2 >>= fun t2' =>
OK (WAppTy (WAppTy WFunTyCon t1') t2')
| ForAllTy cv t => match coreVarToWeakVar cv with
coreTypeToWeakType' t2 >>= fun t2' =>
OK (WAppTy (WAppTy WFunTyCon t1') t2')
| ForAllTy cv t => match coreVarToWeakVar cv with
- | WExprVar _ => Error "encountered expression variable in a type"
+ | WExprVar _ => Error "encountered expression variable in a type abstraction"
| WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
| WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
- | WCoerVar _ => Error "encountered coercion variable in a type"
+ | WCoerVar (weakCoerVar v t1' t2') =>
+ coreTypeToWeakType' t >>= fun t3' =>
+ OK (WCoFunTy t1' t2' t3')
end
| PredTy (ClassP cl lct) => ((fix rec tl := match tl with
| nil => OK nil
end
| PredTy (ClassP cl lct) => ((fix rec tl := match tl with
| nil => OK nil
@@
-81,40
+90,50
@@
Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
| PredTy (EqPred _ _) => Error "hit a bare EqPred"
end.
| PredTy (EqPred _ _) => Error "hit a bare EqPred"
end.
-Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
+Definition coreTypeToWeakType t :=
+ addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
(* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_brak_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_brak_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
- | WTypeVar tv => Some (v,tv,tbody)
| WCoerVar _ => None
| WCoerVar _ => None
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
end else None
| _ => None
end.
end else None
| _ => None
end.
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_esc_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_esc_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
- | WTypeVar tv => Some (v,tv,tbody)
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
| WCoerVar _ => None
end else None
| _ => None
end.
| WCoerVar _ => None
end else None
| _ => None
end.
-Definition isCSP (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_csp_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
=> if coreName_eq hetmet_csp_name (coreVarCoreName v) then
match coreVarToWeakVar ec with
| WExprVar _ => None
- | WTypeVar tv => Some (v,tv,tbody)
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
| WCoerVar _ => None
end else None
| _ => None
| WCoerVar _ => None
end else None
| _ => None
@@
-125,8
+144,8
@@
Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
- | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
- | _ => Error ("expectTyConApp encountered " +++ wt)
+ | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+ | _ => Error ("expectTyConApp encountered " +++ toString wt)
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
@@
-206,24
+225,23
@@
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
- coreExprToWeakExpr e >>= fun e' =>
expectTyConApp te' nil >>= fun tca =>
expectTyConApp te' nil >>= fun tca =>
- let (tc,lt) := tca in
- ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
- : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
+ let (tc,lt) := tca:(TyCon * list WeakType) in
+ ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
+ : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match branches with
| nil => OK nil
| (mkTriple alt vars e)::rest =>
mkBranches rest >>= fun rest' =>
coreExprToWeakExpr e >>= fun e' =>
match alt with
match branches with
| nil => OK nil
| (mkTriple alt vars e)::rest =>
mkBranches rest >>= fun rest' =>
coreExprToWeakExpr e >>= fun e' =>
match alt with
- | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest')
- | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest')
+ | DEFAULT => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
+ | LitAlt lit => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
| DataAlt dc => let vars := map coreVarToWeakVar vars in
| DataAlt dc => let vars := map coreVarToWeakVar vars in
- OK (((DataAlt dc),
- (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
- (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+ OK (((WeakDataAlt dc),
+ (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+ (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
e')::rest')
end
end) alts)
e')::rest')
end
end) alts)