Merge branch 'master' into substitution

Author: quicquid

_oasis

@@ -7,7 +7,7 @@ License:     BSD-3-clause
 Plugins:     META (0.3)
 AlphaFeatures: ocamlbuild_more_args
 
-Executable tlapm
+Executable tlapm2
   Path:       src
   BuildTools: ocamlbuild
 #  CompiledObject: native

_tags

@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: eeea92f4095e11397222270722383a49)
+# DO NOT EDIT (digest: f0e44f04570ded47df44744f470a0578)
 # Ignore VCS directories, you can use the same kind of rule outside
 # OASIS_START/STOP if you want to exclude directories that contains
 # useless stuff for the build process
@@ -14,7 +14,7 @@ true: annot, bin_annot
 ".git": not_hygienic
 "_darcs": -traverse
 "_darcs": not_hygienic
-# Executable tlapm
+# Executable tlapm2
 "src/tlapm.byte": pkg_result
 "src/tlapm.byte": pkg_sexplib
 "src/tlapm.byte": pkg_str

nunchaku/prelude.nun

@@ -6,4 +6,7 @@ include "set-theory.nun".
 
 spec dom : u -> u
 and app : u -> u -> u :=
-	 forall f g. (dom (upcast f) = dom (upcast g)) && (forall x. mem x (dom (upcast f)) => ((app (upcast f) x)=(app (upcast g) x))) => (f=g).
+    forall f g. (dom (upcast f) = dom (upcast g))
+                && (forall x. t_mem x (dom (upcast f))
+                              => ((app (upcast f) x)=(app (upcast g) x)))
+                    => (f=g).

nunchaku/set-theory.nun

@@ -6,43 +6,43 @@ val mem_raw : u -> u -> prop.
 # extensionality
 axiom forall (A : alpha_u) (B : alpha_u). upcast A = upcast B || (exists (x : alpha_u). ~ (mem_raw (upcast x) (upcast A) = mem_raw (upcast x) (upcast B))).
 
-rec mem : u -> u -> prop :=
-   forall x y. mem x y = (mem_raw x y asserting ((exists a. upcast a = x) && (exists b. upcast b = y))).
-#  forall x y. mem x y = unique_unsafe (fun P. P = mem_raw x y && (exists a. upcast a = x) && (exists b. upcast b = y)).
+rec t_mem : u -> u -> prop :=
+   forall x y. t_mem x y = (mem_raw x y asserting ((exists a. upcast a = x) && (exists b. upcast b = y))).
+#  forall x y. t_mem x y = unique_unsafe (fun P. P = mem_raw x y && (exists a. upcast a = x) && (exists b. upcast b = y)).
 
-val trans_mem : alpha_u  -> alpha_u -> prop.
+val t_trans_mem : alpha_u  -> alpha_u -> prop.
 
 # overapproximation of transitive closure
-axiom forall x (y : alpha_u). mem_raw (upcast x) (upcast y) => trans_mem x y.
-axiom forall x y (z : alpha_u). trans_mem x y && mem_raw (upcast y) (upcast z) => trans_mem x z.
+axiom forall x (y : alpha_u). mem_raw (upcast x) (upcast y) => t_trans_mem x y.
+axiom forall x y (z : alpha_u). t_trans_mem x y && mem_raw (upcast y) (upcast z) => t_trans_mem x z.
 
 # acyclicity
-axiom forall x. ~ trans_mem x x.
+axiom forall x. ~ t_trans_mem x x.
 
 # empty set
-rec emptyset : u :=
-  emptyset = unique_unsafe (fun A. forall a. ~ mem_raw (upcast a) A && (exists a. upcast a = A)).
+rec t_emptyset : u :=
+  t_emptyset = unique_unsafe (fun A. forall a. ~ mem_raw (upcast a) A && (exists a. upcast a = A)).
 
 # subset
-rec subset : u -> u -> prop :=
-  forall A B. subset A B = (forall a. mem (upcast a) A => mem (upcast a) B).
+rec t_subset : u -> u -> prop :=
+  forall A B. t_subset A B = (forall a. t_mem (upcast a) A => t_mem (upcast a) B).
 
 # union
-rec union : u -> u -> u :=
-  forall A B. union A B = unique_unsafe (fun C. forall x. mem (upcast x) C = (mem (upcast x) A || mem (upcast x) B)).
+rec t_union : u -> u -> u :=
+  forall A B. t_union A B = unique_unsafe (fun C. forall x. t_mem (upcast x) C = (t_mem (upcast x) A || t_mem (upcast x) B)).
 
 # intersection
-rec inter : u -> u -> u :=
-  forall A B. inter A B = unique_unsafe (fun C. forall x. mem (upcast x) C = (mem (upcast x) A && mem (upcast x) B)).
+rec t_inter : u -> u -> u :=
+  forall A B. t_inter A B = unique_unsafe (fun C. forall x. t_mem (upcast x) C = (t_mem (upcast x) A && t_mem (upcast x) B)).
 
 # substraction
-rec minus : u -> u -> u :=
-  forall A B. minus A B = unique_unsafe (fun C. forall x. mem (upcast x) C = (mem (upcast x) A && ~(mem (upcast x) B))).
+rec t_minus : u -> u -> u :=
+  forall A B. t_minus A B = unique_unsafe (fun C. forall x. t_mem (upcast x) C = (t_mem (upcast x) A && ~(t_mem (upcast x) B))).
 
 # powerset
-rec Pow : u -> u :=
-  forall B. Pow B = unique_unsafe (fun C. forall A. mem (upcast A) C = subset (upcast A) B).
+rec t_Pow : u -> u :=
+  forall B. t_Pow B = unique_unsafe (fun C. forall A. t_mem (upcast A) C = t_subset (upcast A) B).
 
 # big union
-rec Union : u -> u :=
-  forall A. Union A = unique_unsafe (fun U. forall x. mem (upcast x) U = (exists X. mem (upcast x) (upcast X) && mem (upcast X) A)).
+rec t_Union : u -> u :=
+  forall A. t_Union A = unique_unsafe (fun U. forall x. t_mem (upcast x) U = (exists X. t_mem (upcast x) (upcast X) && t_mem (upcast X) A)).

opam

@@ -0,0 +1,34 @@
+opam-version: "1.2"
+name: "tlapm2"
+version: "dev"
+maintainer: "[email protected]"
+authors: ["Martin Riener" "Matthieu Lequesne"]
+homepage: "https://github.com/tlaplus/v2-tlapm"
+bug-reports: "https://github.com/tlaplus/v2-tlapm/issues"
+dev-repo: "https://github.com/tlaplus/v2-tlapm.git"
+build: [
+    ["oasis" "setup"]
+    ["./configure"
+        "--prefix" prefix
+        "--disable-tests"
+        "--enable-docs"
+    ]
+    [make "build"]
+]
+build-doc: [ make "doc" ]
+build-test: [ make "test" ]
+install: [make "install"]
+remove: ["ocamlfind" "remove" "tlapm2"]
+depends: [
+    "ocamlfind" {build}
+    "base-unix"
+    "base-threads"
+    "oasis" {build}
+    "ocamlbuild" {build}
+    "xmlm" {>= "1.2.0"}
+    "sexplib"
+    "result"
+]
+depopts: [
+    "kaputt" {test}
+]

setup.ml

@@ -1,9 +1,9 @@
 (* setup.ml generated for the first time by OASIS v0.3.0 *)
 
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 8262f1c4aea1c2f319112ff96e3a5592) *)
+(* DO NOT EDIT (digest: 61707546127f264f3558ee487b8fab5c) *)
 (*
-   Regenerated by OASIS v0.4.7
+   Regenerated by OASIS v0.4.8
    Visit http://oasis.forge.ocamlcore.org for more information and
    documentation about functions used in this file.
 *)
@@ -658,6 +658,7 @@ module OASISContext = struct
       ignore_unknown_fields: bool;
       printf:                level -> string -> unit;
       srcfs:                 source OASISFileSystem.fs;
+      load_oasis_plugin:     string -> bool;
     }
 
 
@@ -682,6 +683,7 @@ module OASISContext = struct
         ignore_unknown_fields = false;
         printf                = printf;
         srcfs                 = new OASISFileSystem.host_fs(Sys.getcwd ());
+        load_oasis_plugin     = (fun _ -> false);
       }
 
 
@@ -3160,7 +3162,7 @@ module OASISFileUtil = struct
 end
 
 
-# 3163 "setup.ml"
+# 3165 "setup.ml"
 module BaseEnvLight = struct
 (* # 22 "src/base/BaseEnvLight.ml" *)
 
@@ -3240,7 +3242,7 @@ module BaseEnvLight = struct
 end
 
 
-# 3243 "setup.ml"
+# 3245 "setup.ml"
 module BaseContext = struct
 (* # 22 "src/base/BaseContext.ml" *)
 
@@ -5663,7 +5665,7 @@ module BaseCompat = struct
 end
 
 
-# 5666 "setup.ml"
+# 5668 "setup.ml"
 module InternalConfigurePlugin = struct
 (* # 22 "src/plugins/internal/InternalConfigurePlugin.ml" *)
 
@@ -6469,7 +6471,7 @@ module InternalInstallPlugin = struct
 end
 
 
-# 6472 "setup.ml"
+# 6474 "setup.ml"
 module OCamlbuildCommon = struct
 (* # 22 "src/plugins/ocamlbuild/OCamlbuildCommon.ml" *)
 
@@ -6842,7 +6844,7 @@ module OCamlbuildDocPlugin = struct
 end
 
 
-# 6845 "setup.ml"
+# 6847 "setup.ml"
 module CustomPlugin = struct
 (* # 22 "src/plugins/custom/CustomPlugin.ml" *)
 
@@ -6974,7 +6976,7 @@ module CustomPlugin = struct
 end
 
 
-# 6977 "setup.ml"
+# 6979 "setup.ml"
 open OASISTypes;;
 
 let setup_t =
@@ -7075,7 +7077,7 @@ let setup_t =
             [
                Executable
                  ({
-                     cs_name = "tlapm";
+                     cs_name = "tlapm2";
                      cs_data = PropList.Data.create ();
                      cs_plugin_data = []
                   },
@@ -7446,16 +7448,16 @@ let setup_t =
           plugin_data = []
        };
      oasis_fn = Some "_oasis";
-     oasis_version = "0.4.7";
-     oasis_digest = Some "\135\164\028I\2394\153\181HU\245\236y\192\001\016";
+     oasis_version = "0.4.8";
+     oasis_digest = Some "\024\000\131hU\200KA\150\252\184s\228.\206\131";
      oasis_exec = None;
      oasis_setup_args = [];
      setup_update = false
   };;
 
 let setup () = BaseSetup.setup setup_t;;
 
-# 7459 "setup.ml"
+# 7461 "setup.ml"
 let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
 open BaseCompat.Compat_0_4
 (* OASIS_STOP *)

src/nunchaku/nun_mod.ml

@@ -2,8 +2,6 @@ open Sexplib.Type
 open Format
 open CCFormat
 
-
-
 (** Definition **)
 
 type term =
@@ -99,7 +97,7 @@ and unroll_values v = match v with
 
 and unroll_fun_term l = match l with
   | [(List vars);values] -> Fun ((unroll_vars vars),(unroll_values values))
-  | _ -> failwith "ERROR unroll_fun_term failed"   
+  | _ -> failwith "ERROR unroll_fun_term failed"
 
 let unroll_var v = match v with
   | [Atom var_name; var_type] -> (var_name, sexp_to_type var_type)
@@ -110,7 +108,7 @@ let rec sexp_to_fun_model_entry name var_acc t = match t with
   | _ -> Const (name, (Fun (var_acc,(unroll_values t))))
 
 let sexp_to_model_entry t = match t with
-  | List ((Atom "type")::tl) -> sexp_to_type_model_entry tl 
+  | List ((Atom "type")::tl) -> sexp_to_type_model_entry tl
   | List [(Atom "val");name;(List ((Atom "fun")::tl))]  -> sexp_to_fun_model_entry (sexp_to_name name) [] (List ((Atom "fun")::tl)) 
   | List ((Atom "val")::tl)  -> sexp_to_val_model_entry tl
   | _ -> failwith "sexp_to_model_entry failed"
@@ -138,7 +136,7 @@ let rec list_to_string print_one separator list =
   | t::q -> (print_one t)^separator^(list_to_string print_one separator q)
 
 let comma = ", "
-let andand = " && " 
+let andand = " && "
 let newline = " \n"
 let space = " "
 
@@ -187,7 +185,3 @@ let print_nun_mod output_file mod_tree =
   fprintf fft "@.%!";
   print_flush ();
   close_out oc
-
-
-
-

src/nunchaku/nun_pb.ml

@@ -100,9 +100,9 @@ end = struct
     | `Forall -> "forall"
     | `Exists -> "exists"
     | `Apply -> "app"
-    | `Mem -> "mem"
-    | `Intersect -> "inter"
-    | `Union -> "union"
+    | `Mem -> "t_mem"
+    | `Intersect -> "t_inter"
+    | `Union -> "t_union"
     | `Undefined s -> "?_" ^ s
 
   let print out s = Format.pp_print_string out (to_string s)
@@ -305,7 +305,12 @@ let rec unroll_if_ t = match t with
 
 let pp_list_ ~sep p = CCFormat.list ~start:"" ~stop:"" ~sep p
 
-let pp_set p = CCFormat.list ~start:"(unique_unsafe (fun S. forall (x:alpha_u). mem (upcast x) S = ((upcast x) = " ~stop:")))" ~sep:") || ((upcast x) = " p			  
+(* TODO: replace the strings by symbolic represntations of the formulas *)
+let pp_set p = CCFormat.list
+    ~start:"(unique_unsafe (fun S. forall (x:alpha_u). t_mem (upcast x) S = ((upcast x) = "
+    ~stop:")))"
+    ~sep:") || ((upcast x) = "
+    p
 
 let rec print_term out term = match term with
   | Builtin s -> Builtin.print out s
@@ -341,25 +346,29 @@ let rec print_term out term = match term with
   | Ite (a,b,c) ->
     (* special case to avoid deep nesting of ifs *)
     let pp_middle out (a,b) =
-      fpf out "@[<2>else if@ @[%a@]@]@ @[<2>then@ @[%a@]@]" print_term a print_term b
+      fpf out "@[<2>else if@ @[%a@]@]@ @[<2>then@ @[%a@]@]"
+        print_term a print_term b
     in
     let middle, last = unroll_if_ c in
     fpf out "@[<hv>@[<2>if@ @[%a@]@]@ @[<2>then@ %a@]@ %a@ @[<2>else@ %a@]@]"
       print_term a print_term b
       (pp_list_ ~sep:"" pp_middle) middle
       print_term last
   | Forall ((var,ty),None,t) ->
-    fpf out "@[<2>(forall %a.@ %a)@]" print_typed_var (var,ty) print_term t (* TODO replace => by to_string Apply *)
+    fpf out "@[<2>(forall %a.@ %a)@]" print_typed_var (var,ty)
+      print_term t (* TODO replace => by to_string Apply *)
   | Forall ((var,ty),s,t) ->
-    fpf out "@[<2>(forall %a.@ %a => %a)@]" print_typed_var (var,ty) print_mem (var,s) print_term t (* TODO replace => by to_string Apply *)
+    fpf out "@[<2>(forall %a.@ %a => %a)@]" print_typed_var (var,ty)
+      print_mem (var,s) print_term t (* TODO replace => by to_string Apply *)
   | Exists ((var,ty),None,t) ->
     fpf out "@[<2>(exists %a.@ %a)@]" print_typed_var (var,ty) print_term t
   | Exists ((var,ty),s,t) ->
-    fpf out "@[<2>(exists %a.@ %a && %a)@]" print_typed_var (var,ty) print_mem (var,s) print_term t
+    fpf out "@[<2>(exists %a.@ %a && %a)@]" print_typed_var (var,ty)
+      print_mem (var,s) print_term t
   | Asserting (_, []) -> assert false
-  | SetEnum l -> 
+  | SetEnum l ->
     begin match l with
-      | [] -> fpf out "@[<2>%s@]" "emptyset"
+      | [] -> fpf out "@[<2>%s@]" "t_emptyset"
       | _ -> fpf out "@[<2>%a@]" (pp_set print_term_inner) l
     end
   | Asserting (t, l) ->
@@ -397,7 +406,7 @@ and print_typed_var out (v,ty) = match ty with
 
 and print_mem out (var,set) = match set with
   | None -> fpf out ""
-  | Some t -> fpf out "@ mem %a %a" pp_var_or_wildcard (`Var var) print_term t
+  | Some t -> fpf out "@ t_mem %a %a" pp_var_or_wildcard (`Var var) print_term t
 
 
 let pp_rec_defs out l =

src/nunchaku/simple_expr/simple_expr_ds.mli

@@ -281,4 +281,3 @@ type simple_entry =
 
 
 type simple_term_db = (int * simple_entry) list
-

src/nunchaku/tla_mod.ml

@@ -79,7 +79,7 @@ let set_mem_main f = let (_,{cases;_}) = f in set_mem_aux cases []
 let nun_to_tla_fun fvar fdt = (List.map fst fvar, nun_to_tla_dt fdt)
 
 let add_fun name fvar fdt model = match name with
-  | s when s="mem" || s = "trans_mem" || s = "unique_unsafe__u" -> model
+  | s when s="t_mem" || s = "t_trans_mem" || s = "unique_unsafe__u" -> model
   | "mem_raw" -> let mem' = nun_to_tla_fun fvar fdt in
     set_mem model (set_mem_main mem')
   | "app" -> let app' = nun_to_tla_fun fvar fdt in set_app model (Some app')

src/nunchaku/tla_pb.ml

@@ -15,4 +15,3 @@ let print_tla_pb file obl =
   Format.fprintf fft "%a" fmt_tla_pb obl;
   Format.fprintf fft "@.%!";
   close_out oc
-