typage des declarations de types

parent b615b5df
...@@ -88,7 +88,7 @@ check: $(BINARY) $(PRELUDE) ...@@ -88,7 +88,7 @@ check: $(BINARY) $(PRELUDE)
# why # why
##### #####
LIBCMO = lib/pp.cmo lib/loc.cmo LIBCMO = lib/pp.cmo lib/loc.cmo lib/util.cmo
CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo \ CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo \
src/parser.cmo src/lexer.cmo src/typing.cmo src/main.cmo src/parser.cmo src/lexer.cmo src/typing.cmo src/main.cmo
......
let map_fold_left f acc l =
let acc, rev =
List.fold_left
(fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
(acc, []) l
in
acc, List.rev rev
val map_fold_left :
('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
type error type error
exception Lexical_error of error exception Error of error
val report : Format.formatter -> error -> unit val report : Format.formatter -> error -> unit
......
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
| UnterminatedComment | UnterminatedComment
| UnterminatedString | UnterminatedString
exception Lexical_error of error exception Error of error
let report fmt = function let report fmt = function
| IllegalCharacter c -> fprintf fmt "illegal character %c" c | IllegalCharacter c -> fprintf fmt "illegal character %c" c
...@@ -213,7 +213,7 @@ rule token = parse ...@@ -213,7 +213,7 @@ rule token = parse
| eof | eof
{ EOF } { EOF }
| _ as c | _ as c
{ raise (Lexical_error (IllegalCharacter c)) } { raise (Error (IllegalCharacter c)) }
and comment = parse and comment = parse
| "*)" | "*)"
...@@ -223,7 +223,7 @@ and comment = parse ...@@ -223,7 +223,7 @@ and comment = parse
| newline | newline
{ newline lexbuf; comment lexbuf } { newline lexbuf; comment lexbuf }
| eof | eof
{ raise (Lexical_error UnterminatedComment) } { raise (Error UnterminatedComment) }
| _ | _
{ comment lexbuf } { comment lexbuf }
...@@ -235,7 +235,7 @@ and string = parse ...@@ -235,7 +235,7 @@ and string = parse
| newline | newline
{ newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf } { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
| eof | eof
{ raise (Lexical_error UnterminatedString) } { raise (Error UnterminatedString) }
| _ as c | _ as c
{ Buffer.add_char string_buf c; string lexbuf } { Buffer.add_char string_buf c; string lexbuf }
......
...@@ -19,12 +19,14 @@ open Format ...@@ -19,12 +19,14 @@ open Format
let file = Sys.argv.(1) let file = Sys.argv.(1)
let rec report fmt = function let rec report fmt = function
| Lexer.Lexical_error e -> | Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e; fprintf fmt "lexical error: %a" Lexer.report e;
| Loc.Located (loc, e) -> | Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error -> | Parsing.Parse_error ->
fprintf fmt "syntax error" fprintf fmt "syntax error"
| Typing.Error e ->
Typing.report fmt e
| e -> | e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e) fprintf fmt "anomaly: %s" (Printexc.to_string e)
...@@ -33,8 +35,9 @@ let () = ...@@ -33,8 +35,9 @@ let () =
let c = open_in file in let c = open_in file in
let lb = Lexing.from_channel c in let lb = Lexing.from_channel c in
Loc.set_file file lb; Loc.set_file file lb;
let _f = Lexer.parse_logic_file lb in let f = Lexer.parse_logic_file lb in
close_in c close_in c;
ignore (List.fold_left Typing.add Typing.empty f)
with e -> with e ->
eprintf "%a@." report e; eprintf "%a@." report e;
exit 1 exit 1
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
type 'a list type 'a list
logic nil : 'a list (* logic nil : 'a list *)
logic cons : 'a, 'a list -> 'a list (* logic cons : 'a, 'a list -> 'a list *)
open Util
open Format
open Term open Term
(** errors *)
type error =
| ClashType of string
| BadTypeArity of string
exception Error of error
let error ?loc e = match loc with
| None -> raise (Error e)
| Some loc -> raise (Loc.Located (loc, Error e))
let report fmt = function
| ClashType s ->
fprintf fmt "clash with previous type %s" s
| BadTypeArity s ->
fprintf fmt "duplicate type parameter %s" s
module M = Map.Make(String) module M = Map.Make(String)
type env = { type env = {
...@@ -19,3 +39,34 @@ let empty = { ...@@ -19,3 +39,34 @@ let empty = {
vars = M.empty; vars = M.empty;
} }
let find_tysymbol s env = M.find s env.tysymbols
let find_fsymbol s env = M.find s env.fsymbols
let find_psymbol s env = M.find s env.psymbols
let find_tyvar s env = M.find s env.tyvars
let find_var s env = M.find s env.vars
(** typing *)
let term env t =
assert false (*TODO*)
(** building environments *)
open Ptree
let add_type loc ext sl s env =
if M.mem s env.tysymbols then error ~loc (ClashType s);
let add_ty_var env x =
if M.mem x env.tyvars then error ~loc (BadTypeArity x);
let v = Name.from_string x in
{ env with tyvars = M.add x v env.tyvars}, v
in
let _, vl = map_fold_left add_ty_var env sl in
let ty = Ty.create_tysymbol (Name.from_string s) vl None in
{ env with tysymbols = M.add s ty env.tysymbols }
let add env = function
| TypeDecl (loc, ext, sl, s) ->
add_type loc ext sl s env
| _ ->
assert false (*TODO*)
...@@ -7,3 +7,24 @@ type env ...@@ -7,3 +7,24 @@ type env
val empty : env val empty : env
val find_tysymbol : string -> env -> tysymbol
val find_fsymbol : string -> env -> fsymbol
val find_psymbol : string -> env -> psymbol
val find_tyvar : string -> env -> vsymbol
val find_var : string -> env -> vsymbol
(** typing *)
val term : env -> Ptree.lexpr -> term
(** building environments *)
val add : env -> Ptree.logic_decl ->env
(** error reporting *)
type error
exception Error of error
val report : Format.formatter -> error -> unit
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