Rec.Extras.sysf_print

From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Framework.graded Framework.sysf_types Framework.sysf_terms.
Set Implicit Arguments.
Unset Strict Implicit.

Local Ltac asimpl :=
  repeat progress (cbn; fsimpl; gsimpl; ty_simpl; vt_simpl).

Definition id := nat.

Inductive nty :=
| nvar : id -> nty
| narr : nty -> nty -> nty
| nall : id -> nty -> nty.
Definition printer := id -> nty * id.

Notation "'∀' x .. y , p" := (nall x .. (nall y p) ..)
  (at level 200, right associativity,
   format "'[' '∀' '/ ' x .. y , '/ ' p ']'").
Notation "A → B" := (narr A B) (at level 30, right associativity).
Coercion nvar : id >-> nty.

Definition print_smodel : Ty.smodel id printer := Ty.SModel
  (fun x f => (nvar x, f))
  (fun ps pt f =>
     let: (ns, f') := ps f in
     let: (nt, f'') := pt f' in
     (narr ns nt, f''))
  (fun F f =>
     let: (nb, f') := F f f.+1 in
     (nall f nb, f')).

Definition print (A : ty 0) : nty :=
  (Ty.seval print_smodel null A 0).1.

Definition test : ty 0 :=
  Ty.all (Ty.all (Ty.arr (Ty.var bound) (Ty.all (Ty.arr (Ty.var bound) (Ty.arr (Ty.var (shift bound)) (Ty.var (shift (shift bound)))))))).

Compute print test.