From 7208928de37565a9e38f9540f2bfb1e7a3b877e6 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 17 Sep 2012 20:46:20 +0000 Subject: 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 --- pretyping/cases.ml | 15 +++++++++------ pretyping/detyping.ml | 3 ++- pretyping/termops.ml | 11 ++++++----- pretyping/termops.mli | 3 +++ 4 files changed, 20 insertions(+), 12 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 98cc42aaf..b6b8f8dba 100644 --- a/pretyping/cases.ml +++ b/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) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index da5ccc96b..ce84e6bd5 100644 --- a/pretyping/detyping.ml +++ b/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 diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9db16baac..f8cd3609a 100644 --- a/pretyping/termops.ml +++ b/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 = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index b3e00ebaa..b6bb43868 100644 --- a/pretyping/termops.mli +++ b/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 -- cgit v1.2.3