Add theory file

althelf/README.md

@@ -16,6 +16,8 @@ changing its parser.
   `false`.  Hence, a the simple `false` term should be parsed as the empty
   clause, and `cl false` is the clause containing the literal `false`.
 * Sharing doesn't use `! .. :named`, but instead uses `define` statements.
+* Since AletheLF doesn't support overloading, arithmetic negation uses
+  the operator `u-`.
 
 ## Contexts
 

althelf/alethe.smt3 → althelf/rules.smt3

+(include "./theory.smt3")
+
 % Rule: assume is native
 
 % Note: The hole here does not allow for args or premises.
@@ -101,7 +103,7 @@
 )
 
 % TODO: side condition
-(declare-rule bind ((ctx Context) (xs VarList) (ys VarList) (T Type) (phi T) (phi' T))
+(declare-rule bind ((ctx @Context) (xs @VarList) (ys @VarList) (T Type) (phi T) (phi' T))
   :assumption ctx
   :premises ((cl (= phi phi')))
   :args ((cl (= (forall xs phi) (forall ys phi'))))
@@ -110,7 +112,7 @@
 )
 
 % TODO: side condition
-(declare-rule sko_ex ((ctx Context) (xs VarList) (phi Bool) (psi Bool))
+(declare-rule sko_ex ((ctx @Context) (xs @VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :args ((cl (= (exists xs phi) psi)))
@@ -119,7 +121,7 @@
 )
 
 % TODO: side condition
-(declare-rule sko_forall ((ctx Context) (xs VarList) (phi Bool) (psi Bool))
+(declare-rule sko_forall ((ctx @Context) (xs @VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :args ((cl (= (forall xs phi) psi)))
@@ -128,7 +130,7 @@
 )
 
 % TODO: side condition
-(declare-rule forall_inst ((ctx Bool) (xs VarList) (phi Bool) (psi Bool))
+(declare-rule forall_inst ((ctx Bool) (xs @VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
   :args ((cl (= (forall xs phi) psi)))
@@ -137,14 +139,14 @@
 )
 
 % TODO: side condition
-(declare-rule forall_inst ((P Bool) (P' Bool) (xs VarList))
+(declare-rule forall_inst ((P Bool) (P' Bool) (xs @VarList))
   :args ((cl (or (not (forall xs P) P'))))
   :requires ((check_forall_inst xs P P') true)
   :conclusion (cl (or (not (forall xs P) P')))
 )
 
 % TODO: side condition
-(declare-rule refl ((ctx Context) (T Type) (t1 T) (t2 T))
+(declare-rule refl ((ctx @Context) (T Type) (t1 T) (t2 T))
   :premises (ctx)
   :args ((cl (= t1 t2)))
   :requires ((check_refl ctx t1 t2) true)
@@ -192,7 +194,7 @@
   :conclusion CL
 )
 
-(declare-rule qnt_cnf ((phi Bool) (phi' Bool) (xs VarList) (xs' VarList))
+(declare-rule qnt_cnf ((phi Bool) (phi' Bool) (xs @VarList) (xs' @VarList))
   :args ((cl (or (not (forall xs phi)) (forall xs' phi'))))
   :conclusion (cl (or (not (forall xs phi)) (forall xs' phi')))
 )
@@ -534,7 +536,7 @@
 )
 
 % TODO: sidecondition
-(declare-rule onepoint ((ctx Context) (xs VarList) (ys VarList) (Q (-> VarList Bool Bool)) (T Type) (phi T) (phi' T))
+(declare-rule onepoint ((ctx @Context) (xs @VarList) (ys @VarList) (Q (-> @VarList Bool Bool)) (T Type) (phi T) (phi' T))
   :assumption ctx
   :premises ((cl (= phi phi')))
   :args (((cl (= (Q xs phi) (Q ys phi')))))

althelf/theory.smt3

+; -----------
+;   Builtin
+; -----------
+
+(declare-const ite (-> (! Type :var A :implicit) Bool A A A))
+(declare-const not (-> Bool Bool))
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
+(declare-const => (-> Bool Bool Bool) :right-assoc)
+(declare-const xor (-> Bool Bool Bool) :left-assoc)
+(declare-const = (-> (! Type :var A :implicit) A A Bool) :chainable and)
+(declare-const distinct (-> (! Type :var A :implicit) A A Bool) :pairwise and)
+
+; ---------------------------
+;   Int and Real Arithmetic
+; ---------------------------
+
+(declare-sort Int 0)
+(declare-sort Real 0)
+
+(declare-consts <numeral> Int)
+(declare-consts <rational> Real)
+
+; arith_typeunion
+;   @param x a type
+;   @param y a Type
+;   @return the "union" of x and y.
+; The returned type is the type of the result of mixed arithmetic operators taking arguments x and y.
+(program arith_typeunion ()
+    (Type Type) Type
+    (
+      ((arith_typeunion Int Int) Int)
+      ((arith_typeunion Real Real) Real)
+      ((arith_typeunion Real Int) Real)
+      ((arith_typeunion Int Real) Real)
+    )
+)
+
+; is_arith_type
+;   @param x
+;   @returns true if x is Int or Real
+(program is_arith_type ()
+    (Type) Bool
+    (
+      ((is_arith_type Int) true)
+      ((is_arith_type Real) true)
+    )
+)
+
+; Core operators of arithmetic, which are used in mixed Int/Real arithmetic.
+; Using integer nil terminators ensures typing is accurate.
+(declare-const + (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     T U (arith_typeunion T U)) :right-assoc-nil 0)
+(declare-const - (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     T U (arith_typeunion T U)) :left-assoc)
+(declare-const * (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     T U (arith_typeunion T U)) :right-assoc-nil 1)
+(declare-const / (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     T U
+                     (! Real :requires ((is_arith_type T) true)
+                             :requires ((is_arith_type U) true))) :left-assoc)
+(declare-const div (-> Int Int Int) :left-assoc)
+(declare-const mod (-> Int Int Int))
+
+(declare-const < (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     (! T :requires ((is_arith_type T) true))
+                     (! U :requires ((is_arith_type U) true))
+                     Bool)
+                     :chainable and)
+(declare-const <= (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                      (! T :requires ((is_arith_type T) true))
+                      (! U :requires ((is_arith_type U) true))
+                      Bool)
+                      :chainable and)
+(declare-const > (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                     (! T :requires ((is_arith_type T) true))
+                     (! U :requires ((is_arith_type U) true))
+                     Bool)
+                     :chainable and)
+(declare-const >= (-> (! Type :var T :implicit) (! Type :var U :implicit)
+                      (! T :requires ((is_arith_type T) true))
+                      (! U :requires ((is_arith_type U) true))
+                      Bool)
+                      :chainable and)
+
+; Conversion functions.
+(declare-const to_real (-> (! Type :var T :implicit)
+                           (! T :requires ((is_arith_type T) true))
+                           Real))
+(declare-const to_int (-> (! Type :var T :implicit)
+                          (! T :requires ((is_arith_type T) true))
+                          Int))
+(declare-const is_int (-> (! Type :var T :implicit)
+                          (! T :requires ((is_arith_type T) true))
+                          Bool))
+(declare-const abs (-> (! Type :var T :implicit)
+                       (! T :requires ((is_arith_type T) true))
+                       T))
+
+; Currently unary negation cannot use overload.
+(declare-const u- (-> (! Type :var T :implicit)
+                      (! T :requires ((is_arith_type T) true))
+                      T))
+
+; ---------------
+;   Quantifiers
+; ---------------
+
+(declare-sort @VarList 0)
+(declare-const @varlist.nil @VarList)
+(declare-const @varlist (-> (! Type :var T :implicit) T @VarList @VarList) :right-assoc-nil @varlist.nil)
+
+; TODO: definie VarList
+(declare-const forall (-> @VarList Bool Bool))
+(declare-const exists (-> @VarList Bool Bool))
+(declare-const choice (-> (! Type :var T :implicit) T Bool T))
+
+(declare-sort @Context 0)
+(declare-const @ctx.nil @Context)
+; The first argument is an equality (= v t) mapping term t to the variable v.
+(declare-const @ctx.map (-> Bool @Context @Context :right-assoc-nil @ctx.nil)