Top.Translation

Require Import Helpers.
Require Import Library.
(*
*** Warning: in file Predefs.v,
    required library Definitions matches several files in path
    (found Definitions.v in ../lambda2Gmu and ../../dot-calculus/src/extensions/paths; used the latter)
 *)

Definition type_map := nat → nat × typ_label.
Definition empty_map : type_map := fun x ⇒ (x, GenT).
Definition skip1 : type_map → type_map :=
  fun f x ⇒
    let (n, l) := f x in
    (1 + n, l).
Definition open1 : type_map → typ_label → type_map :=
  fun f l x ⇒
    match x with
    | 0 ⇒ (0, l)
    | S n ⇒
      let (n', l') := f n in
      (n' + 1, l')
    end.

Fixpoint translateType
         (T : Source.typ)
         (ty_map : type_map)
         {struct T}
  : Target.typ :=
  match T with
  | typ_bvar J ⇒
    let (n, l) := ty_map J in
    (ref n) ↓ l
  | typ_fvar X ⇒
    typ_path (pvar X) GenT
  | typ_unit ⇒
    (pvar lib) ↓ Unit
  | T1 ** T2 ⇒
    let T1' := translateType T1 ty_map in
    let T2' := translateType T2 ty_map in
    TupleT T1' T2'
  | T1 ==> T2 ⇒
    let T1' := translateType T1 ty_map in
    let T2' := translateType T2 (skip1 ty_map) in
    typ_all T1' T2'
  | Source.typ_all T ⇒
    let T1 := translateType T (open1 ty_map GenT) in
    typ_all GenArgT T1
  | typ_gadt Ts g ⇒
    let Ts' := List.map (fun t ⇒ translateType t ty_map) Ts in
    let base := pvar env ↓ (GN g) in
    let res :=
        List.fold_left
          (fun acc T ⇒ match acc with
                     | (i, rest) ⇒
                       (
                         1+i,
                         (rest ∧ typ_rcd { Ai i == T })
                       )
                     end)
          Ts'
          (1, base) in
    snd res
  end.

Definition translateTyp0 (T : Source.typ) : Target.typ := translateType T empty_map.

Definition translateEnvTypOpened (Σ : Source.GADTEnv) : Target.typ.
Admitted.

(* Definition translateEnvTyp (Σ : Source.GADTEnv) : Target.typ := *)
(*   Target.typ_bnd ( *)
(*       Target.subst_typ env (p_sel (avar_b 0) 0) *)
(*     ). *)

Definition translateEnvTrm (Σ : Source.GADTEnv) : Target.trm.
Admitted.

Definition TypedTrm := SourceAnnot.trm.

Fixpoint translateTerm (Σ : Source.GADTEnv) (typenv : list Target.typ) (trmenv : list Target.trm) (t : TypedTrm) : Target.trm.
Admitted.

Definition translateProgram (Σ : Source.GADTEnv) (main : TypedTrm) : Target.trm.
Admitted.