Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Code cleanup in notations: use records instead of tuples for entries and subentries #17823

Merged
merged 2 commits into from
Jul 8, 2023
Merged

Code cleanup in notations: use records instead of tuples for entries and subentries #17823

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
99ed573
A notation cleanup suggested in #17117: using records in place of tup…
herbelin Jul 6, 2023
17aeb36
Add overlay
proux01 Jul 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions dev/ci/user-overlays/17823-herbelin-record-notation.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
overlay elpi https://github.com/proux01/coq-elpi coq_17823 17823
11 changes: 9 additions & 2 deletions interp/constrexpr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,17 @@ type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | Le
type notation_entry = InConstrEntry | InCustomEntry of string

(* A notation entry with the level where the notation lives *)
type notation_entry_level = notation_entry * entry_level
type notation_entry_level = {
notation_entry : notation_entry;
notation_level : entry_level;
}
Copy link
Member

@ejgallego ejgallego Jul 6, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@herbelin if you have the energy, the form:

module Entry_level = struct
  type t = { entry : notation_entry;
           ; level : entry_level
           }
end

tends to work better.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't buy the "; ..." formatting which moreover is not the most "standard" way to format records in the code of Coq.

Otherwise, what are the pros and cons of using a module? And how do you measure the "better"?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using a module only makes sense if you have functions directly related to it together. If it is just a one off type its probably not worth it.


(* Notation subentries, to be associated to the variables of the notation *)
type notation_entry_relative_level = notation_entry * (entry_relative_level * side option)
type notation_entry_relative_level = {
notation_subentry : notation_entry;
notation_relative_level : entry_relative_level;
notation_position : side option;
}

type notation_key = string

Expand Down
42 changes: 22 additions & 20 deletions interp/constrextern.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,9 +219,11 @@ let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
| a :: args, [] ->
(a, (entry, ([], scopes))) :: fill_arg_scopes args [] all

let update_with_subscope ((entry,(lev,side)),(scopt,scl)) scopes =
let update_with_subscope (entry,(scopt,scl)) scopes =
let {notation_subentry = entry; notation_relative_level = lev; notation_position = side} = entry in
let lev = if !print_parentheses && side <> None then LevelLe 0 (* min level *) else lev in
((entry,(lev,side)),(scopt,scl@scopes))
let subentry' = {notation_subentry = entry; notation_relative_level = lev; notation_position = side} in
(subentry',(scopt,scl@scopes))

(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
Expand Down Expand Up @@ -334,12 +336,12 @@ let extern_record_pattern cstrsp args =
with
Not_found | No_match | Exit -> None

(* Better to use extern_glob_constr composed with injection/retraction ?? *)
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
match availability_of_entry_coercion custom (InConstrEntry,0) with
match availability_of_entry_coercion custom constr_lowest_level with
| None -> raise No_match
| Some coercion ->
let loc = cases_pattern_loc pat in
Expand All @@ -356,10 +358,10 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
| PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
| pat ->
match availability_of_entry_coercion custom (InConstrEntry,0) with
match availability_of_entry_coercion custom constr_lowest_level with
| None -> raise No_match
| Some coercion ->
let allscopes = ((InConstrEntry,(LevelSome,None)),scopes) in
let allscopes = (constr_some_level,scopes) in
let pat = match pat with
| PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
| PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
Expand Down Expand Up @@ -389,7 +391,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
match rule with
| NotationRule (_,ntn as specific_ntn) ->
begin
let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
let entry = fst (Notation.level_of_notation ntn) in
match availability_of_entry_coercion custom entry with
| None -> raise No_match
| Some coercion ->
Expand Down Expand Up @@ -425,7 +427,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
(make_pat_notation ?loc specific_ntn (l,ll) l2') key)
end
| AbbrevRule kn ->
match availability_of_entry_coercion custom (InConstrEntry, 0) with
match availability_of_entry_coercion custom constr_lowest_level with
| None -> raise No_match
| Some coercion ->
let qid = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
Expand Down Expand Up @@ -493,7 +495,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
|None -> CAst.make @@ CPatCstr (c, Some args, [])

let extern_cases_pattern vars p =
extern_cases_pattern_in_scope ((InConstrEntry,(LevelSome (*??*),None)),([],[])) vars p
extern_cases_pattern_in_scope (constr_some_level,([],[])) vars p

(**********************************************************************)
(* Externalising applications *)
Expand Down Expand Up @@ -749,7 +751,7 @@ let same_binder_type ty nal c =
let extern_possible_prim_token (custom,scopes) r =
if !print_raw_literal then raise No_match;
let (n,key) = uninterp_prim_token r scopes in
match availability_of_entry_coercion custom (InConstrEntry,0) with
match availability_of_entry_coercion custom constr_lowest_level with
| None -> raise No_match
| Some coercion ->
insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
Expand Down Expand Up @@ -889,11 +891,11 @@ let rec extern inctx ?impargs scopes vars r =

| c ->

match availability_of_entry_coercion (fst scopes) (InConstrEntry,0) with
match availability_of_entry_coercion (fst scopes) constr_lowest_level with
| None -> raise No_match
| Some coercion ->

let scopes = ((InConstrEntry,(LevelSome (*??*),None)), snd scopes) in
let scopes = (constr_some_level, snd scopes) in
let c = match c with

(* The remaining cases are only for the constr entry *)
Expand Down Expand Up @@ -1222,7 +1224,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
(* Try availability of interpretation ... *)
match keyrule with
| NotationRule (_,ntn as specific_ntn) ->
let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
let entry = fst (Notation.level_of_notation ntn) in
(match availability_of_entry_coercion custom entry with
| None -> raise No_match
| Some coercion ->
Expand Down Expand Up @@ -1275,7 +1277,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
let args = extern_args (extern true) (vars,uvars) args in
let c = CAst.make ?loc @@ extern_applied_abbreviation inctx nallargs argsimpls (a,cf) l args in
if isCRef_no_univ c.CAst.v && entry_has_global custom then c
else match availability_of_entry_coercion custom (InConstrEntry,0) with
else match availability_of_entry_coercion custom constr_lowest_level with
| None -> raise No_match
| Some coercion -> insert_entry_coercion coercion c
with
Expand All @@ -1294,10 +1296,10 @@ and extern_applied_proj inctx scopes vars (cst,us) params c extraargs =
extern_projection inctx (f,us) nparams args imps

let extern_glob_constr vars c =
extern false ((InConstrEntry,(LevelSome,None)),([],[])) vars c
extern false (constr_some_level,([],[])) vars c

let extern_glob_type ?impargs vars c =
extern_typ ?impargs ((InConstrEntry,(LevelSome,None)),([],[])) vars c
extern_typ ?impargs (constr_some_level,([],[])) vars c

(******************************************************************)
(* Main translation function from constr -> constr_expr *)
Expand All @@ -1306,7 +1308,7 @@ let extern_constr ?(inctx=false) ?scope env sigma t =
let r = Detyping.detype Detyping.Later Id.Set.empty env sigma t in
let vars = extern_env env sigma in
let scope = Option.cata (fun x -> [x]) [] scope in
extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
extern inctx (constr_some_level,(scope,[])) vars r

let extern_constr_in_scope ?inctx scope env sigma t =
extern_constr ?inctx ~scope env sigma t
Expand All @@ -1332,7 +1334,7 @@ let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma
in
let vars = extern_env env sigma in
let scope = Option.cata (fun x -> [x]) [] scope in
extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
extern inctx (constr_some_level,(scope,[])) vars r

(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
Expand Down Expand Up @@ -1474,7 +1476,7 @@ and glob_of_pat_under_context avoid env sigma (nas, pat) =
(Array.rev_of_list nas, pat)

let extern_constr_pattern env sigma pat =
extern true ((InConstrEntry,(LevelSome,None)),([],[]))
extern true (constr_some_level,([],[]))
(* XXX no vars? *)
(Id.Set.empty, Evd.universe_binders sigma)
(glob_of_pat Id.Set.empty env sigma pat)
Expand All @@ -1483,4 +1485,4 @@ let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
let vars = extern_env env sigma in
let a = List.map (extended_glob_local_binder_of_decl) a in
pi3 (extern_local_binder ((InConstrEntry,(LevelSome,None)),([],[])) vars a)
pi3 (extern_local_binder (constr_some_level,([],[])) vars a)
42 changes: 26 additions & 16 deletions interp/notation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1543,21 +1543,27 @@ let sublevel_ord lev lev' =
| LevelLt n, LevelLe n' -> n < n'
| LevelLe n, LevelLt n' -> n <= n'-1

let is_coercion (e1,n1) (e2,(n2,_)) =
let is_coercion
{ notation_entry = e1; notation_level = n1 }
{ notation_subentry = e2; notation_relative_level = n2 } =
not (notation_entry_eq e1 e2) ||
match n2 with
| LevelLt n2 | LevelLe n2 -> n1 < n2
| LevelSome -> true (* unless n2 is the entry top level but we shall know it only dynamically *)

let included (e1,n1) (e2,(n2,_)) =
let included
{ notation_entry = e1; notation_level = n1 }
{ notation_subentry = e2; notation_relative_level = n2 } =
notation_entry_eq e1 e2 && entry_relative_level_le n1 n2

let rec search nfrom nto = function
| [] -> raise Not_found
| ((pfrom,pto),coe)::l ->
if entry_relative_level_le pfrom nfrom && entry_relative_level_le nto pto then coe else search nfrom nto l

let availability_of_entry_coercion (entry,(sublev,_) as entry_sublev) (entry',lev' as entry_lev) =
let availability_of_entry_coercion
({ notation_subentry = entry; notation_relative_level = sublev } as entry_sublev)
({ notation_entry = entry'; notation_level = lev' } as entry_lev) =
if included entry_lev entry_sublev then
(* [entry] is by default included in [relative_entry] *)
Some []
Expand All @@ -1578,21 +1584,23 @@ let rec insert_coercion_path path = function
else path'::insert_coercion_path path paths

let declare_entry_coercion ntn entry_level entry_relative_level' =
let entry, lev = entry_level in
let entry', (sublev',_) = entry_relative_level' in
let { notation_entry = entry; notation_level = lev } = entry_level in
let { notation_subentry = entry'; notation_relative_level = sublev' } = entry_relative_level' in
(* Transitive closure *)
let toaddleft =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',sublev'''),path) l ->
if included entry_level (entry''',(sublev''',None)) &&
not (included (entry'',lev'') entry_relative_level')
if included entry_level
{ notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None } &&
not (included { notation_entry = entry''; notation_level = lev'' } entry_relative_level')
then ((entry'',entry'),((lev'',sublev'),path@[ntn]))::l else l) paths l)
!entry_coercion_map [] in
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',sublev'''),path) l ->
if included (entry'',lev'') entry_relative_level' &&
not (included entry_level (entry''',(sublev''',None)))
if included { notation_entry = entry''; notation_level = lev'' } entry_relative_level' &&
not (included entry_level
{ notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None })
then ((entry,entry'''),((lev,sublev'''),path@[ntn]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
Expand All @@ -1615,9 +1623,10 @@ let declare_custom_entry_has_global s n =
with Not_found ->
entry_has_global_map := String.Map.add s n !entry_has_global_map

let entry_has_global = function
| InConstrEntry, _ -> true
| InCustomEntry s, (n,_) ->
let entry_has_global { notation_subentry = entry; notation_relative_level = n } =
match entry with
| InConstrEntry -> true
| InCustomEntry s ->
try entry_relative_level_le (String.Map.find s !entry_has_global_map) n with Not_found -> false

let entry_has_ident_map = ref String.Map.empty
Expand All @@ -1630,9 +1639,10 @@ let declare_custom_entry_has_ident s n =
with Not_found ->
entry_has_ident_map := String.Map.add s n !entry_has_ident_map

let entry_has_ident = function
| InConstrEntry, _ -> true
| InCustomEntry s, (n,_) ->
let entry_has_ident { notation_subentry = entry; notation_relative_level = n } =
match entry with
| InConstrEntry -> true
| InCustomEntry s ->
try entry_relative_level_le (String.Map.find s !entry_has_ident_map) n with Not_found -> false

type entry_coercion_kind =
Expand Down Expand Up @@ -2002,7 +2012,7 @@ let is_numeral_in_constr (entry,symbs) =
let level_of_notation ntn =
if is_numeral_in_constr (decompose_notation_key ntn) then
(* A primitive notation *)
(fst ntn, 0, []) (* TODO: string notations*)
({ notation_entry = fst ntn; notation_level = 0}, []) (* TODO: string notations*)
else
NotationMap.find ntn !notation_level_map

Expand Down
16 changes: 11 additions & 5 deletions interp/notation_ops.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,14 @@ open Glob_ops
open Mod_subst
open Notation_term

(** Constr default entry *)

let constr_lowest_level =
Constrexpr.{notation_entry = InConstrEntry; notation_level = 0}

let constr_some_level =
Constrexpr.{notation_subentry = InConstrEntry; notation_relative_level = LevelSome; notation_position = None}

(**********************************************************************)
(* Utilities *)

Expand Down Expand Up @@ -1309,11 +1317,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
(terms,termlists,binders,Id.List.remove_assoc x binderlists)

let default_constr_entry_relative_level = Constrexpr.(InConstrEntry,(LevelSome,None))

let add_ldots_var metas = (ldots_var,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas
let add_ldots_var metas = (ldots_var,((constr_some_level,([],[])),NtnTypeConstr))::metas

let add_meta_bindinglist x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas
let add_meta_bindinglist x metas = (x,((constr_some_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas

(* This tells if letins in the middle of binders should be included in
the sequence of binders *)
Expand Down Expand Up @@ -1359,7 +1365,7 @@ let match_binderlist match_iter_fun match_termin_fun alp metas sigma rest x y it
let alp,sigma = bind_bindinglist_env alp sigma x bl in
match_termin_fun alp metas sigma rest termin

let add_meta_term x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
let add_meta_term x metas = (x,((constr_some_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)

let match_termlist match_fun alp metas sigma rest x y iter termin revert =
let rec aux alp sigma acc rest =
Expand Down
8 changes: 8 additions & 0 deletions interp/notation_ops.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,14 @@ open Names
open Notation_term
open Glob_term

(** Constr default entries *)

(* Equivalent to an entry "in constr at level 0"; used for coercion to constr *)
val constr_lowest_level : Constrexpr.notation_entry_level

(* Equivalent to "x constr" in a subentry, at highest level *)
val constr_some_level : Constrexpr.notation_entry_relative_level

(** {5 Utilities about [notation_constr]} *)

val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
Expand Down
15 changes: 9 additions & 6 deletions interp/notationextern.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,14 @@ let notation_entry_eq s1 s2 = match (s1,s2) with
| InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2
| (InConstrEntry | InCustomEntry _), _ -> false

let notation_entry_level_eq (e1,n1) (e2,n2) =
let notation_entry_level_eq
{ notation_entry = e1; notation_level = n1 }
{ notation_entry = e2; notation_level = n2 } =
notation_entry_eq e1 e2 && Int.equal n1 n2

let notation_entry_relative_level_eq (e1,(n1,s1)) (e2,(n2,s2)) =
let notation_entry_relative_level_eq
{ notation_subentry = e1; notation_relative_level = n1; notation_position = s1 }
{ notation_subentry = e2; notation_relative_level = n2; notation_position = s2 } =
notation_entry_eq e1 e2 && entry_relative_level_eq n1 n2 && s1 = s2

let notation_eq (from1,ntn1) (from2,ntn2) =
Expand Down Expand Up @@ -77,13 +81,12 @@ let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) =
List.equal var_attributes_eq vars1 vars2 &&
Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2

type level = notation_entry * entry_level * entry_relative_level list
(* first argument is InCustomEntry s for custom entries *)
type level = notation_entry_level * entry_relative_level list

let level_eq (s1, l1, t1) (s2, l2, t2) =
let level_eq ({ notation_entry = s1; notation_level = l1}, t1) ({ notation_entry = s2; notation_level = l2}, t2) =
notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2

(* Uninterpretation tables *)
(** Uninterpretation tables *)

type 'a interp_rule_gen =
| NotationRule of Constrexpr.specific_notation
Expand Down
4 changes: 2 additions & 2 deletions interp/notationextern.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ val interpretation_eq : interpretation -> interpretation -> bool
val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
(** Equality on [notation_entry_level]. *)

type level = notation_entry * entry_level * entry_relative_level list
(* first argument is InCustomEntry s for custom entries *)
type level = notation_entry_level * entry_relative_level list
(** The "signature" of a rule: its level together with the levels of its subentries *)

val level_eq : level -> level -> bool
(** Equality on [level]. *)
Expand Down