projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet
[coq-hetmet.git]
/
src
/
HaskCoreToWeak.v
diff --git
a/src/HaskCoreToWeak.v
b/src/HaskCoreToWeak.v
index
78223cf
..
ccd4973
100644
(file)
--- a/
src/HaskCoreToWeak.v
+++ b/
src/HaskCoreToWeak.v
@@
-29,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
@@
-45,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) =>