Commit 1c4660cf authored by Mário Pereira's avatar Mário Pereira

Extraction: CakeML printer (wip)

parent 6e26dea7
......@@ -208,7 +208,8 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
parse_smtv2_model
LIB_MLW = ity expr pdecl eval_match typeinv vc pmodule dexpr \
pinterp mltree compile mlinterp pdriver cprinter ocaml_printer
pinterp mltree compile mlinterp pdriver cprinter ocaml_printer \
sml_printer
LIB_PARSER = ptree glob typing parser lexer
......
......@@ -167,8 +167,6 @@ end
module array.Array
syntax type array "%1 array"
syntax function ([]) "%1.(Z.to_int %2)"
(* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)
syntax val ([]) "%1.(Z.to_int %2)"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
module Print = struct
let print_decl info fmt d = assert false (* TODO *)
end
let print_decl =
let memo = Hashtbl.create 16 in
fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d ->
ignore (old);
let info = {
info_syn = pargs.Pdriver.syntax;
info_convert = pargs.Pdriver.converter;
info_literal = pargs.Pdriver.literal;
info_current_th = th;
info_current_mo = Some m;
info_th_known_map = th.th_known;
info_mo_known_map = m.mod_known;
info_fname = Opt.map Compile.clean_name fname;
info_flat = flat;
info_current_ph = [];
} in
if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
Print.print_decl info fmt d end
let fg ?fname m =
let mod_name = m.mod_theory.th_name.id_string in
let path = m.mod_theory.th_path in
(module_name ?fname path mod_name) ^ ".cml"
let () = Pdriver.register_printer "cakeml"
~desc:"printer for CakeML code" fg print_decl
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment