diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 180 |
1 files changed, 110 insertions, 70 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3352bfce38..3da75f67b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -177,9 +177,12 @@ sig type 'a app_node val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -194,6 +197,7 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + val decomp_rev : 'a t -> ('a * 'a t) option val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> @@ -214,13 +218,13 @@ end = struct open EConstr type 'a app_node = int * 'a array * int - (* first releavnt position, arguments, last relevant position *) + (* first relevant position, arguments, last relevant position *) (* - Invariant that this module must ensure : - (behare of direct access to app_node by the rest of Reductionops) + Invariant that this module must ensure: + (beware of direct access to app_node by the rest of Reductionops) - in app_node (i,_,j) i <= j - - There is no array realocation (outside of debug printing) + - There is no array reallocation (outside of debug printing) *) let pr_app_node pr (i,a,j) = @@ -229,9 +233,12 @@ struct ) + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -244,9 +251,9 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,_,br) -> + | Case (_,_,_,_,_,br) -> str "ZCase(" ++ - prvect_with_sep (pr_bar) pr_c br + prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br ++ str ")" | Proj p -> str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" @@ -267,12 +274,10 @@ struct let le = Array.length v in if Int.equal le 0 then s else App (0,v,pred le) :: s - let decomp_node (i,l,j) sk = - if i < j then (l.(i), App (succ i,l,j) :: sk) - else (l.(i), sk) - - let decomp = function - | App node::s -> Some (decomp_node node s) + let decomp_rev = function + | App (i,l,j) :: sk -> + if i < j then Some (l.(j), App (i,l,pred j) :: sk) + else Some (l.(j), sk) | _ -> None let decomp_node_last (i,l,j) sk = @@ -285,7 +290,7 @@ struct ([],[]) -> Int.equal bal 0 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 - | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> + | (Case _ :: s1, Case _::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Proj (p)::s1, Proj(p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 @@ -293,7 +298,7 @@ struct Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in + | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -305,8 +310,9 @@ struct let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in 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 + | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 -> + let f' o (_, t1) (_, t2) = f o t1 t2 in + aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2 | Proj (p1) :: q1, Proj (p2) :: q2 -> aux o q1 q2 | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 -> @@ -321,8 +327,8 @@ struct | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,iv,br) -> - Case (info, f ty, map_invert f iv, Array.map f br) + | Case (info,u,pms,ty,iv,br) -> + Case (info, u, Array.map f pms, on_snd f ty, iv, Array.map (on_snd f) br) | Fix ((r,(na,ty,bo)),arg) -> Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg) | Primitive (p,c,args,kargs) -> @@ -334,29 +340,35 @@ struct append_app a s let rec args_size = function - | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0 + | App (i,_,j) :: s -> j + 1 - i + args_size s + | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0 let strip_app s = let rec aux out = function | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s + let strip_n_app n s = let rec aux n out = function | App (i,a,j) as e :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then - aux (n - nb) (e::out) s + aux (n - nb) (e :: out) s else - let p = i+n in + let p = i + n in Some (CList.rev (if Int.equal n 0 then out else App (i,a,p-1) :: out), a.(p), - if j > p then App(succ p,a,j)::s else s) + if j > p then App (succ p,a,j) :: s else s) | s -> None in aux n [] s + let decomp s = + match strip_n_app 0 s with + | Some (_,a,s) -> Some (a,s) + | None -> None + let not_purely_applicative args = List.exists (function (Fix _ | Case _ | Proj _ ) -> true | App _ | Primitive _ -> false) args @@ -369,12 +381,11 @@ struct (Array.fold_right (fun x y -> x::y) a' args', s') | s -> ([],s) in let (out,s') = aux s in - let init = match s' with [] -> true | _ -> false in - Option.init init out + match s' with [] -> Some out | _ -> None let assign s p c = match strip_n_app p s with - | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk) + | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk) | None -> assert false let tail n0 s0 = @@ -382,12 +393,12 @@ struct if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then aux (n - nb) s else let p = i+n in - if j >= p then App(p,a,j)::s else s + if j >= p then App (p,a,j) :: s else s | _ -> raise (Invalid_argument "Reductionops.Stack.tail") in aux n0 s0 @@ -404,7 +415,7 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s) + | f, (Case (ci,u,pms,rt,iv,br)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s) | f, (Fix (fix,st)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) | f, (Proj (p)::s) -> zip (mkProj (p,f),s) @@ -465,13 +476,13 @@ let strong_with_flags whdfun flags env sigma t = | d -> d in push_rel d env in let rec strongrec env t = - map_constr_with_full_binders sigma + map_constr_with_full_binders env 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 + map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in strongrec env t (*************************************) @@ -698,6 +709,20 @@ let debug_RAKAM = ~key:["Debug";"RAKAM"] ~value:false +let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = + let args = Stack.tail ci.ci_npar args in + let args = Option.get (Stack.list_of_app_stack args) in + let br = lf.(i - 1) in + if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then + (* No let-bindings *) + let subst = List.rev args in + Vars.substl subst (snd br) + else + (* For backwards compat with unification, we do not reduce the let-bindings + upfront. *) + let ctx = expand_branch env sigma u pms (ind, i) br in + applist (it_mkLambda_or_LetIn (snd br) ctx, args) + let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in let rec whrec (x, stack) : state = @@ -781,8 +806,8 @@ let rec whd_state_gen flags env sigma = | _ -> fold ()) | _ -> fold ()) - | Case (ci,p,iv,d,lf) -> - whrec (d, Stack.Case (ci,p,iv,lf) :: stack) + | Case (ci,u,pms,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -790,13 +815,14 @@ let rec whd_state_gen flags env sigma = |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef)::s')) - | Construct ((ind,c),u) -> + | Construct (cstr ,u) -> let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then 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.Case case::s') when use_match -> + let r = apply_branch env sigma cstr args case in + whrec (r, 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')::s'') when use_fix -> @@ -846,7 +872,7 @@ let rec whd_state_gen flags env sigma = whrec (** reduction machine without global env and refold machinery *) -let local_whd_state_gen flags _env sigma = +let local_whd_state_gen flags env sigma = let rec whrec (x, stack) = let c0 = EConstr.kind sigma x in let s = (EConstr.of_kind c0, stack) in @@ -878,8 +904,8 @@ let local_whd_state_gen flags _env sigma = | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (whrec (c, Stack.Proj (p) :: stack)) - | Case (ci,p,iv,d,lf) -> - whrec (d, Stack.Case (ci,p,iv,lf) :: stack) + | Case (ci,u,pms,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -892,13 +918,14 @@ let local_whd_state_gen flags _env sigma = Some c -> whrec (c,stack) | None -> s) - | Construct ((ind,c),u) -> + | Construct (cstr, u) -> let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then 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.Case case :: s') when use_match -> + let r = apply_branch env sigma cstr args case in + whrec (r, 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')::s'') when use_fix -> @@ -930,14 +957,6 @@ let stack_red_of_state_red f = let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f -(* Drops the Cst_stack *) -let iterate_whd_gen flags env sigma s = - let rec aux t = - let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in - let whd_sk = Stack.map aux sk in - Stack.zip sigma (hd,whd_sk) - in aux s - let red_of_state_red f env sigma x = Stack.zip sigma (f env sigma (x,Stack.empty)) @@ -1192,11 +1211,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = let default_plain_instance_ident = Id.of_string "H" +type subst_fun = { sfun : metavariable -> EConstr.t } + (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) -let plain_instance sigma s c = +let plain_instance sigma s c = match s with +| None -> c +| Some s -> let rec irec n u = match EConstr.kind sigma u with - | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) + | Meta p -> (try lift n (s.sfun p) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in let l' = Array.Fun1.Smart.map irec n l in @@ -1205,7 +1228,7 @@ let plain_instance sigma s c = (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) - (try let g = Metamap.find p s in + (try let g = s.sfun p in match EConstr.kind sigma g with | App _ -> let l' = Array.Fun1.Smart.map lift 1 l' in @@ -1216,12 +1239,11 @@ let plain_instance sigma s c = with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta sigma m -> - (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u) + (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u) | _ -> map_with_binders sigma succ irec n u in - if Metamap.is_empty s then c - else irec 0 c + irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -1423,23 +1445,41 @@ let is_arity env sigma c = (*************************************) (* Metas *) -let meta_value env evd mv = - let rec valrec mv = - match meta_opt_fvalue evd mv with - | Some (b,_) -> - let metas = Metamap.bind valrec b.freemetas in - instance env evd metas b.rebus - | None -> mkMeta mv +type meta_instance_subst = { + sigma : Evd.evar_map; + mutable cache : EConstr.t Metamap.t; +} + +let create_meta_instance_subst sigma = { + sigma; + cache = Metamap.empty; +} + +let eval_subst env subst = + let rec ans mv = + try Metamap.find mv subst.cache + with Not_found -> + match meta_opt_fvalue subst.sigma mv with + | None -> mkMeta mv + | Some (b, _) -> + let metas = + if Metaset.is_empty b.freemetas then None + else Some { sfun = ans } + in + let res = instance env subst.sigma metas b.rebus in + let () = subst.cache <- Metamap.add mv res subst.cache in + res in - valrec mv + { sfun = ans } -let meta_instance env sigma b = +let meta_instance env subst b = let fm = b.freemetas in if Metaset.is_empty fm then b.rebus else - let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in - instance env sigma c_sigma b.rebus + let sfun = eval_subst env subst in + instance env subst.sigma (Some sfun) b.rebus let nf_meta env sigma c = + let sigma = create_meta_instance_subst sigma in let cl = mk_freelisted c in meta_instance env sigma { cl with rebus = cl.rebus } |