Commit 25058cde authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Added an optional name argument for case and cut that should be given

at the end of line.
This was commited as a proof of concept. Giving the name at the end is not
convenient.
Should also solve the problem of renaming by asking args_wrapper to do the
work of unification of name.
parent e29da0a5
......@@ -196,6 +196,11 @@ let parse_and_type ~as_fmla s task =
in
t
let last_trans: type a b. (a, b) trans_typ -> bool = function
| Ttrans -> true
| Ttrans_l -> true
| _ -> false
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> task -> b =
fun t f l env task ->
match t with
......@@ -269,6 +274,24 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
_ -> failwith "Theory not found.")
| _ -> failwith "Missing argument: expecting a theory."
end
(* TODO: Tstring is an optional argument if given last. Replaced by a new ident for "h" if
no arguments is given *)
(* TODO: ugly. Did not know how to use function trans for this. Did not investigate further *)
| Tstring t' when (last_trans t') ->
begin
match l with
| [] -> (* No more arguments, we build a string *)
let p = (build_name_tables task).printer in
let id = Decl.create_prsymbol (Ident.id_fresh "h") in
let new_name = Ident.id_unique p id.pr_name in
wrap_to_store t' (f new_name) [] env task
| s :: tail ->
let p = (build_name_tables task).printer in
let id = Decl.create_prsymbol (Ident.id_fresh s) in
let new_name = Ident.id_unique p id.pr_name in
wrap_to_store t' (f new_name) tail env task
| _ -> failwith "Missing argument: expecting a string."
end
| Tstring t' ->
begin
match l with
......@@ -280,7 +303,6 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| _ -> failwith "Missing argument: expecting a string."
end
let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
fun t f l env -> Trans.store (wrap_to_store t f l env)
......
......@@ -12,15 +12,15 @@ let gen_ident = Ident.id_fresh
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t =
let h = Decl.create_prsymbol (gen_ident "h") in
let hnot = Decl.create_prsymbol (gen_ident "hnot") in
let case t name =
let h = Decl.create_prsymbol (gen_ident name) in
let hnot = Decl.create_prsymbol (gen_ident name) in
let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
let t_decl = Decl.create_prop_decl Decl.Paxiom h t in
Trans.par [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
let cut name t =
let cut t name =
let h = Decl.create_prsymbol (gen_ident name) in
let g_t = Decl.create_prop_decl Decl.Pgoal h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
......@@ -206,8 +206,8 @@ let apply pr task =
let use_th th =
Trans.add_tdecls [Theory.create_use th]
let () = register_transform_with_args_l ~desc:"test case" "case" (wrap_l (Tformula Ttrans_l) case)
let () = register_transform_with_args_l ~desc:"test cut" "cut" (wrap_l (Tstring (Tformula Ttrans_l)) cut)
let () = register_transform_with_args_l ~desc:"test case" "case" (wrap_l (Tformula (Tstring Ttrans_l)) case)
let () = register_transform_with_args_l ~desc:"test cut" "cut" (wrap_l (Tformula (Tstring Ttrans_l)) cut)
let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tprsymbol Ttrans) remove)
let () = register_transform_with_args ~desc:"test instantiate" "instantiate"
......
b introduce_premises
(* print goal with premisses introduced *)
b cut "He" "exists x: int. x = x"
b cut "exists x: int. x = x"
(* print goal with h in context *)
b exists "5"
(* print new goal G1 with (x = (2 * 5)) *)
b case "exists x. exists y. x + y = y - x"
b case "exists x. exists y. x + y = y - x" "h10"
(* print the goal with the hypothesis in context *)
pg
(* return to context with positive exists *)
b cut "H" "exists x. exists y. x + y = 0"
b cut "exists x. exists y. x + y = 0" "he"
ng
(* Have to prove h1 with 2 exists *)
b exists "4"
(* Instantiate x1 *)
b cut "H" "forall x. forall y. x + y = 0"
b cut "forall x. forall y. x + y = 0" "hf"
(* print with h2 in context *)
b instantiate "h2" "4"
(* create h21 which is correct *)
......
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