From: Luca Padovani Date: Thu, 14 Jul 2005 09:19:28 +0000 (+0000) Subject: * added group box (?) X-Git-Tag: pre_notation~12 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7df7f06d2bc2a3fe1fe95aab957cef480d27eb86;p=helm.git * added group box (?) * added break layout and partially implemented --- diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index f4651d637..472389de3 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -166,6 +166,7 @@ let extract_term_production pattern = | 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 -> @@ -353,17 +354,17 @@ EXTEND | 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)) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index e04b00b70..fcb42fd18 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -141,6 +141,8 @@ and pp_layout = function | 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) -> diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index a14ff349d..4b47b9014 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -68,32 +68,33 @@ let genuine_math = 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 ([], ")") @@ -238,39 +239,53 @@ let render ids_to_uris = 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 [] diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 5ad1f0b5b..322ce401b 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -109,6 +109,7 @@ and layout_pattern = | Root of term * term (* argument, index *) | Break | Box of box_spec * term list + | Group of term list and magic_term = (* level 1 magics *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index e72bfacc8..436a40571 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -93,26 +93,29 @@ let pp_ast0 t k = 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 "?" @@ -265,7 +268,7 @@ let set_compiled32 f = compiled32 := Some f 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 -> @@ -296,19 +299,17 @@ let instantiate21 env (* precedence associativity *) l1 = 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 -> diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 1f9d9f5cc..d3a87dfc1 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -152,6 +152,7 @@ let visit_layout k = function | 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) @@ -324,6 +325,28 @@ let boxify = function | [ 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 diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index fd7e12f7f..080bbfa36 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -49,7 +49,11 @@ val ncombine: 'a list list -> 'a list list 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 diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index f8620ecec..493db5958 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -54,7 +54,7 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y). 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.