X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=7690aeb9b7464ffaae36a13b6c918acbe93fa268;hb=bcf9a65332d321c25761207e2fb17110dbdc8241;hp=bae4a8f593628821b0f8d1181563aa7e496222b8;hpb=1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index bae4a8f59..7690aeb9b 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -57,11 +57,26 @@ let int_of_string s =
 
 (** {2 Grammar extension} *)
 
+let level_of precedence associativity =
+  if precedence < min_precedence || precedence > max_precedence then
+    raise (Level_not_found precedence);
+  let assoc_string = 
+    match associativity with
+    | Gramext.NonA -> "N"
+    | Gramext.LeftA -> "L"
+    | Gramext.RightA -> "R"
+  in
+  string_of_int precedence ^ assoc_string
+
 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 = Gramext.Sself
+let gram_term = function
+  | None -> Gramext.Sself
+  | Some (precedence, associativity) ->
+      Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence associativity)
+;;
 
 let gram_of_literal =
   function
@@ -80,10 +95,10 @@ let make_action action bindings =
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
     (* LUCA: DEFCON 3 BEGIN *)
-    | Binding (name, Env.TermType) :: tl ->
+    | Binding (name, Env.TermType l) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
-            aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+            aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
     | Binding (name, Env.StringType) :: tl ->
         Gramext.action
           (fun (v:string) ->
@@ -198,7 +213,8 @@ let extract_term_production pattern =
   and aux_variable =
     function
     | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
-    | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+    | Ast.TermVar (s,level) -> 
+        [Binding (s, Env.TermType level), gram_term level]
     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
     | Ast.Ascription (p, s) -> assert false (* TODO *)
     | Ast.FreshVar _ -> assert false
@@ -213,17 +229,6 @@ let extract_term_production pattern =
   in
   aux pattern
 
-let level_of precedence associativity =
-  if precedence < min_precedence || precedence > max_precedence then
-    raise (Level_not_found 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 = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
@@ -334,8 +339,15 @@ EXTEND
     | "opt";   p = l1_simple_pattern -> Ast.Opt p
     ]
   ];
+  l1_associativity : [
+   [ IDENT "L" -> Gramext.LeftA
+   | IDENT "N" -> Gramext.NonA
+   | IDENT "R" -> Gramext.RightA
+   ]
+  ];
   l1_pattern_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; assoc = l1_associativity ; id = IDENT -> 
+        Ast.TermVar (id, Some (int_of_string precedence,assoc))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     ]
@@ -375,7 +387,7 @@ EXTEND
           return_term loc (CicNotationUtil.group p)
       ]
     | "simple" NONA
-      [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+      [ 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)
@@ -387,13 +399,20 @@ EXTEND
 (* {{{ Grammar for ast magics, notation level 2 *)
 EXTEND
   GLOBAL: level2_meta;
+  l2_associativity : [
+   [ IDENT "L" -> Gramext.LeftA
+   | IDENT "N" -> Gramext.NonA
+   | IDENT "R" -> Gramext.RightA
+   ]
+  ];
   l2_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; assoc = l2_associativity; id = IDENT -> 
+        Ast.TermVar (id,Some (int_of_string precedence, assoc))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     | "fresh"; id = IDENT -> Ast.FreshVar id
-    | "anonymous" -> Ast.TermVar "_"
-    | id = IDENT -> Ast.TermVar id
+    | "anonymous" -> Ast.TermVar ("_",None)
+    | id = IDENT -> Ast.TermVar (id,None)
     ]
   ];
   l2_magic: [
@@ -481,7 +500,7 @@ EXTEND
         let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
-        | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
@@ -492,7 +511,7 @@ EXTEND
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
         | _ -> failwith "Invalid index name."
     ]
   ];