Generalize instance declarations to any context, better name handling. Add hole kind info for topconstrs.

Derive eta_expansion from functional extensionality axiom.


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

6 files changed, 59 insertions, 25 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 06edeaed2..69d5ad67a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -651,13 +651,13 @@ let rec extern inctx scopes vars r =
 
   | RVar (loc,id) -> CRef (Ident (loc,id))
 
-  | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
+  | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
 
   | REvar (loc,n,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)
+      if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
 
   | RApp (loc,f,args) ->
       (match f with
@@ -756,7 +756,7 @@ let rec extern inctx scopes vars r =
 
   | RSort (loc,s) -> CSort (loc,extern_rawsort s)
 
-  | RHole (loc,e) -> CHole loc
+  | RHole (loc,e) -> CHole (loc, Some e)
 
   | RCast (loc,c, CastConv (k,t)) ->
       CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 033052325..b2c7728fd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -923,8 +923,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let env'' = List.fold_left (push_name_env lvar) env ids 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)
+    | CHole (loc, k) -> 
+	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 162591872..112c2fc18 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -25,16 +25,8 @@ open Typeclasses
 open Typeclasses_errors
 (*i*)
 
-(* Auxilliary functions for the inference of implicitly quantified variables. *)    
-
-let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
-  let found id bdvars l = if Idset.mem id bdvars then l else if List.mem id l then l else id :: l in
-  let rec aux bdvars l c = match c with
-    | CRef (Ident (_,id)) -> found id bdvars l
-    | 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
+let ids_of_list l = 
+  List.fold_right Idset.add l Idset.empty
 
 
 let locate_reference qid =
@@ -59,6 +51,39 @@ let is_freevar ids env x =
       with _ -> not (is_global x)
   with _ -> true
 
+(* Auxilliary functions for the inference of implicitly quantified variables. *)    
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
+  let found id bdvars l = 
+    if List.mem id l then l 
+    else if not (is_freevar bdvars (Global.env ()) id)
+    then l else id :: l 
+  in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident (_,id)) -> found id bdvars l
+    | 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
+
+let ids_of_names l = 
+  List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) = 
+  let rec aux bdvars l c = match c with
+      ((LocalRawAssum (n, _, c)) :: tl) ->
+	let bound = ids_of_names n in
+	let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+    | ((LocalRawDef (n, c)) :: tl) -> 
+	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+	let l' = bound @ free_vars_of_constr_expr c ~bound:bdvars l in
+	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+	
+    | [] -> bdvars, l
+  in aux bound l binders
+
 let rec make_fresh ids env x =
   if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
 
@@ -82,7 +107,10 @@ let compute_constrs_freevars env constrs =
 
 let compute_constrs_freevars_binders env constrs =
   let elts = compute_constrs_freevars env constrs in
-    List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+    List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
+
+let binder_list_of_ids ids =
+  List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
 (*   let rec name_rec id = *)
@@ -139,9 +167,6 @@ let destClassAppExpl cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, l
     | _ -> raise Not_found
 
-let ids_of_list l = 
-  List.fold_right Idset.add l Idset.empty
-
 let full_class_binders env l = 
   let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
   let l', avoid =
@@ -184,7 +209,7 @@ let resolve_class_binders env l =
   let ctx = full_class_binders env l in
   let fv_ctx = 
     let elts = compute_context_freevars env ctx in
-      List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
   in
     fv_ctx, ctx
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 3e26b6c72..ab23e763c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -23,6 +23,7 @@ open Util
 open Typeclasses
 (*i*)
 
+val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> identifier located * constr_expr list
 val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
 
@@ -30,6 +31,13 @@ val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
   Names.identifier list -> Names.identifier list
 
+val binder_list_of_ids : identifier list -> local_binder list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
+val free_vars_of_binders :
+  ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+
 val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
 val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
 val resolve_class_binders : Idset.t -> typeclass_context -> 
@@ -51,10 +59,10 @@ val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> Names.identifier option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  (Names.identifier option * Term.named_declaration) list ->
+  ((Names.identifier * bool) option * Term.named_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index aa3c923eb..97a0f94da 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -565,7 +565,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc
+  | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
@@ -633,7 +633,7 @@ let constr_loc = function
   | CCases (loc,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
-  | CHole loc -> loc
+  | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
   | CEvar (loc,_,_) -> loc
   | CSort (loc,_) -> loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index fa7940faa..6bbc64cca 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -125,7 +125,7 @@ type constr_expr =
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
-  | CHole of loc
+  | CHole of loc * Evd.hole_kind option
   | CPatVar of loc * (bool * patvar)
   | CEvar of loc * existential_key * constr_expr list option
   | CSort of loc * rawsort
@@ -146,6 +146,7 @@ and recursion_order_expr =
   | CWfRec of constr_expr
   | CMeasureRec of constr_expr
 
+(** Anonymous defs allowed ?? *)
 and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * binder_kind * constr_expr