From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- engine/evarutil.ml | 11 ++-- engine/evarutil.mli | 16 ++--- engine/termops.ml | 70 ++++++++++---------- engine/termops.mli | 185 ++++++++++++++++++++++++++-------------------------- 4 files changed, 141 insertions(+), 141 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 73286f2c4..8940be09d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -47,10 +47,11 @@ let evd_comb2 f evdref x y = z let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x + EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) let new_global evd x = - Sigma.fresh_global (Global.env()) evd x + let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in + Sigma (EConstr.of_constr c, sigma, p) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -230,7 +231,7 @@ let new_meta = let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in fun () -> incr meta_ctr; !meta_ctr -let mk_new_meta () = mkMeta(new_meta()) +let mk_new_meta () = EConstr.mkMeta(new_meta()) (* The list of non-instantiated existential declarations (order is important) *) @@ -396,6 +397,7 @@ let default_source = (Loc.ghost,Evar_kinds.InternalHole) let restrict_evar evd evk filter candidates = let evd = Sigma.to_evar_map evd in + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let evd, evk' = Evd.restrict evk filter ?candidates evd in Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) @@ -408,6 +410,7 @@ let new_pure_evar_full evd evi = let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = let typ = EConstr.Unsafe.to_constr typ in let evd = Sigma.to_evar_map evd in + let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let evi = { @@ -437,7 +440,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in - let map c = EConstr.Unsafe.to_constr (subst2 subst vsubst (EConstr.of_constr c)) in + let map c = subst2 subst vsubst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = match filter with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 5882f02b9..ea9599c8b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -17,18 +17,18 @@ open Environ (** [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable -val mk_new_meta : unit -> constr +val mk_new_meta : unit -> EConstr.constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma val new_pure_evar : named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma @@ -37,7 +37,7 @@ val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma (** the same with side-effects *) val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.types -> EConstr.constr @@ -56,12 +56,12 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.s val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma + EConstr.constr list option -> (existential_key, 'r) Sigma.sigma (** Polymorphic constants *) -val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma -val e_new_global : evar_map ref -> Globnames.global_reference -> constr +val new_global : 'r Sigma.t -> Globnames.global_reference -> (EConstr.constr, 'r) Sigma.sigma +val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -71,7 +71,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr as a telescope) is [sign] *) val new_evar_instance : named_context_val -> 'r Sigma.t -> EConstr.types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:EConstr.constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma diff --git a/engine/termops.ml b/engine/termops.ml index 879d77de2..465832c10 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -210,12 +210,7 @@ let lookup_rel_id id sign = lookrec 1 sign (* Constructs either [forall x:t, c] or [let x:=b:t in c] *) -let mkProd_or_LetIn decl c = - let open RelDecl in - match decl with - | LocalAssum (na,t) -> mkProd (na, t, c) - | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) - +let mkProd_or_LetIn = EConstr.mkProd_or_LetIn (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *) let mkProd_wo_LetIn decl c = let open EConstr in @@ -628,9 +623,10 @@ let vars_of_global_reference env gr = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs sigma m t = + let open EConstr in let eqc x y = - if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y)) - else EConstr.eq_constr_nounivs sigma x y + if univs then not (Option.is_empty (eq_constr_universes sigma x y)) + else eq_constr_nounivs sigma x y in let rec deprec m t = if eqc m t then @@ -638,13 +634,13 @@ let dependent_main noevar univs sigma m t = else match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); + deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); CArray.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> () + | _, Cast (c,_,_) when noevar && isMeta sigma c -> () | _, Evar _ when noevar -> () - | _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t + | _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t in try deprec m t; false with Occur -> true @@ -661,6 +657,7 @@ let dependent_in_decl sigma a decl = | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t) let count_occurrences sigma m t = + let open EConstr in let n = ref 0 in let rec countrec m t = if EConstr.eq_constr sigma m t then @@ -668,13 +665,13 @@ let count_occurrences sigma m t = else match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); + countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); Array.iter (countrec m) (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when EConstr.isMeta sigma c -> () + | _, Cast (c,_,_) when isMeta sigma c -> () | _, Evar _ -> () - | _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t + | _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t in countrec m t; !n @@ -682,7 +679,7 @@ let count_occurrences sigma m t = (* Synonymous *) let occur_term = dependent -let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t) +let pop t = EConstr.Vars.lift (-1) t (***************************) (* bindings functions *) @@ -712,33 +709,35 @@ let collapse_appl sigma c = match EConstr.kind sigma c with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in - EConstr.Unsafe.to_constr (collapse_rec f cl) - | _ -> EConstr.Unsafe.to_constr c + collapse_rec f cl + | _ -> c (* First utilities for avoiding telescope computation for subst_term *) let prefix_application sigma eq_fun (k,c) t = - let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + let open EConstr in + let c' = collapse_appl sigma c and t' = collapse_appl sigma t in match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then - Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then + Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) else None | _ -> None let my_prefix_application sigma eq_fun (k,c) by_c t = - let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + let open EConstr in + let c' = collapse_appl sigma c and t' = collapse_appl sigma t in match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then - Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then + Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) else None | _ -> None @@ -754,7 +753,7 @@ let subst_term_gen sigma eq_fun c t = match prefix_application sigma eq_fun kc t with | Some x -> x | None -> - if eq_fun sigma c t then EConstr.mkRel k + if eq_fun sigma c t then mkRel k else EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t in @@ -775,7 +774,7 @@ let replace_term_gen sigma eq_fun c by_c in_t = EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c)) substrec kc t) in - EConstr.Unsafe.to_constr (substrec (0,c) in_t) + substrec (0,c) in_t let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t @@ -933,12 +932,11 @@ let filtering sigma env cv_pb c1 c2 = aux env cv_pb c1 c2; !evm let decompose_prod_letin sigma c = - let inj c = EConstr.Unsafe.to_constr c in let rec prodec_rec i l sigma c = match EConstr.kind sigma c with - | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c - | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c + | Prod (n,t,c) -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c + | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c | Cast (c,_,_) -> prodec_rec i l sigma c - | _ -> i,l, inj c in + | _ -> i,l, c in prodec_rec 0 [] sigma c (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction @@ -969,7 +967,7 @@ let nb_prod_modulo_zeta sigma x = | _ -> n in count 0 x -let align_prod_letin sigma c a : Context.Rel.t * constr = +let align_prod_letin sigma c a = let (lc,_,_) = decompose_prod_letin sigma c in let (la,l,a) = decompose_prod_letin sigma a in if not (la >= lc) then invalid_arg "align_prod_letin"; @@ -980,21 +978,23 @@ let align_prod_letin sigma c a : Context.Rel.t * constr = (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) (* Remplace 2 earlier buggish versions *) -let rec eta_reduce_head c = - match kind_of_term c with +let rec eta_reduce_head sigma c = + let open EConstr in + let open Vars in + match EConstr.kind sigma c with | Lambda (_,c1,c') -> - (match kind_of_term (eta_reduce_head c') with + (match EConstr.kind sigma (eta_reduce_head sigma c') with | App (f,cl) -> let lastn = (Array.length cl) - 1 in if lastn < 0 then anomaly (Pp.str "application without arguments") else - (match kind_of_term cl.(lastn) with + (match EConstr.kind sigma cl.(lastn) with | Rel 1 -> let c' = if Int.equal lastn 0 then f else mkApp (f, Array.sub cl 0 lastn) in - if noccurn 1 c' + if noccurn sigma 1 c' then lift (-1) c' else c | _ -> c) diff --git a/engine/termops.mli b/engine/termops.mli index 1699d600e..d7d9c743d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -12,6 +12,7 @@ open Pp open Names open Term +open EConstr open Environ (** printers *) @@ -20,59 +21,56 @@ val pr_sort_family : sorts_family -> std_ppcmds val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds (** debug printer: do not use to display terms to the casual user... *) -val set_print_constr : (env -> constr -> std_ppcmds) -> unit -val print_constr : constr -> std_ppcmds -val print_constr_env : env -> constr -> std_ppcmds +val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit +val print_constr : Constr.constr -> std_ppcmds +val print_constr_env : env -> Constr.constr -> std_ppcmds val print_named_context : env -> std_ppcmds val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : Name.t * EConstr.types -> env -> env -val push_rels_assum : (Name.t * types) list -> env -> env -val push_named_rec_types : Name.t array * types array * 'a -> env -> env +val push_rel_assum : Name.t * types -> env -> env +val push_rels_assum : (Name.t * Constr.types) list -> env -> env +val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env -val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types +val lookup_rel_id : Id.t -> Context.Rel.t -> int * Constr.constr option * Constr.types (** Associates the contents of an identifier in a [rel_context]. Raise [Not_found] if there is no such identifier. *) (** Functions that build argument lists matching a block of binders or a context. [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] *) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> EConstr.constr list +val rel_vect : int -> int -> Constr.constr array +val rel_list : int -> int -> constr list (** iterators/destructors on terms *) val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types -val it_mkProd : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types -val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types +val it_mkProd : types -> (Name.t * types) list -> types +val it_mkLambda : constr -> (Name.t * types) list -> constr val it_mkProd_or_LetIn : types -> Context.Rel.t -> types -val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types -val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types -val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr +val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr (** {6 Generic iterators on constr} *) -val map_constr_with_named_binders : - (Name.t -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_binders_left_to_right : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.constr -> EConstr.constr) -> - 'a -> EConstr.constr -> EConstr.constr + ('a -> constr -> constr) -> + 'a -> constr -> constr val map_constr_with_full_binders : Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t + ('a -> constr -> constr) -> 'a -> constr -> constr (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -81,62 +79,61 @@ val map_constr_with_full_binders : index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -val fold_constr_with_binders : - Evd.evar_map -> ('a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_binders : Evd.evar_map -> + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val fold_constr_with_full_binders : - Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b +val fold_constr_with_full_binders : Evd.evar_map -> + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b val iter_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> - constr -> unit + (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a -> + Constr.constr -> unit (**********************************************************************) -val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t -val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_head_cast : Evd.evar_map -> constr -> constr +val drop_extra_implicit_args : Evd.evar_map -> constr -> constr (** occur checks *) exception Occur -val occur_meta : Evd.evar_map -> EConstr.t -> bool -val occur_existential : Evd.evar_map -> EConstr.t -> bool -val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool -val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool -val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool +val occur_meta : Evd.evar_map -> constr -> bool +val occur_existential : Evd.evar_map -> constr -> bool +val occur_meta_or_existential : Evd.evar_map -> constr -> bool +val occur_evar : Evd.evar_map -> existential_key -> constr -> bool +val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> Context.Named.Declaration.t -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) -val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool +val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool -val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t +val free_rels : Evd.evar_map -> constr -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool -val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool -val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int -val collect_metas : Evd.evar_map -> EConstr.t -> int list -val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *) +val dependent : Evd.evar_map -> constr -> constr -> bool +val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_univs : Evd.evar_map -> constr -> constr -> bool +val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool +val dependent_in_decl : Evd.evar_map -> constr -> Context.Named.Declaration.t -> bool +val count_occurrences : Evd.evar_map -> constr -> constr -> int +val collect_metas : Evd.evar_map -> constr -> int list +val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t -val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *) +val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) (* Substitution of metavariables *) -type meta_value_map = (metavariable * constr) list -val subst_meta : meta_value_map -> constr -> constr -val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool +type meta_value_map = (metavariable * Constr.constr) list +val subst_meta : meta_value_map -> Constr.constr -> Constr.constr +val isMetaOf : Evd.evar_map -> metavariable -> constr -> bool (** Type assignment for metavariables *) -type meta_type_map = (metavariable * types) list +type meta_type_map = (metavariable * Constr.types) list (** [pop c] lifts by -1 the positive indexes in [c] *) -val pop : EConstr.t -> constr +val pop : constr -> constr (** {6 ... } *) (** Substitution of an arbitrary large term. Uses equality modulo @@ -145,37 +142,37 @@ val pop : EConstr.t -> constr (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr + (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> - EConstr.t -> EConstr.t -> EConstr.t -> constr + Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> + constr -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr +val subst_term : Evd.evar_map -> constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) -val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr +val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool -val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> - Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool -val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool (* FIXME rename: erases universes*) +val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) -> + Reduction.conv_pb -> constr -> constr -> bool +val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool +val eq_constr : Evd.evar_map -> constr -> constr -> bool (* FIXME rename: erases universes*) -val eta_reduce_head : constr -> constr +val eta_reduce_head : Evd.evar_map -> constr -> constr (** Flattens application lists *) -val collapse_appl : Evd.evar_map -> EConstr.t -> constr +val collapse_appl : Evd.evar_map -> constr -> constr -val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t +val prod_applist : Evd.evar_map -> constr -> constr list -> constr (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr +val strip_outer_cast : Evd.evar_map -> constr -> constr exception CannotFilter @@ -185,32 +182,32 @@ exception CannotFilter (context,term), or raises [CannotFilter]. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts. *) -type subst = (Context.Rel.t * constr) Evar.Map.t -val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst +type subst = (Context.Rel.t * Constr.constr) Evar.Map.t +val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst -val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr -val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr +val decompose_prod_letin : Evd.evar_map -> constr -> int * Context.Rel.t * constr +val align_prod_letin : Evd.evar_map -> constr -> constr -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : Evd.evar_map -> EConstr.t -> int +val nb_lam : Evd.evar_map -> constr -> int (** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : Evd.evar_map -> EConstr.t -> int +val nb_prod : Evd.evar_map -> constr -> int (** Similar to [nb_prod], but zeta-contracts let-in on the way *) -val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int +val nb_prod_modulo_zeta : Evd.evar_map -> constr -> int (** Get the last arg of a constr intended to be an application *) -val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr +val last_arg : Evd.evar_map -> constr -> constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array +val decompose_app_vect : Evd.evar_map -> constr -> constr * constr array -val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list -> - (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list) -val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> - (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array) +val adjust_app_list_size : constr -> constr list -> constr -> constr list -> + (constr * constr list * constr * constr list) +val adjust_app_array_size : constr -> constr array -> constr -> constr array -> + (constr * constr array * constr * constr array) (** name contexts *) type names_context = Name.t list @@ -239,15 +236,15 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env -val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list +val assums_of_rel_context : Context.Rel.t -> (Name.t * Constr.constr) list val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t -val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t +val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) val map_rel_context_in_env : - (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t val map_rel_context_with_binders : - (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t + (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t val fold_named_context_both_sides : ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> Context.Named.t -> init:'a -> 'a @@ -256,10 +253,10 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env -val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list -val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t +val global_vars : env -> Evd.evar_map -> constr -> Id.t list +val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option +val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -268,15 +265,15 @@ val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> I (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses +val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses -val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool +val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool -val isGlobalRef : Evd.evar_map -> EConstr.t -> bool +val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool +val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool -val is_Prop : Evd.evar_map -> EConstr.t -> bool +val is_Prop : Evd.evar_map -> constr -> bool (** Combinators on judgments *) @@ -285,5 +282,5 @@ val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) puns val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment (** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit +val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set -- cgit v1.2.3