diff options
| -rw-r--r-- | interp/symbols.ml | 59 | ||||
| -rw-r--r-- | interp/symbols.mli | 13 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 14 | ||||
| -rw-r--r-- | toplevel/command.ml | 33 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 91 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 3 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 9 |
9 files changed, 145 insertions, 81 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index ef2cf6b0b..ec93062ee 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -42,11 +42,15 @@ open Ppextend type scopes = scope_name list type level = precedence * precedence list type delimiters = string + type scope = { - notations: (interpretation * (level * string)) Stringmap.t; + notations: (interpretation * string) Stringmap.t; delimiters: delimiters option } +(* Uninterpreted notation map: notation -> level *) +let notation_level_map = ref Stringmap.empty + (* Scopes table: scope_name -> symbol_interpretation *) let scope_map = ref Stringmap.empty @@ -204,14 +208,23 @@ let rec find_without_delimiters find ntn_scope = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope +(* Uninterpreted notation levels *) + +let declare_notation_level ntn level = + if not !Options.v7 & Stringmap.mem ntn !notation_level_map then + error ("Notation "^ntn^" is already assigned a level"); + notation_level_map := Stringmap.add ntn level !notation_level_map + +let level_of_notation ntn = + Stringmap.find ntn !notation_level_map + (* The mapping between notations and their interpretation *) -let declare_notation_interpretation ntn scope pat prec df = +let declare_notation_interpretation ntn scope pat df = let sc = find_scope scope in if Stringmap.mem ntn sc.notations && Options.is_verbose () then warning ("Notation "^ntn^" is already used in scope "^scope); - let sc = - { sc with notations = Stringmap.add ntn (pat,(prec,df)) sc.notations } in + let sc = { sc with notations = Stringmap.add ntn (pat,df) sc.notations } in scope_map := Stringmap.add scope sc !scope_map let declare_uninterpretation rule (metas,c as pat) = @@ -227,7 +240,7 @@ let rec find_interpretation f = function let rec interp_notation ntn scopes = let f scope = fst (Stringmap.find ntn scope.notations) in try find_interpretation f (scopes @ !scope_stack) - with Not_found -> anomaly ("Unknown interpretation for notation "^ntn) + with Not_found -> error ("Unknown interpretation for notation "^ntn) let uninterp_notations c = Gmapl.find (rawconstr_key c) !notations_key_table @@ -278,20 +291,13 @@ let availability_of_numeral printer_scope scopes = (* Miscellaneous *) -let exists_notation_in_scope scope prec ntn r = +let exists_notation_in_scope scope ntn r = try let sc = Stringmap.find scope !scope_map in - let (r',(prec',_)) = Stringmap.find ntn sc.notations in - r' = r & prec = prec' + let (r',_) = Stringmap.find ntn sc.notations in + r' = r with Not_found -> false -let exists_notation_prec prec nt sc = - try fst (snd (Stringmap.find nt sc.notations)) = prec with Not_found -> false - -let exists_notation prec nt = - Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc) - !scope_map false - (* Exportation of scopes *) let cache_scope (_,(local,sc)) = check_scope sc; @@ -357,7 +363,7 @@ let pr_named_scope prraw scope sc = str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters ++ fnl () ++ Stringmap.fold - (fun ntn ((_,r),(_,df)) strm -> + (fun ntn ((_,r),df) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -379,7 +385,7 @@ let locate_notation prraw ntn = Stringmap.fold (fun scope_name sc l -> try - let ((_,r),(_,df)) = Stringmap.find ntn sc.notations in + let ((_,r),df) = Stringmap.find ntn sc.notations in (scope_name,r,df)::l with Not_found -> l) !scope_map [] in @@ -396,17 +402,6 @@ let locate_notation prraw ntn = fnl ())) l -let find_notation_level ntn = - let l = - Stringmap.fold - (fun _ sc l -> - try fst (snd (Stringmap.find ntn sc.notations)) :: l - with Not_found -> l) !scope_map [] in - match l with - | [] -> raise Not_found - | [prec] -> prec - | prec::_ -> warning ("Several parsing rules for notation \""^ntn^"\""); prec - (**********************************************************************) (* Mapping notations to concrete syntax *) @@ -427,11 +422,12 @@ let find_notation_printing_rule ntn = (* Synchronisation with reset *) let freeze () = - (!scope_map, !scope_stack, !arguments_scope, !delimiters_map, - !notations_key_table, !printing_rules) + (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !printing_rules) -let unfreeze (scm,scs,asc,dlm,fkm,pprules) = +let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules) = scope_map := scm; + notation_level_map := nlm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; @@ -444,6 +440,7 @@ let init () = scope_stack := Stringmap.empty arguments_scope := Refmap.empty *) + notation_level_map := Stringmap.empty; delimiters_map := Stringmap.empty; notations_key_table := Gmapl.empty; printing_rules := Stringmap.empty diff --git a/interp/symbols.mli b/interp/symbols.mli index fa3d778f1..4c96d071b 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -83,7 +83,7 @@ type interp_rule = | NotationRule of scope_name * notation | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name -> - interpretation -> level -> string -> unit + interpretation -> string -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit @@ -101,12 +101,16 @@ val uninterp_notations : rawconstr -> val availability_of_notation : scope_name * notation -> scopes -> (scope_name option * delimiters option) option +(*s Declare and test the level of a (possibly uninterpreted) notation *) + +val declare_notation_level : notation -> level -> unit +val level_of_notation : notation -> level (* [Not_found] if no level *) + (*s** Miscellaneous *) (* Checks for already existing notations *) -val exists_notation_in_scope : scope_name -> level -> notation -> +val exists_notation_in_scope : scope_name -> notation -> interpretation-> bool -val exists_notation : level -> notation -> bool (* Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope: global_reference -> scope_name option list -> unit @@ -117,9 +121,6 @@ val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds -(* [raise Not_found] if non existing notation *) -val find_notation_level : notation -> level - (**********************************************************************) (*s Printing rules for notations *) diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 581726891..f64062279 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -242,8 +242,18 @@ GEXTEND Gram VernacSyntax (u,el) | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,s,l) + modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; + (s8,mv8) = + [IDENT "V8only"; + s8=OPT STRING; + mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] -> + (s8,mv8) + | -> (None,None)] -> + let s8 = match s8 with Some s -> s | _ -> s in + let mv8 = match mv8 with + Some mv8 -> mv8 + | _ -> List.map map_modl modl in + VernacSyntaxExtension (local,s,modl,Some(s8,mv8)) | IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> VernacOpenScope (local,sc) diff --git a/toplevel/command.ml b/toplevel/command.ml index 337e321df..d9418f58f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -214,14 +214,20 @@ let interp_mutual lparams lnamearconstrs finite = (env0, [], []) lnamearconstrs in let lparnames = List.map (fun (na,_,_) -> na) params in + let notations = + List.map2 (fun (recname,ntnopt,_,_) ar -> + option_app (fun df -> + let larnames = + List.rev_append lparnames + (List.map fst (fst (decompose_prod ar))) in + (recname,larnames,df)) ntnopt) + lnamearconstrs arityl in let fs = States.freeze() in - List.iter2 (fun (recname,ntnopt,_,_) ar -> - option_iter - (fun (df,scope) -> - let larnames = lparnames @ List.map fst (fst (decompose_prod ar)) in - Metasyntax.add_notation_interpretation df - (AVar recname,larnames) scope) ntnopt) - lnamearconstrs arityl; + (* Declare the notations for the inductive types pushed in local context*) + try + List.iter (option_iter (fun (recname,larnames,(df,scope)) -> + Metasyntax.add_notation_interpretation df + (AVar recname,larnames) scope)) notations; let ind_env_params = push_rel_context params ind_env in let mispecvec = List.map2 @@ -238,7 +244,9 @@ let interp_mutual lparams lnamearconstrs finite = mind_entry_lc = constrs }) (List.rev arityl) lnamearconstrs in - { mind_entry_finite = finite; mind_entry_inds = mispecvec } + States.unfreeze fs; + notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec } + with e -> States.unfreeze fs; raise e let declare_mutual_with_eliminations mie = let lrecnames = @@ -277,8 +285,13 @@ let extract_coe_la_lc = function let build_mutual lind finite = let (coes,lparams,lnamearconstructs) = extract_coe_la_lc lind in - let mie = interp_mutual lparams lnamearconstructs finite in - let _ = declare_mutual_with_eliminations mie in + let notations,mie = interp_mutual lparams lnamearconstructs finite in + let kn = declare_mutual_with_eliminations mie in + (* Declare the notations now bound to the inductive types *) + list_iter_i (fun i -> + option_iter (fun (_,names,(df,scope)) -> + Metasyntax.add_notation_interpretation df + (ARef (IndRef (kn,i)),names) scope)) notations; List.iter (fun id -> Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 51a9eec35..1e0077373 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -499,11 +499,25 @@ let make_pp_rule symbols typs n = (* Syntax extenstion: common parsing/printing rules and no interpretation *) let cache_syntax_extension (_,(_,prec,ntn,gr,se)) = - if not (Symbols.exists_notation prec ntn) then begin + try + let oldprec = Symbols.level_of_notation ntn in + if oldprec <> prec then + if !Options.v7 then begin + Options.if_verbose + warning ("Notation "^ntn^" was already assigned a different level"); + raise Not_found + end else + error ("Notation "^ntn^" is already assigned a different level") + else + (* The notation is already declared; no need to redeclare it *) + () + with Not_found -> + (* Reserve the notation level *) + Symbols.declare_notation_level ntn prec; + (* Declare the parsing rule *) Egrammar.extend_grammar (Egrammar.Notation gr); - if se<>None then - Symbols.declare_notation_printing_rule ntn (out_some se,fst prec) - end + (* Declare the printing rule *) + Symbols.declare_notation_printing_rule ntn (se,fst prec) let subst_notation_grammar subst x = x @@ -512,7 +526,7 @@ let subst_printing_rule subst x = x let subst_syntax_extension (_,subst,(local,prec,ntn,gr,se)) = (local,prec,ntn, subst_notation_grammar subst gr, - option_app (subst_printing_rule subst) se) + subst_printing_rule subst se) let classify_syntax_definition (_,(local,_,_,_,_ as o)) = if local then Dispose else Substitute o @@ -602,11 +616,11 @@ let recompute_assoc typs = | _, Some Gramext.RightA -> Some Gramext.RightA | _ -> None -let add_syntax_extension local df modifiers = +let add_syntax_extension local df modifiers mv8 = let (assoc,n,etyps,onlyparse) = interp_notation_modifiers modifiers in let inner = if !Options.v7 then (NumLevel 10,InternalProd) else (NumLevel 200,InternalProd) in - let (vars,symbs) = analyse_tokens (split df) in + let (_,symbs) = analyse_tokens (split df) in let typs = find_symbols (NumLevel n,BorderProd(true,assoc)) inner @@ -614,29 +628,45 @@ let add_syntax_extension local df modifiers = let typs = List.map (set_entry_type etyps) typs in let assoc = recompute_assoc typs in let (prec,notation) = make_symbolic n symbs typs in + let (ppprec,ppn,pptyps,ppsymbols) = + let omodv8 = option_app (fun (s8,ml8) -> + let toks8 = split s8 in + let im8 = interp_notation_modifiers ml8 in + (toks8,im8)) mv8 in + match omodv8 with + Some(toks8,(a8,n8,typs8,_)) when Options.do_translate() -> + let (_,symbols) = analyse_tokens toks8 in + let typs = + find_symbols + (NumLevel n8,BorderProd(true,a8)) (NumLevel 200,InternalProd) + (NumLevel n8,BorderProd(false,a8)) + symbols in + let typs = List.map (set_entry_type typs8) typs in + let (prec,notation) = make_symbolic n8 symbols typs in + (prec, n8, typs, symbols) + | _ -> (prec, n, typs, symbs) in let gram_rule = make_grammar_rule n assoc typs symbs notation in - let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs n) in + let pp_rule = make_pp_rule pptyps ppsymbols ppn in Lib.add_anonymous_leaf - (inSyntaxExtension(local,prec,notation,gram_rule,pp_rule)) + (inSyntaxExtension(local,ppprec,notation,gram_rule,pp_rule)) (**********************************************************************) (* Distfix, Infix, Notations *) (* A notation comes with a grammar rule, a pretty-printing rule, an identifiying pattern called notation and an associated scope *) -let load_notation _ (_,(_,_,prec,ntn,scope,pat,onlyparse,_)) = +let load_notation _ (_,(_,_,ntn,scope,pat,onlyparse,_)) = Symbols.declare_scope scope -let open_notation i (_,(_,oldse,prec,ntn,scope,pat,onlyparse,df)) = -(*print_string ("Open notation "^ntn^" at "^string_of_int (fst prec)^"\n");*) +let open_notation i (_,(_,oldse,ntn,scope,pat,onlyparse,df)) = if i=1 then begin - let b = Symbols.exists_notation_in_scope scope prec ntn pat in + let b = Symbols.exists_notation_in_scope scope ntn pat in (* Declare the old printer rule and its interpretation *) if not b & oldse <> None then Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse}; (* Declare the interpretation *) if not b then - Symbols.declare_notation_interpretation ntn scope pat prec df; + Symbols.declare_notation_interpretation ntn scope pat df; if not b & not onlyparse then Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat end @@ -645,17 +675,16 @@ let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (_,subst,(lc,oldse,prec,ntn,scope,(metas,pat),b,df)) = +let subst_notation (_,subst,(lc,oldse,ntn,scope,(metas,pat),b,df)) = (lc,option_app (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse, - prec,ntn, - scope, + ntn,scope, (metas,subst_aconstr subst pat), b, df) -let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) = +let classify_notation (_,(local,_,_,_,_,_,_ as o)) = if local then Dispose else Substitute o -let export_notation (local,_,_,_,_,_,_,_ as o) = +let export_notation (local,_,_,_,_,_,_ as o) = if local then None else Some o let (inNotation, outNotation) = @@ -718,9 +747,7 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks = (prec, n8, typs, symbols) | _ -> (prec, n, typs, symbols) in let gram_rule = make_grammar_rule n assoc typs symbols notation in - let pp_rule = - if onlyparse then None - else Some (make_pp_rule pptyps ppsymbols n) in + let pp_rule = make_pp_rule pptyps ppsymbols ppn in Lib.add_anonymous_leaf (inSyntaxExtension(local,ppprec,notation,gram_rule,pp_rule)); let old_pp_rule = @@ -732,7 +759,7 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks = (* Declare the interpretation *) let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,ppprec,notation,scope,a,onlyparse,df)) + (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,df)) let add_notation local df a modifiers mv8 sc = let toks = split df in @@ -760,16 +787,28 @@ let add_notation_interpretation df (c,l) sc = let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in let (vars,symbs) = analyse_tokens (split df) in let notation = make_anon_notation symbs in - let old_pp_rule = None in - let prec = Symbols.find_notation_level notation in + let prec = + try Symbols.level_of_notation notation + with Not_found -> + error "Parsing rule for this notation has to be previously declared" in List.iter (check_occur l) vars; + let old_pp_rule = + let c = match c with AVar id -> RVar (dummy_loc,id) + | ARef c -> RRef (dummy_loc,c) + | _ -> anomaly "add_notation_interpretation" in + let typs = List.map2 + (fun id n -> id,ETConstr (NumLevel n,InternalProd)) vars (snd prec) in + let r = RApp (dummy_loc, c, + List.map (function Name id when List.mem id vars -> RVar (dummy_loc,id) + | _ -> RHole (dummy_loc,QuestionMark)) l) in + Some (make_old_pp_rule (fst prec) symbs typs r notation scope vars) in let a = AApp (c,List.map (function Name id when List.mem id vars -> AVar id | _ -> AHole QuestionMark) l) in let la = List.map (fun id -> id,[]) vars in let onlyparse = false in let local = false in Lib.add_anonymous_leaf - (inNotation(local,old_pp_rule,prec,notation,scope,(la,a),onlyparse,df)) + (inNotation(local,old_pp_rule,notation,scope,(la,a),onlyparse,df)) (* TODO add boxes information in the expression *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 59e786fe3..641db8425 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -44,7 +44,7 @@ val add_notation : locality_flag -> string -> constr_expr val add_notation_interpretation : string -> (aconstr * Names.name list) -> scope_name option -> unit -val add_syntax_extension : locality_flag -> string -> syntax_modifier list -> unit +val add_syntax_extension : locality_flag -> string -> syntax_modifier list -> (string * syntax_modifier list) option -> unit val print_grammar : string -> string -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9b11e6879..bc77424c5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1139,7 +1139,7 @@ let interp c = match c with | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al | VernacGrammar (univ,al) -> vernac_grammar univ al - | VernacSyntaxExtension (local,s,l) -> vernac_syntax_extension local s l + | VernacSyntaxExtension (lcl,s,l,l8) -> vernac_syntax_extension lcl s l l8 | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index b2f82854c..b68fe7022 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -152,7 +152,8 @@ type vernac_expr = | VernacTacticGrammar of (string * (string * grammar_production list) * raw_tactic_expr) list | VernacSyntax of string * raw_syntax_entry list - | VernacSyntaxExtension of locality_flag * string * syntax_modifier list + | VernacSyntaxExtension of locality_flag * string * + syntax_modifier list * (string * syntax_modifier list) option | VernacDistfix of locality_flag * grammar_associativity * precedence * string * reference * scope_name option diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 161232a5f..49e455cbb 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -474,9 +474,12 @@ let rec pr_vernac = function (match opt with | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) - | VernacSyntaxExtension (local,a,b) -> - str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs a ++ - (match b with | [] -> mt() | _ as l -> + | VernacSyntaxExtension (local,s,l,mv8) -> + let (s,l) = match mv8 with + None -> (s,l) + | Some ml -> ml in + str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs s ++ + (match l with | [] -> mt() | _ as l -> str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") (* Gallina *) |