Grammar change: let corecs can take no arguments (and they have no recursive

argument).

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 6d18fe83794c622d0657d2cc5558c5d0e241f0f1..00ac411fa51cb24cc5c6bd94da715babcbd36a4e 100644 (file)
--- 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;
 }
@@ -208,8 +209,10 @@ 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,false)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)
+(*          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)*)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -556,10 +559,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
@@ -688,6 +692,23 @@ EXTEND
         defs
     ]
   ];
+  let_codefs: [
+    [ defs = LIST1 [
+        name = single_arg;
+        args = LIST0 arg;
+        ty = OPT [ SYMBOL ":" ; p = term -> p ];
+        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+          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
@@ -717,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"
@@ -797,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
@@ -805,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;
@@ -874,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
 

diff --git a/matita/components/content_pres/cicNotationParser.mli b/matita/components/content_pres/cicNotationParser.mli
index 1ec1fd59cc333b3254e501b2ee57c3ac523efc13..8f2311cf0da1af1879a16fc57d5f1e60fa8b1201 100644 (file)
--- a/matita/components/content_pres/cicNotationParser.mli
+++ b/matita/components/content_pres/cicNotationParser.mli
@@ -79,6 +79,9 @@ val term : #status -> NotationPt.term Grammar.Entry.e
 val let_defs : #status ->
   (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list
     Grammar.Entry.e
+val let_codefs : #status ->
+  (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list
+    Grammar.Entry.e
 
 val protected_binder_vars : #status ->
   (NotationPt.term list * NotationPt.term option) Grammar.Entry.e

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index d07733a1670676435894cb91528c20c084bafc83..23e5a1b56cb68e08c1cd52fa3e10e5e9cefe1368 100644 (file)
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -901,8 +901,10 @@ let definition2pres ?recno term2pres d =
   let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
   let module P = NotationPt in
-  let rec split_pi i t = 
-    if i <= 1 then 
+  let rec split_pi i t =
+    (* dummy case for corecursive defs *)
+    if i = ~-1 then [], P.UserInput, t
+    else if i <= 1 then 
       match t with 
       | P.Binder ((`Pi|`Forall),(var,_ as v),t) 
       | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> 
@@ -930,7 +932,9 @@ let definition2pres ?recno term2pres d =
   B.b_hv [] 
    [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
     ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ 
-        [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] 
+        if params <> [] then
+           [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))]
+        else [])] 
       @ [B.b_h [] 
          ((if rno <> -1 then 
            [B.b_kw "on";B.b_space;term2pres rec_param] else [])

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 4ce91508293241391d9d01c0e09a578266bfb2c4..1ac21965e3f3fe7090addfada9f812a85067bac1 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -95,6 +95,7 @@ let mk_parser statement lstatus =
 (*   let grammar = CicNotationParser.level2_ast_grammar lstatus in *)
   let term = CicNotationParser.term lstatus in
   let let_defs = CicNotationParser.let_defs lstatus in
+  let let_codefs = CicNotationParser.let_codefs lstatus in
   let protected_binder_vars = CicNotationParser.protected_binder_vars lstatus in
   (* {{{ parser initialization *)
 EXTEND
@@ -517,7 +518,7 @@ EXTEND
       paramspec = OPT inverter_param_list ; 
       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
         G.NInverter (loc,name,indty,paramspec,outsort)
-    | LETCOREC ; defs = let_defs -> 
+    | LETCOREC ; defs = let_codefs -> 
         nmk_rec_corec `CoInductive defs loc
     | LETREC ; defs = let_defs -> 
         nmk_rec_corec `Inductive defs loc