From ae46681fcd8c07d4feca66c0940c83446791d8b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Jan 2021 18:47:51 +0100 Subject: Inline the function in contract_[co]fix_use_function. --- pretyping/tacred.ml | 96 ++++++++++++++++++++++++++--------------------------- 1 file changed, 48 insertions(+), 48 deletions(-) (limited to 'pretyping') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index bc7d50ccfa..2a612b4737 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -467,6 +467,29 @@ type fix_reduction_result = NotReducible | Reduced of (constr * constr list) let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = + let (names, (nbfix, lv, n)), u, largs = f in + let lu = List.firstn n largs in + let p = List.length lv in + let lyi = List.map fst lv in + let la = + List.map_i (fun q aq -> + (* k from the comment is q+1 *) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) + with Not_found -> Vars.lift p aq) + 0 lu + in + let f i = match names.(i) with + | None -> None + | Some (minargs,ref) -> + let body = applist (mkEvalRef ref u, la) in + let g = + List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> + let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in + let tij' = Vars.substl (List.rev subst) tij in + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) + in Some (minargs,g) + in let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = List.init nbodies make_Fi in @@ -474,7 +497,29 @@ let contract_fix_use_function env sigma f nf_beta env sigma c let contract_cofix_use_function env sigma f - (bodynum,(_names,_,bodies as typedbodies)) = + (bodynum,(names,_,bodies as typedbodies)) args = + let f = + if isConst sigma f then + let minargs = List.length args in + fun i -> + if Int.equal i bodynum then Some (minargs, f) + else match names.(i).binder_name with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + mutual inductive, try to reuse the global name if + the block was indeed initially built as a global + definition *) + let (kn, u) = destConst sigma f in + let kn = Constant.change_label kn (Label.of_id id) in + let cst = (kn, EInstance.kind sigma u) in + try match constant_opt_value_in env cst with + | None -> None + (* TODO: check kn is correct *) + | Some _ -> Some (minargs,mkConstU (kn, u)) + with Not_found -> None + else + fun _ -> None in let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = List.init nbodies make_Fi in @@ -504,7 +549,7 @@ let reduce_mind_case env sigma mia = mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false -let reduce_mind_case_use_function func env sigma mia = +let reduce_mind_case_use_function f env sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((_, i as cstr),u) -> let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in @@ -513,30 +558,8 @@ let reduce_mind_case_use_function func env sigma mia = let br = it_mkLambda_or_LetIn (snd br) ctx in applist (br, real_cargs) | CoFix (bodynum,(names,_,_) as cofix) -> - let build_cofix_name = - if isConst sigma func then - let minargs = List.length mia.mcargs in - fun i -> - if Int.equal i bodynum then Some (minargs,func) - else match names.(i).binder_name with - | Anonymous -> None - | Name id -> - (* In case of a call to another component of a block of - mutual inductive, try to reuse the global name if - the block was indeed initially built as a global - definition *) - let (kn, u) = destConst sigma func in - let kn = Constant.change_label kn (Label.of_id id) in - let cst = (kn, EInstance.kind sigma u) in - try match constant_opt_value_in env cst with - | None -> None - (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConstU (kn, u)) - with Not_found -> None - else - fun _ -> None in let cofix_def = - contract_cofix_use_function env sigma build_cofix_name cofix in + contract_cofix_use_function env sigma f cofix mia.mcargs in mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -826,29 +849,6 @@ and reduce_fix_use_function env sigma f fix stack = let stack' = List.assign stack recargnum (applist recarg') in (match EConstr.kind sigma recarg'hd with | Construct _ -> - let (names, (nbfix, lv, n)), u, largs = f in - let lu = List.firstn n largs in - let p = List.length lv in - let lyi = List.map fst lv in - let la = - List.map_i (fun q aq -> - (* k from the comment is q+1 *) - try mkRel (p+1-(List.index Int.equal (n-q) lyi)) - with Not_found -> Vars.lift p aq) - 0 lu - in - let f i = match names.(i) with - | None -> None - | Some (minargs,ref) -> - let body = applist (mkEvalRef ref u, la) in - let g = - List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> - let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in - let tij' = Vars.substl (List.rev subst) tij in - let x = make_annot x Sorts.Relevant in (* TODO relevance *) - mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some (minargs,g) - in Reduced (contract_fix_use_function env sigma f fix,stack') | _ -> NotReducible) -- cgit v1.2.3