- Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
- FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
- intros.
- set (fresh_lemma' Γ Σ [] [] ξ0 (refl_equal _)) as q.
- refine (q >>>= fun q' => return _).
- apply FreshMon.
- clear q.
- destruct q' as [varstypes [pf1 pf2]].
- exists (mapOptionTree (@fst _ _) varstypes).
- exists (update_ξ ξ0 (leaves varstypes)).
- symmetry; auto.
- Defined.
-
- Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
- refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
- match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
- | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RCanL t a => let case_RCanL := tt in _
- | RCanR t a => let case_RCanR := tt in _
- | RuCanL t a => let case_RuCanL := tt in _
- | RuCanR t a => let case_RuCanR := tt in _
- | RAssoc t a b c => let case_RAssoc := tt in _
- | RCossa t a b c => let case_RCossa := tt in _
- | RExch t a b => let case_RExch := tt in _
- | RWeak t a => let case_RWeak := tt in _
- | RCont t a => let case_RCont := tt in _
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+
+ Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t
+ .
+ intros Γ Δ.
+ refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t ->
+ ujudg2exprType Γ ξ Δ C t
+ with
+ | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RId a => let case_RId := tt in _
+ | RCanL a => let case_RCanL := tt in _
+ | RCanR a => let case_RCanR := tt in _
+ | RuCanL a => let case_RuCanL := tt in _
+ | RuCanR a => let case_RuCanR := tt in _
+ | RAssoc a b c => let case_RAssoc := tt in _
+ | RCossa a b c => let case_RCossa := tt in _
+ | RExch a b => let case_RExch := tt in _
+ | RWeak a => let case_RWeak := tt in _
+ | RCont a => let case_RCont := tt in _
+ | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)