Library MetaCoq.Translations.standard_model

From MetaCoq.Template Require Import utils All.
From MetaCoq.Translations Require Import translation_utils sigma.
Import MCMonadNotation.

Infix "≤" := Nat.leb.

Definition default_term := tVar "constant_not_found".
Definition debug_term msg:= tVar ("debug: " ^ msg).

****************** WARNING : WIP ! ****************** *

Uses unsafe termination for the translation function
Print Typing Flags.
Unset Guard Checking.

MetaCoq Quote Definition tUnit := unit.
MetaCoq Quote Definition ttt := tt.

Fixpoint kproj (k : nat) (t : term) :=
  match k with
  | 0 ⇒ t
  | S kkproj k (proj1 t)
  end.

Notation app0 := (fun tsubst_app t [tRel 0]).

Fixpoint tsl (ΣE : tsl_context) (Γ : context) (t : term) {struct t}
  : tsl_result term :=
  match t with
  | tSort sΓ' <- tsl_ctx ΣE Γ ;;
              ret (tLambda (nNamed "γ") Γ' (tSort s))
  | tRel kΓ' <- tsl_ctx ΣE Γ ;;
             ret (tLambda (nNamed "γ") Γ' (proj2 (kproj k (tRel 0))))
  
  | tCast t c AΓ' <- tsl_ctx ΣE Γ ;;
                  t' <- tsl ΣE Γ t ;;
                  A' <- tsl ΣE Γ A ;;
                  ret (tLambda (nNamed "γ") Γ'
                               (tCast (app0 t') c (app0 A')))
  | tProd na A BΓ' <- tsl_ctx ΣE Γ ;;
                   A' <- tsl ΣE Γ A ;;
                   B' <- tsl ΣE (Γ ,, vass na A) B ;;
                   ret (tLambda (nNamed "γ") Γ'
                                (tProd na (app0 A')
                                   (subst_app B' [pair Γ' A' (tRel 1) (tRel 0)])))
  | tLambda na A tΓ' <- tsl_ctx ΣE Γ ;;
                     A' <- tsl ΣE Γ A ;;
                     t' <- tsl ΣE (Γ ,, vass na A) t ;;
                     ret (tLambda (nNamed "γ") Γ'
                            (tLambda na (app0 A')
                               (subst_app t' [pair Γ' (up A') (tRel 1) (tRel 0)])))
  | tLetIn na t A uΓ' <- tsl_ctx ΣE Γ ;;
                      t' <- tsl ΣE Γ t ;;
                      A' <- tsl ΣE Γ A ;;
                      u' <- tsl ΣE (Γ ,, vdef na t A) u ;;
                      ret (tLambda (nNamed "γ") Γ' (tLetIn na t' A' u'))
  | tApp t luΓ' <- tsl_ctx ΣE Γ ;;
                t' <- tsl ΣE Γ t ;;
                lu' <- monad_map (tsl ΣE Γ) lu ;;
                ret (tLambda (nNamed "γ") Γ' (mkApps (app0 t') (map app0 lu')))
  
  
  
  
  | tConst s univsΓ' <- tsl_ctx ΣE Γ ;;
                     t' <- lookup_tsl_table' (snd ΣE) (ConstRef s) ;;
                     ret (tLambda (nNamed "γ") Γ' (subst_app t' [ttt]))
  | tInd i univslookup_tsl_table' (snd ΣE) (IndRef i)
  | tConstruct i n univslookup_tsl_table' (snd ΣE) (ConstructRef i n)
  | tProj p tΓ' <- tsl_ctx ΣE Γ ;;
                t' <- tsl ΣE Γ t ;;
                ret (tLambda (nNamed "γ") Γ' (tProj p t'))

  | _ret t
  end
with tsl_ctx (ΣE : tsl_context) (Γ : context) {struct Γ} : tsl_result term :=
       match Γ with
       | []ret tUnit
       | {| decl_body := None; decl_type := A |} :: Γ
            Γ' <- tsl_ctx ΣE Γ ;;
            A' <- tsl ΣE Γ A ;;
            ret (pack Γ' A')
       | _todo "tsl"
       end.

#[global]
Instance param : Translation :=
  {| tsl_id := tsl_ident ;
     tsl_tm := fun ΣEtsl ΣE [] ;
     tsl_ty := Some (fun ΣE tt' <- tsl ΣE [] t ;; ret (subst_app t' [ttt])) ;
     tsl_ind := todo "tsl" |}.

Definition toto := fun (f : A, A A) ⇒ f Type.
MetaCoq Run (Translate emptyTC "toto").
Check (toto : unit ( A, A A) Type Type).

Definition FALSE := X, X.
MetaCoq Run (TC <- Translate emptyTC "FALSE" ;; tmPrint "toto" ;;
   Implement TC "a" ( (A : Set) (A0 : A Set) (x : A), FALSE A0 x)).
Next Obligation.
  compute in X. apply X.
Defined.

Definition T := A, A A.
MetaCoq Run (Translate emptyTC "T").

Definition tm := ((fun A (x:A) ⇒ x) (Type Type) (fun xx)).
MetaCoq Run (Translate emptyTC "tm").