diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories7/Reals/Rsyntax.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories7/Reals/Rsyntax.v')
-rw-r--r-- | theories7/Reals/Rsyntax.v | 236 |
1 files changed, 236 insertions, 0 deletions
diff --git a/theories7/Reals/Rsyntax.v b/theories7/Reals/Rsyntax.v new file mode 100644 index 00000000..7b1b6266 --- /dev/null +++ b/theories7/Reals/Rsyntax.v @@ -0,0 +1,236 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Rsyntax.v,v 1.1.2.1 2004/07/16 19:31:35 herbelin Exp $ i*) + +Require Export Rdefinitions. + +Axiom NRplus : R->R. +Axiom NRmult : R->R. + +V7only[ +Grammar rnatural ident := + nat_id [ prim:var($id) ] -> [$id] + +with rnegnumber : constr := + neg_expr [ "-" rnumber ($c) ] -> [ (Ropp $c) ] + +with rnumber := + +with rformula : constr := + form_expr [ rexpr($p) ] -> [ $p ] +(* | form_eq [ rexpr($p) "==" rexpr($c) ] -> [ (eqT R $p $c) ] *) +| form_eq [ rexpr($p) "==" rexpr($c) ] -> [ (eqT ? $p $c) ] +| form_eq2 [ rexpr($p) "=" rexpr($c) ] -> [ (eqT ? $p $c) ] +| form_le [ rexpr($p) "<=" rexpr($c) ] -> [ (Rle $p $c) ] +| form_lt [ rexpr($p) "<" rexpr($c) ] -> [ (Rlt $p $c) ] +| form_ge [ rexpr($p) ">=" rexpr($c) ] -> [ (Rge $p $c) ] +| form_gt [ rexpr($p) ">" rexpr($c) ] -> [ (Rgt $p $c) ] +(* +| form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ] + -> [ (eqT R $p $c)/\(eqT R $c $c1) ] +*) +| form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ] + -> [ (eqT ? $p $c)/\(eqT ? $c $c1) ] +| form_le_le [ rexpr($p) "<=" rexpr($c) "<=" rexpr($c1) ] + -> [ (Rle $p $c)/\(Rle $c $c1) ] +| form_le_lt [ rexpr($p) "<=" rexpr($c) "<" rexpr($c1) ] + -> [ (Rle $p $c)/\(Rlt $c $c1) ] +| form_lt_le [ rexpr($p) "<" rexpr($c) "<=" rexpr($c1) ] + -> [ (Rlt $p $c)/\(Rle $c $c1) ] +| form_lt_lt [ rexpr($p) "<" rexpr($c) "<" rexpr($c1) ] + -> [ (Rlt $p $c)/\(Rlt $c $c1) ] +| form_neq [ rexpr($p) "<>" rexpr($c) ] -> [ ~(eqT ? $p $c) ] + +with rexpr : constr := + expr_plus [ rexpr($p) "+" rexpr($c) ] -> [ (Rplus $p $c) ] +| expr_minus [ rexpr($p) "-" rexpr($c) ] -> [ (Rminus $p $c) ] +| rexpr2 [ rexpr2($e) ] -> [ $e ] + +with rexpr2 : constr := + expr_mult [ rexpr2($p) "*" rexpr2($c) ] -> [ (Rmult $p $c) ] +| rexpr0 [ rexpr0($e) ] -> [ $e ] + + +with rexpr0 : constr := + expr_id [ constr:global($c) ] -> [ $c ] +| expr_com [ "[" constr:constr($c) "]" ] -> [ $c ] +| expr_appl [ "(" rapplication($a) ")" ] -> [ $a ] +| expr_num [ rnumber($s) ] -> [ $s ] +| expr_negnum [ "-" rnegnumber($n) ] -> [ $n ] +| expr_div [ rexpr0($p) "/" rexpr0($c) ] -> [ (Rdiv $p $c) ] +| expr_opp [ "-" rexpr0($c) ] -> [ (Ropp $c) ] +| expr_inv [ "/" rexpr0($c) ] -> [ (Rinv $c) ] +| expr_meta [ meta($m) ] -> [ $m ] + +with meta := +| rimpl [ "?" ] -> [ ? ] +| rmeta0 [ "?" "0" ] -> [ ?0 ] +| rmeta1 [ "?" "1" ] -> [ ?1 ] +| rmeta2 [ "?" "2" ] -> [ ?2 ] +| rmeta3 [ "?" "3" ] -> [ ?3 ] +| rmeta4 [ "?" "4" ] -> [ ?4 ] +| rmeta5 [ "?" "5" ] -> [ ?5 ] + +with rapplication : constr := + apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ] +| pair [ rexpr($p) "," rexpr($c) ] -> [ ($p, $c) ] +| appl0 [ rexpr($a) ] -> [ $a ]. + +Grammar constr constr0 := + r_in_com [ "``" rnatural:rformula($c) "``" ] -> [ $c ]. + +Grammar constr atomic_pattern := + r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [ $c ]. + +(*i* pp **) + +Syntax constr + level 0: + Rle [ (Rle $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2) "``"]] + | Rlt [ (Rlt $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "< "(REXPR $n2) "``" ]] + | Rge [ (Rge $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] ">= "(REXPR $n2) "``" ]] + | Rgt [ (Rgt $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "> "(REXPR $n2) "``" ]] + | Req [ (eqT R $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "= "(REXPR $n2)"``"]] + | Rneq [ ~(eqT R $n1 $n2) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "<> "(REXPR $n2) "``"]] + | Rle_Rle [ (Rle $n1 $n2)/\(Rle $n2 $n3) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2) + [1 0] "<= " (REXPR $n3) "``"]] + | Rle_Rlt [ (Rle $n1 $n2)/\(Rlt $n2 $n3) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "<= "(REXPR $n2) + [1 0] "< " (REXPR $n3) "``"]] + | Rlt_Rle [ (Rlt $n1 $n2)/\(Rle $n2 $n3) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2) + [1 0] "<= " (REXPR $n3) "``"]] + | Rlt_Rlt [ (Rlt $n1 $n2)/\(Rlt $n2 $n3) ] -> + [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2) + [1 0] "< " (REXPR $n3) "``"]] + | Rzero [ R0 ] -> [ "``0``" ] + | Rone [ R1 ] -> [ "``1``" ] + ; + + level 7: + Rplus [ (Rplus $n1 $n2) ] + -> [ [<hov 0> "``"(REXPR $n1):E "+" [0 0] (REXPR $n2):L "``"] ] + | Rodd_outside [(Rplus R1 $r)] -> [ $r:"r_printer_odd_outside"] + | Rminus [ (Rminus $n1 $n2) ] + -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ] + ; + + level 6: + Rmult [ (Rmult $n1 $n2) ] + -> [ [<hov 0> "``"(REXPR $n1):E "*" [0 0] (REXPR $n2):L "``"] ] + | Reven_outside [ (Rmult (Rplus R1 R1) $r) ] -> [ $r:"r_printer_even_outside"] + | Rdiv [ (Rdiv $n1 $n2) ] + -> [ [<hov 0> "``"(REXPR $n1):E "/" [0 0] (REXPR $n2):L "``"] ] + ; + + level 8: + Ropp [(Ropp $n1)] -> [ [<hov 0> "``" "-"(REXPR $n1):E "``"] ] + | Rinv [(Rinv $n1)] -> [ [<hov 0> "``" "/"(REXPR $n1):E "``"] ] + ; + + level 0: + rescape_inside [<< (REXPR $r) >>] -> [ "[" $r:E "]" ] + ; + + level 4: + Rappl_inside [<<(REXPR (APPLIST $h ($LIST $t)))>>] + -> [ [<hov 0> "("(REXPR $h):E [1 0] (RAPPLINSIDETAIL ($LIST $t)):E ")"] ] + | Rappl_inside_tail [<<(RAPPLINSIDETAIL $h ($LIST $t))>>] + -> [(REXPR $h):E [1 0] (RAPPLINSIDETAIL ($LIST $t)):E] + | Rappl_inside_one [<<(RAPPLINSIDETAIL $e)>>] ->[(REXPR $e):E] + | rpair_inside [<<(REXPR <<(pair $s1 $s2 $r1 $r2)>>)>>] + -> [ [<hov 0> "("(REXPR $r1):E "," [1 0] (REXPR $r2):E ")"] ] + ; + + level 3: + rvar_inside [<<(REXPR ($VAR $i))>>] -> [$i] + | rsecvar_inside [<<(REXPR (SECVAR $i))>>] -> [(SECVAR $i)] + | rconst_inside [<<(REXPR (CONST $c))>>] -> [(CONST $c)] + | rmutind_inside [<<(REXPR (MUTIND $i $n))>>] + -> [(MUTIND $i $n)] + | rmutconstruct_inside [<<(REXPR (MUTCONSTRUCT $c1 $c2 $c3))>>] + -> [ (MUTCONSTRUCT $c1 $c2 $c3) ] + | rimplicit_head_inside [<<(REXPR (XTRA "!" $c))>>] -> [ $c ] + | rimplicit_arg_inside [<<(REXPR (XTRA "!" $n $c))>>] -> [ ] + + ; + + + level 7: + Rplus_inside + [<<(REXPR <<(Rplus $n1 $n2)>>)>>] + -> [ (REXPR $n1):E "+" [0 0] (REXPR $n2):L ] + | Rminus_inside + [<<(REXPR <<(Rminus $n1 $n2)>>)>>] + -> [ (REXPR $n1):E "-" [0 0] (REXPR $n2):L ] + | NRplus_inside + [<<(REXPR <<(NRplus $r)>>)>>] -> [ "(" "1" "+" (REXPR $r):L ")"] + ; + + level 6: + Rmult_inside + [<<(REXPR <<(Rmult $n1 $n2)>>)>>] + -> [ (REXPR $n1):E "*" (REXPR $n2):L ] + | NRmult_inside + [<<(REXPR <<(NRmult $r)>>)>>] -> [ "(" "2" "*" (REXPR $r):L ")"] + ; + + level 5: + Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ " -" (REXPR $n1):E ] + | Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "/" (REXPR $n1):E ] + | Rdiv_inside + [<<(REXPR <<(Rdiv $n1 $n2)>>)>>] + -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ] + ; + + level 0: + Rzero_inside [<<(REXPR <<R0>>)>>] -> ["0"] + | Rone_inside [<<(REXPR <<R1>>)>>] -> ["1"] + | Rodd_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [ $r:"r_printer_odd" ] + | Reven_inside [<<(REXPR <<(Rmult (Rplus R1 R1) $r)>>)>>] -> [ $r:"r_printer_even" ] +. + +(* For parsing/printing based on scopes *) +Module R_scope. + +Infix "<=" Rle (at level 5, no associativity) : R_scope V8only. +Infix "<" Rlt (at level 5, no associativity) : R_scope V8only. +Infix ">=" Rge (at level 5, no associativity) : R_scope V8only. +Infix ">" Rgt (at level 5, no associativity) : R_scope V8only. +Infix "+" Rplus (at level 4) : R_scope V8only. +Infix "-" Rminus (at level 4) : R_scope V8only. +Infix "*" Rmult (at level 3) : R_scope V8only. +Infix "/" Rdiv (at level 3) : R_scope V8only. +Notation "- x" := (Ropp x) (at level 0) : R_scope V8only. +Notation "x == y == z" := (eqT R x y)/\(eqT R y z) + (at level 5, y at level 4, no associtivity): R_scope. +Notation "x <= y <= z" := (Rle x y)/\(Rle y z) + (at level 5, y at level 4) : R_scope + V8only. +Notation "x <= y < z" := (Rle x y)/\(Rlt y z) + (at level 5, y at level 4) : R_scope + V8only. +Notation "x < y < z" := (Rlt x y)/\(Rlt y z) + (at level 5, y at level 4) : R_scope + V8only. +Notation "x < y <= z" := (Rlt x y)/\(Rle y z) + (at level 5, y at level 4) : R_scope + V8only. +Notation "/ x" := (Rinv x) (at level 0): R_scope + V8only. + +Open Local Scope R_scope. +End R_scope. +]. |