Require Import List Arith String.
Require Import MetaCoq.Template.All.
From MetaCoq.PCUIC Require Import TemplateToPCUIC PCUICTyping PCUICAst.
Import ListNotations MonadNotation.
Require Import Vectors.Fin.
Require Import T_continuity_pred.
Set Implicit Arguments.
Local Open Scope string_scope.
Inductive term : Type :=
| zero : term
| succ : term
| var : nat -> term
| rec : type -> term
| lambda : type -> term -> term
| app : term -> term -> term.
Coercion app : term >-> Funclass.
Coercion var : nat >-> term.
Arguments izero {_ _}, {_} _.
Arguments isucc {_ _}, {_} _.
Arguments ivar {_ _} _, {_} _ _.
Arguments irec {_ _} _, {_} _ _.
Fixpoint back {n Γ T} (t : @iterm n Γ T) :=
match t with
| izero => zero
| isucc => succ
| ivar v => var (proj1_sig (Fin.to_nat v))
| irec A => rec A
| @ilambda _ _ A B s => lambda A (back s)
| iapp _ _ s t => app (back s) (back t)
end.
Definition type_eq (t1 t2 : type) :
{t1 = t2} + {t1 <> t2}.
Proof.
decide equality.
Defined.
Fixpoint infer (t : term) {n} (Γ : env n) {struct t} :
option (∑ A, @iterm n Γ A) :=
match t with
| zero => Some (N; izero)
| succ => Some (N ~> N; isucc)
| var v => match lt_dec v n with
| left H => let v' := Fin.of_nat_lt H in Some (Γ v'; ivar v')
| right _ => None
end
| rec A => Some (_ ; irec A )
| lambda A s => match infer s (cns A Γ) with
| Some (A'; t') => Some (A ~> A'; ilambda t')
| None => None end
| app s t => match infer s Γ with
| Some (A ~> B; s') => match infer t Γ with
| Some (A'; t') => match type_eq A A' with
| left H => Some (B; iapp s' (eq_rec_r _ t' H))
| right H => None
end
| None => None
end
| _ => None
end
end.
Lemma infer_correct t n (Γ : env n) t' :
infer t Γ = Some t' -> back (projT2 t') = t.
Proof.
induction t in n, Γ, t' |- *; cbn; intros; try now inversion H.
- destruct lt_dec; inversion H; subst; clear H.
cbn. now rewrite to_nat_of_nat.
- destruct infer as [ [] | ] eqn:E; inversion H; subst; clear H.
cbn. eapply IHt in E. cbn in *. now rewrite E.
- destruct infer as [ [] | ] eqn:E1; inversion H; subst; clear H.
destruct x; inversion H1; subst; clear H1.
destruct (infer t2 _) as [ [] | ] eqn:E2; inversion H0; subst; clear H0.
destruct type_eq; inversion H1; subst; clear H1.
eapply IHt1 in E1. eapply IHt2 in E2.
subst. reflexivity.
Qed.
(* Definition empty_env : env 0. intros ?. inversion H. Defined. *)
Existing Instance option_monad.
Definition tmTryUnfold {A} (f : A) := s <- tmQuote f ;;
match s with
| Ast.tConst name _ => tmEval (unfold name) f
| _ => tmReturn f
end.
Fixpoint reify_type (fuel : nat) (t : PCUICAst.term) : TemplateMonad type :=
match fuel with 0 => tmFail "not enough fuel" | S fuel =>
match t with
tProd na A B => A' <- reify_type fuel A ;;
B' <- reify_type fuel B ;;
ret (A' ~> B')
| tInd {| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} [] =>
ret N
| tConst name u =>
c <- tmUnquote (Ast.tConst name u) ;;
c' <- tmEval Common.hnf (my_projT2 c) ;;
c' <- tmTryUnfold c' ;;
s <- tmQuote c' ;;
s' <- reify_type fuel (trans s) ;;
ret s'
| _ => tmFail "not a System T type"
end end.
Fixpoint reify (fuel : nat) (t : PCUICAst.term) : TemplateMonad term :=
match fuel with 0 => tmFail "not enough fuel" | S fuel =>
match t with
| tRel n =>
ret (var n)
| tLambda na ty body =>
body' <- reify fuel body ;;
A <- reify_type fuel ty ;;
ret (lambda A body')
| tApp (tConst "Coq.Init.Datatypes.nat_rec" _) (tLambda _ _ X) =>
A <- reify_type fuel X ;;
ret (rec A)
| tApp t1 t2 =>
t1' <- reify fuel t1;;
t2' <- reify fuel t2;;
ret (app t1' t2')
| tConst name u =>
c <- tmUnquote (Ast.tConst name u) ;;
c' <- tmEval Common.hnf (my_projT2 c) ;;
c' <- tmTryUnfold c' ;;
s <- tmQuote c' ;;
s' <- reify fuel (trans s) ;;
ret s'
| tConstruct {| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 0 [] =>
ret zero
| tConstruct {| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 1 [] =>
ret succ
| _ => tmFail "not in SystemT fragment"
end end.
Definition Reify (def : ident) {A} (f : A) :=
(* f' <- tmTryUnfold f ;; *)
f <- tmEval hnf f ;;
s <- tmQuote f ;;
s' <- reify 20 (trans s) ;;
s' <- tmEval cbv (infer s' empty_env) ;;
match s' with
| Some (_; s') =>
tmDefinitionRed def (Some Common.hnf) s';;
tmPrint s'
| None => tmFail "could not infer type"
end.
Definition ExtractModulus' {A} (f : A) :=
(* f' <- tmTryUnfold f ;; *)
s <- tmQuote f ;;
s' <- reify 20 (trans s) ;;
s' <- tmEval cbv (infer s' empty_env) ;;
match s' with
| Some (A; s') =>
tmReturn (A; s')
| None => tmFail "could not infer type"
end.
Definition cnst s1 s := (Ast.tApp (Ast.tConst "T_continuity_pred.def_continuous" [])
[s1;
Ast.tApp
(Ast.tConstruct {| inductive_mind := "Coq.Init.Specif.sig"; inductive_ind := 0 |} 0
[])
[Ast.tApp
(Ast.tInd {| inductive_mind := "T_continuity_pred.iterm"; inductive_ind := 0 |} [])
[Ast.tConstruct
{| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 0 [];
Ast.tConst "T_continuity_pred.empty_env" [];
Ast.tApp
(Ast.tConstruct
{| inductive_mind := "T_continuity_pred.type"; inductive_ind := 0 |} 1 [])
[Ast.tApp
(Ast.tConstruct
{| inductive_mind := "T_continuity_pred.type"; inductive_ind := 0 |} 1 [])
[Ast.tConstruct
{| inductive_mind := "T_continuity_pred.type"; inductive_ind := 0 |} 0 [];
Ast.tConstruct
{| inductive_mind := "T_continuity_pred.type"; inductive_ind := 0 |} 0 []];
Ast.tConstruct
{| inductive_mind := "T_continuity_pred.type"; inductive_ind := 0 |} 0 []]];
Ast.tLambda (nNamed "t")
(Ast.tApp
(Ast.tInd {| inductive_mind := "T_continuity_pred.iterm"; inductive_ind := 0 |}
[])
[Ast.tConstruct
{| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 0 [];
Ast.tConst "T_continuity_pred.empty_env" [];
Ast.tConst "T_continuity_pred.functional" []])
(Ast.tApp
(Ast.tInd {| inductive_mind := "Coq.Init.Logic.eq"; inductive_ind := 0 |} [])
[Ast.tApp (Ast.tConst "T_continuity_pred.sem_ty" [])
[Ast.tConst "T_continuity_pred.functional" []];
Ast.tApp (Ast.tConst "T_continuity_pred.sem_tm" [])
[Ast.tConstruct
{| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 0 [];
Ast.tConst "T_continuity_pred.empty_env" [];
Ast.tConst "T_continuity_pred.functional" []; Ast.tRel 0;
Ast.tConst "T_continuity_pred.empty_interp" []]; s1]);
s;
Ast.tApp
(Ast.tConstruct {| inductive_mind := "Coq.Init.Logic.eq"; inductive_ind := 0 |} 0
[])
[Ast.tApp (Ast.tConst "T_continuity_pred.sem_ty" [])
[Ast.tConst "T_continuity_pred.functional" []];
Ast.tApp (Ast.tConst "T_continuity_pred.sem_tm" [])
[Ast.tConstruct
{| inductive_mind := "Coq.Init.Datatypes.nat"; inductive_ind := 0 |} 0 [];
Ast.tConst "T_continuity_pred.empty_env" [];
Ast.tConst "T_continuity_pred.functional" []; s;
Ast.tConst "T_continuity_pred.empty_interp" []]]]]).
Definition ExtractModulus (def : ident) (f : Baire -> nat) : TemplateMonad (continuous f) :=
syn <- tmQuote f ;;
m <- ExtractModulus' f;;
let (A, s) := (m : (∑ A0 : type, iterm empty_env A0)) in
match type_eq A ((N ~> N) ~> N) with
| left H => s <- tmQuote s ;; H <- tmUnquoteTyped (continuous f) (cnst syn s);;
H <- tmEval cbv H;;
tmDefinition def H
| right _ => @tmFail (continuous f) "wrong type"
end.
Definition get_modulus (f : Baire -> nat) (H : continuous f) := fun f => proj1_sig (H f).
(* Definition f2 := (fix f n := match n with 0 => 0 | S n => 1 end). *)
Definition f1 := (fun n : nat => n).
MetaCoq Run (Reify "ext_f1" f1).
Definition add := (fun n m : nat => nat_rec _ m (fun n r => S r) n).
MetaCoq Run (Reify "ext_add" add).
Definition f2 (phi : nat -> nat) (n : nat) : nat := add (phi n) (phi 0).
MetaCoq Run (Reify "ext_f2" f2).
Definition f3 (phi : nat -> nat) n := phi (phi n).
MetaCoq Run (Reify "ext_f3" f3).
MetaCoq Run (Reify "ext_add'" (fun n m : nat => nat_rec _ m (fun n r => S r) n)).
Definition f6 (phi : nat -> nat) := phi 0.
MetaCoq Run (ExtractModulus "cont_f6" f6).
Compute (get_modulus cont_f6).
Definition f5 (phi : nat -> nat) := phi (phi 0).
MetaCoq Run (ExtractModulus "cont_f5" f5).
Compute (get_modulus cont_f5).
Definition f4 (phi : nat -> nat) := add (phi 0) (phi (phi 2)).
MetaCoq Run (Reify "ext_f4" f4).
MetaCoq Run (ExtractModulus "cont_f4" f4).
Compute (get_modulus cont_f4).
Compute (get_modulus cont_f4 (fun x => x)).