X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fsamples.ma;h=46193bf73d90aea14c1493fb1e85fa7f998799a9;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=f0a75667c18fea4c86ac3d701cfcdead72100986;hpb=ec54d490477ece51c19d79750dda9805ffda663c;p=helm.git

diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma
index f0a75667c..46193bf73 100644
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -1,3 +1,82 @@
+
+notation
+  "\langle a , b \rangle"
+for
+  @{ 'pair $a $b }.
+print \langle 1, \langle 2, 3 \rangle \rangle.
+print 'pair 1 ('pair 2 ('pair 3 4)).
+
+notation
+  "a :: b"
+for
+  @{ 'cons $a $b }.
+print 1 :: 2 :: 'ugo.
+
+notation
+  "[ hovbox (list0 a sep ; ) ]"
+for ${
+  fold right
+    @'nil
+  rec acc
+    @{ 'cons $a $acc }
+}.
+print [1;2;3;4].
+
+notation
+  "[ list1 a sep ; | b ]"
+for ${
+  if @{ 'cons $_ $_ } then
+    fold right
+      if @'nil then
+        fail
+      else if @{ 'cons $_ $_ } then
+        fail
+      else
+        b
+    rec acc
+      @{ 'cons $a $acc }
+  else
+    fail
+}.
+print 'cons 1 ('cons 2 ('cons 3 'ugo)).
+print 'cons 1 ('cons 2 ('cons 3 'nil)).
+print [1;2;3;4].
+print [1;2;3;4|5].
+
+notation "a + b" left associative for @{ 'plus $a $b }.
+print 1 + 2 + 3.
+print 1 + (2 + 3).
+
+notation
+  "'if' a 'then' b 'else' c"
+for
+  @{ 'ifthenelse $a $b $c }.
+print if even then x else bump x.
+
+notation
+  "a \vee b"
+for
+  @{ if $a > $b then $a else $b }
+
+notation
+  "'fun' ident x \to a"
+  right associative with precedence 20
+for
+  @{ 'lambda ${ident x} $a }.
+
+NOTES
+
+@a e' un'abbreviazione per @{term a}
+"x" e' un'abbreviazione per @{keyword x}
+@_ e' un'abbreviazione per @{anonymous}
+
+\x simbolo della sintassi concreta
+'x simbolo della sintassi astratta
+
+\lbrace \rbrace per le parentesi graffe al livello 1
+
+OLD SAMPLES
+
 # sample mappings level 1 <--> level 2
 
 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
@@ -6,7 +85,7 @@ print 1 ++ 2.
 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
 print + 1 2 3 4.
 
-notation \[ [ \LIST0 \TERM a \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
+notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
 print [].
 print [1;2;3;4].
 
@@ -25,6 +104,7 @@ interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
+notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
 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)).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
@@ -35,8 +115,8 @@ print 1 + 2.
 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
-notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
-notation \[ \TERM a * \TERM b \] for 'mult \TERM a \TERM b.
+notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
+notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.