diff options
43 files changed, 439 insertions, 471 deletions
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml index 23d4dea34..1db31269b 100644 --- a/contrib/correctness/peffect.ml +++ b/contrib/correctness/peffect.ml @@ -11,6 +11,7 @@ (* $Id$ *) open Names +open Nameops open Pmisc (* The type of effects. diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml index feee251ff..c3cc1ec64 100644 --- a/contrib/correctness/penv.ml +++ b/contrib/correctness/penv.ml @@ -14,6 +14,7 @@ open Pmisc open Past open Ptype open Names +open Nameops open Libobject open Library open Term diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml index 452e1b581..17c673a54 100644 --- a/contrib/correctness/perror.ml +++ b/contrib/correctness/perror.ml @@ -13,6 +13,7 @@ open Pp open Util open Names +open Nameops open Term open Himsg diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml index 682463238..122ff16ab 100644 --- a/contrib/correctness/prename.ml +++ b/contrib/correctness/prename.ml @@ -11,6 +11,7 @@ (* $Id$ *) open Names +open Nameops open Util open Pp open Himsg diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 77d261653..6b487348a 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -14,6 +14,7 @@ open Options open Names +open Nameops open Vernacentries open Reduction open Term diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index fecd577d7..5e454a252 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -12,6 +12,7 @@ open Util open Names +open Nameops open Term open Termops open Pattern diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 2fd997986..77e20c785 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Lib open Extraction diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 9aecdd4c4..132367de9 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -108,7 +108,7 @@ let sort_of env c = Retyping.get_sort_family_of env Evd.empty (strip_outer_cast c) open RedFlags -let whd_betaiotalet = clos_norm_flags (UNIFORM, mkflags [fBETA;fIOTA;fZETA]) +let whd_betaiotalet = clos_norm_flags (mkflags [fBETA;fIOTA;fZETA]) let is_axiom sp = (Global.lookup_constant sp).const_body = None diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 1043ecbdb..97258c506 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -815,12 +815,12 @@ let constants_to_unfold = open RedFlags let polynom_unfold_tac = let flags = - (UNIFORM, mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in + (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in reduct_in_concl (cbv_norm_flags flags) let polynom_unfold_tac_in_term gl = let flags = - (UNIFORM,mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold))) + (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold))) in cbv_norm_flags flags (pf_env gl) (project gl) diff --git a/kernel/closure.ml b/kernel/closure.ml index 3b2655af6..56ef7cafb 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -167,11 +167,11 @@ end : RedFlagsSig) open RedFlags -let betadeltaiota_red = mkflags [fBETA;fDELTA;fZETA;fIOTA] -let betadeltaiotanolet_red = mkflags [fBETA;fDELTA;fIOTA] -let betaiota_red = mkflags [fBETA;fIOTA] -let beta_red = mkflags [fBETA] -let betaiotazeta_red = mkflags [fBETA;fIOTA;fZETA] +let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA] +let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] +let betaiota = mkflags [fBETA;fIOTA] +let beta = mkflags [fBETA] +let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] let unfold_red sp = let flag = match sp with | EvalVarRef id -> fVAR id @@ -309,48 +309,6 @@ let red_get_const red = fin obsolète **************) (* specification of the reduction function *) -type red_mode = UNIFORM | SIMPL | WITHBACK - -type flags = red_mode * reds - -(* (UNIFORM,r) == r-reduce in any context - * (SIMPL,r) == bdi-reduce under cases or fix, r otherwise (like hnf does) - * (WITHBACK,r) == internal use: means we are under a case or in rec. arg. of - * fix - *) - -(* Examples *) -let no_flag = (UNIFORM,no_red) -let beta = (UNIFORM,beta_red) -let betaiota = (UNIFORM,betaiota_red) -let betadeltaiota = (UNIFORM,betadeltaiota_red) -let betadeltaiotanolet = (UNIFORM,betadeltaiotanolet_red) - -let hnf_flags = (SIMPL,betaiotazeta_red) -let unfold_flags sp = (UNIFORM, unfold_red sp) - -let flags_under = function - | (SIMPL,r) -> (WITHBACK,r) - | fl -> fl - - -(* Reductions allowed in "normal" circumstances: reduce only what is - * specified by r *) - -let red_top (_,r) rk = red_set r rk - -(* Sometimes, we may want to perform a bdi reduction, to generate new redexes. - * Typically: in the Simpl reduction, terms in recursive position of a fixpoint - * are bdi-reduced, even if r is weaker. - * - * It is important to keep in mind that when we talk of "normal" or - * "head normal" forms, it always refer to the reduction specified by r, - * whatever the term context. *) - -let red_under (md,r) rk = - match md with - | WITHBACK -> true - | _ -> red_set r rk (* Flags of reduction and cache of constants: 'a is a type that may be * mapped to constr. 'a infos implements a cache for constants and @@ -379,7 +337,7 @@ type table_key = (* FarRel: index in the rel_context part of _initial_ environment *) type 'a infos = { - i_flags : flags; + i_flags : reds; i_repr : 'a infos -> constr -> 'a; i_env : env; i_rels : int * (int * constr) list; @@ -437,9 +395,6 @@ let create mk_cl flgs env = i_tab = Hashtbl.create 17 } -let infos_under infos = { infos with i_flags = flags_under infos.i_flags } - - (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) @@ -472,14 +427,6 @@ let rec stack_args_size = function | Zupdate(_)::s -> stack_args_size s | _ -> 0 -(* Parameterization: check the a given reduction is allowed in the - context of the stack *) -let can_red info stk r = - red_top info.i_flags r || - (fst info.i_flags = SIMPL && - List.exists (function (Zcase _|Zfix _) -> true | _ -> false) stk) - - (* When used as an argument stack (only Zapp can appear) *) let rec decomp_stack = function | Zapp[v]::s -> Some (v, s) @@ -953,23 +900,23 @@ and knht e t stk = (* Computes a normal form from the result of knh. *) let rec knr info m stk = match m.term with - | FLambda(_,_,_,f,e) when can_red info stk fBETA -> + | FLambda(_,_,_,f,e) when red_set info.i_flags fBETA -> (match get_arg m stk with (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s | (None,s) -> (m,s)) - | FFlex(ConstKey sp) when can_red info stk (fCONST sp) -> + | FFlex(ConstKey sp) when red_set info.i_flags (fCONST sp) -> (match ref_value_cache info (ConstKey sp) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FFlex(VarKey id) when can_red info stk (fVAR id) -> + | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info (VarKey id) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FFlex(FarRelKey k) when can_red info stk fDELTA -> + | FFlex(FarRelKey k) when red_set info.i_flags fDELTA -> (match ref_value_cache info (FarRelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct(ind,c) when can_red info stk fIOTA -> + | FConstruct(ind,c) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with (depth, args, Zcase(ci,_,br)::s) -> assert (ci.ci_npar>=0); @@ -981,13 +928,13 @@ let rec knr info m stk = let efx = contract_fix_vect fx.term in kni info efx stk' | (_,args,s) -> (m,args@s)) - | FCoFix _ when can_red info stk fIOTA -> + | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with (_, args, ((Zcase _::_) as stk')) -> let efx = contract_fix_vect m.term in kni info efx (args@stk') | (_,args,s) -> (m,args@s)) - | FLetIn (_,v,_,_,bd,e) when can_red info stk fZETA -> + | FLetIn (_,v,_,_,bd,e) when red_set info.i_flags fZETA -> knit info (subs_cons(v,e)) bd stk | _ -> (m,stk) @@ -1048,6 +995,8 @@ let norm_val info v = let inject = mk_clos (ESID 0) +let whd_stack = kni + (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos @@ -1055,24 +1004,3 @@ let create_clos_infos flgs env = create (fun _ -> inject) flgs env let unfold_reference = ref_value_cache - -(* Head normal form. *) - -(* TODO: optimise *) -let rec strip_applstack k acc m = - match m.term with - FApp(a,b) -> - strip_applstack k (append_stack (lift_fconstr_vect k b) acc) a - | FLIFT(n,a) -> - strip_applstack (k+n) acc a - | FCLOS _ -> assert false - | _ -> (k,m,acc) - - -let fhnf info v = - strip_applstack 0 [] (kh info v []) - - -let fhnf_apply info k head appl = - let stk = zshift k appl in - strip_applstack 0 [] (kh info head stk) diff --git a/kernel/closure.mli b/kernel/closure.mli index 96c86b05f..54c1328b4 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -78,36 +78,13 @@ end module RedFlags : RedFlagsSig open RedFlags -val beta_red : reds -val betaiota_red : reds -val betadeltaiota_red : reds -val betaiotazeta_red : reds -val betadeltaiotanolet_red : reds +val beta : reds +val betaiota : reds +val betadeltaiota : reds +val betaiotazeta : reds +val betadeltaiotanolet : reds -(*s Reduction function specification. *) - -type red_mode = UNIFORM | SIMPL | WITHBACK - -type flags = red_mode * reds - -(* [(UNIFORM,r)] == [r]-reduce in any context. - [(SIMPL,r)] == bdi-reduce under cases or fix, [r] otherwise - (like hnf does). - [(WITHBACK,r)] == internal use: means we are under a case - or in rec. arg. of fix. *) - -val flags_under : flags -> flags -val red_top : flags -> red_kind -> bool -val red_under : flags -> red_kind -> bool - -val no_flag : flags -val beta : flags -val betaiota : flags -val betadeltaiota : flags -val betadeltaiotanolet : flags - -val hnf_flags : flags -val unfold_flags : evaluable_global_reference -> flags +val unfold_red : evaluable_global_reference -> reds (***********************************************************************) @@ -119,9 +96,8 @@ type table_key = type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option -val info_flags: 'a infos -> flags -val infos_under: 'a infos -> 'a infos -val create: ('a infos -> constr -> 'a) -> flags -> env -> 'a infos +val info_flags: 'a infos -> reds +val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos (***********************************************************************) (*s A [stack] is a context of arguments, arguments are pushed by @@ -181,8 +157,8 @@ type fterm = | FLOCKED -(* To lazy reduce a constr, create a ['a clos_infos] with - [create_cbv_infos], inject the term to reduce with [inject]; then use +(* To lazy reduce a constr, create a [clos_infos] with + [create_clos_infos], inject the term to reduce with [inject]; then use a reduction function *) val inject : constr -> fconstr @@ -191,7 +167,7 @@ val term_of_fconstr : fconstr -> constr (* Global and local constant cache *) type clos_infos -val create_clos_infos : flags -> env -> clos_infos +val create_clos_infos : reds -> env -> clos_infos (* Reduction function *) @@ -201,14 +177,12 @@ val norm_val : clos_infos -> fconstr -> constr (* [whd_val] is for weak head normalization *) val whd_val : clos_infos -> fconstr -> constr -(* Conversion auxiliary functions to do step by step normalisation *) - -(* [fhnf] and [fnf_apply] are for weak head normalization but staying - in [fconstr] world to perform step by step weak head normalization *) +(* [whd_stack] performs weak head normalization in a given stack. It + stops whenever a reduction is blocked. *) +val whd_stack : + clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack -val fhnf: clos_infos -> fconstr -> int * fconstr * fconstr stack -val fhnf_apply : clos_infos -> - int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack +(* Conversion auxiliary functions to do step by step normalisation *) (* [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> table_key -> fconstr option @@ -216,20 +190,19 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (***********************************************************************) (*i This is for lazy debug *) -val lift_fconstr : int -> fconstr -> fconstr +val lift_fconstr : int -> fconstr -> fconstr val lift_fconstr_vect : int -> fconstr array -> fconstr array -val mk_clos : fconstr subs -> constr -> fconstr +val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array val mk_clos_deep : (fconstr subs -> constr -> fconstr) -> fconstr subs -> constr -> fconstr -val knr: clos_infos -> fconstr -> fconstr stack -> - fconstr * fconstr stack -val kl: clos_infos -> fconstr -> fconstr +val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack +val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack +val kl : clos_infos -> fconstr -> fconstr -val to_constr : - (lift -> fconstr -> constr) -> lift -> fconstr -> constr +val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr (* End of cbn debug section i*) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml new file mode 100644 index 000000000..350e1a5a0 --- /dev/null +++ b/kernel/conv_oracle.ml @@ -0,0 +1,47 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Names +open Closure + +(* Opaque constants *) +let cst_transp = ref Sppred.full + +let set_opaque_const sp = cst_transp := Sppred.remove sp !cst_transp +let set_transparent_const sp = cst_transp := Sppred.add sp !cst_transp + +let is_opaque_cst sp = not (Sppred.mem sp !cst_transp) + +(* Unfold the first only if it is not opaque and the second is + opaque *) +let const_order sp1 sp2 = is_opaque_cst sp2 & not (is_opaque_cst sp1) + +(* Opaque variables *) +let var_transp = ref Idpred.full + +let set_opaque_var sp = var_transp := Idpred.remove sp !var_transp +let set_transparent_var sp = var_transp := Idpred.add sp !var_transp + +let is_opaque_var sp = not (Idpred.mem sp !var_transp) + +let var_order id1 id2 = is_opaque_var id2 & not (is_opaque_var id1) + +(* *) +let oracle_order k1 k2 = + match (k1,k2) with + (ConstKey sp1, ConstKey sp2) -> const_order sp1 sp2 + | (VarKey id1, VarKey id2) -> var_order id1 id2 + | _ -> false + +(* summary operations *) + +let init() = (cst_transp := Sppred.full; var_transp := Idpred.full) +let freeze () = (!var_transp, !cst_transp) +let unfreeze (vo,co) = (cst_transp := co; var_transp := vo) diff --git a/library/opaque.mli b/kernel/conv_oracle.mli index 7277cb66f..94da48d4d 100644 --- a/library/opaque.mli +++ b/kernel/conv_oracle.mli @@ -6,25 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) +(* $Id$ *) -(*i*) open Names open Closure -open Safe_typing -open Environ -(*i*) -(* The current set of transparent constants and variables *) -val state : unit -> transparent_state +(* Order on section paths for unfolding. + If oracle_order sp1 sp2 is true, then unfold sp1 first. + Note: the oracle does not introduce incompleteness, it only + tries to postpone unfolding of "opaque" constants. *) +val oracle_order : table_key -> table_key -> bool -(* returns true if the global reference has a definition and that is - has not been set opaque *) -val is_evaluable : env -> evaluable_global_reference -> bool - -(* Modifying this state *) -val set_opaque_const : section_path -> unit +(* Changing the oracle *) +val set_opaque_const : section_path -> unit val set_transparent_const : section_path -> unit -val set_opaque_var : identifier -> unit +val set_opaque_var : identifier -> unit val set_transparent_var : identifier -> unit + +(*****************************) + +(* transparent state summary operations *) +val init : unit -> unit +val freeze : unit -> transparent_state +val unfreeze : transparent_state -> unit diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c9399925b..7a01a6dc3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -321,24 +321,6 @@ let check_case_info env indsp ci = (* A powerful notion of subterm *) -let find_sorted_assoc p = - let rec findrec = function - | (a,ta)::l -> - if a < p then findrec l else if a = p then ta else raise Not_found - | _ -> raise Not_found - in - findrec - -let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) -let map_lift_fst = map_lift_fst_n 1 - -let rec instantiate_recarg sp lrc ra = - match ra with - | Mrec(j) -> Imbr((sp,j),lrc) - | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l) - | Norec -> Norec - | Param(k) -> List.nth lrc k - (* To each inductive definition corresponds an array describing the structure of recursive arguments for each constructor, we call it the recursive spec of the type (it has type recargs vect). For @@ -350,6 +332,16 @@ let rec instantiate_recarg sp lrc ra = first argument. *) +let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) +let map_lift_fst = map_lift_fst_n 1 + +let rec instantiate_recarg sp lrc ra = + match ra with + | Mrec(j) -> Imbr((sp,j),lrc) + | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l) + | Norec -> Norec + | Param(k) -> List.nth lrc k + (* f is a function of type env -> int -> (int * recargs) list -> constr -> 'a @@ -390,6 +382,14 @@ let is_inst_var k c = | Rel n -> n=k | _ -> false +let find_sorted_assoc p = + let rec findrec = function + | (a,ta)::l -> + if a < p then findrec l else if a = p then ta else raise Not_found + | _ -> raise Not_found + in + findrec + (* is_subterm_specif env lcx mind_recvec n lst c @@ -514,7 +514,8 @@ let rec check_subterm_rec_meta env vectn k def = (* n gives the index of the recursive variable *) (noccur_with_meta (n+k+1) nfi t) or (* no recursive call in the term *) - (let f,l = hnf_stack env t in + (* Rq: why not try and expand some definitions ? *) + (let f,l = decompose_app (whd_betaiotazeta env t) in match kind_of_term f with | Rel p -> if n+k+1 <= p & p < n+k+nfi+1 then diff --git a/kernel/names.ml b/kernel/names.ml index b91c6b08c..7e9d9ecf3 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -40,31 +40,13 @@ module Idset = Set.Make(IdOrdered) module Idmap = Map.Make(IdOrdered) module Idpred = Predicate.Make(IdOrdered) -let pr_id id = [< 'sTR (string_of_id id) >] - -let wildcard = id_of_string "_" - (* Names *) type name = Name of identifier | Anonymous -(*s Directory paths = section names paths *) -let parse_fields s = - let len = String.length s in - let rec decoupe_dirs n = - try - let pos = String.index_from s n '.' in - let dir = String.sub s n (pos-n) in - let dirs,n' = decoupe_dirs (succ pos) in - (id_of_string dir)::dirs,n' - with - | Not_found -> [],n - in - if len = 0 then invalid_arg "parse_section_path"; - let dirs,n = decoupe_dirs 0 in - let id = String.sub s n (len-n) in - dirs, (id_of_string id) - +(* Dirpaths are lists of module identifiers. The actual representation + is reversed to optimise sharing: Coq.A.B is ["B";"A";"Coq"] *) + type module_ident = identifier type dir_path = module_ident list @@ -84,8 +66,6 @@ let string_of_dirpath = function | sl -> String.concat "." (List.map string_of_id (List.rev sl)) -let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >] - (*s Section paths are absolute names *) type section_path = { diff --git a/kernel/names.mli b/kernel/names.mli index 5a01c2d86..7f410149c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -15,7 +15,6 @@ type name = Name of identifier | Anonymous (* Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier -val pr_id : identifier -> Pp.std_ppcmds (* Identifiers sets and maps *) module Idset : Set.S with type elt = identifier @@ -24,17 +23,17 @@ module Idmap : Map.S with type key = identifier (*s Directory paths = section names paths *) type module_ident = identifier -type dir_path - module ModIdmap : Map.S with type key = module_ident -(* Inner modules idents on top of list *) +type dir_path + +(* Inner modules idents on top of list (to improve sharing). + For instance: A.B.C is ["C";"B";"A"] *) val make_dirpath : module_ident list -> dir_path val repr_dirpath : dir_path -> module_ident list (* Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string -val pr_dirpath : dir_path -> Pp.std_ppcmds (*s Section paths are {\em absolute} names *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4e99446b6..a5b773c24 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -17,6 +17,58 @@ open Environ open Closure open Esubst +let rec is_empty_stack = function + [] -> true + | Zupdate _::s -> is_empty_stack s + | Zshift _::s -> is_empty_stack s + | _ -> false + +(* Compute the lift to be performed on a term placed in a given stack *) +let el_stack el stk = + let n = + List.fold_left + (fun i z -> + match z with + Zshift n -> i+n + | _ -> i) + 0 + stk in + el_shft n el + +let compare_stack_shape stk1 stk2 = + let rec compare_rec bal stk1 stk2 = + match (stk1,stk2) with + ([],[]) -> bal=0 + | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2 + | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 + | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2 + | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2 + | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) -> + bal=0 && c1.ci_ind = c2.ci_ind && compare_rec 0 s1 s2 + | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> + bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 + | (_,_) -> false in + compare_rec 0 stk1 stk2 + +let pure_stack lfts stk = + let rec pure_rec lfts stk = + match stk with + [] -> (lfts,[]) + | zi::s -> + (match (zi,pure_rec lfts s) with + (Zupdate _,lpstk) -> lpstk + | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) + | (Zapp a1,(l,Zapp a2::pstk)) -> + (l,Zapp (List.map (fun t -> (l,t)) a1 @ a2)::pstk) + | (Zapp a, (l,pstk)) -> + (l,Zapp (List.map (fun t -> (l,t)) a)::pstk) + | (Zfix(fx,a),(l,pstk)) -> + let (lfx,pa) = pure_rec l a in + (l, Zfix((lfx,fx),pa)::pstk) + | (Zcase(ci,p,br),(l,pstk)) -> + (l,Zcase(ci,(l,p),Array.map (fun t -> (l,t)) br)::pstk)) in + snd (pure_rec lfts stk) + (****************************************************************************) (* Reduction Functions *) (****************************************************************************) @@ -24,9 +76,8 @@ open Esubst let nf_betaiota t = norm_val (create_clos_infos betaiota empty_env) (inject t) -let hnf_stack env x = - decompose_app - (norm_val (create_clos_infos hnf_flags env) (inject x)) +let whd_betaiotazeta env x = + whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_betadeltaiota env t = whd_val (create_clos_infos betadeltaiota env) (inject t) @@ -43,30 +94,35 @@ let beta_appvect c v = | _ -> app_stack (substl env t, stack) in stacklam [] c (append_stack v empty_stack) -(* pseudo-reduction rule: - * [hnf_prod_app env s (Prod(_,B)) N --> B[N] - * with an HNF on the first argument to produce a product. - * if this does not work, then we use the string S as part of our - * error message. *) - -let hnf_prod_app env t n = - match kind_of_term (whd_betadeltaiota env t) with - | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: Need a product" - -let hnf_prod_applist env t nl = - List.fold_left (hnf_prod_app env) t nl - (********************************************************************) (* Conversion *) (********************************************************************) (* Conversion utility functions *) -type 'a conversion_function = env -> 'a -> 'a -> constraints +type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints exception NotConvertible exception NotConvertibleVect of int +let compare_stacks f lft1 stk1 lft2 stk2 cuniv = + let rec cmp_rec pstk1 pstk2 cuniv = + match (pstk1,pstk2) with + | (z1::s1, z2::s2) -> + let c1 = cmp_rec s1 s2 cuniv in + (match (z1,z2) with + | (Zapp a1,Zapp a2) -> List.fold_right2 f a1 a2 c1 + | (Zfix(fx1,a1),Zfix(fx2,a2)) -> + let c2 = f fx1 fx2 c1 in + cmp_rec a1 a2 c2 + | (Zcase(ci1,p1,br1),Zcase(ci2,p2,br2)) -> + let c2 = f p1 p2 c1 in + array_fold_right2 f br1 br2 c2 + | _ -> assert false) + | _ -> cuniv in + if compare_stack_shape stk1 stk2 then + cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv + else raise NotConvertible + (* Convertibility of sorts *) type conv_pb = @@ -86,24 +142,27 @@ let sort_cmp pb s0 s1 cuniv = | CUMUL -> enforce_geq u2 u1 cuniv) | (_, _) -> raise NotConvertible + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = - eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv + eqappr cv_pb infos + (lft1, whd_stack infos term1 []) + (lft2, whd_stack infos term2 []) + cuniv -(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *) +(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb infos appr1 appr2 cuniv = - let (lft1,(n1,hd1,v1)) = appr1 - and (lft2,(n2,hd2,v2)) = appr2 in - let el1 = el_shft n1 lft1 - and el2 = el_shft n2 lft2 in + let (lft1,(hd1,v1)) = appr1 in + let (lft2,(hd2,v2)) = appr2 in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> (match kind_of_term a1, kind_of_term a2 with | (Sort s1, Sort s2) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then sort_cmp cv_pb s1 s2 cuniv - else raise NotConvertible + assert (is_empty_stack v1 && is_empty_stack v2); + sort_cmp cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if n=m then convert_stacks infos lft1 lft2 v1 v2 cuniv @@ -111,8 +170,8 @@ and eqappr cv_pb infos appr1 appr2 cuniv = | _ -> raise NotConvertible) | (FEvar (ev1,args1), FEvar (ev2,args2)) -> if ev1=ev2 then - let u1 = convert_vect infos el1 el2 args1 args2 cuniv in - convert_stacks infos lft1 lft2 v1 v2 u1 + let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in + convert_vect infos el1 el2 args1 args2 u1 else raise NotConvertible (* 2 index known to be bound to no constant *) @@ -121,70 +180,65 @@ and eqappr cv_pb infos appr1 appr2 cuniv = then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *) + (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) if fl1 = fl2 - then - convert_stacks infos lft1 lft2 v1 v2 cuniv + then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible with NotConvertible -> - (* else expand the second occurrence (arbitrary heuristic) *) - match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb infos appr1 - (lft2, fhnf_apply infos n2 def2 v2) cuniv - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr cv_pb infos - (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv - | None -> raise NotConvertible)) - - (* only one constant, existential, defined var or defined rel *) + (* else the oracle tells which constant is to be expanded *) + let (app1,app2) = + if Conv_oracle.oracle_order fl1 fl2 then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) + else + match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> raise NotConvertible) in + eqappr cv_pb infos app1 app2 cuniv) + + (* only one constant, defined var or defined rel *) | (FFlex fl1, _) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) - appr2 cuniv + eqappr cv_pb infos (lft1, whd_stack infos def1 v1) appr2 cuniv | None -> raise NotConvertible) | (_, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb infos appr1 - (lft2, fhnf_apply infos n2 def2 v2) - cuniv + eqappr cv_pb infos appr1 (lft2, whd_stack infos def2 v2) cuniv | None -> raise NotConvertible) (* other constructors *) | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then - let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in - ccnv CONV infos - (el_lift el1) (el_lift el2) c2 c'2 u1 - else raise NotConvertible - - | (FLetIn _, _) | (_, FLetIn _) -> - anomaly "LetIn normally removed by fhnf" + assert (is_empty_stack v1 && is_empty_stack v2); + let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in + ccnv CONV infos (el_lift el1) (el_lift el2) c2 c'2 u1 | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then (* Luo's system *) - let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1 - else raise NotConvertible + assert (is_empty_stack v1 && is_empty_stack v2); + (* Luo's system *) + let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in + ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1 (* Inductive types: MutInd MutConstruct MutCase Fix Cofix *) (* Les annotations du MutCase ne servent qu'à l'affichage *) - +(* | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) -> let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in convert_stacks infos lft1 lft2 v1 v2 u3 - +*) | (FInd op1, FInd op2) -> if op1 = op2 then convert_stacks infos lft1 lft2 v1 v2 cuniv @@ -218,15 +272,17 @@ and eqappr cv_pb infos appr1 appr2 cuniv = convert_stacks infos lft1 lft2 v1 v2 u2 else raise NotConvertible + | ( (FLetIn _, _) | (_, FLetIn _) | (FCases _,_) | (_,FCases _) + | (FApp _,_) | (_,FApp _) | (FCLOS _, _) | (_,FCLOS _) + | (FLIFT _, _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED)) -> + anomaly "Unexpected term returned by fhnf" + | _ -> raise NotConvertible and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = - match (decomp_stack stk1, decomp_stack stk2) with - (Some(a1,s1), Some(a2,s2)) -> - let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in - convert_stacks infos lft1 lft2 s1 s2 u1 - | (None, None) -> cuniv - | _ -> raise NotConvertible + compare_stacks + (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c) + lft1 stk1 lft2 stk2 cuniv and convert_vect infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in @@ -247,12 +303,12 @@ let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then Constraint.empty else - let infos = create_clos_infos hnf_flags env in + let infos = create_clos_infos betaiotazeta env in ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty -let conv env = fconv CONV env -let conv_leq env = fconv CUMUL env +let conv = fconv CONV +let conv_leq = fconv CUMUL let conv_leq_vecti env v1 v2 = array_fold_left2_i @@ -279,6 +335,20 @@ let conv env t1 t2 = (* Special-Purpose Reduction *) (********************************************************************) +(* pseudo-reduction rule: + * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * with an HNF on the first argument to produce a product. + * if this does not work, then we use the string S as part of our + * error message. *) + +let hnf_prod_app env t n = + match kind_of_term (whd_betadeltaiota env t) with + | Prod (_,_,b) -> subst1 n b + | _ -> anomaly "hnf_prod_app: Need a product" + +let hnf_prod_applist env t nl = + List.fold_left (hnf_prod_app env) t nl + (* Dealing with arities *) let dest_prod env = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9ac3d8042..50371e85f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -16,15 +16,11 @@ open Environ (***********************************************************************) (*s Reduction functions *) +val whd_betaiotazeta : env -> constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr val nf_betaiota : constr -> constr -val hnf_stack : env -> constr -> constr * constr list -val hnf_prod_applist : env -> types -> constr list -> types - -(* Builds an application node, reducing beta redexes it may produce. *) -val beta_appvect : constr -> constr array -> constr (***********************************************************************) (*s conversion functions *) @@ -38,6 +34,15 @@ val conv_leq : types conversion_function val conv_leq_vecti : types array conversion_function (***********************************************************************) + +(* Builds an application node, reducing beta redexes it may produce. *) +val beta_appvect : constr -> constr array -> constr + +(* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) +val hnf_prod_applist : env -> types -> constr list -> types + + +(***********************************************************************) (*s Recognizing products and arities modulo reduction *) val dest_prod : env -> types -> Sign.rel_context * types diff --git a/lib/util.ml b/lib/util.ml index 743550481..30e64307d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -342,6 +342,16 @@ let array_fold_left_i f v a = let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in fold 0 v +let array_fold_right2 f v1 v2 a = + let lv1 = Array.length v1 in + let rec fold a n = + if n=0 then a + else + let k = n-1 in + fold (f v1.(k) v2.(k) a) k in + if Array.length v2 <> lv1 then invalid_arg "array_fold_right2"; + fold a lv1 + let array_fold_left2 f a v1 v2 = let lv1 = Array.length v1 in let rec fold a n = diff --git a/lib/util.mli b/lib/util.mli index bbf5cf240..7bd7d71c4 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -107,6 +107,8 @@ val array_cons : 'a -> 'a array -> 'a array val array_fold_right_i : (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a +val array_fold_right2 : + ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left2_i : diff --git a/library/nameops.ml b/library/nameops.ml index b7609bafd..0bcaeffbc 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -8,6 +8,7 @@ (* $Id$ *) +open Pp open Util open Names open Declarations @@ -16,6 +17,8 @@ open Term (* Identifiers *) +let pr_id id = [< 'sTR (string_of_id id) >] + let wildcard = id_of_string "_" (* Utilities *) @@ -141,6 +144,9 @@ let next_name_away name l = | Anonymous -> id_of_string "_" (**********************************************) + +let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >] + (* Operations on dirpaths *) let empty_dirpath = make_dirpath [] diff --git a/library/nameops.mli b/library/nameops.mli index fc5bc6a6a..b0376723b 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -13,6 +13,7 @@ open Term open Environ (* Identifiers and names *) +val pr_id : identifier -> Pp.std_ppcmds val wildcard : identifier val make_ident : string -> int option -> identifier @@ -34,6 +35,7 @@ val next_name_away_with_default : val out_name : name -> identifier (* Section and module mechanism: dealinng with dir paths *) +val pr_dirpath : dir_path -> Pp.std_ppcmds val empty_dirpath : dir_path val default_module : dir_path diff --git a/library/opaque.ml b/library/opaque.ml deleted file mode 100644 index ff551ce55..000000000 --- a/library/opaque.ml +++ /dev/null @@ -1,64 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ *) - -(*i*) -open Util -open Pp -open Names -open Closure -open Summary -open Term -open Declarations -(*i*) - -let tr_state = ref all_transparent - -let state () = !tr_state - -let _ = - declare_summary "Transparent constants and variables" - { freeze_function = state; - unfreeze_function = (fun ts -> tr_state := ts); - init_function = (fun () -> tr_state := all_transparent); - survive_section = false } - -let is_evaluable env ref = - match ref with - EvalConstRef sp -> - let (ids,sps) = !tr_state in - Sppred.mem sp sps & - let cb = Environ.lookup_constant sp env in - cb.const_body <> None & not cb.const_opaque - | EvalVarRef id -> - let (ids,sps) = !tr_state in - Idpred.mem id ids & - let (_,value,_) = Environ.lookup_named id env in - value <> None - -(* Modifying this state *) -let set_opaque_const sp = - let (ids,sps) = !tr_state in - tr_state := (ids, Sppred.remove sp sps) -let set_transparent_const sp = - let (ids,sps) = !tr_state in - let cb = Global.lookup_constant sp in - if cb.const_body <> None & cb.const_opaque then - errorlabstrm "set_transparent_const" - [< 'sTR "Cannot make"; 'sPC; - Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp); - 'sPC; 'sTR "transparent because it was declared opaque." >]; - tr_state := (ids, Sppred.add sp sps) - -let set_opaque_var id = - let (ids,sps) = !tr_state in - tr_state := (Idpred.remove id ids, sps) -let set_transparent_var id = - let (ids,sps) = !tr_state in - tr_state := (Idpred.add id ids, sps) diff --git a/parsing/ast.ml b/parsing/ast.ml index dc751186f..1830e45e9 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -104,15 +104,16 @@ let rec print_ast ast = match ast with | Num(_,n) -> [< 'iNT n >] | Str(_,s) -> [< 'qS s >] - | Path(_,sl) -> [< pr_sp sl >] + | Path(_,sl) -> [< 'sTR(string_of_path sl) >] | Id (_,s) -> [< 'sTR"{" ; 'sTR s ; 'sTR"}" >] - | Nvar(_,s) -> [< pr_id s >] + | Nvar(_,s) -> [< 'sTR(string_of_id s) >] | Nmeta(_,s) -> [< 'sTR s >] | Node(_,op,l) -> hOV 3 [< 'sTR"(" ; 'sTR op ; 'sPC ; print_astl l; 'sTR")" >] | Slam(_,None,ast) -> hOV 1 [< 'sTR"[<>]"; print_ast ast >] | Slam(_,Some x,ast) -> - hOV 1 [< 'sTR"["; pr_id x; 'sTR"]"; 'cUT; print_ast ast >] + hOV 1 + [< 'sTR"["; 'sTR(string_of_id x); 'sTR"]"; 'cUT; print_ast ast >] | Smetalam(_,id,ast) -> hOV 1 [< 'sTR id; print_ast ast >] | Dynamic(_,d) -> hOV 0 [< 'sTR"<dynamic: "; 'sTR(Dyn.tag d); 'sTR">" >] @@ -138,7 +139,8 @@ let rec print_astpat = function hOV 2 [< 'sTR"(" ; 'sTR op; 'sPC; print_astlpat al; 'sTR")" >] | Pslam(None,b) -> hOV 1 [< 'sTR"[<>]"; 'cUT; print_astpat b >] | Pslam(Some id,b) -> - hOV 1 [< 'sTR"["; pr_id id; 'sTR"]"; 'cUT; print_astpat b >] + hOV 1 + [< 'sTR"["; 'sTR(string_of_id id); 'sTR"]"; 'cUT; print_astpat b >] and print_astlpat = function | Pnil -> [< >] diff --git a/parsing/printer.ml b/parsing/printer.ml index 76c0995a5..77d0f59a1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Termops open Sign diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 96af71ce6..fa1d9fa3a 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -91,6 +91,11 @@ let contract_cofixp env (i,(_,_,bds as bodies)) = in subst_bodies_from_i 0 env, bds.(i) +let make_constr_ref n = function + | FarRelKey p -> mkRel (n+p) + | VarKey id -> mkVar id + | ConstKey cst -> mkConst cst + (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context @@ -119,27 +124,13 @@ let stack_app appl stack = | (_, APP(args,stk)) -> APP(appl@args,stk) | _ -> APP(appl, stack) -(* Tests if we are in a case (modulo some applications) *) -let under_case_stack = function - | (CASE _ | APP(_,CASE _)) -> true - | _ -> false - -(* Tells if the reduction rk is allowed by flags under a given stack. - * The stack is useful when flags is (SIMPL,r) because in that case, - * we perform bdi-reduction under the Case, or r-reduction otherwise - *) -let red_allowed flags stack rk = - if under_case_stack stack then - red_under flags rk - else - red_top flags rk open RedFlags -let red_allowed_ref flags stack = function - | FarRelKey _ -> red_allowed flags stack fDELTA - | VarKey id -> red_allowed flags stack (fVAR id) - | ConstKey sp -> red_allowed flags stack (fCONST sp) +let red_set_ref flags = function + | FarRelKey _ -> red_set flags fDELTA + | VarKey id -> red_set flags (fVAR id) + | ConstKey sp -> red_set flags (fCONST sp) (* Transfer application lists from a value to the stack * useful because fixpoints may be totally applied in several times @@ -152,45 +143,29 @@ let strip_appl head stack = | _ -> (head, stack) -(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last - * argument is []. - * Because we must put all the applied terms in the stack. - *) -let reduce_const_body redfun v stk = - if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk - - (* Tests if fixpoint reduction is possible. A reduction function is given as argument *) -let rec check_app_constr redfun = function +let rec check_app_constr = function | ([], _) -> false | ((CONSTR _)::_, 0) -> true - | (t::_, 0) -> (* TODO: partager ce calcul *) - (match redfun t with - | CONSTR _ -> true - | _ -> false) - | (_::l, n) -> check_app_constr redfun (l,(pred n)) + | (_::l, n) -> check_app_constr (l,(pred n)) -let fixp_reducible redfun flgs ((reci,i),_) stk = - if red_allowed flgs stk fIOTA then +let fixp_reducible flgs ((reci,i),_) stk = + if red_set flgs fIOTA then match stk with (* !!! for Acc_rec: reci.(i) = -2 *) - | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i)) + | APP(appl,_) -> reci.(i) >=0 & check_app_constr (appl, reci.(i)) | _ -> false else false -let cofixp_reducible redfun flgs _ stk = - if red_allowed flgs stk fIOTA then +let cofixp_reducible flgs _ stk = + if red_set flgs fIOTA then match stk with | (CASE _ | APP(_,CASE _)) -> true | _ -> false else false -let mindsp_nparams env (sp,i) = - let mib = lookup_mind sp env in - mib.Declarations.mind_packets.(i).Declarations.mind_nparams - (* The main recursive functions * * Go under applications and cases (pushed in the stack), expand head @@ -216,28 +191,23 @@ let rec norm_head info env t stack = (* constants, axioms * the first pattern is CRUCIAL, n=0 happens very often: * when reducing closed terms, n is always 0 *) - | Rel i -> (match expand_rel i env with - | Inl (0,v) -> - reduce_const_body (cbv_norm_more info env) v stack - | Inl (n,v) -> - reduce_const_body - (cbv_norm_more info env) (shift_value n v) stack - | Inr (n,None) -> - (VAL(0, mkRel n), stack) - | Inr (n,Some p) -> - norm_head_ref (n-p) info env stack (FarRelKey p)) + | Rel i -> + (match expand_rel i env with + | Inl (0,v) -> strip_appl v stack + | Inl (n,v) -> strip_appl (shift_value n v) stack + | Inr (n,None) -> (VAL(0, mkRel n), stack) + | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (FarRelKey p)) | Var id -> norm_head_ref 0 info env stack (VarKey id) - | Const sp -> - norm_head_ref 0 info env stack (ConstKey sp) + | Const sp -> norm_head_ref 0 info env stack (ConstKey sp) | LetIn (x, b, t, c) -> (* zeta means letin are contracted; delta without zeta means we *) (* allow substitution but leave let's in place *) - let zeta = red_allowed (info_flags info) stack fZETA in + let zeta = red_set (info_flags info) fZETA in let env' = - if zeta or red_allowed (info_flags info) stack fDELTA then + if zeta or red_set (info_flags info) fDELTA then subs_cons (cbv_stack_term info TOP env b,env) else subs_lift env in @@ -264,17 +234,11 @@ let rec norm_head info env t stack = stack) and norm_head_ref k info env stack normt = - if red_allowed_ref (info_flags info) stack normt then + if red_set_ref (info_flags info) normt then match ref_value_cache info normt with - | Some body -> - reduce_const_body (cbv_norm_more info env) (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k info normt), stack) - else (VAL(0,make_constr_ref k info normt), stack) - -and make_constr_ref n info = function - | FarRelKey p -> mkRel (n+p) - | VarKey id -> mkVar id - | ConstKey cst -> mkConst cst + | Some body -> strip_appl (shift_value k body) stack + | None -> (VAL(0,make_constr_ref k normt), stack) + else (VAL(0,make_constr_ref k normt), stack) (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak @@ -286,32 +250,31 @@ and cbv_stack_term info stack env t = match norm_head info env t stack with (* a lambda meets an application -> BETA *) | (LAM (x,a,b,env), APP (arg::args, stk)) - when red_allowed (info_flags info) stk fBETA -> + when red_set (info_flags info) fBETA -> let subs = subs_cons (arg,env) in cbv_stack_term info (stack_app args stk) subs b (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,_), stk) - when fixp_reducible (cbv_norm_more info env) (info_flags info) fix stk -> + when fixp_reducible (info_flags info) fix stk -> let (envf,redfix) = contract_fixp env fix in cbv_stack_term info stk envf redfix (* constructor guard satisfied or Cofix in a Case -> IOTA *) | (COFIXP(cofix,env,_), stk) - when cofixp_reducible (cbv_norm_more info env) (info_flags info) cofix stk-> + when cofixp_reducible (info_flags info) cofix stk-> let (envf,redfix) = contract_cofixp env cofix in cbv_stack_term info stk envf redfix - (* constructor in a Case -> IOTA - (use red_under because we know there is a Case) *) + (* constructor in a Case -> IOTA *) | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk))) - when red_under (info_flags info) fIOTA -> + when red_set (info_flags info) fIOTA -> let real_args = snd (list_chop ci.ci_npar args) in cbv_stack_term info (stack_app real_args stk) env br.(n-1) - (* constructor of arity 0 in a Case -> IOTA ( " " )*) + (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR((_,n),_), CASE(_,br,_,env,stk)) - when red_under (info_flags info) fIOTA -> + when red_set (info_flags info) fIOTA -> cbv_stack_term info stk env br.(n-1) (* may be reduced later by application *) @@ -324,14 +287,6 @@ and cbv_stack_term info stack env t = | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk) -(* if we are in SIMPL mode, maybe v isn't reduced enough *) -and cbv_norm_more info env v = - match (v, (info_flags info)) with - | (VAL(k,t), ((SIMPL|WITHBACK),_)) -> - cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t - | _ -> v - - (* When we are sure t will never produce a redex with its stack, we * normalize (even under binders) the applied terms and we build the * final term diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 000ed4e3f..6c9ebde6f 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -9,10 +9,8 @@ (*i $Id$ i*) (*i*) -open Pp open Names open Term -open Evd open Environ open Closure open Esubst @@ -23,8 +21,9 @@ open Esubst (* Entry point for cbv normalization of a constr *) type cbv_infos -val create_cbv_infos : flags -> env -> cbv_infos -val cbv_norm : cbv_infos -> constr -> constr + +val create_cbv_infos : RedFlags.reds -> env -> cbv_infos +val cbv_norm : cbv_infos -> constr -> constr (***********************************************************************) (*i This is for cbv debug *) @@ -43,19 +42,12 @@ type cbv_stack = | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack val stack_app : cbv_value list -> cbv_stack -> cbv_stack -val under_case_stack : cbv_stack -> bool val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack -open RedFlags -val red_allowed : flags -> cbv_stack -> red_kind -> bool -val reduce_const_body : - (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack - (* recursive functions... *) val cbv_stack_term : cbv_infos -> cbv_stack -> cbv_value subs -> constr -> cbv_value val cbv_norm_term : cbv_infos -> cbv_value subs -> constr -> constr -val cbv_norm_more : cbv_infos -> cbv_value subs -> cbv_value -> cbv_value val norm_head : cbv_infos -> cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack val apply_stack : cbv_infos -> constr -> cbv_stack -> constr diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d545e96cb..a1291284f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -56,7 +56,7 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a (*s Generic Optimized Reduction Function using Closures *) -val clos_norm_flags : Closure.flags -> reduction_function +val clos_norm_flags : Closure.RedFlags.reds -> reduction_function (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function val nf_betaiota : local_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 854a61b26..6c38f6d9a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -14,6 +14,7 @@ open Names open Nameops open Term open Termops +open Declarations open Inductive open Environ open Reductionops @@ -24,6 +25,39 @@ open Cbv exception Elimconst exception Redelimination +let set_opaque_const = Conv_oracle.set_opaque_const +let set_transparent_const sp = + let cb = Global.lookup_constant sp in + if cb.const_body <> None & cb.const_opaque then + errorlabstrm "set_transparent_const" + [< 'sTR "Cannot make"; 'sPC; + Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp); + 'sPC; 'sTR "transparent because it was declared opaque." >]; + Conv_oracle.set_transparent_const sp + +let set_opaque_var = Conv_oracle.set_opaque_var +let set_transparent_var = Conv_oracle.set_transparent_var + +let _ = + Summary.declare_summary "Transparent constants and variables" + { Summary.freeze_function = Conv_oracle.freeze; + Summary.unfreeze_function = Conv_oracle.unfreeze; + Summary.init_function = Conv_oracle.init; + Summary.survive_section = false } + +let is_evaluable env ref = + match ref with + EvalConstRef sp -> + let (ids,sps) = Conv_oracle.freeze() in + Sppred.mem sp sps & + let cb = Environ.lookup_constant sp env in + cb.const_body <> None & not cb.const_opaque + | EvalVarRef id -> + let (ids,sps) = Conv_oracle.freeze() in + Idpred.mem id ids & + let (_,value,_) = Environ.lookup_named id env in + value <> None + type evaluable_reference = | EvalConst of constant | EvalVar of identifier @@ -37,8 +71,8 @@ let mkEvalRef = function | EvalEvar ev -> mkEvar ev let isEvalRef env c = match kind_of_term c with - | Const sp -> Opaque.is_evaluable env (EvalConstRef sp) - | Var id -> Opaque.is_evaluable env (EvalVarRef id) + | Const sp -> is_evaluable env (EvalConstRef sp) + | Var id -> is_evaluable env (EvalVarRef id) | Rel _ | Evar _ -> true | _ -> false @@ -353,7 +387,7 @@ let special_red_case env whfun (ci, p, c, lf) = let (constr, cargs) = whfun s in match kind_of_term constr with | Const cst -> - (if not (Opaque.is_evaluable env (EvalConstRef cst)) then + (if not (is_evaluable env (EvalConstRef cst)) then raise Redelimination; let gvalue = constant_value env cst in if reducible_mind_case gvalue then @@ -449,7 +483,7 @@ and construct_const env sigma = (* Red reduction tactic: reduction to a product *) let internal_red_product env sigma c = - let simpfun = clos_norm_flags (UNIFORM,betaiotazeta_red) env sigma in + let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = match kind_of_term x with | App (f,l) -> @@ -660,8 +694,8 @@ let string_of_evaluable_ref = function | EvalConstRef sp -> string_of_path sp let unfold env sigma name = - if Opaque.is_evaluable env name then - clos_norm_flags (unfold_flags name) env sigma + if is_evaluable env name then + clos_norm_flags (unfold_red name) env sigma else error (string_of_evaluable_ref name^" is opaque") @@ -728,8 +762,8 @@ type red_expr = | Red of bool | Hnf | Simpl - | Cbv of Closure.flags - | Lazy of Closure.flags + | Cbv of Closure.RedFlags.reds + | Lazy of Closure.RedFlags.reds | Unfold of (int list * evaluable_global_reference) list | Fold of constr list | Pattern of (int list * constr * constr) list @@ -787,7 +821,7 @@ let one_step_reduce env sigma c = let reduce_to_ind_gen allow_product env sigma t = let rec elimrec env t l = - let c, _ = whd_stack t in + let c, _ = Reductionops.whd_stack t in match kind_of_term c with | Ind (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l) | Prod (n,ty,t') -> diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 1b87dc712..4100a31ae 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -19,6 +19,8 @@ open Closure (*s Reduction functions associated to tactics. \label{tacred} *) +val is_evaluable : env -> evaluable_global_reference -> bool + exception Redelimination (* Red (raise Redelimination if nothing reducible) *) @@ -42,7 +44,7 @@ val pattern_occs : (int list * constr * constr) list -> reduction_function (* Rem: Lazy strategies are defined in Reduction *) (* Call by value strategy (uses Closures) *) -val cbv_norm_flags : Closure.flags -> reduction_function +val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function val cbv_beta : local_reduction_function val cbv_betaiota : local_reduction_function val cbv_betadeltaiota : reduction_function @@ -62,10 +64,17 @@ type red_expr = | Red of bool (* raise Redelimination if true otherwise UserError *) | Hnf | Simpl - | Cbv of Closure.flags - | Lazy of Closure.flags + | Cbv of Closure.RedFlags.reds + | Lazy of Closure.RedFlags.reds | Unfold of (int list * evaluable_global_reference) list | Fold of constr list | Pattern of (int list * constr * constr) list val reduction_of_redexp : red_expr -> reduction_function + +(* Opaque and Transparent commands. *) +val set_opaque_const : section_path -> unit +val set_transparent_const : section_path -> unit + +val set_opaque_var : identifier -> unit +val set_transparent_var : identifier -> unit diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ec90fc925..d73264e92 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Termops open Sign diff --git a/proofs/logic.ml b/proofs/logic.ml index 6043857fa..61edd06bf 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Evd open Term open Termops diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2b8416eae..b148c019a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Sign open Term open Declarations diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 809fbd7b8..af106b1c4 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -11,6 +11,7 @@ open Closure open Util open Names +open Nameops open Term open Termops open Sign @@ -262,7 +263,7 @@ let rec ast_of_cvt_intro_pattern = function (* Gives the ast list corresponding to a reduction flag *) open RedFlags -let last_of_cvt_flags (_,red) = +let last_of_cvt_flags red = (if (red_set red fBETA) then [ope("Beta",[])] else [])@ (let (n_unf,lconst) = red_get_const red in diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 32d96bce1..56fe36890 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -213,14 +213,10 @@ let glob_const_nvar loc env qid = (* We first look for a variable of the current proof *) match Nametab.repr_qualid qid with | d,id when repr_dirpath d = [] -> - (* lookup_value may raise Not_found *) - (match Environ.lookup_named id env with - | (_,Some _,_) -> - let v = EvalVarRef id in - if Opaque.is_evaluable env v then v - else error ("variable "^(string_of_id id)^" is opaque") - | _ -> error ((string_of_id id)^ - " does not denote an evaluable constant")) + let v = EvalVarRef id in + if Tacred.is_evaluable env v then v + else error + ((string_of_id id^" does not denote an evaluable constant")) | _ -> raise Not_found with Not_found -> try @@ -229,7 +225,7 @@ let glob_const_nvar loc env qid = | VarRef id -> EvalVarRef id | _ -> error ((Nametab.string_of_qualid qid) ^ " does not denote an evaluable constant")) in - if Opaque.is_evaluable env ev then ev + if Tacred.is_evaluable env ev then ev else error ((Nametab.string_of_qualid qid) ^ " does not denote an evaluable constant") with Not_found -> @@ -1124,7 +1120,7 @@ and flag_of_ast ist lf = in add_flag red lf | Node(_,"Delta",[])::Node(loc,"UnfBut",l)::lf -> let red = red_add red fDELTA in - let red = red_add_transparent red (Opaque.state()) in + let red = red_add_transparent red (Conv_oracle.freeze()) in let red = List.fold_right (fun v red -> @@ -1134,7 +1130,7 @@ and flag_of_ast ist lf = in add_flag red lf | Node(_,"Delta",[])::lf -> let red = red_add red fDELTA in - let red = red_add_transparent red (Opaque.state()) in + let red = red_add_transparent red (Conv_oracle.freeze()) in add_flag red lf | Node(_,"Iota",[])::lf -> add_flag (red_add red fIOTA) lf | Node(_,"Zeta",[])::lf -> add_flag (red_add red fZETA) lf @@ -1153,8 +1149,8 @@ and redexp_of_ast ist = function | ("Simpl", []) -> Simpl | ("Unfold", ul) -> Unfold (List.map (cvt_unfold ist) ul) | ("Fold", cl) -> Fold (List.map (cvt_fold ist) cl) - | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast ist lf) - | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast ist lf) + | ("Cbv",lf) -> Cbv(flag_of_ast ist lf) + | ("Lazy",lf) -> Lazy(flag_of_ast ist lf) | ("Pattern",lp) -> Pattern (List.map (cvt_pattern ist) lp) | (s,_) -> invalid_arg ("malformed reduction-expression: "^s) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d8ef207ff..377893fd2 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -10,6 +10,7 @@ open Util open Names +open Nameops open Sign open Term open Termops diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 01e7cca46..1e28b23bb 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Termops open Sign diff --git a/tactics/equality.ml b/tactics/equality.ml index d1ac66b1f..f1f3870ad 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Univ open Term open Termops diff --git a/tactics/inv.ml b/tactics/inv.ml index c8da9ed1d..67e92ac8f 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Termops open Global diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b0da5c41b..678ad6431 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -12,6 +12,7 @@ open Pp open Util open Options open Names +open Nameops open Term open Termops open Inductive diff --git a/toplevel/record.ml b/toplevel/record.ml index d113b9450..2f294af98 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -11,6 +11,7 @@ open Pp open Util open Names +open Nameops open Term open Termops open Environ diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 3e2ab8c10..b065d7b57 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -11,6 +11,7 @@ open Util open Pp open Names +open Nameops open Term open Instantiate open Lib diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 52bd586ca..de728ee15 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -591,8 +591,8 @@ let _ = (function | VARG_QUALID qid -> (match Nametab.global dummy_loc qid with - | ConstRef sp -> Opaque.set_transparent_const sp - | VarRef id -> Opaque.set_transparent_var id + | ConstRef sp -> Tacred.set_transparent_const sp + | VarRef id -> Tacred.set_transparent_var id | _ -> error "cannot set an inductive type or a constructor as transparent") | _ -> bad_vernac_args "TRANSPARENT") @@ -605,8 +605,8 @@ let _ = (function | VARG_QUALID qid -> (match Nametab.global dummy_loc qid with - | ConstRef sp -> Opaque.set_opaque_const sp - | VarRef id -> Opaque.set_opaque_var id + | ConstRef sp -> Tacred.set_opaque_const sp + | VarRef id -> Tacred.set_opaque_var id | _ -> error "cannot set an inductive type or a constructor as opaque") | _ -> bad_vernac_args "OPAQUE") |