"safe clone": by default, cloned axioms become lemmas

Clone "with axiom ." or "with goal ." to change the default
("with lemma ." is also accepted, just in case).

examples/avl/avl.mlw

@@ -69,14 +69,15 @@ module AVL
       the sequence. In other words, `M.sum f [a_1;...;a_n]` is the
       monoidal summary of sequence `[a_1;...;a_n]` with respect to
       measure `f`. *)
-  clone monoid.ComputableMonoid as M
+  clone monoid.ComputableMonoid as M with axiom .
   clone monoid.MonoidSum as M with
     (* scope M = M *)
     type M.t = M.t,
     constant M.zero = M.zero,
     function M.op = M.op,
     goal M.assoc,
-    goal M.neutral
+    goal M.neutral,
+    axiom .
 
   (** Abstract description of the data stored in the tree:
       measurable elements. *)

examples/avl/monoid.mlw

@@ -24,7 +24,7 @@ end
 module MonoidSum
 
   use import seq.Seq
-  clone import Monoid as M
+  clone import Monoid as M with axiom .
 
   function agg (f:'a -> t) (s:seq 'a) : t
   axiom agg_empty : forall f:'a -> t. agg f empty = zero
@@ -42,7 +42,7 @@ module MonoidSumDef
   use import seq.FreeMonoid
 
   (* TODO: do that refinement correctly ! *)
-  clone import Monoid as M
+  clone import Monoid as M with axiom .
 
   let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t
     variant { length s }
@@ -70,7 +70,7 @@ end
 (** {2 Computable monoid} *)
 module ComputableMonoid
 
-  clone export Monoid
+  clone export Monoid with axiom .
 
   (** Abstract routines computing operations in the monoid. *)
   val zero () : t ensures { result = zero }

examples/avl/preorder.mlw

@@ -8,7 +8,7 @@ theory Full
   (** Standard preorder theory. *)
   type t
   predicate le t t
-  clone export relations.PreOrder with type t = t, predicate rel = le
+  clone export relations.PreOrder with type t = t, predicate rel = le, axiom .
   (** Definable symbols for equality and strict ordering. *)
   predicate eq t t
   axiom eq_def : forall x y. eq x y <-> le x y /\ le y x
@@ -28,10 +28,9 @@ end
 (** {2 Total preorder} *)
 theory TotalFull
 
-  clone export Full
-  clone export relations.Total with type t = t, predicate rel = le
-  clone relations.Total as Lt with type t = t,
-    predicate rel = le, goal Total
+  clone export Full with axiom .
+  clone export relations.Total with type t = t, predicate rel = le, axiom Total
+  clone relations.Total as Lt with type t = t, predicate rel = le, goal Total
   lemma lt_def2 : forall x y. lt x y <-> not le y x
 
 end
@@ -40,7 +39,7 @@ end
 module Computable
 
   use import int.Int
-  clone export TotalFull
+  clone export TotalFull with axiom .
 
   (** Comparison is computable. *)
   val compare (x y:t) : int

examples/avl/priority_queue.mlw

@@ -24,7 +24,7 @@ module PQueue
   scope D type t 'a end
   scope K type t end
   clone export key_type.KeyType with type t = D.t, type key = K.t
-  clone preorder.Computable as CO with type t = K.t
+  clone preorder.Computable as CO with type t = K.t, axiom .
 
   (** {2 Instantiation of the AVL tree module} *)
 

examples/avl/tables.mlw

@@ -24,7 +24,7 @@ module MapBase
   (** Stored elements are identified by totally ordered keys *)
   scope D type t 'a end scope K type t end
   clone export key_type.KeyType with type t = D.t, type key = K.t
-  clone preorder.Computable as CO with type t = K.t
+  clone preorder.Computable as CO with type t = K.t, axiom .
   scope D
     let function measure 'a : unit = ()
   end
@@ -512,7 +512,7 @@ module Map
 
   (** Parameter: key type with computable total preorder. *)
   scope K type t end
-  clone preorder.Computable as CO with type t = K.t
+  clone preorder.Computable as CO with type t = K.t, axiom .
 
   (** Elements are key-value pairs *)
   scope D
@@ -711,7 +711,7 @@ module Set
 
   (** Parameter: comparable elements. *)
   scope K type t end
-  clone preorder.Computable as CO with type t = K.t
+  clone preorder.Computable as CO with type t = K.t, axiom .
 
   (** Elements are themselves the keys. *)
   scope D

examples/binomial_heap.mlw

@@ -20,7 +20,7 @@ module BinomialHeap
   type elt
 
   val predicate le elt elt
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom .
 
   (** Trees.
 

examples/bitvectors/bitvector.why

@@ -358,7 +358,7 @@ theory BV32
 
   function size : int = 32
 
-  clone export BitVector with function size, lemma size_positive
+  clone export BitVector with function size, lemma size_positive, axiom .
 
 end
 
@@ -367,7 +367,7 @@ theory BV64
 
   function size : int = 64
 
-  clone export BitVector with function size, lemma size_positive
+  clone export BitVector with function size, lemma size_positive, axiom .
 
 end
 

examples/braun_trees.mlw

@@ -26,7 +26,7 @@ module BraunHeaps
 
   val predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom .
 
   (* [e] is no greater than the root of [t], if any *)
   let predicate le_root (e: elt) (t: tree elt) = match t with

examples/bts/13375.mlw

@@ -37,7 +37,7 @@ module Spec
  type my_type
 
  clone Signed as My_Type_T
-   with type signed_type = my_type
+   with type signed_type = my_type, axiom .
  axiom axiom_first :
   My_Type_T.first = 1
 

examples/check-builtin/ac.why

 theory Test
        type t
        function f t t : t
-       clone algebra.AC with type t = t, function op = f
+       clone algebra.AC with type t = t, function op = f, axiom .
        goal G1 : forall x y : t. f x y = f y x
        goal G2 : forall x y z : t. f (f x y) z = f x (f y z)
 end

examples/coincidence_count_list.mlw

@@ -60,7 +60,7 @@ module CoincidenceCountAnyType
     ensures { result <-> x = y }
   val predicate rel (x y : t)
 
-  clone import relations.TotalStrictOrder with type t, predicate rel
+  clone import relations.TotalStrictOrder with type t, predicate rel, axiom .
 
   clone export list.Sorted
      with type t = t, predicate le = rel, goal Transitive.Trans

examples/fibonacci.mlw

@@ -280,7 +280,8 @@ theory Mat22
   clone export
     int.Exponentiation with
       type t = t, function one = id, function (*) = mult,
-      goal Assoc, goal Unit_def_l, goal Unit_def_r
+      goal Assoc, goal Unit_def_l, goal Unit_def_r,
+      axiom . (* FIXME: replace with "goal" and prove *)
 
 end
 

examples/finite_tarski.mlw

@@ -11,7 +11,7 @@ Authors:  Martin Clochard
 module Tarski
 
   use import set.Fset
-  clone export relations.PartialOrder
+  clone export relations.PartialOrder with axiom .
 
   constant a : set t
 
@@ -28,7 +28,7 @@ end
 
 module Tarski_rec
   use import set.Fset
-  clone export Tarski
+  clone export Tarski with axiom .
 
   let lemma least_fix_point () : unit
    ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
@@ -45,7 +45,7 @@ end
 
 module Tarski_while
   use import set.Fset
-  clone export Tarski
+  clone export Tarski with axiom .
   use import ref.Ref
 
   let lemma least_fix_point () : unit

examples/insertion_sort_list.mlw

@@ -6,9 +6,10 @@ module InsertionSort
   type elt
   val predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le,
-   goal Transitive.Trans
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
+  clone export list.Sorted with
+    type t = elt, predicate le  = le, goal Transitive.Trans
 
   use import list.List
   use import list.Permut

examples/leftist_heap.mlw

@@ -14,7 +14,8 @@ module Heap
   type elt
   predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   type heap
 
@@ -103,7 +104,8 @@ module LeftistHeap
 
   type elt
   val predicate le elt elt
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   use import TreeRank
   use export Size

examples/linear_probing.mlw

@@ -30,7 +30,7 @@ end
 
 module LinearProbing
 
-  clone import HashedTypeWithDummy
+  clone import HashedTypeWithDummy with axiom .
 
   use import int.Int
   use import int.ComputerDivision

examples/logic/einstein.why

@@ -33,14 +33,14 @@ theory Einstein
 
   (** Each house is associated bijectively to a color and a person *)
 
-  clone Bijection as Color with type t = house, type u = color
-  clone Bijection as Owner with type t = house, type u = person
+  clone Bijection as Color with type t = house, type u = color, axiom .
+  clone Bijection as Owner with type t = house, type u = person, axiom .
 
   (** Each drink, cigar brand and pet are associated bijectively to a person *)
 
-  clone Bijection as Drink with type t = person, type u = drink
-  clone Bijection as Cigar with type t = person, type u = cigar
-  clone Bijection as Pet   with type t = person, type u = pet
+  clone Bijection as Drink with type t = person, type u = drink, axiom .
+  clone Bijection as Cigar with type t = person, type u = cigar, axiom .
+  clone Bijection as Pet   with type t = person, type u = pet, axiom .
 
   (** Relative positions of the houses *)
 

examples/logic/sorted_list.why

@@ -19,7 +19,7 @@ end
 
 theory SortedList
   use import List
-  clone import Order as O
+  clone import Order as O with axiom .
 
   inductive sorted (l : list t) =
     | sorted_nil :

examples/max_matrix.mlw

@@ -91,7 +91,7 @@ module MaxMatrixMemo
   use import Bitset
   use map.Map
 
-  clone import appmap.Appmap with type key = int
+  clone import appmap.Appmap with type key = int, axiom .
 
   val constant n : int
     ensures { 0 <= result <= size }
@@ -108,7 +108,7 @@ module MaxMatrixMemo
   predicate permutation (s: mapii) = solution s 0
 
   function f (s: mapii) (i: int) : int = m[i][Map.get s i]
-  clone import sum.Sum with type container = mapii, function f = f
+  clone import sum.Sum with type container = mapii, function f = f, axiom .
 
   lemma sum_ind:
     forall i: int. i < n -> forall j: int.

examples/mergesort_array.mlw

@@ -15,9 +15,11 @@ module Elt
 
   val predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
-  clone export array.Sorted with type elt = elt, predicate le = le
+  clone export array.Sorted with type
+    elt = elt, predicate le = le, axiom .
 
 end
 
@@ -30,7 +32,7 @@ end
 
 module Merge
 
-  clone export Elt
+  clone export Elt with axiom .
   use export ref.Refint
   use export array.Array
   use import map.Occ
@@ -94,7 +96,7 @@ end
 
 module TopDownMergesort
 
-  clone import Merge
+  clone import Merge with axiom .
   use import mach.int.Int
 
   let rec mergesort_rec (a tmp: array elt) (l r: int) : unit
@@ -131,7 +133,7 @@ end
 
 module BottomUpMergesort
 
-  clone import Merge
+  clone import Merge with axiom .
   use import mach.int.Int
   use import int.MinMax
 
@@ -207,7 +209,7 @@ end
 
 module NaturalMergesort
 
-  clone import Merge
+  clone import Merge with axiom .
   use import mach.int.Int
   use import int.MinMax
 

examples/mergesort_list.mlw

@@ -14,9 +14,10 @@ module Elt
 
   type elt
   val predicate le elt elt
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le,
-  goal Transitive.Trans
+  clone relations.TotalPreOrder
+    with type t = elt, predicate rel = le, axiom .
+  clone export list.Sorted with
+    type t = elt, predicate le  = le, goal Transitive.Trans
 
 end
 
@@ -24,7 +25,7 @@ end
 
 module Merge (* : MergeSpec *)
 
-  clone export Elt
+  clone export Elt with axiom .
 
   let rec merge (l1 l2: list elt) : list elt
     requires { sorted l1 /\ sorted l2 }
@@ -44,7 +45,7 @@ end
 
 module EfficientMerge (* : MergeSpec *)
 
-  clone export Elt
+  clone export Elt with axiom .
   use import list.Mem
   use import list.Reverse
   use import list.RevAppend
@@ -84,7 +85,7 @@ end
 
 module Mergesort
 
-  clone import Merge (* or EfficientMerge *)
+  clone import Merge (* or EfficientMerge *) with axiom .
 
   let split (l0: list 'a) : (list 'a, list 'a)
     requires { length l0 >= 2 }
@@ -132,7 +133,7 @@ end
 
 module OCamlMergesort
 
-  clone export Elt
+  clone export Elt with axiom .
   use import list.Mem
   use import list.Reverse
   use import list.RevAppend

examples/mergesort_queue.mlw

@@ -15,9 +15,10 @@ module MergesortQueue
 
   type elt
   val predicate le elt elt
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
-  clone export list.Sorted      with type t = elt, predicate le  = le,
-  goal Transitive.Trans
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
+  clone export list.Sorted with
+    type t = elt, predicate le  = le, goal Transitive.Trans
 
   let merge (q1: t elt) (q2: t elt) (q: t elt)
     requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }

examples/multiprecision/lineardecision.mlw

@@ -2,13 +2,17 @@ module LinearEquationsCoeffs
 
 type a
 function (+) a a : a
-function ( *) a a : a
+function (*) a a : a
 function (-_) a : a
 function azero: a
 function aone: a
 predicate ale a a
 
-clone algebra.OrderedUnitaryCommutativeRing as A with type t = a, function (+) = (+), function ( *) = ( *), function (-_) = (-_), constant zero = azero, constant one=aone, predicate (<=) = ale
+clone algebra.OrderedUnitaryCommutativeRing as A with
+  type t = a, function (+) = (+), function (*) = (*),
+  function (-_) = (-_), constant zero = azero,
+  constant one=aone, predicate (<=) = ale,
+  axiom .
 
 function (-) a a : a
 
@@ -57,7 +61,7 @@ module LinearEquationsDecision
 use import int.Int
 type coeff
 
-clone LinearEquationsCoeffs as C with type t = coeff
+clone LinearEquationsCoeffs as C with type t = coeff, axiom .
 type vars = C.vars
 
 type expr = Term coeff int | Add expr expr | Cst coeff
@@ -80,7 +84,7 @@ let rec predicate expr_bound (e:expr) (b:int)
 
 function interp (e:expr) (y:vars) (z:C.cvars) : C.a
 = match e with
-  | Term c v -> C.( *) (C.interp c z) (y v)
+  | Term c v -> C.(*) (C.interp c z) (y v)
   | Add e1 e2 -> C.(+) (interp e1 y z) (interp e2 y z)
   | Cst c -> C.interp c z
   end
@@ -262,9 +266,9 @@ let rec opp_expr (e:expr) : expr
   | Term c j ->
     let oc = C.opp c in
     let r = Term oc j in
-    assert { forall y z. interp r y z = C.( *) (C.interp oc z) (y j)
-             = C.( *) (C.(-_) (C.interp c z)) (y j)
-             = C.(-_) (C.( *) (C.interp c z) (y j))
+    assert { forall y z. interp r y z = C.(*) (C.interp oc z) (y j)
+             = C.(*) (C.(-_) (C.interp c z)) (y j)
+             = C.(-_) (C.(*) (C.interp c z) (y j))
              = C.(-_) (interp e y z) };
     r
   | Add e1 e2 ->
@@ -353,7 +357,7 @@ let rec lemma interp_ctx_wl (ctx l: context) (g:equality)
 
 let rec mul_expr (e:expr) (c:coeff) : expr
   ensures { forall y z. interp result y z
-            = C.( *) (C.interp c z) (interp e y z) }
+            = C.(*) (C.interp c z) (interp e y z) }
   ensures { valid_expr e -> valid_expr result }
   variant { e }
   raises  { C.Unknown -> true }
@@ -475,9 +479,9 @@ let sub_expr (e1 e2:expr)
            let v2 = interp e2 y z in
            let vr = interp r y z in
            C.(+) vr v2 = v1
-           by C.( *) v2 (C.(-_) C.aone) = C.(-_) v2
+           by C.(*) v2 (C.(-_) C.aone) = C.(-_) v2
            so C.(+) vr v2
-           = C.(+) (C.(+) v1 (C.( *) v2 (C.(-_) C.aone))) v2
+           = C.(+) (C.(+) v1 (C.(*) v2 (C.(-_) C.aone))) v2
            = C.(+) (C.(+) v1 (C.(-_) v2)) v2 = v1 };
   r
 
@@ -982,7 +986,8 @@ use import RationalCoeffs
 use import real.RealInfix
 use import real.FromInt
 
-clone export LinearEquationsDecision with type  C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
+clone export LinearEquationsDecision with type  C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 end
 
@@ -1027,7 +1032,8 @@ let iinv (t:t') : t'
   raises { NError -> true }
 = raise NError
 
-clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
+clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 
 use import real.FromInt
@@ -1398,7 +1404,8 @@ use import real.RealInfix
 
 type coeff = t
 
-clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
+clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.(*) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 end
 module LinearDecisionIntMP
@@ -1448,7 +1455,8 @@ let mpinv (a:t) : t
 = raise MPError
 
 
-clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
+clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 use LinearDecisionRationalMP as R
 use import real.FromInt
@@ -2056,4 +2064,4 @@ goal g:
      forall a: value.
      ((forall x. forall y. foo (add x (add (add a dummy) y))) = True)
 
-end
\ No newline at end of file
+end

examples/pairing_heap.mlw

@@ -14,7 +14,8 @@ module Heap
   type elt
   val predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   type heap
 
@@ -162,7 +163,8 @@ module PairingHeap
   use import list.Length
 
   val predicate le elt elt
-  clone import relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone import relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   (* [e] is no greater than the root of [h], if any *)
   predicate le_root (e: elt) (h: heap) = match h with
@@ -304,4 +306,4 @@ module PairingHeap
        merge_pairs l
     end
 
-end
\ No newline at end of file
+end

examples/pairing_heap_bin.mlw

@@ -14,7 +14,8 @@ module Heap
   type elt
   val predicate le elt elt
 
-  clone relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   type heap
 
@@ -131,7 +132,8 @@ module PairingHeap
   use import Occ
 
   val predicate le elt elt
-  clone import relations.TotalPreOrder with type t = elt, predicate rel = le
+  clone import relations.TotalPreOrder with
+    type t = elt, predicate rel = le, axiom .
 
   predicate le_root (e: elt) (h: heap) = match h with
     | E -> true

examples/ring_decision/ringdecision.mlw

 module UnitaryCommutativeRingDecision
 
-clone algebra.UnitaryCommutativeRing as C
+clone algebra.UnitaryCommutativeRing as C with axiom .
 
-clone algebra.UnitaryCommutativeRing as Z
+clone algebra.UnitaryCommutativeRing as Z with axiom .
 
 function morph Z.t : C.t
 
 axiom morph_zero: morph Z.zero = C.zero
 axiom morph_one: morph Z.one = C.one
 axiom morph_add: forall z1 z2:Z.t. morph (Z.(+) z1 z2) = C.(+) (morph z1) (morph z2)
-axiom morph_mul: forall z1 z2:Z.t. morph (Z.( *) z1 z2)
-                                   = C.( *) (morph z1) (morph z2)
+axiom morph_mul: forall z1 z2:Z.t. morph (Z.(*) z1 z2)
+                                   = C.(*) (morph z1) (morph z2)
 axiom morph_inv: forall z:Z.t. morph (Z.(-_) z) = C.(-_) (morph z)
 
 val predicate eq0 (x:Z.t) ensures { result <-> x = Z.zero }
@@ -26,7 +26,7 @@ function interp (x:t) (y:vars) : C.t =
   match x with
   | Var n -> y n
   | Add x1 x2 -> C.(+) (interp x1 y) (interp x2 y)
-  | Mul x1 x2 -> C.( *) (interp x1 y) (interp x2 y)
+  | Mul x1 x2 -> C.(*) (interp x1 y) (interp x2 y)
   | Cst c -> morph c end
 
 predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y
@@ -39,12 +39,12 @@ type t' = list m (* sum of monomials *)
 function mon (x:list int) (y:vars) : C.t =
   match x with
   | Nil -> C.one
-  | Cons x r -> C.( *) (y x) (mon r y) end
+  | Cons x r -> C.(*) (y x) (mon r y) end
 
 function interp' (x:t') (y:vars) : C.t =
   match x with
   | Nil -> C.zero
-  | Cons (M a m) r -> C.(+) (C.( *) (morph a) (mon m y)) (interp' r y) end
+  | Cons (M a m) r -> C.(+) (C.(*) (morph a) (mon m y)) (interp' r y) end
 
 predicate eq_mon (m1 m2: list int) = forall y: vars. mon m1 y = mon m2 y
 predicate eq' (x1 x2: t') = forall y: vars. interp' x1 y = interp' x2 y
@@ -53,7 +53,7 @@ use import list.Append
 use import list.Length
 
 let rec lemma mon_append (x1 x2: list int) (y:vars)
-  ensures { mon (x1 ++ x2) y = C.( *) (mon x1 y) (mon x2 y) }
+  ensures { mon (x1 ++ x2) y = C.(*) (mon x1 y) (mon x2 y) }
   variant { x1 }
 =
   match x1 with Nil -> () | Cons _ x -> mon_append x x2 y end
@@ -72,12 +72,12 @@ let rec lemma interp_sum (x1 x2:t') (y:vars)
 
 let ghost function append_mon (m1 m2:m)
   ensures { forall y. interp' (Cons result Nil) y
-              = C.( *) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) }
-= match m1,m2 with M a1 l1, M a2 l2 -> M (Z.( *) a1 a2) (l1 ++ l2) end
+              = C.(*) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) }
+= match m1,m2 with M a1 l1, M a2 l2 -> M (Z.(*) a1 a2) (l1 ++ l2) end
 
 let rec ghost function mul_mon (x:t') (mon:m) : t'
   ensures { forall y.
-            interp' result y = C.( *) (interp' x y) (interp' (Cons mon Nil) y) }
+            interp' result y = C.(*) (interp' x y) (interp' (Cons mon Nil) y) }
 = match x with
   | Nil -> Nil
   | Cons m r ->
@@ -87,7 +87,7 @@ let rec ghost function mul_mon (x:t') (mon:m) : t'
 end
 
 let rec ghost function mul_devel (x1 x2:t') : t'
-  ensures { forall y. interp' result y = C.( *) (interp' x1 y) (interp' x2 y) } =
+  ensures { forall y. interp' result y = C.(*) (interp' x1 y) (interp' x2 y) } =
   match x1 with
   | Nil -> Nil
   | Cons (M a m) r -> (mul_mon x2 (M a m)) ++ (mul_devel r x2)
@@ -211,7 +211,8 @@ function id (x:int) : int = x
 let predicate eq0_int (x:int) = x = 0
 
 
-clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.(*) = (*), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.(*) = (*), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int
+clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.(*) = (*), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.(*) = (*), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 meta "compute_max_steps" 0x10000000
 
@@ -226,10 +227,10 @@ type r
 type a
 
 function (+) a a : a
-function ( *) a a : a
+function (*) a a : a
 
-clone algebra.UnitaryCommutativeRing as R with type t = r
-clone algebra.Ring as A with type t = a, function (+) = (+), function (*) = (*)
+clone algebra.UnitaryCommutativeRing as R with type t = r, axiom .
+clone algebra.Ring as A with type t = a, function (+) = (+), function (*) = (*), axiom .
 constant one : a
 constant zero : a = A.zero
 axiom AUnitary : forall x:a. one * x = x * one = x
@@ -242,7 +243,7 @@ val function ($) r a : a
 
 axiom ExtDistSumA : forall r: r, x y: a. r $ (x + y) = r $ x + r $ y
 axiom ExtDistSumR : forall r s: r, x: a. (R.(+) r s)$x = r$x + s$x
-axiom AssocMulExt : forall r s: r, x: a. (R.( *) r s)$x = r$(s$x)
+axiom AssocMulExt : forall r s: r, x: a. (R.(*) r s)$x = r$(s$x)
 axiom UnitExt     : forall x: a.         R.one $ x = x
 axiom CommMulExt  : forall r: r, x y: a. r$(x*y) = (r$x)*y = x*(r$y)
 
@@ -272,7 +273,7 @@ val function aplus a a : a
 val function atimes a a : a
 val function aopp a : a
 
-clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.( *) = rtimes, function R.(-_) = ropp, function (+) = aplus, function ( *) = atimes, function A.(-_) = aopp
+clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.(*) = rtimes, function R.(-_) = ropp, function (+) = aplus, function (*) = atimes, function A.(-_) = aopp, axiom .
 
 (*axiom azero_def: azero = A.zero*) (* FIXME *)
 
@@ -464,7 +465,8 @@ let predicate eq0_int (x:int) = x=0
 
 let function ($$) (x y:int) :int = x * y
 
-clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = ( *), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = ( *), val ($) = ($$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc
+clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = (*), val ($) = ($$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc,
+  axiom . (* FIXME: replace with "goal" and prove *)
 
 
 goal g: forall x y. x + y = y + x

examples/ring_decision/strassen.mlw

@@ -4,7 +4,7 @@ use import int.Int
 
 type mat 'a
 
-clone algebra.UnitaryCommutativeRing as F
+clone algebra.UnitaryCommutativeRing as F with axiom .
 
 function get (mat F.t) int int : F.t
 function set (mat F.t) int int F.t : mat F.t
@@ -109,16 +109,19 @@ module InfMatrix
   type t
   constant tzero: t
 
-  clone export algebra.UnitaryCommutativeRing with type t = t, constant zero = tzero
+  clone export algebra.UnitaryCommutativeRing with
+    type t = t, constant zero = tzero, axiom .
 
   use import int.Int
-  clone export relations.MinMax with type t = int, predicate le = (<=)
+  clone export relations.MinMax with
+    type t = int, predicate le = (<=),
+    axiom . (* FIXME: replace with "goal" and prove *)
 
   type mat
 
   val function get mat int int : t
- 
- val function row_zeros mat int : int
+
+  val function row_zeros mat int : int
   val function col_zeros mat int : int
 
   val function create (rz: int -> int) (cz: int -> int) (f: int -> int -> t)
@@ -163,7 +166,8 @@ module InfMatrix
     lemma set_def_rowz_changed,
     lemma set_def_rowz_unchanged,
     lemma set_def_other_rowz,
-    lemma set_def_other_colz
+    lemma set_def_other_colz,
+    axiom . (* FIXME: replace with "goal" and prove *)
 
   let ghost function fcreate (r c: int) (f: int -> int -> t) : mat =
     create (fun _ -> max 0 c) (fun _ -> max 0 r) f