Commit 63f6b075 authored by MARCHE Claude's avatar MARCHE Claude

ITP: transformations with args only take strings as arguments

"parsing" of these strings is delayed in the transformations themselves,
because in case such an argument must be interpreted as a term, the
task itself is needed do perform name resolution.

Incidentally, saving transformations with arguments in sessions is not an
issue anymore
parent a7878cce
......@@ -193,7 +193,8 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry case
induction_pr prop_curry \
args_wrapper case
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
......
......@@ -333,108 +333,7 @@ let list_transforms_l () =
(** transformations with arguments *)
(*
type _ trans_gadt =
| TAvoid : (task -> task list) -> unit trans_gadt
| TAint : (int -> 'a trans_gadt) -> (int * 'a) trans_gadt
let rec apply_trans_gadt : type a. a trans_gadt -> a -> task -> task list =
fun t x ->
match t,x with
| TAvoid f,() -> f
| TAint f,(n,rem) -> apply_trans_gadt (f n) rem
let id_trans = TAvoid (fun task -> [task])
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
let duplicate = TAint (fun n -> TAvoid (fun task -> dup n task))
let []
let l = [id_trans ; duplicate]
let transforms_with_args : 'a trans_gadt Mstr.t = Mstr.empty
let m = Mstr.add "id" id_trans transforms_with_args
let m1 = Mstr.add "dup" duplicate m
*)
type trans_arg =
| TAint of int
| TAstring of string
| TAterm of Term.term
| TAty of Ty.ty
| TAtysymbol of Ty.tysymbol
type trans_with_args = trans_arg list -> task -> task list
(* TODO : syntax to be confirmed *)
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
let rec wrap : type a. a trans_typ -> a -> trans_with_args =
fun t f ->
match t with
| Ttrans -> fun _ -> f
| Tint t' ->
begin fun l ->
match l with
| (TAint i) :: tail -> wrap t' (f i) tail
| _ -> assert false
end
| Tstring t' ->
begin fun l ->
match l with
| (TAstring s) :: tail -> wrap t' (f s) tail
| _ -> assert false
end
| Tterm t' ->
begin fun l ->
match l with
| (TAterm te) :: tail -> wrap t' (f te) tail
| _ -> assert false
end
| Tty t' ->
begin fun l ->
match l with
| (TAty ty) :: tail -> wrap t' (f ty) tail
| _ -> assert false
end
| Ttysymbol t' ->
begin fun l ->
match l with
| (TAtysymbol tys) :: tail -> wrap t' (f tys) tail
| _ -> assert false
end
(* example of use: TO BE REMOVED*)
(*
let case : term -> task -> task list = ...
let aus : int -> term -> string -> task -> task list = ...
let case' = wrap (Tterm Ttrans) case
let aus' = wrap (Tint (Tterm (Tstring Ttrans))) aus *)
(*
type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
| TTlsymbol | TTprsymbol
let encapsulate : trans_arg_type list -> ? -> trans_with_args =
fun args f tr ->
match args with
| [] -> fun
*)
type trans_with_args = string list -> task -> task list
let transforms_with_args = Hstr.create 17
......
......@@ -134,36 +134,16 @@ val named : string -> 'a trans -> 'a trans
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly *)
(** {2 Transformations with arguments} *)
(** {2 Transformations with arguments}
type trans_arg =
| TAint of int
| TAstring of string
| TAterm of Term.term
| TAty of Ty.ty
| TAtysymbol of Ty.tysymbol
(* | ... *)
(* note: la fonction register des transformations doit permettre de
declarer les types des arguments
type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol
| TTlsymbol | TTprsymbol
These transformations take strings as arguments. For a more "typed" version,
see file [src/transform/args_wrapper.ml]
*)
type trans_with_args = trans_arg list -> task -> task list
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
val wrap : 'a trans_typ -> 'a -> trans_with_args
type trans_with_args = string list -> task -> task list
val register_transform_with_args : desc:Pp.formatted -> string -> trans_with_args -> unit
val apply_transform_args : string -> Env.env -> trans_arg list -> task -> task list
val apply_transform_args : string -> Env.env -> string list -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -78,7 +78,7 @@ val schedule_transformation :
controller ->
proofNodeID ->
string ->
Trans.trans_arg list ->
string list ->
callback:(transformation_status -> unit) -> unit
(** [schedule_transformation c id cb] schedules a transformation for a
goal specified by [id]; the function [cb] will be called each time
......
......@@ -46,7 +46,7 @@ type proof_node = {
type transformation_node = {
transf_name : string;
transf_args : Trans.trans_arg list;
transf_args : string list;
transf_subtasks : proofNodeID list;
transf_parent : proofNodeID;
}
......@@ -326,7 +326,7 @@ let mk_transf_proof_node (s : session) (tid : int) (t : Task.task) =
id
let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
(name : string) (args : Trans.trans_arg list) (pnl : proofNodeID list) =
(name : string) (args : string list) (pnl : proofNodeID list) =
let pn = get_proofNode s id in
let tn = { transf_name = name;
transf_args = args;
......@@ -336,7 +336,7 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
pn.proofn_transformations <- node_id::pn.proofn_transformations
let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : Trans.trans_arg list) (tl : Task.task list) =
(args : string list) (tl : Task.task list) =
let tid = gen_transID s in
let sub_tasks = List.map (mk_transf_proof_node s tid) tl in
mk_transf_node s id tid name args sub_tasks;
......
......@@ -121,11 +121,11 @@ val update_proof_attempt : session -> proofNodeID -> Whyconf.prover ->
(** [update_proof_attempt s id pr st] update the status of the
corresponding proof attempt with [st]. *)
val graft_transf : session -> proofNodeID -> string -> Trans.trans_arg list ->
val graft_transf : session -> proofNodeID -> string -> string list ->
Task.task list -> transID
(** [graft_transf s id name l tl] adds the transformation [name] as a
child of the task [id] of the session [s]. [l] is the list of
argument of the transformation, and [tl] is the list of subtasks.
arguments of the transformation, and [tl] is the list of subtasks.
*)
val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
......
open Task
open Ty
open Term
open Trans
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
let rec wrap : type a. a trans_typ -> a -> trans_with_args =
fun t f l task ->
match t with
| Ttrans -> f task
| Tint t' ->
begin
match l with
| s :: tail ->
let n = int_of_string s in
wrap t' (f n) tail task
| _ -> assert false
end
| Tstring t' ->
begin
match l with
| s :: tail -> wrap t' (f s) tail task
| _ -> assert false
end
| Tterm t' ->
begin
match l with
| _s :: tail ->
let te = Term.t_true in (* TODO: parsing + typing of s *)
wrap t' (f te) tail task
| _ -> assert false
end
| Tty t' ->
begin
match l with
| _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap t' (f ty) tail task
| _ -> assert false
end
| Ttysymbol t' ->
begin
match l with
| _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap t' (f tys) tail task
| _ -> assert false
end
open Task
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
| Tty : 'a trans_typ -> (Ty.ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (Ty.tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ
val wrap : 'a trans_typ -> 'a -> Trans.trans_with_args
......@@ -4,14 +4,10 @@ open Term
open Decl
open Theory
open Task
open Args_wrapper
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
let duplicate args task =
match args with
| [TAint n] -> dup n task
| _ -> failwith "wrong arguments for duplicate"
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t task =
......@@ -228,10 +224,14 @@ let apply name task =
| Tbinop (Timplies, _ta, _tb) -> failwith "Not implemented yet" (* TODO to be done later *)
| _ -> failwith "Not of the form forall x. A -> B"
let case' args task =
(*
let case' =
(*
args task =
match args with
| [TAterm t] -> case t task
| _ -> failwith "wrong arguments for case"
*)
let cut' args task =
match args with
......@@ -257,11 +257,13 @@ let apply' args task =
match args with
| [TAstring name] -> apply name task
| _ -> failwith "wrong arguments of simple_apply"
*)
let () = register_transform_with_args ~desc:"test case" "case" case'
let () = register_transform_with_args ~desc:"test cut" "cut" cut'
let () = register_transform_with_args ~desc:"test exists" "exists" exists'
let () = register_transform_with_args ~desc:"test remove" "remove" remove'
let () = register_transform_with_args ~desc:"test simple_apply" "simple_apply" simple_apply'
let () = register_transform_with_args ~desc:"test apply" "apply" apply'
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" duplicate
let () = register_transform_with_args ~desc:"test case" "case" (wrap (Tterm Ttrans) case)
let () = register_transform_with_args ~desc:"test cut" "cut" (wrap (Tterm Ttrans) cut)
let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tstring Ttrans) remove)
let () = register_transform_with_args ~desc:"test simple_apply" "simple_apply"
(wrap (Tstring (Tterm Ttrans)) simple_apply)
let () = register_transform_with_args ~desc:"test apply" "apply" (wrap (Tstring Ttrans) apply)
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" (wrap (Tint Ttrans) dup)
......@@ -388,17 +388,12 @@ let apply_transform_no_args fmt args =
let test_transformation_with_args fmt args =
(* temporary : apply duplicate on the first goal *)
let n =
match args with
| [s] -> int_of_string s
| _ -> assert false
in
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "duplicate" [Trans.TAint n] ~callback
C.schedule_transformation cont id "duplicate" args ~callback
(* Do not use this. TODO
Claude: indeed type_fmla and type_term should never be used like this
......@@ -407,6 +402,7 @@ let typing_terms t th =
try (Typing.type_fmla th (fun _ -> None) t) with
| _ -> Typing.type_term th (fun _ -> None) t
(*
let parse_transformation_arg args : Term.term option =
(* temporary : parses the term *)
match args with
......@@ -428,8 +424,10 @@ let parse_transformation_arg args : Term.term option =
None
end
| _ -> let _ = printf "term argument expected@." in None
*)
(*
let parse_transformation_string args : string option =
(* temporary : parses a string *)
match args with
......@@ -443,9 +441,11 @@ let parse_transformation_string args : string option =
printf "parsing string \"%s\"@." s;
Some s
| _ -> let _ = printf "term argument expected@." in None
*)
let test_simple_apply fmt args =
(* temporary : parses a string *)
(*
match args with
| [s';s] ->
let s =
......@@ -471,39 +471,46 @@ let test_simple_apply fmt args =
let th = Theory.use_export th int_theory in
let t = typing_terms t th in
let _ = printf "typing OK: %a@." Pretty.print_term t in
let id = nearest_goal () in
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "simple_apply" [Trans.TAstring s'; Trans.TAterm t] ~callback
C.schedule_transformation cont id "simple_apply" args ~callback
(*
with e ->
let _ = printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e in
()
end
| _ -> let _ = printf "term argument expected@." in ()
*)
let test_apply_with_string_args fmt args =
(*
match (parse_transformation_string args) with
| None -> ()
| Some s ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "apply" [Trans.TAstring s] ~callback
C.schedule_transformation cont id "apply" args ~callback
let test_remove_with_string_args fmt args =
(*
match (parse_transformation_string args) with
| None -> ()
| Some s ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "remove" [Trans.TAstring s] ~callback
C.schedule_transformation cont id "remove" args ~callback
(*** term argument parsed in the context of the task ***)
......@@ -544,38 +551,46 @@ let parse_arg_only s task =
[task]
let () = Trans.(register_transform_with_args
"parse_arg_only" (wrap (Tstring Ttrans) parse_arg_only)
"parse_arg_only" Args_wrapper.(wrap (Tstring Ttrans) parse_arg_only)
~desc:"Just parse and type the string argument")
let test_transformation_with_string_parsed_later fmt args =
(*
match args with
| [s] ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "parse_arg_only" [Trans.TAstring s] ~callback
C.schedule_transformation cont id "parse_arg_only" args ~callback
(*
| _ -> printf "string argument expected@."
*)
(*******)
(* Only parses arguments and print debugging information *)
(*
let test_transformation_with_term_arg _fmt args =
let _ = parse_transformation_arg args in ()
*)
let test_case_with_term_args fmt args =
(*
match (parse_transformation_arg args) with
| None -> ()
| Some t ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "case" [Trans.TAterm t] ~callback
C.schedule_transformation cont id "case" args ~callback
(* TODO rewrite this. Only for testing *)
......@@ -588,10 +603,13 @@ let test_transformation_one_arg_term fmt args =
fprintf fmt "transformation %s status: %a@."
tr Controller_itp.print_trans_status status
in
(*
match (parse_transformation_arg tl) with
| None -> ()
| Some t ->
C.schedule_transformation cont id tr [Trans.TAterm t] ~callback
*)
C.schedule_transformation cont id tr tl ~callback
let task_driver =
let d = Filename.concat (Whyconf.datadir main)
......
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