aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r--vernac/metasyntax.ml140
1 files changed, 76 insertions, 64 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 462f6215a..6ee0d6c82 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -377,8 +377,8 @@ let is_non_terminal = function
| NonTerminal _ | SProdList _ -> true
| _ -> false
-let is_next_non_terminal = function
-| [] -> false
+let is_next_non_terminal b = function
+| [] -> b
| pr :: _ -> is_non_terminal pr
let is_next_terminal = function Terminal _ :: _ -> true | _ -> false
@@ -387,8 +387,9 @@ let is_next_break = function Break _ :: _ -> true | _ -> false
let add_break n l = (None,UnpCut (PpBrk(n,0))) :: l
-let add_break_if_none n = function
- | (((_,UnpCut (PpBrk _)) :: _) | []) as l -> l
+let add_break_if_none n b = function
+ | (_,UnpCut (PpBrk _)) :: _ as l -> l
+ | [] when not b -> []
| l -> (None,UnpCut (PpBrk(n,0))) :: l
let check_open_binder isopen sl m =
@@ -403,45 +404,58 @@ let check_open_binder isopen sl m =
prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
+let unparsing_metavar i from typs =
+ match List.nth typs (i-1) with
+ | ETConstr _ | ETReference | ETBigint ->
+ let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+ UnpMetaVar (i,prec)
+ | ETPattern n ->
+ UnpBinderMetaVar (i,Prec n)
+ | ETName ->
+ UnpBinderMetaVar (i,Prec 0)
+ | ETBinder isopen ->
+ assert false
+ | ETOther _ -> failwith "TODO"
+
(* Heuristics for building default printing rules *)
let index_id id l = List.index Id.equal id l
let make_hunks etyps symbols from =
let vars,typs = List.split etyps in
- let rec make = function
+ let rec make b = function
| NonTerminal m :: prods ->
let i = index_id m vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let u = UnpMetaVar (i,prec) in
- if is_next_non_terminal prods then
- (None,u) :: add_break_if_none 1 (make prods)
+ let u = unparsing_metavar i from typs in
+ if is_next_non_terminal b prods then
+ (None, u) :: add_break_if_none 1 b (make b prods)
else
- (None,u) :: make_with_space prods
- | Terminal s :: prods when List.exists is_non_terminal prods ->
+ (None, u) :: make_with_space b prods
+ | Terminal s :: prods
+ when (* true to simulate presence of non-terminal *) b || List.exists is_non_terminal prods ->
if (is_comma s || is_operator s) then
(* Always a breakable space after comma or separator *)
- (None,UnpTerminal s) :: add_break_if_none 1 (make prods)
+ (None, UnpTerminal s) :: add_break_if_none 1 b (make b prods)
else if is_right_bracket s && is_next_terminal prods then
(* Always no space after right bracked, but possibly a break *)
- (None,UnpTerminal s) :: add_break_if_none 0 (make prods)
- else if is_left_bracket s && is_next_non_terminal prods then
- (None,UnpTerminal s) :: make prods
+ (None, UnpTerminal s) :: add_break_if_none 0 b (make b prods)
+ else if is_left_bracket s && is_next_non_terminal b prods then
+ (None, UnpTerminal s) :: make b prods
else if not (is_next_break prods) then
(* Add rigid space, no break, unless user asked for something *)
- (None,UnpTerminal (s^" ")) :: make prods
+ (None, UnpTerminal (s^" ")) :: make b prods
else
(* Rely on user spaces *)
- (None,UnpTerminal s) :: make prods
+ (None, UnpTerminal s) :: make b prods
| Terminal s :: prods ->
(* Separate but do not cut a trailing sequence of terminal *)
(match prods with
- | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make prods
- | _ -> (None,UnpTerminal s) :: make prods)
+ | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make b prods
+ | _ -> (None,UnpTerminal s) :: make b prods)
| Break n :: prods ->
- add_break n (make prods)
+ add_break n (make b prods)
| SProdList (m,sl) :: prods ->
let i = index_id m vars in
@@ -451,40 +465,40 @@ let make_hunks etyps symbols from =
(* If no separator: add a break *)
if List.is_empty sl then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
- else snd (List.sep_last (make (sl@[NonTerminal m]))) in
+ else make true sl in
let hunk = match typ with
| ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
| ETBinder isopen ->
check_open_binder isopen sl m;
UnpBinderListMetaVar (i,isopen,List.map snd sl')
| _ -> assert false in
- (None,hunk) :: make_with_space prods
+ (None, hunk) :: make_with_space b prods
| [] -> []
- and make_with_space prods =
+ and make_with_space b prods =
match prods with
| Terminal s' :: prods'->
if is_operator s' then
(* A rigid space before operator and a breakable after *)
- (None,UnpTerminal (" "^s')) :: add_break_if_none 1 (make prods')
+ (None,UnpTerminal (" "^s')) :: add_break_if_none 1 b (make b prods')
else if is_comma s' then
(* No space whatsoever before comma *)
- make prods
+ make b prods
else if is_right_bracket s' then
- make prods
+ make b prods
else
(* A breakable space between any other two terminals *)
- add_break_if_none 1 (make prods)
+ add_break_if_none 1 b (make b prods)
| (NonTerminal _ | SProdList _) :: _ ->
(* A breakable space before a non-terminal *)
- add_break_if_none 1 (make prods)
+ add_break_if_none 1 b (make b prods)
| Break _ :: _ ->
(* Rely on user wish *)
- make prods
+ make b prods
| [] -> []
- in make symbols
+ in make false symbols
(* Build default printing rules from explicit format *)
@@ -538,8 +552,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
| NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') ->
let i = index_id s vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
+ let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l
| symbs, (_,UnpBox (a,b)) :: fmt ->
let symbs', b' = aux (symbs,b) in
let symbs', l = aux (symbs',fmt) in
@@ -642,7 +655,7 @@ let prod_entry_type = function
| ETBigint -> ETProdBigint
| ETBinder _ -> assert false (* See check_binder_type *)
| ETConstr p -> ETProdConstr p
- | ETPattern -> ETProdPattern
+ | ETPattern n -> ETProdPattern n
| ETOther (s,t) -> ETProdOther (s,t)
let make_production etyps symbols =
@@ -699,17 +712,14 @@ let recompute_assoc typs =
(* Registration of syntax extensions (parsing/printing, no interpretation)*)
let pr_arg_level from (lev,typ) =
- let pplev = match lev with
+ let pplev = function
| (n,L) when Int.equal n from -> str "at next level"
| (n,E) -> str "at level " ++ int n
| (n,L) -> str "at level below " ++ int n
| (n,Prec m) when Int.equal m n -> str "at level " ++ int n
| (n,_) -> str "Unknown level" in
- let pptyp = match typ with
- | NtnInternTypeConstr -> mt ()
- | NtnInternTypeBinder -> str " " ++ surround (str "binder")
- | NtnInternTypeIdent -> str " " ++ surround (str "ident") in
- pplev ++ pptyp
+ Ppvernac.pr_set_entry_type typ ++
+ (match typ with ETConstr _ | ETPattern _ -> spc () ++ pplev lev | _ -> mt ())
let pr_level ntn (from,args,typs) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
@@ -916,7 +926,7 @@ let set_entry_type etyps (x,typ) =
| ETConstr (n,()), (_,BorderProd (left,_)) ->
ETConstr (n,BorderProd (left,None))
| ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
- | (ETPattern | ETName | ETBigint | ETOther _ |
+ | (ETPattern _ | ETName | ETBigint | ETOther _ |
ETReference | ETBinder _ as t), _ -> t
with Not_found -> ETConstr typ
in (x,typ)
@@ -937,11 +947,9 @@ let join_auxiliary_recursive_types recvars etyps =
recvars etyps
let internalization_type_of_entry_type = function
- | ETConstr _ -> NtnInternTypeConstr
- | ETBigint | ETReference -> NtnInternTypeConstr
- | ETBinder _ -> NtnInternTypeBinder
- | ETName -> NtnInternTypeIdent
- | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.")
+ | ETBinder _ -> NtnInternTypeOnlyBinder
+ | ETConstr _ | ETBigint | ETReference
+ | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
let set_internalization_type typs =
List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -952,28 +960,32 @@ let make_internalization_vars recvars mainvars typs =
maintyps @ extratyps
let make_interpretation_type isrec isonlybinding = function
- | NtnInternTypeConstr when isrec -> NtnTypeConstrList
- | NtnInternTypeConstr | NtnInternTypeIdent ->
- if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
- | NtnInternTypeBinder when isrec -> NtnTypeBinderList
- | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.")
-
-let make_interpretation_vars recvars allvars =
+ | ETConstr _ ->
+ if isrec then NtnTypeConstrList else
+ if isonlybinding then NtnTypeBinder true (* Parsed as constr, but interpreted as binder *)
+ else NtnTypeConstr
+ | ETName | ETPattern _ -> NtnTypeBinder false (* Parsed as ident/pattern, primarily interpreted as binder *)
+ | ETBigint | ETReference | ETOther _ -> NtnTypeConstr
+ | ETBinder _ ->
+ if isrec then NtnTypeBinderList
+ else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+
+let make_interpretation_vars recvars allvars typs =
let eq_subscope (sc1, l1) (sc2, l2) =
Option.equal String.equal sc1 sc2 &&
List.equal String.equal l1 l2
in
let check (x, y) =
- let (_,scope1, _) = Id.Map.find x allvars in
- let (_,scope2, _) = Id.Map.find y allvars in
+ let (_,scope1) = Id.Map.find x allvars in
+ let (_,scope2) = Id.Map.find y allvars in
if not (eq_subscope scope1 scope2) then error_not_same_scope x y
in
let () = List.iter check recvars in
let useless_recvars = List.map snd recvars in
let mainvars =
Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
- Id.Map.mapi (fun x (isonlybinding, sc, typ) ->
- (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
+ Id.Map.mapi (fun x (isonlybinding, sc) ->
+ (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1042,7 +1054,7 @@ let find_precedence lev etyps symbols onlyprint =
| _ ->
user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
- | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
+ | ETPattern _ | ETBinder _ | ETOther _ -> (* Give a default ? *)
if Option.is_empty lev then
user_err Pp.(str "Need an explicit level.")
else [],Option.get lev
@@ -1167,7 +1179,7 @@ let compute_syntax_data df modifiers =
let i_typs = set_internalization_type sy_typs in
let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
let pp_sy_data = (sy_typs,symbols) in
- let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in
+ let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = ntn_for_interp, df' in
@@ -1186,7 +1198,7 @@ let compute_syntax_data df modifiers =
mainvars;
intern_typs = i_typs;
- level = (n,prec,i_typs);
+ level = (n,prec,List.map snd sy_typs);
pa_syntax_data = pa_sy_data;
pp_syntax_data = pp_sy_data;
not_data = sy_fulldata;
@@ -1345,7 +1357,7 @@ let add_notation_in_scope local df env c mods scope =
ninterp_rec_vars = to_map sd.recvars;
} in
let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
- let interp = make_interpretation_vars sd.recvars acvars in
+ let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable sd.only_parsing reversibility ac in
let notation = {
@@ -1378,13 +1390,13 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Declare interpretation *)
let path = (Lib.library_dp(), Lib.current_dirpath true) in
let df' = (make_notation_key symbs, (path,df)) in
- let i_vars = make_internalization_vars recvars mainvars i_typs in
+ let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
let nenv = {
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
} in
let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
- let interp = make_interpretation_vars recvars acvars in
+ let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
let onlyparse = is_not_printable onlyparse reversibility ac in
let notation = {
@@ -1517,14 +1529,14 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
let vars,reversibility,pat =
try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
with Not_found ->
- let fold accu id = Id.Map.add id NtnInternTypeConstr accu in
+ let fold accu id = Id.Map.add id NtnInternTypeAny accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
let nenv = {
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
} in
let nvars, pat, reversibility = interp_notation_constr env nenv c in
- let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
+ let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
List.map map vars, reversibility, pat
in
let onlyparse = match onlyparse with
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 12:19:56 +0000