let rec/corec and co/inductive are not printed!

[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..1a664d525d82018672d727548b807e3bf3232c83 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)
@@ -460,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 ->
@@ -588,7 +588,7 @@ EXTEND
     ]
   ];
   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 +712,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 +754,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 ->
@@ -808,6 +816,8 @@ let exc_located_wrapper f =
   with
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
+  | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+      raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
   | Stdpp.Exc_located (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))