summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore3
-rw-r--r--backends/IsabelleHOL/Primitives.thy19
-rw-r--r--backends/IsabelleHOL/ROOT6
-rw-r--r--backends/IsabelleHOL/document/root.tex60
-rw-r--r--compiler/Config.ml7
-rw-r--r--compiler/Extract.ml285
-rw-r--r--compiler/ExtractBase.ml108
-rw-r--r--compiler/ExtractBuiltin.ml18
-rw-r--r--compiler/ExtractTypes.ml105
-rw-r--r--compiler/Main.ml6
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/SymbolicToPure.ml2
-rw-r--r--compiler/Translate.ml39
13 files changed, 528 insertions, 132 deletions
diff --git a/.gitignore b/.gitignore
index 67b16555..45010773 100644
--- a/.gitignore
+++ b/.gitignore
@@ -79,3 +79,6 @@ nohup.out
*/.#*
*.smt2
.DS_Store
+
+# Isabelle output
+backends/IsabelleHOL/output
diff --git a/backends/IsabelleHOL/Primitives.thy b/backends/IsabelleHOL/Primitives.thy
new file mode 100644
index 00000000..a0cc40bd
--- /dev/null
+++ b/backends/IsabelleHOL/Primitives.thy
@@ -0,0 +1,19 @@
+theory Primitives imports
+ Main
+ "HOL-Library.Monad_Syntax"
+begin
+
+
+datatype u32 = u32 nat
+datatype 'a result = Ok 'a | Err
+fun u32_lt :: "u32 \<Rightarrow> u32 \<Rightarrow> bool" where
+ "u32_lt (u32 a) (u32 b) = (a < b)"
+
+definition bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow> 'b result" where
+ "bind m f \<equiv> (case m of Err \<Rightarrow> Err | Ok a \<Rightarrow> f a)"
+
+adhoc_overloading Monad_Syntax.bind bind
+
+declare bind_def[simp]
+
+end \ No newline at end of file
diff --git a/backends/IsabelleHOL/ROOT b/backends/IsabelleHOL/ROOT
new file mode 100644
index 00000000..9f8e0820
--- /dev/null
+++ b/backends/IsabelleHOL/ROOT
@@ -0,0 +1,6 @@
+session Aeneas = "HOL-Library" +
+ options [document = pdf, document_output = "output"]
+ theories [document = false]
+ Primitives
+ document_files
+ "root.tex"
diff --git a/backends/IsabelleHOL/document/root.tex b/backends/IsabelleHOL/document/root.tex
new file mode 100644
index 00000000..63ac8e42
--- /dev/null
+++ b/backends/IsabelleHOL/document/root.tex
@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+ %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+ %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+ %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+ %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+ %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+ %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+ %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+ %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{IsabelleHOL}
+\author{stuebinm}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 98a5eea1..0abe94a9 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -3,9 +3,9 @@
(** {1 Backend choice} *)
(** The choice of backend *)
-type backend = FStar | Coq | Lean | HOL4
+type backend = FStar | Coq | Lean | HOL4 | IsabelleHOL
-let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ]
+let backend_names = [ "fstar"; "coq"; "lean"; "hol4"; "IsabelleHOL"]
(** Utility to compute the backend from an input parameter *)
let backend_of_string (b : string) : backend option =
@@ -14,6 +14,7 @@ let backend_of_string (b : string) : backend option =
| "coq" -> Some Coq
| "lean" -> Some Lean
| "hol4" -> Some HOL4
+ | "IsabelleHOL" -> Some IsabelleHOL
| _ -> None
let opt_backend : backend option ref = ref None
@@ -374,7 +375,7 @@ let variant_concatenate_type_name = ref true
let use_tuple_structs = ref true
let backend_has_tuple_projectors backend =
- match backend with Lean -> true | Coq | FStar | HOL4 -> false
+ match backend with Lean -> true | Coq | FStar | HOL4 | IsabelleHOL -> false
(** Toggle the use of tuple projectors *)
let use_tuple_projectors = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index cf632388..e640edd1 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -62,6 +62,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
match backend () with
| Coq | FStar -> ctx
| HOL4 -> craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
+ | IsabelleHOL -> craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
| Lean -> ctx_add_decreases_proof def ctx
else ctx
in
@@ -280,7 +281,7 @@ let lets_require_wrap_in_do (span : Meta.span)
| Lean ->
(* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
List.exists (fun (m, _, _) -> m) lets
- | HOL4 ->
+ | HOL4 | IsabelleHOL ->
(* HOL4 is similar to HOL4, but we add a sanity check *)
let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
if wrap_in_do then
@@ -305,7 +306,7 @@ let extract_texpression_errors (fmt : F.formatter) =
match backend () with
| FStar | Coq -> F.pp_print_string fmt "admit"
| Lean -> F.pp_print_string fmt "sorry"
- | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+ | HOL4 | IsabelleHOL -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
(fmt : F.formatter) (inside : bool) (e : texpression) : unit =
@@ -596,7 +597,7 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
(* Check if we need to extract the type as a tuple *)
if is_tuple_struct then
match backend () with
- | FStar | HOL4 | Coq -> FieldId.to_string proj.field_id
+ | FStar | HOL4 | Coq | IsabelleHOL -> FieldId.to_string proj.field_id
| Lean ->
(* Tuples in Lean are syntax sugar for nested products/pairs,
so we need to map the field id accordingly.
@@ -644,15 +645,24 @@ and extract_field_projector (span : Meta.span) (ctx : extraction_ctx)
in
(* Open a box *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (* Extract the expression *)
- extract_texpression span ctx fmt true arg;
- (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
- if backend () <> Lean then F.pp_print_break fmt 0 0;
- F.pp_print_string fmt ".";
- (* If in Coq, the field projection has to be parenthesized *)
- (match backend () with
- | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
- | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+ (* In Isabelle, there is no special record syntax, so fake a function call *)
+ if backend () = IsabelleHOL then (
+ if inside then F.pp_print_string fmt "(";
+ F.pp_print_string fmt field_name;
+ F.pp_print_space fmt ();
+ extract_texpression span ctx fmt true arg;
+ if inside then F.pp_print_string fmt ")")
+ else (
+ (* Extract the expression *)
+ extract_texpression span ctx fmt true arg;
+ (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
+ if backend () <> Lean then F.pp_print_break fmt 0 0;
+ F.pp_print_string fmt ".";
+ (* If in Coq, the field projection has to be parenthesized *)
+ (match backend () with
+ | FStar | Lean | HOL4 | IsabelleHOL -> F.pp_print_string fmt field_name
+ | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+ );
(* Close the box *)
F.pp_close_box fmt ()
| arg :: args ->
@@ -718,7 +728,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let lets, next_e =
match backend () with
| HOL4 -> destruct_lets_no_interleave span e
- | FStar | Coq | Lean -> destruct_lets e
+ | FStar | Coq | Lean | IsabelleHOL -> destruct_lets e
in
(* Extract the let-bindings *)
let extract_let (ctx : extraction_ctx) (monadic : bool) (lv : typed_pattern)
@@ -743,7 +753,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let arrow =
match backend () with
| Coq | HOL4 -> "<-"
- | FStar | Lean -> craise __FILE__ __LINE__ span "impossible"
+ | FStar | Lean | IsabelleHOL -> craise __FILE__ __LINE__ span "impossible"
in
F.pp_print_string fmt arrow;
F.pp_print_space fmt ();
@@ -760,7 +770,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| Coq | Lean ->
F.pp_print_string fmt "let";
F.pp_print_space fmt ()
- | HOL4 -> ()
+ | HOL4 | IsabelleHOL -> ()
else (
F.pp_print_string fmt "let";
F.pp_print_space fmt ());
@@ -772,6 +782,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| Coq -> ":="
| Lean -> if monadic then "←" else ":="
| HOL4 -> if monadic then "<-" else "="
+ | IsabelleHOL -> if monadic then "\\<leftarrow>" else "="
in
F.pp_print_string fmt eq;
F.pp_print_space fmt ();
@@ -783,7 +794,13 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
()
| Coq | FStar | HOL4 ->
F.pp_print_space fmt ();
- F.pp_print_string fmt "in");
+ F.pp_print_string fmt "in";
+ | IsabelleHOL ->
+ if monadic then
+ F.pp_print_string fmt ";"
+ else (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "in"));
ctx)
in
(* Close the box for the let-binding *)
@@ -798,7 +815,10 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
at the end of every let-binding: let-bindings are indeed not ended
with an "in" keyword.
*)
- if backend () = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
+ if backend () = Lean then
+ F.pp_open_vbox fmt 0
+ else
+ F.pp_open_hvbox fmt (if backend () = IsabelleHOL then ctx.indent_incr else 0);
(* Open parentheses *)
if inside && backend () <> Lean then F.pp_print_string fmt "(";
(* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
@@ -806,6 +826,8 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let wrap_in_do_od = lets_require_wrap_in_do span lets in
if wrap_in_do_od then (
F.pp_print_string fmt "do";
+ if backend () = IsabelleHOL then (
+ F.pp_print_string fmt " {");
F.pp_print_space fmt ());
let ctx =
List.fold_left
@@ -820,10 +842,13 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* do-box (Lean and HOL4 only) *)
- if wrap_in_do_od then
+ if wrap_in_do_od then (
if backend () = HOL4 then (
F.pp_print_space fmt ();
F.pp_print_string fmt "od");
+ if backend () = IsabelleHOL then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "}"));
(* Close parentheses *)
if inside && backend () <> Lean then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
@@ -845,6 +870,8 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| If (e_then, e_else) ->
(* Open a box for the [if e] *)
F.pp_open_hovbox fmt ctx.indent_incr;
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt "(";
F.pp_print_string fmt "if";
if backend () = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
F.pp_print_space fmt ();
@@ -875,7 +902,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "begin";
F.pp_print_space fmt
- | Coq | Lean | HOL4 ->
+ | Coq | Lean | HOL4 | IsabelleHOL ->
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
F.pp_print_cut fmt)
@@ -896,13 +923,15 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| FStar ->
F.pp_print_space fmt ();
F.pp_print_string fmt "end"
- | Coq | Lean | HOL4 -> F.pp_print_string fmt ")");
+ | Coq | Lean | HOL4 | IsabelleHOL -> F.pp_print_string fmt ")");
(* Close the box for the then/else+branch *)
F.pp_close_box fmt ()
in
extract_branch true e_then;
- extract_branch false e_else
+ extract_branch false e_else;
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt ")"
| Match branches -> (
(* Open a box for the [match ... with] *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -912,7 +941,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| FStar -> "begin match"
| Coq -> "match"
| Lean -> if ctx.use_dep_ite then "match h:" else "match"
- | HOL4 ->
+ | HOL4 | IsabelleHOL ->
(* We're being extra safe in the case of HOL4 *)
"(case"
in
@@ -924,12 +953,15 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
extract_texpression span ctx fmt scrut_inside scrut;
F.pp_print_space fmt ();
let match_scrut_end =
- match backend () with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+ match backend () with FStar | Coq | Lean -> "with" | HOL4 | IsabelleHOL -> "of"
in
F.pp_print_string fmt match_scrut_end;
(* Close the box for the [match ... with] *)
F.pp_close_box fmt ();
+ let
+ first = ref true;
+ in
(* Extract the branches *)
let extract_branch (br : match_branch) : unit =
F.pp_print_space fmt ();
@@ -938,12 +970,16 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the pattern *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the pattern *)
- F.pp_print_string fmt "|";
+ if not !first && backend () = IsabelleHOL then
+ F.pp_print_string fmt "|"
+ else
+ F.pp_print_space fmt ();
+ first := false;
F.pp_print_space fmt ();
let ctx = extract_typed_pattern span ctx fmt false false br.pat in
F.pp_print_space fmt ();
let arrow =
- match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+ match backend () with FStar -> "->" | Coq | Lean | HOL4 -> "=>" | IsabelleHOL -> "\\<Rightarrow>"
in
F.pp_print_string fmt arrow;
(* Close the box for the pattern *)
@@ -956,7 +992,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the box for the branch *)
F.pp_close_box fmt ();
(* Close the box for the pattern+branch *)
- F.pp_close_box fmt ()
+ F.pp_close_box fmt ();
in
List.iter extract_branch branches;
@@ -967,7 +1003,7 @@ and extract_Switch (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
| FStar | Coq ->
F.pp_print_space fmt ();
F.pp_print_string fmt "end"
- | HOL4 -> F.pp_print_string fmt ")"));
+ | HOL4 | IsabelleHOL -> F.pp_print_string fmt ")"));
(* Close the box for the whole expression *)
F.pp_close_box fmt ()
@@ -1019,13 +1055,14 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
match backend () with
| Lean | FStar -> (Some "{", Some "}")
| Coq -> (Some "{|", Some "|}")
- | HOL4 -> (None, None)
+ | HOL4 | IsabelleHOL -> (None, None)
in
(* Inner brackets *)
let ilb, irb =
match backend () with
| Lean | FStar | Coq -> (None, None)
| HOL4 -> (Some "<|", Some "|>")
+ | IsabelleHOL -> (Some "\\<lparr>", Some "\\<rparr>")
in
(* Helper *)
let print_bracket (is_left : bool) b =
@@ -1037,22 +1074,25 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
| None -> ()
in
print_bracket true olb;
- let need_paren = inside && backend () = HOL4 in
+ let need_paren = inside && backend () = HOL4 || backend () = IsabelleHOL in
if need_paren then F.pp_print_string fmt "(";
F.pp_open_hvbox fmt ctx.indent_incr;
if supd.init <> None then (
let var_name = ctx_get_var span (Option.get supd.init) ctx in
F.pp_print_string fmt var_name;
F.pp_print_space fmt ();
- F.pp_print_string fmt "with";
- F.pp_print_space fmt ());
+ if backend () <> IsabelleHOL then (
+ F.pp_print_string fmt "with";
+ F.pp_print_space fmt ()));
print_bracket true ilb;
F.pp_open_hvbox fmt 0;
let delimiter =
- match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+ match backend () with Lean | IsabelleHOL -> "," | Coq | FStar | HOL4 -> ";"
in
let assign =
- match backend () with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+ match backend () with
+ | Coq | Lean | HOL4 | FStar -> "="
+ | IsabelleHOL -> if supd.init <> None then ":=" else "="
in
Collections.List.iter_link
(fun () ->
@@ -1100,7 +1140,7 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
F.pp_close_box fmt ();
(* Print the values *)
let delimiter =
- match backend () with Lean -> "," | Coq | FStar | HOL4 -> ";"
+ match backend () with Lean -> "," | Coq | FStar | HOL4 | IsabelleHOL -> ";"
in
F.pp_print_space fmt ();
F.pp_open_hovbox fmt 0;
@@ -1179,16 +1219,18 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
insert_req_space fmt space;
(* Open a box for the input parameter *)
F.pp_open_hovbox fmt 0;
- F.pp_print_string fmt "(";
+ if backend () <> IsabelleHOL then
+ F.pp_print_string fmt "(";
let ctx =
extract_typed_pattern def.item_meta.span ctx fmt true false lv
in
- F.pp_print_space fmt ();
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
- lv.ty;
- F.pp_print_string fmt ")";
+ if backend () <> IsabelleHOL then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
+ lv.ty;
+ F.pp_print_string fmt ")");
(* Close the box for the input parameters *)
F.pp_close_box fmt ();
ctx)
@@ -1597,9 +1639,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ()
in
(* Print the "=" *)
+ if backend () = IsabelleHOL then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "where \"";
+ F.pp_print_string fmt def_name);
if not is_opaque then (
F.pp_print_space fmt ();
- let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+ let eq = match backend () with FStar | HOL4 | IsabelleHOL -> "=" | Coq | Lean -> ":=" in
F.pp_print_string fmt eq);
(* Close the box for "(PARAMS) : EFFECT =" *)
F.pp_close_box fmt ();
@@ -1704,6 +1750,128 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if backend () <> HOL4 || decl_is_not_last_from_group kind then
F.pp_print_break fmt 0 0
+
+(** Extract a function definition for Isabelle/HOL. Written as its own
+ function since the syntax is a little more different from the others *)
+let extract_fun_decl_isabelle (ctx : extraction_ctx) (fmt : F.formatter)
+ (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
+ sanity_check __FILE__ __LINE__
+ (not def.is_global_decl_body)
+ def.item_meta.span;
+ (* Retrieve the function name *)
+ let def_name = ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx in
+ (* Add a break before *)
+ F.pp_print_break fmt 0 0;
+ (* Print a comment to link the extracted definition to its original rust definition *)
+ extract_fun_comment ctx fmt def;
+ F.pp_print_space fmt ();
+ (* Open two boxes for the definition, so that whenever possible it gets printed on
+ * one line and indents are correct *)
+ F.pp_open_hvbox fmt 0;
+ F.pp_open_vbox fmt ctx.indent_incr;
+
+ (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+ F.pp_open_vbox fmt ctx.indent_incr;
+
+ (* > "fun FUN_NAME" *)
+ (* Open a box for the "function FUN_NAME :: FUN_TYPE where" *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+
+ (* Print the top-level command *)
+ if def.signature.inputs = [] then (
+ (* functions must have at least one argument; if we have non, use definition *)
+ F.pp_print_string fmt "definition";
+ F.pp_print_space fmt ())
+ else if Option.is_some def.loop_id then (
+ (* Isabelle has "fun" and "function", which requires an explicit termination proof;
+ "fun" can prove most things, but struggles with loops, so these get a blanket
+ explicit proof
+ *)
+ F.pp_print_string fmt "function";
+ F.pp_print_space fmt ())
+ else (
+ let qualif = fun_decl_kind_to_qualif kind in
+ (match qualif with
+ | Some qualif ->
+ F.pp_print_string fmt qualif;
+ F.pp_print_space fmt ()
+ | None -> ()));
+ F.pp_print_string fmt def_name;
+ F.pp_print_space fmt ();
+
+ (* Open a box for the :: FUN_TYPE *)
+ F.pp_open_hvbox fmt 0;
+
+ (* print the function's type. TODO: this is in the wrong order;
+ the context still lacks some type variables, so this currently
+ breaks traits / sort constraints
+ *)
+ let _ =
+ (* Open a box for the return type *)
+ F.pp_open_hbox fmt ();
+ F.pp_print_string fmt "::";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "\"";
+ (* Print the return type *)
+ (* For opaque definitions, as we don't have named parameters under the hand,
+ * we don't print parameters in the form [(x : a) (y : b) ...] above,
+ * but wait until here to print the types: [a -> b -> ...]. *)
+ extract_fun_input_parameters_types ctx fmt def;
+ (* [Tot] *)
+ if has_decreases_clause then (
+ assert_backend_supports_decreases_clauses def.item_meta.span);
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty has_decreases_clause
+ def.signature.output;
+ (* Close the box for the return type *)
+ F.pp_print_string fmt "\"";
+ F.pp_close_box fmt ();
+ in
+ (* Close the box for ":: FUN_TYPE" *)
+ F.pp_close_box fmt ();
+ F.pp_print_string fmt " where";
+ (* Close the box for the "function FUN_NAME :: FUN_TYPE where" *)
+ F.pp_close_box fmt ();
+ F.pp_print_space fmt ();
+ (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
+ F.pp_close_box fmt ();
+
+ (* Open a box for the body *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+ (* Open a box for the parameters *)
+ F.pp_open_hbox fmt ();
+ F.pp_print_string fmt "\"";
+ F.pp_print_string fmt def_name;
+ let ctx, ctx_body, all_params = extract_fun_parameters (ref false) ctx fmt def in
+ F.pp_print_string fmt " =";
+ (* Close the box for the parameters *)
+ F.pp_close_box fmt ();
+ F.pp_print_space fmt ();
+
+ (* Extract the body *)
+ let _ =
+ extract_texpression def.item_meta.span ctx_body fmt false (Option.get def.body).body
+ in
+ (* Close the box for the body *)
+ F.pp_close_box fmt ();
+ (* Close the inner box for the definition *)
+ F.pp_close_box fmt ();
+ (* Close the quote of the function equation *)
+ F.pp_print_string fmt "\"";
+ (* Termination clause and proof for Lean *)
+
+ (* Close the outer box for the definition *)
+ F.pp_close_box fmt ();
+
+ (* if a loop, add a by-auto clause and hope it's enough *)
+ if Option.is_some def.loop_id then
+ F.pp_print_string fmt " by auto";
+
+ (* Add breaks to insert new lines between definitions *)
+ (* if decl_is_not_last_from_group kind then *)
+ F.pp_print_break fmt 0 0
+
+
+
(** Extract an opaque function declaration to HOL4.
Remark (SH): having to treat this specific case separately is very annoying,
@@ -1771,6 +1939,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* We treat HOL4 opaque functions in a specific manner *)
if backend () = HOL4 && Option.is_none def.body then
extract_fun_decl_hol4_opaque ctx fmt def
+ else if backend () = IsabelleHOL then
+ extract_fun_decl_isabelle ctx fmt kind has_decreases_clause def
else extract_fun_decl_gen ctx fmt kind has_decreases_clause def
(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY"
@@ -1833,7 +2003,7 @@ let extract_global_decl_body_gen (span : Meta.span) (ctx : extraction_ctx)
if not is_opaque then (
(* Print " =" *)
F.pp_print_space fmt ();
- let eq = match backend () with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
+ let eq = match backend () with FStar | HOL4 | IsabelleHOL -> "=" | Coq | Lean -> ":=" in
F.pp_print_string fmt eq);
(* Close ": TYPE =" box (depth=2) *)
F.pp_close_box fmt ();
@@ -1998,6 +2168,11 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "get_return_value";
F.pp_print_space fmt ()),
fun () -> () )
+ | IsabelleHOL ->
+ ( (fun () ->
+ F.pp_print_string fmt "value";
+ F.pp_print_space fmt ()),
+ fun () -> () )
in
before ();
if use_brackets then F.pp_print_string fmt "(";
@@ -2305,12 +2480,16 @@ let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter)
(item_name : string) (separator : string) (ty : unit -> unit) : unit =
F.pp_print_space fmt ();
F.pp_open_hovbox fmt ctx.indent_incr;
+ if backend () = IsabelleHOL then F.pp_print_string fmt "(";
F.pp_print_string fmt item_name;
F.pp_print_space fmt ();
(* ":" or "=" *)
F.pp_print_string fmt separator;
ty ();
- (match backend () with Lean -> () | _ -> F.pp_print_string fmt ";");
+ (match backend () with
+ | Lean -> ()
+ | IsabelleHOL -> F.pp_print_string fmt ")"
+ | _ -> F.pp_print_string fmt ";");
F.pp_close_box fmt ()
let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter)
@@ -2366,7 +2545,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
f.signature.llbc_generics generics ctx
in
let backend_uses_forall =
- match backend () with Coq | Lean -> true | FStar | HOL4 -> false
+ match backend () with Coq | Lean -> true | FStar | HOL4 | IsabelleHOL -> false
in
let generics_not_empty = generics <> empty_generic_params in
let use_forall = generics_not_empty && backend_uses_forall in
@@ -2457,6 +2636,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
in
F.pp_print_string fmt (":= " ^ cons ^ " {")
+ | IsabelleHOL ->
+ let cons = ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx in
+ F.pp_print_string fmt ("= " ^ cons)
| _ -> F.pp_print_string fmt "{");
(* Close the box for the name + generics *)
@@ -2533,7 +2715,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
if backend () <> Lean then F.pp_close_box fmt ();
(* Close the brackets *)
match backend () with
- | Lean -> ()
+ | Lean | IsabelleHOL -> ()
| Coq ->
F.pp_print_space fmt ();
F.pp_print_string fmt "}."
@@ -2985,6 +3167,17 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
if sg.inputs <> [] then (
F.pp_print_space fmt ();
F.pp_print_string fmt "()");
+ F.pp_print_string fmt "”)";
+ | IsabelleHOL ->
+ F.pp_print_string fmt "val _ = test_the_thing (";
+ F.pp_print_string fmt "“";
+ let fun_name =
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
+ in
+ F.pp_print_string fmt fun_name;
+ if sg.inputs <> [] then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "()");
F.pp_print_string fmt "”)");
(* Close the box for the test *)
F.pp_close_box fmt ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4d05f0d0..710009c4 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -512,7 +512,7 @@ let str_name () = if backend () = Lean then "String" else "string"
let int_name (int_ty : integer_type) : string =
let isize, usize, i_format, u_format =
match backend () with
- | FStar | Coq | HOL4 ->
+ | FStar | Coq | HOL4 | IsabelleHOL ->
("isize", "usize", format_of_string "i%d", format_of_string "u%d")
| Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
in
@@ -534,9 +534,9 @@ let scalar_name (ty : literal_type) : string =
match ty with
| TInteger ty -> int_name ty
| TBool -> (
- match backend () with FStar | Coq | HOL4 -> "bool" | Lean -> "Bool")
+ match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "bool" | Lean -> "Bool")
| TChar -> (
- match backend () with FStar | Coq | HOL4 -> "char" | Lean -> "Char")
+ match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "char" | Lean -> "Char")
(** Extraction context.
@@ -799,7 +799,8 @@ let unop_name (unop : unop) : string =
| FStar -> "not"
| Lean -> "¬"
| Coq -> "negb"
- | HOL4 -> "~")
+ | HOL4 -> "~"
+ | IsabelleHOL -> "\\<not>")
| Neg (int_ty : integer_type) -> (
match backend () with Lean -> "-." | _ -> int_name int_ty ^ "_neg")
| Cast _ ->
@@ -832,7 +833,7 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
(* Remark: the Lean case is actually not used *)
match backend () with
| Lean -> int_name int_ty ^ "." ^ binop_s
- | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s
+ | FStar | Coq | HOL4 | IsabelleHOL -> int_name int_ty ^ "_" ^ binop_s
(** A list of keywords/identifiers used by the backend and with which we
want to check collision.
@@ -1047,6 +1048,32 @@ let keywords () =
"then";
"Theorem";
]
+ | IsabelleHOL ->
+ [
+ "axiomatization";
+ "case";
+ "definition";
+ "else";
+ "end";
+ "fix";
+ "function";
+ "fun";
+ "if";
+ "in";
+ "int";
+ "inductive";
+ "let";
+ "of";
+ "proof";
+ "lemma";
+ "qed";
+ "then";
+ "theorem";
+ "extract";
+ "o";
+ "value"
+ (* TODO: this list is very incomplete, and ironically probably contains things which aren't keywords *)
+ ]
in
List.concat [ named_unops; named_binops; misc ]
@@ -1055,7 +1082,7 @@ let assumed_adts () : (assumed_ty * string) list =
if !use_state then
match backend () with
| Lean -> [ (TState, "State") ]
- | Coq | FStar | HOL4 -> [ (TState, "state") ]
+ | Coq | FStar | HOL4 | IsabelleHOL -> [ (TState, "state") ]
else []
in
(* We voluntarily omit the type [Error]: it is never directly
@@ -1073,7 +1100,7 @@ let assumed_adts () : (assumed_ty * string) list =
(TRawPtr Mut, "MutRawPtr");
(TRawPtr Const, "ConstRawPtr");
]
- | Coq | FStar | HOL4 ->
+ | Coq | FStar | HOL4 | IsabelleHOL ->
[
(TResult, "result");
(TFuel, if backend () = HOL4 then "num" else "nat");
@@ -1092,6 +1119,7 @@ let assumed_struct_constructors () : (assumed_ty * string) list =
| Coq -> [ (TArray, "mk_array") ]
| FStar -> [ (TArray, "mk_array") ]
| HOL4 -> [ (TArray, "mk_array") ]
+ | IsabelleHOL -> [ (TArray, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match backend () with
@@ -1132,10 +1160,19 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
]
+ | IsabelleHOL ->
+ [
+ (TResult, result_ok_id, "Ok");
+ (TResult, result_fail_id, "Fail");
+ (TError, error_failure_id, "Failure");
+ (TError, error_out_of_fuel_id, "OutOfFuel");
+ (* No Fuel::Zero on purpose *)
+ (* No Fuel::Succ on purpose *)
+ ]
let assumed_llbc_functions () : (A.assumed_fun_id * string) list =
match backend () with
- | FStar | Coq | HOL4 ->
+ | FStar | Coq | HOL4 | IsabelleHOL ->
[
(ArrayIndexShared, "array_index_usize");
(ArrayIndexMut, "array_index_mut_usize");
@@ -1175,6 +1212,9 @@ let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
| HOL4 ->
(* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
[ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+ | IsabelleHOL ->
+ (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+ [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
let names_map_init () : names_map_init =
{
@@ -1310,6 +1350,15 @@ let type_decl_kind_to_qualif (span : Meta.span) (kind : decl_kind)
| Assumed -> Some "axiom"
| Declared -> Some "axiom")
| HOL4 -> None
+ | IsabelleHOL -> (
+ match kind with
+ | SingleNonRec -> Some "datatype"
+ | SingleRec -> Some "datatype"
+ | MutRecFirst -> Some "datatype"
+ | MutRecInner -> Some "and"
+ | MutRecLast -> Some "and"
+ | Assumed -> Some "axiomatization"
+ | Declared -> Some "aximoatization")
(** Compute the qualified for a function definition/declaration.
@@ -1347,6 +1396,15 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
| Assumed -> Some "axiom"
| Declared -> Some "axiom")
| HOL4 -> None
+ | IsabelleHOL -> (
+ match kind with
+ | SingleNonRec -> Some "fun"
+ | SingleRec -> Some "fun"
+ | MutRecFirst -> Some "fun"
+ | MutRecInner -> Some "and"
+ | MutRecLast -> Some "and"
+ | Assumed -> Some "axiomatization"
+ | Declared -> Some "axiomatization")
(** The type of types.
@@ -1356,7 +1414,7 @@ let type_keyword (span : Meta.span) =
match backend () with
| FStar -> "Type0"
| Coq | Lean -> "Type"
- | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+ | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
(** Helper *)
let name_last_elem_as_ident (span : Meta.span) (n : llbc_name) : string =
@@ -1410,7 +1468,7 @@ let ctx_compute_type_name (item_meta : Types.item_meta) (ctx : extraction_ctx)
match backend () with
| FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
| Coq | HOL4 -> name ^ "_t"
- | Lean -> name
+ | Lean | IsabelleHOL -> name
(** Inputs:
- type name
@@ -1447,7 +1505,7 @@ let ctx_compute_field_name (def : type_decl) (field_meta : Meta.attr_info)
^ "_" ^ field_name_s
in
match backend () with
- | Lean | HOL4 -> name
+ | Lean | HOL4 | IsabelleHOL -> name
| Coq | FStar -> StringUtils.lowercase_first_letter name
(** Inputs:
@@ -1461,7 +1519,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
Option.value variant.attr_info.rename ~default:variant.variant_name
in
match backend () with
- | FStar | Coq | HOL4 ->
+ | FStar | Coq | HOL4 | IsabelleHOL ->
let variant = to_camel_case variant in
(* Prefix the name of the variant with the name of the type, if necessary
(some backends don't support collision of variant names) *)
@@ -1494,14 +1552,14 @@ let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
(* TODO: don't convert to snake case for Coq, HOL4, F* *)
let fname = flatten_name fname in
match backend () with
- | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
+ | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter fname
| Lean -> fname
(** Provided a basename, compute the name of a global declaration. *)
let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
(name : llbc_name) : string =
match Config.backend () with
- | Coq | FStar | HOL4 ->
+ | Coq | FStar | HOL4 | IsabelleHOL ->
let parts =
List.map to_snake_case (ctx_compute_simple_name span ctx name)
in
@@ -1582,7 +1640,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
(* Additional modifications to make sure we comply with the backends restrictions *)
match backend () with
| FStar -> StringUtils.lowercase_first_letter name
- | Coq | HOL4 | Lean -> name
+ | Coq | HOL4 | Lean | IsabelleHOL -> name
let ctx_compute_trait_decl_constructor (ctx : extraction_ctx)
(trait_decl : trait_decl) : string =
@@ -1659,7 +1717,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
let clause = clause ^ "Inst" in
match backend () with
| FStar -> StringUtils.lowercase_first_letter clause
- | Coq | HOL4 | Lean -> clause
+ | Coq | HOL4 | Lean | IsabelleHOL -> clause
let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
(item : string) : string =
@@ -1676,7 +1734,7 @@ let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
can't disambiguate fields coming from different ADTs if they have the same
names), and thus don't need to add a prefix starting with a lowercase.
*)
- match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 -> name
+ match backend () with FStar -> "t" ^ name | Coq | Lean | HOL4 | IsabelleHOL -> name
let ctx_compute_trait_const_name (ctx : extraction_ctx)
(trait_decl : trait_decl) (item : string) : string =
@@ -1685,7 +1743,7 @@ let ctx_compute_trait_const_name (ctx : extraction_ctx)
else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ item
in
(* See [trait_type_name] *)
- match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 -> name
+ match backend () with FStar -> "c" ^ name | Coq | Lean | HOL4 | IsabelleHOL -> name
let ctx_compute_trait_method_name (ctx : extraction_ctx)
(trait_decl : trait_decl) (item : string) : string =
@@ -1723,7 +1781,7 @@ let ctx_compute_termination_measure_name (span : Meta.span)
match Config.backend () with
| FStar -> "_decreases"
| Lean -> "_terminates"
- | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+ | Coq | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
in
(* Concatenate *)
fname ^ lp_suffix ^ suffix
@@ -1751,7 +1809,7 @@ let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
let suffix =
match Config.backend () with
| Lean -> "_decreases"
- | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+ | FStar | Coq | HOL4 | IsabelleHOL -> craise __FILE__ __LINE__ span "Unexpected"
in
(* Concatenate *)
fname ^ lp_suffix ^ suffix
@@ -1792,7 +1850,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
(* This should be a no-op *)
match Config.backend () with
| Lean -> basename
- | FStar | Coq | HOL4 -> to_snake_case basename)
+ | FStar | Coq | HOL4 | IsabelleHOL -> to_snake_case basename)
| None -> (
(* No basename: we use the first letter of the type *)
match ty with
@@ -1824,7 +1882,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx)
(* TODO: use "t" also for F* *)
match backend () with
| FStar -> "x" (* lacking inspiration here... *)
- | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
+ | Coq | Lean | HOL4 | IsabelleHOL -> "t" (* lacking inspiration here... *))
| TLiteral lty -> (
match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
| TArrow _ -> "f"
@@ -1839,7 +1897,7 @@ let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
| FStar ->
(* This is *not* a no-op: this removes the capital letter *)
to_snake_case basename
- | HOL4 ->
+ | HOL4 | IsabelleHOL ->
(* In HOL4, type variable names must start with "'" *)
"'" ^ to_snake_case basename
| Coq | Lean -> basename
@@ -1849,7 +1907,7 @@ let ctx_compute_const_generic_var_basename (_ctx : extraction_ctx)
(basename : string) : string =
(* Rust type variables are snake-case and start with a capital letter *)
match backend () with
- | FStar | HOL4 ->
+ | FStar | HOL4 | IsabelleHOL ->
(* This is *not* a no-op: this removes the capital letter *)
to_snake_case basename
| Coq | Lean -> basename
@@ -1871,7 +1929,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
in
let clause = clause ^ "Inst" in
match backend () with
- | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
+ | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter clause
| Lean -> clause
let trait_self_clause_basename = "self_clause"
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 37b676bb..f0460035 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -44,7 +44,7 @@ let split_on_separator (s : string) : string list =
let flatten_name (name : string list) : string =
match backend () with
- | FStar | Coq | HOL4 -> String.concat "_" name
+ | FStar | Coq | HOL4 | IsabelleHOL -> String.concat "_" name
| Lean -> String.concat "." name
(** Utility for Lean-only definitions **)
@@ -61,7 +61,7 @@ let () =
is F*, Coq or HOL4, and a different value if the target is Lean.
*)
let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
- match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+ match backend () with Coq | FStar | HOL4 | IsabelleHOL -> fstar_coq_hol4 | Lean -> lean
let builtin_globals : (string * string) list =
[
@@ -135,10 +135,10 @@ type type_variant_kind =
let mk_struct_constructor (type_name : string) : string =
let prefix =
- match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+ match backend () with FStar -> "Mk" | Coq | HOL4 | IsabelleHOL -> "mk" | Lean -> ""
in
let suffix =
- match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk"
+ match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "" | Lean -> ".mk"
in
prefix ^ type_name ^ suffix
@@ -168,7 +168,7 @@ let builtin_types () : builtin_type_info list =
( rname,
match backend () with
| FStar | Lean -> name
- | Coq | HOL4 -> extract_name ^ "_" ^ name ))
+ | Coq | HOL4 | IsabelleHOL -> extract_name ^ "_" ^ name ))
fields
in
let constructor = mk_struct_constructor extract_name in
@@ -201,7 +201,7 @@ let builtin_types () : builtin_type_info list =
extract_name =
(match backend () with
| Lean -> "Option"
- | Coq | FStar | HOL4 -> "option");
+ | Coq | FStar | HOL4 | IsabelleHOL -> "option");
keep_params = None;
body_info =
Some
@@ -211,7 +211,7 @@ let builtin_types () : builtin_type_info list =
rust_variant_name = "None";
extract_variant_name =
(match backend () with
- | FStar | Coq -> "None"
+ | FStar | Coq | IsabelleHOL -> "None"
| Lean -> "none"
| HOL4 -> "NONE");
fields = None;
@@ -220,7 +220,7 @@ let builtin_types () : builtin_type_info list =
rust_variant_name = "Some";
extract_variant_name =
(match backend () with
- | FStar | Coq -> "Some"
+ | FStar | Coq | IsabelleHOL -> "Some"
| Lean -> "some"
| HOL4 -> "SOME");
fields = None;
@@ -574,7 +574,7 @@ let builtin_trait_decls_info () =
in
let type_name =
match backend () with
- | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
+ | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter type_name
| Lean -> type_name
in
let clauses = [] in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 78382179..0162310a 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -23,7 +23,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
| VScalar sv -> (
match backend () with
| FStar -> F.pp_print_string fmt (Z.to_string sv.value)
- | Coq | HOL4 | Lean ->
+ | Coq | HOL4 | Lean | IsabelleHOL ->
let print_brackets = inside && backend () = HOL4 in
if print_brackets then F.pp_print_string fmt "(";
(match backend () with
@@ -54,6 +54,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
match backend () with
| HOL4 -> if b then "T" else "F"
| Coq | FStar | Lean -> if b then "true" else "false"
+ | IsabelleHOL -> if b then "True" else "False"
in
F.pp_print_string fmt b
| VChar c -> (
@@ -62,6 +63,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
(* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
| FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+ | IsabelleHOL -> F.pp_print_string fmt ("CHR ''" ^ String.make 1 c ^ "''")
| Coq ->
if inside then F.pp_print_string fmt "(";
F.pp_print_string fmt "char_of_byte";
@@ -105,7 +107,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
(* HOL4 has a special treatment: because it doesn't support dependent
types, we don't have a specific operator for the cast *)
match backend () with
- | HOL4 ->
+ | HOL4 | IsabelleHOL ->
(* Casting, say, an u32 to an i32 would be done as follows:
{[
mk_i32 (u32_to_int x)
@@ -135,7 +137,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
| TInteger src, TInteger tgt ->
let cast_str =
match backend () with
- | Coq | FStar -> "scalar_cast"
+ | Coq | FStar | IsabelleHOL -> "scalar_cast"
| Lean -> "Scalar.cast"
| HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
in
@@ -148,7 +150,7 @@ let extract_unop (span : Meta.span) (extract_expr : bool -> texpression -> unit)
| TBool, TInteger tgt ->
let cast_str =
match backend () with
- | Coq | FStar -> "scalar_cast_bool"
+ | Coq | FStar | IsabelleHOL -> "scalar_cast_bool"
| Lean -> "Scalar.cast_bool"
| HOL4 -> craise __FILE__ __LINE__ span "Unreachable"
in
@@ -205,6 +207,7 @@ let extract_binop (span : Meta.span)
(* Some binary operations have a special notation depending on the backend *)
(match (backend (), binop) with
| HOL4, (Eq | Ne)
+ | IsabelleHOL, (Eq | Ne)
| (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
| Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) ->
let binop =
@@ -231,7 +234,7 @@ let extract_binop (span : Meta.span)
in
let binop =
match backend () with
- | FStar | Lean | HOL4 -> binop
+ | FStar | Lean | HOL4 | IsabelleHOL -> binop
| Coq -> "s" ^ binop
in
extract_expr false arg0;
@@ -283,7 +286,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(is_rec : bool) (dg : Pure.fun_decl list) =
match backend () with
- | FStar | Coq | Lean -> ()
+ | FStar | Coq | Lean | IsabelleHOL -> ()
| HOL4 ->
(* In HOL4, opaque functions have a special treatment *)
if is_single_opaque_fun_decl_group dg then ()
@@ -313,7 +316,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
(dg : Pure.fun_decl list) =
match backend () with
- | FStar -> ()
+ | FStar | IsabelleHOL -> ()
| Coq ->
(* For aesthetic reasons, we print the Coq end group delimiter directly
in {!extract_fun_decl}. *)
@@ -344,7 +347,7 @@ let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(is_rec : bool) (dg : Pure.type_decl list) =
match backend () with
- | FStar | Coq -> ()
+ | FStar | Coq | IsabelleHOL -> ()
| Lean ->
if is_rec && List.length dg > 1 then (
F.pp_print_space fmt ();
@@ -371,7 +374,7 @@ let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
(dg : Pure.type_decl list) =
match backend () with
- | FStar -> ()
+ | FStar | IsabelleHOL -> ()
| Coq ->
(* For aesthetic reasons, we print the Coq end group delimiter directly
in {!extract_fun_decl}. *)
@@ -402,12 +405,14 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
F.pp_print_break fmt 0 0)
let unit_name () =
- match backend () with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
+ match backend () with Lean -> "Unit" | Coq | FStar | HOL4 | IsabelleHOL -> "unit"
(** Small helper *)
let extract_arrow (fmt : F.formatter) () : unit =
- if Config.backend () = Lean then F.pp_print_string fmt "→"
- else F.pp_print_string fmt "->"
+ match Config.backend() with
+ | Lean -> F.pp_print_string fmt "→"
+ | IsabelleHOL -> F.pp_print_string fmt "\\<Rightarrow>"
+ | _ -> F.pp_print_string fmt "->"
let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
(fmt : F.formatter) (inside : bool) (cg : const_generic) : unit =
@@ -452,7 +457,7 @@ let extract_ty_errors (fmt : F.formatter) : unit =
match Config.backend () with
| FStar | Coq -> F.pp_print_string fmt "admit"
| Lean -> F.pp_print_string fmt "sorry"
- | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+ | HOL4 | IsabelleHOL -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
@@ -473,7 +478,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
let product =
match backend () with
| FStar -> "&"
- | Coq -> "*"
+ | Coq | IsabelleHOL -> "*"
| Lean -> "×"
| HOL4 -> "#"
in
@@ -517,7 +522,7 @@ let rec extract_ty (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_generic_args span ctx fmt no_params_tys generics;
if print_paren then F.pp_print_string fmt ")"
- | HOL4 ->
+ | HOL4 | IsabelleHOL ->
let { types; const_generics; trait_refs } = generics in
(* Const generics are not supported in HOL4 *)
cassert __FILE__ __LINE__ (const_generics = []) span
@@ -869,15 +874,16 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
(fmt : F.formatter) (type_decl_group : TypeDeclId.Set.t)
(type_name : string) (type_params : string list) (cg_params : string list)
- (cons_name : string) (fields : field list) : unit =
+ (cons_name : string) (fields : field list) (index : int): unit =
F.pp_print_space fmt ();
(* variant box *)
F.pp_open_hvbox fmt ctx.indent_incr;
(* [| Cons :]
* Note that we really don't want any break above so we print everything
* at once. *)
- let opt_colon = if backend () <> HOL4 then " :" else "" in
- F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon);
+ let opt_colon = if backend () <> HOL4 && backend () <> IsabelleHOL then " :" else "" in
+ let colon = if backend () <> IsabelleHOL || index <> 0 then "| " else "" in
+ F.pp_print_string fmt (colon ^ cons_name ^ opt_colon);
let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
extraction_ctx =
F.pp_print_space fmt ();
@@ -901,7 +907,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
F.pp_print_string fmt (field_name ^ " :");
F.pp_print_space fmt ();
ctx)
- | Coq | Lean | HOL4 -> ctx
+ | Coq | Lean | HOL4 | IsabelleHOL -> ctx
in
(* Print the field type *)
let inside = backend () = HOL4 in
@@ -923,7 +929,7 @@ let extract_type_decl_variant (span : Meta.span) (ctx : extraction_ctx)
(* Sanity check: HOL4 doesn't support const generics *)
sanity_check __FILE__ __LINE__ (cg_params = [] || backend () <> HOL4) span;
(* Print the final type *)
- if backend () <> HOL4 then (
+ if backend () <> HOL4 && backend () <> IsabelleHOL then (
F.pp_print_space fmt ();
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt type_name;
@@ -973,13 +979,13 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
Note that we already printed: [type s =]
*)
- let print_variant _variant_id (v : variant) =
+ let print_variant variant_id (v : variant) =
(* We don't lookup the name, because it may have a prefix for the type
id (in the case of Lean) *)
let cons_name = ctx_compute_variant_name ctx def v in
let fields = v.fields in
extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
- def_name type_params cg_params cons_name fields
+ def_name type_params cg_params cons_name fields (VariantId.to_int variant_id)
in
(* Print the variants *)
let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
@@ -993,7 +999,7 @@ let extract_type_decl_tuple_struct_body (span : Meta.span)
F.pp_print_space fmt ();
F.pp_print_string fmt (unit_name ()))
else
- let sep = match backend () with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
+ let sep = match backend () with Coq | FStar | HOL4 | IsabelleHOL -> "*" | Lean -> "×" in
Collections.List.iter_link
(fun () ->
F.pp_print_space fmt ();
@@ -1072,22 +1078,26 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(instead of a record). We start with the "normal" case: we extract it
as a record. *)
else if (not is_rec) || (backend () <> Coq && backend () <> Lean) then (
- if backend () <> Lean then F.pp_print_space fmt ();
- (* If Coq: print the constructor name *)
+ if backend () <> Lean then (
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt " "
+ else F.pp_print_space fmt ());
+ (* If Coq or Isabelle: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
- if backend () = Coq && not is_rec then (
+ if (backend () = Coq && not is_rec) || backend () = IsabelleHOL then (
F.pp_print_string fmt
(ctx_get_struct def.item_meta.span (TAdtId def.def_id) ctx);
- F.pp_print_string fmt " ");
+ if backend () = Coq then
+ F.pp_print_string fmt " ");
(match backend () with
- | Lean -> ()
+ | Lean | IsabelleHOL -> ()
| FStar | Coq -> F.pp_print_string fmt "{"
| HOL4 -> F.pp_print_string fmt "<|");
F.pp_print_break fmt 1 ctx.indent_incr;
(* The body itself *)
(* Open a box for the body *)
(match backend () with
- | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
+ | Coq | FStar | HOL4 | IsabelleHOL -> F.pp_open_hvbox fmt 0
| Lean -> F.pp_open_vbox fmt 0);
(* Print the fields *)
let print_field (field_id : FieldId.id) (f : field) : unit =
@@ -1096,12 +1106,19 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
in
(* Open a box for the field *)
F.pp_open_box fmt ctx.indent_incr;
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt "(";
F.pp_print_string fmt field_name;
- F.pp_print_space fmt ();
+ if backend () <> IsabelleHOL then
+ F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt "\"";
extract_ty def.item_meta.span ctx fmt type_decl_group false f.field_ty;
- if backend () <> Lean then F.pp_print_string fmt ";";
+ if backend () <> Lean && backend () <> IsabelleHOL then F.pp_print_string fmt ";";
+ if backend () = IsabelleHOL then
+ F.pp_print_string fmt "\")";
(* Close the box for the field *)
F.pp_close_box fmt ()
in
@@ -1112,7 +1129,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the box for the body *)
F.pp_close_box fmt ();
match backend () with
- | Lean -> ()
+ | Lean | IsabelleHOL -> ()
| FStar | Coq ->
F.pp_print_space fmt ();
F.pp_print_string fmt "}"
@@ -1136,7 +1153,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
in
let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
- def_name type_params cg_params cons_name fields)
+ def_name type_params cg_params cons_name fields 0)
in
()
@@ -1146,6 +1163,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
let ld, space, rd =
match backend () with
| Coq | FStar | HOL4 -> ("(** ", 4, " *)")
+ | IsabelleHOL -> ("(*", 3, "*)")
| Lean -> ("/- ", 3, " -/")
in
F.pp_open_vbox fmt space;
@@ -1263,7 +1281,7 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
(const_generics : const_generic_var list)
(trait_clauses : trait_clause list) : unit =
(* Note that in HOL4 we don't print the type parameters. *)
- if backend () <> HOL4 then (
+ if backend () <> HOL4 && backend () <> IsabelleHOL then (
(* Print the type parameters *)
if type_params <> [] then (
insert_req_space ();
@@ -1437,7 +1455,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
* one line. Note however that in the case of Lean line breaks are important
* for parsing: we thus use a hovbox. *)
(match backend () with
- | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
+ | Coq | FStar | HOL4 | IsabelleHOL -> F.pp_open_hvbox fmt 0
| Lean ->
if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
(* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
@@ -1479,7 +1497,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
| Lean ->
if type_kind = Some Struct && kind = SingleNonRec then "where"
else ":="
- | HOL4 -> "="
+ | HOL4 | IsabelleHOL -> "="
in
F.pp_print_string fmt eq)
else (
@@ -1519,6 +1537,11 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
if backend () <> HOL4 || decl_is_not_last_from_group kind then
+ F.pp_print_break fmt 0 0;
+
+ (* magic invocation to get field extractor functions & struct updates *)
+ if backend () = IsabelleHOL && type_kind = Some Struct then
+ F.pp_print_string fmt ("local_setup \\<open>Datatype_Records.mk_update_defs \\<^type_name>\\<open>"^def_name^"\\<close>\\<close>");
F.pp_print_break fmt 0 0
(** Extract an opaque type declaration to HOL4.
@@ -1558,6 +1581,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
Remark (SH): having to treat this specific case separately is very annoying,
but I could not find a better way.
*)
+(* TODO: same must be done for Isabelle *)
let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
(fmt : F.formatter) (def : type_decl) : unit =
(* Retrieve the definition name *)
@@ -1595,7 +1619,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
match backend () with
| FStar | Coq | Lean ->
extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
- | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def
+ | HOL4 | IsabelleHOL -> extract_type_decl_hol4_opaque ctx fmt def
(** Generate a [Argument] instruction in Coq to allow omitting implicit
arguments for variants, fields, etc..
@@ -1894,7 +1918,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
match backend () with
- | FStar | HOL4 -> ()
+ | FStar | HOL4 | IsabelleHOL -> ()
| Lean | Coq ->
if
not
@@ -1924,6 +1948,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
match backend () with
| Coq -> "Axiom"
| Lean -> "axiom"
+ | IsabelleHOL -> "axiomatization"
| FStar | HOL4 -> raise (Failure "Unexpected")
in
F.pp_print_string fmt axiom;
@@ -1953,7 +1978,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt "Type0"
| HOL4 ->
F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
- | Coq | Lean -> print_axiom ())
+ | Coq | Lean | IsabelleHOL -> print_axiom ())
| Declared -> (
match backend () with
| FStar ->
@@ -1966,7 +1991,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt "Type0"
| HOL4 ->
F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
- | Coq | Lean -> print_axiom ()));
+ | Coq | Lean | IsabelleHOL -> print_axiom ()));
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
diff --git a/compiler/Main.ml b/compiler/Main.ml
index d78b9081..ff6a4d67 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -253,6 +253,12 @@ let () =
(* We don't support fuel for the HOL4 backend *)
if !use_fuel then (
log#error "The HOL4 backend doesn't support the -use-fuel option";
+ fail ())
+ | IsabelleHOL ->
+ record_fields_short_names := true;
+ (* We don't support fuel for the IsabelleHOL backend *)
+ if !use_fuel then (
+ log#error "The IsabelleHOL backend doesn't support the -use-fuel option";
fail ()))
in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 9673f542..a2ba5dbc 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -243,7 +243,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
let texpression_requires_parentheses span e =
match Config.backend () with
| FStar | Lean -> false
- | Coq | HOL4 -> let_group_requires_parentheses span e
+ | Coq | HOL4 | IsabelleHOL -> let_group_requires_parentheses span e
let is_var (e : texpression) : bool =
match e.e with Var _ -> true | _ -> false
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e829ed30..3f858124 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3754,7 +3754,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
let match_ty = body.ty in
let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in
{ e = match_e; ty = match_ty }
- | Lean | HOL4 ->
+ | Lean | HOL4 | IsabelleHOL ->
(* We should have checked the command line arguments before *)
raise (Failure "Unexpected")
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 672fb22f..afd3420e 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -692,6 +692,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
| HOL4 ->
raise
(Failure "HOL4 doesn't have decreases/termination clauses")
+ | IsabelleHOL ->
+ raise
+ (Failure "HOL4 doesn't have decreases/termination clauses")
in
extract_decrease f.f;
List.iter extract_decrease f.loops)
@@ -886,7 +889,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
| Lean ->
Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
- | Coq | FStar | HOL4 ->
+ | Coq | FStar | HOL4 | IsabelleHOL ->
Printf.fprintf out
"(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
@@ -968,7 +971,23 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
Printf.fprintf out "open %s\n\n" imports
else Printf.fprintf out "\n";
(* Initialize the theory *)
- Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name);
+ Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name
+ | IsabelleHOL ->
+ Printf.fprintf out "theory \"%s\" imports\n" fi.module_name;
+ (* Add the custom imports and includes *)
+ let imports =
+ "Aeneas.Primitives"
+ :: "HOL-Library.Datatype_Records"
+ :: fi.custom_imports @ fi.custom_includes in
+ (* The imports are a list of module names: we need to add a "Theory" suffix *)
+ let imports = List.map (fun s -> "\"" ^ s ^ "\"") imports in
+ if imports <> [] then
+ let imports = String.concat "\n " imports in
+ Printf.fprintf out " %s\n" imports
+ else Printf.fprintf out "\n";
+ Printf.fprintf out "begin\n\n"
+ (* Initialize the theory *)
+ );
(* From now onwards, we use the formatter *)
(* Set the margin *)
Format.pp_set_margin fmt 80;
@@ -988,7 +1007,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
| FStar -> ()
| Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
| HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
- | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
+ | Coq -> Printf.fprintf out "End %s.\n" fi.module_name
+ | IsabelleHOL -> Printf.fprintf out "end");
(* Some logging *)
if !Errors.error_list <> [] then
@@ -1148,7 +1168,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* We use the raw crate name for the namespaces *)
let namespace =
match Config.backend () with
- | FStar | Coq | HOL4 -> crate.name
+ | FStar | Coq | HOL4 | IsabelleHOL -> crate.name
| Lean -> crate.name
in
(* Concatenate *)
@@ -1189,6 +1209,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
| Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
| Lean -> None
| HOL4 -> None
+ | IsabelleHOL -> None
in
match primitives_src_dest with
| None -> ()
@@ -1223,6 +1244,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
| Coq -> "_"
| Lean -> "."
| HOL4 -> "_"
+ | IsabelleHOL -> "."
in
let file_delimiter =
if Config.backend () = Lean then "/" else module_delimiter
@@ -1234,6 +1256,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
| Coq -> ".v"
| Lean -> ".lean"
| HOL4 -> "Script.sml"
+ | IsabelleHOL -> ".thy"
in
(* File extension for the opaque module *)
let opaque_ext =
@@ -1242,6 +1265,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
| Coq -> ".v"
| Lean -> ".lean"
| HOL4 -> "Script.sml"
+ | IsabelleHOL -> ".thy"
in
(* Extract one or several files, depending on the configuration *)
@@ -1284,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
match Config.backend () with
| FStar ->
("TypesExternal", "TypesExternal", ": external type declarations")
- | HOL4 | Coq | Lean ->
+ | HOL4 | Coq | Lean | IsabelleHOL ->
( (* The name of the file we generate *)
"TypesExternal_Template",
(* The name of the file that will be imported by the Types
@@ -1339,6 +1363,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
| Coq -> ".v"
| Lean -> ".lean"
| HOL4 -> "Script.sml"
+ | IsabelleHOL -> ".thy"
in
let types_filename =
extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
@@ -1410,7 +1435,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
( "FunsExternal",
"FunsExternal",
": external function declarations" )
- | HOL4 | Coq | Lean ->
+ | HOL4 | Coq | Lean | IsabelleHOL ->
( (* The name of the file we generate *)
"FunsExternal_Template",
(* The name of the file that will be imported by the Funs
@@ -1530,7 +1555,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Generate the build file *)
match Config.backend () with
- | Coq | FStar | HOL4 ->
+ | Coq | FStar | HOL4 | IsabelleHOL ->
()
(* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.
But then we can't modify it if we want to add more files for the proofs
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 05:03:22 +0000