From 68f3812e06c04ddd664e86dbfd3a1c32f96a22d1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Jun 2008 13:49:50 +0000 Subject: [PATCH] notation support fixed to parentesize in a more sane way and andded two windows: 1) tex/utf8 table 2) terms grammar --- .../components/acic_content/cicNotationEnv.ml | 4 +- .../acic_content/cicNotationEnv.mli | 2 +- .../components/acic_content/cicNotationPp.ml | 7 +- .../components/acic_content/cicNotationPt.ml | 6 +- helm/software/components/content_pres/.depend | 15 +- .../software/components/content_pres/Makefile | 2 +- .../software/components/content_pres/boxPp.ml | 4 +- .../content_pres/cicNotationParser.ml | 160 +++++---- .../content_pres/cicNotationParser.mli | 5 +- .../content_pres/cicNotationPres.ml | 35 +- .../content_pres/content2presMatcher.ml | 4 +- .../content_pres/termContentPres.ml | 14 +- .../components/grafite_parser/.depend | 2 + .../components/grafite_parser/.depend.opt | 2 + .../components/grafite_parser/Makefile | 3 +- .../grafite_parser/grafiteParser.ml | 4 +- .../grafite_parser/print_grammar.ml | 304 ++++++++---------- .../components/syntax_extensions/utf8Macro.ml | 25 +- .../syntax_extensions/utf8Macro.mli | 4 +- .../syntax_extensions/utf8MacroTable.ml | 2 +- helm/software/matita/matita.glade | 16 + helm/software/matita/matitaGui.ml | 27 ++ 22 files changed, 365 insertions(+), 282 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationEnv.ml b/helm/software/components/acic_content/cicNotationEnv.ml index f0a14846f..5b4190eb8 100644 --- a/helm/software/components/acic_content/cicNotationEnv.ml +++ b/helm/software/components/acic_content/cicNotationEnv.ml @@ -35,7 +35,7 @@ type value = | ListValue of value list type value_type = - | TermType of int option + | TermType of int | StringType | NumType | OptType of value_type @@ -98,7 +98,7 @@ let list_declaration (n, ty) = (n, ListType ty) let declaration_of_var = function | Ast.NumVar s -> s, NumType | Ast.IdentVar s -> s, StringType - | Ast.TermVar (s,l) -> s, TermType l + | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l | _ -> assert false let value_of_term = function diff --git a/helm/software/components/acic_content/cicNotationEnv.mli b/helm/software/components/acic_content/cicNotationEnv.mli index c332bcfff..aa937d00c 100644 --- a/helm/software/components/acic_content/cicNotationEnv.mli +++ b/helm/software/components/acic_content/cicNotationEnv.mli @@ -33,7 +33,7 @@ type value = | ListValue of value list type value_type = - | TermType of int option + | TermType of int (* the level of the expected term *) | StringType | NumType | OptType of value_type diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 4f94fa742..a0f9dc2f1 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -250,8 +250,8 @@ and pp_sep_opt = function and pp_variable = function | Ast.NumVar s -> "number " ^ s | Ast.IdentVar s -> "ident " ^ s - | Ast.TermVar (s,None) -> s - | Ast.TermVar (s,Some l) -> "term " ^string_of_int l + | Ast.TermVar (s,Ast.Self _) -> s + | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l | Ast.Ascription (t, n) -> assert false | Ast.FreshVar n -> "fresh " ^ n @@ -328,8 +328,7 @@ let rec pp_value = function let rec pp_value_type = function - | Env.TermType None -> "Term" - | Env.TermType (Some l) -> "Term "^string_of_int l + | Env.TermType l -> "Term "^string_of_int l | Env.StringType -> "String" | Env.NumType -> "Number" | Env.OptType t -> "Maybe " ^ pp_value_type t diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 1ca514810..7e06fa5e8 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 3 +let magic = 4 type term = (* CIC AST *) @@ -140,11 +140,13 @@ and magic_term = | Fail | If of term * term * term (* test, pattern if true, pattern if false *) +and term_level = Self of int | Level of int + and pattern_variable = (* level 1 and 2 variables *) | NumVar of string | IdentVar of string - | TermVar of string * int option + | TermVar of string * term_level (* level 1 variables *) | Ascription of term * string diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 2c5d65140..5ab78a89e 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -1,5 +1,6 @@ -cicNotationPres.cmi: mpresentation.cmi box.cmi +termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi +cicNotationPres.cmi: mpresentation.cmi box.cmi content2pres.cmi: cicNotationPres.cmi sequent2pres.cmi: cicNotationPres.cmi renderingAttrs.cmo: renderingAttrs.cmi @@ -15,17 +16,17 @@ box.cmx: renderingAttrs.cmx box.cmi content2presMatcher.cmo: content2presMatcher.cmi content2presMatcher.cmx: content2presMatcher.cmi termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \ - termContentPres.cmi + cicNotationParser.cmi termContentPres.cmi termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \ - termContentPres.cmi -cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \ - cicNotationPres.cmi -cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \ - cicNotationPres.cmi + cicNotationParser.cmx termContentPres.cmi boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ boxPp.cmi boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ boxPp.cmi +cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi boxPp.cmi box.cmi \ + cicNotationPres.cmi +cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx boxPp.cmx box.cmx \ + cicNotationPres.cmi content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ diff --git a/helm/software/components/content_pres/Makefile b/helm/software/components/content_pres/Makefile index 2eadef187..7501004fb 100644 --- a/helm/software/components/content_pres/Makefile +++ b/helm/software/components/content_pres/Makefile @@ -9,8 +9,8 @@ INTERFACE_FILES = \ box.mli \ content2presMatcher.mli \ termContentPres.mli \ - cicNotationPres.mli \ boxPp.mli \ + cicNotationPres.mli \ content2pres.mli \ sequent2pres.mli \ $(NULL) diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml index 0c1847548..a51920c79 100644 --- a/helm/software/components/content_pres/boxPp.ml +++ b/helm/software/components/content_pres/boxPp.ml @@ -198,8 +198,8 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = s else match Utf8Macro.tex_of_unicode s with - | Some s -> s ^ " " - | None -> " " ^ s ^ " " + | s::_ -> s ^ " " + | [] -> " " ^ s ^ " " end else s in diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 2d03762ae..8940c6614 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -60,16 +60,17 @@ let int_of_string s = let level_of precedence = if precedence < min_precedence || precedence > max_precedence then raise (Level_not_found precedence); - string_of_int precedence ^ "N" + string_of_int precedence let gram_symbol s = Gramext.Stoken ("SYMBOL", s) let gram_ident s = Gramext.Stoken ("IDENT", s) let gram_number s = Gramext.Stoken ("NUMBER", s) let gram_keyword s = Gramext.Stoken ("", s) let gram_term = function - | None -> Gramext.Sself - | Some (precedence) -> - Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence) + | Ast.Self _ -> Gramext.Sself + | Ast.Level precedence -> + Gramext.Snterml + (Grammar.Entry.obj (term: 'a Grammar.Entry.e), level_of precedence) ;; let gram_of_literal = @@ -193,8 +194,8 @@ let extract_term_production pattern = and aux_variable = function | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""] - | Ast.TermVar (s,level) -> - [Binding (s, Env.TermType level), gram_term level] + | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) -> + [Binding (s, Env.TermType level), gram_term lv] | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""] | Ast.Ascription (p, s) -> assert false (* TODO *) | Ast.FreshVar _ -> assert false @@ -224,7 +225,7 @@ let check_l1_pattern level1_pattern level associativity = | Ast.Literal _ as l -> incr symbols; l | Ast.Layout l -> Ast.Layout (aux_layout l) | Ast.Magic m -> Ast.Magic (aux_magic m) - | Ast.Variable v -> Ast.Variable (aux_variable v) + | Ast.Variable v -> (aux_variable v) | t -> assert false and aux_layout = function | Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2) @@ -247,39 +248,43 @@ let check_l1_pattern level1_pattern level associativity = | _ -> assert false and aux_variable = function - | Ast.NumVar _ as t -> t - | Ast.TermVar (s,None) when associativity <> Gramext.NonA -> + | Ast.NumVar _ as t -> Ast.Variable t + | Ast.TermVar (s,Ast.Self _) when associativity <> Gramext.NonA -> incr variables; if !variables > 2 then raise (Parse_error ("Exactly 2 variables must be specified in an "^ "associative notation")); (match !variables, associativity with - | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some - (level-1)) *) - | 1,Gramext.RightA -> Ast.TermVar (s, None) - | 2,Gramext.LeftA ->Ast.TermVar (s, None) - | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1)) + | 1,Gramext.LeftA -> + Ast.Variable (Ast.TermVar (s, Ast.Self level)) + | 1,Gramext.RightA -> + Ast.Variable (Ast.TermVar (s, Ast.Self (level+1))) + | 2,Gramext.LeftA -> + Ast.Variable (Ast.TermVar (s, Ast.Self (level+1))) + | 2,Gramext.RightA -> + Ast.Variable (Ast.TermVar (s, Ast.Level (level-1))) | _ -> assert false) - | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA -> + | Ast.TermVar (s,Ast.Level _) when associativity <> Gramext.NonA -> raise (Parse_error ("Variables can not be declared with a " ^ "precedence in an associative notation")) - (* avoid camlp5 divergence due to non-Sself recursion at the same level *) - | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 -> - raise (Parse_error ("Left recursive rule with precedence not greater " ^ - "than " ^ string_of_int level ^ " is not allowed to avoid divergence")) - | Ast.TermVar _ as t -> incr variables; t - | Ast.IdentVar _ as t -> t + (*avoid camlp5 divergence due to non-Sself recursion at the same level *) + | Ast.TermVar (s,Ast.Level l) when l<=level && !variables=0 && !symbols=0-> + raise(Parse_error("Left recursive rule with precedence not greater " ^ + "than " ^ string_of_int level ^ " is not allowed to avoid divergence")) + | Ast.TermVar _ as t -> incr variables; Ast.Variable t + | Ast.IdentVar _ as t -> Ast.Variable t | Ast.Ascription _ -> assert false (* TODO *) | Ast.FreshVar _ -> assert false in if associativity <> Gramext.NonA && level = min_precedence then raise (Parse_error ("You can not specify an associative notation " ^ "at level "^string_of_int min_precedence ^ "; increase it")); - let cp = CL1P (aux level1_pattern, level) in + let cp = aux level1_pattern in +(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *) if !variables <> 2 && associativity <> Gramext.NonA then raise (Parse_error ("Exactly 2 variables must be specified in an "^ "associative notation")); - cp + CL1P (cp,level) ;; let extend (CL1P (level1_pattern,precedence)) action = @@ -315,7 +320,7 @@ let delete rule_id = (** {2 Grammar} *) -let parse_level1_pattern_ref = ref (fun _ -> assert false) +let parse_level1_pattern_ref = ref (fun _ _ -> assert false) let parse_level2_ast_ref = ref (fun _ -> assert false) let parse_level2_meta_ref = ref (fun _ -> assert false) @@ -337,6 +342,8 @@ let fold_binder binder pt_names body = pt_names body let return_term loc term = Ast.AttributedTerm (`Loc loc, term) +let return_term_of_level loc term l = + Ast.AttributedTerm (`Loc loc, term l) (* create empty precedence level for "term" *) let _ = @@ -352,7 +359,7 @@ let _ = | i when i < first -> acc | i -> aux - ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod) + ((Some (level_of i), Some Gramext.NonA, dummy_prod) :: acc) (i - 1) in @@ -367,8 +374,13 @@ let _ = EXTEND GLOBAL: level1_pattern; - level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ]; - l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ]; + level1_pattern: [ + [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ] + ]; + l1_pattern: [ + [ p = LIST1 l1_simple_pattern -> + fun l -> List.map (fun x -> x l) p ] + ]; literal: [ [ s = SYMBOL -> `Symbol s | k = QKEYWORD -> `Keyword k @@ -376,17 +388,17 @@ EXTEND ] ]; sep: [ [ "sep"; sep = literal -> sep ] ]; -(* row_sep: [ [ "rowsep"; sep = literal -> sep ] ]; - field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *) l1_magic_pattern: [ - [ "list0"; p = l1_simple_pattern; sep = OPT sep -> Ast.List0 (p, sep) - | "list1"; p = l1_simple_pattern; sep = OPT sep -> Ast.List1 (p, sep) - | "opt"; p = l1_simple_pattern -> Ast.Opt p + [ "list0"; p = l1_simple_pattern; sep = OPT sep -> + fun l -> Ast.List0 (p l, sep) + | "list1"; p = l1_simple_pattern; sep = OPT sep -> + fun l -> Ast.List1 (p l, sep) + | "opt"; p = l1_simple_pattern -> fun l -> Ast.Opt (p l) ] ]; l1_pattern_variable: [ [ "term"; precedence = NUMBER; id = IDENT -> - Ast.TermVar (id, Some (int_of_string precedence)) + Ast.TermVar (id, Ast.Level (int_of_string precedence)) | "number"; id = IDENT -> Ast.NumVar id | "ident"; id = IDENT -> Ast.IdentVar id ] @@ -394,42 +406,56 @@ EXTEND l1_simple_pattern: [ "layout" LEFTA [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Sub (p1, p2))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l))) | p1 = SELF; SYMBOL "\\sup"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Sup (p1, p2))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l))) | p1 = SELF; SYMBOL "\\below"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Below (p1, p2))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l))) | p1 = SELF; SYMBOL "\\above"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Above (p1, p2))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l))) | p1 = SELF; SYMBOL "\\over"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Over (p1, p2))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l))) | p1 = SELF; SYMBOL "\\atop"; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Atop (p1, p2))) -(* | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep -> - return_term loc (Array (p, csep, rsep)) *) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l))) | SYMBOL "\\frac"; p1 = SELF; p2 = SELF -> - return_term loc (Ast.Layout (Ast.Frac (p1, p2))) - | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Ast.Layout (Ast.Sqrt p)) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l))) + | SYMBOL "\\sqrt"; p = SELF -> + return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l)) | SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF -> - return_term loc (Ast.Layout (Ast.Root (arg, index))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Root (arg l, index l))) | "hbox"; LPAREN; p = l1_pattern; RPAREN -> - return_term loc (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Box ((Ast.H, false, false), p l))) | "vbox"; LPAREN; p = l1_pattern; RPAREN -> - return_term loc (Ast.Layout (Ast.Box ((Ast.V, false, false), p))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Box ((Ast.V, false, false), p l))) | "hvbox"; LPAREN; p = l1_pattern; RPAREN -> - return_term loc (Ast.Layout (Ast.Box ((Ast.HV, false, false), p))) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Box ((Ast.HV, false, false), p l))) | "hovbox"; LPAREN; p = l1_pattern; RPAREN -> - return_term loc (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p))) - | "break" -> return_term loc (Ast.Layout Ast.Break) -(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *) + return_term_of_level loc + (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l))) + | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break) | LPAREN; p = l1_pattern; RPAREN -> - return_term loc (CicNotationUtil.group p) + return_term_of_level loc (fun l -> CicNotationUtil.group (p l)) ] | "simple" NONA - [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None))) - | m = l1_magic_pattern -> return_term loc (Ast.Magic m) - | v = l1_pattern_variable -> return_term loc (Ast.Variable v) - | l = literal -> return_term loc (Ast.Literal l) + [ i = IDENT -> + return_term_of_level loc + (fun l -> Ast.Variable (Ast.TermVar (i,Ast.Self l))) + | m = l1_magic_pattern -> + return_term_of_level loc (fun l -> Ast.Magic (m l)) + | v = l1_pattern_variable -> + return_term_of_level loc (fun _ -> Ast.Variable v) + | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l) ] ]; END @@ -440,12 +466,12 @@ EXTEND GLOBAL: level2_meta; l2_variable: [ [ "term"; precedence = NUMBER; id = IDENT -> - Ast.TermVar (id,Some (int_of_string precedence)) + Ast.TermVar (id,Ast.Level (int_of_string precedence)) | "number"; id = IDENT -> Ast.NumVar id | "ident"; id = IDENT -> Ast.IdentVar id | "fresh"; id = IDENT -> Ast.FreshVar id - | "anonymous" -> Ast.TermVar ("_",None) - | id = IDENT -> Ast.TermVar (id,None) + | "anonymous" -> Ast.TermVar ("_",Ast.Self 0) (* is the level relevant?*) + | id = IDENT -> Ast.TermVar (id,Ast.Self 0) ] ]; l2_magic: [ @@ -601,7 +627,7 @@ EXTEND | vars = protected_binder_vars -> vars ] ]; - term: LEVEL "10N" + term: LEVEL "10" [ [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> @@ -614,18 +640,18 @@ EXTEND return_term loc (Ast.LetRec (`Inductive, defs, body)) ] ]; - term: LEVEL "20N" + term: LEVEL "20" [ - [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" -> + [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" -> return_term loc (fold_cluster b vars typ body) | SYMBOL <:unicode> (* ∃ *); - (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"-> + (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19"-> return_term loc (fold_exists vars typ body) ] ]; - term: LEVEL "70N" + term: LEVEL "70" [ - [ p1 = term; p2 = term LEVEL "71N" -> + [ p1 = term; p2 = term LEVEL "71" -> let rec aux = function | Ast.Appl (hd :: tl) | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) -> @@ -635,7 +661,7 @@ EXTEND return_term loc (Ast.Appl (aux p1 @ [p2])) ] ]; - term: LEVEL "90N" + term: LEVEL "90" [ [ id = IDENT -> return_term loc (Ast.Ident (id, None)) | id = IDENT; s = explicit_subst -> @@ -681,9 +707,9 @@ let exc_located_wrapper f = | Stdpp.Exc_located (floc, exn) -> raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) -let parse_level1_pattern lexbuf = +let parse_level1_pattern precedence lexbuf = exc_located_wrapper - (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf)) + (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf) precedence) let parse_level2_ast lexbuf = exc_located_wrapper diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index 161c9167c..0df3f83d0 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -30,8 +30,9 @@ type checked_l1_pattern = private CL1P of CicNotationPt.term * int (** {2 Parsing functions} *) - (** concrete syntax pattern: notation level 1 *) -val parse_level1_pattern: Ulexing.lexbuf -> CicNotationPt.term + (** concrete syntax pattern: notation level 1, the + * integer is the precedence *) +val parse_level1_pattern: int -> Ulexing.lexbuf -> CicNotationPt.term (** AST pattern: notation level 2 *) val parse_level2_ast: Ulexing.lexbuf -> CicNotationPt.term diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 175aae993..728651acc 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -182,22 +182,23 @@ let is_atomic t = aux_mpres t let add_parens child_prec curr_prec t = -(* eprintf - ("add_parens: " ^^ - "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!") - child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos) - curr_prec; *) - if is_atomic t then t -(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *) - else if child_prec >= 0 && child_prec <= curr_prec then - begin (* parens should be added *) -(* prerr_endline "adding parens!"; *) + if is_atomic t then + ((*prerr_endline ("NOT adding parens around ATOMIC: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*)t) + else if child_prec >= 0 && child_prec < curr_prec then + begin + (*prerr_endline ("adding parens around: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*) match t with | Mpresentation.Mobject (_, box) -> mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren]) end else - t + ((*prerr_endline ("NOT adding parens around: "^ + BoxPp.render_to_string (function x::_->x|_->assert false) + ~map_unicode_to_tex:false 80 t);*)t) let render ids_to_uris ?(prec=(-1)) = let module A = Ast in @@ -322,7 +323,6 @@ let render ids_to_uris ?(prec=(-1)) = let expected_level = ref None in let new_xref = ref [] in let new_xmlattrs = ref [] in -(* let reinit = ref false in *) let rec aux_attribute = function | A.AttributedTerm (attr, t) -> @@ -346,12 +346,17 @@ let render ids_to_uris ?(prec=(-1)) = (match !inferred_level with | None -> aux !new_xmlattrs mathonly new_xref prec t | Some child_prec -> - let t' = - aux !new_xmlattrs mathonly new_xref child_prec t in + let t' = aux !new_xmlattrs mathonly new_xref child_prec t in + (*prerr_endline + ("inferred: "^string_of_int child_prec^ + " exp: "^string_of_int prec ^ + " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false + (function x::_->x|_->assert false) 80 t');*) if !reset - then t' + then ((*prerr_endline "reset";*)t') else add_parens child_prec prec t') in +(* prerr_endline (CicNotationPp.pp_term t); *) aux_attribute t and aux_literal xmlattrs xref prec l = let attrs = make_href xmlattrs xref in diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml index bcb4257bf..3c6a61a6f 100644 --- a/helm/software/components/content_pres/content2presMatcher.ml +++ b/helm/software/components/content_pres/content2presMatcher.ml @@ -73,7 +73,7 @@ struct let add_magic m = let name = Util.fresh_name () in magic_map := (name, m) :: !magic_map; - Ast.Variable (Ast.TermVar (name,None)) + Ast.Variable (Ast.TermVar (name,Ast.Level 0)) in let rec aux = function | Ast.AttributedTerm (_, t) -> assert false @@ -91,7 +91,7 @@ struct List.map2 (fun p t -> match p, t with - | Ast.Variable (Ast.TermVar (name,l)), _ -> + | Ast.Variable (Ast.TermVar (name,(Ast.Self l|Ast.Level l))), _ -> name, (Env.TermType l, Env.TermValue t) | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) -> name, (Env.NumType, Env.NumValue s) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 85edd595c..691d4426d 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -323,8 +323,7 @@ let instantiate21 idrefs env l1 = let value = CicNotationEnv.term_of_value value in let value = match expected_ty with - | Env.TermType (Some l) -> - Ast.AttributedTerm (`Level l,value) + | Env.TermType l -> Ast.AttributedTerm (`Level l,value) | _ -> value in [ value ] @@ -532,6 +531,7 @@ let tail_names names env = aux [] env let instantiate_level2 env term = +(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = try @@ -544,7 +544,7 @@ let instantiate_level2 env term = let rec aux env term = (* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *) match term with - | Ast.AttributedTerm (_, term) -> aux env term + | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) | Ast.Binder (binder, var, body) -> Ast.Binder (binder, aux_capture_var env var, aux env body) @@ -593,9 +593,7 @@ let instantiate_level2 env term = and aux_variable env = function | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0) | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None) - | Ast.TermVar (name,None) -> - Env.lookup_term env name - | Ast.TermVar (name,Some l) -> + | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> Ast.AttributedTerm (`Level l,Env.lookup_term env name) | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None) | Ast.Ascription (term, name) -> assert false @@ -637,7 +635,7 @@ let instantiate_level2 env term = | Env.ListValue (_ :: _) -> instantiate_fold_left (let acc_binding = - acc_name, (Env.TermType None, Env.TermValue acc) + acc_name, (Env.TermType 0, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern) (tail_names names env') @@ -659,7 +657,7 @@ let instantiate_level2 env term = | Env.ListValue (_ :: _) -> let acc = instantiate_fold_right (tail_names names env') in let acc_binding = - acc_name, (Env.TermType None, Env.TermValue acc) + acc_name, (Env.TermType 0, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern | Env.ListValue [] -> aux env base_pattern diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index f097cc8d3..bc5bede45 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -11,3 +11,5 @@ grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi +print_grammar.cmo: print_grammar.cmi +print_grammar.cmx: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index f097cc8d3..bc5bede45 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -11,3 +11,5 @@ grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi +print_grammar.cmo: print_grammar.cmi +print_grammar.cmx: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/Makefile b/helm/software/components/grafite_parser/Makefile index eb2f1b1eb..3df8517a9 100644 --- a/helm/software/components/grafite_parser/Makefile +++ b/helm/software/components/grafite_parser/Makefile @@ -8,10 +8,11 @@ INTERFACE_FILES = \ grafiteDisambiguator.mli \ grafiteDisambiguate.mli \ grafiteWalker.mli \ + print_grammar.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -all: test_parser print_grammar test_dep +all: test_parser test_dep clean: clean_tests # cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 20aad1cd3..7b119ab11 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -95,7 +95,7 @@ type by_continuation = EXTEND GLOBAL: term statement; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; - tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; + tactic_term: [ [ t = term LEVEL "90" -> t ] ]; new_name: [ [ id = IDENT -> Some id | SYMBOL "_" -> None ] @@ -593,7 +593,7 @@ EXTEND in let p1 = add_raw_attribute ~text:s - (CicNotationParser.parse_level1_pattern + (CicNotationParser.parse_level1_pattern prec (Ulexing.from_utf8_string s)) in (dir, p1, assoc, prec, p2) diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml index f05b77a11..d2eb817ad 100644 --- a/helm/software/components/grafite_parser/print_grammar.ml +++ b/helm/software/components/grafite_parser/print_grammar.ml @@ -27,16 +27,75 @@ open Gramext -let tex_of_unicode s = -(*CSC: ??????? What's the meaning of this function? - let contractions = ("\\Longrightarrow","=>") :: [] in - if String.length s <= 1 then s - else (* probably an extended unicode symbol *) - let s = Utf8Macro.tex_of_unicode s in - try List.assoc s contractions with Not_found -> s -*) match Utf8Macro.tex_of_unicode s with - Some s -> s - | None -> s +let rec flatten_tree = function + | DeadEnd -> [] + | LocAct _ -> [[]] + | Node {node = n; brother = b; son = s} -> + List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b + +let tex_of_unicode s = s + +let rec clean_dummy_desc = function + | Dlevels l -> Dlevels (clean_levels l) + | x -> x + +and clean_levels = function + | [] -> [] + | l :: tl -> clean_level l @ clean_levels tl + +and clean_level = function + | x -> + let pref = clean_tree x.lprefix in + let suff = clean_tree x.lsuffix in + match pref,suff with + | DeadEnd, DeadEnd -> [] + | _ -> [{x with lprefix = pref; lsuffix = suff}] + +and clean_tree = function + | Node n -> clean_node n + | x -> x + +and clean_node = function + | {node=node;son=son;brother=brother} -> + let bn = is_symbol_dummy node in + let bs = is_tree_dummy son in + let bb = is_tree_dummy brother in + let son = if bs then DeadEnd else son in + let brother = if bb then DeadEnd else brother in + if bb && bs && bn then + DeadEnd + else + if bn then + Node {node=Sself;son=son;brother=brother} + else + Node {node=node;son=son;brother=brother} + +and is_level_dummy = function + | {lsuffix=lsuffix;lprefix=lprefix} -> + is_tree_dummy lsuffix && is_tree_dummy lprefix + +and is_desc_dummy = function + | Dlevels l -> List.for_all is_level_dummy l + | Dparser _ -> true + +and is_entry_dummy = function + | {edesc=edesc} -> is_desc_dummy edesc + +and is_symbol_dummy = function + | Stoken ("DUMMY", _) -> true + | Stoken _ -> false + | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt + | Snterm e | Snterml (e, _) -> is_entry_dummy e + | Slist1 x | Slist0 x -> is_symbol_dummy x + | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself | Snext -> false + | Stree t -> is_tree_dummy t + | _ -> assert false + +and is_tree_dummy = function + | Node {node=node} -> is_symbol_dummy node + | _ -> true let needs_brackets t = let rec count_brothers = function @@ -46,13 +105,13 @@ let needs_brackets t = count_brothers t > 1 let visit_description desc fmt self = - let skip s = List.mem s [ ] in + let skip s = true in let inline s = List.mem s [ "int" ] in - let rec visit_entry e todo is_son nesting = + let rec visit_entry e todo is_son = let { ename = ename; edesc = desc } = e in if inline ename then - visit_desc desc todo is_son nesting + visit_desc desc todo is_son else begin Format.fprintf fmt "%s " ename; @@ -62,105 +121,93 @@ let visit_description desc fmt self = todo @ [e] end - and visit_desc d todo is_son nesting = + and visit_desc d todo is_son = match d with - | Dlevels [] -> todo - | Dlevels [lev] -> visit_level lev todo is_son nesting - | Dlevels (lev::levels) -> - let todo = visit_level lev todo is_son nesting in + | Dlevels l -> List.fold_left - (fun acc l -> - Format.fprintf fmt "@ | "; - visit_level l acc is_son nesting) - todo levels; - | _ -> todo + (fun acc l -> + Format.fprintf fmt "@ "; + visit_level l acc is_son ) + todo l; + | Dparser _ -> todo - and visit_level l todo is_son nesting = - let { lsuffix = suff ; lprefix = pref } = l in - let todo = visit_tree suff todo is_son nesting in - visit_tree pref todo is_son nesting + and visit_level l todo is_son = + let { lname = name ; lsuffix = suff ; lprefix = pref } = l in + visit_tree name + (List.map + (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref) + todo is_son - and visit_tree t todo is_son nesting = - match t with - | Node node -> visit_node node todo is_son nesting - | _ -> todo - - and visit_node n todo is_son nesting = - let is_tree_printable t = - match t with - | Node _ -> true - | _ -> false - in - let { node = symbol; son = son ; brother = brother } = n in - let todo = visit_symbol symbol todo is_son nesting in - let todo = - if is_tree_printable son then - begin - let need_b = needs_brackets son in - if not is_son then - Format.fprintf fmt "@["; - if need_b then - Format.fprintf fmt "( "; - let todo = visit_tree son todo true nesting in - if need_b then - Format.fprintf fmt ")"; - if not is_son then - Format.fprintf fmt "@]"; - todo - end - else - todo + and visit_tree name t todo is_son = + if List.for_all (List.for_all is_symbol_dummy) t then todo else ( + Format.fprintf fmt "@["; + (match name with + |Some name -> Format.fprintf fmt "Precedence %s:@ " name + | None -> ()); + Format.fprintf fmt "@["; + let todo = + List.fold_left + (fun acc x -> + if List.for_all is_symbol_dummy x then todo else ( + Format.fprintf fmt "@[ | "; + let todo = + List.fold_left + (fun acc x -> + let todo = visit_symbol x acc true in + Format.fprintf fmt "@ "; + todo) + acc x + in + Format.fprintf fmt "@]@ "; + todo)) + todo t in - if is_tree_printable brother then - begin - Format.fprintf fmt "@ | "; - visit_tree brother todo is_son nesting - end - else - todo + Format.fprintf fmt "@]"; + Format.fprintf fmt "@]"; + todo) - and visit_symbol s todo is_son nesting = + and visit_symbol s todo is_son = match s with | Smeta (name, sl, _) -> Format.fprintf fmt "%s " name; List.fold_left ( fun acc s -> - let todo = visit_symbol s acc is_son nesting in + let todo = visit_symbol s acc is_son in if is_son then Format.fprintf fmt "@ "; todo) todo sl - | Snterm entry -> visit_entry entry todo is_son nesting - | Snterml (entry,_) -> visit_entry entry todo is_son nesting + | Snterm entry -> visit_entry entry todo is_son + | Snterml (entry,_) -> visit_entry entry todo is_son | Slist0 symbol -> Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting+1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo | Slist0sep (symbol,sep) -> Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son (nesting + 2) in + let todo = visit_symbol sep todo is_son in Format.fprintf fmt " "; - let todo = visit_symbol symbol todo is_son (nesting + 2) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @]] @ "; todo | Slist1 symbol -> Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]}+ @ "; todo | Slist1sep (symbol,sep) -> - let todo = visit_symbol symbol todo is_son nesting in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son (nesting + 1) in - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol sep todo is_son in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo | Sopt symbol -> Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]] @ "; todo | Sself -> Format.fprintf fmt "%s " self; todo @@ -168,89 +215,20 @@ let visit_description desc fmt self = | Stoken pattern -> let constructor, keyword = pattern in if keyword = "" then - Format.fprintf fmt "`%s' " constructor + (if constructor <> "DUMMY" then + Format.fprintf fmt "`%s' " constructor) else - Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); + Format.fprintf fmt "%s " (tex_of_unicode keyword); todo | Stree tree -> - if needs_brackets tree then - begin - Format.fprintf fmt "@[( "; - let todo = visit_tree tree todo is_son (nesting + 1) in - Format.fprintf fmt ")@] @ "; - todo - end - else - visit_tree tree todo is_son (nesting + 1) + visit_tree None (flatten_tree tree) todo is_son + | _ -> assert false in - visit_desc desc [] false 0 + visit_desc desc [] false ;; -let rec clean_dummy_desc = function - | Dlevels l -> Dlevels (clean_levels l) - | x -> x -and clean_levels = function - | [] -> [] - | l :: tl -> clean_level l @ clean_levels tl - -and clean_level = function - | x -> - let pref = clean_tree x.lprefix in - let suff = clean_tree x.lsuffix in - match pref,suff with - | DeadEnd, DeadEnd -> [] - | _ -> [{x with lprefix = pref; lsuffix = suff}] - -and clean_tree = function - | Node n -> clean_node n - | x -> x - -and clean_node = function - | {node=node;son=son;brother=brother} -> - let bn = is_symbol_dummy node in - let bs = is_tree_dummy son in - let bb = is_tree_dummy brother in - let son = if bs then DeadEnd else son in - let brother = if bb then DeadEnd else brother in - if bb && bs && bn then - DeadEnd - else - if bn then - Node {node=Sself;son=son;brother=brother} - else - Node {node=node;son=son;brother=brother} - -and is_level_dummy = function - | {lsuffix=lsuffix;lprefix=lprefix} -> - is_tree_dummy lsuffix && is_tree_dummy lprefix - -and is_desc_dummy = function - | Dlevels l -> List.for_all is_level_dummy l - | Dparser _ -> true - -and is_entry_dummy = function - | {edesc=edesc} -> is_desc_dummy edesc - -and is_symbol_dummy = function - | Stoken ("DUMMY", _) -> true - | Stoken _ -> false - | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt - | Snterm e | Snterml (e, _) -> is_entry_dummy e - | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y - | Sopt x -> is_symbol_dummy x - | Sself | Snext -> false - | Stree t -> is_tree_dummy t - -and is_tree_dummy = function - | Node {node=node} -> is_symbol_dummy node - | _ -> true -;; - - -let rec visit_entries todo pped = - let fmt = Format.std_formatter in +let rec visit_entries fmt todo pped = match todo with | [] -> () | hd :: tl -> @@ -258,12 +236,10 @@ let rec visit_entries todo pped = if not (List.memq hd pped) then begin let { ename = ename; edesc = desc } = hd in - Format.fprintf fmt "@[%s ::=@ " ename; + Format.fprintf fmt "@[%s ::= " ename; let desc = clean_dummy_desc desc in let todo = visit_description desc fmt ename @ todo in - Format.fprintf fmt "@]"; - Format.pp_print_newline fmt (); - Format.pp_print_newline fmt (); + Format.fprintf fmt "@]\n\n"; todo end else @@ -283,9 +259,15 @@ let rec visit_entries todo pped = pped in let todo,pped = clean_todo todo in - visit_entries todo pped + visit_entries fmt todo pped ;; -let _ = - let g_entry = Grammar.Entry.obj GrafiteParser.statement in - visit_entries [g_entry] [] +let ebnf_of_term () = + let g_entry = Grammar.Entry.obj CicNotationParser.term in + let buff = Buffer.create 100 in + let fmt = Format.formatter_of_buffer buff in + visit_entries fmt [g_entry] []; + Format.fprintf fmt "@?"; + let s = Buffer.contents buff in + s +;; diff --git a/helm/software/components/syntax_extensions/utf8Macro.ml b/helm/software/components/syntax_extensions/utf8Macro.ml index 36d6b175d..00e10f183 100644 --- a/helm/software/components/syntax_extensions/utf8Macro.ml +++ b/helm/software/components/syntax_extensions/utf8Macro.ml @@ -42,9 +42,28 @@ let unicode_of_tex s = let tex_of_unicode s = (*WARNING: the space below is a nbsp (0x00A0), not a normal space *) - if s = " " then Some "" + if s = " " then [""] else try - Some ("\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s) - with Not_found -> None + let alt = Hashtbl.find_all Utf8MacroTable.utf82macro s in + List.sort + (fun x y -> Pervasives.compare (String.length x) (String.length y)) + alt + with Not_found -> [] +let pp_table () = + let rec list_uniq ?(eq=(=)) = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when eq h1 h2 -> list_uniq ~eq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq ~eq tl + in + let l = ref [] in + Hashtbl.iter (fun k _ -> l := k :: !l) Utf8MacroTable.utf82macro; + l := list_uniq (List.sort compare !l); + List.map + (fun k -> + let vs = Hashtbl.find_all Utf8MacroTable.utf82macro k in + (k, List.map (fun x -> "\\"^x) vs)) + !l +;; diff --git a/helm/software/components/syntax_extensions/utf8Macro.mli b/helm/software/components/syntax_extensions/utf8Macro.mli index b21ba504f..3eab22e77 100644 --- a/helm/software/components/syntax_extensions/utf8Macro.mli +++ b/helm/software/components/syntax_extensions/utf8Macro.mli @@ -36,4 +36,6 @@ val expand: string -> string val unicode_of_tex: string -> string (** ... the other way round *) -val tex_of_unicode: string -> string option +val tex_of_unicode: string -> string list + +val pp_table: unit -> (string * (string list)) list diff --git a/helm/software/components/syntax_extensions/utf8MacroTable.ml b/helm/software/components/syntax_extensions/utf8MacroTable.ml index eefdcea0f..588321c48 100644 --- a/helm/software/components/syntax_extensions/utf8MacroTable.ml +++ b/helm/software/components/syntax_extensions/utf8MacroTable.ml @@ -2136,5 +2136,5 @@ let _ = List.iter (fun (macro, utf8) -> Hashtbl.replace macro2utf8 macro utf8; - Hashtbl.replace utf82macro utf8 macro) + Hashtbl.add utf82macro utf8 macro) data;; diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 0eaaaa780..8cd2a9a73 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1180,6 +1180,14 @@ + + + True + Displays the term grammar + Show term's grammar + True + + @@ -1222,6 +1230,14 @@ + + + True + Displays the Tex/Unicode table + Show Tex/Unicode table + True + + True diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 98612ab2b..55b044ba4 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -905,6 +905,33 @@ class gui () = c#load (`About `Coercions)); connect_menu_item main#showAutoGuiMenuItem (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); + connect_menu_item main#showTermGrammarMenuItem + (fun _ -> + let w = GWindow.window ~resizable:true + ~position:`CENTER_ON_PARENT + ~title:"Terms grammar" ~width:640 ~height:400 () in + w#set_transient_for (main#toplevel#as_window); + let s = GBin.scrolled_window () in + (w :> GContainer.container)#add (s :> GObj.widget); + let t = GText.view () in + t#buffer#insert (Print_grammar.ebnf_of_term ()); + s#add (t:>GObj.widget); + w#show ()); + connect_menu_item main#showUnicodeTable + (fun _ -> + let w = GWindow.window ~resizable:true + ~position:`CENTER_ON_PARENT + ~title:"Tex/UTF8 table" ~width:640 ~height:400 () in + w#set_transient_for (main#toplevel#as_window); + let s = GBin.scrolled_window () in + (w :> GContainer.container)#add (s :> GObj.widget); + let t = GTree.view () in + let m = new MatitaGtkMisc.multiStringListModel ~cols:2 t in + List.iter (fun (k,vs) -> + m#easy_mappend [k;String.concat " " vs]) + (Utf8Macro.pp_table ()); + s#add (t:>GObj.widget); + w#show ()); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) -- 2.39.2