Source file error.ml

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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
(*                  Copyright 2008-2021 INRIA                             *)
(*                                                                        *)
(*  More information on "http://acg.gforge.inria.fr/"                     *)
(*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *)
(*  Authors: see the AUTHORS file                                         *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*  $Rev::                              $:  Revision of last commit       *)
(*  $Author::                           $:  Author of last commit         *)
(*  $Date::                             $:  Date of last commit           *)
(*                                                                        *)
(**************************************************************************)

open UtilsLib

let update_loc lexbuf file =
  let pos = lexbuf.Lexing.lex_curr_p in
  let new_file = match file with
    | None -> pos.Lexing.pos_fname
    | Some s -> s
  in
    lexbuf.Lexing.lex_curr_p <- { pos with
			     Lexing.pos_fname = new_file;
			     Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
			     Lexing.pos_bol = pos.Lexing.pos_cnum;
			 }


let infix_as_prefix = ref None
  
  
let set_infix l = infix_as_prefix := Some l
  
let unset_infix () = infix_as_prefix := None
  
(*let bad_infix_usage () =  !infix_as_prefix  *)


type lex_error =
  | Unstarted_comment
  | Unstarted_bracket
  | Mismatch_parentheses of char
  | Unclosed_comment
  | Expect of string
  | Bad_token

type parse_error =
  | Syntax_error of string
  | Duplicated_term of string
  | Duplicated_type of string
  | Binder_expected of string
  | Unknown_constant of string
  | Not_def_as_infix of string
  | Unknown_constant_nor_variable of string
  | Unknown_constant_nor_type of string
  | Unknown_type of string
  | Missing_arg_of_Infix of string
  | No_such_signature of string
  | No_such_lexicon of string
  | Not_associative of string
  | Not_infix of string
  | Prefix_missing_arg of string
  | Infix_missing_first_arg of string
  | Infix_missing_second_arg of string

type type_error =
  | Already_defined_var of string
  | Not_defined_var of string
  | Not_defined_const of string
  | Not_well_typed_term of string * string
  | Not_well_typed_term_plus of string * string * string
  | Not_well_kinded_type of string
  | Non_linear_var of string
  | Linear_var of string
  | Other
  | Is_Used of string * string
  | Two_occurrences_of_linear_variable of (Lexing.position * Lexing.position)
  | Non_empty_context of (string*(Lexing.position * Lexing.position)*(Lexing.position * Lexing.position)*string)
  | Not_normal
  | Vacuous_abstraction of (string * (Lexing.position * Lexing.position))


type env_error =
  | Duplicated_signature of string
  | Duplicated_lexicon of string
  | Duplicated_entry of string

type version_error =  Outdated_version of (string*string)
    


type lexicon_error =
  | Missing_interpretations of (string * string * (string list))


type error = 
  | Parse_error of parse_error * (Lexing.position * Lexing.position)
  | Lexer_error of lex_error * (Lexing.position * Lexing.position)
  | Type_error of type_error * (Lexing.position * Lexing.position)
  | Env_error of env_error * (Lexing.position * Lexing.position)
  | Version_error of version_error
  | Lexicon_error of lexicon_error * (Lexing.position * Lexing.position)
  | System_error of string



type warning =
  | Variable_or_constant of (string * (Lexing.position * Lexing.position))

exception Error of error


let compute_comment_for_position pos1 pos2 =
  let line2 = pos2.Lexing.pos_lnum in
  let col2 = pos2.Lexing.pos_cnum - pos2.Lexing.pos_bol in
  let pos1 = pos1 in
  let line1 = pos1.Lexing.pos_lnum in
  let col1 = pos1.Lexing.pos_cnum - pos1.Lexing.pos_bol in
    if line1=line2 then
      Printf.sprintf "line %d, characters %d-%d" line2 col1 col2
    else
      Printf.sprintf "line %d, character %d to line %d, character %d" line1 col1 line2 col2


let lex_error_to_string = function
  | Unstarted_comment -> "Syntax error: No comment opened before this closing of comment"
  | Unstarted_bracket -> "Syntax error: No bracket opened before this right bracket"
  | Unclosed_comment -> "Syntax error: Unclosed comment"
  | Mismatch_parentheses c -> Printf.sprintf "Syntax error: Unclosed parenthesis '%c'" c
  | Expect s -> Printf.sprintf "Syntax error: %s expected" s
  | Bad_token -> "Lexing error: no such token allowed"

let parse_error_to_string = function
  | Syntax_error s -> Printf.sprintf "Syntax error: %s" s
  | Duplicated_type ty ->  Printf.sprintf "Syntax error: Type \"%s\" has already been defined" ty
  | Duplicated_term te ->  Printf.sprintf "Syntax error: Term \"%s\" has already been defined" te
  | Binder_expected id -> Printf.sprintf "Syntax error: Unknown binder \"%s\"" id
  | Unknown_constant id -> Printf.sprintf "Syntax error: Unknown constant \"%s\"" id
  | Not_def_as_infix id -> Printf.sprintf "Syntax error: \"%s\" is not an infix operator" id
  | Unknown_constant_nor_variable id -> Printf.sprintf "Syntax error: Unknown constant or variable \"%s\"" id
  | Unknown_constant_nor_type id -> Printf.sprintf "Syntax error: Unknown constant or type \"%s\"" id
  | Unknown_type id -> Printf.sprintf "Syntax error: Unknown atomic type \"%s\"" id
  | Missing_arg_of_Infix  id -> Printf.sprintf "Syntax error: \"%s\" is defined as infix but used here with less than two arguments" id
  | No_such_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" not in the current environment" s
  | No_such_lexicon s -> Printf.sprintf "Syntax error: Lexicon id \"%s\" not in the current environment" s
  | Not_associative s -> Printf.sprintf "Syntax error: Operator \"%s\" is not associative but is used without parenthesis" s
  | Not_infix s -> Printf.sprintf "Syntax error: Operator \"%s\" is not infix but is used as infix" s
  | Prefix_missing_arg s -> Printf.sprintf "Syntax error: The prefix operator \"%s\" is missing its argument" s
  | Infix_missing_first_arg s  -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s
  | Infix_missing_second_arg s  -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s

let type_error_to_string = function
  | Already_defined_var s ->
      Printf.sprintf "Var \"%s\" is already defined" s
  | Not_defined_var s -> 
      Printf.sprintf "Var \"%s\" is not defined" s
  | Not_defined_const s -> 
      Printf.sprintf "Const \"%s\" is not defined" s
  | Not_well_typed_term (s,typ) ->
      Printf.sprintf "Term \"%s\" not well typed.\nType expected : %s\n" s typ
  | Not_well_typed_term_plus (s,typ,wrong_typ) ->
      Printf.sprintf "Term \"%s\" not well typed.\n \"%s\" is of type %s but is here used with type  %s\n" s s typ wrong_typ
  | Not_well_kinded_type s ->
      Printf.sprintf "Type \"%s\" not well kinded" s
  | Non_linear_var s ->
      Printf.sprintf "Var \"%s\" is supposed to be non linear" s
  | Linear_var s ->
      Printf.sprintf "Var \"%s\" is supposed to be linear" s
  | Other -> "Not yet implemented"
  | Is_Used (s1,s2) -> Printf.sprintf "The type of this expression is \"%s\" but is used with type %s" s1 s2
  | Two_occurrences_of_linear_variable (s,e) -> Printf.sprintf "This linear variable was already used: %s" (compute_comment_for_position s e)
  | Non_empty_context (x,(s,e),funct_pos,funct_type) -> Printf.sprintf "This term contains a free linear variable \"%s\" at %s and is argument the term  of type \"%s\" at %s )" x (compute_comment_for_position s e)   funct_type (compute_comment_for_position (fst funct_pos) (snd funct_pos))
  | Not_normal -> "This term is not in normal form"
  | Vacuous_abstraction (x,(s,e)) -> Printf.sprintf "This linear variable \"%s\" is abstracted over but not used in term %s" x (compute_comment_for_position s e)

let env_error_to_string = function
  | Duplicated_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" is used twice in this environment" s
  | Duplicated_lexicon s -> Printf.sprintf "Syntax error: Lexicon id \"%s\" is used twice in this environment" s
  | Duplicated_entry s -> Printf.sprintf "Syntax error: Entry id \"%s\" is used twice in this environment" s

let lexicon_error_to_string = function
  | Missing_interpretations (lex_name,abs_name,missing_inters) ->
      Printf.sprintf "Lexicon definition error: Lexicon \"%s\" is missing the interpretations of the following terms of the abstract signature \"%s\":\n%s" lex_name abs_name (Utils.string_of_list "\n" (fun x -> Printf.sprintf"\t%s" x) missing_inters)

let version_error_to_string = function
  | Outdated_version (old_v,current_v) -> Printf.sprintf "You are trying to use an object file that was generated with a former version of the acgc compiler (version %s) while the current version of the compiler is %s" old_v current_v

let warning_to_string w input_file = 
  match w with
  | Variable_or_constant (s,(start,e)) ->
     Printf.sprintf "File \"%s\", %s\nWarning: %s"
                    input_file
                    (compute_comment_for_position start e)
                    (Printf.sprintf "\"%s\" is a variable here, but is also declared as constant in the signature" s)
	      
let error_msg e input_file =
  let msg,location_msg =
    match e with
      | Parse_error (er,(s,e)) -> parse_error_to_string er,Some (compute_comment_for_position s e)
      | Lexer_error (er,(s,e))  -> lex_error_to_string er,Some (compute_comment_for_position s e)
      | Type_error (er,(s,e)) -> type_error_to_string er,Some (compute_comment_for_position s e)
      | Env_error (er,(s,e)) -> env_error_to_string er,Some (compute_comment_for_position s e)
      | Version_error er ->  version_error_to_string er,None
      | Lexicon_error (er,(s,e)) -> lexicon_error_to_string er,Some (compute_comment_for_position s e)
      | System_error s -> Printf.sprintf "System error: \"%s\"" s,None in
    match location_msg with
      | None -> msg
      | Some loc -> Printf.sprintf "File \"%s\", %s\n%s" input_file loc msg

                                   (*
let dyp_error lexbuf =
  let pos1=Lexing.lexeme_start_p lexbuf in
  let pos2=Lexing.lexeme_end_p lexbuf in
    match bad_infix_usage () with
      | None -> Error (Parse_error (Dyp_error,(pos1,pos2)))
      | Some (sym,(s,e)) -> Error (Parse_error (Missing_arg_of_Infix sym,(s,e)))
                                    *)
(*
let emit_warning w input_file = 
  match w with
    | Variable_or_constant (_,(pos1,pos2)) -> 
	let msg = warning_to_string w input_file in
	let line2 = pos2.Lexing.pos_lnum in
	let col2 = pos2.Lexing.pos_cnum - pos2.Lexing.pos_bol in
	let pos1 = pos1 in
	let line1 = pos1.Lexing.pos_lnum in
	let col1 = pos1.Lexing.pos_cnum - pos1.Lexing.pos_bol in
	  if line1=line2 then
	    Printf.sprintf "File \"%s\", line %d, characters %d-%d\nWarning: %s"
	      input_file line2 col1 col2 msg
	  else
	    Printf.sprintf "File \"%s\", from l:%d, c:%d to l:%d,c:%d\nWarning: %s"
	      input_file line1 col1 line2 col2 msg
 *)	      

let warnings_to_string input_file ws = Utils.string_of_list "\n" (fun w -> warning_to_string w input_file) ws
  
let get_loc_error = function
  | Parse_error (_,(s,e))
  | Lexer_error (_,(s,e))
  | Type_error (_,(s,e))
  | Env_error (_,(s,e))
  | Lexicon_error (_,(s,e)) -> (s,e)
  | (Version_error _ | System_error _) -> failwith "Bug: should not occur"

                                        
let get_string_error = function
      | Parse_error (er,pos) -> parse_error_to_string er,pos
      | Lexer_error (er,pos)  -> lex_error_to_string er,pos
      | Type_error (er,pos) -> type_error_to_string er,pos
      | Env_error (er,pos) -> env_error_to_string er,pos
      | Lexicon_error (er,pos) -> lexicon_error_to_string er,pos
      | (Version_error _ | System_error _) -> failwith "Bug: should not occur"

let change_loc err pos =
  match err with
  | Parse_error (er,_) -> Parse_error (er,pos)
  | Lexer_error (er,_) -> Lexer_error (er,pos)
  | Type_error (er,_) -> Type_error (er,pos)
  | Env_error (er,_) -> Env_error (er,pos)
  | Lexicon_error (er,_) -> Lexicon_error (er,pos)
  | (Version_error _ | System_error _) -> failwith "Bug: should not occur"