diff --git a/doc/code/Abduction.html b/doc/code/Abduction.html index 6f3bc51..c2fff4f 100644 --- a/doc/code/Abduction.html +++ b/doc/code/Abduction.html @@ -78,6 +78,19 @@

Module Abduction

val no_num_abduction : bool Pervasives.ref
+guess_eqs_nonvar=true means the only guess equations x=y tried + are for x=s, y=t in either the premise or conclusion of + abduction problem where neither s nor t are variables. + Default true.
+
+ +
val guess_eqs_nonvar : bool Pervasives.ref
+prefer_guess=true tries to guess equality-between-parameters + before considering other candidate abduction answer atoms. + Default false.
+
+ +
val prefer_guess : bool Pervasives.ref
neg_before_abd=false moves numerical negation elimination till after numerical abduction, with possibly better determination of negative facts, but worse availability of the negative @@ -92,9 +105,9 @@

Module Abduction

val num_neg_since : int Pervasives.ref
val abd_fail_flag : bool Pervasives.ref
val abd_timeout_flag : bool Pervasives.ref
-
val abd_simple : Defs.quant_ops ->
       ?without_quant:unit ->
       bvs:Defs.VarSet.t ->
       pms:Defs.VarSet.t ->
       dissociate:bool ->
       validate:(Defs.var_name list * Terms.subst -> unit) ->
       discard:(Defs.var_name list * Terms.subst) list ->
       int ->
       Defs.var_name list * Terms.subst ->
       Terms.sep_formula * Terms.subst ->
       (Defs.VarSet.t * (Defs.var_name list * Terms.subst)) option
-
val abd_typ : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       ?dissociate:bool ->
       validate:(Defs.var_name list * Terms.subst -> unit) ->
       discard:(Defs.var_name list * Terms.subst) list ->
       (Terms.sep_formula * Terms.subst) list ->
       Defs.VarSet.t * Terms.subst * Defs.var_name list * Terms.subst *
       (Terms.sep_formula * Terms.sep_formula) list
-
type discarded = ((Defs.var_name list * Terms.subst) list, NumDefs.formula list, unit)
       Terms.sep_sorts
+
val abd_simple : Defs.quant_ops ->
       ?without_quant:unit ->
       obvs:Defs.VarSet.t ->
       bvs:Defs.VarSet.t ->
       dissociate:bool ->
       validate:(Defs.var_name list * Terms.subst -> unit) ->
       neg_validate:(Defs.var_name list * Terms.subst -> int) ->
       discard:(Defs.var_name list * Terms.subst) list ->
       int ->
       Defs.var_name list * Terms.subst ->
       Terms.sep_formula * Terms.subst ->
       (Defs.VarSet.t * (Defs.var_name list * Terms.subst)) option
+
val abd_typ : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       ?dissociate:bool ->
       validate:(Defs.var_name list * Terms.subst -> unit) ->
       neg_validate:(Defs.var_name list * Terms.subst -> int) ->
       discard:(Defs.var_name list * Terms.subst) list ->
       (Terms.sep_formula * Terms.subst) list ->
       Defs.VarSet.t * Terms.subst * Defs.var_name list * Terms.subst *
       (Terms.sep_formula * Terms.sep_formula) list
+
type discarded = ((Defs.var_name list * Terms.subst) list, NumDefs.formula list,
        OrderDefs.formula list, unit)
       Terms.sep_sorts
Raises Contradiction if constraints are contradictory and NoAnswer when no answer can be found. Returns candidate @@ -103,5 +116,5 @@

Module Abduction

-
val abd : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       ?iter_no:int ->
       discard:discarded ->
       (bool * Terms.formula * Terms.formula) list ->
       (Terms.formula * Defs.loc) list ->
       Defs.VarSet.t * Terms.subst * (Defs.var_name list * Terms.formula)
+
val abd : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       xbvs:(int * Defs.VarSet.t) list ->
       ?orig_ren:(Defs.var_name, Defs.var_name) Hashtbl.t ->
       ?b_of_v:(Defs.var_name -> Defs.var_name) ->
       upward_of:(Defs.var_name -> Defs.var_name -> bool) ->
       nonparam_vars:Defs.VarSet.t ->
       ?iter_no:int ->
       discard:discarded ->
       (bool * (int * (Defs.var_name * Defs.var_name) list) list * Terms.formula *
        Terms.formula)
       list ->
       (Terms.formula * Defs.loc) list ->
       Defs.VarSet.t * Terms.subst * (Defs.var_name list * Terms.formula)
val abd_mockup_num : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       (Terms.formula * Terms.formula) list ->
       (NumDefs.formula * NumDefs.formula) list option
\ No newline at end of file diff --git a/doc/code/DisjElim.html b/doc/code/DisjElim.html index 9ca8009..0fa533f 100644 --- a/doc/code/DisjElim.html +++ b/doc/code/DisjElim.html @@ -37,14 +37,13 @@

Module DisjElim

val more_existential : bool Pervasives.ref
Allow more general argument types by inferring more existential - result type. Default value false.
+ result type. Default value false. +

+If drop_csts=true, drop assignments of existential variables to + constants during initial steps of main algorithm, as long as the + variables are constrained in other atoms of the answer. Default + true.

-
val disjelim : Defs.quant_ops ->
       bvs:Defs.VarSet.t ->
       preserve:Defs.VarSet.t ->
       do_num:bool ->
       initstep:bool ->
       Terms.formula list -> Terms.subst * (Defs.var_name list * Terms.atom list)
-
val initstep_heur : Defs.quant_ops ->
       validate:(Terms.formula -> unit) -> Terms.answer -> Terms.answer
-Filter out "suspicious" and invalid atoms of a formula. validate - should raise Contradiction when a result is - incorrect. Currently: first removes min/max atoms comparing a - variable to a constant, then performs a greedy search for valid atoms.
-
- \ No newline at end of file +
val drop_csts : bool Pervasives.ref
+
val disjelim : Defs.quant_ops ->
       ?target:Defs.var_name ->
       bvs:Defs.VarSet.t ->
       param_bvs:Defs.VarSet.t ->
       up_of_anchor:(Defs.var_name -> bool) ->
       do_num:bool ->
       guess:bool ->
       initstep:bool ->
       residuum:Terms.formula ->
       (Terms.formula * Terms.formula) list ->
       bool * Terms.formula * (Defs.var_name list * Terms.formula) *
       Terms.formula list
\ No newline at end of file diff --git a/doc/code/Infer.html b/doc/code/Infer.html index 163fd39..ddbbbef 100644 --- a/doc/code/Infer.html +++ b/doc/code/Infer.html @@ -67,7 +67,7 @@

Module Infer

| -Or of (cnstrnt * (unit -> unit)) list +Or of Defs.var_name
* (Defs.VarSet.t * cnstrnt * Terms.formula * (unit -> unit)) list
* cnstrnt @@ -129,15 +129,26 @@

Normalization


val normalize : Defs.quant_ops -> cnstrnt -> (int, int) Hashtbl.t * branch list
-
val simplify : Defs.VarSet.t -> Defs.quant_ops -> branch list -> branch list

+
val phantom_enumeration : (Terms.cns_name, Terms.cns_name list) Hashtbl.t
+Contains information about phantom enumerations, + i.e. alternatives to a datatype parameter's nullary concrete type + excluded by an assert false pattern-matching branch. + If the value for an is an empty list, the entry is not a phantom + enumeration.
+
+ +
val simplify : Defs.VarSet.t -> Defs.quant_ops -> branch list -> branch list
+Eliminate shared conclusions. Solve RetType constraints.
+
+

Postprocessing and printing


-
val separate_subst : ?avoid:Defs.VarSet.t ->
       ?keep_uni:bool ->
       Defs.quant_ops -> Terms.formula -> Terms.subst * Terms.formula
-
val separate_sep_subst : ?avoid:Defs.VarSet.t ->
       ?keep_uni:bool ->
       Defs.quant_ops -> Terms.sep_formula -> Terms.subst * Terms.sep_formula
+
val separate_subst : ?avoid:Defs.VarSet.t ->
       ?keep:Defs.VarSet.t ->
       ?bvs:Defs.VarSet.t ->
       ?keep_uni:bool ->
       apply:bool -> Defs.quant_ops -> Terms.formula -> Terms.subst * Terms.formula
+
val separate_sep_subst : ?avoid:Defs.VarSet.t ->
       ?keep:Defs.VarSet.t ->
       ?bvs:Defs.VarSet.t ->
       ?keep_uni:bool ->
       apply:bool ->
       Defs.quant_ops -> Terms.sep_formula -> Terms.subst * Terms.sep_formula
val pr_cnstrnt : Format.formatter -> cnstrnt -> unit
val pr_brs : Format.formatter -> branch list -> unit
val pr_rbrs : Format.formatter -> (Terms.formula * Terms.formula) list -> unit
val pr_rbrs3 : Format.formatter -> (bool * Terms.formula * Terms.formula) list -> unit
-
val pr_rbrs4 : Format.formatter -> (bool * 'a * Terms.formula * Terms.formula) list -> unit
-
val pr_rbrs5 : Format.formatter ->
       (bool * 'a * 'b * Terms.formula * Terms.formula) list -> unit
+
val pr_rbrs4 : Format.formatter ->
       (bool * 'a list * Terms.formula * Terms.formula) list -> unit
+
val pr_rbrs5 : Format.formatter ->
       (bool * (int * Terms.typ) list *
        (int * Terms.typ * Terms.typ * Terms.lc) list * Terms.atom list *
        Terms.atom list)
       list -> unit
val reset_state : unit -> unit
\ No newline at end of file diff --git a/doc/code/Invariants.html b/doc/code/Invariants.html index d20a38d..1611bec 100644 --- a/doc/code/Invariants.html +++ b/doc/code/Invariants.html @@ -37,6 +37,18 @@

Module Invariants

val timeout_count : int Pervasives.ref
val timeout_flag : bool Pervasives.ref
val unfinished_postcond_flag : bool Pervasives.ref
+
val use_prior_discards : bool Pervasives.ref
+Breakdown of steps through the main iteration to achieve + convergence, counting from 0. The iteration: +

+ + * disj_step.(0) is + * disj_step.(1) is + * disj_step.(2) is + * disj_step.(3) is when convergence of postconditions is enforced.
+

+ +
val disj_step : int array
type chi_subst = (int * (Defs.var_name list * Terms.formula)) list
diff --git a/doc/code/Terms.html b/doc/code/Terms.html index 3906d40..babe197 100644 --- a/doc/code/Terms.html +++ b/doc/code/Terms.html @@ -39,7 +39,18 @@

Module Terms

-
val show_extypes : bool Pervasives.ref

+
val show_extypes : bool Pervasives.ref
+If show_extypes = true, print existential type definitions in + gadti signatures. Default false. +

+If parse_if_as_integer = true, parse if a <= b then c else d + as match () with _ when a <= b -> c | _ when b+1 <= a -> d, otherwise + as match () with _ when a <= b -> c | _ -> d. Multi-conjunction + if clauses are always parsed with the else branch without the + when clause. Default true.
+

+ +
val parse_if_as_integer : bool Pervasives.ref

Definitions


val debug : bool Pervasives.ref
@@ -65,6 +76,7 @@

Definitions


val numtype : cns_name
val booltype : cns_name
val stringtype : cns_name
+
val builtin_progseq : string
module CNames: Set.S  with type elt = cns_name
val cnames_of_list : cns_name list -> CNames.t
val add_cnames : cns_name list -> CNames.t -> CNames.t
@@ -133,6 +145,13 @@

Definitions


NumAdd of ('a, 'b) expr * ('a, 'b) expr * lc + + + +| + +NumCoef of int * ('a, 'b) expr * lc + @@ -189,6 +208,13 @@

Definitions


AssertFalse of lc + + + +| + +RuntimeFailure of ('a, 'b) expr * lc + @@ -224,6 +250,13 @@

Definitions


Num_term of NumDefs.term + + + +| + +Order_term of OrderDefs.term + @@ -268,6 +301,13 @@

Definitions


Num_atom of NumDefs.atom + + + +| + +Order_atom of OrderDefs.atom + @@ -307,6 +347,13 @@

Definitions


NotEx of typ * lc + + + +| + +RetType of typ * typ * Defs.loc + @@ -509,6 +556,13 @@

Zippers.


TypConstr of string option * cns_name * Defs.sort list * lc + + + +| + +PrimTyp of string option * cns_name * Defs.sort list * string * lc + @@ -552,6 +606,13 @@

Zippers.


ITypConstr of string option * cns_name * Defs.sort list * lc + + + +| + +IPrimTyp of string option * cns_name * Defs.sort list * string * lc + @@ -594,7 +655,8 @@

Zippers.


val fvs_typs : typ list -> Defs.VarSet.t
val fvs_atom : atom -> Defs.VarSet.t
val fvs_formula : formula -> Defs.VarSet.t
-
val formula_loc : formula -> lc

+
val formula_loc : formula -> lc
+
val prim_constr_var : atom -> Defs.var_name option

Formulas


val atom_loc : atom -> lc
@@ -618,6 +680,13 @@

Formulas


cnj_num : NumDefs.formula; + + + +   + +cnj_ord : OrderDefs.formula; + @@ -635,7 +704,7 @@

Formulas


-
type ('a, 'b, 'c) sep_sorts = {
+
type ('a, 'b, 'c, 'd) sep_sorts = {
@@ -654,7 +723,14 @@

Formulas


+at_ord : 'c; + + + + +
      -at_so : 'c;
+   +at_so : 'd;
} @@ -754,22 +830,23 @@

Substitutions and unification


use_quants whether to check for quantifier violations. bvs are variables that are parameters of invariants (or are candidates for - such in the partial answer). pms are parameters to be ignored - from quantifier violations, but should already be right-most in - the quantifier. The first element of returned triple is the - unifier, the second are numeric constraints including equations, - the third one are predicate variables and NotEx atoms. The - substitution is not applied to the third element atoms!
+ such in the partial answer). The first element of returned triple + is the unifier, the second are numeric constraints including + equations, the third one are predicate variables and NotEx + atoms. The substitution is not applied to the third element + atoms!
-

val unify : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       ?pms:Defs.VarSet.t ->
       ?sb:subst -> Defs.quant_ops -> atom list -> sep_formula
+
val unify : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       ?sb:subst -> Defs.quant_ops -> atom list -> sep_formula
+
val solve_retypes : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       sb:subst -> Defs.quant_ops -> atom list -> sep_formula
+
val solve : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       ?sb:subst -> Defs.quant_ops -> atom list -> sep_formula
val to_formula : subst -> formula
Find the atoms in the formula which are valid substitutions.
-
val subst_of_cnj : ?elim_uni:bool -> Defs.quant_ops -> formula -> subst
-
val combine_sbs : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       ?pms:Defs.VarSet.t ->
       Defs.quant_ops ->
       ?more_phi:formula -> subst list -> sep_formula
-
val subst_solved : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       ?pms:Defs.VarSet.t ->
       Defs.quant_ops -> subst -> cnj:subst -> sep_formula
+
val subst_of_cnj : ?elim_uni:bool ->
       Defs.quant_ops -> formula -> subst * formula
+
val combine_sbs : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       Defs.quant_ops ->
       ?more_phi:formula -> subst list -> sep_formula
+
val subst_solved : ?use_quants:bool ->
       ?bvs:Defs.VarSet.t ->
       Defs.quant_ops -> subst -> cnj:subst -> sep_formula
val cleanup : Defs.quant_ops ->
       Defs.var_name list -> subst -> Defs.var_name list * subst

Global tables


@@ -777,7 +854,11 @@

Global tables


val sigma : sigma
+
val ex_type_chi : (int, int) Hashtbl.t
val all_ex_types : (int * lc) list Pervasives.ref
+
val builtin_gamma : (string * typ_scheme) list
+
val ty_unit : typ
+
val ty_string : typ
val fresh_typ_var : unit -> Defs.var_name
val fresh_num_var : unit -> Defs.var_name
val fresh_var : Defs.sort -> Defs.var_name
@@ -852,7 +933,7 @@

Printing


-
val pr_expr : ?export_num:string * string * string * string ->
       ?export_if:string * string * string ->
       ?export_bool:(bool * string) list ->
       (Format.formatter -> ('a, 'b) pr_expr_annot -> unit) ->
       Format.formatter -> ('a, 'b) expr -> unit
+
val pr_expr : ?export_num:string * string * string * string * string ->
       ?export_if:string * string * string ->
       ?export_bool:(bool * string) list ->
       ?export_progseq:string * string * string ->
       ?export_runtime_failure:string ->
       (Format.formatter -> ('a, 'b) pr_expr_annot -> unit) ->
       Format.formatter -> ('a, 'b) expr -> unit
val pr_uexpr : Format.formatter -> uexpr -> unit
val pr_iexpr : Format.formatter -> iexpr -> unit
val pr_atom : Format.formatter -> atom -> unit
@@ -860,6 +941,7 @@

Printing


val pr_ty : Format.formatter -> typ -> unit
val pr_alien_ty : Format.formatter -> alien_subterm -> unit
val pr_sort : Format.formatter -> Defs.sort -> unit
+
val pr_cns : Format.formatter -> cns_name -> unit
val pr_typscheme : Format.formatter -> typ_scheme -> unit
val pr_ans : Format.formatter -> answer -> unit
val pr_subst : Format.formatter -> subst -> unit
diff --git a/doc/code/html.stamp b/doc/code/html.stamp index 91beac5..1bc34ca 100644 --- a/doc/code/html.stamp +++ b/doc/code/html.stamp @@ -1 +1 @@ -199897d40a8487a113d547a2662f1c14 \ No newline at end of file +a22557df33f7d99076a1845e5d9a3dae \ No newline at end of file diff --git a/doc/code/index_values.html b/doc/code/index_values.html index be79c4f..27c42d0 100644 --- a/doc/code/index_values.html +++ b/doc/code/index_values.html @@ -52,6 +52,10 @@

Index of values


B booltype [Terms] +builtin_gamma [Terms] + +builtin_progseq [Terms] +
C c_subst_typ [Terms] @@ -95,8 +99,12 @@

Index of values


D debug [Terms] +disj_step [Invariants] + disjelim [DisjElim] +drop_csts [DisjElim] +
E early_postcond_abd [Invariants] @@ -104,6 +112,8 @@

Index of values

eq_atom [Terms] +ex_type_chi [Terms] + expr_loc [Terms] extype_id [Terms] @@ -141,6 +151,13 @@

Index of values

fvs_typs [Terms] +
G +guess_eqs_nonvar [Abduction] +
+prefer_guess=true tries to guess equality-between-parameters + before considering other candidate abduction answer atoms. +
+
H hvsubst_formula [Terms] @@ -157,11 +174,6 @@

Index of values

init_types [Terms] -initstep_heur [DisjElim] -
-Filter out "suspicious" and invalid atoms of a formula. -
-
M map_in_subst [Terms]
@@ -207,10 +219,9 @@

Index of values

no_num_abduction [Abduction]
-neg_before_abd=false moves numerical negation elimination till - after numerical abduction, with possibly better determination of - negative facts, but worse availability of the negative - facts. +guess_eqs_nonvar=true means the only guess equations x=y tried + are for x=s, y=t in either the premise or conclusion of + abduction problem where neither s nor t are variables.
normalize [Infer] @@ -233,6 +244,8 @@

Index of values

numtype [Terms]
P +parse_if_as_integer [Terms] + parser_last_num [Terms] parser_last_typ [Terms] @@ -245,6 +258,12 @@

Index of values

pat_loc [Terms] +phantom_enumeration [Infer] +
+Contains information about phantom enumerations, + i.e. +
+ pr_alien_ty [Terms] pr_ans [Terms] @@ -253,6 +272,8 @@

Index of values

pr_brs [Infer] +pr_cns [Terms] + pr_cnstrnt [Infer] pr_exception [Terms] @@ -301,12 +322,22 @@

Index of values

predvar_id [Terms] +prefer_guess [Abduction] +
+neg_before_abd=false moves numerical negation elimination till + after numerical abduction, with possibly better determination of + negative facts, but worse availability of the negative + facts. +
+ prenexize [Infer]
Returns a map from existential type to the unary predicate variable in which it will appear as result type.
+prim_constr_var [Terms] +
R register_notex [Terms]
@@ -364,15 +395,26 @@

Index of values

separate_subst [Infer] show_extypes [Terms] - +
+If show_extypes = true, print existential type definitions in + gadti signatures. +
+ sigma [Terms] simplify [Infer] - +
+Eliminate shared conclusions. +
+ skip_kind [Abduction] solve [Invariants] +solve [Terms] + +solve_retypes [Terms] + stringtype [Terms] subformula [Terms] @@ -413,6 +455,10 @@

Index of values

tuple [Terms] +ty_string [Terms] + +ty_unit [Terms] + typ_down [Terms] typ_fold [Terms] @@ -459,6 +505,12 @@

Index of values

Separate atoms into their sorts.
+use_prior_discards [Invariants] +
+Breakdown of steps through the main iteration to achieve + convergence, counting from 0. +
+
V var_not_left_of [Terms] diff --git a/doc/code/type_Abduction.html b/doc/code/type_Abduction.html index 271d7fe..d0d2d59 100644 --- a/doc/code/type_Abduction.html +++ b/doc/code/type_Abduction.html @@ -23,6 +23,8 @@   val fail_timeout_count : int Pervasives.ref
  val no_alien_prem : bool Pervasives.ref
  val no_num_abduction : bool Pervasives.ref
+  val guess_eqs_nonvar : bool Pervasives.ref
+  val prefer_guess : bool Pervasives.ref
  val neg_before_abd : bool Pervasives.ref
  val num_neg_since : int Pervasives.ref
  val abd_fail_flag : bool Pervasives.ref
@@ -30,10 +32,11 @@   val abd_simple :
    Defs.quant_ops ->
    ?without_quant:unit ->
+    obvs:Defs.VarSet.t ->
    bvs:Defs.VarSet.t ->
-    pms:Defs.VarSet.t ->
    dissociate:bool ->
    validate:(Defs.var_name list * Terms.subst -> unit) ->
+    neg_validate:(Defs.var_name list * Terms.subst -> int) ->
    discard:(Defs.var_name list * Terms.subst) list ->
    int ->
    Defs.var_name list * Terms.subst ->
@@ -44,19 +47,28 @@     bvs:Defs.VarSet.t ->
    ?dissociate:bool ->
    validate:(Defs.var_name list * Terms.subst -> unit) ->
+    neg_validate:(Defs.var_name list * Terms.subst -> int) ->
    discard:(Defs.var_name list * Terms.subst) list ->
    (Terms.sep_formula * Terms.subst) list ->
    Defs.VarSet.t * Terms.subst * Defs.var_name list * Terms.subst *
    (Terms.sep_formula * Terms.sep_formula) list
  type discarded =
-      ((Defs.var_name list * Terms.subst) list, NumDefs.formula list, unit)
+      ((Defs.var_name list * Terms.subst) list, NumDefs.formula list,
+       OrderDefs.formula list, unit)
      Terms.sep_sorts
  val abd :
    Defs.quant_ops ->
    bvs:Defs.VarSet.t ->
+    xbvs:(int * Defs.VarSet.t) list ->
+    ?orig_ren:(Defs.var_name, Defs.var_name) Hashtbl.t ->
+    ?b_of_v:(Defs.var_name -> Defs.var_name) ->
+    upward_of:(Defs.var_name -> Defs.var_name -> bool) ->
+    nonparam_vars:Defs.VarSet.t ->
    ?iter_no:int ->
    discard:Abduction.discarded ->
-    (bool * Terms.formula * Terms.formula) list ->
+    (bool * (int * (Defs.var_name * Defs.var_name) list) list *
+     Terms.formula * Terms.formula)
+    list ->
    (Terms.formula * Defs.loc) list ->
    Defs.VarSet.t * Terms.subst * (Defs.var_name list * Terms.formula)
  val abd_mockup_num :
diff --git a/doc/code/type_DisjElim.html b/doc/code/type_DisjElim.html index e896f6a..fb5258f 100644 --- a/doc/code/type_DisjElim.html +++ b/doc/code/type_DisjElim.html @@ -15,15 +15,18 @@ sig
  val more_existential : bool Pervasives.ref
+  val drop_csts : bool Pervasives.ref
  val disjelim :
    Defs.quant_ops ->
+    ?target:Defs.var_name ->
    bvs:Defs.VarSet.t ->
-    preserve:Defs.VarSet.t ->
+    param_bvs:Defs.VarSet.t ->
+    up_of_anchor:(Defs.var_name -> bool) ->
    do_num:bool ->
+    guess:bool ->
    initstep:bool ->
-    Terms.formula list ->
-    Terms.subst * (Defs.var_name list * Terms.atom list)
-  val initstep_heur :
-    Defs.quant_ops ->
-    validate:(Terms.formula -> unit) -> Terms.answer -> Terms.answer
+    residuum:Terms.formula ->
+    (Terms.formula * Terms.formula) list ->
+    bool * Terms.formula * (Defs.var_name list * Terms.formula) *
+    Terms.formula list
end \ No newline at end of file diff --git a/doc/code/type_Infer.html b/doc/code/type_Infer.html index d42ae0b..8c6d6a1 100644 --- a/doc/code/type_Infer.html +++ b/doc/code/type_Infer.html @@ -22,7 +22,9 @@       A of Terms.formula
    | And of Infer.cnstrnt list
    | Impl of Terms.formula * Infer.cnstrnt
-    | Or of (Infer.cnstrnt * (unit -> unit)) list
+    | Or of Defs.var_name *
+        (Defs.VarSet.t * Infer.cnstrnt * Terms.formula * (unit -> unit)) list *
+        Infer.cnstrnt
    | All of Defs.VarSet.t * Infer.cnstrnt
    | Ex of Defs.VarSet.t * Infer.cnstrnt
  val cn_and : Infer.cnstrnt -> Infer.cnstrnt -> Infer.cnstrnt
@@ -60,15 +62,22 @@   val normalize :
    Defs.quant_ops ->
    Infer.cnstrnt -> (int, int) Hashtbl.t * Infer.branch list
+  val phantom_enumeration : (Terms.cns_name, Terms.cns_name list) Hashtbl.t
  val simplify :
    Defs.VarSet.t -> Defs.quant_ops -> Infer.branch list -> Infer.branch list
  val separate_subst :
    ?avoid:Defs.VarSet.t ->
+    ?keep:Defs.VarSet.t ->
+    ?bvs:Defs.VarSet.t ->
    ?keep_uni:bool ->
+    apply:bool ->
    Defs.quant_ops -> Terms.formula -> Terms.subst * Terms.formula
  val separate_sep_subst :
    ?avoid:Defs.VarSet.t ->
+    ?keep:Defs.VarSet.t ->
+    ?bvs:Defs.VarSet.t ->
    ?keep_uni:bool ->
+    apply:bool ->
    Defs.quant_ops -> Terms.sep_formula -> Terms.subst * Terms.sep_formula
  val pr_cnstrnt : Format.formatter -> Infer.cnstrnt -> unit
  val pr_brs : Format.formatter -> Infer.branch list -> unit
@@ -78,9 +87,12 @@     Format.formatter -> (bool * Terms.formula * Terms.formula) list -> unit
  val pr_rbrs4 :
    Format.formatter ->
-    (bool * 'a * Terms.formula * Terms.formula) list -> unit
+    (bool * 'a list * Terms.formula * Terms.formula) list -> unit
  val pr_rbrs5 :
    Format.formatter ->
-    (bool * 'a * 'b * Terms.formula * Terms.formula) list -> unit
+    (bool * (int * Terms.typ) list *
+     (int * Terms.typ * Terms.typ * Terms.lc) list * Terms.atom list *
+     Terms.atom list)
+    list -> unit
  val reset_state : unit -> unit
end \ No newline at end of file diff --git a/doc/code/type_Invariants.html b/doc/code/type_Invariants.html index 6cf2ba2..783ba6a 100644 --- a/doc/code/type_Invariants.html +++ b/doc/code/type_Invariants.html @@ -18,6 +18,8 @@   val timeout_count : int Pervasives.ref
  val timeout_flag : bool Pervasives.ref
  val unfinished_postcond_flag : bool Pervasives.ref
+  val use_prior_discards : bool Pervasives.ref
+  val disj_step : int array
  type chi_subst = (int * (Defs.var_name list * Terms.formula)) list
  val neg_constrns : bool Pervasives.ref
  val solve :
diff --git a/doc/code/type_Terms.html b/doc/code/type_Terms.html index 847b87a..abb9385 100644 --- a/doc/code/type_Terms.html +++ b/doc/code/type_Terms.html @@ -15,12 +15,14 @@ sig
  val show_extypes : bool Pervasives.ref
+  val parse_if_as_integer : bool Pervasives.ref
  val debug : bool Pervasives.ref
  type cns_name = CNam of string | Extype of int
  val tuple : Terms.cns_name
  val numtype : Terms.cns_name
  val booltype : Terms.cns_name
  val stringtype : Terms.cns_name
+  val builtin_progseq : string
  module CNames :
    sig
      type elt = cns_name
@@ -66,6 +68,7 @@       Var of string * Terms.lc
    | Num of int * Terms.lc
    | NumAdd of ('a, 'b) Terms.expr * ('a, 'b) Terms.expr * Terms.lc
+    | NumCoef of int * ('a, 'b) Terms.expr * Terms.lc
    | String of string * Terms.lc
    | Cons of Terms.cns_name * ('a, 'b) Terms.expr list * Terms.lc
    | App of ('a, 'b) Terms.expr * ('a, 'b) Terms.expr * Terms.lc
@@ -76,6 +79,7 @@     | Letin of string option * Terms.pat * ('a, 'b) Terms.expr *
        ('a, 'b) Terms.expr * Terms.lc
    | AssertFalse of Terms.lc
+    | RuntimeFailure of ('a, 'b) Terms.expr * Terms.lc
    | AssertLeq of ('a, 'b) Terms.expr * ('a, 'b) Terms.expr *
        ('a, 'b) Terms.expr * Terms.lc
    | AssertEqty of ('a, 'b) Terms.expr * ('a, 'b) Terms.expr *
@@ -85,20 +89,23 @@       ('a, 'b) Terms.expr
  val expr_loc : ('a, 'b) Terms.expr -> Terms.lc
  val clause_loc : ('a, 'b) Terms.clause -> Terms.lc
-  type alien_subterm = Num_term of NumDefs.term
+  type alien_subterm =
+      Num_term of NumDefs.term
+    | Order_term of OrderDefs.term
  type typ =
      TVar of Defs.var_name
    | TCons of Terms.cns_name * Terms.typ list
    | Fun of Terms.typ * Terms.typ
    | Alien of Terms.alien_subterm
  val num : NumDefs.term -> Terms.typ
-  type alien_atom = Num_atom of NumDefs.atom
+  type alien_atom = Num_atom of NumDefs.atom | Order_atom of OrderDefs.atom
  type atom =
      Eqty of Terms.typ * Terms.typ * Terms.lc
    | CFalse of Terms.lc
    | PredVarU of int * Terms.typ * Terms.lc
    | PredVarB of int * Terms.typ * Terms.typ * Terms.lc
    | NotEx of Terms.typ * Terms.lc
+    | RetType of Terms.typ * Terms.typ * Defs.loc
    | A of Terms.alien_atom
  val a_num : NumDefs.atom -> Terms.atom
  type formula = Terms.atom list
@@ -146,6 +153,8 @@   val reset_state : unit -> unit
  type struct_item =
      TypConstr of string option * Terms.cns_name * Defs.sort list * Terms.lc
+    | PrimTyp of string option * Terms.cns_name * Defs.sort list * string *
+        Terms.lc
    | ValConstr of string option * Terms.cns_name * Defs.var_name list *
        Terms.formula * Terms.typ list * Terms.cns_name *
        Defs.var_name list * Terms.lc
@@ -158,6 +167,8 @@   type annot_item =
      ITypConstr of string option * Terms.cns_name * Defs.sort list *
        Terms.lc
+    | IPrimTyp of string option * Terms.cns_name * Defs.sort list * string *
+        Terms.lc
    | IValConstr of string option * Terms.cns_name * Defs.var_name list *
        Terms.formula * Terms.typ list * Terms.cns_name * Terms.typ list *
        Terms.lc
@@ -175,15 +186,22 @@   val fvs_atom : Terms.atom -> Defs.VarSet.t
  val fvs_formula : Terms.formula -> Defs.VarSet.t
  val formula_loc : Terms.formula -> Terms.lc
+  val prim_constr_var : Terms.atom -> Defs.var_name option
  val atom_loc : Terms.atom -> Terms.lc
  type subst = (Defs.var_name * (Terms.typ * Terms.lc)) list
  type hvsubst = (Defs.var_name * Defs.var_name) list
  type sep_formula = {
    cnj_typ : Terms.subst;
    cnj_num : NumDefs.formula;
+    cnj_ord : OrderDefs.formula;
    cnj_so : Terms.formula;
  }
-  type ('a, 'b, 'c) sep_sorts = { at_typ : 'a; at_num : 'b; at_so : 'c; }
+  type ('a, 'b, 'c, 'd) sep_sorts = {
+    at_typ : 'a;
+    at_num : 'b;
+    at_ord : 'c;
+    at_so : 'd;
+  }
  val num_unbox : t2:Terms.typ -> Defs.loc -> Terms.typ -> NumDefs.term
  val num_v_unbox : Defs.var_name -> Defs.loc -> Terms.typ -> NumDefs.term
  val subst_atom : Terms.subst -> Terms.atom -> Terms.atom
@@ -246,21 +264,27 @@   val unify :
    ?use_quants:bool ->
    ?bvs:Defs.VarSet.t ->
-    ?pms:Defs.VarSet.t ->
+    ?sb:Terms.subst -> Defs.quant_ops -> Terms.atom list -> Terms.sep_formula
+  val solve_retypes :
+    ?use_quants:bool ->
+    ?bvs:Defs.VarSet.t ->
+    sb:Terms.subst -> Defs.quant_ops -> Terms.atom list -> Terms.sep_formula
+  val solve :
+    ?use_quants:bool ->
+    ?bvs:Defs.VarSet.t ->
    ?sb:Terms.subst -> Defs.quant_ops -> Terms.atom list -> Terms.sep_formula
  val to_formula : Terms.subst -> Terms.formula
  val subst_of_cnj :
-    ?elim_uni:bool -> Defs.quant_ops -> Terms.formula -> Terms.subst
+    ?elim_uni:bool ->
+    Defs.quant_ops -> Terms.formula -> Terms.subst * Terms.formula
  val combine_sbs :
    ?use_quants:bool ->
    ?bvs:Defs.VarSet.t ->
-    ?pms:Defs.VarSet.t ->
    Defs.quant_ops ->
    ?more_phi:Terms.formula -> Terms.subst list -> Terms.sep_formula
  val subst_solved :
    ?use_quants:bool ->
    ?bvs:Defs.VarSet.t ->
-    ?pms:Defs.VarSet.t ->
    Defs.quant_ops -> Terms.subst -> cnj:Terms.subst -> Terms.sep_formula
  val cleanup :
    Defs.quant_ops ->
@@ -271,7 +295,11 @@        Defs.var_name list)
      Hashtbl.t
  val sigma : Terms.sigma
+  val ex_type_chi : (int, int) Hashtbl.t
  val all_ex_types : (int * Terms.lc) list Pervasives.ref
+  val builtin_gamma : (string * Terms.typ_scheme) list
+  val ty_unit : Terms.typ
+  val ty_string : Terms.typ
  val fresh_typ_var : unit -> Defs.var_name
  val fresh_num_var : unit -> Defs.var_name
  val fresh_var : Defs.sort -> Defs.var_name
@@ -288,9 +316,11 @@     | LetInOpen of 'b
    | LetInNode of 'b
  val pr_expr :
-    ?export_num:string * string * string * string ->
+    ?export_num:string * string * string * string * string ->
    ?export_if:string * string * string ->
    ?export_bool:(bool * string) list ->
+    ?export_progseq:string * string * string ->
+    ?export_runtime_failure:string ->
    (Format.formatter -> ('a, 'b) Terms.pr_expr_annot -> unit) ->
    Format.formatter -> ('a, 'b) Terms.expr -> unit
  val pr_uexpr : Format.formatter -> Terms.uexpr -> unit
@@ -300,6 +330,7 @@   val pr_ty : Format.formatter -> Terms.typ -> unit
  val pr_alien_ty : Format.formatter -> Terms.alien_subterm -> unit
  val pr_sort : Format.formatter -> Defs.sort -> unit
+  val pr_cns : Format.formatter -> Terms.cns_name -> unit
  val pr_typscheme : Format.formatter -> Terms.typ_scheme -> unit
  val pr_ans : Format.formatter -> Terms.answer -> unit
  val pr_subst : Format.formatter -> Terms.subst -> unit
diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index 61a7ffb..a242d84 100644 Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ diff --git a/doc/invargent-slides-v2.pdf b/doc/invargent-slides-v2.pdf deleted file mode 100644 index 31725d9..0000000 Binary files a/doc/invargent-slides-v2.pdf and /dev/null differ diff --git a/doc/invargent-slides-v2.tm b/doc/invargent-slides-v2.tm deleted file mode 100644 index 8de45f8..0000000 --- a/doc/invargent-slides-v2.tm +++ /dev/null @@ -1,771 +0,0 @@ - - - - -<\body> - - - - <\ornamented> - - - - <\itemize> - InvarGenT infers preconditions and invariants as types of - recursive definitions, and postconditions as existential types. - - Generalized Algebraic Data Types type system based - on François Pottier and Vincent Simonet's but without - type annotations. - - Extended to a language with existential types represented as - implicitly defined and used GADTs. - - Type inference problem as satisfaction of second order - constraints over a multi-sorted domain. - - Invariants found by , postconditions found by -- anti-unification for terms, extended convex hull. - - A numerical sort with linear equations and inequalities over - rationals, and >min>, - >max> relations (reconstructed - only for postconditions). - - |<\hidden> - - - <\really-tiny> - <\itemize> - |>|>||>>|0:\\\\|]>>>||1:\\\\|]>>>>>>>>|>>||p:\\\|\>\>|D,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p.e:\\\>>>>>>>>>||>|||>>|iC\p:\\\|C\p\p:\\\\\>>>|||x:\\\\|]>\|}>>>>>>>>|>>||D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\>>>>>>>>>|>>|i>|D\p:\\\>|\|\>|\>.\\\\\\\|\>|)>>||\>#FV>>>>>|C\K - p\p:\|\>|)>\\|\>\\\\|)>>>>>>>>>|>>||D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\>>>>>>>>>>>> - - |, added rules>>|||>||>||>>|p:\\\>>|\>\>>>>>|C\p:\\\>>>||p:\\\>>|\\\>>>>>|C\p:\\\>>>||p:\\\>>||\>#FV,\|)>>>>>>|\|\>.C\p:\\\>>>>>>>>|||>||>|||>>||,\\e:\\\>|>|,\\e:\>||)>>>>>>|C,\,\\e - e:\>>>||||\>|)>\>|C,\,\\e:\>>|,\\K - p.e:\\\>|>>>>|C,\,\\ - p=e - e:\>>>||||)>\\Dom|)>=\>>|,\\n:\>>>>>|C,\,\\e:\>>>>>>>>>>>> - - \; - - >|||>|>|>|>>|=\\|\>.D|]>.\>|D>>>>>|C,\\x:\>>>||\>>>>>|C,\\:\>>>|i - C,\\e:\C\D>>|\|\>|\>.\\\\\|\>|)>>>>>>|C,\\K - e\e:\|\>|)>>>>|\\|)> - e:\|C,\\ - p=e - e:\>>>>>>>>>|||>||>||||>>|\e:\\\>>|\e:\>>>>>|C,\\e - e:\>>>||\e:\>|\e:\>>|=\\|\>.D|]>.\>|=\\|}>>>>>>|C,\\ - x=e - e:\>>>||||i - C,\\c:\\\|C,\\\\c|)>:\\\>>>>>>>>>>>> - - | processing>>||||>||>||>>|D,\\e:\>>||\>#FV,C|)>>>>>>|C\\\|\>.D,\\e:\\|\>.D|]>.\>>>||\e:\|\>.\>>|D|\>\|\>|]>>>>>>|C,\\e:\|\>\|\>|]>>>>||\e:\>||\e:\>>>>>|C\D,\\e:\>>>>|>||>||>>|\e:\>>||\>#FV,\|)>>>>>>|\|\>.C,\\e:\>>>||\e:\>>|\>\>>>>>|C,\\e:\>>>||,\\e:\>>>>>>>>|||)>= - x=n|)> K x>>|K\\\l=\>>>||)>=x>>|>|>,\|)>=\|)>|\>|)>>>|>| - e,K|)>=n,K|)> - n,\|)>>>|>|>,\|)>=\|\>|)>>>|>|>,K|)>=\|)>|\>|)>>>|K\\>>>||)>=p.n|)>>>|>| - p=e - e,K|)>= - p=n,\|)> - n,K|)>>>|>>>>>>>>> - - - |<\hidden> - > - - : - - <\code> - datatype Avl : type * num - - datacons Empty : >a. Avl (a, 0) - - datacons Node : - - \ \ >a,k,m,n [k=max(m,n) > - 0>m > 0>n - > n>m+2 > - m>n+2]. - - \ \ \ \ \ Avl (a, m) * a * Avl (a, n) * Num (k+1) - > Avl (a, k+1) - - \; - - let height = function - - \ \ \| Empty -\> 0 - - \ \ \| Node (_, _, _, k) -\> k - - \; - - let create = fun l x r -\> - - \ \ ematch height l, height r with - - \ \ \| i, j when j \= i -\> Node (l, x, r, i+1) - - \ \ \| i, j when i \= j -\> Node (l, x, r, j+1) - - - Result: - - <\code> - val height : >n, a. Avl (a, n) > - Num n - - val create : - - \ \ >k, n, a[k > n + 2 - > n > k + 2 > 0 - > k > 0 > n]. - - \ \ Avl (a, k) > a > Avl (a, n) - > >i[i=max (k + 1, n + 1)].Avl (a, - i) - - |<\hidden> - > - - : - - <\code> - datatype Avl : type * num - - datacons Empty : >a. Avl (a, 0) - - datacons Node : - - \ \ >a,k,m,n [k=max(m,n) > - 0>m > 0>n - > n>m+2 > - m>n+2]. - - \ \ \ \ \ Avl (a, m) * a * Avl (a, n) * Num (k+1) - > Avl (a, k+1) - - \; - - let rec min_binding = function - - \ \ \| Empty -\> assert false - - \ \ \| Node (Empty, x, r, _) -\> x - - \ \ \| Node ((Node (_,_,_,_) as l), x, r, _) -\> min_binding l - - - : - - <\code> - # invargent slide11.gadt -inform - - val min_binding : >n, a[1 > n]. Avl - (a, n) > a - - |<\hidden> - - - : compare two values of types as encoded - - <\small> - <\code> - datatype Ty : type - - datatype List : type - - datacons Zero : Int - - datacons Nil : >a. List a - - datacons TInt : Ty Int - - datacons TPair : >a, b. Ty a * Ty b - > Ty (a, b) - - datacons TList : >a. Ty a > - Ty (List a) - - external let eq_int : Int > Int - > Bool = "(=)" - - external let b_and : Bool > Bool - > Bool = "(&&)" - - external let b_not : Bool > Bool = "not" - - external forall2 : >a, b. (a > b - > Bool) > List a - > List b > Bool = "forall2" - - \; - - let rec equal1 = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal1 (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal1 (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal1 (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - - - Result: >a, b. (Ty a, Ty b) - > a > a > - Bool> - - <\exercise> - Find remaining three maximally general types of . - - |<\hidden> - > - - : - - <\code> - |]>> - - \; - - let rec equal = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - \ \ \| TInt, TList l -\> (function Nil -\> assert false) - - \ \ \| TList l, TInt -\> (fun _ -\> function Nil -\> assert false) - - - Result: - - <\code> - val equal : >a, b. (Ty a, Ty b) > a - > b > Bool - - |<\hidden> - Clause> - - : - - <\code> - |]>> - - let rec equal = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - test b_not (equal (TInt, TList TInt) zero Nil) - - - OCaml code generated -- : - - <\code> - |]>> - - let rec equal : type a b . ((a ty * b ty) -\> a -\> b -\> bool) = - - \ \ (function (TInt, TInt) -\> (fun x y -\> eq_int x y) - - \ \ \ \ \| (TPair (t1, t2), TPair (u1, u2)) -\> - - \ \ \ \ \ \ \ \ (fun ((x1, x2)) ((y1, y2)) -\> - - \ \ \ \ \ \ \ \ \ \ b_and (equal ((t1, u1)) x1 y1) (equal ((t2, u2)) x2 - y2)) - - \ \ \ \ \| (TList t, TList u) -\> forall2 (equal ((t, u))) - - \ \ \ \ \| _ -\> (fun _ _ -\> false)) - - let () = assert (b_not (equal ((TInt, TList TInt)) zero Nil)); () - - |<\hidden> - - - Chuan-kai Lin developed an efficient type inference algorithm for GADTs, - however in a type system restricted to so-called pointwise types. - - Toy example -- : - - <\code> - datatype Split : type * type - - datacons Whole : Split (Int, Int) - - datacons Parts : >a, b. Split ((Int, a), (b, Bool)) - - external let seven : Int = "7" - - external let three : Int = "3" - - \; - - let joint = function - - \ \ \| Whole -\> seven - - \ \ \| Parts -\> three, True - - - Needs non-default setting -- : - - <\code> - # invargent non_pointwise_split.gadt -inform -richer_answers - - val joint : >a. Split (a, a) > a - - - <\exercise> - Check that this is the correct type. - - |<\hidden> - - - A solution to at least one branch of implications, correspondingly of - pattern matching, must be implied by the conjunction of the premise and - the conclusion of the branch. I.e., some branch must be solvable without - arbitrary guessing. If solving a branch requires guessing, for some - ordering of branches, the solution to already solved branches must be a - good guess. - - : - - <\code> - datatype EquLR : type * type * type - - datacons EquL : >a, b. EquLR (a, a, b) - - datacons EquR : >a, b. EquLR (a, b, b) - - datatype Box : type - - datacons Cons : >a. a > Box a - - external let eq : >a. a > a - > Bool = "(=)" - - let vary = fun e y -\> - - \ \ match e with - - \ \ \| EquL, EquL -\> eq y "c" - - \ \ \| EquR, EquR -\> Cons (match y with True -\> 5 \| False -\> 7) - - - : - - <\code> - # invargent non_pointwise_vary.gadt -inform - - File "non_pointwise_vary.gadt", line 11, characters 18-60: - - No answer in type: term abduction failed - - - <\exercise> - Find a type or two for . Check that the type does not - meet the above requirement. - - |<\hidden> - > - - : - - <\code> - |]>> - - let rec add = fun x -\ efunction - - \ \ \| Empty -\ Node (Empty, x, Empty, 1) - - \ \ \| Node (l, y, r, h) -\ - - \ \ \ \ ematch compare x y, height l, height r with - - \ \ \ \ \| EQ, _, _ -\ Node (l, x, r, h) - - \ \ \ \ \| LT, hl, hr -\ - - \ \ \ \ \ \ let l' = add x l in - - \ \ \ \ \ \ (ematch height l' with - - \ \ \ \ \ \ \ \| hl' when hl' \= hr+2 -\ create l' y r - - \ \ \ \ \ \ \ \| hl' when hr+3 \= hl' -\ rotr (l', y, r)) - - \ \ \ \ \| GT, hl, hr -\ - - \ \ \ \ \ \ let r' = add x r in - - \ \ \ \ \ \ (ematch height r' with - - \ \ \ \ \ \ \ \| hr' when hr' \= hl+2 -\ create l y r' - - \ \ \ \ \ \ \ \| hr' when hl+3 \= hr' -\ rotl (l, y, r')) - - - Result: - - <\code> - val add : >a,n.a>Avl(a, - n)>>k[k > n+1 - > 1 > k > n > - k].Avl(a, k) - - |<\hidden> - > - - : - - <\code> - |]>> - - let rotr = efunction - - \ \ \ \ \| Empty, x, r -\ assert false - - \ \ \ \ \| Node (ll, lx, lr, hl), x, r -\ - - \ \ \ \ \ \ assert num 0 \= height r; \ - - \ \ \ \ \ \ assert type hl = height r + 3; - - \ \ \ \ \ \ (ematch height ll, height lr with - - \ \ \ \ \ \ \| m, n when n \= m -\ - - \ \ \ \ \ \ \ \ let r' = create lr x r in - - \ \ \ \ \ \ \ \ create ll lx r' - - \ \ \ \ \ \ \| m, n when m+1 \= n -\ - - \ \ \ \ \ \ \ \ (ematch lr with - - \ \ \ \ \ \ \ \ \| Empty -\ assert false - - \ \ \ \ \ \ \ \ \| Node (lrl, lrx, lrr, _) -\ - - \ \ \ \ \ \ \ \ \ \ let l' = create ll lx lrl in - - \ \ \ \ \ \ \ \ \ \ let r' = create lrr x r in - - \ \ \ \ \ \ \ \ \ \ create l' lrx r')) - - - Result: - - <\code> - val rotr : >a,n[0>n].(Avl(a,n+3),a,Avl(a,n))>>k[n+3>k>k>n+4].Avl(a,k) - - |<\hidden> - - - <\large> - <\theorem> - (expressions). - |\\ce:\|\>,\\ce:\>. - - - <\theorem> - (expressions). If - |)>=\> and - \\ce:\>, then there - exists an interpretation of predicate variables > such - that ,\\C\|\\ce:\|\>>. - - - |<\hidden> - - - <\itemize> - We use an extension of -- ``fully maximal'' is the restriction that we do not guess - facts not implied by premise and conclusion of a given implication. - - Without existential types, the problem in principle is caused by - the complexity of constraint abduction -- not known to be decidable. - Given a correct program with appropriate - clauses, and using an oracle for Simple Constraint Abduction, the - intended type scheme will ultimately be found. - - <\itemize> - This could be shown formally, but the proof is very tedious. - - - Without existential types, the problem in practice is that - although the restriction, when not imposed on all - branches but with accumulating the solution as discussed on slide 22, - seems sufficient for practical programs, fully maximal SCA is still - exponential in the size of input. - - With existential types, there are no guarantees. The intended - solution to the postconditions could be missed by the algorithm. - - <\itemize> - We have not yet found a definite, and practical, such - counterexample. - - - |<\hidden> - - - <\large> - |\>.A> is a - JCAQP>> answer (answer to a - .\\C|)>> - for model >) when: - - <\itemize> - is a conj. of atoms in ``solved form'', - - |\>#FV\C|)>|)>>, - - : \\\A\C|)>>, - - : \\|\>\.A>, - - : \\\|\>\|\>|)>.D\A>. - - - - <\ornamented> - - - |<\hidden> - - - <\large> - Answer |\>.A> to - SCAQP>> problem .D\C> - is when - - <\equation*> - \\|\>.D\A|)>\D\C. - - - - Nondeterministic algorithm for >: - - <\verbatim> - FMA(,): - - \ \ \ \ if C|)>> return > - - \ \ \ \ let be standard form of C> - - \ \ \ \ loop - - \ \ \ \ \ \ \ \ let > be > - - \ \ \ \ \ \ \ \ if A\\.A\D\C|)>> - return - - \ \ \ \ \ \ \ \ choose \> s.t. - D\C> - - - =\|S t|}>> - - > replaces terms at positions by a new - parameter. - |<\hidden> - - - <\itemize> - When solving multiple implications - \C|)>>, - keep a partial answer |\>.A>. - - To solve a particular implication - \C>, find - |\>.A> s.t. - |\>|\>.A\A> - is the SCAQP>> answer: - \|\>|\>.D\A\A|)>\D\C> - etc. - - <\itemize> - In the algorithm for > on previous slide, - the initial is still \C>, but - the implication checks are modified: we check - \A\D\C>, - A\D\C>. - - - In case of success, |\>.A=\|\>|\>.A\A>. - - A general way to deal with failure would be: try all permutations - ,\,i,\> - - In practice we need to give up sooner. - - <\itemize> - If branch \C> fails when - approached with partial answer |\>.A>, - \\>, restart from - \C> with - =\>. - - If branch \C> fails for - =\>, restart from the next unsolved branch (e.g. - \C>) with - =\> and put - \C> aside. - - Solve branches set aside after other branches. - - if solving an aside branch fails. - - - Backtracking: a discard list, aka. taboo list, of visited - answers. - - |<\hidden> - - - <\large> - To simplify the search in presence of a quantifier, we preprocess the - initial candidate by eliminating universally quantified variables: - - <\eqnarray*> - >,|\>,D,C|)>>||c\D\C,S=|\>\|\>|]>\|\>\\,\\D\|\>>|\>,\\\.S|\>\>|]>>|}>>>>> - - - - <\itemize> - We cannot use Herbrandization because it does not preserve - equivalence. - - <\itemize> - Herbrandization works for general abduction defined by logical - validity, but not for constraint abduction defined by validity in a - fixed model.\ - - - |<\shown> - - - <\itemize> - VincentSimonetFrancoisPottier. . , 29(1), JAN - 2007. - - MichaelMaherGeHuang. - . - IlianoCervesato, HelmutVeithAndreiVoronkov, - , 5330, - 421--435. Springer Berlin / Heidelberg, - 2008. - - M.Sulzmann, T.SchrijversP. - J.Stuckey. . - - Kenneth W.KnowlesCormacFlanagan. . , 4421, - 505--519. Springer, 2007. - - PeterBulychev, EgorKostylevVladimirZakharov. . AmirPnueli, IrinaVirbitskaiteAndreiVoronkov, - , - 5947, 413--423. Springer Berlin - / Heidelberg, 2010. - - KomeiFukuda, Thomas M.LieblingChristineLütolf. . . - - > - - - -> - -<\references> - <\collection> - > - > - - \ No newline at end of file diff --git a/doc/invargent-slides.pdf b/doc/invargent-slides.pdf deleted file mode 100644 index 184f03a..0000000 Binary files a/doc/invargent-slides.pdf and /dev/null differ diff --git a/doc/invargent-slides.tm b/doc/invargent-slides.tm deleted file mode 100644 index 88944e5..0000000 --- a/doc/invargent-slides.tm +++ /dev/null @@ -1,1055 +0,0 @@ - - - - -<\body> - - - - <\ornamented> - - - - <\itemize> - InvarGenT infers preconditions and invariants as types of - recursive definitions, and postconditions as existential types. - - Generalized Algebraic Data Types type system based - on François Pottier and Vincent Simonet's but without - type annotations. - - Extended to a language with existential types represented as - implicitly defined and used GADTs. - - Type inference problem as satisfaction of second order - constraints over a multi-sorted domain. - - Invariants found by , postconditions found by -- e.g. anti-unification for terms, extended convex hull. - - A numerical sort with linear equations and inequalities over - rationals, and >min>, - >max> relations (reconstructed - only for postconditions). - - |<\hidden> - - - <\really-tiny> - <\itemize> - |>|>||>>|0:\\\\|]>>>||1:\\\\|]>>>>>>>>|>>||p:\\\|\>\>|D,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p.e:\\\>>>>>>>>>||>|||>>|iC\p:\\\|C\p\p:\\\\\>>>|||x:\\\\|]>\|}>>>>>>>>|>>||D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\>>>>>>>>>|>>|i>|D\p:\\\>|\|\>|\>.\\\\\\\|\>|)>>||\>#FV>>>>>|C\K - p\p:\|\>|)>\\|\>\\\\|)>>>>>>>>>|>>||D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\>>>>>>>>>>>> - - |, added rules>>|||>||>||>>|p:\\\>>|\>\>>>>>|C\p:\\\>>>||p:\\\>>|\\\>>>>>|C\p:\\\>>>||p:\\\>>||\>#FV,\|)>>>>>>|\|\>.C\p:\\\>>>>>>>>|||>||>|||>>||,\\e:\\\>|>|,\\e:\>||)>>>>>>|C,\,\\e - e:\>>>||||\>|)>\>|C,\,\\e:\>>|,\\K - p.e:\\\>|>>>>|C,\,\\ - p=e - e:\>>>||||)>\\Dom|)>=\>>|,\\n:\>>>>>|C,\,\\e:\>>>>>>>>>>>> - - \; - - >|||>|>|>|>>|=\\|\>.D|]>.\>|D>>>>>|C,\\x:\>>>||\>>>>>|C,\\:\>>>|i - C,\\e:\C\D>>|\|\>|\>.\\\\\|\>|)>>>>>>|C,\\K - e\e:\|\>|)>>>>|\\|)> - e:\|C,\\ - p=e - e:\>>>>>>>>>|||>||>||||>>|\e:\\\>>|\e:\>>>>>|C,\\e - e:\>>>||\e:\>|\e:\>>|=\\|\>.D|]>.\>|=\\|}>>>>>>|C,\\ - x=e - e:\>>>||||i - C,\\c:\\\|C,\\\\c|)>:\\\>>>>>>>>>>>> - - | processing>>||||>||>||>>|D,\\e:\>>||\>#FV,C|)>>>>>>|C\\\|\>.D,\\e:\\|\>.D|]>.\>>>||\e:\|\>.\>>|D|\>\|\>|]>>>>>>|C,\\e:\|\>\|\>|]>>>>||\e:\>||\e:\>>>>>|C\D,\\e:\>>>>|>||>||>>|\e:\>>||\>#FV,\|)>>>>>>|\|\>.C,\\e:\>>>||\e:\>>|\>\>>>>>|C,\\e:\>>>||,\\e:\>>>>>>>>|||)>= - x=n|)> K x>>|K\\\l=\>>>||)>=x>>|>|>,\|)>=\|)>|\>|)>>>|>| - e,K|)>=n,K|)> - n,\|)>>>|>|>,\|)>=\|\>|)>>>|>|>,K|)>=\|)>|\>|)>>>|K\\>>>||)>=p.n|)>>>|>| - p=e - e,K|)>= - p=n,\|)> - n,K|)>>>|>>>>>>>>> - - - |<\hidden> - > - - <\equation*> - =\\|\>.D|]>.\>|D>>>>>|C,\\x:\> - - - <\equation*> - |\\x:\|\>=\\|\>.D|\>\\|\>|]>\\>\ - - - <\equation*> - \=\\|\>.D|]>.\,\|\>#FV,\|)> - - - : - - <\code> - datatype Tau - - external x : >b[b = Tau > Tau].b = - "x" - - \; - - let var_rule = x - - - : - - <\code> - # invargent slide3.gadt -inform - - val var_rule : Tau > Tau - - |<\hidden> - > - - <\equation*> - \e:\\\>>|\e:\>>>>>|C,\\e - e:\> - - - <\equation*> - |\\e - e:\|\>=\\.|\\e:\\\|\>\|\\e:\|\>,\#FV,\|)> - - - : - - <\code> - datatype Tau - - datatype Tau' - - datacons E2 : Tau' - - external e1 : Tau' > Tau = "e1" - - \; - - let app_rule = e1 E2 - - - : - - <\code> - # invargent slide4.gadt -inform - - val app_rule : Tau - - |<\hidden> - > - - <\equation*> - i C,\\c:\\\|C,\\\\c|)>:\\\>c=p.e - - - <\equation*> - |\\\>:\|\>=\\\.|\\>:\\\|\>\\\\>\,\\#FV,\|)> - - - <\equation*> - |p:\\\|\>\>|D,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p.e:\\\> - - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |||\\p.e:\\\|\>=|\p\\|\>\\|\>.D\|\\\e:\|\>>>>|>|x:\\\\|]>\|}>>>>>>>||gr-frame|>|||>>|||>>>>> - - : \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ or - \ K x:\\\|\>|\>\|}>> - - <\code> - let abs_gen_rules = fun x -\> x - - - : - - <\code> - # invargent slide5.gadt -inform - - val abs_gen_rules : >a. a > a - - - <\equation*> - \; - - - <\equation*> - \; - - |<\hidden> - > - - <\equation*> - i - C,\\e:\C\D>>|\|\>|\>.\\\\\|\>|)>>>>>>|C,\\K - e\e:\|\>|)>> - - - <\equation*> - |\\K - e\e:\|\>=\|\>|\>.(\|\\e:\|\>|\>\|\>|\>|]>|\>\D|\>|\>\|\>|\>|]>\\|\>|)>>\) - - - Type could be defined as:>> - - : - - <\code> - datatype Box : num - - datacons Small : >n,k [n > - 7> k = n+6]. Num n > Box k - - \; - - let gift = Small 4 - - let package = fun x -\> Small (x + -3) - - - : - - <\code> - # invargent slide6.gadt -inform - - val gift : Box 10 - - val package : >n[n > 10]. Num n - > Box (n + 3) - - |<\hidden> - > - - Height of left sibling, , differs by at most 2 from height of - the right sibling, . - - Resulting height is . Height value is stored with - the node. - - : - - <\code> - datatype Avl : type * num - - datacons Empty : >a. Avl (a, 0) - - datacons Node : - - \ \ >a,k,m,n [k=max(m,n) > - 0>m > 0>n - > n>m+2 > - m>n+2]. - - \ \ \ \ \ Avl (a, m) * a * Avl (a, n) * Num (k+1) - > Avl (a, k+1) - - \; - - let singleton = fun x -\> Node (Empty, x, Empty, 1) - - - : - - <\code> - # invargent slide7.gadt -inform - - val singleton : >a. a > Avl (a, 1) - - |<\hidden> - > - - <\equation*> - |D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\> - - - <\eqnarray*> - |\\p\m\n.e:\\\|\>>||\|\>.|\p\\|\>\\|\>.D\>>|||\|\\\m:Num|)>|\>\|\\\n:Num|)>|\>>>|e\\\\>||\\\\\|\\\e:\|\>|)>>>|\\\.|)>|)>>||\|\>\|\p\\|\>,|\>\|\>#FV,\,\|)>>>>> - - - : - - <\code> - datatype Signed : num - - datacons Pos : >n [0 > n]. Num n - > Signed n - - datacons Neg : >n [n > 0]. Num n - > Signed n - - let foo = function - - \ \ \| i when 7 \= i -\> Pos (i + -7) - - \ \ \| i when i \= 7 -\> Neg (i + -7) - - - Result: >n. Num (n + 7) - > Signed n> - |<\hidden> - > - - : - - <\code> - datatype Avl : type * num - - datacons Empty : >a. Avl (a, 0) - - datacons Node : - - \ \ >a,k,m,n [k=max(m,n) > - 0>m > 0>n - > n>m+2 > - m>n+2]. - - \ \ \ \ \ Avl (a, m) * a * Avl (a, n) * Num (k+1) - > Avl (a, k+1) - - \; - - let height = function - - \ \ \| Empty -\> 0 - - \ \ \| Node (_, _, _, k) -\> k - - \; - - let create = fun l x r -\> - - \ \ ematch height l, height r with - - \ \ \| i, j when j \= i -\> Node (l, x, r, i+1) - - \ \ \| i, j when i \= j -\> Node (l, x, r, j+1) - - - Result: - - <\code> - val height : >n, a. Avl (a, n) > - Num n - - val create : - - \ \ >k, n, a[k > n + 2 - > n > k + 2 > 0 - > k > 0 > n]. - - \ \ Avl (a, k) > a > Avl (a, n) - > >i[i=max (k + 1, n + 1)].Avl (a, - i) - - |<\hidden> - , > - - <\equation*> - |D,\\\m:Num>|)>>|\\\>|>|D,\\\n:Num>|)>>|\\.|)>|)>>|>|p:\\\|\>\>|D\\>\\\>\\>,\\\e:\>||\>#FV,\|)>>>>>>|C,\\p\m\n.e:\\\> - - - <\eqnarray*> - |\\p\m\n.e:\\\|\>>||\\|\>.|\p\\|\>\\|\>.D\>>|||\|\\\m:Num|)>|\>\|\\\n:Num|)>|\>>>|e=\\\>||\>\\\\\\|\\\e:\|\>|)>>>|\\.|)>|)>>||>|||\|\>\|\p\\|\>,|\>\\|\>#FV,\,\|)>>>>> - - - <\equation*> - |\>>>>>|C,\\:\> - - - In the solver, we assume for negation, that the numerical domain is - integers, while in general we take it to be rational numbers. - |<\hidden> - > - - : - - <\code> - datatype Avl : type * num - - datacons Empty : >a. Avl (a, 0) - - datacons Node : - - \ \ >a,k,m,n [k=max(m,n) > - 0>m > 0>n - > n>m+2 > - m>n+2]. - - \ \ \ \ \ Avl (a, m) * a * Avl (a, n) * Num (k+1) - > Avl (a, k+1) - - \; - - let rec min_binding = function - - \ \ \| Empty -\> assert false - - \ \ \| Node (Empty, x, r, _) -\> x - - \ \ \| Node ((Node (_,_,_,_) as l), x, r, _) -\> min_binding l - - - : - - <\code> - # invargent slide11.gadt -inform - - val min_binding : >n, a[1 > n]. Avl - (a, n) > a - - |<\hidden> - > - - <\equation*> - \e:\>|\e:\>>|=\\|\>.D|]>.\>|=\\|}>>>>>>|C,\\ - x=e e:\> - - - <\eqnarray*> - |\\x=ee:\|\>>||\|)>\|\\\|)>|]>.\|}>\e:\|\>|)>|)>\>>|||\.\|)>|)>\|\\\|)>|]>.\|}>\e:\|\>>>|||\#FV,\|)>,\#PV|)>>>>> - - - |)>> is a second order variable. - - : - - <\code> - datatype List : type * num - - datacons LNil : >a. List (a, 0) - - datacons LCons : >a, n [0>n]. a * - List (a, n) > List (a, n+1) - - \; - - let rec map = fun f -\> - - \ \ function LNil -\> LNil - - \ \ \ \ \| LCons (x, xs) -\> LCons (f x, map f xs) - - - Result: >n, a, b. (a - > b) > List (a, n) - > List (b, n)> - |<\hidden> - > - - : - - <\code> - datatype Binary : num - - datatype Carry : num - - datacons Zero : Binary 0 - - datacons PZero : >n [0>n]. Binary n - > Binary(2 n) - - datacons POne : >n [0>n]. Binary n - > Binary(2 n + 1) - - datacons CZero : Carry 0 - - datacons COne : Carry 1 - - \; - - let rec plus = - - \ \ function CZero -\> - - \ \ \ \ (function - - \ \ \ \ \ \ \| Zero -\> - - \ \ \ \ \ \ \ \ (function Zero -\> Zero |]>> - - \ \ \ \ \| COne -\> - - \ \ \ \ (function Zero -\> - - \ \ \ \ \ \ \ \ (function Zero -\> POne(Zero) - - \ \ \ \ \ \ \ \ \ \ \| PZero b1 -\> POne b1 - - \ \ \ \ \ \ \ \ \ \ \| POne b1 -\> PZero (plus COne Zero b1)) - |]>> - - - >i, k, n. Carry i - > Binary k > Binary n - > Binary (n + k + i)> - |<\hidden> - > - - <\equation*> - |,\\e:\\\>|>|,\\e:\>||)>>>>>>|C,\,\\e - e:\> - - - <\equation*> - |\\e - e:\|\>=\\.|\\e:\\\|\>\|\\e:\|\>\|)>,\#FV,\|)> - - - Above, |)>> means that - > is not an existential type. Therefore - fails: - - <\code> - datatype List : type * num - - datacons LNil : >a. List(a, 0) - - datacons LCons : >n, a [0>n]. a * - List(a, n) > List(a, n+1) - - let rec filter = fun f -\> - - \ \ efunction LNil -\> LNil - - \ \ \ \ \| LCons (x, xs) -\> - - \ \ \ \ \ \ ematch f x with - - \ \ \ \ \ \ \ \ \| True -\> LCons (x, filter f xs) - - \ \ \ \ \ \ \ \ \| False -\> filter f xs - - - : unfortunately, error not informative in current - implementation - - <\code> - ../invargent slide14.gadt -inform - - File "slide14.gadt", line 5, characters 2-134: - - No answer in type: term abduction failed - - |<\hidden> - - - : - - <\code> - datatype List : type * num - - datacons LNil : >a. List(a, 0) - - datacons LCons : >n, a [0>n]. a * - List(a, n) > List(a, n+1) - - \; - - let rec filter = fun f -\> - - \ \ efunction LNil -\> LNil - - \ \ \ \ \| LCons (x, xs) -\> - - \ \ \ \ \ \ ematch f x with - - \ \ \ \ \ \ \ \ \| True -\> - - \ \ \ \ \ \ \ \ \ \ let ys = filter f xs in - - \ \ \ \ \ \ \ \ \ \ LCons (x, ys) - - \ \ \ \ \ \ \ \ \| False -\> - - \ \ \ \ \ \ \ \ \ \ filter f xs - - - We use both and (a - >-redex for ), because - and would require the types of - branch bodies to be equal: to be lists of the same length. - - <\code> - val filter : - - \ \ >n, a. - - \ \ (a > Bool) > List (a, n) - > >k[0 > k - > k > n].List (a, k) - - |<\hidden> - > - - <\equation*> - ||\>|)>\>|C,\,\\e:\>>|,\\K - p.e:\\\>|>>>>|C,\,\\ - p=e e:\> - - - <\eqnarray*> - |\\ - p=e - e:\|\>>||\.|\\e:\|\>\>>||||\\p.e:\\\|\>\|)>\\>|\\K - p.e:\\\|\>|)>>>|||\=K\\|\>|\>.\\\|\>|)>\\|}>>>>> - - - <\small> - OCaml code generated for -- : - - <\code> - type _ list = - - \ \ \| LNil : (*>'a.*) ('a (* 0 *)) list - - \ \ \| LCons : (*>'n, 'a[0 > - n].*)'a * ('a (* n *)) list -\ - - \ \ \ \ ('a (* n + 1 *)) list - - = - - \ \ \| Ex2 : (*>'k, 'n, 'a[0 > k - > k > n].*)('a (* k *)) list - -\ - - \ \ \ \ ((* n,*) 'a) ex2 - - let rec filter : - - \ \ type (*n*) a . (((a -\> bool)) -\> (a (* n *)) list -\> ((* n,*) - a) ex2) = - - \ \ (fun f -\> - - \ \ \ \ (function LNil -\> let xcase = LNil in Ex2 xcase - - \ \ \ \ \ \ \| LCons (x, xs) -\> - - \ \ \ \ \ \ \ \ \ \ (if f x then - - \ \ \ \ \ \ \ \ \ \ in let - xcase = LCons (x, ys) in Ex2 xcase - - \ \ \ \ \ \ \ \ \ \ else let Ex2 xcase = filter f xs in Ex2 xcase))) - - - |<\hidden> - - - : compare two values of types as encoded - - <\small> - <\code> - datatype Ty : type - - datatype List : type - - datacons Zero : Int - - datacons Nil : >a. List a - - datacons TInt : Ty Int - - datacons TPair : >a, b. Ty a * Ty b - > Ty (a, b) - - datacons TList : >a. Ty a > - Ty (List a) - - external let eq_int : Int > Int - > Bool = "(=)" - - external let b_and : Bool > Bool - > Bool = "(&&)" - - external let b_not : Bool > Bool = "not" - - external forall2 : >a, b. (a > b - > Bool) > List a - > List b > Bool = "forall2" - - \; - - let rec equal1 = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal1 (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal1 (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal1 (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - - - Result: >a, b. (Ty a, Ty b) - > a > a > - Bool> - - <\exercise> - Find remaining three maximally general types of . - - |<\hidden> - > - - : - - <\code> - |]>> - - \; - - let rec equal = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - \ \ \| TInt, TList l -\> (function Nil -\> assert false) - - \ \ \| TList l, TInt -\> (fun _ -\> function Nil -\> assert false) - - - Result: - - <\code> - val equal : >a, b. (Ty a, Ty b) > a - > b > Bool - - |<\hidden> - Clause> - - : - - <\code> - |]>> - - let rec equal = function - - \ \ \| TInt, TInt -\> fun x y -\> eq_int x y - - \ \ \| TPair (t1, t2), TPair (u1, u2) -\> \ - - \ \ \ \ (fun (x1, x2) (y1, y2) -\> - - \ \ \ \ \ \ \ \ b_and (equal (t1, u1) x1 y1) - - \ \ \ \ \ \ \ \ \ \ \ \ \ \ (equal (t2, u2) x2 y2)) - - \ \ \| TList t, TList u -\> forall2 (equal (t, u)) - - \ \ \| _ -\> fun _ _ -\> False - - test b_not (equal (TInt, TList TInt) zero Nil) - - - OCaml code generated -- : - - <\code> - |]>> - - let rec equal : type a b . ((a ty * b ty) -\> a -\> b -\> bool) = - - \ \ (function (TInt, TInt) -\> (fun x y -\> eq_int x y) - - \ \ \ \ \| (TPair (t1, t2), TPair (u1, u2)) -\> - - \ \ \ \ \ \ \ \ (fun ((x1, x2)) ((y1, y2)) -\> - - \ \ \ \ \ \ \ \ \ \ b_and (equal ((t1, u1)) x1 y1) (equal ((t2, u2)) x2 - y2)) - - \ \ \ \ \| (TList t, TList u) -\> forall2 (equal ((t, u))) - - \ \ \ \ \| _ -\> (fun _ _ -\> false)) - - let () = assert (b_not (equal ((TInt, TList TInt)) zero Nil)); () - - |<\hidden> - - - Chuan-kai Lin developed an efficient type inference algorithm for GADTs, - however in a type system restricted to so-called pointwise types. - - Toy example -- : - - <\code> - datatype Split : type * type - - datacons Whole : Split (Int, Int) - - datacons Parts : >a, b. Split ((Int, a), (b, Bool)) - - external let seven : Int = "7" - - external let three : Int = "3" - - \; - - let joint = function - - \ \ \| Whole -\> seven - - \ \ \| Parts -\> three, True - - - Needs non-default setting -- : - - <\code> - # invargent non_pointwise_split.gadt -inform -richer_answers - - val joint : >a. Split (a, a) > a - - - <\exercise> - Check that this is the correct type. - - |<\hidden> - - - <\small> - Chuan-kai Lin's system needs a workaround, InvarGenT works with def. - settings -- : - - <\code> - (** Normally we would use [num], but this is a stress test for - [type]. *) - - datatype Z - - datatype S : type - - datatype Balance : type * type * type - - datacons Less : >a. Balance (a, S a, S a) - - datacons Same : >a. Balance (a, a, a) - - datacons More : >a. Balance (S a, a, S a) - - datatype AVL : type - - datacons Leaf : AVL Z - - datacons Node : - - \ \ >a, b, c. Balance (a, b, c) * AVL a * Int * AVL b - > AVL (S c) - - \; - - datatype Choice : type * type - - datacons Left : >a, b. a > - Choice (a, b) - - datacons Right : >a, b. b > - Choice (a, b) - - \; - - let rotr = fun z d -\> function - - \ \ \| Leaf -\> assert false - - \ \ \| Node (Less, a, x, Leaf) -\> assert false - - \ \ \| Node (Same, a, x, (Node (_,_,_,_) as b)) -\> - - \ \ \ \ Right (Node (Less, a, x, Node (More, b, z, d))) - |]>> - - - Result: >a.Int > AVL a - > AVL (S (S a)) > Choice (AVL - (S (S a)), AVL (S (S (S a))))> - - |<\hidden> - - - A solution to at least one branch of implications, correspondingly of - pattern matching, must be implied by the conjunction of the premise and - the conclusion of the branch. I.e., some branch must be solvable without - arbitrary guessing. If solving a branch requires guessing, for some - ordering of branches, the solution to already solved branches must be a - good guess. - - : - - <\code> - datatype EquLR : type * type * type - - datacons EquL : >a, b. EquLR (a, a, b) - - datacons EquR : >a, b. EquLR (a, b, b) - - datatype Box : type - - datacons Cons : >a. a > Box a - - external let eq : >a. a > a - > Bool = "(=)" - - let vary = fun e y -\> - - \ \ match e with - - \ \ \| EquL, EquL -\> eq y "c" - - \ \ \| EquR, EquR -\> Cons (match y with True -\> 5 \| False -\> 7) - - - : - - <\code> - # invargent non_pointwise_vary.gadt -inform - - File "non_pointwise_vary.gadt", line 11, characters 18-60: - - No answer in type: term abduction failed - - - <\exercise> - Find a type or two for . Check that the type does not - meet the above requirement. - - |<\hidden> - - - <\large> - <\theorem> - (expressions). - |\\ce:\|\>,\\ce:\>. - - - <\theorem> - (expressions). If - |)>=\> and - \\ce:\>, then there - exists an interpretation of predicate variables > such - that ,C\|\\ce:\|\>>. - - - |<\shown> - - - <\itemize> - We use an extension of -- ``fully maximal'' is the restriction that we do not guess - facts not implied by premise and conclusion of a given implication. - - Without existential types, the problem in principle is caused by - the complexity of constraint abduction -- not known to be decidable. - Given a correct program with appropriate - clauses, and using an oracle for Simple Constraint Abduction, the - intended type scheme will ultimately be found. - - <\itemize> - This could be shown formally, but the proof is very tedious. - - - Without existential types, the problem in practice is that - although the restriction, when not imposed on all - branches but with accumulating the solution as discussed on slide 22, - seems sufficient for practical programs, fully maximal SCA is still - exponential in the size of input. - - With existential types, there are no guarantees. The intended - solution to the postconditions could be missed by the algorithm. - - <\itemize> - We have not yet found a definite, and practical, such - counterexample. - - - > - - - -> - -<\references> - <\collection> - > - > - - \ No newline at end of file diff --git a/doc/invargent.pdf b/doc/invargent.pdf index c2cf2a2..3769f09 100644 Binary files a/doc/invargent.pdf and b/doc/invargent.pdf differ