Merge branch 'master' into stable

Author: c-cube

Makefile

@@ -53,5 +53,17 @@ QTEST_PREAMBLE='open Nunchaku_core;; '
 watch:
 	while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
 		echo "============ at `date` ==========" ; \
-		make ; \
+		make all ; \
 	done
+
+ocp-indent:
+	@which ocp-indent > /dev/null || { \
+	  	echo 'ocp-indent not found; please run `opam install ocp-indent`'; \
+		exit 1 ; \
+	  }
+
+reindent: ocp-indent
+	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: "
+	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i
+
+.PHONY: reindent ocp-indent watch

README.adoc

@@ -19,13 +19,13 @@ There is a dedicated mailing list at [email protected]
 The https://github.com/nunchaku-inria/nunchaku/issues[issue tracker] can be
 used for reporting bugs.
 
+== Documentation
+
+the API documentation can be found at https://nunchaku-inria.github.io/nunchaku/.
 == Build
 
 To build Nunchaku, there are several ways.
 
-== Documentation
-
-the API documentation can be found at https://nunchaku-inria.github.io/nunchaku/.
 
 === Released versions
 

_oasis

@@ -1,6 +1,6 @@
 OASISFormat: 0.4
 Name:        nunchaku
-Version:     0.3.1
+Version:     0.4
 Homepage:    https://github.com/nunchaku/nunchaku
 Authors:     Simon Cruanes, Jasmin Blanchette
 License:     BSD-2-clause
@@ -27,11 +27,11 @@ Library nunchaku_core
                     UntypedAST, Model, TypeUnify, Problem, FO, Reduce,
                     Env, Statement, FO_tptp, FO_rel, Cardinality,
                     Scheduling, Polarity, Traversal, ProblemMetadata,
-                    AnalyzeType, Prelude, TypeCheck, Lazy_list,
-                    Sexp_lib, Sexp_lex,
+                    AnalyzeType, Prelude, TypeCheck, Lazy_list, Bit_set,
+                    Sexp_lib, Sexp_lex, Precedence, Binder, Builtin,
+                    Cardinal_encode,
                     terms/TermInner,
                     terms/TermTyped,
-                    terms/TermMono,
                     terms/Pattern,
                     types/TypePoly,
                     types/TypeMono
@@ -75,6 +75,7 @@ Library nunchaku_transformations
                     ElimRecursion,
                     ElimMultipleEqns,
                     ElimIndPreds,
+                    ElimQuantifiers,
                     ElimCopy,
                     Polarize,
                     Unroll,
@@ -85,6 +86,9 @@ Library nunchaku_transformations
                     Elim_prop_args,
                     Elim_ite,
                     Elim_infinite,
+                    Trans_ho_fo,
+                    Trans_fo_tptp,
+                    Lift_undefined,
                     FoToRelational
   Install:          true
   FindlibName:      transformations

_tags

@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: 0b0218c6de70ee6a72e00f7814fcc531)
+# DO NOT EDIT (digest: 898f771f499cb533fcbf69bd9f225472)
 # 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
@@ -42,11 +42,15 @@ true: annot, bin_annot
 "src/core/Prelude.cmx": for-pack(Nunchaku_core)
 "src/core/TypeCheck.cmx": for-pack(Nunchaku_core)
 "src/core/Lazy_list.cmx": for-pack(Nunchaku_core)
+"src/core/Bit_set.cmx": for-pack(Nunchaku_core)
 "src/core/Sexp_lib.cmx": for-pack(Nunchaku_core)
 "src/core/Sexp_lex.cmx": for-pack(Nunchaku_core)
+"src/core/Precedence.cmx": for-pack(Nunchaku_core)
+"src/core/Binder.cmx": for-pack(Nunchaku_core)
+"src/core/Builtin.cmx": for-pack(Nunchaku_core)
+"src/core/Cardinal_encode.cmx": for-pack(Nunchaku_core)
 "src/core/terms/TermInner.cmx": for-pack(Nunchaku_core)
 "src/core/terms/TermTyped.cmx": for-pack(Nunchaku_core)
-"src/core/terms/TermMono.cmx": for-pack(Nunchaku_core)
 "src/core/terms/Pattern.cmx": for-pack(Nunchaku_core)
 "src/core/types/TypePoly.cmx": for-pack(Nunchaku_core)
 "src/core/types/TypeMono.cmx": for-pack(Nunchaku_core)
@@ -120,6 +124,7 @@ true: annot, bin_annot
 "src/transformations/ElimRecursion.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/ElimMultipleEqns.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/ElimIndPreds.cmx": for-pack(Nunchaku_transformations)
+"src/transformations/ElimQuantifiers.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/ElimCopy.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/Polarize.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/Unroll.cmx": for-pack(Nunchaku_transformations)
@@ -130,6 +135,9 @@ true: annot, bin_annot
 "src/transformations/Elim_prop_args.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/Elim_ite.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/Elim_infinite.cmx": for-pack(Nunchaku_transformations)
+"src/transformations/Trans_ho_fo.cmx": for-pack(Nunchaku_transformations)
+"src/transformations/Trans_fo_tptp.cmx": for-pack(Nunchaku_transformations)
+"src/transformations/Lift_undefined.cmx": for-pack(Nunchaku_transformations)
 "src/transformations/FoToRelational.cmx": for-pack(Nunchaku_transformations)
 <src/transformations/*.ml{,i,y}>: package(containers)
 <src/transformations/*.ml{,i,y}>: package(containers.data)

myocamlbuild.ml

@@ -1,5 +1,5 @@
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 7bbb25e2ce501951df8bcc5d11944431) *)
+(* DO NOT EDIT (digest: 7683553a3de792be536febb657ebf851) *)
 module OASISGettext = struct
 (* # 22 "src/oasis/OASISGettext.ml" *)
 
@@ -746,6 +746,9 @@ module MyOCamlbuildBase = struct
 (* # 110 "src/plugins/ocamlbuild/MyOCamlbuildBase.ml" *)
 
 
+  let env_filename = Pathname.basename BaseEnvLight.default_filename
+
+
   let dispatch_combine lst =
     fun e ->
       List.iter
@@ -878,7 +881,7 @@ module MyOCamlbuildBase = struct
 end
 
 
-# 881 "myocamlbuild.ml"
+# 884 "myocamlbuild.ml"
 open Ocamlbuild_plugin;;
 let package_default =
   {
@@ -931,7 +934,7 @@ let conf = {MyOCamlbuildFindlib.no_automatic_syntax = false}
 
 let dispatch_default = MyOCamlbuildBase.dispatch_default conf package_default;;
 
-# 935 "myocamlbuild.ml"
+# 938 "myocamlbuild.ml"
 (* OASIS_STOP *)
 
 open Ocamlbuild_plugin;;

nunchaku.odocl

@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: f90600f3a098e836f5ece36e8d5f85d5)
+# DO NOT EDIT (digest: 683de1371c8e3d66b66604d410c7f651)
 src/core/ID
 src/core/Var
 src/core/MetaVar
@@ -26,11 +26,15 @@ src/core/AnalyzeType
 src/core/Prelude
 src/core/TypeCheck
 src/core/Lazy_list
+src/core/Bit_set
 src/core/Sexp_lib
 src/core/Sexp_lex
+src/core/Precedence
+src/core/Binder
+src/core/Builtin
+src/core/Cardinal_encode
 src/core/terms/TermInner
 src/core/terms/TermTyped
-src/core/terms/TermMono
 src/core/terms/Pattern
 src/core/types/TypePoly
 src/core/types/TypeMono
@@ -61,6 +65,7 @@ src/transformations/Elim_HOF
 src/transformations/ElimRecursion
 src/transformations/ElimMultipleEqns
 src/transformations/ElimIndPreds
+src/transformations/ElimQuantifiers
 src/transformations/ElimCopy
 src/transformations/Polarize
 src/transformations/Unroll
@@ -71,5 +76,8 @@ src/transformations/ElimTypes
 src/transformations/Elim_prop_args
 src/transformations/Elim_ite
 src/transformations/Elim_infinite
+src/transformations/Trans_ho_fo
+src/transformations/Trans_fo_tptp
+src/transformations/Lift_undefined
 src/transformations/FoToRelational
 # OASIS_STOP

opam

@@ -1,6 +1,6 @@
 opam-version: "1.2"
 name: "nunchaku"
-version: "0.3.1"
+version: "0.4"
 authors: ["Simon Cruanes" "Jasmin Blanchette"]
 maintainer: "[email protected]"
 build: [
@@ -24,7 +24,7 @@ remove: [
 ]
 depends: [
     "ocamlfind" {build}
-    "containers" { >= "0.16" < "1.0" }
+    "containers" { >= "1.0" }
     "menhir" {build}
     "sequence"
     "base-unix"

setup.ml

@@ -1,9 +1,9 @@
 (* setup.ml generated for the first time by OASIS v0.4.5 *)
 
 (* OASIS_START *)
-(* DO NOT EDIT (digest: 3ee647490707707159b917290258991c) *)
+(* DO NOT EDIT (digest: a90055f6f245ece1eda163e6a57a57c5) *)
 (*
-   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 =
@@ -7051,7 +7053,7 @@ let setup_t =
        {
           oasis_version = "0.4";
           ocaml_version = Some (OASISVersion.VGreaterEqual "4.00.1");
-          version = "0.3.1";
+          version = "0.4";
           license =
             OASISLicense.DEP5License
               (OASISLicense.DEP5Unit
@@ -7258,11 +7260,15 @@ let setup_t =
                            "Prelude";
                            "TypeCheck";
                            "Lazy_list";
+                           "Bit_set";
                            "Sexp_lib";
                            "Sexp_lex";
+                           "Precedence";
+                           "Binder";
+                           "Builtin";
+                           "Cardinal_encode";
                            "terms/TermInner";
                            "terms/TermTyped";
-                           "terms/TermMono";
                            "terms/Pattern";
                            "types/TypePoly";
                            "types/TypeMono"
@@ -7732,6 +7738,7 @@ let setup_t =
                            "ElimRecursion";
                            "ElimMultipleEqns";
                            "ElimIndPreds";
+                           "ElimQuantifiers";
                            "ElimCopy";
                            "Polarize";
                            "Unroll";
@@ -7742,6 +7749,9 @@ let setup_t =
                            "Elim_prop_args";
                            "Elim_ite";
                            "Elim_infinite";
+                           "Trans_ho_fo";
+                           "Trans_fo_tptp";
+                           "Lift_undefined";
                            "FoToRelational"
                         ];
                       lib_pack = true;
@@ -8295,16 +8305,16 @@ let setup_t =
           plugin_data = []
        };
      oasis_fn = Some "_oasis";
-     oasis_version = "0.4.7";
-     oasis_digest = Some "|.\210\024x\163\139`?\210\197\227=\026\r\030";
+     oasis_version = "0.4.8";
+     oasis_digest = Some "\228c\019:\241\005\133^\178\015\130p\022E\018\251";
      oasis_exec = None;
      oasis_setup_args = [];
      setup_update = false
   };;
 
 let setup () = BaseSetup.setup setup_t;;
 
-# 8308 "setup.ml"
+# 8318 "setup.ml"
 let setup_t = BaseCompat.Compat_0_4.adapt_setup_t setup_t
 open BaseCompat.Compat_0_4
 (* OASIS_STOP *)