Porting to ocaml 5

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

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 38ce016768914215913ebb4ae0c2c047a6ece4a5..36a3fb01771bac4cfb10274087a1785dbd5b0741 100644 (file)
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -36,6 +36,11 @@ exception Level_not_found of int
 let min_precedence = 0
 let max_precedence = 100
 
+let hash_expr e =
+ e
+ |> Hashtbl.hash
+ |> Printf.sprintf "%08x"
+
 type ('a,'b,'c,'d,'e) grammars = {
   level1_pattern: 'a Grammar.Entry.e;
   level2_ast: 'b Grammar.Entry.e;
@@ -74,7 +79,7 @@ type db = {
 
 let int_of_string s =
   try
-    Pervasives.int_of_string s
+    Stdlib.int_of_string s
   with Failure _ ->
     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
 
@@ -189,15 +194,16 @@ let extract_term_production status pattern =
   and aux_magic magic =
     match magic with
     | Ast.Opt p ->
-        let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-        let action (env_opt : NotationEnv.t option) (loc : Ast.location) =
+        let _p_bindings, p_atoms, p_names, p_action = inner_pattern p in
+        let action (env_opt : NotationEnv.t option) (_loc : Ast.location) =
           match env_opt with
           | Some env -> List.map Env.opt_binding_some env
           | None -> List.map Env.opt_binding_of_name p_names
         in
         [ Env (List.map Env.opt_declaration p_names),
           Gramext.srules
-            [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
+            [ [ Gramext.Sopt (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+              hash_expr action,
               Gramext.action action ] ]
     | Ast.List0 (p, _)
     | Ast.List1 (p, _) ->
@@ -215,7 +221,8 @@ let extract_term_production status pattern =
         in
         [ Env (List.map Env.list_declaration p_names),
           Gramext.srules
-            [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
+            [ [ gram_of_list (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+              hash_expr action,
               Gramext.action action ] ]
     | _ -> assert false
   and aux_variable =
@@ -246,7 +253,7 @@ let compare_rule_id x y =
     | _,[] -> 1
     | ((s1::tl1) as x),((s2::tl2) as y) ->
         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
-        else Pervasives.compare x y 
+        else Stdlib.compare x y 
   in
     aux (x,y)
 
@@ -357,11 +364,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, HExtlib.Localized (_,exn)) ->
+  | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
-  | Stdpp.Exc_located (floc, exn) ->
+  | Ploc.Exc (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
 
 let parse_level1_pattern grammars precedence lexbuf =
@@ -384,7 +391,7 @@ let initialize_grammars grammars =
   in
   (* Needed since campl4 on "delete_rule" remove the precedence level if it gets
    * empty after the deletion. The lexer never generate the Stoken below. *)
-  let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
+  let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], "DUMMY", dummy_action ] in
   let mk_level_list first last =
     let rec aux acc = function
       | i when i < first -> acc
@@ -616,7 +623,8 @@ EXTEND
   ];
   arg: [
     [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN ->
+      typ = OPT [ SYMBOL ":"; typ = term -> typ] ; RPAREN -> (* FG: now type is optional *)
+        let ty = match typ with Some ty -> ty | None -> Ast.Implicit `JustOne in
         List.map (fun n -> Ast.Ident (n, None)) names, Some ty
     | name = IDENT -> [Ast.Ident (name, None)], None
     | blob = UNPARSED_META ->
@@ -657,7 +665,8 @@ EXTEND
         args = LIST1 arg;
         index_name = OPT [ "on"; id = single_arg -> id ];
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let rec position_of name p = function 
             | [] -> None, p
             | n :: _ when n = name -> Some p, p
@@ -695,7 +704,8 @@ EXTEND
         name = single_arg;
         args = LIST0 arg;
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let args =
            List.concat
             (List.map
@@ -859,6 +869,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         [ None,
           Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, 
+            hash_expr "(make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings)",
             (make_action
               (fun (env: NotationEnv.t) (loc: Ast.location) ->
                 (action env loc))