diff options
| author | Son Ho | 2024-03-08 08:03:37 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-08 08:03:37 +0100 |
| commit | e1e888f23935bfb34830fe160593e09df75a7f20 (patch) | |
| tree | 952a5dbf2b65e0076cc9e3aea49d3bd9c4b07b95 /compiler | |
| parent | bc397dea5c5a67766c9c0381efad222524f68881 (diff) | |
Update the code generation
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 8 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 5 |
2 files changed, 6 insertions, 7 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index db887539..5aa8323e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -782,9 +782,13 @@ let ctx_get_termination_measure (def_id : A.FunDeclId.id) let unop_name (unop : unop) : string = match unop with | Not -> ( - match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~") + match !backend with + | FStar -> "not" + | Lean -> "¬" + | Coq -> "negb" + | HOL4 -> "~") | Neg (int_ty : integer_type) -> ( - match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg") + match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg") | Cast _ -> (* We never directly use the unop name in this case *) raise (Failure "Unsupported") diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 51e3fd77..a3dbf3cc 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -31,11 +31,6 @@ let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit = (* We need to add parentheses if the value is negative *) if sv.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.value) - else if !backend = Lean then - (* TODO: parsing issues with Lean because there are ambiguous - interpretations between int values and nat values *) - F.pp_print_string fmt - ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))") else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")"); (match !backend with | Coq -> |