Fix issue #905, improve error message on missing two sided memory

Author: Gustavo2622

src/ecTyping.ml

@@ -116,6 +116,9 @@ type filter_error =
 | FE_InvalidIndex of int
 | FE_NoMatch
 
+type goal_shape_error = 
+| GSE_ExpectedTwoSided
+
 type tyerror =
 | UniVarNotAllowed
 | FreeTypeVariables
@@ -180,6 +183,7 @@ type tyerror =
 | ProcAssign             of qsymbol
 | PositiveShouldBeBeforeNegative
 | NotAnExpression        of [`Unknown | `LL | `Pr | `Logic | `Glob | `MemSel]
+| UnexpectedGoalShape    of goal_shape_error
 
 (* -------------------------------------------------------------------- *)
 exception TyError of EcLocation.t * EcEnv.env * tyerror
@@ -3194,7 +3198,10 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
 
                 map_ss_inv f_tuple res in
 
-              let ml, mr = oget (EcEnv.Memory.get_active_ts env) in
+              let ml, mr = match (EcEnv.Memory.get_active_ts env) with
+              | Some (ml, mr) -> ml, mr
+              | None -> tyerror f.pl_loc env (UnexpectedGoalShape GSE_ExpectedTwoSided)
+              in
               let x1 = ss_inv_generalize_right (create ml) mr in
               let x2 = ss_inv_generalize_left (create mr) ml in
 

src/ecTyping.mli

@@ -108,6 +108,10 @@ type filter_error =
 | FE_InvalidIndex of int
 | FE_NoMatch
 
+
+type goal_shape_error = 
+| GSE_ExpectedTwoSided
+
 type tyerror =
 | UniVarNotAllowed
 | FreeTypeVariables
@@ -172,6 +176,7 @@ type tyerror =
 | ProcAssign             of qsymbol
 | PositiveShouldBeBeforeNegative
 | NotAnExpression        of [`Unknown | `LL | `Pr | `Logic | `Glob | `MemSel]
+| UnexpectedGoalShape    of goal_shape_error
 
 exception TymodCnvFailure of tymod_cnv_failure
 exception TyError of EcLocation.t * env * tyerror

src/ecUserMessages.ml

@@ -226,6 +226,12 @@ end = struct
     | FXE_SynCheckFailure ->
         msg "syntactic termination check failure"
 
+  let pp_gse_error _env fmt error =
+    let msg = Format.fprintf fmt in
+    match error with
+    | GSE_ExpectedTwoSided -> 
+        msg "expected two sided goal"
+
   let pp_tyerror env1 fmt error =
     let env   = EcPrinting.PPEnv.ofenv env1 in
     let msg x = Format.fprintf fmt x in
@@ -551,6 +557,9 @@ end = struct
       end
     end
 
+    | UnexpectedGoalShape gse ->
+        msg "unexpected goal shape %a" (pp_gse_error env) gse
+
   let pp_restr_error env fmt (w, e) =
     let ppe = EcPrinting.PPEnv.ofenv env in