1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* Copyright (C) 2002-2008 *)
(* Romain BARDOU *)
(* Jean-Franois COUCHOT *)
(* Mehdi DOGGUY *)
(* Jean-Christophe FILLITRE *)
(* Thierry HUBERT *)
(* Claude MARCH *)
(* Yannick MOY *)
(* Christine PAULIN *)
(* Yann RGIS-GIANAS *)
(* Nicolas ROUSSET *)
(* Xavier URBAIN *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU General Public *)
(* License version 2, as published by the Free Software Foundation. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(* See the GNU General Public License version 2 for more details *)
(* (enclosed in the file GPL). *)
(* *)
(**************************************************************************)
(* One module to rule them all, one module to find them, one module to bring
them all and in the bytecode bind them. *)
open Ml_misc
open Unix
let parse f file_name =
(* Open file *)
let fd = try
openfile file_name [ O_RDONLY ] 0o640
with
| Unix_error _ -> error "Could not read file: %s" file_name
in
let chan = in_channel_of_descr fd in
(* Parse file *)
let lexbuf = Lexing.from_channel chan in
Ml_ocaml.Location.init lexbuf file_name;
try
f Ml_ocaml.Lexer.token lexbuf
with
| Ml_ocaml.Lexer.Error(error, loc) ->
caml_error loc Ml_ocaml.Lexer.report_error error
| Parsing.Parse_error ->
locate_error (Ml_ocaml.Location.curr lexbuf) "Parse error"
let file (mlenv, env) (file_kind, file_name) =
match file_kind with
| Ml_options.Ml ->
log "Implementation %s:" file_name;
let parse_tree = parse Ml_ocaml.Parser.implementation file_name in
(* Type with the OCaml typer *)
log " Typing...";
let typed_tree, _, new_env = try
Ml_ocaml.Typemod.type_structure env parse_tree
with
| Ml_ocaml.Typecore.Error(loc, error) ->
caml_error loc Ml_ocaml.Typecore.report_error error
| Ml_ocaml.Typetexp.Error(loc, error) ->
caml_error loc Ml_ocaml.Typetexp.report_error error
| Ml_ocaml.Typemod.Error(loc, error) ->
caml_error loc Ml_ocaml.Typemod.report_error error
in
(* Add specifications to the environment *)
log " Listing function specifications...";
let mlenv =
Ml_interp.add_structure_specs mlenv typed_tree
in
(*log " Listing type specifications...";
let spec_env =
Ml_interp.add_type_specs spec_env typed_tree
in*)
(* Interpret to a Jessie typed AST *)
log " Interpreting...";
let code_decls, mlenv = Ml_interp.structure mlenv typed_tree in
let type_decls = Ml_type.jc_decls () in
let jessie_ast = Ml_interp.base_decls @ type_decls @ code_decls in
(* Open the output file *)
log " Output file: %s" Ml_options.output_file;
let fd = try
openfile Ml_options.output_file [ O_WRONLY; O_CREAT; O_TRUNC ] 0o640
with
| Unix_error _ -> error "Could not open or create file: %s" file_name
in
let chan = out_channel_of_descr fd in
(* Output our translation *)
Jc_output.print_decls (Format.formatter_of_out_channel chan) jessie_ast;
(* Return the new environment *)
log " Done.";
mlenv, new_env
| Ml_options.Mli ->
log "Interface %s:" file_name;
let parse_tree = parse Ml_ocaml.Parser.interface file_name in
(* Type with the OCaml typer *)
let typed_tree = try
Ml_ocaml.Typemod.transl_signature env parse_tree
with
| Ml_ocaml.Typecore.Error(loc, error) ->
caml_error loc Ml_ocaml.Typecore.report_error error
| Ml_ocaml.Typetexp.Error(loc, error) ->
caml_error loc Ml_ocaml.Typetexp.report_error error
| Ml_ocaml.Typemod.Error(loc, error) ->
caml_error loc Ml_ocaml.Typemod.report_error error
in
(* Return the new environment *)
mlenv, Ml_ocaml.Env.add_signature typed_tree env
let _ =
List.fold_left
file
(Ml_pervasives.default_mlenv, Ml_pervasives.default_env)
Ml_options.input_files
(*
Local Variables:
compile-command: "unset LANG; make -j -C .. bin/jessica.byte"
End:
*)
|
