Merge pull request #242 from AeneasVerif/son/scalars2

Update the scalar notations for the Lean backend

2 files changed, 13 insertions, 7 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index eab85054..4acf3f99 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -241,11 +241,12 @@ let rec extract_typed_pattern (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (is_let : bool) (inside : bool) ?(with_type = false)
     (v : typed_pattern) : extraction_ctx =
   if with_type then F.pp_print_string fmt "(";
+  let is_pattern = true in
   let inside = inside && not with_type in
   let ctx =
     match v.value with
     | PatConstant cv ->
-        extract_literal span fmt inside cv;
+        extract_literal span fmt is_pattern inside cv;
         ctx
     | PatVar (v, _) ->
         let vname = ctx_compute_var_basename span ctx v.basename v.ty in
@@ -307,6 +308,7 @@ let extract_texpression_errors (fmt : F.formatter) =
 
 let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
+  let is_pattern = false in
   match e.e with
   | Var var_id ->
       let var_name = ctx_get_var span var_id ctx in
@@ -314,7 +316,7 @@ let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
   | CVar var_id ->
       let var_name = ctx_get_const_generic_var span var_id ctx in
       F.pp_print_string fmt var_name
-  | Const cv -> extract_literal span fmt inside cv
+  | Const cv -> extract_literal span fmt is_pattern inside cv
   | App _ ->
       let app, args = destruct_apps e in
       extract_App span ctx fmt inside app args
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 15e75da2..631db13e 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -11,12 +11,13 @@ include ExtractBase
 
     Inputs:
     - formatter
+    - [is_pattern]: if [true], it means we are generating a (match) pattern
     - [inside]: if [true], the value should be wrapped in parentheses
       if it is made of an application (ex.: [U32 3])
     - the constant value
  *)
-let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
-    (cv : literal) : unit =
+let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
+    (inside : bool) (cv : literal) : unit =
   match cv with
   | VScalar sv -> (
       match backend () with
@@ -39,8 +40,11 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               let iname = int_name sv.int_ty in
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
-              let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt ("#" ^ iname)
+              (* We don't use the same notation for patterns and regular literals *)
+              if is_pattern then F.pp_print_string fmt "#scalar"
+              else
+                let iname = String.lowercase_ascii (int_name sv.int_ty) in
+                F.pp_print_string fmt ("#" ^ iname)
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
@@ -409,7 +413,7 @@ let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
   | CgGlobal id ->
       let s = ctx_get_global span id ctx in
       F.pp_print_string fmt s
-  | CgValue v -> extract_literal span fmt inside v
+  | CgValue v -> extract_literal span fmt false inside v
   | CgVar id ->
       let s = ctx_get_const_generic_var span id ctx in
       F.pp_print_string fmt s