end
end.
- Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
- intros.
- induction Γ.
- apply INil.
- apply ICons; auto.
- apply tt.
- Defined.
-
- Fixpoint grab (n:nat) {T} (l:list T) : T :=
- match l with
- | nil => Prelude_error "grab failed"
- | h::t => match n with
- | 0 => h
- | S n' => grab n' t
- end
- end.
+ Fixpoint take_trustme {Γ}
+ (n:nat)
+ (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
+ : list (HaskType Γ ★) :=
- Fixpoint count' (n:nat)(ln:list nat) : list nat :=
match n with
- | 0 => ln
- | S n' => count' n' (n'::ln)
+ | 0 => nil
+ | S n' => (fun TV ite => match l TV ite with
+ | nil => Prelude_error "impossible"
+ | a::b => a
+ end)
+ ::
+ take_trustme n' (fun TV ite => match l TV ite with
+ | nil => Prelude_error "impossible"
+ | a::b => b
+ end)
end.
-
- Definition count (n:nat) := count' n nil.
-
- Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
- map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
-
- Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
- (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
+
+ Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
+ unleaves
+ (take_trustme
+ (count_arg_types (ht _ (ite_unit _)))
+ (fun TV ite => take_arg_types (ht TV ite))).
Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
fun TV ite => drop_arg_types (ht TV ite).
Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
intros.
- unfold take_arg_types_as_tree; simpl.
- unfold rebundle at 1.
+ unfold take_arg_types_as_tree at 1.
+ simpl.
admit.
Qed.
left; auto.
Defined.
+ Opaque take_arg_types_as_tree.
Definition skolemize_proof :
forall {h}{c},
ND Rule h c ->
apply RGlobal.
destruct case_RLam.
- simpl.
destruct lev.
- apply nd_rule.
- apply SFlat.
- apply RLam.
+ apply nd_rule.
+ apply SFlat.
+ simpl.
+ apply RLam.
+ simpl.
rewrite take_works.
rewrite drop_works.
apply nd_rule.
- apply SFlat.
- apply RArrange.
- apply RCossa.
+ apply SFlat.
+ apply RArrange.
+ apply RCossa.
destruct case_RCast.
simpl.
simpl.
apply (Prelude_error "CASE: BIG FIXME").
Defined.
+ Transparent take_arg_types_as_tree.
End HaskSkolemizer.