Commit 32433ece authored by Francois Bobot's avatar Francois Bobot
Browse files

ajout de la substitution pour syntaxe : marche pas

parent c417d728
......@@ -55,9 +55,9 @@ PDFVIEWER = @PDFVIEWER@
INCLUDES = -I src/core -I src/util -I src/parser -I src/output \
-I src/transform -I src
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa
COQC7 = @COQC7@
COQC8 = @COQC8@
......
......@@ -45,7 +45,7 @@ let rec print_type fmt ty = match ty.ty_node with
fprintf fmt "(%a) %a"
(print_list comma print_type) tyl print_ident ts.ts_name
let rec print_term fmt t = match t.t_node with
let rec print_term drv fmt t = match t.t_node with
| Tbvar _ ->
assert false
| Tconst c ->
......@@ -53,26 +53,33 @@ let rec print_term fmt t = match t.t_node with
| Tvar { vs_name = id } | Tapp ({ ls_name = id }, []) ->
print_ident fmt id
| Tapp (ls, tl) ->
fprintf fmt "%a(%a)"
print_ident ls.ls_name (print_list comma print_term) 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
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
print_term t1 print_term t2;
(print_term drv) t1 (print_term drv) t2;
forget_var v
| Tcase _ ->
assert false
| Teps _ ->
assert false
let rec print_fmla fmt f = match f.f_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 t1 print_term t2
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) tl
print_ident ls.ls_name (print_list comma (print_term drv)) tl
| Fquant (q, fq) ->
let q = match q with Fforall -> "forall" | Fexists -> "exists" in
let vl, tl, f = f_open_quant fq in
......@@ -80,35 +87,35 @@ let rec print_fmla fmt f = match f.f_node with
fprintf fmt "%s %a:%a" q print_ident v.vs_name print_type v.vs_ty
in
fprintf fmt "@[<hov2>(%a%a.@ %a)@]" (print_list dot forall) vl
(print_list alt print_triggers) tl print_fmla f;
(print_list alt (print_triggers drv)) tl (print_fmla drv) f;
List.iter forget_var vl
| Fbinop (Fand, f1, f2) ->
fprintf fmt "(%a and %a)" print_fmla f1 print_fmla f2
fprintf fmt "(%a and %a)" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (For, f1, f2) ->
fprintf fmt "(%a or %a)" print_fmla f1 print_fmla f2
fprintf fmt "(%a or %a)" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fimplies, f1, f2) ->
fprintf fmt "(%a -> %a)" print_fmla f1 print_fmla f2
fprintf fmt "(%a -> %a)" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fiff, f1, f2) ->
fprintf fmt "(%a <-> %a)" print_fmla f1 print_fmla f2
fprintf fmt "(%a <-> %a)" (print_fmla drv) f1 (print_fmla drv) f2
| Fnot f ->
fprintf fmt "(not %a)" print_fmla f
fprintf fmt "(not %a)" (print_fmla drv) f
| Ftrue ->
fprintf fmt "true"
| Ffalse ->
fprintf fmt "false"
| Fif (f1, f2, f3) ->
fprintf fmt "((%a and %a) or (not %a and %a))"
print_fmla f1 print_fmla f2 print_fmla f1 print_fmla f3
(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f1 (print_fmla drv) f3
| Flet _ ->
assert false
| Fcase _ ->
assert false
and print_trigger fmt = function
| TrTerm t -> print_term fmt t
| TrFmla f -> print_fmla fmt f
and print_trigger drv fmt = function
| TrTerm t -> (print_term drv) fmt t
| TrFmla f -> (print_fmla drv) fmt f
and print_triggers fmt tl = print_list comma print_trigger fmt tl
and print_triggers drv fmt tl = print_list comma (print_trigger drv) fmt tl
let print_logic_binder fmt v =
......@@ -124,22 +131,25 @@ let ac_th = ["algebra";"AC"]
let print_logic_decl drv ctxt fmt = function
| Lfunction (ls, None) ->
let sac = match Driver.query_ident drv ls.ls_name with
| Driver.Remove -> assert false (*TODO message *)
| Driver.Syntax _ -> assert false (*TODO substitution *)
| Driver.Tag s -> if Snm.mem "AC" s then "ac " else "" in
let tyl = ls.ls_args in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
sac
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
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
let tyl = ls.ls_args in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
sac
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
end
| Lfunction (ls, Some defn) ->
let id = ls.ls_name in
let _, vl, t = open_fs_defn defn in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
(print_list comma print_logic_binder) vl print_type ty print_term t;
(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@]"
......@@ -148,7 +158,7 @@ let print_logic_decl drv ctxt fmt = function
let _,vl,f = open_ps_defn fd in
fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
print_ident ls.ls_name
(print_list comma print_logic_binder) vl print_fmla f
(print_list comma print_logic_binder) vl (print_fmla drv) f
let print_decl drv ctxt fmt d = match d.d_node with
| Dtype dl ->
......@@ -160,10 +170,10 @@ let print_decl drv ctxt fmt d = match d.d_node with
Driver.query_ident drv pr.pr_name = Driver.Remove -> ()
| Dprop (Paxiom, pr) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla
print_ident pr.pr_name (print_fmla drv) pr.pr_fmla
| Dprop (Pgoal, pr) ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla
print_ident pr.pr_name (print_fmla drv) pr.pr_fmla
| Dprop (Plemma, _) ->
assert false
| Duse _ | Dclone _ ->
......@@ -175,6 +185,6 @@ let print_context drv fmt ctxt =
let () = Driver.register_printer "alt-ergo" print_context
let print_goal env fmt (id, f, ctxt) =
print_context env fmt ctxt;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id print_fmla f
let print_goal drv fmt (id, f, ctxt) =
print_context drv fmt ctxt;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
......@@ -24,6 +24,48 @@ open Theory
open Driver_ast
open Ident
(* Utils from Str *)
(* From global_substitute of str *)
open Str
let string_after s n fmt = pp_print_string fmt
(String.sub s n (String.length s - n))
let opt_search_forward re s pos =
try Some(search_forward re s pos) with Not_found -> None
let global_substitute expr repl_fun text fmt =
let rec replace start last_was_empty =
let startpos = if last_was_empty then start + 1 else start in
if startpos > String.length text then
string_after text start fmt
else
match opt_search_forward expr text startpos with
| None ->
string_after text start fmt
| Some pos ->
let end_pos = match_end() in
pp_print_string fmt (String.sub text start (pos-start));
repl_fun text fmt;
replace end_pos (end_pos = pos)
in
(replace 0 false)
let iter_group expr iter_fun text =
let rec iter start last_was_empty =
let startpos = if last_was_empty then start + 1 else start in
if startpos < String.length text then
match opt_search_forward expr text startpos with
| None -> ()
| Some pos ->
let end_pos = match_end() in
iter_fun text;
iter end_pos (end_pos = pos)
in
iter 0 false
(* *)
type error = string
exception Error of string
......@@ -125,6 +167,17 @@ let string_of_qualid thl idl =
let idl = String.concat "." idl in
thl^"."^idl
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
let check_syntax loc s ls =
let len = List.length ls.ls_args in
iter_group regexp_arg_pos
(fun s ->
let i = int_of_string (matched_group 1 s) in
if i=0 then errorm ~loc "invalid indice of argument : the first one is %%1 and not %%0";
if i>len then errorm ~loc "invalid indice of argument \"%%%i\" this logic has only %i argument" i len) s
let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
......@@ -143,7 +196,7 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
Hid.add driver.drv_theory id t23 in
let rec find_lident ns = function
| [] -> assert false
| [a] -> (Mnm.find a ns.ns_ls).ls_name
| [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
| [] -> assert false
......@@ -164,14 +217,17 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
| Rsyntax ((loc,q),s) ->
begin
try
add_htheory false (find_lident th.th_export q) (Syntax s)
let ls = (find_lident th.th_export q) in
check_syntax loc s ls;
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) ->
begin
try
add_htheory c (find_lident th.th_export q) (Tag (Snm.singleton s))
add_htheory c (find_lident th.th_export q).ls_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
......@@ -237,6 +293,14 @@ let query_ident drv id =
with Not_found -> acc) r tr in
Hid.add drv.drv_with_ctxt id tr;
tr
let syntax_arguments s print fmt l =
let args = Array.of_list l in
let repl_fun s fmt =
let i = int_of_string (matched_group 1 s) in
print fmt args.(i-1) in
global_substitute regexp_arg_pos repl_fun s fmt
(** using drivers *)
let print_context drv fmt ctxt = match drv.drv_printer with
......
......@@ -35,8 +35,10 @@ type translation =
| Tag of Snm.t
val query_ident : driver -> ident -> translation
(** registering printers *)
val syntax_arguments : string -> (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
(* syntax_argument templ print_arg fmt l print in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** registering printers *)
type printer = driver -> formatter -> context -> unit
......
......@@ -6,7 +6,7 @@ theory Test
use BuiltIn
logic id(x: int) : int = x
logic even(x: int) = 2*(x/2) = x
goal G : (0 : BuiltIn.int) = 0
goal G : forall x:int. even(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