aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml3
-rw-r--r--interp/constrextern.ml16
-rw-r--r--interp/constrintern.ml66
-rw-r--r--interp/constrintern.mli5
-rw-r--r--interp/notation.ml180
-rw-r--r--interp/notation.mli6
-rw-r--r--interp/notation_ops.ml399
-rw-r--r--interp/notation_ops.mli14
-rw-r--r--interp/reserve.ml2
9 files changed, 490 insertions, 201 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 235310660b..977cbbccf2 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -15,8 +15,11 @@ open Libnames
(** [constr_expr] is the abstract syntax tree produced by the parser *)
type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+type cumul_univ_decl_expr =
+ ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl
type ident_decl = lident * universe_decl_expr option
+type cumul_ident_decl = lident * cumul_univ_decl_expr option
type name_decl = lname * universe_decl_expr option
type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d1bec16a3f..8d3cf7274a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,7 +85,7 @@ let is_reserved_type na t =
| Name id ->
try
let pat = Reserve.find_reserved_type id in
- let _ = match_notation_constr false t ([],pat) in
+ let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([],pat) in
true
with Not_found | No_match -> false
@@ -1273,7 +1273,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
| AppBoundedNotation _ -> raise No_match in
(* Try matching ... *)
let terms,termlists,binders,binderlists =
- match_notation_constr !print_universes t pat in
+ match_notation_constr ~print_univ:(!print_universes) t ~vars pat in
(* Try availability of interpretation ... *)
match keyrule with
| NotationRule (_,ntn as specific_ntn) ->
@@ -1293,20 +1293,20 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
| Some (scopt,key) ->
let scopes' = Option.List.cons scopt (snd scopes) in
let l =
- List.map (fun (c,(subentry,(scopt,scl))) ->
+ List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
extern (* assuming no overloading: *) true
(subentry,(scopt,scl@scopes')) vars c)
terms in
let ll =
- List.map (fun (c,(subentry,(scopt,scl))) ->
- List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
+ List.map (fun ((vars,l),(subentry,(scopt,scl))) ->
+ List.map (extern true (subentry,(scopt,scl@scopes')) vars) l)
termlists in
let bl =
- List.map (fun (bl,(subentry,(scopt,scl))) ->
+ List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
binders in
let bll =
- List.map (fun (bl,(subentry,(scopt,scl))) ->
+ List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
let c = make_notation loc specific_ntn (l,ll,bl,bll) in
@@ -1316,7 +1316,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args)
| SynDefRule kn ->
let l =
- List.map (fun (c,(subentry,(scopt,scl))) ->
+ List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
extern true (subentry,(scopt,scl@snd scopes)) vars c)
terms in
let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 06cf19b4f7..c7ed066f7e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -534,15 +534,19 @@ let intern_generalized_binder intern_type ntnvars
in
let na = match na with
| Anonymous ->
- let name =
- let id =
- match ty with
- | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
- qualid_basename qid
- | _ -> default_non_dependent_ident
- in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
- in Name name
- | _ -> na in
+ let id =
+ match ty with
+ | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+ qualid_basename qid
+ | _ -> default_non_dependent_ident
+ in
+ let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in
+ let id =
+ Implicit_quantifiers.make_fresh ids' (Global.env ()) id
+ in
+ Name id
+ | _ -> na
+ in
let impls = impls_type_list 1 ty' in
(push_name_env ntnvars impls env' (make ?loc na),
(make ?loc (na,b',ty')) :: List.rev bl)
@@ -1972,9 +1976,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let env = restart_lambda_binders env in
let idl_temp = Array.map
(fun (id,recarg,bl,ty,_) ->
- let recarg = Option.map (function { CAst.v = v } -> match v with
+ let recarg = Option.map (function { CAst.v = v; loc } -> match v with
| CStructRec i -> i
- | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+ | _ -> user_err ?loc Pp.(str "Well-founded induction requires Program Fixpoint or Function.")) recarg
in
let before, after = split_at_annot bl recarg in
let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
@@ -2092,9 +2096,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ntnargs in
find_appl_head_data c, args
- | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in
- apply_impargs c env impargs args_scopes
- args loc
+ | _ ->
+ assert (Option.is_empty isproj);
+ let f = intern_no_implicit env f in
+ let f, _, args_scopes = find_appl_head_data f in
+ (f,[],args_scopes), args
+ in
+ apply_impargs c env impargs args_scopes args loc
| CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -2405,8 +2413,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
and intern_args env subscopes = function
| [] -> []
| a::args ->
- let (enva,subscopes) = apply_scope_env env subscopes in
- (intern_no_implicit enva a) :: (intern_args env subscopes args)
+ let (enva,subscopes) = apply_scope_env env subscopes in
+ let a = intern_no_implicit enva a in
+ a :: (intern_args env subscopes args)
in
intern env c
@@ -2644,13 +2653,34 @@ let interp_univ_decl env decl =
let binders : lident list = decl.univdecl_instance in
let evd = Evd.from_env ~binders env in
let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
- let decl = { univdecl_instance = binders;
+ let decl = {
+ univdecl_instance = binders;
univdecl_extensible_instance = decl.univdecl_extensible_instance;
univdecl_constraints = cstrs;
- univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+ }
in evd, decl
+let interp_cumul_univ_decl env decl =
+ let open UState in
+ let binders = List.map fst decl.univdecl_instance in
+ let variances = Array.map_of_list snd decl.univdecl_instance in
+ let evd = Evd.from_ctx (UState.from_env ~binders env) in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = {
+ univdecl_instance = binders;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+ }
+ in
+ evd, decl, variances
+
let interp_univ_decl_opt env l =
match l with
| None -> Evd.from_env env, UState.default_univ_decl
| Some decl -> interp_univ_decl env decl
+
+let interp_cumul_univ_decl_opt env = function
+ | None -> Evd.from_env env, UState.default_univ_decl, [| |]
+ | Some decl -> interp_cumul_univ_decl env decl
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 9037ed5414..0de6c3e89d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -204,3 +204,8 @@ val interp_univ_decl : Environ.env -> universe_decl_expr ->
val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
Evd.evar_map * UState.universe_decl
+
+val interp_cumul_univ_decl_opt : Environ.env -> cumul_univ_decl_expr option ->
+ Evd.evar_map * UState.universe_decl * Entries.variance_entry
+(** BEWARE the variance entry needs to be adjusted by
+ [ComInductive.variance_of_entry] if the instance is extensible. *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 8d05fab63c..286ece6cb6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -345,11 +345,23 @@ let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) =
(* No need in principle to compare also_cases as it is inferred *)
also_cases1 = also_cases2 && notation_rule_eq rule1 rule2
+let adjust_application c1 c2 =
+ match c1, c2 with
+ | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 ->
+ NApp (t1, List.firstn (List.length a2) a1)
+ | NApp (t1, a1), _ ->
+ t1
+ | _ -> c1
+
+let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) =
+ let c1 = adjust_application c1 c2 in
+ Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2
+
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
- (* In case of re-import, no need to keep the previous copy *)
- let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in
- KeyMap.add key (interp :: old) map
+ (* strictly finer interpretation are kept in front *)
+ let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in
+ KeyMap.add key (strictly_finer @ interp :: rest) map
let keymap_remove key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
@@ -391,6 +403,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NBinderList (_,_,NApp (NRef ref,args),_,_) ->
RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
| NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+ | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+ RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
+ | NApp (NList (_,_,NApp (_,args),_,_), args') ->
+ Oth, AppBoundedNotation (List.length args + List.length args')
| NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
| NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
| _ -> Oth, NotAppNotation
@@ -1415,12 +1431,12 @@ let check_parsing_override (scopt,ntn) data = function
| OnlyParsingData (_,old_data) ->
let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
warn_override_if_needed (scopt,ntn) overridden data old_data;
- None, not overridden
+ None
| ParsingAndPrintingData (_,on_printing,old_data) ->
let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
warn_override_if_needed (scopt,ntn) overridden data old_data;
- (if on_printing then Some old_data.not_interp else None), not overridden
- | NoParsingData -> None, false
+ if on_printing then Some old_data.not_interp else None
+ | NoParsingData -> None
let check_printing_override (scopt,ntn) data parsingdata printingdata =
let parsing_update = match parsingdata with
@@ -1449,15 +1465,15 @@ let update_notation_data (scopt,ntn) use data table =
try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
match use with
| OnlyParsing ->
- let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
- NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+ let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update
| ParsingAndPrinting ->
- let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
- NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+ let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update
| OnlyPrinting ->
let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
let printingdata = if exists then printingdata else (true,data) :: printingdata in
- NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+ NotationMap.add ntn (parsingdata, printingdata) table, None
let rec find_interpretation ntn find = function
| [] -> raise Not_found
@@ -1730,23 +1746,22 @@ let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecat
not_location = df;
not_deprecation = deprecation;
} in
- let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
- if not exists then
- let sc = { sc with notations = notation_update } in
- scope_map := String.Map.add scope sc !scope_map;
+ let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
+ let sc = { sc with notations = notation_update } in
+ scope_map := String.Map.add scope sc !scope_map;
(* Update the uninterpretation cache *)
begin match printing_update with
| Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
| None -> ()
end;
- if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
+ if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
(* Register visibility of lonely notations *)
- if not exists then begin match scopt with
+ begin match scopt with
| LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
| NotationInScope _ -> ()
end;
(* Declare a possible coercion *)
- if not exists then begin match coe with
+ begin match coe with
| Some (IsEntryCoercion entry) ->
let (_,level,_) = level_of_notation ntn in
let level = match fst ntn with
@@ -2035,12 +2050,12 @@ type symbol =
| Break of int
let rec symbol_eq s1 s2 = match s1, s2 with
-| Terminal s1, Terminal s2 -> String.equal s1 s2
-| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
-| SProdList (id1, l1), SProdList (id2, l2) ->
- Id.equal id1 id2 && List.equal symbol_eq l1 l2
-| Break i1, Break i2 -> Int.equal i1 i2
-| _ -> false
+ | Terminal s1, Terminal s2 -> String.equal s1 s2
+ | NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
+ | SProdList (id1, l1), SProdList (id2, l2) ->
+ Id.equal id1 id2 && List.equal symbol_eq l1 l2
+ | Break i1, Break i2 -> Int.equal i1 i2
+ | _ -> false
let rec string_of_symbol = function
| NonTerminal _ -> ["_"]
@@ -2202,23 +2217,114 @@ let rec raw_analyze_notation_tokens = function
| WhiteSpace n :: sl ->
Break n :: raw_analyze_notation_tokens sl
-let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn)
-
-let possible_notations ntn =
+let rec raw_analyze_anonymous_notation_tokens = function
+ | [] -> []
+ | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_anonymous_notation_tokens sl
+ | String "_" :: sl -> NonTerminal (Id.of_string "dummy") :: raw_analyze_anonymous_notation_tokens sl
+ | String s :: sl ->
+ Terminal (String.drop_simple_quotes s) :: raw_analyze_anonymous_notation_tokens sl
+ | WhiteSpace n :: sl -> raw_analyze_anonymous_notation_tokens sl
+
+(* Interpret notations with a recursive component *)
+
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let msg_expected_form_of_recursive_notation =
+ "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
+let rec find_pattern nt xl = function
+ | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
+ find_pattern nt (x::xl) (l,l')
+ | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
+ find_pattern nt (x::xl) (l,l')
+ | [], NonTerminal x' :: l' ->
+ (out_nt nt,x',List.rev xl),l'
+ | _, Break s :: _ | Break s :: _, _ ->
+ user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
+ | _, Terminal s :: _ | Terminal s :: _, _ ->
+ user_err ~hdr:"Metasyntax.find_pattern"
+ (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
+ | _, [] ->
+ user_err Pp.(str msg_expected_form_of_recursive_notation)
+ | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
+ anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
+
+let rec interp_list_parser hd = function
+ | [] -> [], List.rev hd
+ | NonTerminal id :: tl when Id.equal id Notation_ops.ldots_var ->
+ if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
+ let hd = List.rev hd in
+ let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
+ let xyl,tl'' = interp_list_parser [] tl' in
+ (* We remember each pair of variable denoting a recursive part to *)
+ (* remove the second copy of it afterwards *)
+ (x,y)::xyl, SProdList (x,sl) :: tl''
+ | (Terminal _ | Break _) as s :: tl ->
+ if List.is_empty hd then
+ let yl,tl' = interp_list_parser [] tl in
+ yl, s :: tl'
+ else
+ interp_list_parser (s::hd) tl
+ | NonTerminal _ as x :: tl ->
+ let xyl,tl' = interp_list_parser [x] tl in
+ xyl, List.rev_append hd tl'
+ | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
+
+let get_notation_vars l =
+ List.map_filter (function NonTerminal id | SProdList (id,_) -> Some id | _ -> None) l
+
+let decompose_raw_notation ntn =
+ let l = split_notation_string ntn in
+ let l = raw_analyze_notation_tokens l in
+ let recvars,l = interp_list_parser [] l in
+ let vars = get_notation_vars l in
+ recvars, vars, l
+
+let interpret_notation_string ntn =
(* We collect the possible interpretations of a notation string depending on whether it is
in "x 'U' y" or "_ U _" format *)
let toks = split_notation_string ntn in
- if List.exists (function String "_" -> true | _ -> false) toks then
- (* Only "_ U _" format *)
- [ntn]
- else
- let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in
- if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
+ let toks =
+ if
+ List.exists (function String "_" -> true | _ -> false) toks ||
+ List.for_all (function String id -> Id.is_valid id | _ -> false) toks
+ then
+ (* Only "_ U _" format *)
+ raw_analyze_anonymous_notation_tokens toks
+ else
+ (* Includes the case of only a subset of tokens or an "x 'U' y"-style format *)
+ raw_analyze_notation_tokens toks
+ in
+ let _,toks = interp_list_parser [] toks in
+ let _,ntn' = make_notation_key None toks in
+ ntn'
+
+(* Tell if a non-recursive notation is an instance of a recursive one *)
+let is_approximation ntn ntn' =
+ let rec aux toks1 toks2 = match (toks1, toks2) with
+ | Terminal s1 :: toks1, Terminal s2 :: toks2 -> String.equal s1 s2 && aux toks1 toks2
+ | NonTerminal _ :: toks1, NonTerminal _ :: toks2 -> aux toks1 toks2
+ | SProdList (_,l1) :: toks1, SProdList (_, l2) :: toks2 -> aux l1 l2 && aux toks1 toks2
+ | NonTerminal _ :: toks1, SProdList (_,l2) :: toks2 -> aux' toks1 l2 l2 toks2 || aux toks1 toks2
+ | [], [] -> true
+ | (Break _ :: _, _) | (_, Break _ :: _) -> assert false
+ | (Terminal _ | NonTerminal _ | SProdList _) :: _, _ -> false
+ | [], _ -> false
+ and aux' toks1 l2 l2full toks2 = match (toks1, l2) with
+ | Terminal s1 :: toks1, Terminal s2 :: l2 when String.equal s1 s2 -> aux' toks1 l2 l2full toks2
+ | NonTerminal _ :: toks1, [] -> aux' toks1 l2full l2full toks2 || aux toks1 toks2
+ | _ -> false
+ in
+ let _,toks = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn)) in
+ let _,toks' = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn')) in
+ aux toks toks'
let browse_notation strict ntn map =
- let ntns = possible_notations ntn in
- let find (from,ntn' as fullntn') ntn =
- if String.contains ntn ' ' then String.equal ntn ntn'
+ let ntn = interpret_notation_string ntn in
+ let find (from,ntn' as fullntn') =
+ if String.contains ntn ' ' then
+ if String.string_contains ~where:ntn' ~what:".." then is_approximation ntn ntn'
+ else String.equal ntn ntn'
else
let _,toks = decompose_notation_key fullntn' in
let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
@@ -2230,7 +2336,7 @@ let browse_notation strict ntn map =
String.Map.fold
(fun scope_name sc ->
NotationMap.fold (fun ntn data l ->
- if List.exists (find ntn) ntns
+ if find ntn
then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l
else l) sc.notations)
map [] in
diff --git a/interp/notation.mli b/interp/notation.mli
index b8939ff87b..97955bf92e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -334,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool
val make_notation_key : notation_entry -> symbol list -> notation
val decompose_notation_key : notation -> notation_entry * symbol list
-(** Decompose a notation of the form "a 'U' b" *)
-val decompose_raw_notation : string -> symbol list
+(** Decompose a notation of the form "a 'U' b" together with the lists
+ of pairs of recursive variables and the list of all variables
+ binding in the notation *)
+val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list
(** Prints scopes (expects a pure aconstr printer) *)
val pr_scope_class : scope_class -> Pp.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2e3fa0aa0e..c4d2a2a496 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -24,82 +24,182 @@ open Notation_term
(**********************************************************************)
(* Utilities *)
-(* helper for NVar, NVar case in eq_notation_constr *)
-let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
-
-let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 =
-(vars1 == vars2 && t1 == t2) ||
-match t1, t2 with
-| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
-| NVar id1, NVar id2 -> (
- match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
- | Some n,Some m -> Int.equal n m
- | None ,None -> Id.equal id1 id2
- | _ -> false)
-| NApp (t1, a1), NApp (t2, a2) ->
- (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
-| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
- Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
- Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
- let eqpat (p1, t1) (p2, t2) =
- List.equal cases_pattern_eq p1 p2 &&
- (eq_notation_constr vars) t1 t2
- in
- let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
- let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in
- (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
- in
- Option.equal (eq_notation_constr vars) o1 o2 &&
- List.equal eqf r1 r2 &&
- List.equal eqpat p1 p2
-| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
- List.equal Name.equal nas1 nas2 &&
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2
-| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
- (eq_notation_constr vars) t1 t2 &&
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) u1 u2 &&
- (eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
- let eq (na1, o1, t1) (na2, o2, t2) =
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) t1 t2
- in
- Array.equal Id.equal ids1 ids2 &&
- Array.equal (List.equal eq) ts1 ts2 &&
- Array.equal (eq_notation_constr vars) us1 us2 &&
- Array.equal (eq_notation_constr vars) rs1 rs2
-| NSort s1, NSort s2 ->
- glob_sort_eq s1 s2
-| NCast (t1, c1), NCast (t2, c2) ->
- (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
-| NInt i1, NInt i2 ->
- Uint63.equal i1 i2
-| NFloat f1, NFloat f2 ->
- Float64.equal f1 f2
-| NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
- Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2
- && eq_notation_constr vars ty1 ty2
-| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
- | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false
+let ldots_var = Id.of_string ".."
+
+let rec alpha_var id1 id2 = function
+ | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
+ | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
+ | _::idl -> alpha_var id1 id2 idl
+ | [] -> Id.equal id1 id2
+
+let cast_type_iter2 f t1 t2 = match t1, t2 with
+ | CastConv t1, CastConv t2 -> f t1 t2
+ | CastVM t1, CastVM t2 -> f t1 t2
+ | CastCoerce, CastCoerce -> ()
+ | CastNative t1, CastNative t2 -> f t1 t2
+ | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit
+
+(* used to update the notation variable with the local variables used
+ in NList and NBinderList, since the iterator has its own variable *)
+let replace_var i j var = j :: List.remove Id.equal i var
+
+(* When [lt] is [true], tell if [t1] is a strict refinement of [t2]
+ (this is a partial order, so returning [false] does not mean that
+ [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the
+ same pattern as [t2] *)
+
+let compare_notation_constr lt (vars1,vars2) t1 t2 =
+ (* this is used to reason up to order of notation variables *)
+ let alphameta = ref [] in
+ (* this becomes true when at least one subterm is detected as strictly smaller *)
+ let strictly_lt = ref false in
+ (* this is the stack of inner of iter patterns for comparison with a
+ new iteration or the tail of a recursive pattern *)
+ let tail = ref [] in
+ let check_alphameta id1 id2 =
+ try if not (Id.equal (List.assoc id1 !alphameta) id2) then raise Exit
+ with Not_found ->
+ if (List.mem_assoc id1 !alphameta) then raise Exit;
+ alphameta := (id1,id2) :: !alphameta in
+ let check_eq_id (vars1,vars2) renaming id1 id2 =
+ let ismeta1 = List.mem_f Id.equal id1 vars1 in
+ let ismeta2 = List.mem_f Id.equal id2 vars2 in
+ match ismeta1, ismeta2 with
+ | true, true -> check_alphameta id1 id2
+ | false, false -> if not (alpha_var id1 id2 renaming) then raise Exit
+ | false, true ->
+ if not lt then raise Exit
+ else
+ (* a binder which is not bound in the notation can be
+ considered as strictly more precise since it prevents the
+ notation variables in its scope to be bound by this binder;
+ i.e. it is strictly more precise in the sense that it
+ covers strictly less patterns than a notation where the
+ same binder is bound in the notation; this is hawever
+ disputable *)
+ strictly_lt := true
+ | true, false -> if not lt then raise Exit in
+ let check_eq_name vars renaming na1 na2 =
+ match na1, na2 with
+ | Name id1, Name id2 -> check_eq_id vars renaming id1 id2; (id1,id2)::renaming
+ | Anonymous, Anonymous -> renaming
+ | Anonymous, Name _ when lt -> renaming
+ | _ -> raise Exit in
+ let rec aux (vars1,vars2 as vars) renaming t1 t2 = match t1, t2 with
+ | NVar id1, NVar id2 when id1 = ldots_var && id2 = ldots_var -> ()
+ | _, NVar id2 when lt && id2 = ldots_var -> tail := t1 :: !tail
+ | NVar id1, _ when lt && id1 = ldots_var -> tail := t2 :: !tail
+ | NVar id1, NVar id2 -> check_eq_id vars renaming id1 id2
+ | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> ()
+ | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> ()
+ | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true
+ | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> ()
+ | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *)
+ | _, NHole (_, _, _) when lt -> strictly_lt := true
+ | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+ | NBinderList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+ if b1 <> b2 then raise Exit;
+ let vars1 = replace_var i1 j1 vars1 in
+ let vars2 = replace_var i2 j2 vars2 in
+ check_alphameta i1 i2; aux (vars1,vars2) renaming iter1 iter2; aux vars renaming tail1 tail2;
+ | NBinderList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+ | NList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+ (* They may overlap on a unique iteration of them *)
+ let vars1 = replace_var i1 j1 vars1 in
+ let vars2 = replace_var i2 j2 vars2 in
+ aux (vars1,vars2) renaming iter1 iter2;
+ aux vars renaming tail1 tail2
+ | t1, NList (i2, j2, iter2, tail2, b2)
+ | t1, NBinderList (i2, j2, iter2, tail2, b2) when lt ->
+ (* checking if t1 is a finite iteration of the pattern *)
+ let vars2 = replace_var i2 j2 vars2 in
+ aux (vars1,vars2) renaming t1 iter2;
+ let t1 = List.hd !tail in
+ tail := List.tl !tail;
+ (* either matching a new iteration, or matching the tail *)
+ (try aux vars renaming t1 tail2 with Exit -> aux vars renaming t1 t2)
+ | NList (i1, j1, iter1, tail1, b1), t2
+ | NBinderList (i1, j1, iter1, tail1, b1), t2 when lt ->
+ (* we see the NList as a single iteration *)
+ let vars1 = replace_var i1 j1 vars1 in
+ aux (vars1,vars2) renaming iter1 t2;
+ let t2 = match !tail with
+ | t::rest -> tail := rest; t
+ | _ -> (* ".." is in a discarded fine-grained position *) raise Exit in
+ (* it had to be a single iteration of iter1 *)
+ aux vars renaming tail1 t2
+ | NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
+ | NLambda (na1, t1, u1), NLambda (na2, t2, u2)
+ | NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+ aux vars renaming t1 t2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ aux vars renaming u1 u2
+ | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
+ aux vars renaming b1 b2;
+ Option.iter2 (aux vars renaming) t1 t2;(* TODO : subtyping? *)
+ let renaming = check_eq_name vars renaming na1 na2 in
+ aux vars renaming u1 u2
+ | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
+ let check_pat (p1, t1) (p2, t2) =
+ if not (List.equal cases_pattern_eq p1 p2) then raise Exit; (* TODO: subtyping and renaming *)
+ aux vars renaming t1 t2
+ in
+ let eqf renaming (t1, (na1, o1)) (t2, (na2, o2)) =
+ aux vars renaming t1 t2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ let eq renaming (i1, n1) (i2, n2) =
+ if not (Ind.CanOrd.equal i1 i2) then raise Exit;
+ List.fold_left2 (check_eq_name vars) renaming n1 n2 in
+ Option.fold_left2 eq renaming o1 o2 in
+ let renaming = List.fold_left2 eqf renaming r1 r2 in
+ Option.iter2 (aux vars renaming) o1 o2;
+ List.iter2 check_pat p1 p2
+ | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+ aux vars renaming t1 t2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ Option.iter2 (aux vars renaming) o1 o2;
+ let renaming' = List.fold_left2 (check_eq_name vars) renaming nas1 nas2 in
+ aux vars renaming' u1 u2
+ | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+ aux vars renaming t1 t2;
+ aux vars renaming u1 u2;
+ aux vars renaming r1 r2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ Option.iter2 (aux vars renaming) o1 o2
+ | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
+ let eq renaming (na1, o1, t1) (na2, o2, t2) =
+ Option.iter2 (aux vars renaming) o1 o2;
+ aux vars renaming t1 t2;
+ check_eq_name vars renaming na1 na2
+ in
+ let renaming = Array.fold_left2 (fun r id1 id2 -> check_eq_id vars r id1 id2; (id1,id2)::r) renaming ids1 ids2 in
+ let renamings = Array.map2 (List.fold_left2 eq renaming) ts1 ts2 in
+ Array.iter3 (aux vars) renamings us1 us2;
+ Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2
+ | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> ()
+ | NCast (t1, c1), NCast (t2, c2) ->
+ aux vars renaming t1 t2;
+ cast_type_iter2 (aux vars renaming) c1 c2
+ | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
+ | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
+ | NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
+ Array.iter2 (aux vars renaming) t1 t2;
+ aux vars renaming def1 def2;
+ aux vars renaming ty1 ty2
+ | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+ | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in
+ try
+ let _ = aux (vars1,vars2) [] t1 t2 in
+ if not lt then
+ (* Check that order of notation metavariables does not matter *)
+ List.iter2 check_alphameta vars1 vars2;
+ not lt || !strictly_lt
+ with Exit | (* Option.iter2: *) Option.Heterogeneous | Invalid_argument _ -> false
+
+let eq_notation_constr vars t1 t2 = t1 == t2 || compare_notation_constr false vars t1 t2
+
+let strictly_finer_notation_constr vars t1 t2 = compare_notation_constr true vars t1 t2
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -154,8 +254,6 @@ let rec subst_glob_vars l gc = DAst.map (function
| _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *)
) gc
-let ldots_var = Id.of_string ".."
-
type 'a binder_status_fun = {
no : 'a -> 'a;
restart_prod : 'a -> 'a;
@@ -275,6 +373,12 @@ type found_variables = {
let add_id r id = r := { !r with vars = id :: (!r).vars }
let add_name r = function Anonymous -> () | Name id -> add_id r id
+let mkNApp1 (g,a) =
+ match g with
+ (* Ensure flattening of nested applicative nodes *)
+ | NApp (g,args') -> NApp (g,args'@[a])
+ | _ -> NApp (g,[a])
+
let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
@@ -443,7 +547,10 @@ let notation_constr_and_vars_of_glob_constr recvars a =
aux' c
and aux' x = DAst.with_val (function
| GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
- | GApp (g,args) -> NApp (aux g, List.map aux args)
+ | GApp (g,[]) -> NApp (aux g,[]) (* Encoding @foo *)
+ | GApp (g,args) ->
+ (* Treat applicative notes as binary nodes *)
+ let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
| GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
| GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
| GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
@@ -714,6 +821,20 @@ let abstract_return_type_context_notation_constr tml rtn =
abstract_return_type_context snd
(fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
+let rec push_pattern_binders vars pat =
+ match DAst.get pat with
+ | PatVar na -> Termops.add_vname vars na
+ | PatCstr (c, pl, na) -> List.fold_left push_pattern_binders (Termops.add_vname vars na) pl
+
+let rec push_context_binders vars = function
+ | [] -> vars
+ | b :: bl ->
+ let vars = match DAst.get b with
+ | GLocalAssum (na,_,_) -> Termops.add_vname vars na
+ | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars
+ | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in
+ push_context_binders vars bl
+
let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
with Not_found -> false
@@ -740,17 +861,11 @@ let is_bindinglist_meta id metas =
exception No_match
-let rec alpha_var id1 id2 = function
- | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
- | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
- | _::idl -> alpha_var id1 id2 idl
- | [] -> Id.equal id1 id2
-
let alpha_rename alpmetas v =
if alpmetas == [] then v
else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
-let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
+let add_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var v =
(* Check that no capture of binding variables occur *)
(* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
with an actual term "fun z => ... z ..." when "x" is not bound in the
@@ -778,19 +893,19 @@ let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
refinement *)
let v = alpha_rename alpmetas v in
(* TODO: handle the case of multiple occs in different scopes *)
- ((var,v)::terms,termlists,binders,binderlists)
+ ((var,(vars,v))::terms,termlists,binders,binderlists)
-let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl =
+let add_termlist_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var vl =
if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
let vl = List.map (alpha_rename alpmetas) vl in
- (terms,(var,vl)::termlists,binders,binderlists)
+ (terms,(var,(vars,vl))::termlists,binders,binderlists)
-let add_binding_env alp (terms,termlists,binders,binderlists) var v =
+let add_binding_env (vars,alp) (terms,termlists,binders,binderlists) var v =
(* TODO: handle the case of multiple occs in different scopes *)
- (terms,termlists,(var,v)::binders,binderlists)
+ (terms,termlists,(var,(vars,v))::binders,binderlists)
-let add_bindinglist_env (terms,termlists,binders,binderlists) x bl =
- (terms,termlists,binders,(x,bl)::binderlists)
+let add_bindinglist_env (vars,alp) (terms,termlists,binders,binderlists) var bl =
+ (terms,termlists,binders,(var,(vars,bl))::binderlists)
let rec map_cases_pattern_name_left f = DAst.map (function
| PatVar na -> PatVar (f na)
@@ -835,18 +950,19 @@ let rec pat_binder_of_term t = DAst.map (function
| _ -> raise No_match
) t
-let unify_name_upto alp na na' =
+let unify_name_upto (vars,alp) na na' =
match na, na' with
- | Anonymous, na' -> alp, na'
- | na, Anonymous -> alp, na
+ | Anonymous, na' -> (Termops.add_vname vars na',alp), na'
+ | na, Anonymous -> (Termops.add_vname vars na,alp), na
| Name id, Name id' ->
- if Id.equal id id' then alp, na'
- else (fst alp,(id,id')::snd alp), na'
+ let vars = Termops.add_vname vars na' in
+ if Id.equal id id' then (vars,alp), na'
+ else (vars,(fst alp,(id,id')::snd alp)), na'
let unify_pat_upto alp p p' =
try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match
-let unify_term alp v v' =
+let unify_term (_,alp) v v' =
match DAst.get v, DAst.get v' with
| GHole _, _ -> v'
| _, GHole _ -> v
@@ -889,13 +1005,13 @@ let rec unify_binders_upto alp bl bl' =
alp, b :: bl
| _ -> raise No_match
-let unify_id alp id na' =
+let unify_id (_,alp) id na' =
match na' with
| Anonymous -> Name (rename_var (snd alp) id)
| Name id' ->
if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match
-let unify_pat alp p p' =
+let unify_pat (_,alp) p p' =
if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
else raise No_match
@@ -921,33 +1037,37 @@ let rec unify_terms_binders alp cl bl' =
let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v =
try
(* If already bound to a term, unify with the new term *)
- let v' = Id.List.assoc var terms in
+ let vars,v' = Id.List.assoc var terms in
let v'' = unify_term alp v v' in
if v'' == v' then sigma else
let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in
- add_env alp sigma var v
+ add_env (Id.Set.union vars (fst alp),snd alp) sigma var v
with Not_found -> add_env alp sigma var v
let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl =
try
(* If already bound to a list of term, unify with the new terms *)
- let vl' = Id.List.assoc var termlists in
+ let vars,vl' = Id.List.assoc var termlists in
let vl = unify_terms alp vl vl' in
let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in
- add_termlist_env alp sigma var vl
+ add_termlist_env (Id.Set.union vars (fst alp),snd alp) sigma var vl
with Not_found -> add_termlist_env alp sigma var vl
let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id =
try
(* If already bound to a term, unify the binder and the term *)
- match DAst.get (Id.List.assoc var terms) with
+ let vars',v' = Id.List.assoc var terms in
+ match DAst.get v' with
| GVar id' | GRef (GlobRef.VarRef id',None) ->
- (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
- sigma
+ let (vars,(alpha,alpmetas)) = alp in
+ let vars = Id.Set.add id' vars in
+ let alpmetas = if not (Id.equal id id') then (id,id')::alpmetas else alpmetas in
+ (Id.Set.union vars' vars,(alpha,alpmetas)), sigma
| t ->
(* The term is a non-variable pattern *)
raise No_match
with Not_found ->
+ let alp = (Id.Set.add id (fst alp), snd alp) in
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
(* TODO: look at the consequences for alp *)
@@ -958,43 +1078,56 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma)
let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
try
(* If already bound to a binder, unify the term and the binder *)
- let patl' = Id.List.assoc var binders in
+ let vars,patl' = Id.List.assoc var binders in
let patl'' = List.map2 (unify_pat alp) [pat] patl' in
if patl' == patl'' then sigma
else
let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
- add_binding_env alp sigma var patl''
+ add_binding_env (Id.Set.union vars (fst alp),snd alp) sigma var patl''
with Not_found -> add_binding_env alp sigma var [pat]
let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat =
try
(* If already bound to a binder possibly *)
(* generating an alpha-renaming from unifying the new binder *)
- let disjpat' = Id.List.assoc var binders in
+ let vars,disjpat' = Id.List.assoc var binders in
+ (* if, maybe, there is eventually casts in patterns, the common types have *)
+ (* to exclude the spine of variable from the two locations they occur *)
+ let alp' = (Id.Set.union vars (fst alp),snd alp) in
let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+ alp, add_binding_env alp' sigma var disjpat
+ with Not_found ->
+ (* Note: all patterns of the disjunction are supposed to have the same
+ variables, thus one is enough *)
+ let alp = (push_pattern_binders (fst alp) (List.hd disjpat), snd alp) in
alp, add_binding_env alp sigma var disjpat
- with Not_found -> alp, add_binding_env alp sigma var disjpat
let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
let bl = List.rev bl in
try
(* If already bound to a list of binders possibly *)
(* generating an alpha-renaming from unifying the new binders *)
- let bl' = Id.List.assoc var binderlists in
+ let vars, bl' = Id.List.assoc var binderlists in
+ (* The shared subterm can be under two different spines of *)
+ (* variables (themselves bound in the notation) , so we take the *)
+ (* union of both locations *)
+ let alp' = (Id.Set.union vars (fst alp),snd alp) in
let alp, bl = unify_binders_upto alp bl bl' in
let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
- alp, add_bindinglist_env sigma var bl
+ alp, add_bindinglist_env alp' sigma var bl
with Not_found ->
- alp, add_bindinglist_env sigma var bl
+ let alp = (push_context_binders (fst alp) bl, snd alp) in
+ alp, add_bindinglist_env alp sigma var bl
let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl =
try
(* If already bound to a list of binders, unify the terms and binders *)
- let bl' = Id.List.assoc var binderlists in
+ let vars,bl' = Id.List.assoc var binderlists in
let bl = unify_terms_binders alp cl bl' in
+ let alp = (Id.Set.union vars (fst alp),snd alp) in
let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
- add_bindinglist_env sigma var bl
+ add_bindinglist_env alp sigma var bl
with Not_found ->
anomaly (str "There should be a binder list bindings this list of terms.")
@@ -1028,7 +1161,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
| (Anonymous,Name id2) when is_term_meta id2 metas ->
(* We let the non-binding occurrence define the rhs *)
alp, sigma
- | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma
+ | (Name id1,Name id2) ->
+ let (vars,(alp,alpmetas)) = alp in
+ (vars,((id1,id2)::alp,alpmetas)),sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
@@ -1071,9 +1206,9 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
try
let metas = add_ldots_var (add_meta_bindinglist y metas) in
let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
- let rest = Id.List.assoc ldots_var terms in
+ let _,rest = Id.List.assoc ldots_var terms in
let b =
- match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
+ match Id.List.assoc y binderlists with _,[b] -> b | _ ->assert false
in
let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
(* In case y is bound not only to a binder but also to a term *)
@@ -1102,18 +1237,20 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),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 sigma acc rest =
+ let rec aux alp sigma acc rest =
try
let metas = add_ldots_var (add_meta_term y metas) in
let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
- let rest = Id.List.assoc ldots_var terms in
- let t = Id.List.assoc y terms in
+ let _,rest = Id.List.assoc ldots_var terms in
+ let vars,t = Id.List.assoc y terms in
let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
if !print_parentheses && not (List.is_empty acc) then raise No_match;
- aux sigma (t::acc) rest
+ (* The union is overkill at the current time because each term matches *)
+ (* at worst the same binder metavariable of the same pattern *)
+ aux (Id.Set.union vars (fst alp),snd alp) sigma (t::acc) rest
with No_match when not (List.is_empty acc) ->
- acc, match_fun metas sigma rest termin in
- let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
+ alp, acc, match_fun metas sigma rest termin in
+ let alp,l,(terms,termlists,binders,binderlists as sigma) = aux alp sigma [] rest in
let l = if revert then l else List.rev l in
if is_bindinglist_meta x metas then
(* This is a recursive pattern for both bindings and terms; it is *)
@@ -1174,7 +1311,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert
(* Matching compositionally *)
- | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
+ | GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> sigma
| GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
@@ -1344,9 +1481,9 @@ and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)}
(alp,sigma) disjpatl1 disjpatl2 in
match_in u alp metas sigma rhs1 rhs2
-let match_notation_constr u c (metas,pat) =
+let match_notation_constr ~print_univ c ~vars (metas,pat) =
let terms,termlists,binders,binderlists =
- match_ false u ([],[]) metas ([],[],[],[]) c pat in
+ match_ false print_univ (vars,([],[])) metas ([],[],[],[]) c pat in
(* Turning substitution based on binding/constr distinction into a
substitution based on entry productions *)
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') ->
@@ -1356,9 +1493,9 @@ let match_notation_constr u c (metas,pat) =
((term, scl)::terms',termlists',binders',binderlists')
| NtnTypeBinder (NtnBinderParsedAsConstr _) ->
(match Id.List.assoc x binders with
- | [pat] ->
+ | vars,[pat] ->
let v = glob_constr_of_cases_pattern (Global.env()) pat in
- ((v,scl)::terms',termlists',binders',binderlists')
+ (((vars,v),scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
| NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
(terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 3cc6f82ec8..9d451a5bb9 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -16,6 +16,11 @@ open Glob_term
val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+(** Tell if [t1] is a strict refinement of [t2]
+ (this is a partial order and returning [false] does not mean that
+ [t2] is finer than [t1]) *)
+
(** Substitution of kernel names in interpretation data *)
val subst_interpretation :
@@ -63,10 +68,11 @@ exception No_match
val print_parentheses : bool ref
-val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
- ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
- ('a cases_pattern_disjunction_g * extended_subscopes) list *
- ('a extended_glob_local_binder_g list * extended_subscopes) list
+val match_notation_constr : print_univ:bool -> 'a glob_constr_g -> vars:Id.Set.t -> interpretation ->
+ ((Id.Set.t * 'a glob_constr_g) * extended_subscopes) list *
+ ((Id.Set.t * 'a glob_constr_g list) * extended_subscopes) list *
+ ((Id.Set.t * 'a cases_pattern_disjunction_g) * extended_subscopes) list *
+ ((Id.Set.t * 'a extended_glob_local_binder_g list) * extended_subscopes) list
val match_notation_constr_cases_pattern :
'a cases_pattern_g -> interpretation ->
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 1d5af3ff39..274d3655d3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -119,7 +119,7 @@ let revert_reserved_type t =
then I've introduced a bug... *)
let filter _ pat =
try
- let _ = match_notation_constr false t ([], pat) in
+ let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in
true
with No_match -> false
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:23:18 +0000