| Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
| Break -> []
| Box (_, pl) -> List.flatten (List.map aux pl)
+ | Group pl -> List.flatten (List.map aux pl)
and aux_magic magic =
match magic with
| Opt p ->
| SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
return_term loc (Layout (Root (arg, index)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((H, false, false), p)))
| "vbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((V, false, false), p)))
| "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((HV, false, false), p)))
| "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (Layout (Box ((HOV, false, false), p)))
| "break" -> return_term loc (Layout Break)
(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
| LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.boxify p)
+ return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
[ i = IDENT -> return_term loc (Variable (TermVar i))
| Box (box_spec, terms) ->
sprintf "\\%s [%s]" (pp_box_spec box_spec)
(String.concat " " (List.map pp_term terms))
+ | Group terms ->
+ sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms))
and pp_magic = function
| List0 (t, sep_opt) ->
let box_of mathonly spec attrs children =
match children with
- | [t] -> t
- | _ ->
- let kind, spacing, indent = spec in
- let rec dress = function
- | [] -> []
- | [hd] -> [hd]
- | hd :: tl -> hd :: Mpresentation.Mtext ([], " ") :: dress tl
- in
- if mathonly then Mpresentation.Mrow (attrs, dress children)
- else
- let attrs' =
- if spacing then [None, "spacing", "0.5em"] else []
- @ if indent then [None, "indent", "0em 0.5em"] else []
- @ attrs
- in
- match kind with
- | CicNotationPt.H when List.for_all genuine_math children ->
- Mpresentation.Mrow (attrs', children)
- | CicNotationPt.H ->
- mpres_of_box (Box.H (attrs', List.map box_of_mpres children))
- | CicNotationPt.V ->
- mpres_of_box (Box.V (attrs', List.map box_of_mpres children))
- | CicNotationPt.HV ->
- mpres_of_box (Box.HV (attrs', List.map box_of_mpres children))
- | CicNotationPt.HOV ->
- mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children))
+ | [t] -> t
+ | _ ->
+ let kind, spacing, indent = spec in
+ let dress children =
+ if spacing then
+ CicNotationUtil.dress (Mpresentation.Mtext ([], " ")) children
+ else
+ children
+ in
+ if mathonly then Mpresentation.Mrow (attrs, dress children)
+ else
+ let attrs' =
+ (if spacing then [None, "spacing", "0.5em"] else [])
+ @ (if indent then [None, "indent", "0em 0.5em"] else [])
+ @ attrs
+ in
+ match kind with
+ | CicNotationPt.H when List.for_all genuine_math children ->
+ Mpresentation.Mrow (attrs', dress children)
+ | CicNotationPt.H ->
+ mpres_of_box (Box.H (attrs', List.map box_of_mpres children))
+ | CicNotationPt.V ->
+ mpres_of_box (Box.V (attrs', List.map box_of_mpres children))
+ | CicNotationPt.HV ->
+ mpres_of_box (Box.HV (attrs', List.map box_of_mpres children))
+ | CicNotationPt.HOV ->
+ mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children))
let open_paren = Mpresentation.Mo ([], "(")
let closed_paren = Mpresentation.Mo ([], ")")
P.Mfrac (atop_attributes @ attrs, invoke' t1, invoke' t2)
| A.Sqrt t -> P.Msqrt (attrs, invoke' t)
| A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2)
- | A.Box (kind, terms) ->
- let children = aux_children mathonly xref pos prec uris terms in
+ | A.Box ((_, spacing, _) as kind, terms) ->
+ let children = aux_children mathonly spacing xref pos prec uris (CicNotationUtil.ungroup terms) in
box_of mathonly kind attrs children
+ | A.Group terms ->
+ let children = aux_children false mathonly xref pos prec uris (CicNotationUtil.ungroup terms) in
+ box_of mathonly (A.H, false, false) attrs children
| A.Break -> assert false (* TODO? *)
- and aux_children mathonly xref pos prec uris terms =
- let rec aux_list first =
+ and aux_children mathonly spacing xref pos prec uris terms =
+ let find_clusters =
+ let rec aux_list first clusters acc =
+ function
+ [] when acc = [] -> List.rev clusters
+ | [] -> aux_list first (List.rev acc :: clusters) [] []
+ | (A.Layout A.Break) :: tl when acc = [] -> aux_list first clusters [] tl
+ | (A.Layout A.Break) :: tl -> aux_list first (List.rev acc :: clusters) [] tl
+ | [hd] ->
+ let pos' =
+ if first then
+ pos
+ else
+ match pos with
+ `None -> `Right
+ | `Inner -> `Inner
+ | `Right -> `Right
+ | `Left -> `Inner
+ in
+ aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) []
+ | hd :: tl ->
+ let pos' =
+ match pos, first with
+ `None, true -> `Left
+ | `None, false -> `Inner
+ | `Left, true -> `Left
+ | `Left, false -> `Inner
+ | `Right, _ -> `Inner
+ | `Inner, _ -> `Inner
+ in
+ aux_list false clusters (aux [] mathonly xref pos' prec uris hd :: acc) tl
+ in
+ aux_list true [] []
+ in
+ let boxify_pres =
function
- [] -> []
- | [t] ->
- assert (not first);
- let pos' =
- match pos with
- `None -> `Right
- | `Inner -> `Inner
- | `Right -> `Right
- | `Left -> `Inner
- in
- [aux [] mathonly xref pos' prec uris t]
- | t :: tl ->
- let pos' =
- match pos, first with
- `None, true -> `Left
- | `None, false -> `Inner
- | `Left, true -> `Left
- | `Left, false -> `Inner
- | `Right, _ -> `Inner
- | `Inner, _ -> `Inner
- in
- (aux [] mathonly xref pos' prec uris t) :: aux_list false tl
+ [t] -> t
+ | tl -> box_of mathonly (A.H, spacing, false) [] tl
in
- match terms with
- | [t] -> [aux [] mathonly xref pos prec uris t]
- | tl -> aux_list true tl
+ List.map boxify_pres (find_clusters terms)
in
aux [] false None `None 0 []
| Root of term * term (* argument, index *)
| Break
| Box of box_spec * term list
+ | Group of term list
and magic_term =
(* level 1 magics *)
let rec aux = function
| Ast.Appl ts ->
Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
- Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts)))
+ Ast.Layout
+ (Ast.Box ((Ast.HOV, true, true),
+ (CicNotationUtil.dress
+ (Ast.Layout Ast.Break)
+ (List.map k ts)))))
| Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
| Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
aux_ty ty;
- Ast.Layout (Ast.Box ((Ast.H, false, false), [
- binder_symbol "\\to";
- k body]))])))
+ Ast.Layout Ast.Break;
+ binder_symbol "\\to";
+ k body])))
| Ast.Binder (binder_kind, (id, ty), body) ->
Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
- Ast.Layout (Ast.Box ((Ast.H, false, false), [
- binder_symbol (resolve_binder binder_kind);
- k id;
- builtin_symbol ":";
- aux_ty ty ]));
- Ast.Layout (Ast.Box ((Ast.H, false, false), [
- builtin_symbol ".";
- k body ]))])))
+ binder_symbol (resolve_binder binder_kind);
+ k id;
+ builtin_symbol ":";
+ aux_ty ty;
+ Ast.Layout Ast.Break;
+ builtin_symbol ".";
+ k body ])))
| t -> CicNotationUtil.visit_ast ~special_k k t
and aux_ty = function
| None -> builtin_symbol "?"
let instantiate21 env (* precedence associativity *) l1 =
let rec subst_singleton env t =
- CicNotationUtil.boxify (subst env t)
+ CicNotationUtil.group (subst env t)
and subst env = function
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
let values = CicNotationUtil.ncombine rec_values in
let sep =
match sep_opt with
- | None -> []
- | Some l -> [ CicNotationPt.Literal l ]
- in
+ | None -> []
+ | Some l -> [ CicNotationPt.Literal l ]
+ in
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list
- ((CicNotationUtil.boxify (subst env p)) :: acc) []
+ instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list
- ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
+ instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
in
instantiate_list [] values
| Ast.Opt p ->
| Root (arg, index) -> Root (k arg, k index)
| Break -> Break
| Box (kind, terms) -> Box (kind, List.map k terms)
+ | Group terms -> Group (List.map k terms)
let visit_magic k = function
| List0 (t, l) -> List0 (k t, l)
| [ a ] -> a
| l -> Layout (Box ((H, false, false), l))
+let group = function
+ | [ a ] -> a
+ | l -> Layout (Group l)
+
+let ungroup =
+ let rec aux acc =
+ function
+ [] -> List.rev acc
+ | Layout (Group terms) :: terms' -> aux acc (terms @ terms')
+ | term :: terms -> aux (term :: acc) terms
+ in
+ aux []
+
+let dress sauce =
+ let rec aux =
+ function
+ | [] -> []
+ | [hd] -> [hd]
+ | hd :: tl -> hd :: sauce :: aux tl
+ in
+ aux
+
let find_appl_pattern_uris ap =
let rec aux acc =
function
val string_of_literal: CicNotationPt.literal -> string
+val dress: 'a -> 'a list -> 'a list
+
val boxify: CicNotationPt.term list -> CicNotationPt.term
+val group: CicNotationPt.term list -> CicNotationPt.term
+val ungroup: CicNotationPt.term list -> CicNotationPt.term list
val find_appl_pattern_uris:
CicNotationPt.cic_appl_pattern -> UriManager.uri list
render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
notation
- "'if' a 'then' b 'else' c"
+ "hvbox ('if' a 'then' break b break 'else' break c)"
for
@{ 'ifthenelse $a $b $c }.
print if even then \forall x:nat.x else bump x.
projects / helm.git / commitdiff