Commit b12615b8 authored by Andrei Paskevich's avatar Andrei Paskevich

- accept metas in theories (see algebra.why) and drivers

- bring driver syntax closer to that of theories
- some simple API improvements
parent e11485f7
......@@ -25,10 +25,10 @@ transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
theory int.Int
......@@ -38,15 +38,15 @@ theory int.Int
syntax logic zero "0"
syntax logic one "1"
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
syntax logic (_*_) "(%1 * %2)"
syntax logic (-_) "(-%1)"
syntax logic (+) "(%1 + %2)"
syntax logic (-) "(%1 - %2)"
syntax logic (*) "(%1 * %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(%1 <= %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_>_) "(%1 > %2)"
syntax logic (<=) "(%1 <= %2)"
syntax logic (<) "(%1 < %2)"
syntax logic (>=) "(%1 >= %2)"
syntax logic (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -70,17 +70,17 @@ theory real.Real
syntax logic zero "0.0"
syntax logic 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 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 logic (_<=_) "(%1 <= %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_>_) "(%1 > %2)"
syntax logic (<=) "(%1 <= %2)"
syntax logic (<) "(%1 < %2)"
syntax logic (>=) "(%1 >= %2)"
syntax logic (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -110,7 +110,7 @@ theory Tuple0
end
theory algebra.AC
tag cloned logic op "AC"
meta cloned AC logic op
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
end
......
......@@ -13,23 +13,23 @@ theory BuiltIn
prelude "Require Import ZArith."
prelude "Require Import Rbase."
syntax type int "Z"
syntax type real "R"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "Z"
syntax type real "R"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax type bool "bool"
syntax logic True "true"
syntax logic True "true"
syntax logic 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 logic andb "(andb %1 %2)"
syntax logic orb "(orb %1 %2)"
syntax logic xorb "(xorb %1 %2)"
syntax logic notb "(negb %1)"
end
......@@ -37,17 +37,17 @@ end
theory int.Int
syntax logic zero "0%Z"
syntax logic one "1%Z"
syntax logic one "1%Z"
syntax logic (_+_) "(%1 + %2)%Z"
syntax logic (_-_) "(%1 - %2)%Z"
syntax logic (_*_) "(%1 * %2)%Z"
syntax logic (-_) "(-%1)%Z"
syntax logic (+) "(%1 + %2)%Z"
syntax logic (-) "(%1 - %2)%Z"
syntax logic (*) "(%1 * %2)%Z"
syntax logic (-_) "(-%1)%Z"
syntax logic (_<=_) "(%1 <= %2)%Z"
syntax logic (_<_) "(%1 < %2)%Z"
syntax logic (_>=_) "(%1 >= %2)%Z"
syntax logic (_>_) "(%1 > %2)%Z"
syntax logic (<=) "(%1 <= %2)%Z"
syntax logic (<) "(%1 < %2)%Z"
syntax logic (>=) "(%1 >= %2)%Z"
syntax logic (>) "(%1 > %2)%Z"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -72,19 +72,19 @@ end
theory real.Real
syntax logic zero "0%R"
syntax logic one "1%R"
syntax logic 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 (+) "(%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 logic (_<=_) "(%1 <= %2)%R"
syntax logic (_<_) "(%1 < %2)%R"
syntax logic (_>=_) "(%1 >= %2)%R"
syntax logic (_>_) "(%1 > %2)%R"
syntax logic (<=) "(%1 <= %2)%R"
syntax logic (<) "(%1 < %2)%R"
syntax logic (>=) "(%1 >= %2)%R"
syntax logic (>) "(%1 > %2)%R"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -117,8 +117,7 @@ theory real.Square
prelude "Require Import R_sqrt."
syntax logic sqr "(Rsqr %1)"
syntax logic sqr "(Rsqr %1)"
syntax logic sqrt "(sqrt %1)" (* and not Rsqrt *)
end
......@@ -130,7 +129,6 @@ theory real.ExpLog
prelude "Require Import Rpower."
syntax logic exp "(exp %1)"
syntax logic log "(ln %1)"
end
......
......@@ -23,10 +23,10 @@ transformation "simplify_trivial_quantification"
transformation "encoding_decorate"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(= %1 %2)"
syntax logic (_<>_) "(not (= %1 %2))"
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
syntax logic (<>) "(not (= %1 %2))"
end
theory int.Int
......@@ -35,15 +35,15 @@ theory int.Int
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -65,17 +65,17 @@ theory real.Real
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (_/_) "(/ %1 %2)"
syntax logic (-_) "(- %1)"
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 logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -96,20 +96,20 @@ end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
tag cloned type bool "encoding_decorate : kept"
syntax logic True "true"
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 logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
syntax logic notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
end
*)
theory transform.encoding_decorate.Kept
tag cloned type t "encoding_decorate : kept"
meta cloned "encoding_decorate : kept" type t
end
(*
......
......@@ -22,10 +22,10 @@ transformation "simplify_formula"
transformation "simplify_trivial_quantification"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
theory int.Int
......@@ -35,15 +35,15 @@ theory int.Int
syntax logic zero "0"
syntax logic one "1"
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
syntax logic (_*_) "(%1 * %2)"
syntax logic (-_) "(-%1)"
syntax logic (+) "(%1 + %2)"
syntax logic (-) "(%1 - %2)"
syntax logic (*) "(%1 * %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(%1 <= %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_>_) "(%1 > %2)"
syntax logic (<=) "(%1 <= %2)"
syntax logic (<) "(%1 < %2)"
syntax logic (>=) "(%1 >= %2)"
syntax logic (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -67,17 +67,17 @@ theory real.Real
syntax logic zero "0.0"
syntax logic 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 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 logic (_<=_) "(%1 <= %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_>_) "(%1 > %2)"
syntax logic (<=) "(%1 <= %2)"
syntax logic (<) "(%1 < %2)"
syntax logic (>=) "(%1 >= %2)"
syntax logic (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -95,8 +95,6 @@ theory real.Real
end
(*
Local Variables:
mode: why
......
......@@ -30,10 +30,10 @@ trigger they can't appear since = can't appear *)
(*transformation "encoding_decorate_mono"*)
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(EQ %1 %2)"
syntax logic (_<>_) "(NEQ %1 %2)"
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(EQ %1 %2)"
syntax logic (<>) "(NEQ %1 %2)"
end
theory int.Int
......@@ -42,15 +42,15 @@ theory int.Int
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(- 0 %1)"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (-_) "(- 0 %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -67,7 +67,7 @@ theory int.Int
end
theory transform.encoding_decorate.Kept
tag cloned type t "encoding_decorate : kept"
meta cloned "encoding_decorate : kept" type t
end
(*
......
......@@ -36,10 +36,10 @@ transformation "simple_types"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 != %2)"
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 != %2)"
end
(*
......
......@@ -2,8 +2,8 @@ printer "why3"
filename "%f-%t-%g.why"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
......@@ -11,8 +11,8 @@ transformation "eliminate_let"
transformation "encoding_decorate"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
......@@ -6,8 +6,8 @@ transformation "simplify_recursive_definition"
transformation "inline_all"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
......@@ -11,8 +11,8 @@ transformation "simplify_formula"
transformation "simplify_trivial_quantification"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (<>) "(%1 <> %2)"
end
......@@ -24,10 +24,10 @@ transformation "encoding_decorate"
(* transformation "encoding_decorate_every_simple" *)
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(= %1 %2)"
syntax logic (_<>_) "(not (= %1 %2))"
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
syntax logic (<>) "(not (= %1 %2))"
end
......@@ -37,15 +37,15 @@ theory int.Int
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -69,17 +69,17 @@ theory real.Real
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (_/_) "(/ %1 %2)"
syntax logic (-_) "(- %1)"
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 logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -100,14 +100,14 @@ end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
tag cloned type bool "encoding_decorate : kept"
syntax logic True "true"
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 logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
syntax logic notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
end
*)
......@@ -122,7 +122,7 @@ theory int.EuclideanDivision
end
theory transform.encoding_decorate.Kept
tag cloned type t "encoding_decorate : kept"
meta cloned "encoding_decorate : kept" type t
end
(*
......
......@@ -108,7 +108,8 @@ let syntax_arguments s print fmt l =
(** {2 use printers} *)
let print_prelude = print_list newline pp_print_string
let print_prelude fmt pl =
fprintf fmt "%a@\n" (print_list newline pp_print_string) pl
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
......@@ -132,6 +133,9 @@ let add_ls_syntax ls s sm =
if Mid.mem ls.ls_name sm then raise (KnownLogicSyntax ls);
Mid.add ls.ls_name s sm
let query_syntax sm id =
try Some (Mid.find id sm) with Not_found -> None
let meta_remove_type = "remove_type"
let meta_remove_logic = "remove_logic"
let meta_remove_prop = "remove_prop"
......
......@@ -59,6 +59,8 @@ val get_remove_set : task -> Sid.t
val add_ts_syntax : tysymbol -> string -> syntax_map -> syntax_map
val add_ls_syntax : lsymbol -> string -> syntax_map -> syntax_map
val query_syntax : syntax_map -> ident -> string option
val syntax_arguments : string -> 'a pp -> 'a list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
......
......@@ -208,7 +208,7 @@ let task_decls = task_fold (fun acc td ->
exception NotTaggingMeta of string
let find_meta_ids t tds acc =
let find_tagged t tds acc =
begin match lookup_meta t with
| [MTtysymbol|MTlsymbol|MTprsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
......
......@@ -97,7 +97,7 @@ val task_goal : task -> prsymbol
exception NotTaggingMeta of string
val find_meta_ids : string -> tdecl_set -> Sid.t -> Sid.t
val find_tagged : string -> tdecl_set -> Sid.t -> Sid.t
(* exceptions *)
......
......@@ -154,9 +154,17 @@ let transforms_l : (string, env -> task tlist) Hashtbl.t = Hashtbl.create 17
let register_transform s p =
if Hashtbl.mem transforms s then raise (KnownTrans s);
Hashtbl.replace transforms s (Wenv.memoize 3 p)
Hashtbl.replace transforms s (fun _ -> p)
let register_transform_l s p =
if Hashtbl.mem transforms_l s then raise (KnownTrans s);
Hashtbl.replace transforms_l s (fun _ -> p)
let register_env_transform s p =
if Hashtbl.mem transforms s then raise (KnownTrans s);
Hashtbl.replace transforms s (Wenv.memoize 3 p)
let register_env_transform_l s p =
if Hashtbl.mem transforms_l s then raise (KnownTrans s);
Hashtbl.replace transforms_l s (Wenv.memoize 3 p)
......
......@@ -77,8 +77,11 @@ val on_theories_metas : theory list -> string list ->
exception UnknownTrans of string
exception KnownTrans of string
val register_transform : string -> (Env.env -> task trans) -> unit
val register_transform_l : string -> (Env.env -> task tlist) -> unit
val register_env_transform : string -> (Env.env -> task trans) -> unit
val register_env_transform_l : string -> (Env.env -> task tlist) -> unit
val register_transform : string -> task trans -> unit
val register_transform_l : string -> task tlist -> unit
val lookup_transform : string -> Env.env -> task trans
val lookup_transform_l : string -> Env.env -> task tlist
......
......@@ -136,14 +136,15 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
| Rremovepr (c,q) ->
let td = remove_prop (find_pr th q) in
add_meta th td (if c then meta_cl else meta)
| Rtagts (c,q,s) ->
let td = create_meta s [MAts (find_ts th q)] in
add_meta th td (if c then meta_cl else meta)
| Rtagls (c,q,s) ->
let td = create_meta s [MAls (find_ls th q)] in
add_meta th td (if c then meta_cl else meta)
| Rtagpr (c,q,s) ->
let td = create_meta s [MApr (find_pr th q)] in
| Rmeta (c,s,al) ->
let convert = function
| PMAts q -> MAts (find_ts th q)
| PMAls q -> MAls (find_ls th q)
| PMApr q -> MApr (find_pr th q)
| PMAstr s -> MAstr s
| PMAint i -> MAint i
in
let td = create_meta s (List.map convert al) in
add_meta th td (if c then meta_cl else meta)
in
let add_local th (loc,rule) =
......
......@@ -23,14 +23,19 @@ type qualid = loc * string list
type cloned = bool
type metarg =
| PMAts of qualid
| PMAls of qualid
| PMApr of qualid
| PMAstr of string
| PMAint of int
type th_rule =
| Rprelude of string
| Rsyntaxts of qualid * string
| Rsyntaxls of qualid * string
| Rremovepr of cloned * qualid
| Rtagts of cloned * qualid * string
| Rtagls of cloned * qualid * string
| Rtagpr of cloned * qualid * string
| Rmeta of cloned * string * metarg list
type theory_rules = {
thr_name : qualid;
......
......@@ -24,14 +24,14 @@
open Lexer
let keywords = Hashtbl.create 97
let () =
List.iter
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[ "theory", THEORY;
"end", END;
"syntax", SYNTAX;
"remove", REMOVE;
"tag", TAG;
"meta", META;
"cloned", CLONED;
"prelude", PRELUDE;
"printer", PRINTER;
......@@ -55,33 +55,37 @@ let alpha = ['a'-'z' 'A'-'Z' '_']
let digit = ['0'-'9']
let ident = alpha (alpha | digit | '\'')*
let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%'
'!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
rule token = parse
| '\n'
{ newline lexbuf; token lexbuf }
| space+
| space+
{ token lexbuf }
| "(*)"
{ LEFTPAR_STAR_RIGHTPAR }
| "(*"
{ comment lexbuf; token lexbuf }
| '_'
| '_'
{ UNDERSCORE }
| ident as id
{ try Hashtbl.find keywords id with Not_found -> IDENT id }
| digit+ as i
{ INTEGER (int_of_string i) }
| "<>" | "<" | "<=" | ">" | ">="
| "="
| "+" | "-"
| "*" | "/" | "%" as op
{ OPERATOR op }
| "("
{ LEFTPAR }
| ")"
{ RIGHTPAR }
| "."
{ DOT }
| ","
{ COMMA }
| op_char+ as op
{ OPERATOR op }
| "\""
{ STRING (string lexbuf) }
| eof