X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=8c7460346c624c4993684fa8ee564e462fdbc99a;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=f3953eb08f3e5a24302c142d38c93b15ac8e98a1;hpb=ac80c2cd2667de2942182ae0a98ad3dbadd7b559;p=helm.git

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index f3953eb08..8c7460346 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -43,6 +43,7 @@ type ('a,'b,'c,'d,'e) grammars = {
   term: 'b Grammar.Entry.e;
   ident: 'e Grammar.Entry.e;
   let_defs: 'c Grammar.Entry.e;
+  let_codefs: 'c Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
   level2_meta: 'b Grammar.Entry.e;
 }
@@ -157,7 +158,7 @@ let extract_term_production status pattern =
     | Ast.Magic m -> aux_magic m
     | Ast.Variable v -> aux_variable v
     | t ->
-        prerr_endline (NotationPp.pp_term t);
+        prerr_endline (NotationPp.pp_term status t);
         assert false
   and aux_literal =
     function
@@ -188,8 +189,8 @@ 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
@@ -208,8 +209,8 @@ let extract_term_production status 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),
@@ -356,11 +357,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 =
@@ -556,10 +557,11 @@ END
   let level2_ast = grammars.level2_ast in
   let term = grammars.term in
   let let_defs = grammars.let_defs in
+  let let_codefs = grammars.let_codefs in
   let ident = grammars.ident in
   let protected_binder_vars = grammars.protected_binder_vars in
 EXTEND
-  GLOBAL: level2_ast term let_defs protected_binder_vars ident;
+  GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
@@ -655,7 +657,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
@@ -663,8 +666,10 @@ EXTEND
           in
           let rec find_arg name n = function 
             | [] ->
+                (* CSC: new NCicPp.status is the best I can do here
+                   without changing the return type *)
                 Ast.fail loc (sprintf "Argument %s not found"
-                  (NotationPp.pp_term name))
+                  (NotationPp.pp_term (new NCicPp.status) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -686,6 +691,24 @@ EXTEND
         defs
     ]
   ];
+  let_codefs: [
+    [ defs = LIST1 [
+        name = single_arg;
+        args = LIST0 arg;
+        ty = OPT [ SYMBOL ":" ; p = term -> p ];
+        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
+             (function (names,ty) -> List.map (function x -> x,ty) names
+             ) args)
+          in
+           args, (name, ty), body, 0
+      ] SEP "and" ->
+        defs
+    ]
+  ];
   binder_vars: [
     [ vars = [ l =
         [ l = LIST1 single_arg SEP SYMBOL "," -> l
@@ -715,12 +738,6 @@ EXTEND
       SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
-    | LETCOREC; defs = let_defs; "in";
-      body = term ->
-        return_term loc (Ast.LetRec (`CoInductive, defs, body))
-    | LETREC; defs = let_defs; "in";
-      body = term ->
-        return_term loc (Ast.LetRec (`Inductive, defs, body))
     ]
   ];
   term: LEVEL "20"
@@ -795,6 +812,7 @@ let initial_grammars keywords =
   let term = Grammar.Entry.create level2_ast_grammar "term" in
   let ident = Grammar.Entry.create level2_ast_grammar "ident" in
   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+  let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
   let protected_binder_vars = 
     Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
   let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
@@ -803,6 +821,7 @@ let initial_grammars keywords =
     term=term;
     ident=ident;
     let_defs=let_defs;
+    let_codefs=let_codefs;
     protected_binder_vars=protected_binder_vars;
     level2_meta=level2_meta;
     level2_ast_grammar=level2_ast_grammar;
@@ -814,7 +833,7 @@ class type g_status =
   method notation_parser_db: db
  end
 
-class status ~keywords:kwds =
+class status0 ~keywords:kwds =
  object
   val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
   method notation_parser_db = db
@@ -824,6 +843,12 @@ class status ~keywords:kwds =
    = fun o -> {< db = o#notation_parser_db >}
  end
 
+class virtual status ~keywords:kwds =
+ object
+  inherit NCic.status
+  inherit status0 kwds
+ end
+
 let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         (* move inside constructor XXX *)
   let add1item status (level, level1_pattern, action) =
@@ -848,7 +873,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
   let keywords = NotationUtil.keywords_of_term level1_pattern @
     status#notation_parser_db.keywords in
   let items = current_item :: status#notation_parser_db.items in 
-  let status = status#set_notation_parser_status (new status ~keywords) in
+  let status = status#set_notation_parser_status (new status0 ~keywords) in
   let status = status#set_notation_parser_db 
     {status#notation_parser_db with items = items} in
   List.fold_left add1item status items
@@ -866,6 +891,7 @@ let level2_ast_grammar status =
   status#notation_parser_db.grammars.level2_ast_grammar
 let term status = status#notation_parser_db.grammars.term
 let let_defs status = status#notation_parser_db.grammars.let_defs
+let let_codefs status = status#notation_parser_db.grammars.let_codefs
 let protected_binder_vars status = 
   status#notation_parser_db.grammars.protected_binder_vars