The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Sorry for French. Was not intended to be a reply to the list.

On Sat, Nov 17, 2012 at 04:00:41AM +0100, Hugo Herbelin wrote:
> Voici un patch qui généralise l'utilisation des scopes et qui fait
> incidemment ce que tu veux (mais les "cast" restent dans le terme
> après typage, c'est donc moins purement notationnel que les - moches -
> "%scope"). 
> 
> Hugo
> 
> Inductive U1 := A.
> Inductive U2 := B.
> Bind Scope u with U1.
> Bind Scope v with U2.
> Notation "'ε'" := (A) : u.
> Notation "'ε'" := (B) : v.
> Definition a := ε : U1.
> Check ε : U1.
> 
> On Sat, Nov 17, 2012 at 01:08:02AM +0100, AUGER Cédric wrote:
> > Hi all,
> > suppose I want to overload some notation, let us say in this context:
> > 
> > Inductive U1 := A.
> > Inductive U2 := B.
> > 
> > I want to define the notations
> > 
> > Notation "'ε'" := (A).
> > Notation "'ε'" := (B).
> > 
> > in such a way that both (ε : U1) and (ε : U2) type-checks in the same
> > context (in particular with the same opened scopes).
> > How can I do this (without using that hideous '%<scope>')?
> > 
> > I just want a way to make ': U1' open the U1_scope and ': U2' open the
> > U2_scope. I tried 'Bind Scope' but with no success. I have read the
> > manual, but it is not very clear on that part.
> > 
> > ------------------------------
> > Bind Scope u with U1.
> > Bind Scope v with U2.
> > 
> > Notation "'ε'" := (A) : u.
> > Notation "'ε'" := (B) : v.
> > 
> > Open Scope u.
> > Open Scope v.
> > 
> > Delimit Scope u with u_.
> > Delimit Scope v with v_.
> > 
> > Bind Scope u_ with U1.
> > Bind Scope v_ with U2.
> > 
> > Check (ε : U1).

> diff --git a/trunk/interp/constrintern.ml b/trunk/interp/constrintern.ml
> index cb95af7..83e4c44 100644
> --- a/trunk/interp/constrintern.ml
> +++ b/trunk/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/trunk/interp/constrintern.mli b/trunk/interp/constrintern.mli
> index 16a5875..28e7e29 100644
> --- a/trunk/interp/constrintern.mli
> +++ b/trunk/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/trunk/interp/notation.ml b/trunk/interp/notation.ml
> index 8483e18..58a6d05 100644
> --- a/trunk/interp/notation.ml
> +++ b/trunk/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/trunk/interp/notation.mli b/trunk/interp/notation.mli
> index 8f960e2..8857463 100644
> --- a/trunk/interp/notation.mli
> +++ b/trunk/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/trunk/plugins/funind/indfun.ml b/trunk/plugins/funind/indfun.ml
> index 48ed144..6a7a588 100644
> --- a/trunk/plugins/funind/indfun.ml
> +++ b/trunk/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/trunk/tactics/tacintern.ml b/trunk/tactics/tacintern.ml
> index c601c62..ad62e60 100644
> --- a/trunk/tactics/tacintern.ml
> +++ b/trunk/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/trunk/tactics/tacinterp.ml b/trunk/tactics/tacinterp.ml
> index 3de8395..221f2c6 100644
> --- a/trunk/tactics/tacinterp.ml
> +++ b/trunk/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/trunk/toplevel/metasyntax.ml b/trunk/toplevel/metasyntax.ml
> index 1a61982..c3ca35f 100644
> --- a/trunk/toplevel/metasyntax.ml
> +++ b/trunk/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/trunk/toplevel/record.ml b/trunk/toplevel/record.ml
> index 3332558..85abcc0 100644
> --- a/trunk/toplevel/record.ml
> +++ b/trunk/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'
>