projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
reorganize HaskProof files
[coq-hetmet.git]
/
src
/
HaskWeakToStrong.v
diff --git
a/src/HaskWeakToStrong.v
b/src/HaskWeakToStrong.v
index
b2521e3
..
6d4bf16
100644
(file)
--- a/
src/HaskWeakToStrong.v
+++ b/
src/HaskWeakToStrong.v
@@
-19,9
+19,6
@@
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskCoreVars.
Require Import HaskStrong.
Require Import HaskCoreVars.
-(* can remove *)
-Require Import HaskStrongToWeak.
-
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
@@
-513,7
+510,14
@@
Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
| T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
end.
| T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
end.
-(*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
+Definition checkDistinct :
+ forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
+ intros.
+ set (distinct_decidable lv) as q.
+ destruct q.
+ exact (OK d).
+ exact (Error "checkDistinct failed").
+ Defined.
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
@@
-647,8
+651,9
@@
Definition weakExprToStrongExpr : forall
OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
end) rb
in binds >>= fun binds' =>
OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
end) rb
in binds >>= fun binds' =>
+ checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
- OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+ OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
| WECase vscrut escrut tbranches tc avars alts =>
weakTypeOfWeakExpr escrut >>= fun tscrut =>
| WECase vscrut escrut tbranches tc avars alts =>
weakTypeOfWeakExpr escrut >>= fun tscrut =>
@@
-703,6
+708,8
@@
Definition weakExprToStrongExpr : forall
destruct (ξ c).
simpl.
apply e1.
destruct (ξ c).
simpl.
apply e1.
+ rewrite mapleaves.
+ apply rb_distinct.
destruct case_pf.
set (distinct_decidable (vec2list exprvars')) as dec.
destruct case_pf.
set (distinct_decidable (vec2list exprvars')) as dec.