From f9f70e9fe519e1c3d1523aa573cb97ff8d1e05d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Christophe=20Filli=C3=A2tre?= <filliatr@lri.fr>
Date: Wed, 10 Feb 2010 08:19:34 +0000
Subject: [PATCH] typage des declarations de types
---
Makefile.in | 2 +-
lib/util.ml | 10 ++++++++++
lib/util.mli | 3 +++
src/lexer.mli | 2 +-
src/lexer.mll | 8 ++++----
src/main.ml | 9 ++++++---
src/test.why | 5 +++--
src/typing.ml | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++
src/typing.mli | 21 +++++++++++++++++++++
9 files changed, 100 insertions(+), 11 deletions(-)
create mode 100644 lib/util.ml
create mode 100644 lib/util.mli
diff --git a/Makefile.in b/Makefile.in
index a22fa032cc..1005f6e441 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -88,7 +88,7 @@ check: $(BINARY) $(PRELUDE)
# 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 \
src/parser.cmo src/lexer.cmo src/typing.cmo src/main.cmo
diff --git a/lib/util.ml b/lib/util.ml
new file mode 100644
index 0000000000..c14168ff7f
--- /dev/null
+++ b/lib/util.ml
@@ -0,0 +1,10 @@
+
+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
+
+
diff --git a/lib/util.mli b/lib/util.mli
new file mode 100644
index 0000000000..e59eba0fa3
--- /dev/null
+++ b/lib/util.mli
@@ -0,0 +1,3 @@
+
+val map_fold_left :
+ ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
diff --git a/src/lexer.mli b/src/lexer.mli
index ff8e5f9f89..c474fea3f0 100644
--- a/src/lexer.mli
+++ b/src/lexer.mli
@@ -1,7 +1,7 @@
type error
-exception Lexical_error of error
+exception Error of error
val report : Format.formatter -> error -> unit
diff --git a/src/lexer.mll b/src/lexer.mll
index 65d6615100..461fffbe44 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -12,7 +12,7 @@
| UnterminatedComment
| UnterminatedString
- exception Lexical_error of error
+ exception Error of error
let report fmt = function
| IllegalCharacter c -> fprintf fmt "illegal character %c" c
@@ -213,7 +213,7 @@ rule token = parse
| eof
{ EOF }
| _ as c
- { raise (Lexical_error (IllegalCharacter c)) }
+ { raise (Error (IllegalCharacter c)) }
and comment = parse
| "*)"
@@ -223,7 +223,7 @@ and comment = parse
| newline
{ newline lexbuf; comment lexbuf }
| eof
- { raise (Lexical_error UnterminatedComment) }
+ { raise (Error UnterminatedComment) }
| _
{ comment lexbuf }
@@ -235,7 +235,7 @@ and string = parse
| newline
{ newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
| eof
- { raise (Lexical_error UnterminatedString) }
+ { raise (Error UnterminatedString) }
| _ as c
{ Buffer.add_char string_buf c; string lexbuf }
diff --git a/src/main.ml b/src/main.ml
index ba184518c3..26fe947cf9 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -19,12 +19,14 @@ open Format
let file = Sys.argv.(1)
let rec report fmt = function
- | Lexer.Lexical_error e ->
+ | Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error ->
fprintf fmt "syntax error"
+ | Typing.Error e ->
+ Typing.report fmt e
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
@@ -33,8 +35,9 @@ let () =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
- let _f = Lexer.parse_logic_file lb in
- close_in c
+ let f = Lexer.parse_logic_file lb in
+ close_in c;
+ ignore (List.fold_left Typing.add Typing.empty f)
with e ->
eprintf "%a@." report e;
exit 1
diff --git a/src/test.why b/src/test.why
index d3e64fa673..1a813a92af 100644
--- a/src/test.why
+++ b/src/test.why
@@ -3,6 +3,7 @@
type 'a list
-logic nil : 'a list
-logic cons : 'a, 'a list -> 'a list
+(* logic nil : 'a list *)
+(* logic cons : 'a, 'a list -> 'a list *)
+
diff --git a/src/typing.ml b/src/typing.ml
index ea20d19ada..b09b34ea7b 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -1,6 +1,26 @@
+open Util
+open Format
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)
type env = {
@@ -19,3 +39,34 @@ let 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*)
diff --git a/src/typing.mli b/src/typing.mli
index b803962cbf..78b719a96f 100644
--- a/src/typing.mli
+++ b/src/typing.mli
@@ -7,3 +7,24 @@ type 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
--
GitLab