Commit 0fb7ebe0 authored by Francois Bobot's avatar Francois Bobot

En fait cela marchait. Ajout de syntax type... et de builtins dans alt-ergo.drv

parent 32433ece
......@@ -7,31 +7,42 @@ printer "alt-ergo"
call_on_file "alt-ergo %s"
theory BuiltIn
syntax logic (_=_) "(%1 = %1)"
(* inutile car "<>" devient "not =" *)
syntax logic (_<>_) "(%1 = %1)"
end
theory prelude.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
syntax zero "0"
syntax logic zero "0"
syntax (_+_) "(%1 + %2)"
syntax (_-_) "(%1 - %2)"
syntax (_*_) "(%1 * %2)"
syntax (_/_) "(%1 / %2)"
syntax (-_) "(-%1)"
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
syntax logic (_*_) "(%1 * %2)"
syntax logic (_/_) "(%1 / %2)"
syntax logic (-_) "(-%1)"
syntax (_<=_) "(%1 <= %2)"
syntax (_< _) "(%1 < %2)"
syntax (_>=_) "(%1 >= %2)"
syntax (_> _) "(%1 > %2)"
syntax logic (_<=_) "(%1 <= %2)"
syntax logic (_< _) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_> _) "(%1 > %2)"
remove Mul_comm
remove One_neutral
remove prop Mul_comm
remove prop One_neutral
end
theory algebra.AC
tag cloned op "AC"
remove cloned Comm
remove cloned Assoc
tag logic cloned op "AC"
remove prop cloned Comm
remove prop cloned Assoc
end
(*
......
......@@ -75,11 +75,16 @@ let rec print_term drv fmt t = match t.t_node with
let rec print_fmla drv fmt f = match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
| Fapp (ls, [t1; t2]) when ls == ps_equ ->
fprintf fmt "(%a = %a)" (print_term drv) t1 (print_term drv) t2
| Fapp (ls, tl) ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma (print_term drv)) tl
begin
match Driver.query_ident drv ls.ls_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_term drv) fmt tl
| Driver.Tag _ ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma (print_term drv)) tl
end
| Fquant (q, fq) ->
let q = match q with Fforall -> "forall" | Fexists -> "exists" in
let vl, tl, f = f_open_quant fq in
......@@ -152,8 +157,15 @@ let print_logic_decl drv ctxt fmt = function
(print_list comma print_logic_binder) vl print_type ty (print_term drv) t;
List.iter forget_var vl
| Lpredicate (ls, None) ->
fprintf fmt "@[<hov 2>logic %a : %a -> prop@]"
print_ident ls.ls_name (print_list comma print_type) ls.ls_args
begin
match Driver.query_ident drv ls.ls_name with
| Driver.Remove -> ()
| Driver.Syntax _ -> ()
| Driver.Tag s ->
let sac = if Snm.mem "AC" s then "ac " else "" in
fprintf fmt "@[<hov 2>logic %s%a : %a -> prop@]" sac
print_ident ls.ls_name (print_list comma print_type) ls.ls_args
end
| Lpredicate (ls, Some fd) ->
let _,vl,f = open_ps_defn fd in
fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
......
......@@ -169,8 +169,7 @@ let string_of_qualid thl idl =
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
let check_syntax loc s ls =
let len = List.length ls.ls_args in
let check_syntax loc s len =
iter_group regexp_arg_pos
(fun s ->
let i = int_of_string (matched_group 1 s) in
......@@ -194,43 +193,68 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
with Not_found ->
let t23 = if cloned then (Tag Snm.empty),t else t,(Tag Snm.empty) in
Hid.add driver.drv_theory id t23 in
let rec find_lident ns = function
let rec find_l ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_ls
| a::l -> find_lident (Mnm.find a ns.ns_ns) l in
let rec find_tyident ns = function
| a::l -> find_l (Mnm.find a ns.ns_ns) l in
let rec find_ty ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_ts).ts_name
| a::l -> find_tyident (Mnm.find a ns.ns_ns) l in
let rec find_prident ns = function
| [a] -> Mnm.find a ns.ns_ts
| a::l -> find_ty (Mnm.find a ns.ns_ns) l in
let rec find_pr ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_pr).pr_name
| a::l -> find_prident (Mnm.find a ns.ns_ns) l in
| [a] -> Mnm.find a ns.ns_pr
| a::l -> find_pr (Mnm.find a ns.ns_ns) l in
let add = function
| Rremove (c,(loc,q)) ->
begin
try
add_htheory c (find_prident th.th_export q) Remove
add_htheory c (find_pr th.th_export q).pr_name Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
(string_of_qualid qualid q)
end
| Rsyntax ((loc,q),s) ->
| Rsyntaxls ((loc,q),s) ->
begin
try
let ls = (find_lident th.th_export q) in
check_syntax loc s ls;
let ls = (find_l th.th_export q) in
check_syntax loc s (List.length ls.ls_args);
add_htheory false ls.ls_name (Syntax s)
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
| Rtag (c,(loc,q),s) ->
| Rsyntaxty ((loc,q),s) ->
begin
try
add_htheory c (find_lident th.th_export q).ls_name
let ts = find_ty th.th_export q in
check_syntax loc s (List.length ts.ts_args);
add_htheory false ts.ts_name (Syntax s)
with Not_found -> errorm ~loc "Unknown type %s"
(string_of_qualid qualid q)
end
| Rtagls (c,(loc,q),s) ->
begin
try
add_htheory c (find_l th.th_export q).ls_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
| Rtagty (c,(loc,q),s) ->
begin
try
add_htheory c (find_ty th.th_export q).ts_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown type %s"
(string_of_qualid qualid q)
end
| Rtagpr (c,(loc,q),s) ->
begin
try
add_htheory c (find_pr th.th_export q).pr_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
end
| Rprelude (loc,s) -> if Hid.mem driver.drv_thprelude th.th_name
then errorm ~loc "duplicate prelude"
else Hid.add driver.drv_thprelude th.th_name s in
......
......@@ -25,8 +25,11 @@ type cloned = bool
type trule =
| Rremove of cloned * qualid
| Rsyntax of qualid * string
| Rtag of cloned * qualid * string
| Rsyntaxty of qualid * string
| Rsyntaxls of qualid * string
| Rtagty of cloned * qualid * string
| Rtagls of cloned * qualid * string
| Rtagpr of cloned * qualid * string
| Rprelude of loc * string
type theory_rules = {
......
......@@ -41,6 +41,9 @@
"invalid", INVALID;
"unknown", UNKNOWN;
"fail", FAIL;
"logic", LOGIC;
"type", TYPE;
"prop", PROP;
]
}
......
......@@ -32,6 +32,7 @@
%token THEORY END SYNTAX REMOVE TAG PRELUDE PRINTER CALL_ON_FILE CALL_ON_STDIN
%token VALID INVALID UNKNOWN FAIL
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
%token LOGIC TYPE PROP
%type <Driver_ast.file> file
%start file
......@@ -75,10 +76,13 @@ list0_trule:
;
trule:
| PRELUDE STRING { Rprelude (loc (),$2) }
| REMOVE cloned qualid { Rremove ($2, $3) }
| SYNTAX qualid STRING { Rsyntax ($2, $3) }
| TAG cloned qualid STRING { Rtag ($2, $3, $4) }
| PRELUDE STRING { Rprelude (loc (),$2) }
| REMOVE PROP cloned qualid { Rremove ($3, $4) }
| SYNTAX TYPE qualid STRING { Rsyntaxty ($3, $4) }
| SYNTAX LOGIC qualid STRING { Rsyntaxls ($3, $4) }
| TAG TYPE cloned qualid STRING { Rtagty ($3, $4, $5) }
| TAG LOGIC cloned qualid STRING { Rtagls ($3, $4, $5) }
| TAG PROP cloned qualid STRING { Rtagpr ($3, $4, $5) }
;
cloned:
......
......@@ -6,7 +6,8 @@ theory Test
use BuiltIn
logic id(x: int) : int = x
logic even(x: int) = 2*(x/2) = x
goal G : forall x:int. even(4 + 5)
goal G : forall x:int. even(4)
goal G2 : forall x:int. 4<>5
end
(*
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment