LogRel.Checkers.Functions: conversion and type-checker implementation.

From Coq Require Import Nat Lia.
From Equations Require Import Equations.
From PartialFun Require Import Monad PartialFun MonadExn.
From LogRel Require Import Utils BasicAst AutoSubst.Extra Context NormalForms.

Import MonadNotations.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.

Definition callTypesFactory I (F : I -> Type) (f : forall i, F i) (pfuns : forall (i :I), PFun (f i)) : CallTypes I := {|
  ct_src i := psrc (f i) ;
  ct_tgt i := ptgt (f i) ;
|}.

#[program]
Definition callablePropsFactory I (F : I -> Type) (f : forall i, F i) (pfuns : forall (i :I), PFun (f i))
  : CallableProps (callTypesFactory I F f pfuns) := {|
  cp_graph i := pgraph (f i) ;
  cp_fueled i := pfueled (f i) ;
  cp_def i := pdef (f i)
|}.
Next Obligation. intros. eapply pgraph_fun. all: eassumption. Qed.
Next Obligation. intros; now eapply pfueled_graph. Qed.
Next Obligation. intros; now eapply pdef_graph. Qed.

#[export]Instance CallEmpty : CallTypes False | 5 :=
  callTypesFactory False
        (False_rect _)
        (fun bot => match bot return False_rect _ bot with end)
        (fun bot => match bot return PFun@{Set Set Set} _ with end).

#[export]Instance CallablePropsEmpty : CallableProps CallEmpty | 5 :=
  callablePropsFactory False
    (False_rect _)
    (fun bot => match bot return False_rect _ bot with end)
    (fun bot => match bot return PFun@{Set Set Set} _ with end).

Inductive Sing {F} (f : F) : Set := mkSing.
Inductive Duo {F1 F2} (f1 : F1) (f2 : F2) := mkLeft | mkRight.

Arguments mkLeft {_ _} _ {_}.
Arguments mkRight {_ _} {_} _.

#[global]
Instance callTypesSing {F} (f : F) `{PFun F f} : CallTypes (Sing f) :=
  callTypesFactory _ (fun _ => F) (fun _ => f) (fun _ => _).

#[global]
Instance callablePropsSing {F} (f : F) `{PFun F f} : CallableProps (callTypesSing f) :=
  callablePropsFactory _ (fun _ => F) (fun _ => f) (fun _ => _).

#[global]
Instance callTypesDuo {F1 F2} (f1 : F1) (f2 : F2) `{PFun F1 f1, PFun F2 f2} : CallTypes (Duo f1 f2) :=
  let F := fun x : Duo f1 f2 => match x with mkLeft _ => F1 | mkRight _ => F2 end in
  let f := fun x : Duo f1 f2 => match x as x return F x with
                                | mkLeft _ => f1 | mkRight _ => f2 end in
  let pfun := fun x : Duo f1 f2 => match x as x return PFun (f x) with
                                | mkLeft _ => _ | mkRight _ => _ end in
  callTypesFactory _ F f pfun.

#[global]
Instance callablePropsDuo {F1 F2} (f1 : F1) (f2 : F2) `{PFun F1 f1, PFun F2 f2} : CallableProps (callTypesDuo f1 f2) :=
  let F := fun x : Duo f1 f2 => match x with mkLeft _ => F1 | mkRight _ => F2 end in
  let f := fun x : Duo f1 f2 => match x as x return F x with
                                | mkLeft _ => f1 | mkRight _ => f2 end in
  let pfun := fun x : Duo f1 f2 => match x as x return PFun (f x) with
                                | mkLeft _ => _ | mkRight _ => _ end in
  callablePropsFactory _ F f pfun.

Definition call_single {F}
  (f : F) `{PFun F f} {A B} := ext_call (mkSing f) (A:=A) (B:=B).

(* The combinator rec throws in a return branch with a type 
  necessarily convertible to the exception errors type, but the syntactic 
  mismatch between the 2 types prevents `rec_graph` from `apply`ing.
  This tactic fixes the type in the return branch to what's expected
  syntactically. *)
  Ltac patch_rec_ret :=
    try (unfold rec;
    match goal with
    | |- orec_graph _ (_rec _ (fun _ : ?Bx => _)) ?hBa =>
      let Ba := type of hBa in change Bx with Ba
    end).

#[global]
Obligation Tactic := idtac.

Definition ok {M} `{Monad M} : M unit := ret tt.

Inductive errors : Type :=
  | variable_not_in_context : errors
  | head_mismatch : errors
  | variable_mismatch : errors
  | destructor_mismatch : errors
  | conv_error : errors
  | type_error : errors.

Section Views.

  Variant tm_view1 : term -> Type :=
    | tm_view1_type {t} : ty_entry t -> tm_view1 t
    | tm_view1_fun A t : tm_view1 (tLambda A t)
    | tm_view1_rel n : tm_view1 (tRel n)
    | tm_view1_nat {t} : nat_entry t -> tm_view1 t
    | tm_view1_sig A B a b : tm_view1 (tPair A B a b)
    | tm_view1_id A x : tm_view1 (tRefl A x)
    | tm_view1_dest t (s : dest_entry) : tm_view1 (zip1 t s).

  Definition build_tm_view1 t : tm_view1 t :=
    match t with
    | tRel n => tm_view1_rel n
    | tSort s => tm_view1_type (eSort s)
    | tProd A B => tm_view1_type (eProd A B)
    | tLambda A t => tm_view1_fun A t
    | tApp t u => tm_view1_dest t (eApp u)
    | tNat => tm_view1_type (eNat)
    | tZero => tm_view1_nat (eZero)
    | tSucc t => tm_view1_nat (eSucc t)
    | tNatElim P hs hz t => tm_view1_dest t (eNatElim P hs hz)
    | tEmpty => tm_view1_type (eEmpty)
    | tEmptyElim P t => tm_view1_dest t (eEmptyElim P)
    | tSig A B => tm_view1_type (eSig A B)
    | tPair A B a b => tm_view1_sig A B a b
    | tFst t => tm_view1_dest t eFst
    | tSnd t => tm_view1_dest t eSnd
    | tId A x y => tm_view1_type (eId A x y)
    | tRefl A x => tm_view1_id A x
    | tIdElim A x P hr y e => tm_view1_dest e (eIdElim A x P hr y)
    end.

  Variant ne_view1 : term -> Type :=
    | ne_view1_rel n : ne_view1 (tRel n)
    | ne_view1_dest t s : ne_view1 (zip1 t s).

  Variant nf_view1 : term -> Type :=
    | nf_view1_type {t} : ty_entry t -> nf_view1 t
    | nf_view1_fun A t : nf_view1 (tLambda A t)
    | nf_view1_nat {t} : nat_entry t -> nf_view1 t
    | nf_view1_sig A B a b : nf_view1 (tPair A B a b)
    | nf_view1_id A x : nf_view1 (tRefl A x)
    | nf_view1_ne {t} : ne_view1 t -> nf_view1 t.

  Definition build_nf_view1 t : nf_view1 t :=
    match t with
    | tRel n => nf_view1_ne (ne_view1_rel n)
    | tSort s => nf_view1_type (eSort s)
    | tProd A B => nf_view1_type (eProd A B)
    | tLambda A t => nf_view1_fun A t
    | tApp t u => nf_view1_ne (ne_view1_dest t (eApp u))
    | tNat => nf_view1_type (eNat)
    | tZero => nf_view1_nat (eZero)
    | tSucc t => nf_view1_nat (eSucc t)
    | tNatElim P hs hz t => nf_view1_ne (ne_view1_dest t (eNatElim P hs hz))
    | tEmpty => nf_view1_type (eEmpty)
    | tEmptyElim P t => nf_view1_ne (ne_view1_dest t (eEmptyElim P))
    | tSig A B => nf_view1_type (eSig A B)
    | tPair A B a b => nf_view1_sig A B a b
    | tFst t => nf_view1_ne (ne_view1_dest t eFst)
    | tSnd t => nf_view1_ne (ne_view1_dest t eSnd)
    | tId A x y => nf_view1_type (eId A x y)
    | tRefl A x => nf_view1_id A x
    | tIdElim A x P hr y e => nf_view1_ne (ne_view1_dest e (eIdElim A x P hr y))
    end.

  Variant ty_view1 : term -> Type :=
    | ty_view1_ty {t} : ty_entry t -> ty_view1 t
    | ty_view1_small {t} : ne_view1 t -> ty_view1 t
    | ty_view1_anomaly {t} : ty_view1 t.

  Definition build_ty_view1 t : ty_view1 t :=
    match (build_nf_view1 t) with
    | nf_view1_type e => ty_view1_ty e
    | nf_view1_ne s => ty_view1_small s
    | nf_view1_fun _ _
    | nf_view1_nat _
    | nf_view1_sig _ _ _ _
    | nf_view1_id _ _ => ty_view1_anomaly
    end.

    Inductive nf_ty_view2 : term -> term -> Type :=
    | ty_sorts (s1 s2 : sort) : nf_ty_view2 (tSort s1) (tSort s2)
    | ty_prods (A A' B B' : term) :
        nf_ty_view2 (tProd A B) (tProd A' B')
    | ty_nats : nf_ty_view2 tNat tNat
    | ty_emptys : nf_ty_view2 tEmpty tEmpty
    | ty_sigs (A A' B B' : term) : nf_ty_view2 (tSig A B) (tSig A' B')
    | ty_ids A A' x x' y y' : nf_ty_view2 (tId A x y) (tId A' x' y')
    | ty_neutrals (n n' : term) : nf_ty_view2 n n'
    | ty_mismatch (t u : term) : nf_ty_view2 t u
    | ty_anomaly (t u : term) : nf_ty_view2 t u.

  Equations build_nf_ty_view2 (A A' : term) : nf_ty_view2 A A' :=
    build_nf_ty_view2 A A' with (build_ty_view1 A), (build_ty_view1 A') := {
      

      | ty_view1_ty (eSort s1), ty_view1_ty (eSort s2) :=
          ty_sorts s1 s2 ;
      | ty_view1_ty (eProd A B), ty_view1_ty (eProd A' B') :=
          ty_prods A A' B B' ;
      | ty_view1_ty eNat, ty_view1_ty eNat :=
          ty_nats;
      | ty_view1_ty eEmpty, ty_view1_ty eEmpty :=
          ty_emptys;
      | ty_view1_ty (eSig A B), ty_view1_ty (eSig A' B') :=
          ty_sigs A A' B B'
      | ty_view1_ty (eId A x y), ty_view1_ty (eId A' x' y') :=
          ty_ids A A' x x' y y'
      | ty_view1_small _, ty_view1_small _ :=
          ty_neutrals _ _ ;
      

      | ty_view1_ty _, ty_view1_ty _ :=
          ty_mismatch _ _ ;
      | ty_view1_small _, ty_view1_ty _ :=
          ty_mismatch _ _ ;
      | ty_view1_ty _, ty_view1_small _ :=
          ty_mismatch _ _ ;
      

      | ty_view1_anomaly,_ := ty_anomaly _ _ ;
      | _, ty_view1_anomaly := ty_anomaly _ _;
    }.

  Inductive nf_view3 : term -> term -> term -> Type :=
  | types {A A'} (s : sort) : nf_ty_view2 A A' -> nf_view3 (tSort s) A A'
  | functions A B t t' : nf_view3 (tProd A B) t t'
  | zeros : nf_view3 tNat tZero tZero
  | succs t t' : nf_view3 tNat (tSucc t) (tSucc t')
  | pairs A B t t' : nf_view3 (tSig A B) t t'
  | refls A x y A' x' A'' x'' : nf_view3 (tId A x y) (tRefl A' x') (tRefl A'' x'')
  | neutrals (A n n' : term) : nf_view3 A n n'
  | mismatch (A t u : term) : nf_view3 A t u
  | anomaly (A t u : term) : nf_view3 A t u.

  Equations build_nf_view3 T t t' : nf_view3 T t t' :=
    build_nf_view3 T t t' with (build_ty_view1 T) := {
    

    | ty_view1_ty (eSort s) := types s (build_nf_ty_view2 t t') ;
    

    | ty_view1_ty (eProd A B) := functions A B _ _ ;
    

    | ty_view1_ty eNat with (build_nf_view1 t), (build_nf_view1 t') :=
      {
        | nf_view1_nat eZero, nf_view1_nat eZero :=
          zeros ;
        | nf_view1_nat (eSucc u), nf_view1_nat (eSucc u') :=
          succs u u' ;
        | nf_view1_ne _, nf_view1_ne _ := neutrals _ _ _ ;
        | nf_view1_nat _, nf_view1_nat _ :=
            mismatch _ _ _ ;
        | nf_view1_ne _, nf_view1_nat _ :=
            mismatch _ _ _ ;
        | nf_view1_nat _, nf_view1_ne _ :=
            mismatch _ _ _ ;
        | _, _ := anomaly _ _ _ ;
      } ;
    

    | ty_view1_ty eEmpty with (build_nf_view1 t), (build_nf_view1 t') :=
    {
      | nf_view1_ne _, nf_view1_ne _ :=
        neutrals _ _ _ ;
      | _, _ := anomaly _ _ _ ;
    }
    

    | ty_view1_ty (eSig A B) := pairs A B _ _ ;
    

    | ty_view1_ty (eId A x y) with (build_nf_view1 t), (build_nf_view1 t') :=
      {
        | nf_view1_id A' x', nf_view1_id A'' x'' := refls A x y A' x' A'' x'' ;
        | nf_view1_ne _, nf_view1_ne _ := neutrals _ _ _ ;
        | nf_view1_ne _, nf_view1_id _ _ :=
            mismatch _ _ _ ;
        | nf_view1_id _ _, nf_view1_ne _ :=
            mismatch _ _ _ ;
        | _, _ := anomaly _ _ _ ;
      }
    

    | ty_view1_small _ with (build_nf_view1 t), (build_nf_view1 t') :=
      {
        | nf_view1_ne _, nf_view1_ne _ := neutrals _ _ _ ;
        | _, _ := anomaly _ _ _ ;
      }
    

    | ty_view1_anomaly := anomaly _ _ _ ;
    }.

  Inductive ne_view2 : term -> term -> Type :=
    | ne_rels (n n' : nat) : ne_view2 (tRel n) (tRel n')
    | ne_apps f u f' u' : ne_view2 (tApp f u) (tApp f' u')
    | ne_nats n P hz hs n' P' hz' hs' : ne_view2 (tNatElim P hz hs n) (tNatElim P' hz' hs' n')
    | ne_emptys n P n' P' : ne_view2 (tEmptyElim P n) (tEmptyElim P' n')
    | ne_fsts p p' : ne_view2 (tFst p) (tFst p')
    | ne_snds p p' : ne_view2 (tSnd p) (tSnd p')
    | ne_ids A x P hr y e A' x' P' hr' y' e' : ne_view2 (tIdElim A x P hr y e) (tIdElim A' x' P' hr' y' e')
    | ne_mismatch (t u : term) : ne_view2 t u
    | ne_anomaly (t u : term) : ne_view2 t u.

  Equations build_ne_view2 (t t' : term) : ne_view2 t t' :=
    build_ne_view2 t t' with (build_nf_view1 t), (build_nf_view1 t') := {
      | nf_view1_ne v, nf_view1_ne v' with v, v' := {
          | ne_view1_rel n, ne_view1_rel n' := ne_rels n n' ;
          | ne_view1_dest f (eApp u), ne_view1_dest f' (eApp u') := ne_apps f u f' u' ;
          | ne_view1_dest n (eNatElim P hz hs), ne_view1_dest n' (eNatElim P' hz' hs') :=
              ne_nats n P hz hs n' P' hz' hs' ;
          | ne_view1_dest n (eEmptyElim P), ne_view1_dest n' (eEmptyElim P') :=
              ne_emptys n P n' P' ;
          | ne_view1_dest p eFst, ne_view1_dest p' eFst :=
              ne_fsts p p' ;
          | ne_view1_dest p eSnd, ne_view1_dest p' eSnd :=
              ne_snds p p' ;
          | ne_view1_dest e (eIdElim A x P hr y), ne_view1_dest e' (eIdElim A' x' P' hr' y') :=
              ne_ids A x P hr y e A' x' P' hr' y' e' ;
          | _, _ := ne_mismatch _ _ ;
      }
      | _, _ := ne_anomaly _ _
    }.

  Inductive nf_view2 : term -> term -> Type :=
    | sorts2 (s1 s2 : sort) : nf_view2 (tSort s1) (tSort s2)
    | prods2 (A A' B B' : term) :
        nf_view2 (tProd A B) (tProd A' B')
    | nats2 : nf_view2 tNat tNat
    | emptys2 : nf_view2 tEmpty tEmpty
    | sigs2 (A A' B B' : term) : nf_view2 (tSig A B) (tSig A' B')
    | ids2 A A' x x' y y' : nf_view2 (tId A x y) (tId A' x' y')
    | lams2 A A' t t' : nf_view2 (tLambda A t) (tLambda A' t')
    | lam_ne2 A t n' : nf_view2 (tLambda A t) n'
    | ne_lam2 n A' t' : nf_view2 n (tLambda A' t')
    | zeros2 : nf_view2 tZero tZero
    | succs2 t t' : nf_view2 (tSucc t) (tSucc t')
    | pairs2 A A' B B' t t' u u' :
        nf_view2 (tPair A B t u) (tPair A' B' t' u')
    | pair_ne2 A B t u n' :
        nf_view2 (tPair A B t u) n'
    | ne_pair2 n A' B' t' u' :
        nf_view2 n (tPair A' B' t' u')
    | refls2 A A' x x' : nf_view2 (tRefl A x) (tRefl A' x')
    | neutrals2 (n n' : term) : nf_view2 n n'
    | mismatch2 (t u : term) : nf_view2 t u
    | anomaly2 (t u : term) : nf_view2 t u.

  Equations build_nf_view2 (t t' : term) : nf_view2 t t' :=
    build_nf_view2 t t' with (build_nf_view1 t) := {
    | nf_view1_type (eSort s) with (build_nf_view1 t') := {
      | nf_view1_type (eSort s') := sorts2 s s' ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_type (eProd A B) with (build_nf_view1 t') := {
      | nf_view1_type (eProd A' B') := prods2 A A' B B' ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_type eNat with (build_nf_view1 t') := {
      | nf_view1_type eNat := nats2 ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_type eEmpty with (build_nf_view1 t') := {
      | nf_view1_type eEmpty := emptys2 ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_type (eSig A B) with (build_nf_view1 t') := {
      | nf_view1_type (eSig A' B') := sigs2 A A' B B' ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_type (eId A x y) with (build_nf_view1 t') := {
      | nf_view1_type (eId A' x' y') := ids2 A A' x x' y y' ;
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_fun A t with (build_nf_view1 t') := {
      | nf_view1_fun A' t' := lams2 A A' t t' ;
      | nf_view1_ne _ := lam_ne2 A t _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_nat eZero with (build_nf_view1 t') := {
      | nf_view1_nat eZero := zeros2 ;
      | nf_view1_nat (eSucc _) := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_nat (eSucc u) with (build_nf_view1 t') := {
      | nf_view1_nat (eSucc u') := succs2 u u' ;
      | nf_view1_nat eZero := mismatch2 _ _ ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_sig A B t u with (build_nf_view1 t') := {
      | nf_view1_sig A' B' t' u' := pairs2 A A' B B' t t' u u' ;
      | nf_view1_ne _ := pair_ne2 A B t u _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_id A x with (build_nf_view1 t') := {
      | nf_view1_id A' x' := refls2 A A' x x' ;
      | nf_view1_ne _ := mismatch2 _ _ ;
      | _ := anomaly2 _ _ } ;
    | nf_view1_ne _ with (build_nf_view1 t') := {
      | nf_view1_type _ := mismatch2 _ _ ;
      | nf_view1_fun A' t' := ne_lam2 _ A' t' ;
      | nf_view1_nat _ := mismatch2 _ _ ;
      | nf_view1_sig A' B' t' u' := ne_pair2 _ A' B' t' u' ;
      | nf_view1_id _ _ := mismatch2 _ _ ;
      | nf_view1_ne _ := neutrals2 _ _ ;
    }
  }.

End Views.

#[export]Existing Instance OrecEffectExn.
#[export]Existing Instance MonadExn | 1.
#[export]Existing Instance MonadRaiseExn.

Equations ctx_access (Γ : context) (n : nat) : exn errors term :=
  ctx_access ε _ := raise variable_not_in_context ;

  ctx_access (_,,d) 0 := ret (d⟨↑⟩) ;
  ctx_access (Γ,,_) (S n') := d ← (ctx_access Γ n') ;; ret d⟨↑⟩.

Definition eq_sort (s s' : sort) : exn errors unit := ok.

Equations wh_red_stack : ∇(_ : term × stack), [False]⇒ term :=
  wh_red_stack (t,π) with (build_tm_view1 t) :=
  wh_red_stack (?(tRel n) ,π) (tm_view1_rel n) := ret (zip (tRel n) π) ;
  wh_red_stack (?(zip1 t s) ,π) (tm_view1_dest t s) := rec (t,cons s π) ;
  wh_red_stack (?(tLambda A t) ,nil) (tm_view1_fun A t) := ret (tLambda A t) ;
  wh_red_stack (?(tLambda A t) ,cons (eApp u) π) (tm_view1_fun A t) := rec (t[u..], π) ;
  wh_red_stack (_ ,cons _ _) (tm_view1_fun _ _) := undefined ;
  wh_red_stack (t ,nil) (tm_view1_nat _) := ret t ;
  wh_red_stack (?(tZero) ,cons (eNatElim _ hz _) π) (tm_view1_nat eZero) := rec (hz,π) ;
  wh_red_stack (?(tSucc t) ,cons (eNatElim P hz hs) π) (tm_view1_nat (eSucc t)) := rec (hs ,cons (eApp t) (cons (eApp (tNatElim P hz hs t)) π)) ;
  wh_red_stack (t ,cons _ _) (tm_view1_nat _) := undefined ;
  wh_red_stack (?(tPair A B a b),nil) (tm_view1_sig A B a b) := ret (tPair A B a b) ;
  wh_red_stack (?(tPair A B a b),cons eFst π) (tm_view1_sig A B a b) := rec (a , π) ;
  wh_red_stack (?(tPair A B a b),cons eSnd π) (tm_view1_sig A B a b) := rec (b , π) ;
  wh_red_stack (?(tPair A B a b),cons _ π) (tm_view1_sig A B a b) := undefined ;
  wh_red_stack (?(tRefl A x) ,nil) (tm_view1_id A x) := ret (tRefl A x) ;
  wh_red_stack (?(tRefl A x) ,cons (eIdElim _ _ _ hr _) π) (tm_view1_id A x) := rec (hr, π) ;
  wh_red_stack (_ ,cons _ _) (tm_view1_id _ _) := undefined ;
  wh_red_stack (t ,nil) (tm_view1_type _) := ret t ;
  wh_red_stack (t ,cons s _) (tm_view1_type _) := undefined.

#[export] Instance: PFun wh_red_stack := pfun_gen _ _ wh_red_stack.

Definition wh_red : ∇(t : term), [Sing wh_red_stack]⇒ term :=
  fun t => call_single wh_red_stack (t,nil).

#[export] Instance: PFun wh_red := pfun_gen _ _ wh_red.

Variant conv_state : Type :=
  | ty_state

  | ty_red_state

  | tm_state

  | tm_red_state

  | ne_state

  | ne_red_state.

Definition cstate_input (c : conv_state) : Set :=
  match c with
  | tm_state | tm_red_state => term
  | ty_state | ty_red_state | ne_state | ne_red_state => unit
  end.

Definition cstate_output (c : conv_state) : Set :=
  match c with
  | ty_state | ty_red_state | tm_state | tm_red_state => unit
  | ne_state | ne_red_state => term
  end.

#[export]Existing Instance combined_monad.
#[export]Existing Instance OrecEffectExnRaise.

Section Conversion.

Definition conv_dom (c : conv_state) :=
  ∑ (_ : context) (_ : cstate_input c) (_ : term), term.
Definition conv_full_dom := ∑ (c : conv_state), conv_dom c.
Definition conv_cod (c : conv_state) := exn errors (cstate_output c).
Definition conv_full_cod (x : conv_full_dom) := conv_cod (x.π1).

#[local]
Notation M0 := (orec (Sing wh_red) (conv_full_dom) (conv_full_cod)).
#[local]
Notation M := (combined_orec (exn errors) (Sing wh_red) conv_full_dom conv_full_cod).

Definition conv_stmt (c : conv_state) :=
  forall x0 : conv_dom c, M (cstate_output c).

Equations conv_ty : conv_stmt ty_state :=
  | (Γ;inp;T;V) :=
    T' ← call_single wh_red T ;;[M0]
    V' ← call_single wh_red V ;;[M0]
    r ← rec (ty_red_state;Γ;tt;T';V') ;;[M]
    ret (A:= unit) r.

Equations conv_ty_red : conv_stmt ty_red_state :=
  | (Γ;inp;T;T') with (build_nf_ty_view2 T T') :=
  {
    | ty_sorts s s' := ret (M:=M0) (eq_sort s s') ;
    | ty_prods A A' B B' :=
        rec (ty_state;Γ;tt;A;A') ;;
        rec (ty_state;(Γ,,A);tt;B;B') ;
    | ty_nats := ok ;
    | ty_emptys := ok ;
    | ty_sigs A A' B B' :=
        rec (ty_state;Γ;tt;A;A') ;;
        rec (ty_state;(Γ,,A);tt;B;B') ;
      | ty_neutrals _ _ :=
          rec (ne_state;Γ;tt;T;T') ;; ok ;
    | ty_ids A A' x x' y y' :=
      rec (ty_state;Γ;tt;A;A') ;;
      rec (tm_state;Γ;A;x;x') ;;
      rec (tm_state;Γ;A;y;y')
    | ty_mismatch _ _ := raise (head_mismatch) ;
    | ty_anomaly _ _ := undefined ;
  }.

Equations conv_tm : conv_stmt tm_state :=
  | (Γ;A;t;u) :=
    A' ← call_single wh_red A ;;[M0]
    t' ← call_single wh_red t ;;[M0]
    u' ← call_single wh_red u ;;[M0]
    map (M:=M) (@id (cstate_output tm_state)) (rec (tm_red_state;Γ;A';t';u')).

Equations conv_tm_red : conv_stmt tm_red_state :=
  | (Γ;A;t;u) with (build_nf_view3 A t u) :=
  {
    | types s (ty_sorts s1 s2) := undefined ;
    | types s (ty_prods A A' B B') :=
      rec (tm_state;Γ;tSort s;A;A') ;;
      rec (tm_state;Γ,,A;tSort s;B;B') ;
    | types _ ty_nats := ok ;
    | types _ ty_emptys := ok ;
    | types s (ty_sigs A A' B B') :=
        rec (tm_state;Γ;tSort s;A;A') ;;
        rec (tm_state;Γ,,A;tSort s;B;B') ;
    | types s (ty_ids A A' x x' y y') :=
        rec (tm_state;Γ;tSort s;A;A') ;;
        rec (tm_state;Γ;A;x;x') ;;
        rec (tm_state;Γ;A;y;y')
    | types _ (ty_neutrals _ _) :=
        rec (ne_state;Γ;tt;t;u) ;; ok ;
    | types s (ty_mismatch _ _) := raise head_mismatch ;
    | types _ (ty_anomaly _ _) := undefined ;
    | functions A B t u :=
        rec (tm_state;Γ,,A;B;eta_expand t;eta_expand u) ;
    | zeros := ok ;
    | succs t' u' :=
        rec (tm_state;Γ;tNat;t';u') ;
    | pairs A B t u :=
        rec (tm_state;Γ;A;tFst t; tFst u) ;;
        rec (tm_state;Γ; B[(tFst t)..]; tSnd t; tSnd u) ;
    | refls A x y A' x' A'' x'' := ok ;
    | neutrals _ _ _ :=
      rec (ne_state;Γ;tt;t;u) ;; ok ;
    | mismatch _ _ _ := raise head_mismatch ;
    | anomaly _ _ _ := undefined ;
  }.

Equations conv_ne : conv_stmt ne_state :=
  | (Γ;inp; t; t') with (build_ne_view2 t t') :=
  {
    | ne_rels n n' with n =? n' :=
    { | false := raise variable_mismatch ;
      | true with (ctx_access Γ n) :=
        {
        | exception e => undefined ;
        | success d => ret d
        }
    } ;
    | ne_apps n t n' t' =>
      T ← rec (ne_red_state;Γ;tt;n;n') ;;
      match T with
      | tProd A B =>
        rec (tm_state;Γ;A;t;t') ;; ret B[t..]
      | _ => undefined

      end ;
    | ne_nats n P hz hs n' P' hz' hs' =>
      rn ← rec (ne_red_state;Γ;tt;n;n') ;;
      match rn with
      | tNat =>
          rec (ty_state;(Γ,,tNat);tt;P;P') ;;
          rec (tm_state;Γ;P[tZero..];hz;hz') ;;
          rec (tm_state;Γ;elimSuccHypTy P;hs;hs') ;;
          ret P[n..]
      | _ => undefined
      end ;
    | ne_emptys n P n' P' =>
      rn ← rec (ne_red_state;Γ;tt;n;n') ;;
      match rn with
      | tEmpty =>
          rec (ty_state;(Γ,,tEmpty);tt;P;P') ;;
          ret P[n..]
      | _ => undefined
      end ;
    | ne_fsts n n' =>
      T ← rec (ne_red_state;Γ;tt;n;n') ;;
      match T with
      | tSig A B => ret A
      | _ => undefined

      end ;
    | ne_snds n n' =>
      T ← rec (ne_red_state;Γ;tt;n;n') ;;
      match T with
      | tSig A B => ret B[(tFst n)..]
      | _ => undefined

      end ;
    | ne_ids A x P hr y n A' x' P' hr' y' n' =>
      T ← rec (ne_red_state;Γ;tt;n;n') ;;
      match T with
      | tId _ _ _ =>
        rec (ty_state;Γ,,A,,tId A⟨↑⟩ x⟨↑⟩ (tRel 0);tt;P;P') ;;
        rec (tm_state;Γ;P[tRefl A x.: x..];hr;hr') ;;
        ret P[n .: y..]
      | _ => undefined
      end ;
    | ne_mismatch _ _ => raise destructor_mismatch ;
    | ne_anomaly _ _ => undefined
  }.

Equations conv_ne_red : conv_stmt ne_red_state :=
  | (Γ;inp;t;u) :=
    Ainf ← rec (ne_state;Γ;tt;t;u) ;;[M]
    r ← call_single wh_red Ainf ;;[M0]
    ret (M:=M) r.

Equations _conv : ∇(x : conv_full_dom), [Sing wh_red]⇒[exn errors] cstate_output x.π1 :=
  | (ty_state; Γ ; inp ; T; V) := conv_ty (Γ; inp; T; V);
  | (ty_red_state; Γ ; inp ; T; V) := conv_ty_red (Γ; inp; T; V);
  | (tm_state; Γ ; inp ; T; V) := conv_tm (Γ; inp; T; V);
  | (tm_red_state; Γ ; inp ; T; V) := conv_tm_red (Γ; inp; T; V);
  | (ne_state; Γ ; inp ; T; V) := conv_ne (Γ; inp; T; V);
  | (ne_red_state; Γ ; inp ; T; V) := conv_ne_red (Γ; inp; T; V).

#[local] Instance: PFun _conv := pfun_gen _ _ _conv.

Equations tconv : (context × term × term) ⇀ exn errors unit :=
  tconv (Γ,T,V) := call _conv (ty_state;Γ;tt;T;V).

End Conversion.

#[export] Instance: PFun tconv := pfun_gen _ _ tconv.

Section Conversion.

Definition uconv_dom := conv_state × term × term.
Definition uconv_cod (_ : uconv_dom) := exn errors unit.

#[local]
Notation M0 := (orec (Sing wh_red) (uconv_dom) (uconv_cod)).
#[local]
Notation M := (combined_orec (exn errors) (Sing wh_red) uconv_dom uconv_cod).

Equations uconv_tm : (term × term) -> M unit :=
  | (t,u) :=
    t' ← call_single wh_red t ;;[M0]
    u' ← call_single wh_red u ;;[M0]
    rec (tm_red_state,t',u').

Equations uconv_tm_red : (term × term) -> M unit :=
  | (t,t') with (build_nf_view2 t t') :=
  {
    | sorts2 s s' :=
        ret (eq_sort s s') ;
    | prods2 A A' B B' :=
        rec (tm_state,A,A') ;;
        rec (tm_state,B,B') ;
    | nats2 := ok ;
    | emptys2 := ok ;
    | sigs2 A A' B B' :=
        rec (tm_state,A,A') ;;
        rec (tm_state,B,B') ;
    | ids2 A A' x x' y y' :=
        rec (tm_state,A,A') ;;
        rec (tm_state,x,x') ;;
        rec (tm_state,y,y') ;
    | lams2 _ _ t t' :=
        rec (tm_state,t,t') ;
    | lam_ne2 _ t t' :=
        rec (tm_state,t,eta_expand t') ;
    | ne_lam2 t _ t' :=
        rec (tm_state,eta_expand t,t') ;
    | zeros2 := ok ;
    | succs2 t t' :=
        rec (tm_state,t,t') ;
    | pairs2 _ _ _ _ t t' u u' :=
        rec (tm_state,t,t') ;;
        rec (tm_state,u,u') ;
    | pair_ne2 _ _ t u t' :=
        rec (tm_state,t,tFst t') ;;
        rec (tm_state,u,tSnd t') ;
    | ne_pair2 t _ _ t' u' :=
        rec (tm_state,tFst t, t') ;;
        rec (tm_state,tSnd t,u') ;
    | refls2 A A' x x' :=
      ok ;
    | neutrals2 _ _ :=
      rec (ne_state,t,t') ;
    | mismatch2 _ _ := raise head_mismatch ;
    | anomaly2 _ _ := undefined ;
  }.

Equations uconv_ne : (term × term) -> M unit :=
  uconv_ne (t,t') with build_ne_view2 t t' :=
  {
  | ne_rels n n' with n =? n' :=
    { | false := raise variable_mismatch ;
      | true := ok ;
    } ;
      
  | ne_apps n t n' t' :=
    rec (ne_state,n,n') ;;
    rec (tm_state,t,t') ;

  | ne_nats n P hz hs n' P' hz' hs' :=
    rec (ne_state,n,n') ;;
    rec (tm_state,P,P') ;;
    rec (tm_state,hz,hz') ;;
    rec (tm_state,hs,hs')

  | ne_emptys n P n' P' :=
    rec (ne_state,n,n') ;;
    rec (tm_state,P,P')

  | ne_fsts n n' :=
    rec (ne_state,n,n')

  | ne_snds n n' :=
    rec (ne_state,n,n')

  | ne_ids A x P hr y n A' x' P' hr' y' n' :=
      rec (ne_state,n,n') ;;
      rec (tm_state,P,P') ;;
      rec (tm_state,hr,hr') ;

  | ne_mismatch _ _ => raise destructor_mismatch ;
  | ne_anomaly _ _ => undefined
}.

Equations _uconv : ∇ _ : conv_state × term × term, [Sing wh_red]⇒[exn errors] unit :=
  | (tm_state,t,u) := uconv_tm (t,u) ;
  | (tm_red_state,t,u) := uconv_tm_red (t,u);
  | (ne_state,t,u) := uconv_ne (t,u) ;
  | (_,t,u) := undefined.

  #[local] Instance: PFun _uconv := pfun_gen _ _ _uconv.

  Equations uconv : (context × term × term) ⇀ exn errors unit :=
    uconv (Γ,T,V) := call _uconv (tm_state,T,V).

End Conversion.

#[export] Instance: PFun uconv := pfun_gen _ _ uconv.