Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

10 files changed, 134 insertions, 64 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 193b38dd..82e3cbe1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -140,14 +140,18 @@ let extern_evar loc n l =
 let debug_global_reference_printer =
   ref (fun _ -> failwith "Cannot print a global reference")
 
+let in_debugger = ref false
+
 let set_debug_global_reference_printer f =
   debug_global_reference_printer := f
 
 let extern_reference loc vars r =
-  try Qualid (loc,shortest_qualid_of_global vars r)
-  with Not_found ->
-    (* happens in debugger *)
+  if !in_debugger then
+    (* Debugger does not have the tables of global reference at hand *)
     !debug_global_reference_printer loc r
+  else
+    Qualid (loc,shortest_qualid_of_global vars r)
+
 
 (************************************************************************)
 (* Equality up to location (useful for translator v8) *)
@@ -344,7 +348,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       let p =
 	try
-          if !Flags.raw_print then raise Exit;
+          if !in_debugger || !Flags.raw_print then raise Exit;
 	  let projs = Recordops.lookup_projections (fst cstrsp) in
 	  let rec ip projs args acc =
 	    match projs with
@@ -447,6 +451,7 @@ let is_needed_for_correct_partial_application tail imp =
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let explicitize loc inctx impl (cf,f) args =
+  let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
@@ -482,7 +487,9 @@ let explicitize loc inctx impl (cf,f) args =
 	if args = [] then f else CApp (loc, (None, f), args)
 
 let extern_global loc impl f =
-  if impl <> [] & List.for_all is_status_implicit impl then
+  if not !Constrintern.parsing_explicit &&
+     impl <> [] && List.for_all is_status_implicit impl
+  then
     CAppExpl (loc, (None, f), [])
   else
     CRef f
@@ -491,7 +498,7 @@ let extern_app loc inctx impl (cf,f) args =
   if args = [] (* maybe caused by a hidden coercion *) then
     extern_global loc impl f
   else
-  if
+  if not !Constrintern.parsing_explicit &&
     ((!Flags.raw_print or
       (!print_implicits & not !print_implicits_explicit_args)) &
      List.exists is_status_implicit impl)
@@ -761,7 +768,7 @@ and factorize_prod scopes vars aty c =
 and factorize_lambda inctx scopes vars aty c =
   try
     if !Flags.raw_print or !print_no_symbol then raise No_match;
-    ([],extern_symbol scopes vars c (uninterp_notations c))
+    ([],extern_symbol (Some Notation.type_scope,snd scopes) vars c (uninterp_notations c))
   with No_match -> match c with
   | GLambda (loc,na,bk,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
@@ -889,21 +896,30 @@ let extern_glob_type vars c =
 
 let loc = dummy_loc (* for constr and pattern, locations are lost *)
 
-let extern_constr_gen at_top scopt env t =
-  let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_constr_gen goal_concl_style scopt env t =
+  (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
+  (* i.e.: avoid using the names of goal/section/rel variables and the short *)
+  (* names of global definitions of current module when computing names for *)
+  (* bound variables. *)
+  (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
+  (* those goal/section/rel variables that occurs in the subterm under *)
+  (* consideration; see namegen.ml for further details *)
+  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let rel_env_names = names_of_rel_context env in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
 
-let extern_constr_in_scope at_top scope env t =
-  extern_constr_gen at_top (Some scope) env t
+let extern_constr_in_scope goal_concl_style scope env t =
+  extern_constr_gen goal_concl_style (Some scope) env t
 
-let extern_constr at_top env t =
-  extern_constr_gen at_top None env t
+let extern_constr goal_concl_style env t =
+  extern_constr_gen goal_concl_style None env t
 
-let extern_type at_top env t =
-  let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
+let extern_type goal_concl_style env t =
+  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let rel_env_names = names_of_rel_context env in
+  let r = Detyping.detype goal_concl_style avoid rel_env_names t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort s = extern_glob_sort (detype_sort s)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e1fdd068..2a53eb85 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -53,6 +53,7 @@ val print_projections : bool ref
 (** Debug printing options *)
 val set_debug_global_reference_printer :
   (loc -> global_reference -> reference) -> unit
+val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b161d001..1dd735ad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -166,6 +166,8 @@ let error_inductive_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
+let parsing_explicit = ref false
+
 let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
@@ -408,12 +410,12 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
   | LocalRawAssum(nal,bk,ty) ->
       (match bk with
       | Default k ->
-          let (loc,na) = List.hd nal in
-	  (* TODO: fail if several names with different implicit types *)
-	  let ty = locate_if_isevar loc na (intern_type env ty) in
+	  let ty = intern_type env ty in
+          let impls = impls_type_list ty in
 	    List.fold_left
-	     (fun (env,bl) na ->
-	       (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+	     (fun (env,bl) (loc,na as locna) ->
+	       (push_name_env lvar impls env locna,
+                (na,k,None,locate_if_isevar loc na ty)::bl))
 	      (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -452,12 +454,12 @@ let iterate_binder intern lvar (env,bl) = function
       let intern_type env = intern (set_type_scope env) in
       (match bk with
       | Default k ->
-          let (loc,na) = List.hd nal in
-	  (* TODO: fail if several names with different implicit types *)
 	  let ty = intern_type env ty in
-	  let ty = locate_if_isevar loc na ty in
+          let impls = impls_type_list ty in
 	  List.fold_left
-	    (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+	    (fun (env,bl) (loc,na as locna) ->
+              (push_name_env lvar impls env locna,
+               (na,k,None,locate_if_isevar loc na ty)::bl))
 	    (env,bl) nal
       | Generalized (b,b',t) ->
 	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -731,8 +733,9 @@ let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
 
-let rec simple_adjust_scopes n = function
-  | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+let rec simple_adjust_scopes n scopes =
+  if n=0 then [] else match scopes with
+  | [] -> None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
@@ -809,9 +812,6 @@ let message_redundant_alias (id1,id2) =
 
 (* Expanding notations *)
 
-let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern.")
-
 let chop_aconstr_constructor loc (ind,k) args =
   if List.length args = 0 then (* Tolerance for a @id notation *) args else
     begin
@@ -1293,7 +1293,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
                 find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
-	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
+          intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
@@ -1417,13 +1417,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
     (tm',(snd na,typ)), na::ids
 
   and iterate_prod loc2 env bk ty body nal =
-    let rec default env bk = function
-    | (loc1,na as locna)::nal ->
-	if nal <> [] then check_capture loc1 ty na;
-	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
-	  GProd (join_loc loc1 loc2, na, bk, ty, body)
-    | [] -> intern_type env body
+    let default env bk = function
+    | (loc1,na)::nal' as nal ->
+	if nal' <> [] then check_capture loc1 ty na;
+        let ty = intern_type env ty in
+        let impls = impls_type_list ty in
+	let env = List.fold_left (push_name_env lvar impls) env nal in
+        List.fold_right (fun (loc,na) c ->
+          GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+          nal (intern_type env body)
+    | [] -> assert false
     in
       match bk with
 	| Default b -> default env b nal
@@ -1433,13 +1436,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	      it_mkGProd ibind body
 
   and iterate_lam loc2 env bk ty body nal =
-    let rec default env bk = function
-      | (loc1,na as locna)::nal ->
-	  if nal <> [] then check_capture loc1 ty na;
-	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	  let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
-	    GLambda (join_loc loc1 loc2, na, bk, ty, body)
-      | [] -> intern env body
+    let default env bk = function
+    | (loc1,na)::nal' as nal ->
+        if nal' <> [] then check_capture loc1 ty na;
+        let ty = intern_type env ty in
+        let impls = impls_type_list ty in
+	let env = List.fold_left (push_name_env lvar impls) env nal in
+        List.fold_right (fun (loc,na) c ->
+          GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+          nal (intern env body)
+    | [] -> assert false
     in match bk with
       | Default b -> default env b nal
       | Generalized (b, b', t) ->
@@ -1450,6 +1456,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
+    if !parsing_explicit then
+      if eargs <> [] then
+        error "Arguments given by name or position not supported in explicit mode."
+      else
+        intern_args env subscopes rargs
+    else
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
       match (impl,rargs) with
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index be78837f..7d000902 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -178,5 +178,8 @@ val interp_aconstr : ?impls:internalization_env ->
   (identifier * identifier) list -> constr_expr ->
   (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
 
+(** Globalization options *)
+val parsing_explicit : bool ref
+
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e564bd11..594e8fd9 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -63,23 +63,10 @@ type 'a with_ebindings = 'a * open_constr bindings
 
 type 'a generic_argument = argument_type * Obj.t
 
-let dyntab = ref ([] : string list)
-
 type rlevel
 type glevel
 type tlevel
 
-type ('a,'b) abstract_argument_type = argument_type
-
-let create_arg s =
-  if List.mem s !dyntab then
-    anomaly ("Genarg.create: already declared generic argument " ^ s);
-  dyntab := s :: !dyntab;
-  let t = ExtraArgType s in
-  (t,t,t)
-
-let exists_argtype s = List.mem s !dyntab
-
 type intro_pattern_expr =
   | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
@@ -259,3 +246,32 @@ let unquote x = x
 type an_arg_of_this_type = Obj.t
 
 let in_generic t x = (t, Obj.repr x)
+
+let dyntab = ref ([] : (string * glevel generic_argument option) list)
+
+type ('a,'b) abstract_argument_type = argument_type
+
+let create_arg v s =
+  if List.mem_assoc s !dyntab then
+    anomaly ("Genarg.create: already declared generic argument " ^ s);
+  let t = ExtraArgType s in
+  dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
+  (t,t,t)
+
+let exists_argtype s = List.mem_assoc s !dyntab
+
+let default_empty_argtype_value s = List.assoc s !dyntab
+
+let default_empty_value t =
+  let rec aux = function
+  | List0ArgType _ -> Some (in_gen t [])
+  | OptArgType _ -> Some (in_gen t None)
+  | PairArgType(t1,t2) ->
+      (match aux t1, aux t2 with
+      | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2))
+      | _ -> None)
+  | ExtraArgType s -> default_empty_argtype_value s
+  | _ -> None in
+  match aux t with
+  | Some v -> Some (out_gen t v)
+  | None -> None
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 54aadba1..01217204 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -256,7 +256,8 @@ val app_pair :
 
 (** create a new generic type of argument: force to associate
    unique ML types at each of the three levels *)
-val create_arg : string ->
+val create_arg : 'rawa option ->
+    string ->
       ('a,tlevel) abstract_argument_type
       * ('globa,glevel) abstract_argument_type
       * ('rawa,rlevel) abstract_argument_type
@@ -298,7 +299,6 @@ val in_gen :
 val out_gen :
   ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
 
-
 (** [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
    [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
@@ -312,3 +312,5 @@ type an_arg_of_this_type
 
 val in_generic :
   argument_type -> an_arg_of_this_type -> 'co generic_argument
+
+val default_empty_value : ('a,rlevel) abstract_argument_type -> 'a option
diff --git a/interp/notation.ml b/interp/notation.ml
index 8f19ab85..d2bee550 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -817,3 +817,8 @@ let _ =
     { freeze_function = freeze;
       unfreeze_function = unfreeze;
       init_function = init }
+
+let with_notation_protection f x =
+  let fs = freeze () in
+  try let a = f x in unfreeze fs; a
+  with e -> unfreeze fs; raise e
diff --git a/interp/notation.mli b/interp/notation.mli
index f92ef94e..f429e377 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -177,3 +177,5 @@ val declare_notation_printing_rule : notation -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 
 (** Rem: printing rules for primitive token are canonical *)
+
+val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b484d175..04d39fbf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -239,7 +239,7 @@ let compare_recursive_parts found f (iterator,subc) =
   | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
   | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
       (* We found a binding position where it differs *)
-      check_is_hole y t_x;
+      check_is_hole x t_x;
       check_is_hole y t_y;
       !diff = None && (diff := Some (x,y,None); aux c term)
   | _ ->
@@ -564,8 +564,11 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 (fst metas) ->
-      alp, bind_env alp sigma id2 (GVar (dummy_loc,id1))
+  | (_,Name id2) when List.mem id2 (fst metas) ->
+      let rhs = match na1 with
+      | Name id1 -> GVar (dummy_loc,id1)
+      | Anonymous -> GHole (dummy_loc,Evd.InternalHole) in
+      alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
@@ -922,6 +925,12 @@ let names_of_local_binders bl =
   List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
 
 (**********************************************************************)
+(* Miscellaneous *)
+
+let error_invalid_pattern_notation loc =
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
+
+(**********************************************************************)
 (* Functions on constr_expr *)
 
 let constr_loc = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4527dc48..79bab389 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -268,3 +268,7 @@ val ntn_loc :
   Util.loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :
   Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list
+
+(** For cases pattern parsing errors *)
+
+val error_invalid_pattern_notation : Util.loc -> 'a