internalize_tac
Require Export LTactics internalize_def.
Require Import bijection Template.Template Strings.Ascii StringBase intermediate.
(* needed to enable fanxy dec-type-notation *)
(* TODO: is this bad for complexity *)
Typeclasses Transparent dec.
Definition String := String.
(* Auxiliary tactics to assert and find correctness lemmas *)
Ltac assert_correct t :=
let x := fresh "H" in
pose (x := correct t);
cbn -[internalizer] in x;
change internalizer with (int t) in x; simpl in x.
(* Typeclass for registering types *)
Ltac toTT' t :=
match eval hnf in t with
forall (x_:?ta),_ =>
let tt1 := constr:ltac:(toTT' ta) in
let B := getBody t in
let x := fresh "x" in
exact (TyAll tt1 (fun (x:ta) => ltac:(toTT' (B x)))) || fail 1 "toTT' failed for basic type" t
| Prop => exact (TyElim Prop) || fail 1 "toTT' prop elimination failed" t
| ?t1 => match type of t1 with
| Prop => exact (TyElim t1) || fail 2 "toTT' elimination failed for extended type" t
| ?t' => exact (TyB t1) || fail 1 "toTT' failed for extended type" t "(type:" t' ")"
end
end.
Ltac toTT t' :=
let t := eval lazy [dec] in t' in constr:(ltac:(toTT' t)).
(* Tactics to ease registration *)
Ltac register encf := refine (@mk_registered _ encf _);
abstract (now ((induction 0 || intros);simpl;value)).
Ltac register_inj := constructor;intros x; induction x; destruct 0;simpl; intros eq; try (injection eq || discriminate eq);intros;f_equal;auto;try now apply inj_enc.
(* Tactics to internalize automatically *)
Fixpoint transform (t : Ast.term) : Ast.term :=
let transform_app := fix f s l {struct l} :=
match l with
| [] => s
| s' :: l' => f (Ast.tApp s [transform s']) l'
end
in
let transform_app' := fix f s l {struct l} :=
match l with
| [] => s
| s' :: l' => f (Ast.tApp s [transform (snd s')]) l'
end
in
match t with
| Ast.tApp t ls => transform_app (transform t) ls
| Ast.tLambda x y s => Ast.tLambda x y (transform s)
| Ast.tCase _ _ s l => transform_app' (transform s) l
| Ast.tFix [Ast.mkdef _ x1 x2 b x3] x4 => Ast.tFix [Ast.mkdef _ x1 x2 (transform b) x3] x4
| t => t
end.
(* translates constructors into encode or internalize *)
Ltac matchToApp s l :=
match eval hnf in l with
| nil => constr : s
| cons ?x ?xs =>
let t := matchToApp (iApp s x) xs in
constr:(t)
end.
Definition elAt' L m := nth m L 0.
Ltac annotateVariables' t L :=
let f x := annotateVariables' x L in
match eval hnf in t with
| iVar ?n ?m =>
let m' := eval lazy in (m + elAt' L m) in
constr: (iVar n m')
| iApp ?s ?t =>
let s' := annotateVariables' s L in
let t' := annotateVariables' t L in
constr: (iApp s' t')
| iLam ?s =>
let s' := annotateVariables' s (0 :: L) in
constr: (iLam s')
| iFix ?s =>
let s' := annotateVariables' s (0::map S L) in
constr: (iFix s')
| iMatch ?s ?l =>
let l' := list_map iTerm f l in
let s' := annotateVariables' s L in
constr:(iMatch s' l')
| iType ?x => constr:(iType x)
| iConst ?f => constr:(iConst f)
| _ => fail 1000 "annotation failed in:" t
end.
Ltac annotateVariables t := annotateVariables' t (@nil nat).
Ltac toLambda t (* : iTerm -> L.term + Coq.term *) :=
match t with
| iVar ?n ?m => let v := eval cbv in (@inl term True (Lvw.var m)) in constr: v
| iLam ?t =>
match toLambda t with
| inl ?x => constr : (@inl term True (lam x ))
end
| iApp ?s ?t =>
let x := toLambda s in
match x with
| inl ?r1 =>
let y := toLambda t in
match y with
inl ?r2 => constr: (@inl term True (app r1 r2))
| inr _ => fail 1000 "internalized lhs" s "succesfully, but rhs " t "failed"
end
| inr ?r1 =>
let r2 := reconstruct t in
constr:( @inl term True (int (r1 r2)) )
(* if internalization failed *)
| inr ?r1 =>
let r2 := reconstruct t in
constr: (@inr True _ (r1 r2))
| inr ?r1 =>
fail 1000 "internalization failed for" r1 "(reconstructing" t "didn't work)"
end
| @iConst ?X ?x =>
constr: (@inl term True (int x))
| @iConst ?X ?x =>
constr: (@inr True X x)
| iFix ?s =>
match toLambda s with
inl ?s' => constr:(@inl term True(Lvw.rho (Lvw.lam s')))
| _ => fail 100 "failed under fix" t
end
| iMatch ?s ?l =>
let l' := matchToApp s l in
let t := toLambda l' in
constr:(t)
| iType _ => constr: ( @inl term True I)
| _ => fail 100 "failed to internalize iterm " t
end.
Ltac visableHead t :=
match t with
?h _ => visableHead h
| _ => t
end.
(* this can be used to internalize with an anonymous term, defined in coq*)
Ltac internalizeWith' p t_arg:=
match goal with
| [ |- internalizedClass _ ?f ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let t' := eval lazy [decision] in e in
match p with 4 => pose t' | _ =>
let tern := to_iTerm t' in
match p with 6 => pose tern | _ =>
let ter := type_elim tern in
match p with 5 => let ter' := to_iTerm t' in pose ter' | _ =>
match p with 3 => pose ter | _ =>
let ter' := annotateVariables ter in
match p with 2 => pose ter' | _ =>
let Lter' := toLambda ter' in
match Lter' with
| inl ?Lter =>
match p with
| 1 => pose Lter
| _ => apply Build_internalizedClass with (internalizer:=Lter);
[try value|]
end end end end end end end
end.
(* this derives the term autonomously*)
Ltac internalize' p :=
match goal with
| [ |- internalizedClass _ ?t ] => internalizeWith' p t
end.
Ltac internalizePretty :=
let y := fresh "y" in
let p := fresh "p" in
let s := fresh "s" in
let ps := fresh "ps" in
let R := fresh "R" in
match goal with
| |- internalizesF _ (TyAll (TyB _) _) _=> intros y s ps R;hnf in R;internalizePretty;rewrite R;clear s ps R
| |- internalizesF _ (TyAll (TyElim _) _) _=> intros p s ps R;hnf in R;internalizePretty;rewrite R;clear s ps R
| |- internalizesF _ (TyAll _ _) _=> intros y s ps R;cbn in R;internalizePretty
| |- internalizesF _ (TyB _) _=> hnf
| |- internalizesF _ (TyElim _) _=> hnf
| |- _ => fail 1000
end.
Ltac internalize := internalize' 0;internalizePretty;crush. (* Call to internalize non-recursive functions*)
Ltac internalizeC Lter' :=
match goal with
| [ |- internalizedClass _ ?t ] =>
let X := type of t in
let tt := toTT X in
apply Build_internalizedClass with (internalizer:=Lter') (ty :=tt);(try unfold Lter');[simpl;try abstract (value)|try abstract (simpl;crush;simpl)]
end.
Ltac internalizeWith s := internalizeWith' 0 s;internalizePretty;crush.
Ltac recRem :=
match goal with
| |- context[rho ?s] =>
let rP := fresh "rP" in
set (rP:=s);
assert (proc rP);[unfold rP;value|
let P := fresh "P" in
set (P := rho rP);
assert (proc P);[unfold P;value|]]
end.
Ltac internalizeR :=
internalize' 0;internalizePretty;recRem. (* Call to internalize recursive functions, use "recStep P at i" to do one step of the recursive stuff*)
Ltac internalizeWithR s:=
internalizeWith' 0 s;internalizePretty;recRem. (* Call to internalize recursive functions, use "recStep P at i" to do one step of the recursive stuff*)
Ltac enc_correct:=intros;
match goal with
| |- context C [@enc _ ?H ?x] =>
let cl:= fresh "cl" in
assert (cl:=@proc_enc _ H);unfold enc in cl;simpl in cl;
let g := context C [@enc_f _ H x] in change g; simpl;induction x;simpl;crush
end.
Notation "'internalized' f" := (internalizedClass ltac:(let t := type of f in let x := toTT t in exact x) f) (at level 100,only parsing).
Tactic Notation "internalize" := internalize.
Tactic Notation "internalize" "template" :=
match goal with
| [ |- internalizedClass _ ?t_arg ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let x := do_quote e in
pose x
end.
Tactic Notation "internalize" "transform" :=
match goal with
| [ |- internalizedClass _ ?t_arg ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let x := do_quote e in
let x := transform x in
idtac x
end.
Tactic Notation "internalize" "elim" := internalize' 2.
Tactic Notation "internalize" "intermadiate" := internalize' 6.
Tactic Notation "internalize" "term" := internalize' 1.
Tactic Notation "internalize" "constructor" :=
match goal with
| [ |- internalizedClass _ ?t ] =>
let X := type of t in
let f := constr:(enc_f X) in
internalizeC (f t)
end.
Tactic Notation "internalize" "constructor" "using" open_constr(t) := internalizeC t.
Tactic Notation "internalize" open_constr(t) "instead" := internalizeWith t.
Tactic Notation "internalize" "using" open_constr(Lter) :=
match goal with
| [ |- internalizedClass _ ?t ] =>
apply Build_internalizedClass with (internalizer:=Lter)
end.
Require Import bijection Template.Template Strings.Ascii StringBase intermediate.
(* needed to enable fanxy dec-type-notation *)
(* TODO: is this bad for complexity *)
Typeclasses Transparent dec.
Definition String := String.
(* Auxiliary tactics to assert and find correctness lemmas *)
Ltac assert_correct t :=
let x := fresh "H" in
pose (x := correct t);
cbn -[internalizer] in x;
change internalizer with (int t) in x; simpl in x.
(* Typeclass for registering types *)
Ltac toTT' t :=
match eval hnf in t with
forall (x_:?ta),_ =>
let tt1 := constr:ltac:(toTT' ta) in
let B := getBody t in
let x := fresh "x" in
exact (TyAll tt1 (fun (x:ta) => ltac:(toTT' (B x)))) || fail 1 "toTT' failed for basic type" t
| Prop => exact (TyElim Prop) || fail 1 "toTT' prop elimination failed" t
| ?t1 => match type of t1 with
| Prop => exact (TyElim t1) || fail 2 "toTT' elimination failed for extended type" t
| ?t' => exact (TyB t1) || fail 1 "toTT' failed for extended type" t "(type:" t' ")"
end
end.
Ltac toTT t' :=
let t := eval lazy [dec] in t' in constr:(ltac:(toTT' t)).
(* Tactics to ease registration *)
Ltac register encf := refine (@mk_registered _ encf _);
abstract (now ((induction 0 || intros);simpl;value)).
Ltac register_inj := constructor;intros x; induction x; destruct 0;simpl; intros eq; try (injection eq || discriminate eq);intros;f_equal;auto;try now apply inj_enc.
(* Tactics to internalize automatically *)
Fixpoint transform (t : Ast.term) : Ast.term :=
let transform_app := fix f s l {struct l} :=
match l with
| [] => s
| s' :: l' => f (Ast.tApp s [transform s']) l'
end
in
let transform_app' := fix f s l {struct l} :=
match l with
| [] => s
| s' :: l' => f (Ast.tApp s [transform (snd s')]) l'
end
in
match t with
| Ast.tApp t ls => transform_app (transform t) ls
| Ast.tLambda x y s => Ast.tLambda x y (transform s)
| Ast.tCase _ _ s l => transform_app' (transform s) l
| Ast.tFix [Ast.mkdef _ x1 x2 b x3] x4 => Ast.tFix [Ast.mkdef _ x1 x2 (transform b) x3] x4
| t => t
end.
(* translates constructors into encode or internalize *)
Ltac matchToApp s l :=
match eval hnf in l with
| nil => constr : s
| cons ?x ?xs =>
let t := matchToApp (iApp s x) xs in
constr:(t)
end.
Definition elAt' L m := nth m L 0.
Ltac annotateVariables' t L :=
let f x := annotateVariables' x L in
match eval hnf in t with
| iVar ?n ?m =>
let m' := eval lazy in (m + elAt' L m) in
constr: (iVar n m')
| iApp ?s ?t =>
let s' := annotateVariables' s L in
let t' := annotateVariables' t L in
constr: (iApp s' t')
| iLam ?s =>
let s' := annotateVariables' s (0 :: L) in
constr: (iLam s')
| iFix ?s =>
let s' := annotateVariables' s (0::map S L) in
constr: (iFix s')
| iMatch ?s ?l =>
let l' := list_map iTerm f l in
let s' := annotateVariables' s L in
constr:(iMatch s' l')
| iType ?x => constr:(iType x)
| iConst ?f => constr:(iConst f)
| _ => fail 1000 "annotation failed in:" t
end.
Ltac annotateVariables t := annotateVariables' t (@nil nat).
Ltac toLambda t (* : iTerm -> L.term + Coq.term *) :=
match t with
| iVar ?n ?m => let v := eval cbv in (@inl term True (Lvw.var m)) in constr: v
| iLam ?t =>
match toLambda t with
| inl ?x => constr : (@inl term True (lam x ))
end
| iApp ?s ?t =>
let x := toLambda s in
match x with
| inl ?r1 =>
let y := toLambda t in
match y with
inl ?r2 => constr: (@inl term True (app r1 r2))
| inr _ => fail 1000 "internalized lhs" s "succesfully, but rhs " t "failed"
end
| inr ?r1 =>
let r2 := reconstruct t in
constr:( @inl term True (int (r1 r2)) )
(* if internalization failed *)
| inr ?r1 =>
let r2 := reconstruct t in
constr: (@inr True _ (r1 r2))
| inr ?r1 =>
fail 1000 "internalization failed for" r1 "(reconstructing" t "didn't work)"
end
| @iConst ?X ?x =>
constr: (@inl term True (int x))
| @iConst ?X ?x =>
constr: (@inr True X x)
| iFix ?s =>
match toLambda s with
inl ?s' => constr:(@inl term True(Lvw.rho (Lvw.lam s')))
| _ => fail 100 "failed under fix" t
end
| iMatch ?s ?l =>
let l' := matchToApp s l in
let t := toLambda l' in
constr:(t)
| iType _ => constr: ( @inl term True I)
| _ => fail 100 "failed to internalize iterm " t
end.
Ltac visableHead t :=
match t with
?h _ => visableHead h
| _ => t
end.
(* this can be used to internalize with an anonymous term, defined in coq*)
Ltac internalizeWith' p t_arg:=
match goal with
| [ |- internalizedClass _ ?f ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let t' := eval lazy [decision] in e in
match p with 4 => pose t' | _ =>
let tern := to_iTerm t' in
match p with 6 => pose tern | _ =>
let ter := type_elim tern in
match p with 5 => let ter' := to_iTerm t' in pose ter' | _ =>
match p with 3 => pose ter | _ =>
let ter' := annotateVariables ter in
match p with 2 => pose ter' | _ =>
let Lter' := toLambda ter' in
match Lter' with
| inl ?Lter =>
match p with
| 1 => pose Lter
| _ => apply Build_internalizedClass with (internalizer:=Lter);
[try value|]
end end end end end end end
end.
(* this derives the term autonomously*)
Ltac internalize' p :=
match goal with
| [ |- internalizedClass _ ?t ] => internalizeWith' p t
end.
Ltac internalizePretty :=
let y := fresh "y" in
let p := fresh "p" in
let s := fresh "s" in
let ps := fresh "ps" in
let R := fresh "R" in
match goal with
| |- internalizesF _ (TyAll (TyB _) _) _=> intros y s ps R;hnf in R;internalizePretty;rewrite R;clear s ps R
| |- internalizesF _ (TyAll (TyElim _) _) _=> intros p s ps R;hnf in R;internalizePretty;rewrite R;clear s ps R
| |- internalizesF _ (TyAll _ _) _=> intros y s ps R;cbn in R;internalizePretty
| |- internalizesF _ (TyB _) _=> hnf
| |- internalizesF _ (TyElim _) _=> hnf
| |- _ => fail 1000
end.
Ltac internalize := internalize' 0;internalizePretty;crush. (* Call to internalize non-recursive functions*)
Ltac internalizeC Lter' :=
match goal with
| [ |- internalizedClass _ ?t ] =>
let X := type of t in
let tt := toTT X in
apply Build_internalizedClass with (internalizer:=Lter') (ty :=tt);(try unfold Lter');[simpl;try abstract (value)|try abstract (simpl;crush;simpl)]
end.
Ltac internalizeWith s := internalizeWith' 0 s;internalizePretty;crush.
Ltac recRem :=
match goal with
| |- context[rho ?s] =>
let rP := fresh "rP" in
set (rP:=s);
assert (proc rP);[unfold rP;value|
let P := fresh "P" in
set (P := rho rP);
assert (proc P);[unfold P;value|]]
end.
Ltac internalizeR :=
internalize' 0;internalizePretty;recRem. (* Call to internalize recursive functions, use "recStep P at i" to do one step of the recursive stuff*)
Ltac internalizeWithR s:=
internalizeWith' 0 s;internalizePretty;recRem. (* Call to internalize recursive functions, use "recStep P at i" to do one step of the recursive stuff*)
Ltac enc_correct:=intros;
match goal with
| |- context C [@enc _ ?H ?x] =>
let cl:= fresh "cl" in
assert (cl:=@proc_enc _ H);unfold enc in cl;simpl in cl;
let g := context C [@enc_f _ H x] in change g; simpl;induction x;simpl;crush
end.
Notation "'internalized' f" := (internalizedClass ltac:(let t := type of f in let x := toTT t in exact x) f) (at level 100,only parsing).
Tactic Notation "internalize" := internalize.
Tactic Notation "internalize" "template" :=
match goal with
| [ |- internalizedClass _ ?t_arg ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let x := do_quote e in
pose x
end.
Tactic Notation "internalize" "transform" :=
match goal with
| [ |- internalizedClass _ ?t_arg ] =>
let t := (let t' := eval lazy [enc] in t_arg in eval cbn in t') in
let h := visableHead t in (* hack: we allow polymorphic type variables, but ignore them here*)
let e1 := eval cbv in h in (* this allows to branch depending on an transparent/opaque (e.g. constructor) head*)
let e :=
match h with
e1 => t
| _ => (let t' := eval lazy [h enc] in t in t')
end
in
let x := do_quote e in
let x := transform x in
idtac x
end.
Tactic Notation "internalize" "elim" := internalize' 2.
Tactic Notation "internalize" "intermadiate" := internalize' 6.
Tactic Notation "internalize" "term" := internalize' 1.
Tactic Notation "internalize" "constructor" :=
match goal with
| [ |- internalizedClass _ ?t ] =>
let X := type of t in
let f := constr:(enc_f X) in
internalizeC (f t)
end.
Tactic Notation "internalize" "constructor" "using" open_constr(t) := internalizeC t.
Tactic Notation "internalize" open_constr(t) "instead" := internalizeWith t.
Tactic Notation "internalize" "using" open_constr(Lter) :=
match goal with
| [ |- internalizedClass _ ?t ] =>
apply Build_internalizedClass with (internalizer:=Lter)
end.