Library CatSem.RPCF.RPCF_rep

Require Export CatSem.CAT.retype_functor_po.
Require Export CatSem.CAT.rmonad_gen_type_po.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Transparent Obligations.
Unset Automatic Introduction.

Notation "a 'x' b" := (product a b) (at level 30).
Notation "M [ z ]" := (FIB_RMOD _ z M) (at level 35).
Notation "'d' M // s" := (DER_RMOD _ _ s M) (at level 25).
Notation "'*'" := (Term (C:=RMOD _ Ord)).
Notation "y [* := z ]":= (Rsubstar z _ y)(at level 55).

Section PCF_rep.

Variable Sorts : Type.
Variable P : RMonad (IDelta Sorts).

Variable Arrow : Sorts -> Sorts -> Sorts.
Variable Bool : Sorts.
Variable Nat : Sorts.
Notation "a ~~> b" := (Arrow a b) (at level 60, right associativity).

Class PCFPO_rep_struct := {
  app : forall u v, (P[u ~~> v]) x (P[u]) ---> P[v];
  abs : forall u v, (d P // u)[v] ---> P[u ~~> v];
  rec : forall t, P[t ~~> t] ---> P[t];
  tttt : * ---> P[Bool];
  ffff : * ---> P[Bool];
  nats : forall m:nat, * ---> P[Nat];
  Succ : * ---> P[Nat ~~> Nat];
  Pred : * ---> P[Nat ~~> Nat];
  Zero : * ---> P[Nat ~~> Bool];
  CondN: * ---> P[Bool ~~> Nat ~~> Nat ~~> Nat];
  CondB: * ---> P[Bool ~~> Bool ~~> Bool ~~> Bool];
  bottom: forall t, * ---> P[t];

  beta_red : forall r s V y z,
        app r s V (abs r s V y, z) << y[*:= z] ;

  CondN_t: forall V n m,
     app _ _ _ (app _ _ _
          (app _ _ _ (CondN V tt, tttt _ tt),
                       n), m) << n ;
  
  CondN_f: forall V n m,
     app _ _ _ (app _ _ _
          (app _ _ _ (CondN V tt, ffff _ tt),
                       n), m) << m ;
 
  CondB_t: forall V u v,
     app _ _ _ (app _ _ _
          (app _ _ _ (CondB V tt, tttt _ tt),
                        u), v) << u ;
  
  CondB_f: forall V u v,
     app _ _ _ (app _ _ _
          (app _ _ _ (CondB V tt, ffff _ tt),
                       u), v) << v ;
  
  Succ_red: forall V n,
     app _ _ _ (Succ V tt, nats n _ tt) << nats (S n) _ tt ;

  Zero_t: forall V,
     app _ _ _ (Zero V tt, nats 0 _ tt) << tttt _ tt ;

  Zero_f: forall V n,
     app _ _ _ (Zero V tt, nats (S n) _ tt) << ffff _ tt ;

  Pred_Succ: forall V n,
     app _ _ _ (Pred V tt, app _ _ _ (Succ V tt, nats n _ tt)) <<
             nats n _ tt;
   
  Pred_Z: forall V,
     app _ _ _ (Pred V tt, nats 0 _ tt) << nats 0 _ tt ;
 
  Rec_A: forall V t g,
     rec _ _ g << app t t V (g, rec _ _ g)
 }.

End PCF_rep.

Record PCFPO_rep := {
  Sorts : Type;
  Arrow : Sorts -> Sorts -> Sorts;
  Bool : Sorts ;
  Nat : Sorts ;
  pcf_rep_monad :> RMonad (IDelta Sorts);


  pcf_rep_struct :> PCFPO_rep_struct pcf_rep_monad Arrow Bool Nat
               
}.

Existing Instance pcf_rep_struct.
Notation "a ~~> b" := (Arrow a b)
         (at level 60, right associativity).