summaryrefslogtreecommitdiff
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml298
1 files changed, 228 insertions, 70 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 70f2279c..6371fd3a 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: termops.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
@@ -34,7 +32,6 @@ let pr_name = function
| Name id -> pr_id id
| Anonymous -> str "_"
-let pr_path sp = str(string_of_kn sp)
let pr_con sp = str(string_of_con sp)
let rec pr_constr c = match kind_of_term c with
@@ -149,11 +146,13 @@ let print_env env =
let set_module m = current_module := m*)
-let new_univ =
+let new_univ_level =
let univ_gen = ref 0 in
(fun sp ->
incr univ_gen;
- Univ.make_univ (Lib.library_dp(),!univ_gen))
+ Univ.make_universe_level (Lib.library_dp(),!univ_gen))
+
+let new_univ () = Univ.make_universe (new_univ_level ())
let new_Type () = mkType (new_univ ())
let new_Type_sort () = Type (new_univ ())
@@ -238,18 +237,18 @@ let mkProd_wo_LetIn (na,body,t) c =
| None -> mkProd (na, t, c)
| Some b -> subst1 b c
-let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
-let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
let it_named_context_quantifier f ~init =
List.fold_left (fun c d -> f d c) init
-let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn
-let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn
-let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn
-let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
-let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
-let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
+let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
+let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
+let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
(* *)
@@ -265,11 +264,45 @@ let rec strip_head_cast c = match kind_of_term c with
| Cast (c,_,_) -> strip_head_cast c
| _ -> c
+let rec drop_extra_implicit_args c = match kind_of_term c with
+ (* Removed trailing extra implicit arguments, what improves compatibility
+ for constants with recently added maximal implicit arguments *)
+ | App (f,args) when isEvar (array_last args) ->
+ drop_extra_implicit_args
+ (mkApp (f,fst (array_chop (Array.length args - 1) args)))
+ | _ -> c
+
(* Get the last arg of an application *)
let last_arg c = match kind_of_term c with
| App (f,cl) -> array_last cl
| _ -> anomaly "last_arg"
+(* Get the last arg of an application *)
+let decompose_app_vect c =
+ match kind_of_term c with
+ | App (f,cl) -> (f, cl)
+ | _ -> (c,[||])
+
+let adjust_app_list_size f1 l1 f2 l2 =
+ let len1 = List.length l1 and len2 = List.length l2 in
+ if len1 = len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = list_chop (len2-len1) l2 in
+ (f1, l1, applist (f2,extras), restl2)
+ else
+ let extras,restl1 = list_chop (len1-len2) l1 in
+ (applist (f1,extras), restl1, f2, l2)
+
+let adjust_app_array_size f1 l1 f2 l2 =
+ let len1 = Array.length l1 and len2 = Array.length l2 in
+ if len1 = len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = array_chop (len2-len1) l2 in
+ (f1, l1, appvect (f2,extras), restl2)
+ else
+ let extras,restl1 = array_chop (len1-len2) l1 in
+ (appvect (f1,extras), restl1, f2, l2)
+
(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
subterms of [c]; it carries an extra data [l] (typically a name
list) which is processed by [g na] (which typically cons [na] to
@@ -523,6 +556,14 @@ let collect_metas c =
in
List.rev (collrec [] c)
+(* collects all vars; warning: this is only visible vars, not dependencies in
+ all section variables; for the latter, use global_vars_set *)
+let collect_vars c =
+ let rec aux vars c = match kind_of_term c with
+ | Var id -> Idset.add id vars
+ | _ -> fold_constr aux vars c in
+ aux Idset.empty c
+
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -546,6 +587,25 @@ let dependent_main noevar m t =
let dependent = dependent_main false
let dependent_no_evar = dependent_main true
+let count_occurrences m t =
+ let n = ref 0 in
+ let rec countrec m t =
+ if eq_constr m t then
+ incr n
+ else
+ match kind_of_term m, kind_of_term t with
+ | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+ 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 isMeta c -> ()
+ | _, Evar _ -> ()
+ | _ -> iter_constr_with_binders (lift 1) countrec m t
+ in
+ countrec m t;
+ !n
+
(* Synonymous *)
let occur_term = dependent
@@ -592,10 +652,9 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
None
| _ -> None
-(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
- [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
- term [c] in a term [t] *)
-(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
+(* Recognizing occurrences of a given subterm in a term: [subst_term c t]
+ substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
+ works if [c] has rels *)
let subst_term_gen eq_fun c t =
let rec substrec (k,c as kc) t =
@@ -608,10 +667,11 @@ let subst_term_gen eq_fun c t =
in
substrec (1,c) t
-(* Recognizing occurrences of a given (closed) subterm in a term :
- [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
- term [c1] in a term [t] *)
-(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
+let subst_term = subst_term_gen eq_constr
+
+(* Recognizing occurrences of a given subterm in a term :
+ [replace_term c1 c2 t] substitutes [c2] for all occurrences of
+ term [c1] in a term [t]; works if [c1] and [c2] have rels *)
let replace_term_gen eq_fun c by_c in_t =
let rec substrec (k,c as kc) t =
@@ -624,8 +684,6 @@ let replace_term_gen eq_fun c by_c in_t =
in
substrec (0,c) in_t
-let subst_term = subst_term_gen eq_constr
-
let replace_term = replace_term_gen eq_constr
(* Substitute only at a list of locations or excluding a list of
@@ -633,6 +691,11 @@ let replace_term = replace_term_gen eq_constr
occurrence except the ones in l and b=false, means all occurrences
except the ones in l *)
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+ | InHyp
+ | InHypTypeOnly
+ | InHypValueOnly
+
type occurrences = bool * int list
let all_occurrences = (false,[])
let no_occurrences_in_set = (true,[])
@@ -643,57 +706,127 @@ let error_invalid_occurrence l =
(str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
prlist_with_sep spc int l ++ str ".")
-let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
+let pr_position (cl,pos) =
+ let clpos = match cl with
+ | None -> str " of the goal"
+ | Some (id,InHyp) -> str " of hypothesis " ++ pr_id id
+ | Some (id,InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id
+ | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
+ int pos ++ clpos
+
+let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_except_in,locs) =
+ let s = if nested then "Found nested occurrences of the pattern"
+ else "Found incompatible occurrences of the pattern" in
+ errorlabstrm ""
+ (str s ++ str ":" ++
+ spc () ++ str "Matched term " ++ quote (print_constr t2) ++
+ strbrk " at position " ++ pr_position (cl2,pos2) ++
+ strbrk " is not compatible with matched term " ++
+ quote (print_constr t1) ++ strbrk " at position " ++
+ pr_position (cl1,pos1) ++ str ".")
+
+let is_selected pos (nowhere_except_in,locs) =
+ nowhere_except_in && List.mem pos locs ||
+ not nowhere_except_in && not (List.mem pos locs)
+
+exception NotUnifiable
+
+type 'a testing_function = {
+ match_fun : constr -> 'a;
+ merge_fun : 'a -> 'a -> 'a;
+ mutable testing_state : 'a;
+ mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+}
+
+let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t =
let maxocc = List.fold_right max locs 0 in
let pos = ref occ in
- assert (List.for_all (fun x -> x >= 0) locs);
- let rec substrec (k,c as kc) t =
- if nowhere_except_in & !pos > maxocc then t
- else
- if eq_constr c t then
- let r =
- if nowhere_except_in then
- if List.mem !pos locs then (mkRel k) else t
- else
- if List.mem !pos locs then t else (mkRel k)
- in incr pos; r
- else
- map_constr_with_binders_left_to_right
- (fun d (k,c) -> (k+1,lift 1 c))
- substrec kc t
+ let nested = ref false in
+ let add_subst t subst =
+ try
+ test.testing_state <- test.merge_fun subst test.testing_state;
+ test.last_found <- Some (cl,!pos,t)
+ with NotUnifiable ->
+ let lastpos = Option.get test.last_found in
+ error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in
+ let rec substrec k t =
+ if nowhere_except_in & !pos > maxocc then t else
+ try
+ let subst = test.match_fun t in
+ if is_selected !pos plocs then
+ (add_subst t subst; incr pos;
+ (* Check nested matching subterms *)
+ nested := true; ignore (subst_below k t); nested := false;
+ (* Do the effective substitution *)
+ mkRel k)
+ else
+ (incr pos; subst_below k t)
+ with NotUnifiable ->
+ subst_below k t
+ and subst_below k t =
+ map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
in
- let t' = substrec (1,c) t in
+ let t' = substrec 1 t in
(!pos, t')
-let subst_term_occ (nowhere_except_in,locs as plocs) c t =
- if locs = [] then if nowhere_except_in then t else subst_term c t
- else
- let (nbocc,t') = subst_term_occ_gen plocs 1 c t in
- let rest = List.filter (fun o -> o >= nbocc) locs in
- if rest <> [] then error_invalid_occurrence rest;
- t'
-
-type hyp_location_flag = (* To distinguish body and type of local defs *)
- | InHyp
- | InHypTypeOnly
- | InHypValueOnly
-
-let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
- match bodyopt,hloc with
- | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
- | None, _ -> (id,None,subst_term_occ plocs c typ)
- | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
- | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
+let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = []
+
+let check_used_occurrences nbocc (nowhere_except_in,locs) =
+ let rest = List.filter (fun o -> o >= nbocc) locs in
+ if rest <> [] then error_invalid_occurrence rest
+
+let proceed_with_occurrences f plocs x =
+ if is_nowhere plocs then (* optimization *) x else
+ begin
+ assert (List.for_all (fun x -> x >= 0) (snd plocs));
+ let (nbocc,x) = f 1 x in
+ check_used_occurrences nbocc plocs;
+ x
+ end
+
+let make_eq_test c = {
+ match_fun = (fun c' -> if eq_constr c c' then () else raise NotUnifiable);
+ merge_fun = (fun () () -> ());
+ testing_state = ();
+ last_found = None
+}
+
+let subst_closed_term_occ_gen plocs pos c t =
+ subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t
+
+let subst_closed_term_occ plocs c t =
+ proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c)
+ plocs t
+
+let subst_closed_term_occ_modulo plocs test cl t =
+ proceed_with_occurrences
+ (subst_closed_term_occ_gen_modulo plocs test cl) plocs t
+
+let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
+ let f = f (Some (id,hyploc)) in
+ match bodyopt,hyploc with
+ | None, InHypValueOnly ->
+ errorlabstrm "" (pr_id id ++ str " has no value.")
+ | None, _ | Some _, InHypTypeOnly ->
+ let acc,typ = f acc typ in acc,(id,bodyopt,typ)
+ | Some body, InHypValueOnly ->
+ let acc,body = f acc body in acc,(id,Some body,typ)
| Some body, InHyp ->
- if locs = [] then
- if nowhere_except_in then d
- else (id,Some (subst_term c body),subst_term c typ)
- else
- let (nbocc,body') = subst_term_occ_gen plocs 1 c body in
- let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in
- let rest = List.filter (fun o -> o >= nbocc') locs in
- if rest <> [] then error_invalid_occurrence rest;
- (id,Some body',t')
+ let acc,body = f acc body in
+ let acc,typ = f acc typ in
+ acc,(id,Some body,typ)
+
+let subst_closed_term_occ_decl (plocs,hyploc) c d =
+ proceed_with_occurrences
+ (map_named_declaration_with_hyploc
+ (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d
+
+let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d =
+ proceed_with_occurrences
+ (map_named_declaration_with_hyploc
+ (subst_closed_term_occ_gen_modulo plocs test)
+ hyploc)
+ plocs d
let vars_of_env env =
let s =
@@ -965,7 +1098,7 @@ let on_judgment_value f j = { j with uj_val = f j.uj_val }
let on_judgment_type f j = { j with uj_type = f j.uj_type }
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
- variables *)
+ variables; skips let-in's *)
let context_chop k ctx =
let rec chop_aux acc = function
| (0, l2) -> (List.rev acc, l2)
@@ -974,3 +1107,28 @@ let context_chop k ctx =
| (_, []) -> anomaly "context_chop"
in chop_aux [] (k,ctx)
+(* Do not skip let-in's *)
+let env_rel_context_chop k env =
+ let rels = rel_context env in
+ let ctx1,ctx2 = list_chop k rels in
+ push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
+ ctx1
+
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+let impossible_default_case = ref None
+
+let set_impossible_default_clause c = impossible_default_case := Some c
+
+let coq_unit_judge =
+ let na1 = Name (id_of_string "A") in
+ let na2 = Name (id_of_string "H") in
+ fun () ->
+ match !impossible_default_case with
+ | Some (id,type_of_id) ->
+ make_judge id type_of_id
+ | None ->
+ (* In case the constants id/ID are not defined *)
+ make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+ (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:41:59 +0000