diff options
-rw-r--r-- | kernel/esubst.ml | 4 | ||||
-rw-r--r-- | kernel/vars.ml | 75 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
-rw-r--r-- | proofs/goal.ml | 5 |
4 files changed, 56 insertions, 36 deletions
diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 998bba492..32ccebea6 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -87,7 +87,7 @@ let subs_shft = function | (0, s) -> s | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) | (n, s) -> SHIFT (n,s) -let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a) +let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s let subs_shift_cons = function (0, s, t) -> CONS(t,s) @@ -136,7 +136,7 @@ let rec comp mk_cl s1 s2 = | ESID _, _ -> s2 | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) | _, CONS(x,s') -> - CONS(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s') + CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') | CONS(x,s), SHIFT(k,s') -> let lg = Array.length x in if k == lg then comp mk_cl s s' diff --git a/kernel/vars.ml b/kernel/vars.ml index 123c96d6d..ca1d31c0b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -28,7 +28,7 @@ let closedn n c = (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) -let closed0 = closedn 0 +let closed0 c = closedn 0 c (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) @@ -84,10 +84,10 @@ let rec exliftn el c = match Constr.kind c with (* Lifting the binding depth across k bindings *) -let liftn n k = +let liftn n k c = match el_liftn (pred k) (el_shft n el_id) with - | ELID -> (fun c -> c) - | el -> exliftn el + | ELID -> c + | el -> exliftn el c let lift n = liftn n 1 @@ -109,8 +109,13 @@ let rec lift_substituend depth s = | Closed -> s.sit | Open -> lift depth s.sit | Unknown -> - s.sinfo <- if closed0 s.sit then Closed else Open; - lift_substituend depth s + let sit = s.sit in + if closed0 sit then + let () = s.sinfo <- Closed in + sit + else + let () = s.sinfo <- Open in + lift depth sit let make_substituend c = { sinfo=Unknown; sit=c } @@ -121,7 +126,7 @@ let substn_many lamv n c = let rec substrec depth c = match Constr.kind c with | Constr.Rel k -> if k<=depth then c - else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1) + else if k-depth <= lv then lift_substituend depth (Array.unsafe_get lamv (k-depth-1)) else Constr.mkRel (k-lv) | _ -> Constr.map_with_binders succ substrec depth c in substrec n c @@ -134,22 +139,29 @@ let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; let make_subst = function | [] -> [||] | hd :: tl -> - let subst = Array.make (1 + List.length tl) (make_substituend hd) in - let iteri i x = Array.unsafe_set subst (succ i) (make_substituend x) in - let () = CList.iteri iteri tl in + let len = List.length tl in + let subst = Array.make (1 + len) (make_substituend hd) in + let s = ref tl in + for i = 1 to len do + match !s with + | [] -> assert false + | x :: tl -> + Array.unsafe_set subst i (make_substituend x); + s := tl + done; subst -let substnl laml n = substn_many (make_subst laml) n -let substl laml = substnl laml 0 -let subst1 lam = substl [lam] +let substnl laml n c = substn_many (make_subst laml) n c +let substl laml c = substnl laml 0 c +let subst1 lam c = substl [lam] c -let substnl_decl laml k = map_rel_declaration (substnl laml k) -let substl_decl laml = substnl_decl laml 0 -let subst1_decl lam = substl_decl [lam] +let substnl_decl laml k r = map_rel_declaration (substnl laml k) r +let substl_decl laml r = substnl_decl laml 0 r +let subst1_decl lam r = substl_decl [lam] r -let substnl_named_decl laml k = map_named_declaration (substnl laml k) -let substl_named_decl laml = substnl_named_decl laml 0 -let subst1_named_decl lam = substl_named_decl [lam] +let substnl_named_decl laml k d = map_named_declaration (substnl laml k) d +let substl_named_decl laml d = substnl_named_decl laml 0 d +let subst1_named_decl lam d = substl_named_decl [lam] d (* (thin_val sigma) removes identity substitutions from sigma *) @@ -169,17 +181,18 @@ let rec find_var id = function else find_var id subst (* (replace_vars sigma M) applies substitution sigma to term M *) -let replace_vars var_alist = +let replace_vars var_alist x = let var_alist = thin_val var_alist in - let rec substrec n c = match Constr.kind c with + match var_alist with + | [] -> x + | _ -> + let rec substrec n c = match Constr.kind c with | Constr.Var x -> - (try lift_substituend n (find_var x var_alist) - with Not_found -> c) + (try lift_substituend n (find_var x var_alist) + with Not_found -> c) | _ -> Constr.map_with_binders succ substrec n c - in - match var_alist with - | [] -> (function x -> x) - | _ -> substrec 0 + in + substrec 0 x (* let repvarkey = Profile.declare_profile "replace_vars";; @@ -187,12 +200,12 @@ let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; *) (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) -let subst_var str = replace_vars [(str, Constr.mkRel 1)] +let subst_var str t = replace_vars [(str, Constr.mkRel 1)] t (* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) -let substn_vars p vars = +let substn_vars p vars c = let _,subst = List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars - in replace_vars (List.rev subst) + in replace_vars (List.rev subst) c -let subst_vars = substn_vars 1 +let subst_vars subst c = substn_vars 1 subst c diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2b28c1a75..3de63c9d4 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -312,9 +312,13 @@ let push_rel_context_to_named_context env typ = let inst_vars = List.map mkVar ids in let inst_rels = List.rev (rel_list 0 (nb_rel env)) in let replace_var_named_declaration id0 id (id',b,t) = - let id' = if id_ord id0 id' = 0 then id else id' in + let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - id', Option.map (replace_vars vsubst) b, replace_vars vsubst t + let b = match b with + | None -> None + | Some c -> Some (replace_vars vsubst c) + in + id', b, replace_vars vsubst t in let replace_var_named_context id0 id env = let nc = Environ.named_context env in diff --git a/proofs/goal.ml b/proofs/goal.ml index ebd6ca84d..a036f728d 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -433,9 +433,12 @@ let convert_concl check cl' = (); fun env rdefs gl info -> (* Renames a hypothesis. *) let rename_hyp_sign id1 id2 sign = + let subst = [id1,mkVar id2] in + let replace_vars c = replace_vars subst c in Environ.apply_to_hyp_and_dependent_on sign id1 (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) + (fun d _ -> map_named_declaration replace_vars d) + let rename_hyp id1 id2 = (); fun env rdefs gl info -> let hyps = hyps env rdefs gl info in if not (Names.Id.equal id1 id2) && |