summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml149
1 files changed, 105 insertions, 44 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 84bda0af..ca64cda0 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml,v 1.105.2.2 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: metasyntax.ml,v 1.105.2.6 2004/11/22 12:41:38 herbelin Exp $ *)
open Pp
open Util
@@ -606,6 +606,41 @@ let make_hunks etyps symbols from =
in make NoBreak symbols
+let error_format () = error "The format does not match the notation"
+
+let rec split_format_at_ldots hd = function
+ | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt
+ | u :: fmt ->
+ check_no_ldots_in_box u;
+ split_format_at_ldots (u::hd) fmt
+ | [] -> raise Exit
+
+and check_no_ldots_in_box = function
+ | UnpBox (_,fmt) ->
+ (try
+ let _ = split_format_at_ldots [] fmt in
+ error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse")
+ with Exit -> ())
+ | _ -> ()
+
+let skip_var_in_recursive_format = function
+ | UnpTerminal _ :: sl (* skip first var *) ->
+ (* To do, though not so important: check that the names match
+ the names in the notation *)
+ sl
+ | _ -> error_format ()
+
+let read_recursive_format sl fmt =
+ let get_head fmt =
+ let sl = skip_var_in_recursive_format fmt in
+ try split_format_at_ldots [] sl with Exit -> error_format () in
+ let rec get_tail = function
+ | a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt)
+ | [], tail -> skip_var_in_recursive_format tail
+ | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"" in
+ let slfmt, fmt = get_head fmt in
+ slfmt, get_tail (slfmt, fmt)
+
let hunks_of_format (from,(vars,typs) as vt) symfmt =
let rec aux = function
| symbs, (UnpTerminal s' as u) :: fmt
@@ -624,12 +659,20 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
symbs', UnpBox (a,b') :: l
| symbs, (UnpCut _ as u) :: fmt ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
+ | SProdList (m,sl) :: symbs, fmt ->
+ let i = list_index m vars in
+ let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+ let slfmt,fmt = read_recursive_format sl fmt in
+ let sl, slfmt = aux (sl,slfmt) in
+ if sl <> [] then error_format ();
+ let symbs, l = aux (symbs,fmt) in
+ symbs, UnpListMetaVar (i,prec,slfmt) :: l
| symbs, [] -> symbs, []
- | _, _ -> error "The format does not match the notation"
+ | _, _ -> error_format ()
in
match aux symfmt with
| [], l -> l
- | _ -> error "The format does not match the notation"
+ | _ -> error_format ()
let string_of_prec (n,p) =
(string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
@@ -708,13 +751,6 @@ let recompute_assoc typs =
| _, Some Gramext.RightA -> Some Gramext.RightA
| _ -> None
-let rec expand_squash = function
- | Term ("","{") :: NonTerm (ETConstr _, n) :: Term ("","}") :: l ->
- NonTerm (ETConstr (NextLevel,InternalProd),n)
- :: expand_squash l
- | a :: l -> a :: expand_squash l
- | [] -> []
-
let make_grammar_rule n typs symbols ntn perm =
let assoc = recompute_assoc typs in
let prod = make_production typs symbols in
@@ -777,7 +813,7 @@ let pr_level ntn (from,args) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
prlist_with_sep pr_coma (pr_arg_level from) args
-let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
+let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) =
try
let oldprec, oldprec8 = Symbols.level_of_notation ntn in
if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then
@@ -799,13 +835,14 @@ let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
warning ("Notation "^ntn^
" was already assigned a different level or sublevels");
if oldprec = None or out_some oldprec <> out_some prec then
- Egrammar.extend_grammar (Egrammar.Notation (out_some gr))
+ Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr))
end
with Not_found ->
(* Reserve the notation level *)
Symbols.declare_notation_level ntn (prec,prec8);
(* Declare the parsing rule *)
- option_iter (fun gr -> Egrammar.extend_grammar (Egrammar.Notation gr)) gr;
+ option_iter (fun gr ->
+ Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr;
(* Declare the printing rule *)
Symbols.declare_notation_printing_rule ntn (se,fst prec8)
@@ -813,15 +850,15 @@ let subst_notation_grammar subst x = x
let subst_printing_rule subst x = x
-let subst_syntax_extension (_,subst,(local,prec,ntn,gr,se)) =
- (local,prec,ntn,
+let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) =
+ (local,(prec,ntn,
option_app (subst_notation_grammar subst) gr,
- subst_printing_rule subst se)
+ subst_printing_rule subst se))
-let classify_syntax_definition (_,(local,_,_,_,_ as o)) =
+let classify_syntax_definition (_,(local,_ as o)) =
if local then Dispose else Substitute o
-let export_syntax_definition (local,_,_,_,_ as o) =
+let export_syntax_definition (local,_ as o) =
if local then None else Some o
let (inSyntaxExtension, outSyntaxExtension) =
@@ -897,6 +934,10 @@ let check_rule_reversibility l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
error "A notation must include at least one symbol"
+let is_not_printable = function
+ | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
+ | _ -> false
+
let find_precedence_v7 lev etyps symbols =
(match symbols with
| NonTerminal x :: _ ->
@@ -1010,7 +1051,7 @@ let add_syntax_extension local mv mv8 =
let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
let pp_rule = make_pp_rule ppdata in
Lib.add_anonymous_leaf
- (inSyntaxExtension (local,(prec,ppprec),ntn',gram_rule,pp_rule))
+ (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule)))
(**********************************************************************)
(* Distfix, Infix, Symbols *)
@@ -1139,33 +1180,38 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
let gram_rule = make_grammar_rule n typs symbols ntn permut in
Lib.add_anonymous_leaf
(inSyntaxExtension
- (local,(Some prec,ppprec),ntn,Some gram_rule,pp_rule));
+ (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule)));
(* Declare interpretation *)
let (acvars,ac) = interp_aconstr [] ppvars c in
let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in
let old_pp_rule =
(* Used only by v7; disable if contains a recursive pattern *)
- if onlyparse or pprecvars <> [] then None
+ if onlyparse or pprecvars <> [] or not (!Options.v7) then None
else
let r = interp_global_rawconstr_with_vars vars c in
Some (make_old_pp_rule n symbols typs r intnot scope vars) in
- let onlyparse = onlyparse or !Options.v7_only in
+ let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in
Lib.add_anonymous_leaf
(inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df'))
let level_rule (n,p) = if p = E then n else max (n-1) 0
-let check_notation_existence notation =
- try
- let a,_ = Symbols.level_of_notation (contract_notation notation) in
- if a = None then raise Not_found
- with Not_found ->
- error "Parsing rule for this notation has to be previously declared"
+let recover_syntax ntn =
+ try
+ match Symbols.level_of_notation ntn with
+ | (Some prec,_ as pprec) ->
+ let rule,_ = Symbols.find_notation_printing_rule ntn in
+ let gr = Egrammar.recover_notation_grammar ntn prec in
+ Some (pprec,ntn,Some gr,rule)
+ | None,_ -> None
+ with Not_found -> None
-let exists_notation_syntax ntn =
- try fst (Symbols.level_of_notation (contract_notation ntn)) <> None
- with Not_found -> false
+let recover_notation_syntax rawntn =
+ let ntn = contract_notation rawntn in
+ match recover_syntax ntn with
+ | None -> None
+ | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }")
let set_data_for_v7_pp recs a vars =
if not !Options.v7 then None else
@@ -1185,34 +1231,44 @@ let build_old_pp_rule notation scope symbs (r,vars) =
make_old_pp_rule (fst prec) symbs typs r notation scope vars
let add_notation_interpretation_core local symbs for_old df a scope onlyparse
- onlypp =
+ onlypp gram_data =
let notation = make_notation_key symbs in
let old_pp_rule =
if !Options.v7 then
option_app (build_old_pp_rule notation scope symbs) for_old
else None in
+ option_iter
+ (fun (x,y) ->
+ Lib.add_anonymous_leaf (inSyntaxExtension (local,x));
+ option_iter
+ (fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y)
+ gram_data;
Lib.add_anonymous_leaf
(inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,
(Lib.library_dp(),df)))
let add_notation_interpretation df names c sc =
let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
- check_notation_existence (make_notation_key symbs);
+ let gram_data = recover_notation_syntax (make_notation_key symbs) in
+ if gram_data = None then
+ error "Parsing rule for this notation has to be previously declared";
let (acvars,ac) = interp_aconstr names vars c in
let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in
let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
- add_notation_interpretation_core false symbs for_oldpp df a sc false false
+ let onlyparse = is_not_printable ac in
+ add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse
+ false gram_data
let add_notation_in_scope_v8only local df c mv8 scope toks =
let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
let pp_rule = make_pp_rule ppdata in
Lib.add_anonymous_leaf
- (inSyntaxExtension(local,(None,prec),notation,None,pp_rule));
+ (inSyntaxExtension(local,((None,prec),notation,None,pp_rule)));
(* Declare the interpretation *)
- let onlyparse = false in
let (acvars,ac) = interp_aconstr [] vars c in
let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
+ let onlyparse = is_not_printable ac in
Lib.add_anonymous_leaf
(inNotation(local,None,intnot,scope,a,onlyparse,true,df'))
@@ -1231,11 +1287,12 @@ let add_notation_v8only local c (df,modifiers) sc =
else
(* Declare only interpretation *)
let (recs,vars,symbs) = analyse_notation_tokens toks in
- let onlyparse = modifiers = [SetOnlyParsing] in
let (acvars,ac) = interp_aconstr [] vars c in
+ let onlyparse = modifiers = [SetOnlyParsing]
+ or is_not_printable ac in
let a = (remove_vars recs acvars,ac) in
add_notation_interpretation_core local symbs None df a sc
- onlyparse true
+ onlyparse true None
| Some n ->
(* Declare both syntax and interpretation *)
let mods =
@@ -1266,14 +1323,17 @@ let add_notation local c dfmod mv8 sc =
else
(* Declare only interpretation *)
let (recs,vars,symbs) = analyse_notation_tokens toks in
- if exists_notation_syntax (make_notation_key symbs) then
- let onlyparse = modifiers = [SetOnlyParsing] in
+ let gram_data =
+ recover_notation_syntax (make_notation_key symbs) in
+ if gram_data <> None then
let (acvars,ac) = interp_aconstr [] vars c in
let a = (remove_vars recs acvars,ac) in
+ let onlyparse = modifiers = [SetOnlyParsing]
+ or is_not_printable ac in
let a_for_old = interp_global_rawconstr_with_vars vars c in
let for_old = set_data_for_v7_pp recs a_for_old vars in
add_notation_interpretation_core local symbs for_old df a
- sc onlyparse false
+ sc onlyparse false gram_data
else
add_notation_in_scope local df c modifiers mv8 sc toks
| Some n ->
@@ -1340,7 +1400,7 @@ let add_infix local (inf,modl) pr mv8 sc =
let a' = (remove_vars recs acvars,ac) in
let a_for_old = interp_global_rawconstr_with_vars vars a in
add_notation_interpretation_core local symbs None df a' sc
- onlyparse true
+ onlyparse true None
else
if n8 = None then error "Needs a level" else
let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in
@@ -1365,13 +1425,14 @@ let add_infix local (inf,modl) pr mv8 sc =
(* de ne déclarer que l'interprétation *)
(* Declare only interpretation *)
let (recs,vars,symbs) = analyse_notation_tokens toks in
- if exists_notation_syntax (make_notation_key symbs) then
+ let gram_data = recover_notation_syntax (make_notation_key symbs) in
+ if gram_data <> None then
let (acvars,ac) = interp_aconstr [] vars a in
let a' = (remove_vars recs acvars,ac) in
let a_for_old = interp_global_rawconstr_with_vars vars a in
let for_old = set_data_for_v7_pp recs a_for_old vars in
add_notation_interpretation_core local symbs for_old df a' sc
- onlyparse false
+ onlyparse false gram_data
else
let mv,mv8 = make_infix_data n assoc modl mv8 in
add_notation_in_scope local df a mv mv8 sc toks
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 17:01:54 +0000