program typing now uses modules

Makefile.in

@@ -282,7 +282,7 @@ PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
 	       src/programs/pgm_lexer.ml
 
 PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
-	    pgm_types pgm_module # pgm_env pgm_typing pgm_wp pgm_main
+	    pgm_types pgm_module pgm_typing # pgm_env pgm_wp pgm_main
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 

src/parser/typing.mli

@@ -71,6 +71,7 @@ val dfmla : ?localize:bool -> denv -> Ptree.lexpr -> Denv.dfmla
 val dpat : denv -> Ptree.pattern -> denv * Denv.dpattern
 val dpat_list : denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
 
+val string_list_of_qualid : string list -> Ptree.qualid -> string list
 val qloc : Ptree.qualid -> Loc.position
 
 val ts_tuple : int -> Ty.tysymbol

src/programs/pgm_env.ml

@@ -130,25 +130,6 @@ let empty_env uc = {
   ls_add   = find_ls uc ["infix +"];
 }
 
-(* parsing LOGIC strings using functions from src/parser/
-   requires proper relocation *)
-
-let reloc loc lb =
-  lb.Lexing.lex_curr_p <- loc;
-  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum + 1
-
-let parse_string f loc s =
-  let lb = Lexing.from_string s in
-  reloc loc lb;
-  f lb
-
-let logic_lexpr ((pos, _), s) =
-  parse_string Lexer.parse_lexpr pos s
-
-let logic_decls ((loc, _), s) e env =
-  let parse = Lexer.parse_list0_decl e Mnm.empty env.uc in
-  { env with uc = parse_string parse loc s }
-
 (* addition *)
 
 let add_global id tyv env =

src/programs/pgm_module.ml

@@ -74,6 +74,9 @@ type uc = {
   uc_export : namespace list;
 }
 
+let namespace uc = List.hd uc.uc_import
+let theory_uc uc = uc.uc_th
+
 let create_module n =
   let uc = Theory.create_theory n in
   (* let th = Env.find_theory env ["programs"] "Prelude" in *)
@@ -104,6 +107,30 @@ let close_namespace uc import s =
   | [_], [_] -> raise NoOpenedNamespace
   | _ -> assert false
 
+(** Insertion of new declarations *)
+
+let add_symbol add id v uc =
+  match uc.uc_import, uc.uc_export with
+  | i0 :: sti, e0 :: ste -> { uc with
+      uc_import = add false id.id_string v i0 :: sti;
+      uc_export = add true  id.id_string v e0 :: ste }
+  | _ -> assert false
+
+let add_psymbol ps uc =
+  add_symbol add_pr ps.p_ls.ls_name ps uc
+
+let add_esymbol ls uc =
+  add_symbol add_ex ls.ls_name ls uc
+
+let add_decl d uc =
+  { uc with uc_decls = d :: uc.uc_decls }
+
+let add_logic_decl d uc =
+  let th = Typing.with_tuples Theory.add_decl uc.uc_th d in
+  { uc with uc_th = th }
+
+(** Modules *)
+
 type t = {
   m_name   : Ident.ident;
   m_th     : theory;
@@ -122,6 +149,25 @@ let close_module uc = match uc.uc_export with
   | _ ->
       raise CloseModule
 
+(* parsing LOGIC strings using functions from src/parser/
+   requires proper relocation *)
+
+let reloc loc lb =
+  lb.Lexing.lex_curr_p <- loc;
+  lb.Lexing.lex_abs_pos <- loc.Lexing.pos_cnum + 1
+
+let parse_string f loc s =
+  let lb = Lexing.from_string s in
+  reloc loc lb;
+  f lb
+
+let logic_lexpr ((pos, _), s) =
+  parse_string Lexer.parse_lexpr pos s
+
+let parse_logic_decls env ((loc, _), s) uc =
+  let parse = Lexer.parse_list0_decl env Theory.Mnm.empty uc.uc_th in
+  { uc with uc_th = parse_string parse loc s }
+
 
 
 

src/programs/pgm_module.mli

@@ -19,6 +19,9 @@ val ns_find_ns : namespace -> string list -> namespace
 (** a module under construction *)
 type uc
 
+val namespace : uc -> namespace
+val theory_uc : uc -> Theory.theory_uc
+
 (** a module *)
 type t
 
@@ -28,6 +31,19 @@ val close_module : uc -> t
 val open_namespace  : uc -> uc
 val close_namespace : uc -> bool -> string option -> uc
 
-(* exceptions *)
+(** insertion *)
+
+exception ClashSymbol of string
+
+val add_psymbol : psymbol -> uc -> uc
+val add_esymbol : esymbol -> uc -> uc
+val add_decl : Pgm_ttree.decl -> uc -> uc
+val add_logic_decl : Decl.decl -> uc -> uc
+
+(** TODO: *)
+val parse_logic_decls : Env.env -> Loc.position * string -> uc -> uc
+val logic_lexpr : Loc.position * string -> Ptree.lexpr
+
+(** exceptions *)
 
 exception CloseModule

src/programs/pgm_ttree.ml

@@ -200,9 +200,9 @@ and recfun = Term.vsymbol * binder list * rec_variant option * triple
 and triple = pre * expr * post
 
 type decl =
-  | Dlet    of Term.lsymbol * expr
-  | Dletrec of (Term.lsymbol * recfun) list
-  | Dparam  of Term.lsymbol * type_v
+  | Dlet    of Pgm_types.psymbol * expr
+  | Dletrec of (Pgm_types.psymbol * recfun) list
+  | Dparam  of Pgm_types.psymbol * type_v
 
 type file = decl list
 

src/programs/pgm_types.ml

@@ -61,8 +61,10 @@ type psymbol = {
   p_tv : type_v;
 }
 
-(* TODO: ensure ls = purify v *)
-let create_psymbol ls v = { p_ls = ls; p_tv = v }
+let create_psymbol id v = 
+  let tyl, ty = uncurry_type v in
+  let ls = create_lsymbol id tyl (Some ty) in
+  { p_ls = ls; p_tv = v }
 
 type esymbol = lsymbol
 

src/programs/pgm_types.mli

@@ -41,7 +41,7 @@ type psymbol = private {
   p_tv : type_v;
 }
 
-val create_psymbol : lsymbol -> type_v -> psymbol
+val create_psymbol : preid -> type_v -> psymbol
 
 type esymbol = lsymbol
 

src/programs/pgm_typing.mli

@@ -21,8 +21,7 @@ open Why
 
 val debug : Debug.flag
 
-val decl :
-  Env.env -> Pgm_env.env -> Pgm_ptree.decl -> Pgm_env.env * Pgm_ttree.decl list
+val decl : Env.env -> Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
 
 val print_post : Format.formatter -> Pgm_ttree.post -> unit