Commit 19fccc50 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Adding bind_comp, relocating sort, adding pose/hide

parent abafcb81
......@@ -55,6 +55,9 @@ let store fn = let tr = Wtask.memoize_option 63 fn in fun t -> match t with
let bind f g = store (fun task -> g (f task) task)
let bind_comp f g =
store (fun task -> let (ret, new_task) = f task in g ret new_task)
let trace_goal msg tr =
fun task ->
begin match task with
......
......@@ -32,6 +32,7 @@ val identity_l : task tlist
val singleton : 'a trans -> 'a tlist
val return : 'a -> 'a trans
val bind : 'a trans -> ('a -> 'b trans) -> 'b trans
val bind_comp : ('a * task) trans -> ('a -> 'b trans) -> 'b trans
val trace_goal : string -> task trans -> task trans
......@@ -85,7 +86,6 @@ val add_decls : decl list -> task trans
val add_tdecls : tdecl list -> task trans
(** [add_decls ld t1] adds decls ld at the end of the task t1 (before the goal) *)
(** {2 Dependent Transformations} *)
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
......
......@@ -267,32 +267,6 @@ let unfold unf h =
end
| _ -> [d]) None
let sort local_decls =
let l = ref [] in
Trans.decl
(fun d ->
match d.d_node with
| _ when not (List.exists (fun x -> Decl.d_equal x d) local_decls) ->
[d]
| Dprop (Paxiom, _, _)
| Dprop (Plemma, _, _)
| Dprop (Pskip, _, _) ->
(* This goes in the second group *)
l := !l @ [d];
[]
| Dprop (Pgoal, _, _) ->
(* Last element, we concatenate the list of postponed elements *)
!l @ [d]
| _ -> [d]) None
(* TODO is sort really needed ? It looked like it was for subst in some example where I wanted to subst the definition of a logic constant into an equality and it would fail because the equality is defined before the logic definition. This may be solved by current implementation of subst: to be tested *)
let sort =
Trans.bind get_local sort
let get_local task =
let ut = Task.used_symbols (Task.used_theories task) in
Task.local_decls task ut
(* This function is used to find a specific ident in an equality:
(to_subst = term or term = to_subst) in order to subst and remove said
equality.
......@@ -388,7 +362,7 @@ let subst_all (is_local_decl: Decl.decl -> bool) =
Trans.bind (find_eq2 is_local_decl) subst_eq
let return_local_decl task =
let decl_list = get_local task in
let decl_list = get_local_task task in
let is_local_decl d = List.exists (fun x -> Decl.d_equal d x) decl_list in
is_local_decl
......
......@@ -130,6 +130,47 @@ let clear_but (l: prsymbol list) =
let use_th th =
Trans.add_tdecls [Theory.create_use th]
(* Equivalent of Coq pose (x := term). Adds a new constant of appropriate type
and an hypothesis x = term.
This function returns the declarations of hypothesis and constant. *)
let pose (clear: bool) (name: string) (t: term) =
let ty = Term.t_type t in
let ls = Term.create_lsymbol (gen_ident name) [] (Some ty) in
let ls_term = Term.t_app_infer ls [] in
let new_constant = Decl.create_param_decl ls in
let pr = create_prsymbol (gen_ident "H") in
(* hyp = [pr : ls = t] *)
let hyp =
Decl.create_prop_decl Paxiom pr (Term.t_app_infer ps_equ [ls_term;t])
in
let trans_new_task =
if clear then
Trans.add_decls [new_constant]
else
Trans.add_decls [new_constant; hyp]
in
(* Note that sort is necessary *and* the complexity is probably the same as if
we use a function Trans.prepend_decl (which will be linear in the size of
the task. Sort should be too). *)
Trans.compose trans_new_task
(Trans.compose sort (Trans.store (fun task -> ((hyp, new_constant, ls_term), task))))
(* Sometimes it is useful to hide part of a term (actually to pose a constant
equal to a term). It may also help provers to completely remove reference to
stuff *)
let hide (clear: bool) (name: string) (t: term) =
let replace_all hyp new_constant ls_term =
Trans.decl (fun d ->
match d.d_node with
| _ when (Decl.d_equal d hyp || Decl.d_equal d new_constant) -> [d]
| Dprop (p, pr, t1) ->
let new_decl = create_prop_decl p pr (replace_in_term t ls_term t1) in
[new_decl]
| _ -> [d]) None
in
Trans.bind_comp (pose clear name t)
(fun (hyp,new_constant,ls_term) -> replace_all hyp new_constant ls_term)
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument"
"clear_but"
(Tprlist Ttrans) clear_but
......@@ -152,3 +193,21 @@ let () = wrap_and_register
let () = wrap_and_register
~desc:"use_th <theory> imports the theory" "use_th"
(Ttheory Ttrans) use_th
let pose (name: string) (t: term) =
Trans.bind (pose false name t) (fun (_, task) -> Trans.store (fun _ -> task))
let () = wrap_and_register
~desc:"pose <name> <term> adds a new constant <name> equal to <term>"
"pose"
(Tstring (Tterm Ttrans)) pose
let () = wrap_and_register
~desc:"hide <name> <term> adds a new constant <name> equal to <term> and replace everywhere the term with the new constant."
"hide"
(Tstring (Tterm Ttrans)) (hide false)
let () = wrap_and_register
~desc:"hide and clear <name> <term> adds a new constant <name> which replaces all occurences of <term>."
"hide_and_clear"
(Tstring (Tterm Ttrans)) (hide true)
......@@ -10,6 +10,7 @@
(********************************************************************)
open Term
open Decl
exception Arg_trans of string
exception Arg_trans_term of (string * term * term)
......@@ -84,3 +85,34 @@ let get_local =
let ut = Task.used_symbols (Task.used_theories task) in
Task.local_decls task ut in
local_decls)
let get_local_task task =
let ut = Task.used_symbols (Task.used_theories task) in
Task.local_decls task ut
let sort local_decls =
let l = ref [] in
Trans.decl
(fun d ->
match d.d_node with
| _ when not (List.exists (fun x -> Decl.d_equal x d) local_decls) ->
[d]
| Dprop (Paxiom, _, _)
| Dprop (Plemma, _, _)
| Dprop (Pskip, _, _) ->
(* This goes in the second group *)
l := !l @ [d];
[]
| Dprop (Pgoal, _, _) ->
(* Last element, we concatenate the list of postponed elements *)
!l @ [d]
| _ -> [d]) None
(* TODO is sort really needed ? It looked like it was for subst in some example
where I wanted to subst the definition of a logic constant into an equality
and it would fail because the equality is defined before the logic definition.
This may be solved by current implementation of subst: to be tested.
*)
let sort =
Trans.bind get_local sort
......@@ -37,3 +37,9 @@ val subst_forall_list: term -> term list -> term
(* Returns the list of local declarations *)
val get_local: Decl.decl list Trans.trans
val get_local_task: Task.task -> Decl.decl list
(* Returns same list of declarations but reorganized with constant/type
definitions defined before axioms *)
val sort: Task.task Trans.trans
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