diff --git a/doc/code/Abduction.html b/doc/code/Abduction.html index 44d3955..6f3bc51 100644 --- a/doc/code/Abduction.html +++ b/doc/code/Abduction.html @@ -63,7 +63,13 @@

Module Abduction

are not most general. Default false.
-
val richer_answers : bool Pervasives.ref
+
val richer_answers : bool Pervasives.ref
+revert_cst=true tries replacing constants by variables in the + initial candidates for abduction answer, given corresponding + equations in the premise. Default true.
+
+ +
val revert_cst : bool Pervasives.ref
val timeout_count : int Pervasives.ref
val fail_timeout_count : int Pervasives.ref
val no_alien_prem : bool Pervasives.ref
diff --git a/doc/code/Infer.html b/doc/code/Infer.html index 3f77cc7..163fd39 100644 --- a/doc/code/Infer.html +++ b/doc/code/Infer.html @@ -40,6 +40,7 @@

Module Infer

val annotating_fun : bool Pervasives.ref
val annotating_letin : bool Pervasives.ref
val inform_toplevel : bool Pervasives.ref
+
val time_toplevel : bool Pervasives.ref
type cnstrnt =
+LetVal of string option * pat * uexpr * typ_scheme option * lc
diff --git a/doc/code/Terms.html b/doc/code/Terms.html index 5f99326..3906d40 100644 --- a/doc/code/Terms.html +++ b/doc/code/Terms.html @@ -38,7 +38,8 @@

Module Terms

Since Mar 2013
-
+ +
val show_extypes : bool Pervasives.ref

Definitions


val debug : bool Pervasives.ref
@@ -534,7 +535,7 @@

Zippers.


 | -LetVal of string option * pat * uexpr * typ_scheme option
* uexpr list * lc
@@ -577,7 +578,7 @@

Zippers.


| -ILetVal of string option * pat * texpr * typ_scheme
* (string * typ_scheme) list * texpr list
* (pat * int option) list * lc +ILetVal of string option * pat * texpr * typ_scheme
* (string * typ_scheme) list * (pat * int option) list
* lc diff --git a/doc/code/html.stamp b/doc/code/html.stamp index bb5a97d..91beac5 100644 --- a/doc/code/html.stamp +++ b/doc/code/html.stamp @@ -1 +1 @@ -28f09b073267850f329cd388fcfe9996 \ No newline at end of file +199897d40a8487a113d547a2662f1c14 \ No newline at end of file diff --git a/doc/code/index_values.html b/doc/code/index_values.html index 2ec5eac..be79c4f 100644 --- a/doc/code/index_values.html +++ b/doc/code/index_values.html @@ -326,6 +326,8 @@

Index of values

return_type [Terms] +revert_cst [Abduction] + revert_renaming [Terms]
Union/conjunction of sort-separated formulas, additionally @@ -333,7 +335,12 @@

Index of values

richer_answers [Abduction] - +
+revert_cst=true tries replacing constants by variables in the + initial candidates for abduction answer, given corresponding + equations in the premise. +
+
S sb_atom_binary [Terms] @@ -356,6 +363,8 @@

Index of values

separate_subst [Infer] +show_extypes [Terms] + sigma [Terms] simplify [Infer] @@ -389,6 +398,8 @@

Index of values

tdelta' [Terms] +time_toplevel [Infer] + timeout_count [Invariants] timeout_count [Abduction] diff --git a/doc/code/type_Abduction.html b/doc/code/type_Abduction.html index e117b33..271d7fe 100644 --- a/doc/code/type_Abduction.html +++ b/doc/code/type_Abduction.html @@ -18,6 +18,7 @@   val skip_kind : Abduction.skip_kind Pervasives.ref
  val more_general : bool Pervasives.ref
  val richer_answers : bool Pervasives.ref
+  val revert_cst : bool Pervasives.ref
  val timeout_count : int Pervasives.ref
  val fail_timeout_count : int Pervasives.ref
  val no_alien_prem : bool Pervasives.ref
diff --git a/doc/code/type_Infer.html b/doc/code/type_Infer.html index ec594a2..d42ae0b 100644 --- a/doc/code/type_Infer.html +++ b/doc/code/type_Infer.html @@ -17,6 +17,7 @@   val annotating_fun : bool Pervasives.ref
  val annotating_letin : bool Pervasives.ref
  val inform_toplevel : bool Pervasives.ref
+  val time_toplevel : bool Pervasives.ref
  type cnstrnt =
      A of Terms.formula
    | And of Infer.cnstrnt list
diff --git a/doc/code/type_Terms.html b/doc/code/type_Terms.html index 1af8cad..847b87a 100644 --- a/doc/code/type_Terms.html +++ b/doc/code/type_Terms.html @@ -14,6 +14,7 @@ sig
+  val show_extypes : bool Pervasives.ref
  val debug : bool Pervasives.ref
  type cns_name = CNam of string | Extype of int
  val tuple : Terms.cns_name
@@ -153,7 +154,7 @@     | LetRecVal of string option * string * Terms.uexpr *
        Terms.typ_scheme option * Terms.uexpr list * Terms.lc
    | LetVal of string option * Terms.pat * Terms.uexpr *
-        Terms.typ_scheme option * Terms.uexpr list * Terms.lc
+        Terms.typ_scheme option * Terms.lc
  type annot_item =
      ITypConstr of string option * Terms.cns_name * Defs.sort list *
        Terms.lc
@@ -165,8 +166,8 @@     | ILetRecVal of string option * string * Terms.texpr * Terms.typ_scheme *
        Terms.texpr list * (Terms.pat * int option) list * Terms.lc
    | ILetVal of string option * Terms.pat * Terms.texpr * Terms.typ_scheme *
-        (string * Terms.typ_scheme) list * Terms.texpr list *
-        (Terms.pat * int option) list * Terms.lc
+        (string * Terms.typ_scheme) list * (Terms.pat * int option) list *
+        Terms.lc
  val typ_size : Terms.typ -> int
  val atom_size : Terms.atom -> int
  val fvs_typ : Terms.typ -> Defs.VarSet.t
diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 97d4875..23918c7 100644 Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ diff --git a/doc/invargent.pdf b/doc/invargent.pdf index 2bc8e83..8c65ed6 100644 Binary files a/doc/invargent.pdf and b/doc/invargent.pdf differ