Added code gaps, unit + stdlib checking

Author: Gustavo2622

src/ecCorePrinting.ml

@@ -76,6 +76,8 @@ module type PrinterAPI = sig
 
   val pp_codepos       : PPEnv.t -> EcMatching.Position.codepos pp
   val pp_codepos_range : PPEnv.t -> EcMatching.Position.codepos_range pp
+  val pp_codegap1      : PPEnv.t -> EcMatching.Position.codegap1 pp
+  val pp_codegap       : PPEnv.t -> EcMatching.Position.codegap pp
 
   (* ------------------------------------------------------------------ *)
   type vsubst = [

src/ecLowPhlGoal.ml

@@ -390,6 +390,35 @@ let o_split ?rev env i s =
   try  Pos.may_split_at_cpos1 ?rev env i s
   with Pos.InvalidCPos -> raise (InvalidSplit (oget i))
 
+(* Gap-based split functions *)
+let s_split_at_gap env (g : codegap1) s =
+  let module Pos = EcMatching.Position in
+  try  Pos.split_at_cgap1 env g s
+  with Pos.InvalidCPos ->
+    let cp = match g with GapBefore cp | GapAfter cp -> cp in
+    raise (InvalidSplit cp)
+
+let o_split_at_gap ?rev env (g : codegap1 option) s =
+  let module Pos = EcMatching.Position in
+  try  Pos.may_split_at_cgap1 ?rev env g s
+  with Pos.InvalidCPos ->
+    let cp = match oget g with GapBefore cp | GapAfter cp -> cp in
+    raise (InvalidSplit cp)
+
+(* -------------------------------------------------------------------- *)
+(* 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 =
   match (FApi.tc1_goal tc).f_node with