summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon HO2024-06-13 15:19:11 +0200
committerGitHub2024-06-13 15:19:11 +0200
commit234fa36da87b672397f96098bcf832d869f2cfbb (patch)
treeafb669e46c958fc516b8441278a006582d7f2400 /compiler
parent40e79f1fd64a6535334b1af19a817b27a9a0296c (diff)
parent87d088fa9e4493f32ae3f8d447ff1ff6d44e6396 (diff)
Merge pull request #242 from AeneasVerif/son/scalars2
Update the scalar notations for the Lean backend
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml6
-rw-r--r--compiler/ExtractTypes.ml14
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