From: Claudio Sacerdoti Coen Date: Fri, 20 Jun 2008 11:04:18 +0000 (+0000) Subject: - partial implementation of pattern for case documented X-Git-Tag: make_still_working~5008 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef1893c67c666d28018ad74f72db4d29ad669b84;p=helm.git - partial implementation of pattern for case documented - notation partially documented - omitting the precedence level in a notation declaration is no longer allowed --- diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 6ce615091..18c30d4ec 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -55,7 +55,6 @@ let statement = Grammar.Entry.create grammar "statement" let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) -let default_precedence = 50 let default_associativity = Gramext.NonA let mk_rec_corec ind_kind defs loc = @@ -575,7 +574,7 @@ EXTEND ]; notation: [ [ dir = OPT direction; s = QSTRING; - assoc = OPT associativity; prec = OPT precedence; + assoc = OPT associativity; prec = precedence; IDENT "for"; p2 = [ blob = UNPARSED_AST -> @@ -592,11 +591,6 @@ EXTEND | None -> default_associativity | Some assoc -> assoc in - let prec = - match prec with - | None -> default_precedence - | Some prec -> prec - in let p1 = add_raw_attribute ~text:s (CicNotationParser.parse_level1_pattern diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index cb94d108c..21dd9bc7b 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -58,6 +58,10 @@ interpretation_argument"> interpretation_rhs"> csymbol"> + usage"> + notation_lhs"> + notation_rhs"> + associativity"> ]> diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 0205ce8a8..ebd100a26 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -221,7 +221,7 @@ cases cases - cases t hyps + cases t pattern hyps @@ -230,7 +230,7 @@ cases - &term; [([&id;]…)] + &term; &pattern; [([&id;]…)] @@ -249,6 +249,12 @@ It proceed by cases on t. The new generated hypothesis in each branch are named according to hyps. + The elimintation predicate is restricted by + pattern. In particular, if some hypothesis + is listed in pattern, the hypothesis is + generalized and cleared before proceeding by cases on + t. Currently, we only support patterns of the + form H1 … Hn ⊢ %. This limitation will be lifted in the future. diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml index f4b3cc411..46bf146c9 100644 --- a/helm/software/matita/help/C/sec_usernotation.xml +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -2,12 +2,132 @@ Extending the syntax - Introduction: TODO + Introduction: &TODO; notation notation + notation usage "presentation" associativity with precedence p for content - notation: &TODO; + + + Synopsis: + + notation + [&usage;] "¬ation_lhs;" [&associativity;] with precedence &nat; + for + ¬ation_rhs; + + + + + Action: + + Declares a mapping between the presentation + AST presentation and the content AST + content. The declared presentation AST fragment + presentation is at precedence level + p. The precedence level is used to determine where + parentheses must be inserted. In particular, the content AST fragment + content is actually a pattern, since it contains + placeholders (variables) for sub-ASTs. Every placeholder for a term + is given an expected precedence level. Parentheses must be inserted + around sub-ASTs having a precedence level strictly smaller than the + expected one. + If presentation describes a binary + infix operator and if no precedence level is explicitly given for the + operator arguments, an associativity declaration + can be given to automatically choose the right level for the operands. + Otherwise, no associativity can be given. + If direction is + omitted, the mapping is bi-directional and is used both during + parsing and pretty-printing of terms. If direction + is >, the mapping is used only during parsing; + if it is <, it is used only during + pretty-printing. Thus it is possible to use simple notations to type + for writing the term, and nicer ones for rendering it. + + + + Notation arguments: + + + + usage + + + + &usage; + ::= + < + Only for pretty-printing + + + + | + > + Only for parsing + + + +
+ + + associativity + + + + &associativity; + ::= + left associative + Left associative + + + + | + left associative + Right associative + + + + | + non associative + Non associative (default) + + + +
+ + + notation_rhs + + + + ¬ation_rhs; + ::= + &TODO; + &TODO; + + + +
+ + + notation_lhs + + + + ¬ation_lhs; + ::= + &TODO; + &TODO; + + + +
+ + + + @@ -22,7 +142,7 @@ interpretation &qstring; &csymbol; [&interpretation_argument;]… - = + = &interpretation_rhs; diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml index ba7020c10..c7a789c1a 100644 --- a/helm/software/matita/help/C/tactics_quickref.xml +++ b/helm/software/matita/help/C/tactics_quickref.xml @@ -36,7 +36,7 @@ | cases - term [([id]…)] + term pattern [([id]…)]