X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.expanded.ml;h=69b51c398fa304da592702f9bcf71881f558498e;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=bd42ea9cb22516e95b343661038201f99e3b590d;hpb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
index bd42ea9cb..69b51c398 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
@@ -24,9 +24,9 @@
  *)
 
 oopen Printf
-eexception Parse_error of Token.flocation * string
+eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
 llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
-llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
+llet level1_pattern = Grammar.Entry.create grammar "level1_pattern"llet level2_pattern = Grammar.Entry.create grammar "level2_pattern"llet level3_term = Grammar.Entry.create grammar "level3_term"llet l2_pattern = Grammar.Entry.create grammar "l2_pattern"llet notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
 llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
 
 llet return_term loc term = ()
@@ -57,6 +57,7 @@ Elet _ =
     (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
      and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
      and _ = (level3_term : 'level3_term Grammar.Entry.e)
+     and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e)
      and _ = (notation : 'notation Grammar.Entry.e)
      and _ = (interpretation : 'interpretation Grammar.Entry.e) in
      let grammar_entry_create s =
@@ -92,8 +93,6 @@ Elet _ =
        grammar_entry_create "l2_pattern_variable"
      and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
        grammar_entry_create "l2_magic_pattern"
-     and l2_pattern : 'l2_pattern Grammar.Entry.e =
-       grammar_entry_create "l2_pattern"
      and argument : 'argument Grammar.Entry.e =
        grammar_entry_create "argument"
      and associativity : 'associativity Grammar.Entry.e =
@@ -217,7 +216,7 @@ Elet _ =
         Gramext.action
           (fun _ (p : 'l1_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
+             (return_term loc (boxify p) : 'l1_simple_pattern));
         [Gramext.Stoken ("SYMBOL", "\\BREAK")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
@@ -279,7 +278,7 @@ Elet _ =
         Gramext.action
           (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Frac (boxify p1, boxify p2))) :
+             (return_term loc (Layout (Over (boxify p1, boxify p2))) :
               'l1_simple_pattern));
         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
         Gramext.action
@@ -571,7 +570,8 @@ Elet _ =
              (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
              (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
       Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
-      [Some "letin", Some Gramext.NonA,
+      [Some "0", None, [];
+       Some "10", Some Gramext.NonA,
        [[Gramext.Stoken ("IDENT", "let");
          Gramext.Snterm
            (Grammar.Entry.obj
@@ -594,7 +594,7 @@ Elet _ =
              (var : 'possibly_typed_name) _
              (loc : Lexing.position * Lexing.position) ->
              (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))];
-       Some "binder", Some Gramext.RightA,
+       Some "20", Some Gramext.RightA,
        [[Gramext.Snterm
            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
          Gramext.Snterm
@@ -604,8 +604,9 @@ Elet _ =
           (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
              (loc : Lexing.position * Lexing.position) ->
              (return_term loc (fold_binder b names body) : 'l2_pattern))];
-       Some "extension", None, [];
-       Some "apply", Some Gramext.LeftA,
+       Some "30", None, []; Some "40", None, []; Some "50", None, [];
+       Some "60", None, [];
+       Some "70", Some Gramext.LeftA,
        [[Gramext.Sself; Gramext.Sself],
         Gramext.action
           (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
@@ -618,7 +619,8 @@ Elet _ =
               in
               return_term loc (Appl (aux p1 @ [p2])) :
               'l2_pattern))];
-       Some "simple", Some Gramext.NonA,
+       Some "80", None, [];
+       Some "90", Some Gramext.NonA,
        [[Gramext.Snterm
            (Grammar.Entry.obj
               (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
@@ -714,7 +716,8 @@ Elet _ =
         [Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Num (n, 0)) : 'l2_pattern));
+             (prerr_endline "number"; return_term loc (Num (n, 0)) :
+              'l2_pattern));
         [Gramext.Stoken ("URI", "")],
         Gramext.action
           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
@@ -730,7 +733,8 @@ Elet _ =
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Ident (id, None)) : 'l2_pattern))]];
+             (return_term loc (Ident (id, None)) : 'l2_pattern))];
+       Some "100", None, []];
       Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
       [None, None,
        [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
@@ -846,4 +850,150 @@ let parse_ast_pattern stream =
 let parse_interpretation stream =
   exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
 
+(** {2 Grammar extension} *)
+
+type associativity_kind = [ `Left | `Right | `None ]
+
+let symbol s = Gramext.Stoken ("SYMBOL", s)
+let ident s = Gramext.Stoken ("IDENT", s)
+let number s = Gramext.Stoken ("NUMBER", s)
+let term = Gramext.Sself
+
+type env_type = (string * (value_type * value)) list
+
+let make_action action =
+  let rec aux (vl : env_type) =
+    prerr_endline "aux";
+    function
+      [] ->
+        prerr_endline "make_action";
+        Gramext.action (fun (loc : location) -> action vl loc)
+    | None :: tl -> Gramext.action (fun _ -> aux vl tl)
+    | Some (name, TermType) :: tl ->
+        Gramext.action
+          (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
+    | Some (name, StringType) :: tl ->
+        Gramext.action
+          (fun (v : string) ->
+             aux ((name, (StringType, StringValue v)) :: vl) tl)
+    | Some (name, NumType) :: tl ->
+        Gramext.action
+          (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
+    | Some (name, OptType t) :: tl ->
+        Gramext.action
+          (fun (v : 'a option) ->
+             aux ((name, (OptType t, OptValue v)) :: vl) tl)
+    | Some (name, ListType t) :: tl ->
+        Gramext.action
+          (fun (v : 'a list) ->
+             aux ((name, (ListType t, ListValue v)) :: vl) tl)
+  in
+  aux []
+
+let flatten_opt =
+  let rec aux acc =
+    function
+      [] -> List.rev acc
+    | None :: tl -> aux acc tl
+    | Some hd :: tl -> aux (hd :: acc) tl
+  in
+  aux []
+
+  (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
+let extract_term_production pattern =
+  let rec aux =
+    function
+      Literal l -> aux_literal l
+    | Layout l -> aux_layout l
+    | Magic m -> aux_magic m
+    | Variable v -> aux_variable v
+    | _ -> assert false
+  and aux_literal =
+    function
+      `Symbol s -> [None, symbol s]
+    | `Keyword s -> [None, ident s]
+    | `Number s -> [None, number s]
+  and aux_layout =
+    function
+      Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
+    | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
+    | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
+    | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
+    | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
+    | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
+    | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
+    | Root (p1, p2) ->
+        [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
+    | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
+    | Break -> []
+    | Box (_, pl) -> List.flatten (List.map aux pl)
+  and aux_magic =
+    function
+      Opt p ->
+        let (p_bindings, p_atoms) = List.split (aux p) in
+        let p_names = flatten_opt p_bindings in
+        [None,
+         Gramext.srules
+           [[Gramext.Sopt
+               (Gramext.srules
+                  [p_atoms,
+                   make_action (fun (env : env_type) (loc : location) -> env)
+                     p_bindings])],
+            Gramext.action
+              (fun (env_opt : env_type option) (loc : location) ->
+                 match env_opt with
+                   Some env ->
+                     List.map
+                       (fun (name, (typ, v)) ->
+                          name, (OptType typ, OptValue (Some v)))
+                       env
+                 | None ->
+                     List.map
+                       (fun (name, typ) -> name, (OptType typ, OptValue None))
+                       p_names)]]
+    | _ -> assert false
+  and aux_variable =
+    function
+      NumVar s -> [Some (s, NumType), number ""]
+    | TermVar s -> [Some (s, TermType), term]
+    | IdentVar s -> [Some (s, StringType), ident ""]
+    | Ascription (p, s) -> assert false
+    | FreshVar _ -> assert false
+  in
+  aux pattern
+
+let level_of_int precedence =
+  if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
+    raise (Level_not_found precedence);
+  string_of_int precedence
+
+type rule_id = Token.t Gramext.g_symbol list
+
+let extend level1_pattern ?(precedence = 0) =
+  fun ?associativity action ->
+    let (p_bindings, p_atoms) =
+      List.split (extract_term_production level1_pattern)
+    in
+    let level = level_of_int precedence in
+    let p_names = flatten_opt p_bindings in
+    let entry = Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e) in
+    let _ =
+      prerr_endline (string_of_int (List.length p_bindings));
+      Grammar.extend
+        [entry, Some (Gramext.Level level),
+         [Some level, associativity,
+          [p_atoms,
+           make_action
+             (fun (env : env_type) (loc : location) -> action env loc)
+             p_bindings]]]
+    in
+    p_atoms
+
+let delete atoms = Grammar.delete_rule l2_pattern atoms
+
+let print_l2_pattern () =
+  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
+  Format.pp_print_flush Format.std_formatter ();
+  flush stdout
+
 (* vim:set encoding=utf8 foldmethod=marker: *)