helm/ocaml/cic_disambiguation/arit_notation.ml

   1 open Ast
   2 open Parser
   3
   4 EXTEND
   5   term: LEVEL "add"
   6     [
   7       [ t1 = term; SYMBOL "+"; t2 = term ->
   8           return_term loc (Appl [Ident ("plus", []); t1; t2])
   9       | t1 = term; SYMBOL "-"; t2 = term ->
  10           return_term loc (Appl [Ident ("minus", []); t1; t2])
  11       ]
  12     ];
  13   term: LEVEL "mult"
  14     [
  15       [ t1 = term; SYMBOL "*"; t2 = term ->
  16           return_term loc (Appl [Ident ("times", []); t1; t2])
  17       | t1 = term; SYMBOL "/"; t2 = term ->
  18           return_term loc (Appl [Ident ("div", []); t1; t2])
  19       ]
  20     ];
  21   term: LEVEL "inv"
  22     [
  23       [ SYMBOL "-"; t = term ->
  24         return_term loc (Appl [Ident ("uminus", []); t])
  25       ]
  26     ];
  27 END