transformations with arguments, first draft

src/core/trans.ml

@@ -274,7 +274,7 @@ let create_debugging_trans trans_name (tran : Task.task trans) =
     print_task_goal t2;
     Debug.dprintf debug "@.@.";
     t2;
-    
+
   end in
   store new_trans
 
@@ -331,23 +331,98 @@ let list_transforms () =
 let list_transforms_l () =
   Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l []
 
-(** fast transform *)
+(** 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
+
+(*
+
+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
+
+ *)
+
+
+let transforms_with_args = Hstr.create 17
+
+let lookup_transform_with_args s =
+ try snd (Hstr.find transforms_with_args s)
+ with Not_found -> raise (UnknownTrans s)
+
+let register_transform_with_args ~desc s p =
+  if Hstr.mem transforms_with_args s then raise (KnownTrans s);
+  Hstr.replace transforms_with_args s (desc, fun _ -> p)
+
 type gentrans =
   | Trans_one of Task.task trans
   | Trans_list of Task.task tlist
+  | Trans_with_args of trans_with_args
 
 let lookup_trans env name =
   try
     let t = lookup_transform name env in
     Trans_one t
   with UnknownTrans _ ->
-    let t = lookup_transform_l name env in
-    Trans_list t
+    try
+      let t = lookup_transform_l name env in
+      Trans_list t
+    with UnknownTrans _ ->
+         let t = lookup_transform_with_args name env in
+         Trans_with_args t
 
 let apply_transform tr_name env task =
    match lookup_trans env tr_name with
     | Trans_one t -> [apply t task]
     | Trans_list t -> apply t task
+    | Trans_with_args t -> t [] task
+
+let apply_transform_args tr_name env args task =
+   match lookup_trans env tr_name with
+    | Trans_one t -> [apply t task]
+    | Trans_list t -> apply t task
+    | Trans_with_args t -> t args task
+
 
 (** Flag-dependent transformations *)
 

src/core/trans.mli

@@ -132,4 +132,28 @@ val named : string -> 'a trans -> 'a trans
 (** give transformation a name without registering *)
 
 val apply_transform : string -> Env.env -> task -> task list
-(** apply a registered 1-to-1 or a 1-to-n function directly *)
+(** apply a registered 1-to-1 or a 1-to-n, directly *)
+
+(** {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
+
+*)
+
+type trans_with_args = trans_arg 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
+(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)

src/session/controller_itp.ml

@@ -146,7 +146,7 @@ let schedule_transformation c id name args ~callback =
   let apply_trans () =
     let task = get_task c.controller_session id in
     try
-      let subtasks = Trans.apply_transform name c.controller_env task in
+      let subtasks = Trans.apply_transform_args name c.controller_env args task in
       let _tid = graft_transf c.controller_session id name args subtasks in
       callback TSdone;
       false

src/session/controller_itp.mli

@@ -78,7 +78,7 @@ val schedule_transformation :
   controller ->
   proofNodeID ->
   string ->
-  trans_arg list ->
+  Trans.trans_arg 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

src/session/session_itp.ml

@@ -43,17 +43,10 @@ type proof_node = {
   mutable proofn_transformations : transID list;
 }
 
-type trans_arg =
-  | TAint      of int
-  | TAstring   of string
-  | TAterm     of Term.term
-  | TAty       of Ty.ty
-  | TAtysymbol of Ty.tysymbol
-  (* | ... *)
 
 type transformation_node = {
   transf_name     : string;
-  transf_args     : trans_arg list;
+  transf_args     : Trans.trans_arg list;
   transf_subtasks : proofNodeID list;
   transf_parent   : proofNodeID;
 }
@@ -333,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_arg list) (pnl : proofNodeID list) =
+    (name : string) (args : Trans.trans_arg list) (pnl : proofNodeID list) =
   let pn = get_proofNode s id in
   let tn = { transf_name = name;
              transf_args = args;
@@ -343,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_arg list) (tl : Task.task list) =
+    (args : Trans.trans_arg 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;

src/session/session_itp.mli

@@ -44,20 +44,6 @@ Each goal
 type proof_attempt
 type transID
 
-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
-
-*)
 
 type proof_parent = Trans of transID | Theory of theory
 
@@ -135,7 +121,7 @@ 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_arg list ->
+val graft_transf : session -> proofNodeID -> string -> Trans.trans_arg 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

src/why3shell/why3shell.ml

@@ -378,6 +378,20 @@ let test_transformation fmt _args =
   in
   C.schedule_transformation cont id "split_goal_wp" [] ~callback
 
+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
+
 let task_driver =
   let d = Filename.concat (Whyconf.datadir main)
                           (Filename.concat "drivers" "why3_itp.drv")
@@ -418,6 +432,7 @@ let commands =
     "r", "reload the session (test only)", test_reload;
     "s", "[s my_session] save the current session in my_session.xml", test_save_session;
     "tr", "test schedule_transformation with split_goal on the current or next right goal (or on the top goal if there is none", test_transformation;
+    "tra", "test duplicate transformation", test_transformation_with_args;
     "ngr", "get to the next goal right", ngr_ret_p;
     "pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper)
   ]