intermediate
Require Import Base Template.Template Strings.Ascii String StringBase.
(* without prop, "iConst T" with T := list gives inconsistencies... *)
Inductive iTerm : Prop :=
iApp : iTerm -> iTerm -> iTerm
| iLam : iTerm -> iTerm
| iFix : iTerm -> iTerm
| iConst (X:Type) : X -> iTerm (* not-unfolded constants *)
| iMatch : iTerm -> list iTerm -> iTerm (* matches with all the cases *)
| iVar : nat -> nat -> iTerm
| iType (X : Type) : option X -> iTerm.
(* Tactics to translate from AST to Coq again *)
Ltac denote_type s :=
let t := constr:(Ast.tInd (Ast.mkInd s 0)) in
let k x := exact x in
denote_term t k.
Ltac denote_constr s n :=
let t := constr:(Ast.tConstruct (Ast.mkInd s 0) n) in
let k x := exact x in
denote_term t k.
Ltac denote_name s :=
let t := constr:(Ast.tVar s) in
let k x := exact x in
denote_term t k.
Ltac denote s :=
match s with
| _ => denote_type s
(* | _ => denote_constr s *)
| _ => denote_name s
| _ => fail
end.
Ltac pose_denote s := let f := constr:(ltac:( denote s )) in pose f.
(* Definition of the valid types for internalization *)
Ltac do_quote s := let k x := refine x in
let ter := constr: ( ltac:( quote_term s k ) ) in constr : ter .
(* Tactics to internalize automatically *)
Ltac list_map retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let x' := f x in
let xs' := list_map retType f xs in
constr:(x'::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac list_map_constr retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let x' := constr:(f x) in
let x'':= eval hnf in x' in
let xs' := list_map_constr retType f xs in
constr:(x''::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac list_map_2 retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let s := constr:(snd x) in
let s' := eval hnf in s in
let v := f s' in
let x' := constr:(fst x, v) in
let xs' := list_map_2 retType f xs in
constr:(x'::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac transform t :=
let transform_app' f s l :=
match eval hnf in l with
| nil => constr:s
| ?s' :: ?l' =>
let s'' := transform s' in
let u := constr:(Ast.tApp s [s'']) in
let r := f f u l' in
constr:r
| _ => fail 1000 "no list:" l
end
in
let transform_app s l := transform_app' transform_app' s l in
match t with
| Ast.tApp ?t ?ls =>
let t' := transform t in
transform_app t' ls
| Ast.tLambda ?x ?y ?s =>
let s' := transform s in
constr:(Ast.tLambda x y s')
| Ast.tCase ?a ?b ?s ?l =>
let s' := transform s in
let l' := list_map_2 (prod nat Ast.term) transform l in
constr:(Ast.tCase a b s' l')
| Ast.tFix [Ast.mkdef _ ?x1 ?x2 ?b ?x3] ?x4 =>
let b' := transform b in
constr:(Ast.tFix [Ast.mkdef _ x1 x2 b' x3] x4)
| Ast.tProd ?x ?y ?s =>
let s' := transform s in
constr:(Ast.tProd x y s')
| Ast.tConstruct _ _ => constr:t
| Ast.tConst _ => constr:t
| Ast.tInd _ => constr:t
| Ast.tRel _ => constr:t
| Ast.tVar _ => constr:t
| Ast.tSort _ => constr:t
| t => fail 100 "not supported:" t
end.
Ltac to_iTerm' t := (* Ast.term -> iTerm *)
match t with
| Ast.tRel ?n => constr:(iVar n n)
| Ast.tLambda _ _ ?s =>
let s' := to_iTerm' s in
constr:(iLam s')
| Ast.tApp ?s [?t] =>
let s' := to_iTerm' s in
let t' := to_iTerm' t in
constr:(iApp s' t')
| Ast.tCase _ _ ?s ?xt =>
let s' := to_iTerm' s in
let xt'' := list_map_constr Ast.term (@snd nat Ast.term) xt in
let xt' := list_map iTerm to_iTerm' xt'' in
constr:(iMatch s' xt')
| Ast.tFix [Ast.mkdef _ _ _ ?s _] _ =>
let s' := to_iTerm' s in
constr:(iFix s')
| Ast.tConstruct (Ast.mkInd ?s _) ?n =>
let c := constr:(ltac:( denote_constr s n )) in
constr: (iConst c )
| Ast.tInd (Ast.mkInd ?s _) =>
let s' := eval cbv in s in
let c := constr:(ltac:( denote s')) in
constr: (iConst c )
| Ast.tConst ?s =>
let s' := eval cbv in (name_after_dot s) in
let x := constr:(ltac:( denote s' )) in
constr: (iConst x)
| Ast.tVar ?s =>
let x := constr:(ltac:( denote s )) in
constr: (iConst x)
| Ast.tProd _ _ _ => constr:(iType (@None unit))
| _ => fail 1000 "failed to build iTerm (is identifier available on top-level?)" t
end.
Definition helper (H:Type) := exists X (F:X -> Type) , H = (forall x, F x).
Ltac getHelper H :=
let G := fresh "G" in
let H' := constr:(H) in
assert (G:helper H') by repeat eexists;exact G.
Ltac getBody H :=
let H' := constr:(ltac:(getHelper H)) in
match eval hnf in H' with
ex_intro _ _ (ex_intro _ ?B _) => constr:(B)
end.
(* the Type level of an expression that returns a type is the number of arguments until it returns a type *)
Ltac TypeLevel' t :=
match eval hnf in t with
| Ast.tProd _ _ ?t'=>
let n := TypeLevel' t' in
constr:(S n)
| Ast.tSort _ => constr:(0)
| Ast.tApp ?s _ =>
let n := TypeLevel' s in
let n' := eval cbv in (pred n) in
constr:(n')
| Ast.tInd (Ast.mkInd ?s _) => fail 1 (*
let c := constr:(ltac:( denote s)) in
let t'' := type of c in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term t'' k) in
TypeLevel' t'*)
| Ast.tConst ?s => fail 1 (*
let s' := eval cbv in (name_after_dot s) in
let c := constr:(ltac:( denote s')) in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term c k) in
TypeLevel' t'*)
| Ast.tVar ?s => fail 1(*
let s' := eval cbv in (name_after_dot s) in
let c := constr:(ltac:( denote s')) in
let t'' := type of c in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term t'' k) in
TypeLevel' t' *)
| Ast.tRel ?s => fail 1
| _ => fail 1 "not supported:" t
end.
Ltac TypeLevel f:=
let t := type of f in
let k x := exact x in
let t'' := constr:ltac:(quote_term t k) in
let t' := transform t'' in
match constr:(0) with
_ => let n := TypeLevel' t' in constr:(Some n)
| _ => constr:(@None nat)
end.
Ltac reconstruct t :=
match t with
| iApp ?s ?t =>
let s' := reconstruct s in
let t' := reconstruct t in
constr: (s' t')
| iLam ?s =>
let s' := reconstruct s in
constr:(fun x : nat => s')
| iType (Some ?x) => constr:(x)
| iType None => constr:(True)
| iConst ?f => constr:(f)
(* | _ => fail 1000 "reconstruction failed for:" t *)
end.
Ltac type_elim' u := (* iTerm -> ( iTerm * option prop_level *)
let F x :=
match type_elim' x with
(?x',_) => constr:(x')
end in
match u with
iApp ?s ?t =>
match type_elim' s with
(?s',?n) =>
match type_elim' t with
(?t',_) =>
match n with
None => constr:(iApp s' t',@None nat)
| Some 1 => let x := reconstruct (iApp s t) in constr:(iType (Some x),@None nat)
| Some 1 => constr:(iType (@None unit),@None nat)
| Some (S (S ?n')) =>constr:(iApp s' t', Some (S n'))
end
end
end
| iFix ?s =>
match type_elim' s with
(?s',?n) =>
match n with
| None => constr:(iFix s', @None nat)
| Some ?n => constr:(iFix s', Some (S n))
end
end
| iLam ?s =>
match type_elim' s with
(?s',?n) =>
match n with
| None => constr:(iLam s', @None nat)
| Some ?n => constr:(iLam s', Some (S n))
end
end
| iConst ?f =>
let n := TypeLevel f in
match n with
Some 0 => constr:(iType (Some f),@None nat)
| _ => constr:(iConst f,n)
end
| iMatch ?s ?lc =>
let s' := F s in
let lc' := list_map iTerm F lc in
constr:(iMatch s' lc',@None nat)
| iVar ?n ?m => constr:(iVar n m,@None nat)
| iType ?x => constr:(iType x,Some 0)
| ?s => fail 1000 "failed for: " s
end.
Ltac type_elim s :=
match type_elim' s with
(?s,?n) =>
match n with
None => constr:(s)
| _ => fail "Prop-returning values are not supported"
end
end.
Ltac to_iTerm'' t :=
let x := fresh "t" in
let k x := refine (x) in
let ter := constr: ( ltac:( quote_term t k ) ) in
let ter'' := transform ter in
let ter' := eval cbn in ter'' in
constr:(ter').
Ltac to_iTerm t :=
let x := fresh "t" in
let k x := refine (x) in
let ter := constr: ( ltac:( quote_term t k ) ) in
let ter'' := transform ter in
let ter' := eval cbn in ter'' in
let t' := to_iTerm' ter' in t'.
(* without prop, "iConst T" with T := list gives inconsistencies... *)
Inductive iTerm : Prop :=
iApp : iTerm -> iTerm -> iTerm
| iLam : iTerm -> iTerm
| iFix : iTerm -> iTerm
| iConst (X:Type) : X -> iTerm (* not-unfolded constants *)
| iMatch : iTerm -> list iTerm -> iTerm (* matches with all the cases *)
| iVar : nat -> nat -> iTerm
| iType (X : Type) : option X -> iTerm.
(* Tactics to translate from AST to Coq again *)
Ltac denote_type s :=
let t := constr:(Ast.tInd (Ast.mkInd s 0)) in
let k x := exact x in
denote_term t k.
Ltac denote_constr s n :=
let t := constr:(Ast.tConstruct (Ast.mkInd s 0) n) in
let k x := exact x in
denote_term t k.
Ltac denote_name s :=
let t := constr:(Ast.tVar s) in
let k x := exact x in
denote_term t k.
Ltac denote s :=
match s with
| _ => denote_type s
(* | _ => denote_constr s *)
| _ => denote_name s
| _ => fail
end.
Ltac pose_denote s := let f := constr:(ltac:( denote s )) in pose f.
(* Definition of the valid types for internalization *)
Ltac do_quote s := let k x := refine x in
let ter := constr: ( ltac:( quote_term s k ) ) in constr : ter .
(* Tactics to internalize automatically *)
Ltac list_map retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let x' := f x in
let xs' := list_map retType f xs in
constr:(x'::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac list_map_constr retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let x' := constr:(f x) in
let x'':= eval hnf in x' in
let xs' := list_map_constr retType f xs in
constr:(x''::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac list_map_2 retType f A :=
match eval hnf in A with
| nil => constr:(@nil retType)
| ?x :: ?xs =>
let s := constr:(snd x) in
let s' := eval hnf in s in
let v := f s' in
let x' := constr:(fst x, v) in
let xs' := list_map_2 retType f xs in
constr:(x'::xs')
| _ => fail 1000 "not list of type" retType ": " A
end.
Ltac transform t :=
let transform_app' f s l :=
match eval hnf in l with
| nil => constr:s
| ?s' :: ?l' =>
let s'' := transform s' in
let u := constr:(Ast.tApp s [s'']) in
let r := f f u l' in
constr:r
| _ => fail 1000 "no list:" l
end
in
let transform_app s l := transform_app' transform_app' s l in
match t with
| Ast.tApp ?t ?ls =>
let t' := transform t in
transform_app t' ls
| Ast.tLambda ?x ?y ?s =>
let s' := transform s in
constr:(Ast.tLambda x y s')
| Ast.tCase ?a ?b ?s ?l =>
let s' := transform s in
let l' := list_map_2 (prod nat Ast.term) transform l in
constr:(Ast.tCase a b s' l')
| Ast.tFix [Ast.mkdef _ ?x1 ?x2 ?b ?x3] ?x4 =>
let b' := transform b in
constr:(Ast.tFix [Ast.mkdef _ x1 x2 b' x3] x4)
| Ast.tProd ?x ?y ?s =>
let s' := transform s in
constr:(Ast.tProd x y s')
| Ast.tConstruct _ _ => constr:t
| Ast.tConst _ => constr:t
| Ast.tInd _ => constr:t
| Ast.tRel _ => constr:t
| Ast.tVar _ => constr:t
| Ast.tSort _ => constr:t
| t => fail 100 "not supported:" t
end.
Ltac to_iTerm' t := (* Ast.term -> iTerm *)
match t with
| Ast.tRel ?n => constr:(iVar n n)
| Ast.tLambda _ _ ?s =>
let s' := to_iTerm' s in
constr:(iLam s')
| Ast.tApp ?s [?t] =>
let s' := to_iTerm' s in
let t' := to_iTerm' t in
constr:(iApp s' t')
| Ast.tCase _ _ ?s ?xt =>
let s' := to_iTerm' s in
let xt'' := list_map_constr Ast.term (@snd nat Ast.term) xt in
let xt' := list_map iTerm to_iTerm' xt'' in
constr:(iMatch s' xt')
| Ast.tFix [Ast.mkdef _ _ _ ?s _] _ =>
let s' := to_iTerm' s in
constr:(iFix s')
| Ast.tConstruct (Ast.mkInd ?s _) ?n =>
let c := constr:(ltac:( denote_constr s n )) in
constr: (iConst c )
| Ast.tInd (Ast.mkInd ?s _) =>
let s' := eval cbv in s in
let c := constr:(ltac:( denote s')) in
constr: (iConst c )
| Ast.tConst ?s =>
let s' := eval cbv in (name_after_dot s) in
let x := constr:(ltac:( denote s' )) in
constr: (iConst x)
| Ast.tVar ?s =>
let x := constr:(ltac:( denote s )) in
constr: (iConst x)
| Ast.tProd _ _ _ => constr:(iType (@None unit))
| _ => fail 1000 "failed to build iTerm (is identifier available on top-level?)" t
end.
Definition helper (H:Type) := exists X (F:X -> Type) , H = (forall x, F x).
Ltac getHelper H :=
let G := fresh "G" in
let H' := constr:(H) in
assert (G:helper H') by repeat eexists;exact G.
Ltac getBody H :=
let H' := constr:(ltac:(getHelper H)) in
match eval hnf in H' with
ex_intro _ _ (ex_intro _ ?B _) => constr:(B)
end.
(* the Type level of an expression that returns a type is the number of arguments until it returns a type *)
Ltac TypeLevel' t :=
match eval hnf in t with
| Ast.tProd _ _ ?t'=>
let n := TypeLevel' t' in
constr:(S n)
| Ast.tSort _ => constr:(0)
| Ast.tApp ?s _ =>
let n := TypeLevel' s in
let n' := eval cbv in (pred n) in
constr:(n')
| Ast.tInd (Ast.mkInd ?s _) => fail 1 (*
let c := constr:(ltac:( denote s)) in
let t'' := type of c in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term t'' k) in
TypeLevel' t'*)
| Ast.tConst ?s => fail 1 (*
let s' := eval cbv in (name_after_dot s) in
let c := constr:(ltac:( denote s')) in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term c k) in
TypeLevel' t'*)
| Ast.tVar ?s => fail 1(*
let s' := eval cbv in (name_after_dot s) in
let c := constr:(ltac:( denote s')) in
let t'' := type of c in
let k x := exact (transform x) in
let t' := constr:ltac:(quote_term t'' k) in
TypeLevel' t' *)
| Ast.tRel ?s => fail 1
| _ => fail 1 "not supported:" t
end.
Ltac TypeLevel f:=
let t := type of f in
let k x := exact x in
let t'' := constr:ltac:(quote_term t k) in
let t' := transform t'' in
match constr:(0) with
_ => let n := TypeLevel' t' in constr:(Some n)
| _ => constr:(@None nat)
end.
Ltac reconstruct t :=
match t with
| iApp ?s ?t =>
let s' := reconstruct s in
let t' := reconstruct t in
constr: (s' t')
| iLam ?s =>
let s' := reconstruct s in
constr:(fun x : nat => s')
| iType (Some ?x) => constr:(x)
| iType None => constr:(True)
| iConst ?f => constr:(f)
(* | _ => fail 1000 "reconstruction failed for:" t *)
end.
Ltac type_elim' u := (* iTerm -> ( iTerm * option prop_level *)
let F x :=
match type_elim' x with
(?x',_) => constr:(x')
end in
match u with
iApp ?s ?t =>
match type_elim' s with
(?s',?n) =>
match type_elim' t with
(?t',_) =>
match n with
None => constr:(iApp s' t',@None nat)
| Some 1 => let x := reconstruct (iApp s t) in constr:(iType (Some x),@None nat)
| Some 1 => constr:(iType (@None unit),@None nat)
| Some (S (S ?n')) =>constr:(iApp s' t', Some (S n'))
end
end
end
| iFix ?s =>
match type_elim' s with
(?s',?n) =>
match n with
| None => constr:(iFix s', @None nat)
| Some ?n => constr:(iFix s', Some (S n))
end
end
| iLam ?s =>
match type_elim' s with
(?s',?n) =>
match n with
| None => constr:(iLam s', @None nat)
| Some ?n => constr:(iLam s', Some (S n))
end
end
| iConst ?f =>
let n := TypeLevel f in
match n with
Some 0 => constr:(iType (Some f),@None nat)
| _ => constr:(iConst f,n)
end
| iMatch ?s ?lc =>
let s' := F s in
let lc' := list_map iTerm F lc in
constr:(iMatch s' lc',@None nat)
| iVar ?n ?m => constr:(iVar n m,@None nat)
| iType ?x => constr:(iType x,Some 0)
| ?s => fail 1000 "failed for: " s
end.
Ltac type_elim s :=
match type_elim' s with
(?s,?n) =>
match n with
None => constr:(s)
| _ => fail "Prop-returning values are not supported"
end
end.
Ltac to_iTerm'' t :=
let x := fresh "t" in
let k x := refine (x) in
let ter := constr: ( ltac:( quote_term t k ) ) in
let ter'' := transform ter in
let ter' := eval cbn in ter'' in
constr:(ter').
Ltac to_iTerm t :=
let x := fresh "t" in
let k x := refine (x) in
let ter := constr: ( ltac:( quote_term t k ) ) in
let ter'' := transform ter in
let ter' := eval cbn in ter'' in
let t' := to_iTerm' ter' in t'.