Modifying case.

Added cut.
Added exists.
Should work by calling ttr "case" term.
Added a function typing_terms that should not be used and which exists
to avoid duplicating parse_transformation_arg.

src/transform/case.ml

 
 open Trans
+open Term
+open Decl
+open Theory
 
 let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
 
@@ -8,23 +11,51 @@ let duplicate args task =
     | [TAint n] -> dup n task
     | _ -> failwith "wrong arguments for duplicate"
 
-(* from task [delta |- G] and term t, build the tasks:
+(* From task [delta |- G] and term t, build the tasks:
    [delta, t] |- G] and [delta, not t | - G] *)
 let case t task =
-  let g, task = Task.task_separate_goal task in
   let h = Decl.create_prsymbol (Ident.id_fresh "h") in
   let hnot = Decl.create_prsymbol (Ident.id_fresh "hnot") 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
-  [Task.add_tdecl (Task.add_decl task t_decl) g; Task.add_tdecl (Task.add_decl task t_not_decl) g]
+  List.map (fun f -> Trans.apply f task) [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
 
-let cut _t task = (* Sylvain *)
-  [task;task]
-  (* TODO : from task [delta |- G] , build the tasks [delta] |- t] and [delta, t | - G] *)
+(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
+let cut t task =
+  let g, task = Task.task_separate_goal task in
+  let h = Decl.create_prsymbol (Ident.id_fresh "h") 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 = Task.add_decl task g_t in
+  let goal = Task.add_tdecl (Task.add_decl task h_t) g in
+  [goal; goal_cut]
 
-let exists _t task = (* ? *)
-  [task;task]
-  (* TODO : from task [delta |- exists x. G] , build the task [delta] |- G[x -> t]] *)
+(* Transform (exists v, f) into f[x/v] *)
+let subst_exist t x =
+  match t.t_node with
+  | Tquant (Texists, tq) ->
+      let (vsl, tr, te) = t_open_quant tq in
+      (match vsl with
+      | hdv :: tl ->
+          (try
+            (let new_t = t_subst_single hdv x te in
+              t_exists_close tl tr new_t)
+          with
+          | Ty.TypeMismatch (_ty1, _ty2) -> failwith "type mismatch") (* TODO match errors *)
+      | [] -> failwith "no")
+  | _ -> failwith "term do not begin with exists"
+
+(* From task [delta |- exists x. G] and term t, build the task [delta] |- G[x -> t]]
+   Return an error if x and t are not unifiable. *)
+let exists x task =
+  let g, task = Task.task_separate_goal task in
+  match g.td_node with
+  | Decl {d_node = Dprop (_, _, t)} ->
+      let t = subst_exist t x in
+      let pr_goal = create_prsymbol (Ident.id_fresh "G") in
+      let new_goal = Decl.create_prop_decl Decl.Pgoal pr_goal t in
+      [Task.add_decl task new_goal]
+  | _ -> failwith "No goal"
 
 let remove _name task =
   [task;task]
@@ -45,6 +76,17 @@ let case' args task  =
   | [TAterm t] -> case t task
   | _ -> failwith "wrong arguments for case"
 
+let cut' args task =
+  match args with
+  | [TAterm t] -> cut t task
+  | _ -> failwith "wrong arguments for cut"
+
+let exists' args task =
+   match args with
+  | [TAterm t] -> exists t task
+  | _ -> failwith "wrong arguments for exists"
 
 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 duplicate" "duplicate" duplicate

src/why3shell/why3shell.ml

@@ -392,6 +392,11 @@ let test_transformation_with_args fmt args =
   in
   C.schedule_transformation cont id "duplicate" [Trans.TAint n] ~callback
 
+(* Do not use this. TODO *)
+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
@@ -411,7 +416,7 @@ let parse_transformation_arg args : Term.term option =
          let th = Theory.create_theory (Ident.id_fresh "dummy") in
          let int_theory = Env.read_theory env ["int"] "Int" in
          let th = Theory.use_export th int_theory in
-         let t = Typing.type_fmla th (fun _ -> None) t in
+         let t = typing_terms t th in
          let _ = printf "typing OK: %a@." Pretty.print_term t in
          Some t
        with e ->
@@ -424,34 +429,6 @@ let parse_transformation_arg args : Term.term option =
 let test_transformation_with_term_arg _fmt args =
   let _ = parse_transformation_arg args in ()
 
-(*
-let test_transformation_with_term_arg _fmt args =
-  (* temporary : parses the term *)
-  match args with
-  | [s] ->
-     let s =
-       let l = String.length s in
-       if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
-         String.sub s 1 (l - 2)
-       else s
-     in
-     printf "parsing string \"%s\"@." s;
-     begin try
-         let lb = Lexing.from_string s in
-         let t = Lexer.parse_term lb in
-         printf "parsing OK@.";
-         let env = cont.controller_env in
-         let th = Theory.create_theory (Ident.id_fresh "dummy") in
-         let int_theory = Env.read_theory env ["int"] "Int" in
-         let th = Theory.use_export th int_theory in
-         let t = Typing.type_fmla th (fun _ -> None) t in
-         printf "typing OK: %a@." Pretty.print_term t
-       with e ->
-         printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e
-     end
-  | _ -> printf "term argument expected@."
-*)
-
 let test_case_with_term_args fmt args =
   match (parse_transformation_arg args) with
   | None -> ()
@@ -463,6 +440,22 @@ let test_case_with_term_args fmt args =
   in
   C.schedule_transformation cont id "case" [Trans.TAterm t] ~callback
 
+
+(* TODO rewrite this. Only for testing *)
+let test_transformation_one_arg_term fmt args =
+  match args with
+  | [] -> printf "Give the name of the transformation@."
+  | tr :: tl ->
+      let id = nearest_goal () in
+      let callback status =
+        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
+
 let task_driver =
   let d = Filename.concat (Whyconf.datadir main)
                           (Filename.concat "drivers" "why3_itp.drv")
@@ -504,6 +497,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;
+    "ttr", "takes 2 arguments. Name of the transformation (with one term argument) and a term" , test_transformation_one_arg_term;
     "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);