summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml130
1 files changed, 89 insertions, 41 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 95ba2f02..3ea3a862 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -64,7 +64,11 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
| FStar | Coq -> int_name int_ty ^ "_" ^ binop
(** A list of keywords/identifiers used by the backend and with which we
- want to check collision. *)
+ want to check collision.
+
+ Remark: this is useful mostly to look for collisions when generating
+ names for *variables*.
+ *)
let keywords () =
let named_unops =
unop_name Not
@@ -80,58 +84,108 @@ let keywords () =
match !backend with
| FStar ->
[
- "let";
- "rec";
- "in";
+ "assert";
+ "assert_norm";
+ "assume";
+ "else";
"fun";
"fn";
- "val";
- "int";
- "list";
"FStar";
"FStar.Mul";
- "type";
+ "if";
+ "in";
+ "include";
+ "int";
+ "let";
+ "list";
"match";
- "with";
- "assert";
- "assert_norm";
- "assume";
+ "not";
+ "open";
+ "rec";
+ "scalar_cast";
+ "then";
+ "type";
"Type0";
"Type";
"unit";
- "not";
- "scalar_cast";
+ "val";
+ "with";
]
| Coq ->
[
- "Record";
- "Inductive";
- "Fixpoint";
- "Definition";
+ "assert";
"Arguments";
- "Notation";
- "Check";
- "Search";
- "SearchPattern";
"Axiom";
- "Type";
- "Set";
- "let";
- "rec";
- "in";
- "unit";
+ "char_of_byte";
+ "Check";
+ "Declare";
+ "Definition";
+ "else";
+ "End";
"fun";
- "type";
+ "Fixpoint";
+ "if";
+ "in";
"int";
+ "Inductive";
+ "Import";
+ "let";
+ "Lemma";
"match";
- "with";
- "assert";
+ "Module";
"not";
+ "Notation";
+ "Proof";
+ "Qed";
+ "rec";
+ "Record";
+ "Require";
+ "Scope";
+ "Search";
+ "SearchPattern";
+ "Set";
+ "then";
(* [tt] is unit *)
"tt";
- "char_of_byte";
+ "type";
+ "Type";
+ "unit";
+ "with";
+ ]
+ | Lean ->
+ [
+ "by";
+ "class";
+ "decreasing_by";
+ "def";
+ "deriving";
+ "do";
+ "else";
+ "end";
+ "for";
+ "have";
+ "if";
+ "inductive";
+ "instance";
+ "import";
+ "let";
+ "macro";
+ "match";
+ "namespace";
+ "open";
+ "return";
+ "run_cmd";
+ "set_option";
+ "simp";
+ "structure";
+ "syntax";
+ "termination_by";
+ "then";
+ "Type";
+ "unsafe";
+ "where";
+ "with";
]
- | Lean -> [] (* TODO *)
in
List.concat [ named_unops; named_binops; misc ]
@@ -222,14 +276,8 @@ let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
(* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
[ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
| Lean ->
- [
- (Return, "return");
- (Fail, "fail_");
- (Assert, "massert");
- (* TODO: figure out how to deal with this *)
- (FuelDecrease, "decrease");
- (FuelEqZero, "is_zero");
- ]
+ (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+ [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ]
let names_map_init () : names_map_init =
{