Library Firstorder

Application to first-order uncurrying

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

Definition typenv_of_arityenv (e: arity_env) : typenv := type_of_arity e.

Remark subtype_curry_type:
  forall n, subtype (curry_type (replicate T n) T) T.
  induction n; simpl.
  apply subtype_trans with (F (T :: nil) T).
  apply subtype_fun. constructor. constructor. constructor.

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.
  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));

  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.


  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.
  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.

  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.

  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.


  simpl. constructor; auto.

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).
  intros. eapply transl_correct; eauto.
  change (@nil type) with (typenv_of_arityenv nil).
  apply ztransl_transl; auto.