Library Firstorder
Require Omega.
Require Import Arith.
Require Import Setoid.
Require Import Wf.
Require Import Wf_nat.
Require Import Coqlib.
Open Scope nat_scope.
Require Import Uncurry.
Inductive arity : Set :=
| Unknown : arity
| Known: nat -> arity.
Definition arity_env : Set := list arity.
Specification of first-order uncurrying
Inductive ztransl: arity_env -> uterm -> nterm -> Prop :=
| ztransl_var_1: forall e n,
nth_error e n = Some Unknown \/ nth_error e n = Some (Known 0) ->
ztransl e (UVar n) (NVar n)
| ztransl_var_2: forall ar e n,
nth_error e n = Some (Known ar) ->
ztransl e (UVar n) (NApp (curry (S ar)) (NVar n :: nil))
| ztransl_const: forall e n,
ztransl e (UConst n) (NConst n)
| ztransl_fun: forall e a a',
ztransl (Unknown :: e) a a' ->
ztransl e (UFun a) (NFun 1 a')
| ztransl_app: forall e a b a' b',
ztransl e a a' ->
ztransl e b b' ->
ztransl e (UApp a b) (NApp a' (b' :: nil))
| ztransl_app_known: forall e n ar bl bl',
nth_error e n = Some (Known ar) ->
ztransl_list e bl bl' ->
List.length bl = S ar ->
ztransl e (UApp_n (UVar n) bl) (NApp (NVar n) bl')
| ztransl_let_1: forall e a a' b b',
ztransl e a a' ->
ztransl (Unknown :: e) b b' ->
ztransl e (ULet a b) (NLet a' b')
| ztransl_let_2: forall e n a a' b b',
ztransl (replicate Unknown (S n) ++ e) a a' ->
ztransl (Known n :: e) b b' ->
ztransl e (ULet (UFun_n (S n) a) b) (NLet (NFun (S n) a') b')
| ztransl_letrec: forall e n a a' b b',
ztransl (replicate Unknown (S n) ++ Known n :: e) a a' ->
ztransl (Known n :: e) b b' ->
ztransl e (ULetrec (UFun_n n a) b) (NLetrec (S n) a' b')
with ztransl_list: arity_env -> list uterm -> list nterm -> Prop :=
| ztransl_nil: forall e,
ztransl_list e nil nil
| ztransl_cons: forall e a1 al b1 bl,
ztransl e a1 b1 -> ztransl_list e al bl ->
ztransl_list e (a1 :: al) (b1 :: bl).
Scheme ztransl_ind2 := Minimality for ztransl Sort Prop
with ztransl_list_ind2 := Minimality for ztransl_list Sort Prop.
Connections between arity information and representation types
Definition type_of_arity (a: arity) : type :=
match a with
| Unknown => T
| Known n => F (replicate T (S n)) T
end.
Definition typenv_of_arityenv (e: arity_env) : typenv :=
List.map type_of_arity e.
Remark subtype_curry_type:
forall n, subtype (curry_type (replicate T n) T) T.
Proof.
induction n; simpl.
constructor.
apply subtype_trans with (F (T :: nil) T).
apply subtype_fun. constructor. constructor. constructor.
auto.
constructor.
Qed.
First-order uncurrying is an instance of the generic
higher-order uncurrying transformation.
Lemma ztransl_transl:
forall e u t,
ztransl e u t ->
transl (typenv_of_arityenv e) u T t.
Proof.
apply (ztransl_ind2
(fun e u t => transl (typenv_of_arityenv e) u T t)
(fun e ul tl => transl_list (typenv_of_arityenv e) ul (replicate T (length ul)) tl));
intros.
destruct H.
constructor. unfold typenv_of_arityenv.
rewrite list_map_nth. rewrite H. auto.
apply transl_coerce with (F (T :: nil) T) (NVar n).
constructor. unfold typenv_of_arityenv.
rewrite list_map_nth. rewrite H. auto.
apply coerce_sub. constructor.
apply transl_coerce with (t := F (replicate T (S ar)) T) (b := NVar n).
constructor. unfold typenv_of_arityenv.
rewrite list_map_nth. rewrite H. auto.
eapply coerce_trans. apply coerce_curry.
simpl; congruence.
rewrite replicate_length. apply coerce_sub. apply subtype_curry_type.
constructor.
apply transl_coerce with (t := F (T :: nil) T) (b := NFun (length (T::nil)) a').
change (UFun a) with (UFun_n (length (T::nil)) a). apply transl_fun. congruence.
assumption.
apply coerce_sub. constructor.
apply transl_appT. auto. auto.
eapply transl_app with (targs := replicate T (length bl)).
rewrite H2. simpl; congruence.
rewrite H2. constructor. unfold typenv_of_arityenv.
rewrite list_map_nth. rewrite H. simpl. reflexivity.
auto.
eapply transl_let; eauto.
apply transl_let with (t1 := F (replicate T (S n)) T).
set (targs := replicate T (S n)).
replace (S n) with (length targs). apply transl_fun.
unfold targs; simpl; congruence.
unfold targs. rewrite replicate_rev. unfold typenv_of_arityenv in H0.
rewrite map_app in H0. rewrite replicate_map in H0. auto.
unfold targs. apply replicate_length.
auto.
set (targs := replicate T n).
assert (length targs = n). unfold targs; apply replicate_length.
rewrite <- H3. apply transl_letrec with (targ1 := T) (tres := T).
unfold typenv_of_arityenv in H0. simpl in H0. rewrite map_app in H0.
rewrite replicate_map in H0. simpl in H0.
replace (rev (T :: targs)) with (T :: targs). assumption.
change (T :: targs) with (replicate T (S n)). rewrite replicate_rev; auto.
assumption.
constructor.
simpl. constructor; auto.
Qed.
Semantic preservation follows as a corollary
Lemma ztransl_correct:
forall u t n c,
ztransl nil u t ->
ueval n nil u (UC c) ->
neval nil t (NC c).
Proof.
intros. eapply transl_correct; eauto.
change (@nil type) with (typenv_of_arityenv nil).
apply ztransl_transl; auto.
Qed.