From: Enrico Tassi Date: Mon, 26 Jan 2009 17:11:10 +0000 (+0000) Subject: maction layout added to notation X-Git-Tag: make_still_working~4232 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git maction layout added to notation --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 4d68dadf9..a994c9fd1 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -212,7 +212,10 @@ and pp_layout = function | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2) | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2) | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2) - | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3) + | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) + (pp_term t2) (pp_term t3) + | Ast.Maction l -> sprintf "\\MACTION (%s)" + (String.concat "," (List.map pp_term l)) | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t) | Ast.Root (arg, index) -> sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index cfbd21b3a..3ffa95258 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -122,6 +122,7 @@ and layout_pattern = | InfRule of term * term * term (* | array of term * literal option * literal option |+ column separator, row separator +| *) + | Maction of term list | Sqrt of term | Root of term * term (* argument, index *) | Break diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 1ddd5c9c3..48258d7ba 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -99,6 +99,7 @@ let visit_layout k = function | Ast.Group terms -> Ast.Group (List.map k terms) | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term) | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term) + | Ast.Maction terms -> Ast.Maction (List.map k terms) let visit_magic k = function | Ast.List0 (t, l) -> Ast.List0 (k t, l) diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index bbc901dab..ac3b11422 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -88,7 +88,8 @@ let level1_layouts = [ "sub"; "sup"; "below"; "above"; "over"; "atop"; "frac"; - "sqrt"; "root" + "sqrt"; "root"; "mstyle" ; "mpadded"; "maction" + ] let level1_keywords = @@ -96,7 +97,7 @@ let level1_keywords = "break"; "list0"; "list1"; "sep"; "opt"; - "term"; "ident"; "number"; "mstyle" ; "mpadded" + "term"; "ident"; "number"; ] @ level1_layouts let level2_meta_keywords = @@ -131,9 +132,7 @@ let _ = List.iter (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol) [ ("->", <:unicode>); ("=>", <:unicode>); - ("<=", <:unicode>); (">=", <:unicode>); - ("<>", <:unicode>); (":=", <:unicode>); - ("==", <:unicode>); + (":=", <:unicode>); ] let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 60eb41424..8ddb78781 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -187,6 +187,7 @@ let extract_term_production pattern = | Ast.Group pl -> List.flatten (List.map aux pl) | Ast.Mstyle (_,pl) -> List.flatten (List.map aux pl) | Ast.Mpadded (_,pl) -> List.flatten (List.map aux pl) + | Ast.Maction l -> List.flatten (List.map aux l) and aux_magic magic = match magic with | Ast.Opt p -> @@ -257,7 +258,7 @@ let owned_keywords = ref (initial_owned_keywords ()) type checked_l1_pattern = CL1P of CicNotationPt.term * int -let check_l1_pattern level1_pattern level associativity = +let check_l1_pattern level1_pattern pponly level associativity = let variables = ref 0 in let symbols = ref 0 in let rec aux = function @@ -283,6 +284,10 @@ let check_l1_pattern level1_pattern level associativity = | Ast.Group pl -> Ast.Group (List.map aux pl) | Ast.Mstyle (l,pl) -> Ast.Mstyle (l, List.map aux pl) | Ast.Mpadded (l,pl) -> Ast.Mpadded (l, List.map aux pl) + | Ast.Maction l as t -> + if not pponly then + raise(Parse_error("Maction can be used only in output notations")) + else t and aux_magic magic = match magic with | Ast.Opt p -> Ast.Opt (aux p) @@ -505,6 +510,10 @@ EXTEND return_term_of_level loc (fun l -> Ast.Layout (Ast.Mpadded (m, t l))) + | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] -> + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Maction (List.map (fun x -> + CicNotationUtil.group (x l)) m))) | LPAREN; p = l1_pattern; RPAREN -> return_term_of_level loc (fun l -> CicNotationUtil.group (p l)) ] diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index 433711edd..ba9003e90 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -44,8 +44,8 @@ type rule_id val compare_rule_id : rule_id -> rule_id -> int -val check_l1_pattern: (* level1_pattern *) - CicNotationPt.term -> int -> Gramext.g_assoc -> checked_l1_pattern +val check_l1_pattern: (* level1_pattern, pponly, precedence, assoc *) + CicNotationPt.term -> bool -> int -> Gramext.g_assoc -> checked_l1_pattern val extend: checked_l1_pattern -> diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index c4dd944b4..1a092909e 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -411,6 +411,8 @@ let render ids_to_uris ?(prec=(-1)) = box_of mathonly (A.H, false, false) attrs (aux_children mathonly false xref prec (CicNotationUtil.ungroup terms))) + | A.Maction alternatives -> + toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> let children = aux_children mathonly false xref prec diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml index 2b963e94e..ebc9463ee 100644 --- a/helm/software/components/lexicon/cicNotation.ml +++ b/helm/software/components/lexicon/cicNotation.ml @@ -49,7 +49,8 @@ let process_notation st = match st with | Notation (loc, dir, l1, associativity, precedence, l2) -> let l1 = - CicNotationParser.check_l1_pattern l1 precedence associativity + CicNotationParser.check_l1_pattern + l1 (dir = Some `RightToLeft) precedence associativity in let item = (l1, precedence, associativity, l2) in let rule_id = ref [] in