diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
| commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
| tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /interp/implicit_quantifiers.ml | |
| parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) | |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 39 |
1 files changed, 24 insertions, 15 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 73e3910a..22075654 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: implicit_quantifiers.ml 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -93,7 +93,7 @@ let is_freevar ids env x = with _ -> not (is_global x) with _ -> true -(* Auxilliary functions for the inference of implicitly quantified variables. *) +(* Auxiliary functions for the inference of implicitly quantified variables. *) let ungeneralizable loc id = user_err_loc (loc, "Generalization", @@ -110,7 +110,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = in let rec aux bdvars l c = match c with | CRef (Ident (loc,id)) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) -> + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c @@ -297,19 +297,28 @@ let implicit_application env ?(allow_partial=true) f ty = CAppExpl (loc, (None, id), args), avoid in c, avoid -let implicits_of_rawterm l = +let implicits_of_rawterm ?(with_products=true) l = let rec aux i c = - match c with - RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> - let rest = aux (succ i) b in - if bk = Implicit then - let name = - match na with - Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: rest - else rest + let abs loc na bk t b = + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + | Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true, true)) :: rest + else rest + in + match c with + | RProd (loc, na, bk, t, b) -> + if with_products then abs loc na bk t b + else + (if bk = Implicit then + msg_warning (str "Ignoring implicit status of product binder " ++ + pr_name na ++ str " and following binders"); + []) + | RLambda (loc, na, bk, t, b) -> abs loc na bk t b | RLetIn (loc, na, t, b) -> aux i b | _ -> [] in aux 1 l |