From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- interp/constrextern.ml | 50 +++++++++++++++++++++++------------ interp/constrextern.mli | 1 + interp/constrintern.ml | 70 +++++++++++++++++++++++++++++-------------------- interp/constrintern.mli | 3 +++ interp/genarg.ml | 42 ++++++++++++++++++++--------- interp/genarg.mli | 6 +++-- interp/notation.ml | 5 ++++ interp/notation.mli | 2 ++ interp/topconstr.ml | 15 ++++++++--- interp/topconstr.mli | 4 +++ 10 files changed, 134 insertions(+), 64 deletions(-) (limited to 'interp') 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 @@ -921,6 +924,12 @@ let names_of_local_assums bl = 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 *) 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 -- cgit v1.2.3