diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 16 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 20 | ||||
| -rw-r--r-- | interp/constrextern.ml | 168 | ||||
| -rw-r--r-- | interp/constrintern.ml | 18 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 104 | ||||
| -rw-r--r-- | interp/notation.mli | 15 |
7 files changed, 194 insertions, 149 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b96ef7c4e5..4bdacda529 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -19,11 +19,21 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option +type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string + +type entry_level = int +type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome + type notation_entry = InConstrEntry | InCustomEntry of string -type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level type notation_key = string + +(* A notation associated to a given parsing rule *) type notation = notation_entry_level * notation_key +(* A notation associated to a given interpretation *) +type specific_notation = notation_with_optional_scope * notation + type 'a or_by_notation_r = | AN of 'a | ByNotation of (string * string option) @@ -78,7 +88,7 @@ type cases_pattern_expr_r = (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of qualid option | CPatOr of cases_pattern_expr list - | CPatNotation of notation * cases_pattern_notation_substitution + | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) @@ -119,7 +129,7 @@ and constr_expr_r = | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type - | CNotation of notation * constr_notation_substitution + | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index b4798127f9..401853b625 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -75,7 +75,8 @@ let rec cases_pattern_expr_eq p1 p2 = Option.equal qualid_eq r1 r2 | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 - | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> + | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) -> + Option.equal notation_with_optional_scope_eq inscope1 inscope2 && notation_eq n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 @@ -160,7 +161,8 @@ let rec constr_expr_eq e1 e2 = Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 - | CNotation(n1, s1), CNotation(n2, s2) -> + | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> + Option.equal notation_with_optional_scope_eq inscope1 inscope2 && notation_eq n1 n2 && constr_notation_substitution_eq s1 s2 | CPrim i1, CPrim i2 -> @@ -271,7 +273,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with | CPatCstr (_,patl1,patl2) -> List.fold_left (cases_pattern_fold_names f) (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,(patl,patll),patl') -> + | CPatNotation (_,_,(patl,patll),patl') -> List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat @@ -320,7 +322,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bl,bll)) -> + | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in @@ -399,9 +401,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bl,bll)) -> + | CNotation (inscope,n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, + CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) | CDelimiters (s,a) -> CDelimiters (s,f e a) @@ -574,7 +576,7 @@ let mkAppPattern ?loc p lp = CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" (Pp.str "Nested applications not supported.") | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp) - | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp) + | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp) | _ -> CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern" (Pp.str "Such pattern cannot have arguments.")) @@ -591,8 +593,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v | CAppExpl ((None,r,i),args) -> CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) - | CNotation (ntn,(c,cl,[],[])) -> - CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, + | CNotation (inscope,ntn,(c,cl,[],[])) -> + CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c, List.map (List.map coerce_to_cases_pattern_expr) cl),[]) | CPrim p -> CPatPrim p diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 06232b8e1a..38dc10a9b3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes (* This suppresses printing of primitive tokens (e.g. numeral) and notations *) let print_no_symbol = ref false +(* This tells to skip types if a variable has this type by default *) +let print_use_implicit_types = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Printing";"Use";"Implicit";"Types"] + ~value:true + +(**********************************************************************) + +let hole = CAst.make @@ CHole (None, IntroAnonymous, None) + +let is_reserved_type na t = + not !Flags.raw_print && print_use_implicit_types () && + match na with + | Anonymous -> false + | Name id -> + try + let pat = Reserve.find_reserved_type id in + let _ = match_notation_constr false t ([],pat) in + true + with Not_found | No_match -> false + (**********************************************************************) (* Turning notations and scopes on and off for printing *) module IRuleSet = Set.Make(struct @@ -75,10 +97,10 @@ let inactive_notations_table = let inactive_scopes_table = Summary.ref ~name:"inactive_scopes_table" CString.Set.empty -let show_scope scopt = - match scopt with - | None -> str "" - | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc +let show_scope inscope = + match inscope with + | LastLonelyNotation -> str "" + | NotationInScope sc -> spc () ++ str "in scope" ++ spc () ++ str sc let _show_inactive_notations () = begin @@ -97,8 +119,8 @@ let _show_inactive_notations () = let _ = Feedback.msg_notice (str "Inactive notations:") in IRuleSet.iter (function - | NotationRule (scopt, ntn) -> - Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) + | NotationRule (inscope, ntn) -> + Feedback.msg_notice (pr_notation ntn ++ show_scope inscope) | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)))) !inactive_notations_table @@ -107,18 +129,19 @@ let deactivate_notation nr = | SynDefRule kn -> (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table - | NotationRule (scopt, ntn) -> - match availability_of_notation (scopt, ntn) (scopt, []) with + | NotationRule (inscope, ntn) -> + let scopt = match inscope with NotationInScope sc -> Some sc | LastLonelyNotation -> None in + match availability_of_notation (inscope, ntn) (scopt, []) with | None -> user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" - ++ (match scopt with - | None -> spc () ++ str "in the empty scope." - | Some _ -> show_scope scopt ++ str ".")) + ++ (match inscope with + | LastLonelyNotation -> spc () ++ str "in the empty scope." + | NotationInScope _ -> show_scope inscope ++ str ".")) | Some _ -> if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ str "is already inactive" ++ show_scope scopt ++ str ".") + ++ str "is already inactive" ++ show_scope inscope ++ str ".") else inactive_notations_table := IRuleSet.add nr !inactive_notations_table let reactivate_notation nr = @@ -127,9 +150,9 @@ let reactivate_notation nr = IRuleSet.remove nr !inactive_notations_table with Not_found -> match nr with - | NotationRule (scopt, ntn) -> + | NotationRule (inscope, ntn) -> Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ str "is already active" ++ show_scope scopt ++ + ++ str "is already active" ++ show_scope inscope ++ str ".") | SynDefRule kn -> let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in @@ -157,8 +180,8 @@ let reactivate_scope sc = let is_inactive_rule nr = IRuleSet.mem nr !inactive_notations_table || match nr with - | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table - | NotationRule (None, ntn) -> false + | NotationRule (NotationInScope sc, ntn) -> CString.Set.mem sc !inactive_scopes_table + | NotationRule (LastLonelyNotation, ntn) -> false | SynDefRule _ -> false (* args: notation, scope, activate/deactivate *) @@ -169,10 +192,13 @@ let toggle_scope_printing ~scope ~activate = deactivate_scope scope let toggle_notation_printing ?scope ~notation ~activate = + let inscope = match scope with + | None -> LastLonelyNotation + | Some sc -> NotationInScope sc in if activate then - reactivate_notation (NotationRule (scope, notation)) + reactivate_notation (NotationRule (inscope, notation)) else - deactivate_notation (NotationRule (scope, notation)) + deactivate_notation (NotationRule (inscope, notation)) (* This governs printing of projections using the dot notation symbols *) let print_projections = ref false @@ -254,11 +280,11 @@ let insert_pat_alias ?loc p = function let rec insert_coercion ?loc l c = match l with | [] -> c - | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[])) + | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[])) let rec insert_pat_coercion ?loc l c = match l with | [] -> c - | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) + | (inscope,ntn)::l -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,([insert_pat_coercion ?loc l c],[]),[]) (**********************************************************************) (* conversion of references *) @@ -348,19 +374,19 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl = | None -> mknot (loc,ntn,l,bl) end | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = +let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) = if not (List.is_empty termlists) || not (List.is_empty binderlists) then - CAst.make ?loc @@ CNotation (ntn,subst) + CAst.make ?loc @@ CNotation (Some inscope,ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (Some inscope,ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) destPrim terms binders -let make_pat_notation ?loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else +let make_pat_notation ?loc (inscope,ntn) (terms,termlists as subst) args = + if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (Some inscope,ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) destPatPrim terms [] @@ -450,12 +476,12 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (custom, (tmp_scope, scopes) as allscopes) vars = function - | NotationRule (sc,ntn) -> + | NotationRule (_,ntn as specific_ntn) -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) (tmp_scope,scopes) with + match availability_of_notation specific_ntn (tmp_scope,scopes) with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -479,7 +505,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in insert_pat_coercion coercion (insert_pat_delimiters ?loc - (make_pat_notation ?loc ntn (l,ll) l2') key) + (make_pat_notation ?loc specific_ntn (l,ll) l2') key) end | SynDefRule kn -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -786,17 +812,21 @@ let rec flatten_application c = match DAst.get c with end | a -> c +let same_binder_type ty nal c = + match nal, DAst.get c with + | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty' + | [], _ -> true + | _ -> assert false + (**********************************************************************) (* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = let (sc,n) = uninterp_prim_token r in - let coercion = - if entry_has_prim_token n custom then [] else - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> coercion in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> match availability_of_prim_token n sc scopes with | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) @@ -937,12 +967,10 @@ let rec extern inctx scopes vars r = extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_prod scopes (add_vname vars na) na bk t c + factorize_prod scopes vars na bk t c | GLambda (na,bk,t,c) -> - let t = extern_typ scopes vars t in - factorize_lambda inctx scopes (add_vname vars na) na bk t c + factorize_lambda inctx scopes vars na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -971,17 +999,19 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in + let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map CAst.make nal, + let inctx = inctx || typopt <> None in + CLetTuple (List.map CAst.make nal, (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> + let inctx = inctx || typopt <> None in CIf (sub_extern false scopes vars c, (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), @@ -1004,7 +1034,7 @@ let rec extern inctx scopes vars r = | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) in ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, - extern false scopes vars1 def)) idv + sub_extern true scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> @@ -1015,7 +1045,7 @@ let rec extern inctx scopes vars r = let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), - sub_extern false scopes vars1 bv.(i))) idv + sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) @@ -1041,7 +1071,10 @@ and extern_typ (subentry,(_,scopes)) = and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) -and factorize_prod scopes vars na bk aty c = +and factorize_prod scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1058,18 +1091,25 @@ and factorize_prod scopes vars na bk aty c = | _ -> CProdN ([binder],b)) | _ -> assert false) | _, _ -> - let c = extern_typ scopes vars c in - match na, c.v with + let c' = extern_typ scopes vars c in + match na, c'.v with | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + when binding_kind_eq bk bk' + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let ty = if implicit_type then ty else aty in + CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b) | _, CProdN (bl,b) -> - CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CProdN (CLocalAssum([make na],Default bk,ty)::bl,b) | _, _ -> - CProdN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CProdN ([CLocalAssum([make na],Default bk,ty)],c') -and factorize_lambda inctx scopes vars na bk aty c = +and factorize_lambda inctx scopes vars na bk t c = + let implicit_type = is_reserved_type na t in + let aty = extern_typ scopes vars t in + let vars = add_vname vars na in let store, get = set_temporary_memory () in match na, DAst.get c with | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) @@ -1086,16 +1126,20 @@ and factorize_lambda inctx scopes vars na bk aty c = | _ -> CLambdaN ([binder],b)) | _ -> assert false) | _, _ -> - let c = sub_extern inctx scopes vars c in - match c.v with + let c' = sub_extern inctx scopes vars c in + match c'.v with | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + when binding_kind_eq bk bk' + && not (occur_name na ty) (* avoid na in ty escapes scope *) + && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) -> + let aty = if implicit_type then ty else aty in CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | CLambdaN (bl,b) -> - CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + let ty = if implicit_type then hole else aty in + CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b) | _ -> - CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) + let ty = if implicit_type then hole else aty in + CLambdaN ([CLocalAssum([make na],Default bk,ty)],c') and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -1109,15 +1153,17 @@ and extern_local_binder scopes vars = function Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> + let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) - when constr_expr_eq ty ty' && + when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> + let ty = if implicit_type then hole else ty in (na::assums,na::ids, CLocalAssum([CAst.make na],Default bk,ty) :: l)) @@ -1185,11 +1231,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) match keyrule with - | NotationRule (sc,ntn) -> + | NotationRule (_,ntn as specific_ntn) -> (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) scopes with + match availability_of_notation specific_ntn scopes with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) @@ -1212,7 +1258,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = List.map (fun (bl,(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in - let c = make_notation loc ntn (l,ll,bl,bll) in + let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b2c572d290..1cfd50e26e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -226,7 +226,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> + | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -242,7 +242,7 @@ let contract_curly_brackets_pat ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> + | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -1719,13 +1719,13 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> + | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in rcp_of_glob scopes pat - | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> + | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> in_pat top scopes a - | CPatNotation (ntn,fullargs,extrargs) -> + | CPatNotation (_,ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in @@ -2035,11 +2035,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2) - | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> + | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p))) - | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a - | CNotation (ntn,args) -> + | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a + | CNotation (_,ntn,args) -> intern_notation intern env ntnvars loc ntn args | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c @@ -2070,7 +2070,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (ntn,([],[],[],[])) -> + | CNotation (_,ntn,([],[],[],[])) -> assert (Option.is_empty isproj); let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index ffbb982ab7..e6f12f7eb2 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (qid,_) when qualid_is_ident qid -> found c.CAst.loc (qualid_basename qid) bdvars l - | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c diff --git a/interp/notation.ml b/interp/notation.ml index 9d6cab550d..2086e08f79 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false +let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with + | LastLonelyNotation, LastLonelyNotation -> true + | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2 + | (LastLonelyNotation | NotationInScope _), _ -> false + let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 @@ -63,6 +68,15 @@ module NotationOrd = module NotationSet = Set.Make(NotationOrd) module NotationMap = CMap.Make(NotationOrd) +module SpecificNotationOrd = + struct + type t = specific_notation + let compare = pervasives_compare + end + +module SpecificNotationSet = Set.Make(SpecificNotationOrd) +module SpecificNotationMap = CMap.Make(SpecificNotationOrd) + (**********************************************************************) (* Scope of symbols *) @@ -148,21 +162,21 @@ let normalize_scope sc = (**********************************************************************) (* The global stack of scopes *) -type scope_elem = Scope of scope_name | SingleNotation of notation -type scopes = scope_elem list +type scope_item = OpenScopeItem of scope_name | LonelyNotationItem of notation +type scopes = scope_item list let scope_eq s1 s2 = match s1, s2 with -| Scope s1, Scope s2 -> String.equal s1 s2 -| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2 -| Scope _, SingleNotation _ -| SingleNotation _, Scope _ -> false +| OpenScopeItem s1, OpenScopeItem s2 -> String.equal s1 s2 +| LonelyNotationItem s1, LonelyNotationItem s2 -> notation_eq s1 s2 +| OpenScopeItem _, LonelyNotationItem _ +| LonelyNotationItem _, OpenScopeItem _ -> false let scope_stack = ref [] let current_scopes () = !scope_stack let scope_is_open_in_scopes sc l = - List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l + List.exists (function OpenScopeItem sc' -> String.equal sc sc' | _ -> false) l let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) @@ -188,7 +202,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_elem -> obj = +let inScope : bool * bool * scope_item -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -197,11 +211,11 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) + Lib.add_anonymous_leaf (inScope (local,opening,OpenScopeItem (normalize_scope sc))) let empty_scope_stack = [] -let push_scope sc scopes = Scope sc :: scopes +let push_scope sc scopes = OpenScopeItem sc :: scopes let push_scopes = List.fold_right push_scope @@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key = (* Uninterpretation tables *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t (* We define keys for glob_constr and aconstr to split the syntax entries @@ -1064,17 +1078,17 @@ let check_required_module ?loc sc (sp,d) = the scope stack [scopes], and if yes, using delimiters or not *) let find_with_delimiters = function - | None -> None - | Some scope -> + | LastLonelyNotation -> None + | NotationInScope scope -> match (String.Map.find scope !scope_map).delimiters with | Some key -> Some (Some scope, Some key) | None -> None let rec find_without_delimiters find (ntn_scope,ntn) = function - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with - | Some scope' when String.equal scope scope' -> + | NotationInScope scope' when String.equal scope scope' -> Some (None,None) | _ -> (* If the most recently open scope has a notation/numeral printer @@ -1084,9 +1098,9 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function else find_without_delimiters find (ntn_scope,ntn) scopes end - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> begin match ntn_scope, ntn with - | None, Some ntn when notation_eq ntn ntn' -> + | LastLonelyNotation, Some ntn when notation_eq ntn ntn' -> Some (None, None) | _ -> find_without_delimiters find (ntn_scope,ntn) scopes @@ -1123,7 +1137,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = scope_map := String.Map.add scope sc !scope_map end; begin match scopt with - | None -> scope_stack := SingleNotation ntn :: !scope_stack + | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack | Some _ -> () end @@ -1133,15 +1147,15 @@ let declare_uninterpretation rule (metas,c as pat) = let rec find_interpretation ntn find = function | [] -> raise Not_found - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) - | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> + | LonelyNotationItem ntn'::scopes when notation_eq ntn' ntn -> (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) - | SingleNotation _::scopes -> + | LonelyNotationItem _::scopes -> find_interpretation ntn find scopes let find_notation ntn sc = @@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes = commonly from the lowest level of the source entry to the highest level of the target entry. *) -type entry_coercion = notation list +type entry_coercion = (notation_with_optional_scope * notation) list module EntryCoercionOrd = struct @@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function else if shorter_path path path' then path::allpaths else path'::insert_coercion_path path paths -let declare_entry_coercion (entry,_ as ntn) entry' = +let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' = let entry, lev = decompose_custom_entry entry in let entry', lev' = decompose_custom_entry entry' in (* Transitive closure *) @@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' = List.fold_right (fun ((lev'',lev'''),path) l -> if notation_entry_eq entry entry''' && level_ord lev lev''' && not (notation_entry_eq entry' entry'') - then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l) + then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l) !entry_coercion_map [] in let toaddright = EntryCoercionMap.fold (fun (entry'',entry''') paths l -> List.fold_right (fun ((lev'',lev'''),path) l -> if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' - then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l) + then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l) !entry_coercion_map [] in entry_coercion_map := List.fold_right (fun (pair,path) -> let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in EntryCoercionMap.add pair (insert_coercion_path path olds)) - (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft) + (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft) !entry_coercion_map let entry_has_global_map = ref String.Map.empty @@ -1349,34 +1363,6 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false -let entry_has_numeral_map = ref String.Map.empty -let entry_has_string_map = ref String.Map.empty - -let declare_custom_entry_has_numeral s n = - try - let p = String.Map.find s !entry_has_numeral_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for numerals at level " ++ int p ++ str ".") - with Not_found -> - entry_has_numeral_map := String.Map.add s n !entry_has_numeral_map - -let declare_custom_entry_has_string s n = - try - let p = String.Map.find s !entry_has_string_map in - user_err (str "Custom entry " ++ str s ++ - str " has already a rule for strings at level " ++ int p ++ str ".") - with Not_found -> - entry_has_string_map := String.Map.add s n !entry_has_string_map - -let entry_has_prim_token prim = function - | InConstrEntrySomeLevel -> true - | InCustomEntryLevel (s,n) -> - match prim with - | Numeral _ -> - (try String.Map.find s !entry_has_numeral_map <= n with Not_found -> false) - | String _ -> - (try String.Map.find s !entry_has_string_map <= n with Not_found -> false) - let uninterp_prim_token c = match glob_prim_constr_key c with | None -> raise Notation_ops.No_match @@ -1417,7 +1403,7 @@ let availability_of_prim_token n printer_scope local_scopes = with Not_found -> false in let scopes = make_current_scopes local_scopes in - Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) + Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes) (* Miscellaneous *) @@ -1733,11 +1719,11 @@ let pr_scopes prglob = let rec find_default ntn = function | [] -> None - | Scope scope :: scopes -> + | OpenScopeItem scope :: scopes -> if NotationMap.mem ntn (find_scope scope).notations then Some scope else find_default ntn scopes - | SingleNotation ntn' :: scopes -> + | LonelyNotationItem ntn' :: scopes -> if notation_eq ntn ntn' then Some default_scope else find_default ntn scopes @@ -1891,13 +1877,13 @@ let collect_notation_in_scope scope sc known = let collect_notations stack = fst (List.fold_left (fun (all,knownntn as acc) -> function - | Scope scope -> + | OpenScopeItem scope -> if String.List.mem_assoc scope all then acc else let (l,knownntn) = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) - | SingleNotation ntn -> + | LonelyNotationItem ntn -> if List.mem_f notation_eq ntn knownntn then (all,knownntn) else try diff --git a/interp/notation.mli b/interp/notation.mli index 707be6cb87..26c45d5896 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool (** Equality on [notation_entry_level]. *) +val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool + val notation_eq : notation -> notation -> bool (** Equality on [notation]. *) module NotationSet : Set.S with type elt = notation module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet +module SpecificNotationSet : Set.S with type elt = specific_notation +module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet (** {6 Scopes } *) (** A scope is a set of interpreters for symbols + optional @@ -213,7 +217,7 @@ val availability_of_prim_token : (** Binds a notation in a given scope to an interpretation *) type interp_rule = - | NotationRule of scope_name option * notation + | NotationRule of specific_notation | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> @@ -236,7 +240,7 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> subscopes -> +val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option (** {6 Miscellaneous} *) @@ -299,18 +303,15 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -type entry_coercion = notation list -val declare_entry_coercion : notation -> notation_entry_level -> unit +type entry_coercion = (notation_with_optional_scope * notation) list +val declare_entry_coercion : specific_notation -> notation_entry_level -> unit val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit -val declare_custom_entry_has_numeral : string -> int -> unit -val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool -val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) |