From: Stefano Zacchiroli Date: Tue, 19 Jul 2005 09:37:09 +0000 (+0000) Subject: handled difference associativity for the same level of the extensible grammar X-Git-Tag: V_0_7_2~186 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2817260358878e72fa359c6d2431b4c7c358a841;p=helm.git handled difference associativity for the same level of the extensible grammar (no more " changing associativity of level ..." messages) --- diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 7ba1c4f75..21cfffd5e 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -1,21 +1,21 @@ TODO -* gestione priorita'/associativita' - - triplicare livelli nella grammatica? * implementare type-checker per le trasformazioni * prestazioni trasformazioni 3 => 2 e 2 => 1 * magic per gestione degli array? -* gestione speciale dei numeri +* gestione della notazione per i numeri * sintassi concreta - studiare/implementare sintassi con ... per i magic fold * integrazione - portare le trasformazioni al nuovo ast - - salvare la notazione nei file .moo - togliere file non piu' utilizzati (caterva di cvs remove) + - gestire i problemi di ridefinizione della stessa notazione? DONE +* gestione priorita'/associativita' + - triplicare livelli nella grammatica? * implementare trasformazione 1 => 0 * implementare istanziazione dei magic a livello 1 (2 => 1) * implementare compilazione dei default in 2 => 1 @@ -30,4 +30,5 @@ DONE - porting della disambiguazione al nuovo ast - refactoring: unico punto di accesso allo stato imperativo della notazione - gestire cast + - salvare la notazione nei file .moo diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 041010649..85b894511 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -38,7 +38,6 @@ let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer let min_precedence = 0 let max_precedence = 100 -let default_precedence = 50 let level1_pattern = Grammar.Entry.create level1_pattern_grammar "level1_pattern" @@ -211,30 +210,34 @@ let extract_term_production pattern = in aux pattern -let level_of_int precedence = +let level_of precedence associativity = if precedence < min_precedence || precedence > max_precedence then raise (Level_not_found precedence); - string_of_int precedence + let assoc_string = + match associativity with + | Gramext.NonA -> "N" + | Gramext.LeftA -> "L" + | Gramext.RightA -> "R" + in + string_of_int precedence ^ assoc_string type rule_id = Token.t Gramext.g_symbol list (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *) let owned_keywords = Hashtbl.create 23 -let extend level1_pattern ?(precedence = default_precedence) - ?associativity action -= +let extend level1_pattern ~precedence ~associativity action = let p_bindings, p_atoms = List.split (extract_term_production level1_pattern) in - let level = level_of_int precedence in + let level = level_of precedence associativity in let p_names = flatten_opt p_bindings in let _ = Grammar.extend [ Grammar.Entry.obj (term: 'a Grammar.Entry.e), Some (Gramext.Level level), [ None, - associativity, + Some associativity, [ p_atoms, (make_action (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc)) @@ -276,7 +279,13 @@ let _ = (* create empty precedence level for "term" *) let mk_level_list first last = let rec aux acc = function | i when i < first -> acc - | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1) + | i -> + aux + ((Some (string_of_int i ^ "N"), Some Gramext.NonA, []) + :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, []) + :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, []) + :: acc) + (i - 1) in aux [] last in @@ -356,7 +365,7 @@ EXTEND END (* }}} *) - +(* {{{ Grammar for ast magics, notation level 2 *) EXTEND GLOBAL: level2_meta; l2_variable: [ @@ -387,10 +396,11 @@ EXTEND ] ]; END +(* }}} *) +(* {{{ Grammar for ast patterns, notation level 2 *) EXTEND GLOBAL: level2_ast term let_defs; -(* {{{ Grammar for ast patterns, notation level 2 *) level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop @@ -513,24 +523,23 @@ EXTEND RPAREN -> (vars, typ) ] ]; - term: LEVEL "10" (* let in *) - [ "10" NONA - [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); - p1 = term; "in"; p2 = term -> - return_term loc (LetIn (var, p1, p2)) - | "let"; k = induction_kind; defs = let_defs; "in"; - body = term -> - return_term loc (LetRec (k, defs, body)) - ] - ]; - term: LEVEL "20" (* binder *) - [ "20" RIGHTA + term: LEVEL "10N" [ (* let in *) + [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); + p1 = term; "in"; p2 = term -> + return_term loc (LetIn (var, p1, p2)) + | "let"; k = induction_kind; defs = let_defs; "in"; + body = term -> + return_term loc (LetRec (k, defs, body)) + ] + ]; + term: LEVEL "20R" (* binder *) + [ [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term -> return_term loc (fold_cluster b vars typ body) ] ]; - term: LEVEL "70" (* apply *) - [ "70" LEFTA + term: LEVEL "70L" (* apply *) + [ [ p1 = term; p2 = term -> let rec aux = function | Appl (hd :: tl) @@ -541,8 +550,8 @@ EXTEND return_term loc (Appl (aux p1 @ [p2])) ] ]; - term: LEVEL "90" (* simple *) - [ "90" NONA + term: LEVEL "90N" (* simple *) + [ [ id = IDENT -> return_term loc (Ident (id, None)) | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s)) | s = CSYMBOL -> return_term loc (Symbol (s, 0)) @@ -570,8 +579,8 @@ EXTEND | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob) ] ]; -(* }}} *) END +(* }}} *) (** {2 API implementation} *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 083d442eb..048551915 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -41,8 +41,8 @@ type rule_id val extend: CicNotationPt.term -> - ?precedence:int -> - ?associativity:Gramext.g_assoc -> + precedence:int -> + associativity:Gramext.g_assoc -> (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) -> rule_id diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 3118753f6..639ae48e0 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -53,9 +53,7 @@ let rec pp_term ?(pp_parens = true) t = sprintf "#[%s]" (pp_term term) | AttributedTerm (_, term) when print_attributes -> sprintf "@[%s]" (pp_term term) *) - | AttributedTerm (`Raw (text, None), _) -> text - | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text - | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text + | AttributedTerm (`Raw text, _) -> text | AttributedTerm (_, term) -> pp_term ~pp_parens:false term | Appl terms -> diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 4ea310ee5..68ad7d83d 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -39,8 +39,6 @@ let fail floc msg = let (x, y) = loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) -type blob_context = [ `Ast | `Meta ] - type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) @@ -48,7 +46,7 @@ type term_attribute = | `Level of int * Gramext.g_assoc (* precedence, associativity *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) - | `Raw of string * blob_context option (* unparsed version *) + | `Raw of string (* unparsed version *) ] type literal = diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 91b40fbee..b7322afd4 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -29,9 +29,6 @@ type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id -let default_prec = 50 -let default_assoc = Gramext.NonA - module Ast = CicNotationPt type term_info = @@ -446,9 +443,7 @@ let lookup_interpretations symbol = !(Hashtbl.find interpretations symbol) with Not_found -> raise Interpretation_not_found -let add_pretty_printer - ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 -= +let add_pretty_printer ~precedence ~associativity l2 l1 = let id = fresh_id () in let l2' = CicNotationUtil.strip_attributes l2 in Hashtbl.add level1_patterns21 id (precedence, associativity, l1); diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 105f3ffba..22b4f64e8 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -51,8 +51,8 @@ val lookup_interpretations: CicNotationPt.cic_appl_pattern) list val add_pretty_printer: - ?precedence:int -> - ?associativity:Gramext.g_assoc -> + precedence:int -> + associativity:Gramext.g_assoc -> CicNotationPt.term -> (* level 2 pattern *) CicNotationPt.term -> (* level 1 pattern *) pretty_printer_id diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index 7d09e2d6a..a5c4db085 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -133,7 +133,7 @@ type ('term,'obj) command = | Alias of loc * alias_spec (** parameters, name, type, fields *) | Obj of loc * 'obj - | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option * + | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int * CicNotationPt.term (* level 1 pattern, associativity, precedence, level 2 pattern *) | Interpretation of loc * diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index b7a62476c..029152e36 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -248,14 +248,11 @@ let pp_l1_pattern = CicNotationPp.pp_term let pp_l2_pattern = CicNotationPp.pp_term let pp_associativity = function - | Some Gramext.LeftA -> "left associative " - | Some Gramext.RightA -> "right associative " - | Some Gramext.NonA -> "non associative " - | None -> "" + | Gramext.LeftA -> "left associative" + | Gramext.RightA -> "right associative" + | Gramext.NonA -> "non associative" -let pp_precedence = function - | Some i -> sprintf "with precedence %d " i - | None -> "" +let pp_precedence i = sprintf "with precedence %d" i let pp_command = function | Include (_,path) -> "include " ^ path @@ -274,7 +271,7 @@ let pp_command = function (String.concat " " (List.map pp_argument_pattern arg_patterns)) (pp_cic_appl_pattern cic_appl_pattern) | Notation (_, l1_pattern, assoc, prec, l2_pattern) -> - sprintf "notation \"%s\" %s%sfor %s" + sprintf "notation \"%s\" %s %s for %s" (pp_l1_pattern l1_pattern) (pp_associativity assoc) (pp_precedence prec) diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 984635ec6..908ad007f 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -30,8 +30,10 @@ let grammar = CicNotationParser.level2_ast_grammar let term = CicNotationParser.term let statement = Grammar.Entry.create grammar "statement" -let add_raw_attribute ?context ~text term = - CicNotationPt.AttributedTerm (`Raw (text, context), term) +let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t) + +let default_precedence = 50 +let default_associativity = Gramext.NonA EXTEND GLOBAL: term statement; @@ -361,12 +363,22 @@ EXTEND IDENT "for"; p2 = [ blob = UNPARSED_AST -> - add_raw_attribute ~context:`Ast ~text:blob + add_raw_attribute ~text:(sprintf "@{%s}" blob) (CicNotationParser.parse_level2_ast (Stream.of_string blob)) | blob = UNPARSED_META -> - add_raw_attribute ~context:`Meta ~text:blob + add_raw_attribute ~text:(sprintf "${%s}" blob) (CicNotationParser.parse_level2_meta (Stream.of_string blob)) ] -> + let assoc = + match assoc with + | None -> default_associativity + | Some assoc -> assoc + in + let prec = + match prec with + | None -> default_precedence + | Some prec -> prec + in (add_raw_attribute ~text:s (CicNotationParser.parse_level1_pattern (Stream.of_string s)), assoc, prec, p2) diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 62b0ae32b..960af9d5f 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -53,6 +53,13 @@ let errquit ignore_exn = exit 2 end +let pp_associativity = function + | Gramext.LeftA -> "left" + | Gramext.RightA -> "right" + | Gramext.NonA -> "non" + +let pp_precedence = string_of_int + let process_stream ?(ignore_exn = false) istream = let char_count = ref 0 in let module P = CicNotationPt in @@ -66,40 +73,32 @@ let process_stream ?(ignore_exn = false) istream = char_count := y + !char_count; match statement with | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline "===="; - prerr_endline (CicNotationPp.pp_term t); flush stdout; + prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); let t' = CicNotationRew.pp_ast t in - prerr_endline (CicNotationPp.pp_term t'); flush stdout; - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" + prerr_endline (sprintf "rendered ast: %s" + (CicNotationPp.pp_term t')); + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" | G.Executable (_, G.Command (_, G.Notation (_, l1, associativity, precedence, l2))) -> - prerr_endline "Extending parser ..."; flush stdout; - prerr_endline (CicNotationPp.pp_term l1) ; - prerr_endline (CicNotationPp.pp_term l2) ; - prerr_endline (sprintf "Found keywords: %s" - (String.concat " " (CicNotationUtil.keywords_of_term l1))); - let time1 = Unix.gettimeofday () in - ignore (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); - let time2 = Unix.gettimeofday () in - prerr_endline "Extending pretty printer ..."; flush stdout; - let time3 = Unix.gettimeofday () in - ignore (CicNotationRew.add_pretty_printer - ?precedence ?associativity l2 l1); - let time4 = Unix.gettimeofday () in - printf ("done (extending parser took %f, " ^^ - "extending pretty printer took %f)\n") - (time2 -. time1) (time4 -. time3); - flush stdout + prerr_endline "notation"; + prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); + prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); + prerr_endline (sprintf "prec: %s" (pp_precedence precedence)); + prerr_endline (sprintf "assoc: %s" (pp_associativity associativity)); + let keywords = CicNotationUtil.keywords_of_term l1 in + if keywords <> [] then + prerr_endline (sprintf "keywords: %s" + (String.concat " " keywords)); + ignore (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); + ignore (CicNotationRew.add_pretty_printer + ?precedence ?associativity l2 l1) | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> - prerr_endline "Adding interpretation ..."; flush stdout; - let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation id l2 l3); - let time2 = Unix.gettimeofday () in - printf "done (patterns compilation took %f seconds)\n" - (time2 -. time1); - flush stdout + prerr_endline "interpretation"; + prerr_endline (sprintf "dsc: %s" id); + ignore (CicNotationRew.add_interpretation id l2 l3); + flush stdout | G.Executable (_, G.Command (_, G.Dump _)) -> CicNotationParser.print_l2_pattern (); print_newline () | G.Executable (_, G.Command (_, G.Render (_, uri))) -> @@ -113,25 +112,15 @@ let process_stream ?(ignore_exn = false) istream = | Cic.AVariable (_, _, _, ty, _, _) -> ty | _ -> assert false in - let time1 = Unix.gettimeofday () in let t, id_to_uri = CicNotationRew.ast_of_acic id_to_sort annterm in - let time2 = Unix.gettimeofday () in - prerr_endline (sprintf "ast creation took %f seconds\n" - (time2 -. time1)); - prerr_endline "AST"; - prerr_endline (CicNotationPp.pp_term t); - flush stdout; - let time3 = Unix.gettimeofday () in - let t' = CicNotationRew.pp_ast t in - let time4 = Unix.gettimeofday () in - prerr_endline (sprintf "pretty printing took %f seconds\n" - (time4 -. time3)); - prerr_endline (CicNotationPp.pp_term t'); - dump_xml t' id_to_uri "out.xml" - | _ -> - prerr_endline "Unsupported statement" + prerr_endline "AST"; + prerr_endline (CicNotationPp.pp_term t); + let t' = CicNotationRew.pp_ast t in + prerr_endline (CicNotationPp.pp_term t'); + dump_xml t' id_to_uri "out.xml" + | _ -> prerr_endline "Unsupported statement" with | End_of_file -> raise End_of_file | CicNotationParser.Parse_error (floc, msg) -> @@ -157,9 +146,7 @@ let _ = let usage = "" in Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; print_endline "Loading builtin notation ..."; - let ic = open_in (Helm_registry.get "notation.core_file") in - process_stream ~ignore_exn:true (Stream.of_channel ic); - close_in ic; + CicNotation.load_notation (Helm_registry.get "notation.core_file"); print_endline "done."; flush stdout; process_stream ~ignore_exn:false (Stream.of_channel stdin)