X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=bb3d29f069d336544546c1a22e86fbdfc9a71f4c;hb=f1f80d3696cca276a0e07babe46debd2447007f7;hp=60eb41424f23d7e802fb80d09f28f7ef2cee2619;hpb=be73a507f4f3c1b40a77dd7fc587adaf45b4d8ea;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 60eb41424..bb3d29f06 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -170,23 +170,24 @@ let extract_term_production pattern =
         [NoBinding, gram_keyword s]
     | `Number s -> [NoBinding, gram_number s]
   and aux_layout = function
-    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
-    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
-    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
-    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
-    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
-    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
-    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
-    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+    | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2
+    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2
+    | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below "] @ aux p2
+    | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above "] @ aux p2
+    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac "] @ aux p2
+    | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop "] @ aux p2
+    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over "] @ aux p2
     | Ast.Root (p1, p2) ->
-        [NoBinding, gram_symbol "\\root"] @ aux p2
-        @ [NoBinding, gram_symbol "\\of"] @ aux p1
-    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+        [NoBinding, gram_symbol "\\root "] @ aux p2
+        @ [NoBinding, gram_symbol "\\of "] @ aux p1
+    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p
     | Ast.Break -> []
     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
     | 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)
@@ -455,33 +460,33 @@ EXTEND
       v = [ PERCENTAGE ] -> id, v]];
   l1_simple_pattern:
     [ "layout" LEFTA
-      [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
+      [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\sup "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\below "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\above "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\over "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\atop "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
-      | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
+      | p1 = SELF; SYMBOL "\\frac "; p2 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
-      | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+      | SYMBOL "\\infrule "; p1 = SELF; p2 = SELF; p3 = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
-      | SYMBOL "\\sqrt"; p = SELF -> 
+      | 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 ->
+      | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF ->
           return_term_of_level loc 
             (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
@@ -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))
       ]
@@ -572,13 +581,14 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
+    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [
-    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+    [ SYMBOL "\\subst ";  (* to avoid catching frequent "a [1]" cases *)
       SYMBOL "[";
       substs = LIST1 [
         i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
@@ -598,18 +608,21 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
+    | id = PIDENT -> Ast.Ident (id, None), None
     | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
+        Ast.Ident (id, None), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
         Ast.Ident ("_", None), Some typ
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> Ast.Pattern (id, None, [])
+    [ SYMBOL "_" -> Ast.Wildcard
+    | id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
        Ast.Pattern (id, None, vars)
     | id = IDENT; vars = LIST1 possibly_typed_name ->
        Ast.Pattern (id, None, vars)
-    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [
@@ -680,9 +693,11 @@ EXTEND
     ]
   ];
   binder_vars: [
-    [ vars = [
-          l = LIST1 single_arg SEP SYMBOL "," -> l
-        | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
+    [ vars = [ l =
+        [ l = LIST1 single_arg SEP SYMBOL "," -> l
+        | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
+            List.map (fun x -> Ast.Ident(x,None)) l
+      ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
   ];