Commit e29da0a5 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Changed args_wrapper to also take a string. cut now takes the name of

hypothesis as argument.
parent cc53bc33
......@@ -170,6 +170,7 @@ type (_, _) trans_typ =
| Ttysymbol : ('a, 'b) trans_typ -> ((tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
| Tstring : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
......@@ -268,6 +269,17 @@ 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
| Tstring t' ->
begin
match l with
| 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
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)
......
......@@ -21,6 +21,7 @@ type (_, _) trans_typ =
| Ttysymbol : ('a, 'b) trans_typ -> ((Ty.tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Tstring : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
......
......@@ -20,9 +20,8 @@ let case t =
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 t =
(* let g, task = Task.task_separate_goal task in *)
let h = Decl.create_prsymbol (gen_ident "h") in
let cut name t =
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
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
......@@ -83,24 +82,6 @@ let remove_task_decl (name: Ident.ident) : task trans =
let remove name =
remove_task_decl name.pr_name
(* let pr_prsymbol pr = *)
(* match pr with *)
(* | Decl {d_node = Dprop (_pk, pr, _t)} -> Some pr *)
(* | _ -> None *)
(* (\* Looks for the hypothesis name and return it. If not found return None *\) *)
(* let find_hypothesis_aux (name:Ident.ident) (d: task_hd) (ndecl: tdecl option) = *)
(* match ndecl with *)
(* | Some pr -> Some pr *)
(* | None -> *)
(* (match d.task_decl.td_node with *)
(* | Decl {d_node = Dprop (_pk, pr, _t)} when Ident.id_equal pr.pr_name name -> Some d.task_decl *)
(* | _ -> None) *)
(* (\* Return a tdecl option trans which is the specific declaration name name *\) *)
(* let find_hypothesis (name: Ident.ident) = *)
(* Trans.fold (find_hypothesis_aux name) *)
(* from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let instantiate (pr: Decl.prsymbol) t =
......@@ -114,24 +95,6 @@ let instantiate (pr: Decl.prsymbol) t =
[d; new_decl]
| _ -> [d]) None
(* (\* from task [delta, name:forall x.A |- G, *)
(* build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *\) *)
(* let instantiate (pr:Decl.prsymbol) t task = *)
(* let name = pr.pr_name in *)
(* (\* let g, task = Task.task_separate_goal task in *\) *)
(* let ndecl = Trans.fold (find_hypothesis name) task in *)
(* match ndecl with *)
(* | None -> Format.printf "Hypothesis %s not found@." name.Ident.id_string; *)
(* Task.add_tdecl task g *)
(* | Some decl -> (match decl.td_node with *)
(* | Decl {d_node = Dprop (pk, _pr, ht)} -> *)
(* let t_subst = subst_forall ht t in *)
(* let new_pr = create_prsymbol (Ident.id_clone name) in *)
(* let new_decl = create_prop_decl pk new_pr t_subst in *)
(* let task = add_decl task new_decl in *)
(* Task.add_tdecl task g *)
(* | _ -> Format.printf "Not an hypothesis@."; Task.add_tdecl task g) *)
(* TODO find correct librrary *)
let choose_option a b =
match a, b with
......@@ -244,7 +207,7 @@ 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 (Tformula Ttrans_l) cut)
let () = register_transform_with_args_l ~desc:"test cut" "cut" (wrap_l (Tstring (Tformula 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 "exists x: int. x = x"
b cut "He" "exists x: int. x = x"
(* print goal with h in context *)
b exists "5"
(* print new goal G1 with (x = (2 * 5)) *)
......@@ -8,12 +8,12 @@ b case "exists x. exists y. x + y = y - x"
(* print the goal with the hypothesis in context *)
pg
(* return to context with positive exists *)
b cut "exists x. exists y. x + y = 0"
b cut "H" "exists x. exists y. x + y = 0"
ng
(* Have to prove h1 with 2 exists *)
b exists "4"
(* Instantiate x1 *)
b cut "forall x. forall y. x + y = 0"
b cut "H" "forall x. forall y. x + y = 0"
(* 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