diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-19 22:36:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 09:54:23 +0100 |
| commit | f66e604a9d714ee9dba09234d935ee208bc89d97 (patch) | |
| tree | eef297f9dc05464acebeb1839c4ee979d503195f /kernel/vars.ml | |
| parent | ff8d99117f142dd6851eb7cecc0ae84ec8642fe1 (diff) | |
Experimenting documentation of the Vars.subst functions.
Related questions:
- What balance to find between precision and conciseness?
- What convention to follow for typesetting the different components
of the documentation is unclear?
New tentative type substl to emphasize that substitutions (for substl)
are represented the other way round compared to instances for
application (applist), though there are represented the same way
(i.e. most recent/dependent component on top) as instances of evars
(mkEvar).
Also removing unused subst*_named_decl functions (at least
substnl_named_decl is somehow non-sense).
Diffstat (limited to 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index a800e2531..f8c0a65e6 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -151,6 +151,11 @@ let make_subst = function done; subst +(* The type of substitutions, with term substituting most recent + binder at the head *) + +type substl = Constr.t list + let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c @@ -159,13 +164,6 @@ let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r -let substnl_named_decl laml k d = - map_named_declaration (fun c -> substnl laml k c) d -let substl_named_decl laml d = - map_named_declaration (fun c -> substnl laml 0 c) d -let subst1_named_decl lam d = - map_named_declaration (fun c -> subst1 lam c) d - (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function @@ -197,15 +195,10 @@ let replace_vars var_alist x = in substrec 0 x -(* -let repvarkey = Profile.declare_profile "replace_vars";; -let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;; -*) - -(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *) +(* (subst_var str t) substitute (Var str) by (Rel 1) in t *) 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 *) +(* (subst_vars [id1;...;idn] t) substitute (Var idj) by (Rel j) in t *) let substn_vars p vars c = let _,subst = List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars |