diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/rawterm.ml | 9 | ||||
-rw-r--r-- | pretyping/rawterm.mli | 9 | ||||
-rw-r--r-- | pretyping/tacred.ml | 182 | ||||
-rw-r--r-- | pretyping/tacred.mli | 7 | ||||
-rw-r--r-- | pretyping/termops.ml | 56 | ||||
-rw-r--r-- | pretyping/termops.mli | 12 | ||||
-rw-r--r-- | pretyping/unification.ml | 3 |
7 files changed, 112 insertions, 166 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index fe48cd4fa..79708e9fb 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -335,7 +335,14 @@ let all_flags = type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a with_occurrences = int or_var list * 'a +type occurrences_expr = bool * int or_var list + +let all_occurrences_expr_but l = (false,l) +let no_occurrences_expr_but l = (true,l) +let all_occurrences_expr = (false,[]) +let no_occurrences_expr = (true,[]) + +type 'a with_occurrences = occurrences_expr * 'a type ('a,'b) red_expr_gen = | Red of bool diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index ab67a0922..0eee3e73a 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -146,7 +146,14 @@ val all_flags : 'a raw_red_flag type 'a or_var = ArgArg of 'a | ArgVar of identifier located -type 'a with_occurrences = int or_var list * 'a +type occurrences_expr = bool * int or_var list + +val all_occurrences_expr_but : int or_var list -> occurrences_expr +val no_occurrences_expr_but : int or_var list -> occurrences_expr +val all_occurrences_expr : occurrences_expr +val no_occurrences_expr : occurrences_expr + +type 'a with_occurrences = occurrences_expr * 'a type ('a,'b) red_expr_gen = | Red of bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 05d108673..47bc132ac 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -35,16 +35,23 @@ exception ReductionTacticError of reduction_tactic_error exception Elimconst exception Redelimination -let is_evaluable env ref = - match ref with - EvalConstRef kn -> - is_transparent (ConstKey kn) && - let cb = Environ.lookup_constant kn env in - cb.const_body <> None & not cb.const_opaque - | EvalVarRef id -> - is_transparent (VarKey id) && - let (_,value,_) = Environ.lookup_named id env in - value <> None +let is_evaluable env = function + | EvalConstRef kn -> + is_transparent (ConstKey kn) && + let cb = Environ.lookup_constant kn env in + cb.const_body <> None & not cb.const_opaque + | EvalVarRef id -> + is_transparent (VarKey id) && + let (_,value,_) = Environ.lookup_named id env in + value <> None + +let value_of_evaluable_ref env = function + | EvalConstRef con -> constant_value env con + | EvalVarRef id -> Option.get (pi2 (lookup_named id env)) + +let constr_of_evaluable_ref = function + | EvalConstRef con -> mkConst con + | EvalVarRef id -> mkVar id type evaluable_reference = | EvalConst of constant @@ -627,20 +634,16 @@ let is_head c t = | App (f,_) -> f = c | _ -> false -let contextually byhead (locs,c) f env sigma t = +let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - let except = List.exists (fun n -> n<0) locs in - if except & (List.exists (fun n -> n>=0) locs) - then error "mixing of positive and negative occurences" - else - let rec traverse (env,c as envc) t = - if locs <> [] & (not except) & (!pos > maxocc) then t + let rec traverse (env,c as envc) t = + if nowhere_except_in & (!pos > maxocc) then t else if (not byhead & eq_constr c t) or (byhead & is_head c t) then let ok = - if except then not (List.mem (- !pos) locs) - else (locs = [] or List.mem !pos locs) in + if nowhere_except_in then List.mem !pos locs + else not (List.mem !pos locs) in incr pos; if ok then f env sigma t @@ -656,112 +659,34 @@ let contextually byhead (locs,c) f env sigma t = traverse envc t in let t' = traverse (env,c) t in - if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then - error_invalid_occurrence locs; + if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; t' (* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurence of name. * ol is the occurence list to find. *) -let rec substlin env name n ol c = - match kind_of_term c with - | Const kn when EvalConstRef kn = name -> - if List.hd ol = n then - try - (n+1, List.tl ol, constant_value env kn) - with - NotEvaluableConst _ -> - errorlabstrm "substlin" - (pr_con kn ++ str " is not a defined constant") - else - ((n+1), ol, c) - - | Var id when EvalVarRef id = name -> - if List.hd ol = n then - match lookup_named id env with - | (_,Some c,_) -> (n+1, List.tl ol, c) - | _ -> - errorlabstrm "substlin" - (pr_id id ++ str " is not a defined constant") - else - ((n+1), ol, c) - - (* INEFFICIENT: OPTIMIZE *) - | App (c1,cl) -> - Array.fold_left - (fun (n1,ol1,c1') c2 -> - (match ol1 with - | [] -> (n1,[],applist(c1',[c2])) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,applist(c1',[c2'])))) - (substlin env name n ol c1) cl - - | Lambda (na,c1,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkLambda (na,c1',c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkLambda (na,c1',c2'))) - - | LetIn (na,c1,t,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkLetIn (na,c1',t,c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkLetIn (na,c1',t,c2'))) - - | Prod (na,c1,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkProd (na,c1',c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkProd (na,c1',c2'))) - - | Case (ci,p,d,llf) -> - let rec substlist nn oll = function - | [] -> (nn,oll,[]) - | f::lfe -> - let (nn1,oll1,f') = substlin env name nn oll f in - (match oll1 with - | [] -> (nn1,[],f'::lfe) - | _ -> - let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in - (nn2,oll2,f'::lfe')) - in - (* p is printed after d in v8 syntax *) - let (n1,ol1,d') = substlin env name n ol d in - (match ol1 with - | [] -> (n1,[],mkCase (ci, p, d', llf)) - | _ -> - let (n2,ol2,p') = substlin env name n1 ol1 p in - (match ol2 with - | [] -> (n2,[],mkCase (ci, p', d', llf)) - | _ -> - let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) - in (n3,ol3,mkCase (ci, p', d', Array.of_list lf')))) - - | Cast (c1,k,c2) -> - let (n1,ol1,c1') = substlin env name n ol c1 in - (match ol1 with - | [] -> (n1,[],mkCast (c1',k,c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkCast (c1',k,c2'))) - - | Fix _ -> - (Flags.if_verbose - warning "do not consider occurrences inside fixpoints"; (n,ol,c)) - - | CoFix _ -> - (Flags.if_verbose - warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) - | (Rel _|Meta _|Var _|Sort _ - |Evar _|Const _|Ind _|Construct _) -> (n,ol,c) +let substlin env evalref n (nowhere_except_in,locs) c = + let maxocc = List.fold_right max locs 0 in + let pos = ref n in + assert (List.for_all (fun x -> x >= 0) locs); + let value = value_of_evaluable_ref env evalref in + let term = constr_of_evaluable_ref evalref in + let rec substrec () c = + if nowhere_except_in & !pos > maxocc then c + else if c = term then + let ok = + if nowhere_except_in then List.mem !pos locs + else not (List.mem !pos locs) in + incr pos; + if ok then value else c + else + map_constr_with_binders_left_to_right + (fun _ () -> ()) + substrec () c + in + let t' = substrec () c in + (!pos, t') let string_of_evaluable_ref env = function | EvalVarRef id -> string_of_id id @@ -779,16 +704,15 @@ let unfold env sigma name = * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. * Performs a betaiota reduction after unfolding. *) -let unfoldoccs env sigma (occl,name) c = - match occl with - | [] -> unfold env sigma name c - | l -> - match substlin env name 1 (Sort.list (<) l) c with - | (_,[],uc) -> nf_betaiota uc - | (1,_,_) -> - error ((string_of_evaluable_ref env name)^" does not occur") - | (_,l,_) -> - error_invalid_occurrence l +let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = + if locs = [] then if nowhere_except_in then c else unfold env sigma name c + else + let (nbocc,uc) = substlin env name 1 plocs c in + if nbocc = 1 then + error ((string_of_evaluable_ref env name)^" does not occur"); + let rest = List.filter (fun o -> o >= nbocc) locs in + if rest <> [] then error_invalid_occurrence rest; + nf_betaiota uc (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 0ff5154f6..1516a2bd6 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -16,6 +16,7 @@ open Evd open Reductionops open Closure open Rawterm +open Termops (*i*) type reduction_tactic_error = @@ -47,13 +48,13 @@ val hnf_constr : reduction_function (* Unfold *) val unfoldn : - (int list * evaluable_global_reference) list -> reduction_function + (occurrences * evaluable_global_reference) list -> reduction_function (* Fold *) val fold_commands : constr list -> reduction_function (* Pattern *) -val pattern_occs : (int list * constr) list -> reduction_function +val pattern_occs : (occurrences * constr) list -> reduction_function (* Rem: Lazy strategies are defined in Reduction *) (* Call by value strategy (uses Closures) *) @@ -81,7 +82,7 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -val contextually : bool -> int list * constr -> reduction_function +val contextually : bool -> occurrences * constr -> reduction_function -> reduction_function (* Compatibility *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9a9e25c59..aa6c37491 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -621,32 +621,33 @@ let subst_term = subst_term_gen eq_constr let replace_term = replace_term_gen eq_constr -(* Substitute only a list of locations locs, the empty list is - interpreted as substitute all, if 0 is in the list then no - bindings is done. The list may contain only negative occurrences - that will not be substituted. *) +(* Substitute only at a list of locations or excluding a list of + locations; in the occurrences list (b,l), b=true means no + occurrence except the ones in l and b=false, means all occurrences + except the ones in l *) + +type occurrences = bool * int list +let all_occurrences = (false,[]) +let no_occurrences_in_set = (true,[]) let error_invalid_occurrence l = errorlabstrm "" (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ prlist_with_sep spc int l) -let subst_term_occ_gen locs occ c t = +let subst_term_occ_gen (nowhere_except_in,locs) occ c t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in - let except = List.exists (fun n -> n<0) locs in - if except & (List.exists (fun n -> n>=0) locs) - then error "mixing of positive and negative occurences" - else - let rec substrec (k,c as kc) t = - if (not except) & (!pos > maxocc) then t + 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 except then - if List.mem (- !pos) locs then t else (mkRel k) - else + 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 @@ -656,28 +657,27 @@ let subst_term_occ_gen locs occ c t = let t' = substrec (1,c) t in (!pos, t') -let subst_term_occ locs c t = - if locs = [] then subst_term c t - else if List.mem 0 locs then - 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 locs 1 c t in - let rest = List.filter (fun o -> o >= nbocc or o <= -nbocc) locs in + 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' -let subst_term_occ_decl locs c (id,bodyopt,typ as d) = +let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) = match bodyopt with - | None -> (id,None,subst_term_occ locs c typ) + | None -> (id,None,subst_term_occ plocs c typ) | Some body -> if locs = [] then - (id,Some (subst_term c body),subst_term c typ) - else if List.mem 0 locs then - d + if nowhere_except_in then + (id,Some (subst_term c body),subst_term c typ) + else + d else - let (nbocc,body') = subst_term_occ_gen locs 1 c body in - let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in - let rest = List.filter (fun o -> o >= nbocc' or o <= -nbocc') locs in + 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') diff --git a/pretyping/termops.mli b/pretyping/termops.mli index bc483cfc3..f80deab10 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -131,18 +131,24 @@ val subst_term : constr -> constr -> constr (* [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr +(* In occurrences sets, false = everywhere except and true = nowhere except *) +type occurrences = bool * int list +val all_occurrences : occurrences +val no_occurrences_in_set : occurrences + (* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_term_occ_gen : int list -> int -> constr -> types -> int * types +val subst_term_occ_gen : + occurrences -> int -> constr -> types -> int * types (* [subst_term_occ occl c d] replaces occurrences of [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_term_occ : int list -> constr -> constr -> constr +val subst_term_occ : occurrences -> constr -> constr -> constr (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at positions [occl] by [Rel 1] in [decl] *) val subst_term_occ_decl : - int list -> constr -> named_declaration -> named_declaration + occurrences -> constr -> named_declaration -> named_declaration val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ca1be55bb..41d6ff4c1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -44,7 +44,8 @@ let abstract_scheme env c l lname_typ = let abstract_list_all env evd typ c l = let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in + let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in + let p = abstract_scheme env c l_with_all_occs ctxt in try if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" |