PR: Refactor codepositions

Author: Gustavo2622

examples/global-hybrid/GlobalHybridExamp2.ec

@@ -416,7 +416,7 @@ rcondf{1} 1; first auto.
 rcondf{2} 1; first auto; smt().
 rcondt{2} 1; first auto.
 wp; inline*.
-swap{2} 2 -1; swap{2} 6 -4; swap{2} 10 -7.
+swap{2} 2 -1; swap{2} 6 -4. 
 seq 2 3 :
   (#pre /\ x{1} = r0{2} /\ y{1} = r1{2} /\
    x0{2} = A); first auto.

src/ecCorePrinting.ml

@@ -68,10 +68,17 @@ module type PrinterAPI = sig
   val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp
 
   (* ------------------------------------------------------------------ *)
-  val pp_codepos1    : PPEnv.t -> EcMatching.Position.codepos1 pp
-  val pp_codeoffset1 : PPEnv.t -> EcMatching.Position.codeoffset1 pp
-
-  val pp_codepos     : PPEnv.t -> EcMatching.Position.codepos pp
+  val pp_codepos1      : PPEnv.t -> EcMatching.Position.codepos1 pp
+  val pp_codepos_brsel : EcMatching.Position.codepos_brsel pp
+  val pp_codepos_step  : PPEnv.t -> EcMatching.Position.codepos_step pp
+  val pp_codepos_path  : PPEnv.t -> EcMatching.Position.codepos_path pp
+  val pp_codeoffset1   : PPEnv.t -> EcMatching.Position.codeoffset1 pp
+
+  val pp_codepos        : PPEnv.t -> EcMatching.Position.codepos pp
+  val pp_codegap1       : PPEnv.t -> EcMatching.Position.codegap1 pp
+  val pp_codegap        : PPEnv.t -> EcMatching.Position.codegap pp
+  val pp_codegap1_range : PPEnv.t -> EcMatching.Position.codegap1_range pp
+  val pp_codegap_range  : PPEnv.t -> EcMatching.Position.codegap_range pp
 
   (* ------------------------------------------------------------------ *)
   type vsubst = [

src/ecHiTacticals.ml

@@ -238,11 +238,15 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
 
   try  tx tc
   with (* PHL Specific low errors *)
-  | EcLowPhlGoal.InvalidSplit cpos1 ->
+  | EcLowPhlGoal.InvalidSplit is ->
       tc_error_lazy !!tc (fun fmt ->
         let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in
         Format.fprintf fmt "invalid split index: %a"
-          (EcPrinting.pp_codepos1 ppe) cpos1)
+        (fun fmt is -> match is with
+        | `Gap gap -> Format.fprintf fmt "%a" EcPrinting.(pp_codegap1 ppe) gap
+        | `Instr i -> Format.fprintf fmt "%a" EcPrinting.(pp_codepos1 ppe) i
+        ) is)
+          
 
 (* -------------------------------------------------------------------- *)
 and process_sub (ttenv : ttenv) tts tc =

src/ecLowPhlGoal.ml

@@ -207,11 +207,18 @@ let tc1_get_stmt side tc =
       tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc
 
 (* ------------------------------------------------------------------ *)
-let tc1_process_codepos_range tc (side, cpr) =
+let tc1_process_codepos_or_range tc (side, cpor) =
   let me, _ = tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
   let env = EcEnv.Memory.push_active_ss me env in
-  EcTyping.trans_codepos_range env cpr
+  EcTyping.trans_codepos_or_range env cpor
+
+(* ------------------------------------------------------------------ *)
+let tc1_process_codegap_range tc (side, cgr) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codegap_range env cgr
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos tc (side, cpos) =
@@ -379,22 +386,37 @@ let logicS_post_read (env : env) (f : logicS) =
       add EcPV.PMVS.empty (es_po es).inv
 
 (* -------------------------------------------------------------------- *)
-exception InvalidSplit of codepos1
+exception InvalidSplit of [ `Instr of codepos1 | `Gap of codegap1 ]
+
 
 let s_split env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.split_at_cpos1 env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit i)
+  let module Pos = EcMatching.Position in
+  try  Pos.split_at_cgap1 env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i))
 
 let s_split_i env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.find_by_cpos1 ~rev:false env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit i)
+  let module Pos = EcMatching.Position in
+  try  Pos.find_by_cpos1 ~rev:false env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit (`Instr i))
 
 let o_split ?rev env i s =
-  let module Zpr = EcMatching.Zipper in
-  try  Zpr.may_split_at_cpos1 ?rev env i s
-  with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))
+  let module Pos = EcMatching.Position in
+  try  Pos.may_split_at_cgap1 ?rev env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit (`Gap(oget i)))
+
+(* -------------------------------------------------------------------- *)
+(* Gap processing functions *)
+let tc1_process_codegap1 tc (side, g) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codegap1 env g
+
+let tc1_process_codegap tc (side, g) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codegap env g
 
 (* -------------------------------------------------------------------- *)
 let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc =
@@ -740,14 +762,14 @@ let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
     let env = EcEnv.LDecl.toenv (snd cenv) in
     let (me, f) = Zpr.fold env cenv cpos (fun _ -> f) state s in
       ((me, f, []) : memenv * _ * form list)
-  with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
+  with InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
 let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
   try
     let env = EcEnv.LDecl.toenv (snd cenv) in
     let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in
       ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
-  with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
+  with InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
 let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
   let pf = FApi.tc1_penv tc in