diff options
author | 2012-11-17 03:09:23 +0000 | |
---|---|---|
committer | 2012-11-17 03:09:23 +0000 | |
commit | 35846ec22445e14cb044ef3beb62f5c559d94752 (patch) | |
tree | 283e8cc0a05b3f1722dadaabc900341ee63499ed | |
parent | beca7a2c11d6521bd9eec7bb0eb5d77a345f99ef (diff) |
Taking into account the type of a definition (if it exists), and the
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | interp/constrintern.ml | 47 | ||||
-rw-r--r-- | interp/constrintern.mli | 2 | ||||
-rw-r--r-- | interp/notation.ml | 6 | ||||
-rw-r--r-- | interp/notation.mli | 2 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
-rw-r--r-- | tactics/tacintern.ml | 3 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | test-suite/success/Scopes.v | 8 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 4 | ||||
-rw-r--r-- | toplevel/record.ml | 2 |
10 files changed, 54 insertions, 24 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index cb95af733..83e4c4415 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -296,6 +296,12 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} let reset_tmp_scope env = {env with tmp_scope = None} +let set_scope env = function + | CastConv (GSort _) -> set_type_scope env + | CastConv (GRef (_,ref) | GApp (_,GRef (_,ref),_)) -> + {env with tmp_scope = compute_scope_of_global ref} + | _ -> env + let rec it_mkGProd loc2 env body = match env with (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) @@ -1441,7 +1447,9 @@ let internalize sigma globalenv env allow_patvar lvar c = | CSort (loc, s) -> GSort(loc,s) | CCast (loc, c1, c2) -> - GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2) + let c2 = Miscops.map_cast_type (intern_type env) c2 in + let env' = set_scope env c2 in + GCast (loc,intern env' c1, c2) and intern_type env = intern (set_type_scope env) @@ -1599,19 +1607,23 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Idset.empty -let intern_gen isarity sigma env +let scope_of_type_kind = function + | IsType -> Some Notation.type_scope + | OfType (Some typ) -> compute_type_scope typ + | OfType None -> None + +let intern_gen kind sigma env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let tmp_scope = - if isarity then Some Notation.type_scope else None in - internalize sigma env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls = impls} - allow_patvar (ltacvars, []) c + let tmp_scope = scope_of_type_kind kind in + internalize sigma env {ids = extract_ids env; unb = false; + tmp_scope = tmp_scope; scopes = []; + impls = impls} + allow_patvar (ltacvars, []) c -let intern_constr sigma env c = intern_gen false sigma env c +let intern_constr sigma env c = intern_gen (OfType None) sigma env c -let intern_type sigma env c = intern_gen true sigma env c +let intern_type sigma env c = intern_gen IsType sigma env c let intern_pattern globalenv patt = try @@ -1629,7 +1641,7 @@ let intern_pattern globalenv patt = let interp_gen kind sigma env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in + let c = intern_gen kind ~impls ~allow_patvar ~ltacvars sigma env c in understand_gen kind sigma env c let interp_constr sigma env c = @@ -1645,7 +1657,7 @@ let interp_open_constr sigma env c = understand_tcc sigma env (intern_constr sigma env c) let interp_open_constr_patvar sigma env c = - let raw = intern_gen false sigma env c ~allow_patvar:true in + let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in let sigma = ref sigma in let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in let rec patvar_to_evar r = match r with @@ -1673,7 +1685,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) | Some evdref -> evdref in let istype = kind = IsType in - let c = intern_gen istype ~impls !evdref env c in + let c = intern_gen kind ~impls !evdref env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in understand_tcc_evars ~fail_evar evdref env kind c, imps @@ -1688,7 +1700,7 @@ let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_intern interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c = - let c = intern_gen (kind=IsType) ~impls !evdref env c in + let c = intern_gen kind ~impls !evdref env c in understand_tcc_evars evdref env kind c let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ = @@ -1700,7 +1712,8 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c = type ltac_sign = identifier list * unbound_ltac_var_map let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = - let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in + let c = intern_gen (if as_type then IsType else OfType None) + ~allow_patvar:true ~ltacvars sigma env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = @@ -1722,12 +1735,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = (* Interpret binders and contexts *) let interp_binder sigma env na t = - let t = intern_gen true sigma env t in + let t = intern_gen IsType sigma env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand_type sigma env t' let interp_binder_evars evdref env na t = - let t = intern_gen true !evdref env t in + let t = intern_gen IsType !evdref env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand_tcc_evars evdref env IsType t' diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 16a5875de..28e7e2985 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -78,7 +78,7 @@ val intern_constr : evar_map -> env -> constr_expr -> glob_constr val intern_type : evar_map -> env -> constr_expr -> glob_constr -val intern_gen : bool -> evar_map -> env -> +val intern_gen : typing_constraint -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr diff --git a/interp/notation.ml b/interp/notation.ml index 8483e18a9..58a6d0593 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -513,6 +513,12 @@ let compute_arguments_scope_full t = let compute_arguments_scope t = fst (compute_arguments_scope_full t) +let compute_type_scope t = + find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) + +let compute_scope_of_global ref = + find_scope_class_opt (Some (ScopeRef ref)) + (** When merging scope list, we give priority to the first one (computed by substitution), using the second one (user given or earlier automatic) as fallback *) diff --git a/interp/notation.mli b/interp/notation.mli index 8f960e24c..88574636f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -160,6 +160,8 @@ val declare_scope_class : scope_name -> scope_class -> unit val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list +val compute_type_scope : Term.types -> scope_name option +val compute_scope_of_global : global_reference -> scope_name option (** Building notation key *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 48ed14473..6a7a588d4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -133,7 +133,7 @@ let rec abstract_glob_constr c = function (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = - Constrintern.intern_gen false sigma env ~impls + Constrintern.intern_gen (Pretyping.OfType None) sigma env ~impls ~allow_patvar:false ~ltacvars:([],[]) c (* diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c601c623d..ad62e6015 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -347,8 +347,9 @@ let intern_binding_name ist x = let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in + let scope = if isarity then Pretyping.IsType else Pretyping.OfType None in let c' = - warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c + warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c in (c',if !strict_check then None else Some c) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3de839525..221f2c6f4 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -465,7 +465,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma intros/lettac/inversion hypothesis names *) | Some c -> let ltacdata = (List.map fst ltacvars,unbndltacvars) in - intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c + intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c in let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in let evdc = diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 997fedd38..ab40a7c48 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -13,3 +13,11 @@ Record B := { f :> Z -> Z }. Variable a:B. Arguments Scope a [Z_scope]. Check a 0. + +(* Check that casts activate scopes if ever possible *) + +Inductive U := A. +Bind Scope u with U. +Notation "'ε'" := A : u. +Definition c := ε : U. +Check ε : U diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 1a61982ea..c3ca35fe5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -313,10 +313,10 @@ let rec find_pattern nt xl = function find_pattern nt (x::xl) (l,l') | [], NonTerminal x' :: l' -> (out_nt nt,x',List.rev xl),l' - | _, Terminal s :: _ | Terminal s :: _, _ -> - error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") + | _, Terminal s :: _ | Terminal s :: _, _ -> + error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") | _, [] -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 3332558a8..85abcc01c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,7 +26,7 @@ open Constrexpr_ops (********** definition d'un record (structure) **************) let interp_evars evdref env impls k typ = - let typ' = intern_gen true ~impls !evdref env typ in + let typ' = intern_gen Pretyping.IsType ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in imps, Pretyping.understand_tcc_evars evdref env k typ' |