Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
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...
commit 7208928de37565a9e38f9540f2bfb1e7a3b877e6 1 parent a6dac99
@ppedrot ppedrot authored
View
16 checker/checker.ml
@@ -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
12 interp/reserve.ml
@@ -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
36 lib/cList.ml
@@ -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
15 lib/cList.mli
@@ -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
5 lib/util.ml
@@ -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
6 lib/util.mli
@@ -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
2  library/nameops.ml
@@ -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
2  library/nameops.mli
@@ -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
23 parsing/egramcoq.ml
@@ -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
15 parsing/pcoq.ml4
@@ -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
View
25 plugins/extraction/extract_env.ml
@@ -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 =
View
4 plugins/extraction/ocaml.ml
@@ -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
6 plugins/funind/indfun.ml
@@ -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
19 plugins/funind/invfun.ml
@@ -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
7 plugins/funind/recdef.ml
@@ -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|])::
View
4 plugins/romega/refl_omega.ml
@@ -929,10 +929,10 @@ let filter_compatible_systems required systems =
let rec select = function
(x::l) ->
if List.mem x required then select l
- else if List.mem (barre x) required then failwith "Exit"
+ else if List.mem (barre x) required then raise Exit
else x :: select l
| [] -> [] in
- map_succeed (function (sol,splits) -> (sol,select splits)) systems
+ List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems
let rec equas_of_solution_tree = function
Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
View
15 pretyping/cases.ml
@@ -1409,20 +1409,23 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
- [subst0] is made of items [(p,u,(u,ty))] where [ty] is the type of [u]
and both are adjusted to [extenv] while [p] is the index of [id] in
[extenv] (after expansion of the aliases) *)
- let subst0 = map_succeed (fun (x,u) ->
+ let map (x, u) =
(* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
(* \--env-/ (= x:ty) *)
(* \--------------extenv------------/ *)
- let (p,_,_) = lookup_rel_id x (rel_context extenv) in
+ let (p, _, _) = lookup_rel_id x (rel_context extenv) in
let rec traverse_local_defs p =
match pi2 (lookup_rel p extenv) with
| Some c -> assert (isRel c); traverse_local_defs (p + destRel c)
| None -> p in
let p = traverse_local_defs p in
- let u = lift (n'-n) u in
- (p,u,expand_vars_in_term extenv u)) subst in
- let t0 = lift (n'-n) t in
- (subst0,t0)
+ let u = lift (n' - n) u in
+ try Some (p, u, expand_vars_in_term extenv u)
+ (* pedrot: does this really happen to raise [Failure _]? *)
+ with Failure _ -> None in
+ let subst0 = List.map_filter map subst in
+ let t0 = lift (n' - n) t in
+ (subst0, t0)
let push_binder d (k,env,subst) =
(k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
View
3  pretyping/detyping.ml
@@ -687,7 +687,8 @@ let simple_cases_matrix_of_branches ind brs =
let nal,c = it_destRLambda_or_LetIn_names n b in
let mkPatVar na = PatVar (Loc.ghost,na) in
let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in
- let ids = map_succeed Nameops.out_name nal in
+ let map name = try Some (Nameops.out_name name) with Failure _ -> None in
+ let ids = List.map_filter map nal in
(Loc.ghost,ids,[p],c))
brs
View
11 pretyping/termops.ml
@@ -217,12 +217,13 @@ let push_named_rec_types (lna,typarray,_) env =
(fun e assum -> push_named assum e) env ctxt
let lookup_rel_id id sign =
- let rec lookrec = function
- | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
- | (n, (Name id',b,t)::l) -> if id' = id then (n,b,t) else lookrec (n+1,l)
- | (_, []) -> raise Not_found
+ let rec lookrec n = function
+ | [] -> raise Not_found
+ | (Anonymous, _, _) :: l -> lookrec (n + 1) l
+ | (Name id', b, t) :: l ->
+ if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l
in
- lookrec (1,sign)
+ lookrec 1 sign
(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
let mkProd_or_LetIn (na,body,t) c =
View
3  pretyping/termops.mli
@@ -40,7 +40,10 @@ val print_env : env -> std_ppcmds
val push_rel_assum : name * types -> env -> env
val push_rels_assum : (name * types) list -> env -> env
val push_named_rec_types : name array * types array * 'a -> env -> env
+
val lookup_rel_id : identifier -> rel_context -> int * constr option * types
+(** Associates the contents of an identifier in a [rel_context]. Raise
+ [Not_found] if there is no such identifier. *)
(** builds argument lists matching a block of binders or a context *)
val rel_vect : int -> int -> constr array
View
16 tactics/auto.ml
@@ -538,9 +538,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty)
let make_resolves env sigma flags pri ?name c =
let cty = Retyping.get_type_of env sigma c in
- let ents =
- map_succeed
- (fun f -> f (c,cty))
+ let try_apply f =
+ try Some (f (c, cty)) with Failure _ -> None in
+ let ents = List.map_filter try_apply
[make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
in
if ents = [] then
@@ -912,11 +912,11 @@ let pr_hints_db (name,db,hintlist) =
(* Print all hints associated to head c in any database *)
let pr_hint_list_for_head c =
let dbs = Hintdbmap.to_list !searchtable in
- let valid_dbs =
- map_succeed
- (fun (name,db) -> (name,db, List.map (fun v -> 0, v) (Hint_db.map_all c db)))
- dbs
+ let validate (name, db) =
+ let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in
+ (name, db, hints)
in
+ let valid_dbs = List.map validate dbs in
if valid_dbs = [] then
(str "No hint declared for :" ++ pr_global c)
else
@@ -941,7 +941,7 @@ let pr_hint_term cl =
with Bound -> Hint_db.map_none
in
let fn db = List.map (fun x -> 0, x) (fn db) in
- map_succeed (fun (name, db) -> (name, db, fn db)) dbs
+ List.map (fun (name, db) -> (name, db, fn db)) dbs
in
if valid_dbs = [] then
(str "No hint applicable for current goal")
View
4 tactics/class_tactics.ml4
@@ -257,8 +257,8 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
hints)
else []
in
- (hints @ map_succeed
- (fun f -> try f (c,cty) with UserError _ -> failwith "")
+ (hints @ List.map_filter
+ (fun f -> try Some (f (c, cty)) with Failure _ | UserError _ -> None)
[make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri])
else []
View
32 tactics/equality.ml
@@ -1075,20 +1075,21 @@ let simplify_args env sigma t =
let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
let e = next_ident_away eq_baseid (ids_of_context env) in
- let e_env = push_named (e,None,t) env in
- let injectors =
- map_succeed
- (fun (cpath,t1',t2') ->
- (* arbitrarily take t1' as the injector default value *)
- let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
- let injfun = mkNamedLambda e t injbody in
- let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
- let pf_typ = get_type_of env sigma pf in
- let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
- let pf = clenv_value_cast_meta inj_clause in
- let ty = simplify_args env sigma (clenv_type inj_clause) in
- (pf,ty))
- posns in
+ let e_env = push_named (e, None,t) env in
+ let filter (cpath, t1', t2') =
+ try
+ (* arbitrarily take t1' as the injector default value *)
+ let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
+ let injfun = mkNamedLambda e t injbody in
+ let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
+ let pf_typ = get_type_of env sigma pf in
+ let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+ let pf = clenv_value_cast_meta inj_clause in
+ let ty = simplify_args env sigma (clenv_type inj_clause) in
+ Some (pf, ty)
+ with Failure _ -> None
+ in
+ let injectors = List.map_filter filter posns in
if injectors = [] then
errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
tclTHEN
@@ -1493,7 +1494,8 @@ let subst_all ?(flags=default_subst_tactic_flags ()) gl =
match kind_of_term y with Var y -> y | _ -> failwith "caught"
with PatternMatchingFailure -> failwith "caught"
in
- let ids = map_succeed test (pf_hyps_types gl) in
+ let test p = try Some (test p) with Failure _ -> None in
+ let ids = List.map_filter test (pf_hyps_types gl) in
let ids = List.uniquize ids in
subst_gen flags.rewrite_dependent_proof ids gl
View
8 tactics/tactics.ml
@@ -1024,9 +1024,11 @@ let progress_with_clause flags innerclause clause =
let ordered_metas = List.rev (clenv_independent clause) in
if ordered_metas = [] then error "Statement without assumptions.";
let f mv =
- find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
- try List.try_find f ordered_metas
- with Failure _ -> error "Unable to unify."
+ try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause)
+ with Failure _ -> None
+ in
+ try List.find_map f ordered_metas
+ with Not_found -> error "Unable to unify."
let apply_in_once_main flags innerclause (d,lbind) gl =
let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
View
16 toplevel/mltop.ml4
@@ -144,18 +144,20 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Names.id_of_string d
with _ ->
- if_warn msg_warning
- (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
- flush_all ();
- failwith "caught"
+ if_warn 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 = Names.repr_dirpath coq_root in
- let convert_dirs (lp,cp) =
- (lp,Names.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 (fun lpe -> add_ml_dir (fst lpe)) dirs;
add_ml_dir unix_path;
List.iter (Library.add_load_path false) dirs;
Please sign in to comment.
Something went wrong with that request. Please try again.