helm/ocaml/cic_notation/doc/samples.ma

   1
   2 notation
   3   "\langle a , b \rangle"
   4 for
   5   @{ 'pair $a $b }.
   6 print \langle 1, \langle 2, 3 \rangle \rangle.
   7 print 'pair 1 ('pair 2 ('pair 3 4)).
   8
   9 notation
  10   "a :: b"
  11 for
  12   @{ 'cons $a $b }.
  13 print 1 :: 2 :: 'ugo.
  14
  15 notation
  16   "[ hovbox (list0 a sep ; ) ]"
  17 for ${
  18   fold right
  19     @'nil
  20   rec acc
  21     @{ 'cons $a $acc }
  22 }.
  23 print [1;2;3;4].
  24
  25 notation
  26   "[ list1 a sep ; | b ]"
  27 for ${
  28   if @{ 'cons $_ $_ } then
  29     fold right
  30       if @'nil then
  31         fail
  32       else if @{ 'cons $_ $_ } then
  33         fail
  34       else
  35         b
  36     rec acc
  37       @{ 'cons $a $acc }
  38   else
  39     fail
  40 }.
  41 print 'cons 1 ('cons 2 ('cons 3 'ugo)).
  42 print 'cons 1 ('cons 2 ('cons 3 'nil)).
  43 print [1;2;3;4].
  44 print [1;2;3;4|5].
  45
  46 notation "a + b" left associative for @{ 'plus $a $b }.
  47 print 1 + 2 + 3.
  48 print 1 + (2 + 3).
  49
  50 notation
  51   "'if' a 'then' b 'else' c"
  52 for
  53   @{ 'ifthenelse $a $b $c }.
  54 print if even then x else bump x.
  55
  56 notation
  57   "a \vee b"
  58 for
  59   @{ if $a > $b then $a else $b }
  60
  61 notation
  62   "'fun' ident x \to a"
  63   right associative with precedence 20
  64 for
  65   @{ 'lambda ${ident x} $a }.
  66
  67 NOTES
  68
  69 @a e' un'abbreviazione per @{term a}
  70 "x" e' un'abbreviazione per @{keyword x}
  71 @_ e' un'abbreviazione per @{anonymous}
  72
  73 \x simbolo della sintassi concreta
  74 'x simbolo della sintassi astratta
  75
  76 \lbrace \rbrace per le parentesi graffe al livello 1
  77
  78 OLD SAMPLES
  79
  80 # sample mappings level 1 <--> level 2
  81
  82 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
  83 print 1 ++ 2.
  84
  85 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
  86 print + 1 2 3 4.
  87
  88 notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
  89 print [].
  90 print [1;2;3;4].
  91
  92 notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
  93 print [].
  94 print [1;2].
  95 print [1;2;3;4].
  96
  97 notation \[ | \LIST0 \[ \TERM a \OPT \[ , \TERM b \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ \TERM a \] \[ ('pair \TERM a \TERM b) \] \TERM acc \] .
  98
  99 notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
 100
 101 # sample mappings level 2 <--> level 3
 102
 103 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 104 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 105 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 106
 107 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
 108 interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).
 109 render cic:/Coq/Arith/Plus/plus_comm.con.
 110
 111 # full samples
 112
 113 notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
 114 print 1 + 2.
 115 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 116 render cic:/Coq/Arith/Plus/plus_comm.con.
 117
 118 notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
 119 notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
 120 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 121 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 122 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 123
 124 notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
 125