Permalink
Browse files

More cleaning on Utils and CList. Some parts of the code being

peculiarly messy, I hope I did not introduce too many bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent a6dac99 commit 7208928de37565a9e38f9540f2bfb1e7a3b877e6 ppedrot committed Sep 17, 2012
View
@@ -72,18 +72,20 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try id_of_string d
with _ ->
- if_verbose msg_warning
- (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
- flush_all ();
- failwith "caught"
+ if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+ raise Exit
let add_rec_path ~unix_path ~coq_root =
if exists_dir unix_path then
let dirs = all_subdirs ~unix_path in
let prefix = repr_dirpath coq_root in
- let convert_dirs (lp,cp) =
- (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
- let dirs = map_succeed convert_dirs dirs in
+ let convert_dirs (lp, cp) =
+ try
+ let path = List.map convert_string (List.rev cp) @ prefix in
+ Some (lp, Names.make_dirpath path)
+ with Exit -> None
+ in
+ let dirs = List.map_filter convert_dirs dirs in
List.iter Check.add_load_path dirs;
Check.add_load_path (unix_path, coq_root)
else
View
@@ -77,10 +77,14 @@ let revert_reserved_type t =
try
let l = Gmapl.find (constr_key t) !reserve_revtable in
let t = Detyping.detype false [] [] t in
- List.try_find
- (fun (pat,id) ->
- try let _ = Notation_ops.match_notation_constr false t ([], pat) in Name id
- with Notation_ops.No_match -> failwith "") l
+ (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
+ then I've introduced a bug... *)
+ let find (pat, id) =
+ try let _ = Notation_ops.match_notation_constr false t ([], pat) in true
+ with Notation_ops.No_match -> false
+ in
+ let (_, id) = List.find find l in
+ Name id
with Not_found | Failure _ -> Anonymous
let _ = Namegen.set_reserved_typed_name revert_reserved_type
View
@@ -118,8 +118,7 @@ sig
val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
- val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
- val try_find : ('a -> 'b) -> 'a list -> 'b
+ val find_map : ('a -> 'b option) -> 'a list -> 'b
val uniquize : 'a list -> 'a list
(** merges two sorted lists and preserves the uniqueness property: *)
@@ -143,7 +142,6 @@ sig
(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
val map_append : ('a -> 'b list) -> 'a list -> 'b list
- val join_map : ('a -> 'b list) -> 'a list -> 'b list
(** raises [Invalid_argument] if the two lists don't have the same length *)
val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
@@ -169,14 +167,12 @@ sig
val combinations : 'a list list -> 'a list list
val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
- (** Keep only those products that do not return None *)
- val cartesian_filter :
- ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
val cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+ (** Keep only those products that do not return None *)
- val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+
end
include List
@@ -555,12 +551,12 @@ let try_find_i f =
in
try_find_f
-let try_find f =
- let rec try_find_f = function
- | [] -> failwith "try_find"
- | h::t -> try f h with Failure _ -> try_find_f t
- in
- try_find_f
+let rec find_map f = function
+| [] -> raise Not_found
+| x :: l ->
+ match f x with
+ | None -> find_map f l
+ | Some y -> y
let uniquize l =
let visited = Hashtbl.create 23 in
@@ -722,7 +718,6 @@ let drop_prefix p l =
| None -> l
let map_append f l = List.flatten (List.map f l)
-let join_map = map_append (* Alias *)
let map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
@@ -760,18 +755,6 @@ let rec assoc_f f a = function
| (x, e) :: xs -> if f a x then e else assoc_f f a xs
| [] -> raise Not_found
-(* Specification:
- - =p= is set equality (double inclusion)
- - f such that \forall l acc, (f l acc) =p= append (f l []) acc
- - let g = fun x -> f x [] in
- - union_map f l acc =p= append (flatten (map g l)) acc
- *)
-let union_map f l acc =
- List.fold_left
- (fun x y -> f y x)
- acc
- l
-
(* A generic cartesian product: for any operator (**),
[cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
and so on if there are more elements in the lists. *)
@@ -817,4 +800,3 @@ let rec factorize_left = function
(a,(b::List.map snd al)) :: factorize_left l'
| [] ->
[]
-
View
@@ -150,8 +150,10 @@ sig
val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
- val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
- val try_find : ('a -> 'b) -> 'a list -> 'b
+
+ val find_map : ('a -> 'b option) -> 'a list -> 'b
+ (** Returns the first element that is mapped to [Some _]. Raise [Not_found] if
+ there is none. *)
val uniquize : 'a list -> 'a list
(** Return the list of elements without duplicates. *)
@@ -184,9 +186,6 @@ sig
val map_append : ('a -> 'b list) -> 'a list -> 'b list
(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
- val join_map : ('a -> 'b list) -> 'a list -> 'b list
- (** Alias of [map_append]. *)
-
val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
(** As [map_append]. Raises [Invalid_argument _] if the two lists don't have
the same length. *)
@@ -215,14 +214,10 @@ sig
val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
- val cartesian_filter :
- ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
- (** Keep only those products that do not return None *)
-
val cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+ (** Keep only those products that do not return None *)
- val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val factorize_left : ('a * 'b) list -> ('a * 'b list) list
end
View
@@ -441,11 +441,6 @@ let interval n m =
in
interval_n ([],m)
-
-let map_succeed f l =
- let filter x = try Some (f x) with Failure _ -> None in
- List.map_filter filter l
-
(*s Memoization *)
let memo1_eq eq f =
View
@@ -118,12 +118,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
-
-(** In [map_succeed f l] an element [a] is removed if [f a] raises
- [Failure _] otherwise behaves as [List.map f l] *)
-
-val map_succeed : ('a -> 'b) -> 'a list -> 'b list
-
(** {6 Memoization. } *)
(** General comments on memoization:
View
@@ -114,7 +114,7 @@ let atompart_of_id id = fst (repr_ident id)
let out_name = function
| Name id -> id
- | Anonymous -> failwith "out_name: expects a defined name"
+ | Anonymous -> failwith "Nameops.out_name"
let name_fold f na a =
match na with
View
@@ -26,6 +26,8 @@ val lift_subscript : identifier -> identifier
val forget_subscript : identifier -> identifier
val out_name : name -> identifier
+(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
+ otherwise. *)
val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
val name_iter : (identifier -> unit) -> name -> unit
View
@@ -171,12 +171,13 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
grammar_extend entry reinit (pos,[(name, p4assoc, [])])
let pure_sublevels level symbs =
- map_succeed
- (function s ->
- let i = level_of_snterml s in
- if level = Some i then failwith "";
- i)
- symbs
+ let filter s =
+ try
+ let i = level_of_snterml s in
+ if level = Some i then None else Some i
+ with Failure _ -> None
+ in
+ List.map_filter filter symbs
let extend_constr (entry,level) (n,assoc) mkact forpat rules =
List.fold_left (fun nb pt ->
@@ -260,11 +261,11 @@ let extend_grammar gram =
grammar_state := (nb,gram) :: !grammar_state
let recover_notation_grammar ntn prec =
- let l = map_succeed (function
- | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
- vars, x
- | _ ->
- failwith "") !grammar_state in
+ let filter = function
+ | _, Notation (prec', vars, (_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+ Some (vars, x)
+ | _ -> None in
+ let l = List.map_filter filter !grammar_state in
assert (List.length l = 1);
List.hd l
View
@@ -545,12 +545,15 @@ let rec list_mem_assoc_triple x = function
| (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
let register_empty_levels forpat levels =
- map_succeed (fun n ->
- let levels = (if forpat then snd else fst) (List.hd !level_stack) in
- if not (list_mem_assoc_triple n levels) then
- find_position_gen forpat true None (Some n)
- else
- failwith "") levels
+ let filter n =
+ try
+ let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+ if not (list_mem_assoc_triple n levels) then
+ Some (find_position_gen forpat true None (Some n))
+ else None
+ with Failure _ -> None
+ in
+ List.map_filter filter levels
let find_position forpat assoc level =
find_position_gen forpat false assoc level
@@ -30,17 +30,24 @@ let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
let mp,_,l = repr_kn kn in
- let seb = match Libobject.object_tag o with
- | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
- | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
- | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+ begin match Libobject.object_tag o with
+ | "CONSTANT" ->
+ let constant = Global.lookup_constant (constant_of_kn kn) in
+ Some (l, SFBconst constant)
+ | "INDUCTIVE" ->
+ let inductive = Global.lookup_mind (mind_of_kn kn) in
+ Some (l, SFBmind inductive)
+ | "MODULE" ->
+ let modl = Global.lookup_module (MPdot (mp, l)) in
+ Some (l, SFBmodule modl)
| "MODULE TYPE" ->
- SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
- | _ -> failwith "caught"
- in l,seb
- | _ -> failwith "caught"
+ let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+ Some (l, SFBmodtype modtype)
+ | _ -> None
+ end
+ | _ -> None
in
- SEBstruct (List.rev (map_succeed get_reference seg))
+ SEBstruct (List.rev (List.map_filter get_reference seg))
let environment_until dir_opt =
@@ -634,7 +634,7 @@ and pp_module_type params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp, sign) ->
push_visible mp params;
- let l = map_succeed pp_specif sign in
+ let l = List.map pp_specif sign in
pop_visible ();
str "sig " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +707,7 @@ and pp_module_expr params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEstruct (mp, sel) ->
push_visible mp params;
- let l = map_succeed pp_structure_elem sel in
+ let l = List.map pp_structure_elem sel in
pop_visible ();
str "struct " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
View
@@ -97,11 +97,7 @@ let functional_induction with_clean c princl pat =
if with_clean
then
let idl =
- map_succeed
- (fun id ->
- if Idset.mem id old_idl then failwith "subst_and_reduce";
- id
- )
+ List.filter (fun id -> not (Idset.mem id old_idl))
(Tacmach.pf_ids_of_hyps g)
in
let flag =
View
@@ -116,10 +116,13 @@ let generate_type g_to_f f graph i =
| (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
in
let nb_args = List.length fun_ctxt in
- let args_from_decl i decl =
- match decl with
- | (_,Some _,_) -> incr i; failwith "args_from_decl"
- | _ -> let j = !i in incr i;mkRel (nb_args - j + 1)
+ let rec args_from_decl i accu = function
+ | [] -> accu
+ | (_, Some _, _) :: l ->
+ args_from_decl (succ i) accu l
+ | _ :: l ->
+ let t = mkRel (nb_args - i + 1) in
+ args_from_decl (succ i) (t :: accu) l
in
(*i We need to name the vars [res] and [fv] i*)
let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
@@ -131,12 +134,11 @@ let generate_type g_to_f f graph i =
let fv_id =
Namegen.next_ident_away_in_goal
(id_of_string "fv")
- (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
+ (res_id::(List.map_filter (function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None) fun_ctxt))
in
(*i we can then type the argument to be applied to the function [f] i*)
let args_as_rels =
- let i = ref 0 in
- Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt)))
+ Array.of_list (args_from_decl 0 [] fun_ctxt)
in
let args_as_rels = Array.map Termops.pop args_as_rels in
(*i
@@ -152,8 +154,7 @@ let generate_type g_to_f f graph i =
i*)
let graph_applied =
let args_and_res_as_rels =
- let i = ref 0 in
- Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) )
+ Array.of_list (args_from_decl 0 [] ((Name res_id,None,res_type) :: fun_ctxt))
in
let args_and_res_as_rels =
Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels
View
@@ -667,11 +667,10 @@ let mkDestructEq :
fun not_on_hyp expr g ->
let hyps = pf_hyps g in
let to_revert =
- Util.map_succeed
- (fun (id,_,t) ->
+ Util.List.map_filter
+ (fun (id, _, t) ->
if List.mem id not_on_hyp || not (Termops.occur_term expr t)
- then failwith "is_expr_context";
- id) hyps in
+ then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
let type_of_expr = pf_type_of g expr in
let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
Oops, something went wrong.

0 comments on commit 7208928

Please sign in to comment.