diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 20 | ||||
| -rw-r--r-- | interp/notation.ml | 41 | ||||
| -rw-r--r-- | interp/notation.mli | 6 |
3 files changed, 45 insertions, 22 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 25f2526f74..faff0d71e0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -388,7 +388,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern allscopes vars pat - (uninterp_cases_pattern_notations pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> let loc = pat.CAst.loc in match DAst.get pat with @@ -530,7 +530,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern allscopes vars ind args - (uninterp_ind_pattern_notations ind) + (uninterp_ind_pattern_notations scopes ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in @@ -760,32 +760,32 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx scopes vars r = +let rec extern inctx (custom,scopes as allscopes) vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + extern_optimal (extern_possible_prim_token allscopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal - (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation allscopes vars r (uninterp_notations scopes r)) r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with - | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) + | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id) | c -> - match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - let scopes = (InConstrEntrySomeLevel, snd scopes) in + let scopes = (InConstrEntrySomeLevel, scopes) in let c = match c with (* The remaining cases are only for the constr entry *) @@ -797,7 +797,7 @@ let rec extern inctx scopes vars r = | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> - extern_evar n (List.map (on_snd (extern false scopes vars)) l) + extern_evar n (List.map (on_snd (extern false allscopes vars)) l) | GPatVar kind -> if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else diff --git a/interp/notation.ml b/interp/notation.ml index db8ee5bc18..49403c6e34 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -982,15 +982,38 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) - -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table - -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let sort_notations scopes l = + let extract_scope l = function + | Scope sc -> List.partitioni (fun _i x -> + match x with + | NotationRule (Some sc',_),_,_ -> String.equal sc sc' + | _ -> false) l + | SingleNotation ntn -> List.partitioni (fun _i x -> + match x with + | NotationRule (None,ntn'),_,_ -> notation_eq ntn ntn' + | _ -> false) l in + let rec aux l scopes = + if l == [] then [] (* shortcut *) else + match scopes with + | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes + | [] -> l in + aux l scopes + +let uninterp_notations scopes c = + let scopes = make_current_scopes scopes in + let keys = glob_constr_keys c in + let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in + sort_notations scopes maps + +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_scopes scopes in + let maps = keymap_find (cases_pattern_key c) !notations_key_table in + sort_notations scopes maps + +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_scopes scopes in + let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in + sort_notations scopes maps let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..40b7f2c2c9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -214,9 +214,9 @@ val interp_notation : ?loc:Loc.t -> notation -> subscopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first |