From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 21:41:41 +0200
Subject: Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
---
 interp/topconstr.ml | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'interp/topconstr.ml')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a79f10df6b..94bbc60eaf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms =
     (fun (_, ona, indnal) l ->
       Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
       indnal
-        (Option.fold_right (down_located (name_fold Id.Set.add)) ona l))
+        (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_constr_expr_binders g f n' acc b l) t
   | [] ->
       f n acc b
@@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function
 let rec fold_local_binders g f n acc b = function
   | CLocalAssum (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_local_binders g f n' acc b l) t
   | CLocalDef ((_,na),c,t)::l ->
-      Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
+      Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
   | CLocalPattern (_,(pat,t))::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
@@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
   | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (na,a,t,b) ->
-     f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+     f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
   | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
   | CCast (a,CastCoerce) -> f n acc a
   | CNotation (_,(l,ll,bll)) ->
@@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
   | CLetTuple (nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (name_fold g)) nal n in
-      f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+      let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
+      f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
   | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-	(f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+	(f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
   | CFix (_,l) ->
       let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -198,7 +198,7 @@ let split_at_annot bl na =
 
 (* Used in correctness and interface *)
 
-let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -212,7 +212,7 @@ let map_local_binders f g e bl =
       CLocalAssum(nal,k,ty) ->
         (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
     | CLocalDef((loc,na),c,ty) ->
-        (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
+        (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
     | CLocalPattern (loc,(pat,t)) ->
         let ids = ids_of_pattern pat in
         (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
@@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
   | CLambdaN (bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
   | CLetIn (na,a,t,b) ->
-      CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
   | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
   | CNotation (n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
@@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (name_fold g)) nal e in
-      let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
+      let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
   | CIf (c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
   | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->
-- 
cgit v1.2.3