From 99b99b0a3a68af8411df55b26018396e009fcc0c Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Wed, 29 Jun 2011 19:44:40 +0200 Subject: [PATCH] replace "logic" with "function" and "predicate" in drivers --- drivers/alt_ergo.drv | 81 ++++++++++++------------- drivers/alt_ergo_smt2.drv | 51 ++++++++-------- drivers/alt_ergo_trunk.drv | 5 +- drivers/coq.drv | 112 +++++++++++++++++------------------ drivers/cvc3_bare.drv | 71 +++++++++++----------- drivers/gappa.drv | 106 ++++++++++++++++----------------- drivers/simplify.drv | 22 +++---- drivers/tptp.drv | 2 +- drivers/vampire.drv | 2 +- drivers/verit.drv | 62 +++++++++---------- drivers/why3.drv | 2 +- drivers/why3_smt.drv | 8 +-- drivers/why3_tptp.drv | 2 +- drivers/yices_bare.drv | 62 +++++++++---------- drivers/z3_bare.drv | 80 ++++++++++++------------- drivers/z3_smtv1.drv | 62 +++++++++---------- src/driver/driver.ml | 22 ++++++- src/driver/driver_ast.ml | 6 +- src/driver/driver_lexer.mll | 3 +- src/driver/driver_parser.mly | 26 ++++---- 20 files changed, 405 insertions(+), 382 deletions(-) diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv index 41e005386..5085b96cf 100644 --- a/drivers/alt_ergo.drv +++ b/drivers/alt_ergo.drv @@ -30,25 +30,26 @@ transformation "simplify_formula" theory BuiltIn syntax type int "int" syntax type real "real" - syntax logic (=) "(%1 = %2)" + + syntax predicate (=) "(%1 = %2)" end theory int.Int prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (-_) "(-%1)" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (-_) "(-%1)" - syntax logic (<=) "(%1 <= %2)" - syntax logic (<) "(%1 < %2)" - syntax logic (>=) "(%1 >= %2)" - syntax logic (>) "(%1 > %2)" + syntax predicate (<=) "(%1 <= %2)" + syntax predicate (<) "(%1 < %2)" + syntax predicate (>=) "(%1 >= %2)" + syntax predicate (>) "(%1 > %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -69,8 +70,8 @@ end theory int.EuclideanDivision - syntax logic div "(%1 / %2)" - syntax logic mod "(%1 % %2)" + syntax function div "(%1 / %2)" + syntax function mod "(%1 % %2)" end @@ -79,20 +80,20 @@ theory real.Real prelude "(* this is a prelude for Alt-Ergo real arithmetic *)" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (/) "(%1 / %2)" - syntax logic (-_) "(-%1)" - syntax logic inv "(1.0 / %1)" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (/) "(%1 / %2)" + syntax function (-_) "(-%1)" + syntax function inv "(1.0 / %1)" - syntax logic (<=) "(%1 <= %2)" - syntax logic (<) "(%1 < %2)" - syntax logic (>=) "(%1 >= %2)" - syntax logic (>) "(%1 > %2)" + syntax predicate (<=) "(%1 <= %2)" + syntax predicate (<) "(%1 < %2)" + syntax predicate (>=) "(%1 >= %2)" + syntax predicate (>) "(%1 > %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -114,32 +115,32 @@ end theory real.RealInfix - syntax logic (+.) "(%1 + %2)" - syntax logic (-.) "(%1 - %2)" - syntax logic ( *.) "(%1 * %2)" - syntax logic (/.) "(%1 / %2)" - syntax logic (-._) "(-%1)" + syntax function (+.) "(%1 + %2)" + syntax function (-.) "(%1 - %2)" + syntax function ( *.) "(%1 * %2)" + syntax function (/.) "(%1 / %2)" + syntax function (-._) "(-%1)" - syntax logic (<=.) "(%1 <= %2)" - syntax logic (<.) "(%1 < %2)" - syntax logic (>=.) "(%1 >= %2)" - syntax logic (>.) "(%1 > %2)" + syntax predicate (<=.) "(%1 <= %2)" + syntax predicate (<.) "(%1 < %2)" + syntax predicate (>=.) "(%1 >= %2)" + syntax predicate (>.) "(%1 > %2)" end theory bool.Bool - syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" + syntax type bool "bool" + syntax function True "true" + syntax function False "false" end theory Tuple0 - syntax type tuple0 "unit" - syntax logic Tuple0 "void" + syntax type tuple0 "unit" + syntax function Tuple0 "void" end theory algebra.AC - meta cloned AC logic op + meta cloned AC function op remove cloned prop Comm.Comm remove cloned prop Assoc.Assoc end diff --git a/drivers/alt_ergo_smt2.drv b/drivers/alt_ergo_smt2.drv index 6e44dc4cf..9603758b5 100644 --- a/drivers/alt_ergo_smt2.drv +++ b/drivers/alt_ergo_smt2.drv @@ -25,7 +25,8 @@ transformation "encoding_smt" theory BuiltIn syntax type int "Int" syntax type real "Real" - syntax logic (=) "(= %1 %2)" + + syntax predicate (=) "(= %1 %2)" meta "encoding : kept" type int end @@ -34,18 +35,18 @@ theory int.Int prelude ";;; this is a prelude for Alt-Ergo integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -66,8 +67,8 @@ end theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" end @@ -75,20 +76,20 @@ theory real.Real prelude ";;; this is a prelude for Alt-Ergo real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (/) "(/ %1 %2)" + syntax function (-_) "(- %1)" + syntax function inv "(/ 1.0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc diff --git a/drivers/alt_ergo_trunk.drv b/drivers/alt_ergo_trunk.drv index 4f4dde4de..7ea3caec3 100644 --- a/drivers/alt_ergo_trunk.drv +++ b/drivers/alt_ergo_trunk.drv @@ -2,8 +2,9 @@ import "alt_ergo.drv" theory map.Map syntax type map "(%1,%2) farray" - syntax logic get "(%1[%2])" - syntax logic set "(%1[%2 <- %3])" + + syntax function get "(%1[%2])" + syntax function set "(%1[%2 <- %3])" end (* diff --git a/drivers/coq.drv b/drivers/coq.drv index 344bd3d0a..abc54c719 100644 --- a/drivers/coq.drv +++ b/drivers/coq.drv @@ -30,38 +30,38 @@ theory BuiltIn syntax type int "Z" syntax type real "R" - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" end theory bool.Bool syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" + syntax function True "true" + syntax function False "false" - syntax logic andb "(andb %1 %2)" - syntax logic orb "(orb %1 %2)" - syntax logic xorb "(xorb %1 %2)" - syntax logic notb "(negb %1)" + syntax function andb "(andb %1 %2)" + syntax function orb "(orb %1 %2)" + syntax function xorb "(xorb %1 %2)" + syntax function notb "(negb %1)" end theory int.Int - syntax logic zero "0%Z" - syntax logic one "1%Z" + syntax function zero "0%Z" + syntax function one "1%Z" - syntax logic (+) "(%1 + %2)%Z" - syntax logic (-) "(%1 - %2)%Z" - syntax logic (*) "(%1 * %2)%Z" - syntax logic (-_) "(-%1)%Z" + syntax function (+) "(%1 + %2)%Z" + syntax function (-) "(%1 - %2)%Z" + syntax function (*) "(%1 * %2)%Z" + syntax function (-_) "(-%1)%Z" - syntax logic (<=) "(%1 <= %2)%Z" - syntax logic (<) "(%1 < %2)%Z" - syntax logic (>=) "(%1 >= %2)%Z" - syntax logic (>) "(%1 > %2)%Z" + syntax predicate (<=) "(%1 <= %2)%Z" + syntax predicate (<) "(%1 < %2)%Z" + syntax predicate (>=) "(%1 >= %2)%Z" + syntax predicate (>) "(%1 > %2)%Z" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -83,14 +83,14 @@ end theory int.Abs - syntax logic abs "(Zabs %1)" + syntax function abs "(Zabs %1)" end theory int.MinMax - syntax logic min "(Zmin %1 %2)" - syntax logic max "(Zmax %1 %2)" + syntax function min "(Zmin %1 %2)" + syntax function max "(Zmax %1 %2)" end @@ -98,8 +98,8 @@ theory int.EuclideanDivision prelude "Require Import Zdiv." - syntax logic div "(Zdiv %1 %2)" - syntax logic mod "(Zmod %1 %2)" + syntax function div "(Zdiv %1 %2)" + syntax function mod "(Zmod %1 %2)" end @@ -107,28 +107,28 @@ theory int.ComputerDivision prelude "Require Import ZOdiv." - syntax logic div "(ZOdiv %1 %2)" - syntax logic mod "(ZOmod %1 %2)" + syntax function div "(ZOdiv %1 %2)" + syntax function mod "(ZOmod %1 %2)" end theory real.Real - syntax logic zero "0%R" - syntax logic one "1%R" + syntax function zero "0%R" + syntax function one "1%R" - syntax logic (+) "(%1 + %2)%R" - syntax logic (-) "(%1 - %2)%R" - syntax logic (-_) "(-%1)%R" - syntax logic (*) "(%1 * %2)%R" - syntax logic (/) "(Rdiv %1 %2)%R" - syntax logic inv "(Rinv %1)" + syntax function (+) "(%1 + %2)%R" + syntax function (-) "(%1 - %2)%R" + syntax function (-_) "(-%1)%R" + syntax function (*) "(%1 * %2)%R" + syntax function (/) "(Rdiv %1 %2)%R" + syntax function inv "(Rinv %1)" - syntax logic (<=) "(%1 <= %2)%R" - syntax logic (<) "(%1 < %2)%R" - syntax logic (>=) "(%1 >= %2)%R" - syntax logic (>) "(%1 > %2)%R" + syntax predicate (<=) "(%1 <= %2)%R" + syntax predicate (<) "(%1 < %2)%R" + syntax predicate (>=) "(%1 >= %2)%R" + syntax predicate (>) "(%1 > %2)%R" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -151,16 +151,16 @@ end theory real.RealInfix - syntax logic (+.) "(%1 + %2)%R" - syntax logic (-.) "(%1 - %2)%R" - syntax logic (-._) "(-%1)%R" - syntax logic ( *.) "(%1 * %2)%R" - syntax logic (/.) "(%1 / %2)%R" + syntax function (+.) "(%1 + %2)%R" + syntax function (-.) "(%1 - %2)%R" + syntax function (-._) "(-%1)%R" + syntax function ( *.) "(%1 * %2)%R" + syntax function (/.) "(%1 / %2)%R" - syntax logic (<=.) "(%1 <= %2)%R" - syntax logic (<.) "(%1 < %2)%R" - syntax logic (>=.) "(%1 >= %2)%R" - syntax logic (>.) "(%1 > %2)%R" + syntax predicate (<=.) "(%1 <= %2)%R" + syntax predicate (<.) "(%1 < %2)%R" + syntax predicate (>=.) "(%1 >= %2)%R" + syntax predicate (>.) "(%1 > %2)%R" end @@ -168,7 +168,7 @@ theory real.Abs prelude "Require Import Rbasic_fun." - syntax logic abs "(Rabs %1)" + syntax function abs "(Rabs %1)" remove prop Abs_pos @@ -176,7 +176,7 @@ end theory real.FromInt - syntax logic from_int "(IZR %1)" + syntax function from_int "(IZR %1)" end @@ -184,8 +184,8 @@ theory real.Square prelude "Require Import R_sqrt." - syntax logic sqr "(Rsqr %1)" - syntax logic sqrt "(sqrt %1)" (* and not Rsqrt *) + syntax function sqr "(Rsqr %1)" + syntax function sqrt "(sqrt %1)" (* and not Rsqrt *) end @@ -195,8 +195,8 @@ theory real.ExpLog prelude "Require Import Rtrigo_def." prelude "Require Import Rpower." - syntax logic exp "(exp %1)" - syntax logic log "(ln %1)" + syntax function exp "(exp %1)" + syntax function log "(ln %1)" remove prop Exp_zero remove prop Exp_sum @@ -220,12 +220,12 @@ theory real.Trigonometry prelude "Require Import Rtrigo." prelude "Require Import AltSeries. (* for def of pi *)" - syntax logic cos "(Rtrigo_def.cos %1)" - syntax logic sin "(Rtrigo_def.sin %1)" + syntax function cos "(Rtrigo_def.cos %1)" + syntax function sin "(Rtrigo_def.sin %1)" - syntax logic pi "PI" + syntax function pi "PI" - syntax logic tan "(Rtrigo.tan %1)" - (* syntax logic atan "atan not defined in Coq ?" *) + syntax function tan "(Rtrigo.tan %1)" + (* syntax function atan "atan not defined in Coq ?" *) end diff --git a/drivers/cvc3_bare.drv b/drivers/cvc3_bare.drv index 7e7600793..6d044e743 100644 --- a/drivers/cvc3_bare.drv +++ b/drivers/cvc3_bare.drv @@ -27,7 +27,7 @@ transformation "encoding_smt" theory BuiltIn syntax type int "INT" syntax type real "REAL" - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" meta "encoding : kept" type int end @@ -36,18 +36,18 @@ theory int.Int prelude "%%% this is a prelude for CVC3 integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(%1 <= %2)" - syntax logic (<) "(%1 < %2)" - syntax logic (>=) "(%1 >= %2)" - syntax logic (>) "(%1 > %2)" + syntax predicate (<=) "(%1 <= %2)" + syntax predicate (<) "(%1 < %2)" + syntax predicate (>=) "(%1 >= %2)" + syntax predicate (>) "(%1 > %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -71,21 +71,20 @@ theory real.Real prelude "%%% this is a prelude for CVC3 real arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (/) "(%1 / %2)" + syntax function (-_) "(- %1)" + syntax function inv "(1 / %1)" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (/) "(%1 / %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(1 / %1)" - - syntax logic (<=) "(%1 <= %2)" - syntax logic (<) "(%1 < %2)" - syntax logic (>=) "(%1 >= %2)" - syntax logic (>) "(%1 > %2)" + syntax predicate (<=) "(%1 <= %2)" + syntax predicate (<) "(%1 < %2)" + syntax predicate (>=) "(%1 >= %2)" + syntax predicate (>) "(%1 > %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -111,20 +110,20 @@ end (* L'encodage des types sommes bloquent cette théorie builtin *) theory bool.Bool syntax type bool "BITVECTOR(1)" - syntax logic True "0bin1" - syntax logic False "0bin0" - syntax logic andb "(%1 & %2)" - syntax logic orb "(%1 | %2)" - syntax logic xorb "(BVXOR(%1,%2))" - syntax logic notb "(~ %1)" + syntax function True "0bin1" + syntax function False "0bin0" + syntax function andb "(%1 & %2)" + syntax function orb "(%1 | %2)" + syntax function xorb "(BVXOR(%1,%2))" + syntax function notb "(~ %1)" meta cloned "encoding_decorate : kept" type bool end *) (* theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 @@ -135,11 +134,11 @@ end theory map.Map syntax type map "(ARRAY %1 OF %2)" - meta "encoding : lskept" logic get - meta "encoding : lskept" logic set + meta "encoding : lskept" function get + meta "encoding : lskept" function set - syntax logic get "(%1[%2])" - syntax logic set "(%1 WITH [%2] := %3)" + syntax function get "(%1[%2])" + syntax function set "(%1 WITH [%2] := %3)" end (* diff --git a/drivers/gappa.drv b/drivers/gappa.drv index 96da9dcc8..eeecd15a1 100644 --- a/drivers/gappa.drv +++ b/drivers/gappa.drv @@ -29,34 +29,34 @@ transformation "abstract_unknown_lsymbols" theory BuiltIn syntax type int "int" syntax type real "real" - syntax logic (=) "dummy" + syntax predicate (=) "dummy" end theory int.Int prelude "# this is a prelude for Gappa integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (-_) "(-%1)" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (-_) "(-%1)" - syntax logic (<=) "dummy" - syntax logic (>=) "dummy" - syntax logic (<) "dummy" - syntax logic (>) "dummy" + syntax predicate (<=) "dummy" + syntax predicate (>=) "dummy" + syntax predicate (<) "dummy" + syntax predicate (>) "dummy" - meta "gappa arith" logic (<=), "", "<=", ">=" - meta "gappa arith" logic (>=), "", ">=", "<=" - meta "gappa arith" logic (<), "not ", ">=", "<=" - meta "gappa arith" logic (>), "not ", "<=", ">=" + meta "gappa arith" predicate (<=), "", "<=", ">=" + meta "gappa arith" predicate (>=), "", ">=", "<=" + meta "gappa arith" predicate (<), "not ", ">=", "<=" + meta "gappa arith" predicate (>), "not ", "<=", ">=" - meta "inline : no" logic (<=) - meta "inline : no" logic (>=) - meta "inline : no" logic (>) + meta "inline : no" predicate (<=) + meta "inline : no" predicate (>=) + meta "inline : no" predicate (>) remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -75,19 +75,19 @@ end theory int.Abs - syntax logic abs "| %1 |" + syntax function abs "| %1 |" end theory int.EuclideanDivision - syntax logic div "int(%1 / %2)" + syntax function div "int(%1 / %2)" end theory int.ComputerDivision - syntax logic div "int(%1 / %2)" + syntax function div "int(%1 / %2)" end @@ -95,29 +95,29 @@ theory real.Real prelude "# this is a prelude for Gappa real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(%1 + %2)" - syntax logic (-) "(%1 - %2)" - syntax logic (*) "(%1 * %2)" - syntax logic (/) "(%1 / %2)" - syntax logic (-_) "(-%1)" - syntax logic inv "(1.0 / %1)" + syntax function (+) "(%1 + %2)" + syntax function (-) "(%1 - %2)" + syntax function (*) "(%1 * %2)" + syntax function (/) "(%1 / %2)" + syntax function (-_) "(-%1)" + syntax function inv "(1.0 / %1)" - syntax logic (<=) "dummy" - syntax logic (>=) "dummy" - syntax logic (<) "dummy" - syntax logic (>) "dummy" + syntax predicate (<=) "dummy" + syntax predicate (>=) "dummy" + syntax predicate (<) "dummy" + syntax predicate (>) "dummy" - meta "gappa arith" logic (<=), "", "<=", ">=" - meta "gappa arith" logic (>=), "", ">=", "<=" - meta "gappa arith" logic (<), "not ", ">=", "<=" - meta "gappa arith" logic (>), "not ", "<=", ">=" + meta "gappa arith" predicate (<=), "", "<=", ">=" + meta "gappa arith" predicate (>=), "", ">=", "<=" + meta "gappa arith" predicate (<), "not ", ">=", "<=" + meta "gappa arith" predicate (>), "not ", "<=", ">=" - meta "inline : no" logic (<=) - meta "inline : no" logic (>=) - meta "inline : no" logic (>) + meta "inline : no" predicate (<=) + meta "inline : no" predicate (>=) + meta "inline : no" predicate (>) remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -137,49 +137,49 @@ end theory real.Abs - syntax logic abs "| %1 |" + syntax function abs "| %1 |" end theory real.Square - syntax logic sqrt "sqrt(%1)" + syntax function sqrt "sqrt(%1)" end theory real.Truncate - syntax logic truncate "int(%1)" - syntax logic floor "int(%1)" - syntax logic ceil "int(%1)" + syntax function truncate "int(%1)" + syntax function floor "int(%1)" + syntax function ceil "int(%1)" end theory real.FromInt - syntax logic from_int "%1" + syntax function from_int "%1" end theory floating_point.Single - syntax logic round "float(%2)" + syntax function round "float(%2)" end theory floating_point.Double - syntax logic round "float(%2)" + syntax function round "float(%2)" end theory floating_point.Rounding - syntax logic NearestTiesToEven "ne" - syntax logic ToZero "zr" - syntax logic Up "up" - syntax logic Down "dn" - syntax logic NearTiesToAway "na" + syntax function NearestTiesToEven "ne" + syntax function ToZero "zr" + syntax function Up "up" + syntax function Down "dn" + syntax function NearTiesToAway "na" end diff --git a/drivers/simplify.drv b/drivers/simplify.drv index 3272f2495..63f1f23ad 100644 --- a/drivers/simplify.drv +++ b/drivers/simplify.drv @@ -31,7 +31,7 @@ trigger they can't appear since = can't appear *) transformation "encoding_tptp" theory BuiltIn - syntax logic (=) "(EQ %1 %2)" + syntax predicate (=) "(EQ %1 %2)" meta "enco_poly" "decorate" meta "encoding : kept" type int @@ -42,18 +42,18 @@ theory int.Int prelude ";;; this is a prelude for Simplify integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- 0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- 0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc diff --git a/drivers/tptp.drv b/drivers/tptp.drv index e20e55f6d..c9431dce9 100644 --- a/drivers/tptp.drv +++ b/drivers/tptp.drv @@ -31,7 +31,7 @@ transformation "eliminate_let" transformation "encoding_tptp" theory BuiltIn - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" end (* diff --git a/drivers/vampire.drv b/drivers/vampire.drv index 3b015bc99..ec00c884d 100644 --- a/drivers/vampire.drv +++ b/drivers/vampire.drv @@ -31,7 +31,7 @@ transformation "eliminate_let" transformation "encoding_tptp" theory BuiltIn - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" end (* diff --git a/drivers/verit.drv b/drivers/verit.drv index 8aa97cfc2..ab2d6c0df 100644 --- a/drivers/verit.drv +++ b/drivers/verit.drv @@ -27,7 +27,7 @@ transformation "encoding_sort" theory BuiltIn syntax type int "Int" syntax type real "Real" - syntax logic (=) "(= %1 %2)" + syntax predicate (=) "(= %1 %2)" meta "encoding : kept" type int end @@ -36,18 +36,18 @@ theory int.Int prelude ";;; this is a prelude for integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -71,20 +71,20 @@ theory real.Real prelude ";;; this is a prelude for real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (/) "(/ %1 %2)" + syntax function (-_) "(- %1)" + syntax function inv "(/ 1.0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -110,20 +110,20 @@ end (* L'encodage des types sommes bloquent cette théorie builtin *) theory bool.Bool syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" - syntax logic andb "(and %1 %2)" - syntax logic orb "(or %1 %2)" - syntax logic xorb "(xor %1 %2)" - syntax logic notb "(not %1)" + syntax function True "true" + syntax function False "false" + syntax function andb "(and %1 %2)" + syntax function orb "(or %1 %2)" + syntax function xorb "(xor %1 %2)" + syntax function notb "(not %1)" meta cloned "encoding_decorate : kept" type bool end *) theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 diff --git a/drivers/why3.drv b/drivers/why3.drv index 597369adf..84dd34a52 100644 --- a/drivers/why3.drv +++ b/drivers/why3.drv @@ -6,6 +6,6 @@ filename "%f-%t-%g.why" theory BuiltIn syntax type int "int" syntax type real "real" - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" end diff --git a/drivers/why3_smt.drv b/drivers/why3_smt.drv index a00596d4b..e01e76530 100644 --- a/drivers/why3_smt.drv +++ b/drivers/why3_smt.drv @@ -16,16 +16,16 @@ transformation "encoding_smt" theory BuiltIn syntax type int "int" syntax type real "real" - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" meta "encoding : kept" type int meta "encoding : kept" type real end theory map.Map - meta "encoding : lskept" logic get - meta "encoding : lskept" logic set - meta "encoding : lskept" logic const + meta "encoding : lskept" function get + meta "encoding : lskept" function set + meta "encoding : lskept" function const end import "discrimination.gen" diff --git a/drivers/why3_tptp.drv b/drivers/why3_tptp.drv index 5899d5292..66c5e4f72 100644 --- a/drivers/why3_tptp.drv +++ b/drivers/why3_tptp.drv @@ -16,5 +16,5 @@ transformation "discriminate" transformation "encoding_tptp" theory BuiltIn - syntax logic (=) "(%1 = %2)" + syntax predicate (=) "(%1 = %2)" end diff --git a/drivers/yices_bare.drv b/drivers/yices_bare.drv index b32f39384..0861fb1d4 100644 --- a/drivers/yices_bare.drv +++ b/drivers/yices_bare.drv @@ -28,7 +28,7 @@ transformation "encoding_sort" theory BuiltIn syntax type int "Int" syntax type real "Real" - syntax logic (=) "(= %1 %2)" + syntax predicate (=) "(= %1 %2)" meta "encoding : kept" type int end @@ -37,18 +37,18 @@ theory int.Int prelude ";;; this is a prelude for Yices integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -72,20 +72,20 @@ theory real.Real prelude ";;; this is a prelude for Yices real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (/) "(/ %1 %2)" + syntax function (-_) "(- %1)" + syntax function inv "(/ 1.0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -111,20 +111,20 @@ end (* L'encodage des types sommes bloquent cette théorie builtin *) theory bool.Bool syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" - syntax logic andb "(and %1 %2)" - syntax logic orb "(or %1 %2)" - syntax logic xorb "(xor %1 %2)" - syntax logic notb "(not %1)" + syntax function True "true" + syntax function False "false" + syntax function andb "(and %1 %2)" + syntax function orb "(or %1 %2)" + syntax function xorb "(xor %1 %2)" + syntax function notb "(not %1)" meta cloned "encoding_decorate : kept" type bool end *) (* theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 diff --git a/drivers/z3_bare.drv b/drivers/z3_bare.drv index 77708bc3f..a4473cb36 100644 --- a/drivers/z3_bare.drv +++ b/drivers/z3_bare.drv @@ -1,7 +1,7 @@ (* Why driver for SMT syntax *) prelude ";;; this is a prelude for Z3" -prelude "(set-logic AUFNIRA)" +prelude "(set-function AUFNIRA)" printer "smtv2" filename "%f-%t-%g.smt" @@ -29,7 +29,7 @@ transformation "encoding_smt" theory BuiltIn syntax type int "Int" syntax type real "Real" - syntax logic (=) "(= %1 %2)" + syntax predicate (=) "(= %1 %2)" meta "encoding : kept" type int end @@ -38,18 +38,18 @@ theory int.Int prelude ";;; this is a prelude for Z3 integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -73,20 +73,20 @@ theory real.Real prelude ";;; this is a prelude for Z3 real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (/) "(/ %1 %2)" + syntax function (-_) "(- %1)" + syntax function inv "(/ 1.0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -112,20 +112,20 @@ end (* L'encodage des types sommes bloquent cette théorie builtin *) theory bool.Bool syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" - syntax logic andb "(and %1 %2)" - syntax logic orb "(or %1 %2)" - syntax logic xorb "(xor %1 %2)" - syntax logic notb "(not %1)" + syntax function True "true" + syntax function False "false" + syntax function andb "(and %1 %2)" + syntax function orb "(or %1 %2)" + syntax function xorb "(xor %1 %2)" + syntax function notb "(not %1)" meta cloned "encoding_decorate : kept" type bool end *) theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 @@ -134,7 +134,7 @@ end (* theory real.FromInt - syntax logic from_int "(from_int %1)" + syntax function from_int "(from_int %1)" remove prop Add remove prop Sub remove prop Mul @@ -144,7 +144,7 @@ end (* theory real.Truncate - syntax logic floor "(to_int %1)" + syntax function floor "(to_int %1)" remove prop Floor_down remove prop Floor_monotonic end @@ -152,13 +152,13 @@ end theory map.Map syntax type map "(Array %1 %2)" - meta "encoding : lskept" logic get - meta "encoding : lskept" logic set - meta "encoding : lskept" logic const + meta "encoding : lskept" function get + meta "encoding : lskept" function set + meta "encoding : lskept" function const - syntax logic get "(select %1 %2)" - syntax logic set "(store %1 %2 %3)" - syntax logic const "(const[%t0] %1)" + syntax function get "(select %1 %2)" + syntax function set "(store %1 %2 %3)" + syntax function const "(const[%t0] %1)" end diff --git a/drivers/z3_smtv1.drv b/drivers/z3_smtv1.drv index 14b12fa0f..2b62c786c 100644 --- a/drivers/z3_smtv1.drv +++ b/drivers/z3_smtv1.drv @@ -28,7 +28,7 @@ transformation "encoding_sort" theory BuiltIn syntax type int "Int" syntax type real "Real" - syntax logic (=) "(= %1 %2)" + syntax predicate (=) "(= %1 %2)" meta "encoding : kept" type int end @@ -37,18 +37,18 @@ theory int.Int prelude ";;; this is a prelude for Z3 integer arithmetic" - syntax logic zero "0" - syntax logic one "1" + syntax function zero "0" + syntax function one "1" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (-_) "(- %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -72,20 +72,20 @@ theory real.Real prelude ";;; this is a prelude for Z3 real arithmetic" - syntax logic zero "0.0" - syntax logic one "1.0" + syntax function zero "0.0" + syntax function one "1.0" - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" + syntax function (+) "(+ %1 %2)" + syntax function (-) "(- %1 %2)" + syntax function (*) "(* %1 %2)" + syntax function (/) "(/ %1 %2)" + syntax function (-_) "(- %1)" + syntax function inv "(/ 1.0 %1)" - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" + syntax predicate (<=) "(<= %1 %2)" + syntax predicate (<) "(< %1 %2)" + syntax predicate (>=) "(>= %1 %2)" + syntax predicate (>) "(> %1 %2)" remove prop CommutativeGroup.Comm.Comm remove prop CommutativeGroup.Assoc.Assoc @@ -111,20 +111,20 @@ end (* L'encodage des types sommes bloquent cette théorie builtin *) theory bool.Bool syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" - syntax logic andb "(and %1 %2)" - syntax logic orb "(or %1 %2)" - syntax logic xorb "(xor %1 %2)" - syntax logic notb "(not %1)" + syntax function True "true" + syntax function False "false" + syntax function andb "(and %1 %2)" + syntax function orb "(or %1 %2)" + syntax function xorb "(xor %1 %2)" + syntax function notb "(not %1)" meta cloned "encoding_decorate : kept" type bool end *) theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" + syntax function div "(div %1 %2)" + syntax function mod "(mod %1 %2)" remove prop Mod_bound remove prop Div_mod remove prop Mod_1 diff --git a/src/driver/driver.ml b/src/driver/driver.ml index 1ec6344e8..cadd8012f 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -79,6 +79,8 @@ exception Duplicate of string exception UnknownType of (string list * string list) exception UnknownLogic of (string list * string list) exception UnknownProp of (string list * string list) +exception FSymExpected of lsymbol +exception PSymExpected of lsymbol let load_driver = let driver_tag = ref (-1) in fun env file -> let prelude = ref [] in @@ -129,6 +131,12 @@ let load_driver = let driver_tag = ref (-1) in fun env file -> let find_ts th (loc,q) = try ns_find_ts th.th_export q with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q))) in + let find_fs th q = + let ls = find_ls th q in + if ls.ls_value = None then raise (FSymExpected ls) else ls in + let find_ps th q = + let ls = find_ls th q in + if ls.ls_value <> None then raise (PSymExpected ls) else ls in let add_meta th td m = let s = try snd (Mid.find th.th_name !m) with Not_found -> Stdecl.empty in m := Mid.add th.th_name (th, Stdecl.add td s) !m @@ -140,8 +148,11 @@ let load_driver = let driver_tag = ref (-1) in fun env file -> | Rsyntaxts (c,q,s) -> let td = syntax_type (find_ts th q) s in add_meta th td (if c then meta_cl else meta) - | Rsyntaxls (c,q,s) -> - let td = syntax_logic (find_ls th q) s in + | Rsyntaxfs (c,q,s) -> + let td = syntax_logic (find_fs th q) s in + add_meta th td (if c then meta_cl else meta) + | Rsyntaxps (c,q,s) -> + let td = syntax_logic (find_ps th q) s in add_meta th td (if c then meta_cl else meta) | Rremovepr (c,q) -> let td = remove_prop (find_pr th q) in @@ -149,7 +160,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file -> | Rmeta (c,s,al) -> let convert = function | PMAts q -> MAts (find_ts th q) - | PMAls q -> MAls (find_ls th q) + | PMAfs q -> MAls (find_fs th q) + | PMAps q -> MAls (find_ps th q) | PMApr q -> MApr (find_pr th q) | PMAstr s -> MAstr s | PMAint i -> MAint i @@ -302,5 +314,9 @@ let () = Exn_printer.register (fun fmt exn -> match exn with "Unknown proposition %s" (string_of_qualid thl idl) | UnknownSpec s -> Format.fprintf fmt "Unknown format specifier '%%%s', use %%f, %%t or %%g" s + | FSymExpected ls -> Format.fprintf fmt + "%a is not a function symbol" Pretty.print_ls ls + | PSymExpected ls -> Format.fprintf fmt + "%a is not a predicate symbol" Pretty.print_ls ls | e -> raise e) diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml index 090cad465..8250ee717 100644 --- a/src/driver/driver_ast.ml +++ b/src/driver/driver_ast.ml @@ -25,7 +25,8 @@ type cloned = bool type metarg = | PMAts of qualid - | PMAls of qualid + | PMAfs of qualid + | PMAps of qualid | PMApr of qualid | PMAstr of string | PMAint of int @@ -33,7 +34,8 @@ type metarg = type th_rule = | Rprelude of string | Rsyntaxts of cloned * qualid * string - | Rsyntaxls of cloned * qualid * string + | Rsyntaxfs of cloned * qualid * string + | Rsyntaxps of cloned * qualid * string | Rremovepr of cloned * qualid | Rmeta of cloned * string * metarg list diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll index dbaec3e17..da405b675 100644 --- a/src/driver/driver_lexer.mll +++ b/src/driver/driver_lexer.mll @@ -47,7 +47,8 @@ "time", TIME; "unknown", UNKNOWN; "fail", FAIL; - "logic", LOGIC; + "function", FUNCTION; + "predicate", PREDICATE; "type", TYPE; "prop", PROP; "filename", FILENAME; diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly index 14a23c2c1..c1e17958b 100644 --- a/src/driver/driver_parser.mly +++ b/src/driver/driver_parser.mly @@ -36,7 +36,7 @@ %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER %token VALID INVALID TIMEOUT UNKNOWN FAIL TIME %token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF -%token LOGIC TYPE PROP FILENAME TRANSFORM PLUGIN +%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN %token LEFTPAR_STAR_RIGHTPAR COMMA %token LEFTSQ RIGHTSQ LARROW @@ -88,12 +88,13 @@ list0_trule: ; trule: -| PRELUDE STRING { Rprelude ($2) } -| SYNTAX cloned TYPE qualid STRING { Rsyntaxts ($2, $4, $5) } -| SYNTAX cloned LOGIC qualid STRING { Rsyntaxls ($2, $4, $5) } -| REMOVE cloned PROP qualid { Rremovepr ($2, $4) } -| META cloned ident meta_args { Rmeta ($2, $3, $4) } -| META cloned STRING meta_args { Rmeta ($2, $3, $4) } +| PRELUDE STRING { Rprelude ($2) } +| SYNTAX cloned TYPE qualid STRING { Rsyntaxts ($2, $4, $5) } +| SYNTAX cloned FUNCTION qualid STRING { Rsyntaxfs ($2, $4, $5) } +| SYNTAX cloned PREDICATE qualid STRING { Rsyntaxps ($2, $4, $5) } +| REMOVE cloned PROP qualid { Rremovepr ($2, $4) } +| META cloned ident meta_args { Rmeta ($2, $3, $4) } +| META cloned STRING meta_args { Rmeta ($2, $3, $4) } ; meta_args: @@ -102,11 +103,12 @@ meta_args: ; meta_arg: -| TYPE qualid { PMAts $2 } -| LOGIC qualid { PMAls $2 } -| PROP qualid { PMApr $2 } -| STRING { PMAstr $1 } -| INTEGER { PMAint $1 } +| TYPE qualid { PMAts $2 } +| FUNCTION qualid { PMAfs $2 } +| PREDICATE qualid { PMAps $2 } +| PROP qualid { PMApr $2 } +| STRING { PMAstr $1 } +| INTEGER { PMAint $1 } ; cloned: -- 2.24.1