From db63f65c35efaa93d0a2cc00a194549e791975c9 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 6 Dec 2011 16:37:30 +0000 Subject: [PATCH] Grammar change: let corecs can take no arguments (and they have no recursive argument). --- .../content_pres/cicNotationParser.ml | 36 ++++++++++++++----- .../content_pres/cicNotationParser.mli | 3 ++ .../components/content_pres/content2pres.ml | 10 ++++-- .../grafite_parser/grafiteParser.ml | 3 +- 4 files changed, 39 insertions(+), 13 deletions(-) diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 6d18fe837..00ac411fa 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; } @@ -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> (* ≝ *); 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> (* ≝ *); 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 1ec1fd59c..8f2311cf0 100644 --- 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 d07733a16..23e5a1b56 100644 --- 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 4ce915082..1ac21965e 100644 --- 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 -- 2.39.2