drivers (en cours)

parent 49c92bbd
......@@ -8,6 +8,7 @@ theory prelude.Int
"(* this is a prelude for Alt-Ergo arithmetic *)"
syntax zero "0"
syntax (_+_) "(%1 + %2)"
syntax (_-_) "(%1 - %2)"
syntax (_*_) "(%1 * %2)"
......@@ -23,6 +24,10 @@ theory prelude.Int
remove One_neutral
end
theory algebra.AC
tag cloned op "AC"
end
(*
Local Variables:
mode: why
......
......@@ -86,6 +86,8 @@ let type_file env file =
let extract_goals ctxt =
Transform.apply Transform.extract_goals ctxt
let driver_rules = ref Driver.empty_rules
let transform env l =
let l = List.map
(fun t -> t, Context.use_export Context.create_context t)
......@@ -96,8 +98,11 @@ let transform env l =
(fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
else if !alt_ergo then match l with
| (_,ctxt) :: _ -> begin match extract_goals ctxt with
| g :: _ -> Alt_ergo.print_goal env std_formatter g
| [] -> eprintf "no goal@."
| g :: _ ->
let drv = Driver.create !driver_rules ctxt in
Alt_ergo.print_goal drv std_formatter g
| [] ->
eprintf "no goal@."
end
| [] -> ()
......@@ -105,7 +110,7 @@ let handle_file env file =
if Filename.check_suffix file ".why" then
type_file env file
else if Filename.check_suffix file ".drv" then begin
ignore (Driver.load file);
driver_rules := Driver.load file;
env
end else begin
eprintf "%s: don't know what to do with file %s@." Sys.argv.(0) file;
......@@ -121,6 +126,12 @@ let () =
eprintf "%a@." report e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C .. test"
End:
*)
(****
#load "hashcons.cmo";;
......
......@@ -125,12 +125,12 @@ let print_type_decl fmt = function
let ac_th = ["algebra";"AC"]
open Transform_utils
let print_logic_decl env ctxt fmt = function
let print_logic_decl drv ctxt fmt = function
| Lfunction (ls, None) ->
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"
(if cloned_from_ls env ctxt ac_th "op" ls then "ac " else "")
fprintf fmt "@[<hov 2>logic %a : %a -> %a@]@\n"
(*(if cloned_from_ls env ctxt ac_th "op" ls then "ac " else "") *)
print_ident ls.ls_name
(print_list comma print_type) tyl print_type ty
| Lfunction (ls, Some defn) ->
......@@ -149,16 +149,16 @@ let print_logic_decl env ctxt fmt = function
print_ident ls.ls_name
(print_list comma print_logic_binder) vl print_fmla f
let print_decl env ctxt fmt d = match d.d_node with
let print_decl drv ctxt fmt d = match d.d_node with
| Dtype dl ->
print_list newline print_type_decl fmt dl
| Dlogic dl ->
print_list newline (print_logic_decl env ctxt) fmt dl
print_list newline (print_logic_decl drv ctxt) fmt dl
| Dind _ ->
assert false
| Dprop (Paxiom, pr) when
(cloned_from_pr env ctxt ac_th "Comm" pr
|| cloned_from_pr env ctxt ac_th "Assoc" pr) -> ()
(* | Dprop (Paxiom, pr) when *)
(* (cloned_from_pr drv ctxt ac_th "Comm" pr *)
(* || cloned_from_pr env ctxt ac_th "Assoc" pr) -> () *)
| Dprop (Paxiom, pr) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name print_fmla pr.pr_fmla
......
......@@ -26,6 +26,6 @@ val print_term : formatter -> term -> unit
val print_fmla : formatter -> fmla -> unit
val print_context : Typing.env -> formatter -> context -> unit
val print_context : Driver.t -> formatter -> context -> unit
val print_goal : Typing.env -> formatter -> ident * fmla * context -> unit
val print_goal : Driver.t -> formatter -> ident * fmla * context -> unit
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
type t
type t = unit
type translation =
| Remove
......@@ -25,18 +25,26 @@ type translation =
| Tag of string list
type rules = unit
let empty_rules = ()
let load file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let f = Driver_lexer.parse_file lb in
let _f = Driver_lexer.parse_file lb in
close_in c;
()
let create rules ctxt =
assert false (*TODO*)
(* TODO *)
()
let ident dr id =
assert false (*TODO*)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
End:
*)
......@@ -31,6 +31,8 @@ val ident : t -> ident -> translation
type rules
val empty_rules : rules
val load : string -> rules
val create : rules -> context -> t
......
......@@ -19,18 +19,16 @@
type loc = Loc.position
type ident = { id : string; loc : loc }
type ident = Ptree.ident
type qualid =
| Qident of ident
| Qdot of qualid * ident
type qualid = Ptree.qualid
type star = bool
type cloned = bool
type trule =
| Rremove of star * qualid
| Rremove of cloned * qualid
| Rsyntax of qualid * string
| Rtag of star * qualid * string
| Rtag of cloned * qualid * string
type theory_rules = {
th_name : qualid;
......
......@@ -43,6 +43,7 @@
"syntax", SYNTAX;
"remove", REMOVE;
"tag", TAG;
"cloned", CLONED;
]
let newline lexbuf =
......
......@@ -18,6 +18,7 @@
/**************************************************************************/
%{
open Ptree
open Driver_ast
open Parsing
let loc () = (symbol_start_pos (), symbol_end_pos ())
......@@ -29,7 +30,7 @@
%token <string> STRING
%token <string> OPERATOR
%token THEORY END SYNTAX REMOVE TAG
%token UNDERSCORE LEFTPAR RIGHTPAR STAR DOT EOF
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
%type <Driver_ast.file> file
%start file
......@@ -62,13 +63,14 @@ list0_trule:
;
trule:
| REMOVE star qualid { Rremove ($2, $3) }
| SYNTAX qualid STRING { Rsyntax ($2, $3) }
| REMOVE cloned qualid { Rremove ($2, $3) }
| SYNTAX qualid STRING { Rsyntax ($2, $3) }
| TAG cloned qualid STRING { Rtag ($2, $3, $4) }
;
star:
cloned:
| /* epsilon */ { false }
| STAR { true }
| CLONED { true }
;
qualid:
......@@ -78,12 +80,12 @@ qualid:
ident:
| IDENT
{ { id = $1; loc = loc () } }
{ { id = $1; id_loc = loc () } }
| STRING
{ { id = $1; loc = loc () } }
{ { id = $1; id_loc = loc () } }
| LEFTPAR UNDERSCORE OPERATOR UNDERSCORE RIGHTPAR
{ { id = infix $3; loc = loc () } }
{ { id = infix $3; id_loc = loc () } }
| LEFTPAR OPERATOR UNDERSCORE RIGHTPAR
{ { id = prefix $2; loc = loc () } }
{ { id = prefix $2; id_loc = loc () } }
;
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