diff options
Diffstat (limited to 'contrib/omega/OmegaSyntax.v')
| -rw-r--r-- | contrib/omega/OmegaSyntax.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v new file mode 100644 index 0000000000..dccfc5e890 --- /dev/null +++ b/contrib/omega/OmegaSyntax.v @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) +(* *) +(* Pierre Crégut (CNET, Lannion, France) *) +(* *) +(**************************************************************************) + +Grammar vernac vernac := + omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")] +| omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")] +| omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")] +| omega_unst [ "Unset" "Omega" "Time" "." ] -> [(OmegaFlag "-time")] +| omega_unss [ "Unset" "Omega" "System" "." ] -> [(OmegaFlag "-system")] +| omega_unsa [ "Unset" "Omega" "Action" "." ] -> [(OmegaFlag "-action")] +| omega_swit [ "Switch" "Omega" "Time" "." ] -> [(OmegaFlag "time")] +| omega_swis [ "Switch" "Omega" "System" "." ] -> [(OmegaFlag "system")] +| omega_swia [ "Switch" "Omega" "Action" "." ] -> [(OmegaFlag "action")] +| omega_set [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)]. + + +Grammar tactic simple_tactic := + omega [ "Omega" ] -> [(Omega)]. + +Syntax tactic level 0: + omega [(Omega)] -> ["Omega"]. |