Reworked outline tactic

* Reworked outline and function unification. No longer need to provide left-values, instead use the alias mode via '~'.

* more refactoring, using the new code position ranges

* slightly more flexible unification

Author: Cameron-Low

examples/MEE-CBC/CBC.eca

@@ -187,7 +187,7 @@ section Random_Ideal.
   equiv Random_Ideal: Random.enc ~ Ideal.enc: size p{1} = size p{2} ==> ={res}.
   proof.
   proc.
-  outline {2} [1] { r <@ Sampling.Sample.sample(size p + 1); }.
+  outline {2} 1 by { r <@ Sampling.Sample.sample(size p + 1); }.
   rewrite equiv[{2} 1 Sampling.Sample_LoopSnoc_eq].
   by inline; wp; while (={i} /\ c{1} = l{2} /\ size p{1} + 1 = n{2}); auto=> /#.
   qed.

src/ecMatching.ml

@@ -252,13 +252,20 @@ module Zipper = struct
 
   let zipper_of_cpos_range env cpr s =
     let top, bot = cpr in
-    let zpr = zipper_of_cpos env top s in
+    let zpr, (_, pos) = zipper_of_cpos_r env top s in
     match bot with
-    | `Base cp ->
-      let path = (zipper_of_cpos env cp s).z_path in
-      if path <> zpr.z_path then
+    | `Base cp -> begin
+      let zpr', (_, pos') = zipper_of_cpos_r env cp s in
+      (* The two positions should identify the same block *)
+      if zpr'.z_path <> zpr.z_path then
         raise InvalidCPos;
-      zpr, snd cp
+
+      (* The end position should be after the start *)
+      match pos, pos' with
+      | (_, `ByPos x), (_, `ByPos y) when x <= y ->
+          zpr, (0, `ByPos (y - x))
+      | _ -> raise InvalidCPos
+    end
     | `Offset cp1 -> zpr, cp1
 
   let split_at_cpos1 env cpos1 s =

src/ecParser.mly

@@ -2904,8 +2904,9 @@ interleave_info:
    { (s, c1, c2 :: c3, k) }
 
 %inline outline_kind:
-| s=brace(stmt) { OKstmt(s) }
-| r=sexpr? LEAT f=loc(fident) { OKproc(f, r) }
+| BY s=brace(stmt) { OKstmt(s) }
+| TILD f=loc(fident) { OKproc(f, true) }
+| f=loc(fident) { OKproc(f, false) }
 
 %public phltactic:
 | PROC
@@ -2985,11 +2986,10 @@ interleave_info:
 | INLINE s=side? u=inlineopt? p=codepos
     { Pinline (`CodePos (s, u, p)) }
 
-| OUTLINE s=side LBRACKET st=codepos1 e=option(MINUS e=codepos1 {e}) RBRACKET k=outline_kind
+| OUTLINE s=side cpr=codepos_or_range k=outline_kind
     { Poutline {
 	  outline_side  = s;
-	  outline_start = st;
-	  outline_end   = odfl st e;
+	  outline_range = cpr;
 	  outline_kind  = k }
     }
 

src/ecParsetree.ml

@@ -665,12 +665,11 @@ type inline_info = [
 (* -------------------------------------------------------------------- *)
 type outline_kind =
   | OKstmt of pstmt
-  | OKproc of pgamepath * pexpr option
+  | OKproc of pgamepath * bool
 
 type outline_info = {
     outline_side: side;
-    outline_start: pcodepos1;
-    outline_end: pcodepos1;
+    outline_range: pcodepos_range;
     outline_kind: outline_kind;
 }
 

src/ecProofTyping.ml

@@ -173,19 +173,27 @@ let tc1_process_Xhl_formula ?side tc pf =
 let tc1_process_Xhl_formula_xreal tc pf =
   tc1_process_Xhl_form tc txreal pf
 
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos_range tc (side, cpr) =
+  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active me env in
+  EcTyping.trans_codepos_range env cpr
+
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos tc (side, cpos) =
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
   let env = EcEnv.Memory.push_active me env in
   EcTyping.trans_codepos env cpos
+
 (* ------------------------------------------------------------------ *)
 let tc1_process_codepos1 tc (side, cpos) =
   let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
   let env = FApi.tc1_env tc in
   let env = EcEnv.Memory.push_active me env in
   EcTyping.trans_codepos1 env cpos
-  
+
 (* ------------------------------------------------------------------ *)
 (* FIXME: factor out to typing module                                 *)
 (* FIXME: TC HOOK - check parameter constraints                       *)

src/ecProofTyping.mli

@@ -63,6 +63,7 @@ val tc1_process_stmt :
 val tc1_process_prhl_stmt :
      ?map:EcTyping.ismap -> tcenv1 -> side -> pstmt -> stmt
 
+val tc1_process_codepos_range : tcenv1 -> oside * pcodepos_range -> codepos_range
 val tc1_process_codepos : tcenv1 -> oside * pcodepos -> codepos
 val tc1_process_codepos1 : tcenv1 -> oside * pcodepos1 -> codepos1
 

src/ecTyping.mli

@@ -230,6 +230,7 @@ type ismap = (instr list) EcMaps.Mstr.t
 val transstmt : ?map:ismap -> env -> EcUnify.unienv -> pstmt -> stmt
 
 (* -------------------------------------------------------------------- *)
+val trans_codepos_range : ?memory:EcMemory.memory -> env -> pcodepos_range -> codepos_range
 val trans_codepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 -> codepos1
 val trans_codepos : ?memory:EcMemory.memory -> env -> pcodepos -> codepos
 val trans_dcodepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 doption -> codepos1 doption