partial fix to bugs in skolem expression creation. revealed other bug…

…s in type-checking.

lib/frontend/rewrites/heapsExplicitTrnsl.ml

@@ -3305,6 +3305,8 @@ module TrnslExhale = struct
             List.fold var_decls_skolem_idents ~init:(Map.empty (module QualIdent)) ~f:(
               fun map (vd, skolem_id) -> (
                 let skolemized_expr = 
+                  let univ_args = List.map univ_vars.univ_vars ~f:(fun (_, vd) -> Expr.from_var_decl vd) 
+                  in
                   let optn_args = begin
                     match Map.find witness_args_conds_exprs_map vd.var_name with
                     | None -> []
@@ -3314,7 +3316,7 @@ module TrnslExhale = struct
                       List.map env_local_var_decls_exprs ~f:(fun (_vd, expr) -> expr) 
                     end 
                   in
-                  Expr.mk_app ~loc ~typ:(vd.var_type) (Expr.Var (QualIdent.from_ident skolem_id)) optn_args
+                  Expr.mk_app ~loc ~typ:(vd.var_type) (Expr.Var (QualIdent.from_ident skolem_id)) (univ_args @ optn_args)
 
                 in
 
@@ -3752,7 +3754,9 @@ module TrnslExhale = struct
 
           if QualIdent.(orig_name = Predefs.lib_auth_mod_qual_ident) then
             match given_expr with
-            | App (DataConstr constr_ident, exprs, _) ->
+            | App (DataConstr constr_ident, exprs, _) 
+            | App (Var constr_ident, exprs, _) ->
+              (* #TODO: This exception is added to tackle the case of using AuthRA.auth() function, which is different from the AuthRA.auth_frag() data constructor. As such, this exception is not added in the explicit calculation which should ideally be fixed. *)
                 if
                   Ident.(
                     QualIdent.unqualify constr_ident

lib/frontend/typing.ml

@@ -124,6 +124,18 @@ end
 let check_and_set (expr : expr) (given_typ_lb : type_expr)
     (given_typ_ub : type_expr) (expected_typ : type_expr) : expr Rewriter.t =
   let open Rewriter.Syntax in
+
+  Logs.debug (fun m -> m "Frontend.typing.check_and_set: expr: %a;
+  given_typ_lb: %a
+  given_typ_ub: %a
+  expected_typ: %a"
+    Expr.pr expr
+    Type.pr given_typ_lb
+    Type.pr given_typ_ub
+    Type.pr expected_typ 
+  );
+
+
   let expected_ghost = Type.is_ghost expected_typ in
   let+ given_typ_lb =
     try ProcessTypeExpr.expand_type_expr given_typ_lb
@@ -139,12 +151,13 @@ let check_and_set (expr : expr) (given_typ_lb : type_expr)
   in            
   let typ = Type.meet given_typ_ub expected_typ |> Type.set_ghost expected_ghost in
   if Type.subtype_of given_typ_lb typ then Expr.set_type expr typ
-  else type_mismatch_error (Expr.to_loc expr) expected_typ given_typ_ub
+  else 
+    (Logs.debug (fun m -> m "type_mismatch_error:0"); type_mismatch_error (Expr.to_loc expr) expected_typ given_typ_ub)
 
 (** Infer and check type of [expr] subject to typing environment [tbl] and expected type [expected_typ] *)
 let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
   =
-  Logs.debug (fun m -> m !"process_expr: %{Expr} %b" expr (Type.is_ghost expected_typ));
+  Logs.debug (fun m -> m !"process_expr: %{Expr}; isGhost: %b" expr (Type.is_ghost expected_typ));
   let open Rewriter.Syntax in
   match expr with
   | App (constr, expr_list, expr_attr) -> (
@@ -988,6 +1001,7 @@ module ProcessCallable = struct
                     },
                   disam_tbl )
             | typ ->
+              Logs.debug (fun m -> m "type_mismatch_error:1");
               type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ
             end
         | _ ->
@@ -1016,6 +1030,7 @@ module ProcessCallable = struct
                   },
                 disam_tbl )
             | typ ->
+              Logs.debug (fun m -> m "type_mismatch_error:2");
               type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ
             end
         | _ -> Error.type_error loc "commitAU takes at least one argument"
@@ -1034,6 +1049,7 @@ module ProcessCallable = struct
               ( Stmt.AUAction { auaction_kind = AbortAU token },
                 disam_tbl )
             | typ ->
+              Logs.debug (fun m -> m "type_mismatch_error:3");
               type_mismatch_error (Expr.to_loc token) (Type.atomic_token (Ident.make Loc.dummy "?" 0 |> QualIdent.from_ident)) typ
             end
         | _ -> Error.type_error loc "abortAU takes exactly one argument"
@@ -1566,7 +1582,8 @@ module ProcessCallable = struct
 
         (Stmt.New new_desc, disam_tbl)
       else
-        type_mismatch_error stmt_loc Type.ref var_decl.var_type
+        (Logs.debug (fun m -> m "type_mismatch_error:4");
+        type_mismatch_error stmt_loc Type.ref var_decl.var_type)
       (* The following constructs are not expected here because the parser stores these commands as Assign stmts.
          The job of this function is to intercept the Assign stmts with the specific expressions on the RHS, and then transform
          them to the appropriate construct, ie Call, New, BindAU, OpenAU, AbortAU, CommitAU etc.

test/concurrent/templates/give-up-simplified.rav

@@ -198,7 +198,7 @@ interface GiveUpTemplate[Node: NodeImpl] {
     atomic requires css(r, c)
     atomic ensures css(r, c) && nodePred(r, n, c_n, i_n) && inFP(r, n)
   {
-    ghost var phi: AtomicToken := bindAU();
+    ghost var phi := bindAU();
 
     ghost var g_i0: Flow_K;
 
@@ -222,7 +222,7 @@ interface GiveUpTemplate[Node: NodeImpl] {
     atomic requires css(r, c)
     atomic ensures css(r, c) && inFP(r, n)
   {
-    ghost var phi: AtomicToken := bindAU();
+    ghost var phi := bindAU();
     ghost val c1: Set[K] := openAU(phi);
     unfold css(r, c1);
     cssInFp(r, n, c1);
@@ -330,7 +330,7 @@ interface GiveUpTemplate[Node: NodeImpl] {
   lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], c_n: Set[K], i_n: Flow_K, implicit ghost g_i: Flow_K)
     requires cssR(r, c, g_i)
     requires nodePred(r, n, c_n, i_n)
-f    requires k in outset(i_n, n1)
+    requires k in outset(i_n, n1)
     requires n in g_i.dom
     ensures cssR(r, c, g_i)
     ensures nodePred(r, n, c_n, i_n)
@@ -361,7 +361,7 @@ f    requires k in outset(i_n, n1)
     ensures inFP(r, nn)
     ensures k in keyset(i_nn)
   {
-    ghost val phi: AtomicToken := bindAU();
+    ghost val phi := bindAU();
 
     ghost var c_n: Set[K];
     ghost var i_n: Flow_K;
@@ -473,7 +473,7 @@ f    requires k in outset(i_n, n1)
     atomic requires css(r, c)
     atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res))
   {
-    ghost val phi: AtomicToken := bindAU();
+    ghost val phi := bindAU();
 
     var n: Ref;
     var c_n: Set[K];