WIP

src/ecFol.ml

@@ -1039,9 +1039,7 @@ let destr_ands ~deep =
 
   in fun f -> doit f
 
-
-(*---------------------------------------------*)
-
+(* -------------------------------------------------------------------- *)
 let rec one_sided mem fp =
   match fp.f_node with
   | Fint   _      -> true

src/ecHiGoal.ml

@@ -1974,11 +1974,17 @@ let process_right (tc : tcenv1) =
     tc_error !!tc "cannot apply `right` on that goal"
 
 (* -------------------------------------------------------------------- *)
-let process_split ?i (tc : tcenv1) =
-  let i = Option.map (fun n -> int_of_string n.pl_desc) i in
-  try  t_ors [EcLowGoal.t_split ?i; EcLowGoal.t_split_prind] tc
+let process_split ?(i : int option) (tc : tcenv1) =
+  let tactics : FApi.backward list =
+    match i with
+    | None -> [EcLowGoal.t_split; EcLowGoal.t_split_prind]
+    | Some i -> [EcLowGoal.t_split ~i] in
+
+  try  t_ors tactics tc
   with InvalidGoalShape ->
-    tc_error !!tc "cannot apply `split` on(Option.map (fun n -> int_of_string n.pl_desc) i) that goal"
+    tc_error !!tc
+      "cannot apply `split/%a` on that goal"
+      (EcPrinting.pp_opt Format.pp_print_int) i
 
 (* -------------------------------------------------------------------- *)
 let process_elim (pe, qs) tc =

src/ecHiGoal.mli

@@ -82,7 +82,7 @@ val process_cut         : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward
 val process_cutdef      : ttenv -> cutdef_t -> backward
 val process_left        : backward
 val process_right       : backward
-val process_split       : ?i:psymbol -> backward
+val process_split       : ?i:int -> backward
 val process_elim        : prevert * pqsymbol option -> backward
 val process_case        : ?doeq:bool -> prevertv -> backward
 val process_exists      : ppt_arg located list -> backward

src/ecLowGoal.ml

@@ -1511,23 +1511,50 @@ let t_elim_iso_or ?reduce tc =
     let tc = t_elim_prind_r ?reduce ~accept `Case tc in (oget !outgoals, tc)
 
 
-let rec t_and_i i opsym (f1, f2 : form pair) (tc : tcenv1) =
-  if i <= 0 then
-    begin
-      let tc =
-        FApi.mutate1 tc (fun hd -> VConv (hd, Sid.empty))
-          (EcFol.f_and f1 f2)
-      in
+(* -------------------------------------------------------------------- *)
+let t_split_and_i (i : int) (f : form) (tc : tcenv1) =
+  assert (0 <= i);
+
+  let fsl, fsr =
+    let rec destr (acc : ([`Asym | `Sym] * form) list) (i  : int) (f : form) =
+      if i < 0 then
+        (List.rev acc, f)
+      else
+        match sform_of_form f with
+        | SFand (b, (f1, f2)) ->
+            destr ((b, f1) :: acc) (i - 1) f2
+        | _ -> assert false in
+
+    destr [] i f in
+
+  let fsl =
+    let rec doit = function
+      | [] -> assert false
+      | [_, f] -> f
+      | (b, f) :: fs ->
+          (match b with `Asym -> f_anda | `Sym -> f_and) f (doit fs) in
+
+    doit fsl in
+
+  FApi.xmutate1
+    tc (fun hd -> VConv (hd, Sid.empty)) [fsl; fsr]
+
+
+(*
+  if i <= 0 then begin
+    let tc =
+      FApi.mutate1 tc (fun hd -> VConv (hd, Sid.empty))
+        (EcFol.f_and f1 f2)
+    in
+    t_and_intro_s opsym (f1, f2) tc
+  end else begin
+    match sform_of_form f2 with
+    | SFand (b, (f1', f2')) ->
+      t_and_i (i - 1) b (EcFol.f_and f1 f1', f2') tc
+    | _ ->
       t_and_intro_s opsym (f1, f2) tc
   end
-  else
-    begin
-      match sform_of_form f2 with
-      | SFand (b, (f1', f2')) ->
-        t_and_i (i - 1) b (EcFol.f_and f1 f1', f2') tc
-      |  _ ->
-        t_and_intro_s opsym (f1, f2) tc
-    end
+  *)
 
 (* -------------------------------------------------------------------- *)
 let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) =
@@ -1537,8 +1564,8 @@ let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) =
     match sform_of_form fp with
     | SFtrue ->
         t_true tc
-    | SFand (b, (f1, f2)) when not closeonly ->
-      t_and_i i b (f1, f2) tc
+    | SFand _ when not closeonly ->
+        t_split_and_i i fp tc
     | SFiff (f1, f2) when not closeonly ->
         t_iff_intro_s (f1, f2) tc
     | SFeq (f1, f2) when not closeonly && (is_tuple f1 && is_tuple f2) ->

src/ecParser.mly

@@ -2785,8 +2785,8 @@ logtactic:
 | SMT LPAREN dbmap=dbmap1* RPAREN
    { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) }
 
-| SPLIT i=loc(STRING)?
-    { Psplit i}
+| SPLIT i=word?
+    { Psplit i }
 
 | FIELD eqs=ident*
     { Pfield eqs }

src/ecParsetree.ml

@@ -938,7 +938,7 @@ type logtactic =
   | Preflexivity
   | Passumption
   | Psmt        of pprover_infos
-  | Psplit      of psymbol option
+  | Psplit      of int option
   | Pfield      of psymbol list
   | Pring       of psymbol list
   | Palg_norm