Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Utilopen Ppopen CErrorsopen Namesopen Varsopen Constropen Context
(****************************************************************************)(* Functions for dealing with constr terms *)(****************************************************************************)
(***************************)(* Other term constructors *)(***************************)
let name_annot = map_annot Name.mk_name
let mkNamedProd id typ c = mkProd (name_annot id, typ, subst_var id.binder_name c)let mkNamedLambda id typ c = mkLambda (name_annot id, typ, subst_var id.binder_name c)let mkNamedLetIn id c1 t c2 = mkLetIn (name_annot id, c1, t, subst_var id.binder_name c2)
(* Constructs either [(x:t)c] or [[x=b:t]c] *)let mkProd_or_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkProd (na, t, c) | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
let mkNamedProd_or_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c | LocalDef (id,b,t) -> mkNamedLetIn id b t c
(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)let mkProd_wo_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkProd (na, t, c) | LocalDef (_na,b,_t) -> subst1 b c
let mkNamedProd_wo_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c | LocalDef (id,b,_) -> subst1 b (subst_var id.binder_name c)
(* non-dependent product t1 -> t2 *)let mkArrow t1 r t2 = mkProd (make_annot Anonymous r, t1, t2)let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
(* Constructs either [[x:t]c] or [[x=b:t]c] *)let mkLambda_or_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkLambda (na, t, c) | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
let mkNamedLambda_or_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedLambda id t c | LocalDef (id,b,t) -> mkNamedLetIn id b t c
(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)let prodn n env b = let rec prodrec = function | (0, _env, b) -> b | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) | _ -> assert false in prodrec (n,env,b)
(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)let compose_prod l b = prodn (List.length l) l b
(* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *)let lamn n env b = let rec lamrec = function | (0, _env, b) -> b | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) | _ -> assert false in lamrec (n,env,b)
(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)let compose_lam l b = lamn (List.length l) l b
let applist (f,l) = mkApp (f, Array.of_list l)
let applistc f l = mkApp (f, Array.of_list l)
let appvect = mkApp
let appvectc f l = mkApp (f,l)
(* to_lambda n (x1:T1)...(xn:Tn)T = * [x1:T1]...[xn:Tn]T *)let rec to_lambda n prod = if Int.equal n 0 then prod else match kind prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c | _ -> anomaly Pp.(str "Not enough lambda's.")
let rec to_prod n lam = if Int.equal n 0 then lam else match kind lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c | _ -> anomaly Pp.(str "Not enough prod's.")
let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
(* Application with expected on-the-fly reduction *)
let lambda_applist c l = let rec app subst c l = match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough lambda's.") in app [] c l
let lambda_appvect c v = lambda_applist c (Array.to_list v)
let lambda_applist_decls n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") else match kind t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l
let lambda_appvect_decls n c v = lambda_applist_decls n c (Array.to_list v)
(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)let prod_applist c l = let rec app subst c l = match kind c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l
(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)let prod_appvect c v = prod_applist c (Array.to_list v)
let prod_applist_decls n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") else match kind t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l
let prod_appvect_decls n c v = prod_applist_decls n c (Array.to_list v)
(*********************************)(* Other term destructors *)(*********************************)
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)let decompose_prod = let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec []
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)let decompose_lambda = let rec lamdec_rec l c = match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec []
(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T) *)let decompose_prod_n n = if n < 0 then anomaly (str "decompose_prod_n: integer parameter must be positive."); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> anomaly (str "decompose_prod_n: not enough products.") in prodec_rec [] n
(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T) *)let decompose_lambda_n n = if n < 0 then anomaly (str "decompose_lambda_n: integer parameter must be positive."); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> anomaly (str "decompose_lambda_n: not enough abstractions.") in lamdec_rec [] n
(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)let decompose_prod_decls = let open Context.Rel.Declaration in let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec Context.Rel.empty
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)let decompose_lambda_decls = let rec lamdec_rec l c = let open Context.Rel.Declaration in match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec Context.Rel.empty
(* Given a positive integer n, decompose a product or let-in term of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair of the quantifying context [(xn,None,Tn);..;(xi,Some ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)let decompose_prod_n_decls n = if n < 0 then anomaly (str "decompose_prod_n_decls: integer parameter must be positive."); let rec prodec_rec l n c = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> anomaly (str "decompose_prod_n_decls: not enough declarations.") in prodec_rec Context.Rel.empty n
let decompose_lambda_prod_n_decls n = if n < 0 then anomaly (str "decompose_lambda_prod_n_decls: integer parameter must be positive."); let rec lamprodec_rec l n c t = if Int.equal n 0 then (l, c, t) else let open Context.Rel.Declaration in match kind c, kind t with | Lambda (na, u, c), Prod (_, _, t) -> lamprodec_rec (LocalAssum (na, u) :: l) (n-1) c t | LetIn (na, b, u, c), LetIn (_, _, _, t) -> lamprodec_rec (LocalDef (na, b, u) :: l) (n-1) c t | _ -> anomaly (str "decompose_lambda_prod_n_decls: not same form.") in lamprodec_rec Context.Rel.empty n
(** Given a positive integer n, decompose a lambda term [fun (x1:T1)..(xn:Tn) => T] (possibly with let-ins before xn) into the pair of the abstracted context [(xn,None,Tn);...;(x1,None,T1)] and of the inner body [T]. *)let decompose_lambda_n_assum n = if n < 0 then anomaly (str "decompose_lambda_n_assum: integer parameter must be positive."); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c | _c -> anomaly (str "decompose_lambda_n_assum: not enough abstractions.") in lamdec_rec Context.Rel.empty n
(* Given a positive integer n, decompose a lambda or let-in term [fun (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of the inner body [T]. Lets in between are not expanded but turn into local definitions, and n is the number of lambdas and lets to decompose. *)let decompose_lambda_n_decls_opt n c = if n < 0 then anomaly (str "decompose_lambda_n_decls: integer parameter must be positive."); let rec lamdec_rec l n c = if Int.equal n 0 then Some (l,c) else let open Context.Rel.Declaration in match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> None in lamdec_rec Context.Rel.empty n c
let decompose_lambda_n_decls n c = match decompose_lambda_n_decls_opt n c with | Some v -> v | None -> anomaly (str "decompose_lambda_n_decls: not enough declarations.")
let prod_decls t = fst (decompose_prod_decls t)let prod_n_decls n t = fst (decompose_prod_n_decls n t)let strip_prod_decls t = snd (decompose_prod_decls t)let strip_prod t = snd (decompose_prod t)let strip_prod_n n t = snd (decompose_prod_n n t)let lambda_decls t = fst (decompose_lambda_decls t)let lam_n_assum n t = fst (decompose_lambda_n_assum n t)let strip_lambda_decls t = snd (decompose_lambda_decls t)let strip_lam t = snd (decompose_lambda t)let strip_lam_n n t = snd (decompose_lambda_n n t)
(***************************)(* Arities *)(***************************)
(* An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types and of a sort *)
type arity = Constr.rel_context * Sorts.t
let destArity = let open Context.Rel.Declaration in let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") in prodec_rec []
let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign
let rec isArity c = match kind c with | Prod (_,_,c) -> isArity c | LetIn (_,_,_,c) -> isArity c | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false