Factorisation des opérations sur le type option de Util dans un module

lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting 
des fonctions (à un ou deux arguments tous ou partie de type option).

Il reste quelques opérations dans Util à propos desquelles je ne suis 
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain 
car il est tard (comme some_in qui devrait devenir Option.make je 
suppose) . Elles s'expriment souvent facilement en fonction des 
autres, par exemple "option_compare x y"  est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est 
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.

J'en ai profité aussi pour remplacer les trop nombreux "failwith" par 
des erreurs locales au module, donc plus robustes.

J'ai trouvé aussi une fonction qui était définie deux fois, et une 
définie dans un module particulier.

Mon seul bémol (mais facile à traiter) c'est la proximité entre le 
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de 
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 53 insertions, 58 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ec88e6fe85..ec74c91b25 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -233,11 +233,6 @@ and check_same_fix_binder bl1 bl2 =
 let same c d = try check_same_type c d; true with _ -> false
 
 (* Idem for rawconstr *)
-let option_iter2 f o1 o2 = 
-  match o1, o2 with
-      Some o1, Some o2 -> f o1 o2
-    | None, None -> ()
-    | _ -> failwith "option"
 
 let array_iter2 f v1 v2 =
   List.iter2 f (Array.to_list v1) (Array.to_list v2)
@@ -256,7 +251,7 @@ let rec same_raw c d =
    | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
    | REvar(_,e1,a1), REvar(_,e2,a2) ->
        if e1 <> e2 then failwith "REvar";
-       option_iter2(List.iter2 same_raw) a1 a2
+       Option.iter2(List.iter2 same_raw) a1 a2
   | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
   | RApp(_,f1,a1), RApp(_,f2,a2) ->
       List.iter2 same_raw (f1::a1) (f2::a2)
@@ -274,7 +269,7 @@ let rec same_raw c d =
         (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
           same_raw t1 t2;
           if al1 <> al2 then failwith "RCases";
-          option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
+          Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
             if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
       List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
         List.iter2 same_patt pl1 pl2;
@@ -290,7 +285,7 @@ let rec same_raw c d =
       array_iter2
         (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
           if na1<>na2 then failwith "RRec";
-          option_iter2 same_raw bd1 bd2;
+          Option.iter2 same_raw bd1 bd2;
           same_raw ty1 ty2)) bl1 bl2;
       array_iter2 same_raw ty1 ty2;
       array_iter2 same_raw def1 def2
@@ -659,7 +654,7 @@ let rec extern inctx scopes vars r =
   | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
 
   | REvar (loc,n,l) ->
-      extern_evar loc n (option_map (List.map (extern false scopes vars)) l)
+      extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
 
   | RPatVar (loc,n) ->
       if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
@@ -699,17 +694,17 @@ let rec extern inctx scopes vars r =
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
-      let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in
+      let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
       let tml = List.map (fun (tm,(na,x)) ->
         let na' = match na,tm with
             Anonymous, RVar (_,id) when 
-              rtntypopt<>None & occur_rawconstr id (out_some rtntypopt)
+              rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
               -> Some Anonymous
           | Anonymous, _ -> None
           | Name id, RVar (_,id') when id=id' -> None
           | Name _, _ -> Some na in
 	(sub_extern false scopes vars tm,
-	(na',option_map (fun (loc,ind,n,nal) ->
+	(na',Option.map (fun (loc,ind,n,nal) ->
 	  let params = list_tabulate
 	    (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
 	  let args = List.map (function
@@ -722,15 +717,15 @@ let rec extern inctx scopes vars r =
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (option_map (fun _ -> na) typopt,
-         option_map (extern_typ scopes (add_vname vars na)) typopt),
+        (Option.map (fun _ -> na) typopt,
+         Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (option_map (fun _ -> na) typopt,
-         option_map (extern_typ scopes (add_vname vars na)) typopt),
+        (Option.map (fun _ -> na) typopt,
+         Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -949,12 +944,12 @@ let rec raw_of_pat env = function
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
         (* ind is None only if no branch and no return type *)
-      let ind = out_some indo in
+      let ind = Option.get indo in
       let mat = simple_cases_matrix_of_branches ind brns brs in
       let indnames,rtn =
 	if p = PMeta None then (Anonymous,None),None
 	else 
-	  let nparams,n = out_some ind_nargs in
+	  let nparams,n = Option.get ind_nargs in
 	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
       RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0d9f957956..6fc7a7d310 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -226,7 +226,7 @@ let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
 let set_var_scope loc id (_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
   if !idscopes <> None & 
-    make_current_scope (out_some !idscopes)
+    make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
       pr_id id ++ str " already occurs in a different scope")
@@ -796,7 +796,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg c f =
-	       let before, after = list_chop (succ (out_some n)) bl in
+	       let before, after = list_chop (succ (Option.get n)) bl in
 	       let ((ids',_,_),rafter) =
 		 List.fold_left intern_local_binder (env,[]) after in
 	       let ro = (intern (ids', tmp_scope, scopes) c) in
@@ -898,21 +898,21 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	    let (tm,ind),nal = intern_case_item env citm in
 	    (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
 	  tms ([],env) in
-        let rtnpo = option_map (intern_type env') rtnpo in
+        let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	RCases (loc, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_map (intern_type env'') po in
+        let p' = Option.map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
         let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = option_map (intern_type env'') po in
+        let p' = Option.map (intern_type env'') po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, Evd.QuestionMark true)
@@ -921,7 +921,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
     | CEvar (loc, n, l) ->
-	REvar (loc, n, option_map (List.map (intern env)) l)
+	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
 	RSort(loc,s)
     | CCast (loc, c1, CastConv (k, c2)) ->
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 930cfe7394..fc93f455a2 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -223,7 +223,7 @@ let app_list1 f = function
 let app_opt f = function
   | (OptArgType t as u, l) ->
       let o = Obj.magic l in
-      (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
+      (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
   | _ -> failwith "Genarg: not an opt"
 
 let app_pair f1 f2 = function
diff --git a/interp/notation.ml b/interp/notation.ml
index aaab6a933f..d5de23bc5d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
 type local_scopes = tmp_scope_name option * scope_name list
 
 let make_current_scopes (tmp_scope,scopes) =
-  option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+  Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
 
 (**********************************************************************)
 (* Delimiters *)
@@ -143,7 +143,7 @@ let delimiters_map = ref Gmap.empty
 let declare_delimiters scope key =
   let sc = find_scope scope in
   if sc.delimiters <> None && Options.is_verbose () then begin
-    let old = out_some sc.delimiters in
+    let old = Option.get sc.delimiters in
     Options.if_verbose 
       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
   end;
@@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
-    (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
+    (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> option_map mkString (uninterp r)), inpat)
+    (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.absolute_reference sp in ()
@@ -396,7 +396,7 @@ let uninterp_prim_token_cases_pattern c =
 let availability_of_prim_token printer_scope local_scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
   let scopes = make_current_scopes local_scopes in
-  option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
@@ -454,7 +454,7 @@ type arguments_scope_discharge_request =
   | ArgsScopeNoDischarge
 
 let load_arguments_scope _ (_,(_,r,scl)) =
-  List.iter (option_iter check_scope) scl;
+  List.iter (Option.iter check_scope) scl;
   arguments_scope := Refmap.add r scl !arguments_scope
 
 let cache_arguments_scope o =
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 5a8eafff7b..131ce29701 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -59,17 +59,17 @@ let rec unloc = function
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
   | RCases (_,rtntypopt,tml,pl) ->
       RCases (dummy_loc,
-        (option_map unloc rtntypopt),
+        (Option.map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
   | RLetTuple (_,nal,(na,po),b,c) ->
-      RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
+      RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
   | RIf (_,c,(na,po),b1,b2) ->
-      RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
+      RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,bl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,
             Array.map (List.map 
-              (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
+              (fun (na,obd,ty) -> (na,Option.map unloc obd, unloc ty)))
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a44f0b6b43..fcf3839377 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -94,14 +94,14 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 	let ((idl,e),patl) =
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
-      RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
+      RCases (loc,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
       let e,nal = list_fold_map (name_fold_map g) e nal in 
       let e,na = name_fold_map g e na in
-      RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
+      RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
       let e,na = name_fold_map g e na in
-      RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
+      RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
   | ACast (c,k) -> RCast (loc,f e c, 
 			  match k with 
 			    | CastConv (k,t) -> CastConv (k,f e t)
@@ -185,20 +185,20 @@ let aconstr_and_vars_of_rawconstr a =
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
   | RCases (_,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
-      ACases (option_map aux rtntypopt,
+      ACases (Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
-	  option_iter
+	  Option.iter
 	    (fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
+          (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
         List.map f eqnl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
       List.iter (add_name found) nal;
-      ALetTuple (nal,(na,option_map aux po),aux b,aux c)
+      ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
-      AIf (aux c,(na,option_map aux po),aux b1,aux b2)
+      AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
   | RCast (_,c,k) -> ACast (aux c, 
 			    match k with CastConv (k,t) -> CastConv (k,aux t) 
 			      | CastCoerce -> CastCoerce)
@@ -305,11 +305,11 @@ let rec subst_aconstr subst bound raw =
 	  ALetIn (n,r1',r2')
 
   | ACases (rtntypopt,rl,branches) -> 
-      let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+      let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
 	  let a' = subst_aconstr subst bound a in
-	  let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
+	  let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
 	    let indkn' = subst_kn subst indkn in
 	    if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -327,14 +327,14 @@ let rec subst_aconstr subst bound raw =
           ACases (rtntypopt',rl',branches')
 
   | ALetTuple (nal,(na,po),b,c) ->
-      let po' = option_smartmap (subst_aconstr subst bound) po
+      let po' = Option.smartmap (subst_aconstr subst bound) po
       and b' = subst_aconstr subst bound b 
       and c' = subst_aconstr subst bound c in
 	if po' == po && b' == b && c' == c then raw else
 	  ALetTuple (nal,(na,po'),b',c')
 
   | AIf (c,(na,po),b1,b2) ->
-      let po' = option_smartmap (subst_aconstr subst bound) po
+      let po' = Option.smartmap (subst_aconstr subst bound) po
       and b1' = subst_aconstr subst bound b1
       and b2' = subst_aconstr subst bound b2 
       and c' = subst_aconstr subst bound c in
@@ -368,7 +368,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
 (* Pattern-matching rawconstr and aconstr *)
 
 let abstract_return_type_context pi mklam tml rtno =
-  option_map (fun rtn ->
+  Option.map (fun rtn ->
     let nal =
       List.flatten (List.map (fun (_,(na,t)) ->
 	match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -663,8 +663,8 @@ let ids_of_cases_indtype =
 let ids_of_cases_tomatch tms =
   List.fold_right
     (fun (_,(ona,indnal)) l ->
-      option_fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (option_fold_right name_cons ona l))
+      Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
+      indnal (Option.fold_right name_cons ona l))
     tms []
 
 let is_constructor id =
@@ -715,17 +715,17 @@ let fold_constr_expr_with_binders g f n acc = function
       acc
   | CCases (loc,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
-      let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in
+      let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map fst al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
 	f (Idset.fold g ids n) acc rhs) bl acc
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let n' = List.fold_right (name_fold g) nal n in
-      f (option_fold_right (name_fold g) ona n') (f n acc b) c
+      f (Option.fold_right (name_fold 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 (name_fold g) ona n)) acc po
+      Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
   | CFix (loc,_,l) ->
       let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -828,15 +828,15 @@ let map_constr_expr_with_binders g f e = function
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
       let ids = ids_of_cases_tomatch a in
-      let po = option_map (f (List.fold_right g ids e)) rtnpo in
+      let po = Option.map (f (List.fold_right g ids e)) rtnpo in
       CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
-      let e'' = option_fold_right (name_fold g) ona e in
-      CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
+      let e'' = Option.fold_right (name_fold g) ona e in
+      CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
   | CIf (loc,c,(ona,po),b1,b2) ->
-      let e' = option_fold_right (name_fold g) ona e in
-      CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
+      let e' = Option.fold_right (name_fold g) ona e in
+      CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
         let (e',bl') = map_local_binders f g e bl in