diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 167 |
1 files changed, 79 insertions, 88 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 360c6e86..fb2be89e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -47,29 +47,28 @@ open Libobject type effect_name = string (** create a persistent set to store effect functions *) -module ConstrMap = Map.Make (Constr) (* Table bindings a constant to an effect *) -let constant_effect_table = Summary.ref ~name:"reduction-side-effect" ConstrMap.empty +let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty (* Table bindings function key to effective functions *) let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty (** a test to know whether a constant is actually the effect function *) -let reduction_effect_hook env sigma termkey c = +let reduction_effect_hook env sigma con c = try - let funkey = ConstrMap.find termkey !constant_effect_table in + let funkey = Cmap.find con !constant_effect_table in let effect = String.Map.find funkey !effect_table in effect env sigma (Lazy.force c) with Not_found -> () -let cache_reduction_effect (_,(termkey,funkey)) = - constant_effect_table := ConstrMap.add termkey funkey !constant_effect_table +let cache_reduction_effect (_,(con,funkey)) = + constant_effect_table := Cmap.add con funkey !constant_effect_table -let subst_reduction_effect (subst,(termkey,funkey)) = - (subst_mps subst termkey,funkey) +let subst_reduction_effect (subst,(con,funkey)) = + (subst_constant subst con,funkey) -let inReductionEffect : Constr.constr * string -> obj = +let inReductionEffect : Constant.t * string -> obj = declare_object {(default_object "REDUCTION-EFFECT") with cache_function = cache_reduction_effect; open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o); @@ -83,8 +82,7 @@ let declare_reduction_effect funkey f = (** A function to set the value of the print function *) let set_reduction_effect x funkey = - let termkey = Universes.constr_of_global x in - Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) + Lib.add_anonymous_leaf (inReductionEffect (x,funkey)) (** Machinery to custom the behavior of the reduction *) @@ -104,7 +102,7 @@ module ReductionBehaviour = struct type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] type req = | ReqLocal - | ReqGlobal of global_reference * (int list * int * flag list) + | ReqGlobal of GlobRef.t * (int list * int * flag list) let load _ (_,(_,(r, b))) = table := Refmap.add r b !table @@ -255,9 +253,9 @@ module Cst_stack = struct (applist (cst, List.rev params)) t) cst_l c - let pr l = + let pr env sigma l = let open Pp in - let p_c c = Termops.print_constr c in + let p_c c = Termops.Internal.print_constr_env env sigma c in prlist_with_sep pr_semicolon (fun (c,params,args) -> hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ @@ -280,7 +278,7 @@ sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * Projection.t * Cst_stack.t + | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list @@ -337,11 +335,12 @@ struct type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * Projection.t * Cst_stack.t + | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list + (* Debugging printer *) let rec pr_member pr_c member = let open Pp in let pr_c x = hov 1 (pr_c x) in @@ -351,9 +350,8 @@ struct str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" - | Proj (n,m,p,cst) -> - str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ - pr_comma () ++ Constant.print (Projection.constant p) ++ str ")" + | Proj (p,cst) -> + str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -370,11 +368,11 @@ struct let open Pp in match c with | Cst_const (c, u) -> - if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ + if Univ.Instance.is_empty u then Constant.debug_print c + else str"(" ++ Constant.debug_print c ++ str ", " ++ Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> - str".(" ++ Constant.print (Projection.constant p) ++ str")" + str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" let empty = [] let is_empty = CList.is_empty @@ -413,10 +411,9 @@ struct (f t1 t2) && (equal_rec s1' s2') | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 - | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> - Int.equal n1 n2 && Int.equal m1 m2 - && Constant.equal (Projection.constant p) (Projection.constant p2) - && equal_rec s1 s2 + | (Proj (p,_)::s1, Proj(p2,_)::s2) -> + Projection.Repr.equal (Projection.repr p) (Projection.repr p2) + && equal_rec s1 s2 | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> f_fix f1 f2 && equal_rec (List.rev s1) (List.rev s2) @@ -436,7 +433,7 @@ struct | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 - | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> + | (Proj (p,_)::s1, Proj(p2,_)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -456,7 +453,7 @@ struct aux (f o t1 t2) l1 l2 | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 - | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> + | Proj (p1,_) :: q1, Proj (p2,_) :: q2 -> aux o q1 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in @@ -469,7 +466,7 @@ struct in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | (Proj (_,_,_,_)) as e -> e + | (Proj (_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -513,7 +510,7 @@ struct let will_expose_iota args = List.exists (function (Fix (_,_,l) | Case (_,_,_,l) | - Proj (_,_,_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false) + Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false) args let list_of_app_stack s = @@ -590,9 +587,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Proj (n,m,p,cst_l)::s) when refold -> + | f, (Proj (p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) - | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) + | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s) in zip s @@ -617,9 +614,9 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -let pr_state (tm,sk) = +let pr_state env sigma (tm,sk) = let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) (*************************************) @@ -632,6 +629,18 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None +let strong_with_flags whdfun flags env sigma t = + let push_rel_check_zeta d env = + let open CClosure.RedFlags in + let d = match d with + | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) + | d -> d in + push_rel d env in + let rec strongrec env t = + map_constr_with_full_binders sigma + push_rel_check_zeta strongrec env (whdfun flags env sigma t) in + strongrec env t + let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in @@ -701,18 +710,18 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> - let open Universes in + let open UnivProblem in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = fresh_constant_instance env cst in + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> - let subst = Constraints.fold (fun cst acc -> + let subst = Set.fold (fun cst acc -> let l, r = match cst with | ULub (u, v) | UWeak (u, v) -> u, v | UEq (u, v) | ULe (u, v) -> @@ -845,10 +854,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_notice (h 0 (str "<<" ++ pr x ++ - str "|" ++ cut () ++ Cst_stack.pr cst_l ++ + str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in @@ -871,10 +880,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Evar ev -> fold () | Meta ev -> (match safe_meta_value sigma ev with - | Some body -> whrec cst_l (EConstr.of_constr body, stack) + | Some body -> whrec cst_l (body, stack) | None -> fold ()) | Const (c,u as const) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma x) + reduction_effect_hook env sigma c (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then let u' = EInstance.kind sigma u in @@ -920,16 +929,13 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') ) else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> - (let pb = lookup_projection p env in - let kn = Projection.constant p in - let npars = pb.Declarations.proj_npars - and arg = pb.Declarations.proj_arg in - if not tactic_mode then - let stack' = (c, Stack.Proj (npars, arg, p, Cst_stack.empty (*cst_l*)) :: stack) in + (let npars = Projection.npars p in + if not tactic_mode then + let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (Globnames.ConstRef kn) with + else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with | None -> - let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + let stack' = (c, Stack.Proj (p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in if equal_stacks sigma stack' stack'' then fold () else stack'', csts @@ -946,7 +952,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |[] -> (* if nargs has been specified *) (* CAUTION : the constant is NEVER refold (even when it hides a (co)fix) *) - let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + let stack' = (c, Stack.Proj (p, cst_l) :: stack) in whrec Cst_stack.empty(* cst_l *) stack' | curr::remains -> if curr == 0 then (* Try to reduce the record argument *) @@ -1005,8 +1011,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_)::s') when use_match -> - whrec Cst_stack.empty (Stack.nth args (n+m), s') + |args, (Stack.Proj (p,_)::s') when use_match -> + whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s') |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip sigma (x, args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in @@ -1025,14 +1031,11 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> - let pb = lookup_projection p env in - let npars = pb.Declarations.proj_npars in - let narg = pb.Declarations.proj_arg in - let stack = s' @ (Stack.append_app [|x'|] s'') in + let stack = s' @ (Stack.append_app [|x'|] s'') in match Stack.strip_n_app 0 stack with | None -> assert false | Some (_,arg,s'') -> - whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p,cst_l) :: s'')) + whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s'')) | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with | None -> fold () | Some (bef,arg,s''') -> @@ -1090,10 +1093,7 @@ let local_whd_state_gen flags sigma = | _ -> s) | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> - (let pb = lookup_projection p (Global.env ()) in - whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - p, Cst_stack.empty) - :: stack)) + (whrec (c, Stack.Proj (p, Cst_stack.empty) :: stack)) | Case (ci,p,d,lf) -> whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack) @@ -1106,7 +1106,7 @@ let local_whd_state_gen flags sigma = | Evar ev -> s | Meta ev -> (match safe_meta_value sigma ev with - Some c -> whrec (EConstr.of_constr c,stack) + Some c -> whrec (c,stack) | None -> s) | Construct ((ind,c),u) -> @@ -1116,8 +1116,8 @@ let local_whd_state_gen flags sigma = match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p,_) :: s') when use_match -> - whrec (Stack.nth args (n+m), s') + |args, (Stack.Proj (p,_) :: s') when use_match -> + whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> @@ -1392,7 +1388,7 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = (********************************************************************) let whd_meta sigma c = match EConstr.kind sigma c with - | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c) + | Meta p -> (try meta_value sigma p with Not_found -> c) | _ -> c let default_plain_instance_ident = Id.of_string "H" @@ -1404,7 +1400,7 @@ let plain_instance sigma s c = | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in - let l' = CArray.Fun1.smartmap irec n l in + let l' = Array.Fun1.Smart.map irec n l in (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a @@ -1413,7 +1409,7 @@ let plain_instance sigma s c = (try let g = Metamap.find p s in match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = Array.Fun1.Smart.map lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) @@ -1580,11 +1576,11 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' - |args, (Stack.Proj (n,m,p,_) :: stack'') -> + |args, (Stack.Proj (p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in if isConstruct sigma t_o then - whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') + whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'') else s,csts' |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s @@ -1612,7 +1608,7 @@ let meta_value evd mv = match meta_opt_fvalue evd mv with | Some (b,_) -> let metas = Metamap.bind valrec b.freemetas in - instance evd metas (EConstr.of_constr b.rebus) + instance evd metas b.rebus | None -> mkMeta mv in valrec mv @@ -1625,9 +1621,8 @@ let meta_instance sigma b = instance sigma c_sigma b.rebus let nf_meta sigma c = - let c = EConstr.Unsafe.to_constr c in let cl = mk_freelisted c in - meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus } + meta_instance sigma { cl with rebus = cl.rebus } (* Instantiate metas that create beta/iota redexes *) @@ -1648,7 +1643,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None @@ -1660,7 +1654,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isLambda evd g || not is_coerce then Some g else None with Not_found -> None @@ -1669,7 +1662,6 @@ let meta_reducible_instance evd b = | None -> mkApp (f,Array.map irec l)) | Meta m -> (try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) @@ -1678,7 +1670,6 @@ let meta_reducible_instance evd b = (match try let g, s = Metamap.find m metas in - let g = EConstr.of_constr g in let is_coerce = match s with CoerceToType -> true | _ -> false in if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None |