petite surprise

Makefile.in

@@ -121,7 +121,8 @@ CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\
 	task.cmo pretty.cmo trans.cmo env.cmo register.cmo
 CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
 
-UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo sysutil.cmo hashweak.cmo
+UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
+            sysutil.cmo hashweak.cmo
 UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
 
 PARSER_CMO := parser.cmo lexer.cmo denv.cmo typing.cmo 

share/emacs/why.el

@@ -26,7 +26,7 @@
 
 (defconst why-font-lock-keywords-1
   (list
-   '("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face)
+   '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
    '("{\\([^}]*\\)}" . font-lock-type-face)
    `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
    `(,(why-regexp-opt '("match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "assert" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)

src/main.ml

@@ -57,6 +57,7 @@ let list_printers = ref false
 let list_transforms = ref false
 (*let list_goals = ref false*)
 let print_debug = ref false
+let print_namespace = ref false
 
 let () = 
   Arg.parse 
@@ -88,7 +89,9 @@ provers (0 unlimited, default 10)";
 registered";
 (*     "--list-goals", Arg.Set list_goals, "list the goals of the files";*)
      "--print-debug", Arg.Set print_debug, "print on stderr the theories of \
-the files given on the commandline" 
+the files given on the commandline"; 
+     "--print-namespace", Arg.Set print_namespace, "print on stderr the \
+namespaces for the files given on the command line";
     ]
     (fun f -> Queue.push f files)
     "usage: why [options] files..."
@@ -175,6 +178,27 @@ let extract_goals ?filter =
 let file_sanitizer = 
   Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
 
+let print_theory_namespace fmt th =
+  let module T = struct
+    type t = 
+      | Namespace of string * namespace
+      | Leaf of string
+    let contents ns =
+      let acc = 
+	Mnm.fold (fun s ns acc -> (Namespace (s, ns)) :: acc) ns.ns_ns [] 
+      in
+      let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_ts acc in
+      let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_ls acc in
+      let acc = Mnm.fold (fun s _ acc -> (Leaf s) :: acc) ns.ns_pr acc in
+      acc
+    let decomp = function
+      | Namespace (s, ns) -> s, contents ns
+      | Leaf s -> s, [] 
+  end
+  in
+  let module P = Prtree.Make(T) in
+  P.print fmt (T.Namespace (th.th_name.Ident.id_short, th.th_export))
+
 let do_file env drv filename_printer file =
   if !parse_only then begin
     let filename,c = if file = "-" 
@@ -187,10 +211,15 @@ let do_file env drv filename_printer file =
   end else begin
     let m = Typing.read_file env file in
     if !print_debug then
-      eprintf "%a"
+      eprintf "%a@."
         (Pp.print_iter2 Mnm.iter Pp.newline Pp.nothing Pp.nothing 
            Pretty.print_theory)
         m;
+    if !print_namespace then
+      eprintf "%a@."
+        (Pp.print_iter2 Mnm.iter Pp.newline Pp.nothing Pp.nothing 
+           print_theory_namespace)
+        m;
     if not !type_only then
       let drv =  
         match drv with

src/programs/pgm_main.ml

@@ -52,7 +52,8 @@ let rec report fmt = function
   | Pgm_typing.Error e ->
       Pgm_typing.report fmt e
   | e ->
-      fprintf fmt "anomaly: %s" (Printexc.to_string e)
+      raise e
+(*       fprintf fmt "anomaly: %s" (Printexc.to_string e) *)
 
 open Pgm_ptree
 open Theory
@@ -67,6 +68,8 @@ let type_file file =
   close_in c;
   if !parse_only then raise Exit;
   let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
+  let th = Env.find_theory env ["programs"] "Prelude" in
+  let uc = Theory.use_export uc th in
   let _uc = 
     List.fold_left
       (fun uc d -> match d with

src/programs/pgm_ptree.mli

@@ -42,18 +42,21 @@ type expr = {
 }
 
 and expr_desc =
+  (* lambda-calculus *)
   | Econstant of constant
   | Eident of qualid
   | Eapply of expr * expr
+  | Elet of ident * expr * expr
+  (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr
+  | Ewhile of expr * loop_annotation * expr
+  | Elazy of lazy_op * expr * expr
   | Eskip 
+  (* annotations *)
   | Eassert of assertion_kind * lexpr
-  | Elazy of lazy_op * expr * expr
-  | Elet of ident * expr * expr
   | Eghost of expr
   | Elabel of ident * expr
-  | Ewhile of expr * loop_annotation * expr
 
 type decl =
   | Dcode  of ident * expr

src/programs/pgm_typing.ml

@@ -54,9 +54,9 @@ type denv = {
   uc : theory_uc;
   utyvars : (string, type_var) Hashtbl.t;
   dvars : dty Mstr.t;
-  (* predefined symbols, from theory programs.Prelude *)
-  ts_bool  : Ty.tysymbol;
-  ts_unit  : Ty.tysymbol;
+  (* predefined symbols from theory programs.Prelude *)
+  ty_bool  : dty;
+  ty_unit  : dty;
   ts_arrow : Ty.tysymbol;
 }
 
@@ -65,9 +65,9 @@ let create_denv uc =
   { uc = uc;
     utyvars = Hashtbl.create 17;
     dvars = Mstr.empty;
-    ts_bool  = ns_find_ts ns ["Prelude"; "bool"];
-    ts_unit  = ns_find_ts ns ["Prelude"; "unit"];
-    ts_arrow = ns_find_ts ns ["Prelude"; "arrow"];
+    ty_bool  = Tyapp (ns_find_ts ns ["bool"], []);
+    ty_unit  = Tyapp (ns_find_ts ns ["unit"], []);
+    ts_arrow = ns_find_ts ns ["arrow"];
   }
 (*****************************************************************************)
 
@@ -115,39 +115,39 @@ and expr_desc env loc = function
       Elet (x, e1, e2), e2.expr_type
   | Pgm_ptree.Esequence (e1, e2) ->
       let e1 = expr env e1 in
-      expected_type e1 (Tyapp (env.ts_unit, []));
+      expected_type e1 env.ty_unit;
       let e2 = expr env e2 in
       Esequence (e1, e2), e2.expr_type
   | Pgm_ptree.Eskip ->
-      Eskip, Tyapp (env.ts_unit, [])
+      Eskip, env.ty_unit
   | Pgm_ptree.Elabel (l, e1) ->
       (* TODO: add label to env *)
       let e1 = expr env e1 in
       Elabel (l, e1), e1.expr_type
   | Pgm_ptree.Eif (e1, e2, e3) ->
       let e1 = expr env e1 in
-      expected_type e1 (Tyapp (env.ts_bool, []));
+      expected_type e1 env.ty_bool;
       let e2 = expr env e2 in
       let e3 = expr env e3 in
       expected_type e3 e2.expr_type;
       Eif (e1, e2, e3), e2.expr_type
   | Pgm_ptree.Eassert (k, le) ->
-      Eassert (k, le), Tyapp (env.ts_unit, [])
+      Eassert (k, le), env.ty_unit
   | Pgm_ptree.Eghost e1 ->
       let e1 = expr env e1 in
       Eghost e1, e1.expr_type
   | Pgm_ptree.Ewhile (e1, a, e2) ->
       let e1 = expr env e1 in
-      expected_type e1 (Tyapp (env.ts_bool, []));
+      expected_type e1 env.ty_bool;
       let e2 = expr env e2 in
-      expected_type e1 (Tyapp (env.ts_unit, []));
-      Ewhile (e1, a, e2), Tyapp (env.ts_unit, [])
+      expected_type e1 env.ty_unit;
+      Ewhile (e1, a, e2), env.ty_unit
   | Pgm_ptree.Elazy (op, e1, e2) ->
       let e1 = expr env e1 in
-      expected_type e1 (Tyapp (env.ts_bool, []));
+      expected_type e1 env.ty_bool;
       let e2 = expr env e2 in
-      expected_type e2 (Tyapp (env.ts_bool, []));
-      Elazy (op, e1, e2), Tyapp (env.ts_bool, [])
+      expected_type e2 env.ty_bool;
+      Elazy (op, e1, e2), env.ty_bool
 
 let code uc id e =
   let env = create_denv uc in

src/programs/test.mlw

@@ -2,9 +2,8 @@
 (* test file for ML-why *)
 
 { 
-  use import programs.Prelude
-  type foo
-  logic foo : foo
+  type t
+  logic foo : t
   logic f(int) : int 
   logic g(x : int) : int = f(x+1)
 }
@@ -18,6 +17,8 @@ let p =
     g 2
   end
 
+let q = f(1)
+
 { 
   axiom A : forall x:int. f(x) = g(x-1)
 }

src/test.why

 
 (* test file *)
 
+theory Bug
+  use import int.Int
+  type t
+end
+
 theory Test
   use import int.Int
   logic id(x: int) : int = x

src/util/prtree.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*s Tree structures. *)
+
+module type Tree = sig
+  type t
+  val decomp : t -> string * t list
+end
+
+(*s Pretty-print functor. *)
+
+module Make(T : Tree) = struct
+
+  open Format
+
+  (* [print_node] prints one node and [print_sons] its children.
+     [pref] is the prefix to output at the beginning of line
+     and [start] is the branching drawing (["+-"] the first time, 
+     and then ["|-"]). *)
+
+  let print fmt t =
+    let rec print_node pref t = 
+      let (s, sons) = T.decomp t in
+      pp_print_string fmt s;
+      if sons <> [] then 
+        let w = String.length s in
+        let pref' = pref ^ String.make (w + 1) ' ' in
+        match sons with
+          | [t'] -> pp_print_string fmt "---"; print_node (pref' ^ "  ") t'
+          | _ -> pp_print_string fmt "-"; print_sons pref' "+-" sons
+
+    and print_sons pref start = function
+      | [] -> 
+          assert false
+      | [s] -> 
+          pp_print_string fmt "`-"; print_node (pref ^ "  ") s
+      | s :: sons -> 
+          pp_print_string fmt start; print_node (pref ^ "| ") s;
+          pp_force_newline fmt (); pp_print_string fmt pref;
+          print_sons pref "|-" sons
+
+    in
+    print_node "" t
+        
+end

src/util/prtree.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*s This module provides a generic ASCII pretty-printing function for trees,
+    in a way similar to what the Unix command pstree does:
+
+bash-+-emacs-+-emacsserver
+     |       `-ispell
+     |-pstree
+     `-xdvi.bin
+*)
+
+(*s A tree structure is given as an abstract type [t] together with a
+    decomposition function [decomp] returning the label of the node and
+    the list of the children trees. Leaves are nodes with no child (i.e.
+    an empty list). *)
+
+module type Tree = sig
+  type t
+  val decomp : t -> string * t list
+end
+
+(*s The functor [Make] takes a tree structure [T] as argument and provides a
+    single function [print: formatter -> T.t -> unit] to print a tree on a
+    given formatter. *)
+
+module Make : functor (T : Tree) -> sig
+  val print : Format.formatter -> T.t -> unit
+end