parameter sintax added to axiom statement

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 695db149e3f0c2bc722629d589b8bfc39f61adb9..587c22e4a07b8b9a39fea3225069c4a73454e01f 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -170,18 +170,18 @@ 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)
@@ -211,8 +211,8 @@ let extract_term_production pattern =
           match magic with
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -246,9 +246,14 @@ let compare_rule_id x y =
     | [],[] -> 0
     | [],_ -> ~-1
     | _,[] -> 1
-    | ((s1::tl1) as x),((s2::tl2) as y) ->
+    | ((s1::tl1) ),((s2::tl2) ) ->
         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
-        else Pervasives.compare x y 
+        else 
+          let res = 
+            try Pervasives.compare s1 s2 
+            with Invalid_argument _ -> 0 
+          in
+           if res = 0 then aux (tl1, tl2) else res 
   in
     aux (x,y)
 
@@ -460,33 +465,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 ->
@@ -581,14 +586,14 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+    | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+    | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; 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)
@@ -712,7 +717,13 @@ EXTEND
   ];
   term: LEVEL "10"
   [
-    [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+    [ "let"; 
+     var = 
+      [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
+         id, Some typ
+      | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+         Ast.Ident(id,None), ty ];
+      SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
     | LETCOREC; defs = let_defs; "in";
@@ -748,8 +759,10 @@ EXTEND
           return_term loc (Ast.Ident (id, Some s))
       | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
       | u = URI -> return_term loc (Ast.Uri (u, None))
+      | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
       | n = NUMBER -> return_term loc (Ast.Num (n, 0))
-      | IMPLICIT -> return_term loc (Ast.Implicit)
+      | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+      | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
       | m = META; s = meta_substs ->
@@ -806,9 +819,11 @@ let exc_located_wrapper f =
   try
     f ()
   with
-  | Stdpp.Exc_located (floc, Stream.Error msg) ->
+  | Ploc.Exc (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
+      raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
+  | Ploc.Exc (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 
 let parse_level1_pattern precedence lexbuf =