From 6689cec788d9fb12e7717055c1ea6490389f7d35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Thu, 15 Feb 2018 15:20:17 +0100 Subject: [PATCH] [Driver] add use export to force importation of a theory use it for converting ComputerDivision to EuclideanDivision --- drivers/alt_ergo_common.drv | 15 +------ src/driver/driver.ml | 85 ++++++++++++++++++++++++------------ src/driver/driver_ast.ml | 1 + src/driver/driver_lexer.mll | 2 + src/driver/driver_parser.mly | 3 +- theories/for_drivers.why | 19 ++++++++ 6 files changed, 83 insertions(+), 42 deletions(-) create mode 100644 theories/for_drivers.why diff --git a/drivers/alt_ergo_common.drv b/drivers/alt_ergo_common.drv index 757462feb..fb4dccf1f 100644 --- a/drivers/alt_ergo_common.drv +++ b/drivers/alt_ergo_common.drv @@ -98,20 +98,7 @@ end theory int.ComputerDivision - prelude "logic comp_div: int, int -> int" - prelude "axiom comp_div_def1: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y" - prelude "axiom comp_div_def2: forall x, y:int. x <= 0 and y > 0 -> comp_div(x,y) = - ((-x) / y)" - prelude "axiom comp_div_def3: forall x, y:int. x >= 0 and y < 0 -> comp_div(x,y) = - (x / (-y)))" - prelude "axiom comp_div_def4: forall x, y:int. x <= 0 and y < 0 -> comp_div(x,y) = (-x) / (-y)" - - prelude "logic comp_mod: int, int -> int" - prelude "axiom comp_mod_def1: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y" - prelude "axiom comp_mod_def2: forall x, y:int. x <= 0 and y > 0 -> comp_mod(x,y) = -((-x) % y)" - prelude "axiom comp_mod_def3: forall x, y:int. x >= 0 and y < 0 -> comp_mod(x,y) = x % (-y)" - prelude "axiom comp_mod_def4: forall x, y:int. x <= 0 and y < 0 -> comp_mod(x,y) = -((-x) % (-y)" - - syntax function div "comp_div(%1,%2)" - syntax function mod "comp_mod(%1,%2)" + use export for_drivers.ComputerOfEuclideanDivision end diff --git a/src/driver/driver.ml b/src/driver/driver.ml index 031bd4e5d..009ca3e1d 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -30,6 +30,7 @@ type driver = { drv_transform : string list; drv_prelude : prelude; drv_thprelude : prelude_map; + drv_thuse : (theory * theory) Mid.t; drv_blacklist : string list; drv_meta : (theory * Stdecl.t) Mid.t; drv_res_parser : prover_result_parser; @@ -118,6 +119,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files let thprelude = ref Mid.empty in let meta = ref Mid.empty in let qualid = ref [] in + let thuse = ref Mid.empty in let find_pr th (loc,q) = try ns_find_pr th.th_export q with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q))) @@ -138,34 +140,43 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files 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 in - let add_local th = function + (* th_uc is the theory built with the uses forced by the driver *) + let add_local th th_uc = function | Rprelude s -> let l = Mid.find_def [] th.th_name !thprelude in - thprelude := Mid.add th.th_name (s::l) !thprelude + thprelude := Mid.add th.th_name (s::l) !thprelude; + th_uc | Rsyntaxts (q,s,b) -> let td = syntax_type (find_ts th q) s b in - add_meta th td meta + add_meta th td meta; + th_uc | Rsyntaxfs (q,s,b) -> let td = syntax_logic (find_fs th q) s b in - add_meta th td meta + add_meta th td meta; + th_uc | Rsyntaxps (q,s,b) -> let td = syntax_logic (find_ps th q) s b in - add_meta th td meta + add_meta th td meta; + th_uc | Rremovepr (q) -> let td = remove_prop (find_pr th q) in - add_meta th td meta + add_meta th td meta; + th_uc | Rremoveall -> let it key _ = match (Mid.find key th.th_known).d_node with | Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta | _ -> () in - Mid.iter it th.th_local + Mid.iter it th.th_local; + th_uc | Rconverter (q,s,b) -> let cs = syntax_converter (find_ls th q) s b in - add_meta th cs meta + add_meta th cs meta; + th_uc | Rliteral (q,s,b) -> let cs = syntax_literal (find_ts th q) s b in - add_meta th cs meta + add_meta th cs meta; + th_uc | Rmeta (s,al) -> let rec ty_of_pty = function | PTyvar x -> @@ -190,14 +201,22 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files in let m = lookup_meta s in let td = create_meta m (List.map convert al) in - add_meta th td meta + add_meta th td meta; + th_uc + | Ruse (loc,q) -> + let file, th = Lists.chop_last q in + let th = Loc.try3 ~loc Env.read_theory env file th in + Theory.use_export th_uc th in - let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in + let add_local th th_uc (loc,rule) = Loc.try2 ~loc add_local th th_uc rule in let add_theory { thr_name = (loc,q); thr_rules = trl } = - let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in + let f,id = Lists.chop_last q in let th = Loc.try3 ~loc Env.read_theory env f id in + let th_uc = Theory.create_theory (Ident.id_fresh ~loc ("driver export for "^th.th_name.id_string)) in qualid := q; - List.iter (add_local th) trl + let th_uc' = List.fold_left (add_local th) th_uc trl in + if th_uc != th_uc' then + thuse := Mid.add th.th_name (th, Theory.close_theory th_uc') !thuse in List.iter add_theory f.f_rules; List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files; @@ -220,6 +239,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files prp_model_parser = Model_parser.lookup_model_parser !model_parser }; drv_tag = !driver_tag; + drv_thuse = !thuse; } let syntax_map drv = @@ -264,26 +284,37 @@ let call_on_buffer ~command ~limit exception NoPrinter -let update_task = let ht = Hint.create 5 in fun drv -> - let update task0 = - Mid.fold (fun _ (th,s) task -> - Task.on_theory th (fun task sm -> - Stdecl.fold (fun tdm task -> - add_tdecl task (clone_meta tdm sm) - ) s task - ) task task0 - ) drv.drv_meta task0 - in - function - | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal; - task_prev = task} -> +let update_task = + let ht = Hint.create 5 in fun drv -> + let update task0 = + (** add requested theories *) + let task0 = Mid.fold (fun _ (th,th') task -> + Task.on_theory th (fun task _sm -> + (** could we do some clone_export? *) + Task.use_export task th' + ) task task0 + ) drv.drv_thuse task0 + in + (** apply metas *) + let task0 = Mid.fold (fun _ (th,s) task -> + Task.on_theory th (fun task sm -> + Stdecl.fold (fun tdm task -> + add_tdecl task (clone_meta tdm sm) + ) s task + ) task task0 + ) drv.drv_meta task0 + in task0 + in + function + | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal; + task_prev = task} -> (* we cannot add metas nor memoize after goal *) let update = try Hint.find ht drv.drv_tag with Not_found -> let upd = Trans.store update in Hint.add ht drv.drv_tag upd; upd in let task = Trans.apply update task in add_tdecl task goal - | task -> update task + | task -> update task let add_cntexample_meta task cntexample = if not (cntexample) then task diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml index a41d1757d..e84d07777 100644 --- a/src/driver/driver_ast.ml +++ b/src/driver/driver_ast.ml @@ -36,6 +36,7 @@ type th_rule = | Rremovepr of qualid | Rremoveall | Rmeta of string * metarg list + | Ruse of qualid type theory_rules = { thr_name : qualid; diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll index d2e31ab4d..edc6f3f17 100644 --- a/src/driver/driver_lexer.mll +++ b/src/driver/driver_lexer.mll @@ -58,6 +58,8 @@ "val", VAL; "converter", CONVERTER; "literal", LITERAL; + "use", USE; + "export", EXPORT; ] } diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly index e51049699..f1bd0a97f 100644 --- a/src/driver/driver_parser.mly +++ b/src/driver/driver_parser.mly @@ -19,7 +19,7 @@ %token STRING %token OPERATOR %token INPUT (* never reaches the parser *) -%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING +%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING USE EXPORT %token VALID INVALID UNKNOWN FAIL %token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF @@ -91,6 +91,7 @@ trule: | REMOVE ALL { Rremoveall } | META ident meta_args { Rmeta ($2, $3) } | META STRING meta_args { Rmeta ($2, $3) } +| USE EXPORT qualid { Ruse ($3) } meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 } diff --git a/theories/for_drivers.why b/theories/for_drivers.why new file mode 100644 index 000000000..6d4637dd8 --- /dev/null +++ b/theories/for_drivers.why @@ -0,0 +1,19 @@ +theory ComputerOfEuclideanDivision + + use import int.Int + use import int.EuclideanDivision as ED + use import int.ComputerDivision as CD + + lemma cdiv_cases : forall n d:int [CD.div n d]. + ((n >= 0) -> (d > 0) -> CD.div n d = ED.div n d) /\ + ((n <= 0) -> (d > 0) -> CD.div n d = -(ED.div (-n) d)) /\ + ((n >= 0) -> (d < 0) -> CD.div n d = -(ED.div n (-d))) /\ + ((n <= 0) -> (d < 0) -> CD.div n d = ED.div (-n) (-d)) + + lemma cmod_cases : forall n d:int [CD.mod n d]. + ((n >= 0) -> (d > 0) -> CD.mod n d = ED.mod n d) /\ + ((n <= 0) -> (d > 0) -> CD.mod n d = -(ED.mod (-n) d)) /\ + ((n >= 0) -> (d < 0) -> CD.mod n d = (ED.mod n (-d))) /\ + ((n <= 0) -> (d < 0) -> CD.mod n d = -(ED.mod (-n) (-d))) + +end -- GitLab