Tactics

ab.sig

@@ -17,6 +17,8 @@ sig
 
     val insert: Prop.prop * assum_base -> assum_base
 
+    val insertAlongWithConjuncts: Prop.prop * assum_base -> assum_base
+
     val remove: assum_base * Prop.prop  -> assum_base
 
     val augment: assum_base * Prop.prop list -> assum_base
@@ -48,6 +50,7 @@ sig
 
     val getAssertions: assum_base -> Prop.prop list
     val addAssertion: Prop.prop * assum_base -> assum_base
+    val addAssertionAlongWithConjuncts: Prop.prop * assum_base -> assum_base
     val addAssertions: Prop.prop list * assum_base -> assum_base
     val isAssertion: Prop.prop * assum_base -> bool 
 

ab.sml

@@ -138,7 +138,11 @@ fun addAssertion(p,abase({prop_table,tag,...}):assum_base) =
 fun addAssertions(props,beta:assum_base) = 
   let fun loop([],res) = res
         | loop(a::more,res) = loop(more,addAssertion(a,res))
-  in loop(props,beta) end
+  in 
+    loop(props,beta) 
+  end
+
+fun addAssertionAlongWithConjuncts(p,ab) = addAssertions(p::(Prop.getConjunctsOnly p),ab)
 
 fun isAssertion(p,abase({prop_table,...}):assum_base) = 
       (case IntBinaryMap.find(prop_table,getPropCode(p)) of
@@ -212,10 +216,12 @@ fun insertAux(P,ab as abase({prop_table,tag,...}): assum_base) =
        abase({prop_table=IntBinaryMap.insert(prop_table,code,P),tag=inc(next_ab_tag)})
      end
 
-fun insert(P,ab) =  insertAux(P,ab)
+fun insert(P,ab) = insertAux(P,ab)
 
 fun augment(ab,props) = List.foldl insert ab props
 
+fun insertAlongWithConjuncts(P,ab) = augment(ab,P::(Prop.getConjunctsOnly P))
+
 fun getAll(ab as abase({prop_table,...}):assum_base) = IntBinaryMap.listItems(prop_table)
 
 fun occursFree(v,ab) = List.exists (fn (P) => Prop.occursFree(v,P)) (getAll ab) 

abstract_syntax.sml

@@ -1004,9 +1004,40 @@ and unparseCheckClause({test=boolCond(phr),result,...}:check_clause) = lparen^(u
   | unparseCheckClause({test=elseCond,result,...}:check_clause) = lparen^(Names.else_name)^space^(unparseExp(result))^rparen
 and unparseCheckClauses(clauses) = Basic.printSExpListStr(clauses,unparseCheckClause)
 and unparseBinding({bpat,def,...}) = lparen^(printPat bpat)^space^(unparsePhrase def)^rparen
+and unparseBindingInfix({bpat,def,...}) = (printPat bpat)^ " := " ^(unparsePhrase def)
 and unparseBindings(bindings) = Basic.printSExpListStr(bindings,unparseBinding)
-and unparseDed(methodAppDed({method,args,pos})) = "(!"^(unparseExp method)^space^(Basic.printSExpListStr(args,unparsePhrase))^")"
-  | unparseDed(_) = "(Don't know how to unparse this deduction yet.)"
+and unparseBindingsInfix(bindings) = Basic.printListStr(bindings,unparseBindingInfix,"; ")
+and unparseDed(methodAppDed({method,args,pos})) = 
+       let 
+       in
+          "(!"^(unparseExp method)^space^(Basic.printSExpListStr(args,unparsePhrase))^")"
+       end
+  | unparseDed(UMethAppDed({method, arg, pos})) = 
+       let 
+       in
+         "(!"^(unparseExp method)^space^(Basic.printSExpListStr([arg],unparsePhrase))^")"
+       end 
+  | unparseDed(BMethAppDed({method, arg1, arg2, pos})) = "(!"^(unparseExp method)^space^(Basic.printSExpListStr([arg1,arg2],unparsePhrase))^")"
+  | unparseDed(letDed({bindings,body,pos,...})) = "let {"^(unparseBindingsInfix bindings)^"}"^space^(unparseDed body)
+  | unparseDed(beginDed({members,pos,...})) = "{"^(Basic.printListStr(members, unparseDed, ";\n"))^"}"
+  | unparseDed(matchDed(_)) = "Match ded!"
+  | unparseDed(letRecDed(_)) = "Letrec ded!"
+  | unparseDed(checkDed(_)) = "Check ded!"
+  | unparseDed(assumeDed(_)) = "Assume ded!"
+  | unparseDed(infixAssumeDed(_)) = "Infix Assume ded!"
+  | unparseDed(assumeLetDed(_)) = "Assume-Let ded!"
+  | unparseDed(absurdDed(_)) = "Absurd ded!"
+  | unparseDed(tryDed(_)) = "Try ded!"
+  | unparseDed(absurdLetDed(_)) = "Absurd-Let ded!"
+  | unparseDed(inductionDed(_)) = "Induction ded!"
+  | unparseDed(structureCasesDed(_)) = "Structure-Cases ded!"
+  | unparseDed(byDed(_)) = "By ded!"
+  | unparseDed(fromDed(_)) = "From ded!"
+  | unparseDed(genOverDed(_)) = "Gen-over ded!"
+  | unparseDed(pickAnyDed(_)) = "Pick-any ded!"
+  | unparseDed(withWitnessDed(_)) = "With-witness ded!"
+  | unparseDed(pickWitnessDed(_)) = "Pick-witness ded!"
+  | unparseDed(pickWitnessesDed(_)) = "Pick-witnesses ded!"
 and unparsePhrase(exp(e)) = unparseExp(e)
   | unparsePhrase(ded(d)) = unparseDed(d)
 and

athena.grm

@@ -702,7 +702,6 @@ deduction:  LPAREN expression BY deduction RPAREN (A.byDed({wanted_res=expressio
                 (A.byCasesDed({disj=phrase,from_exps=NONE,
                                arms=case_clauses,pos=getPos BY_CASESleft}))
 
-
           | BY_CASES phrase FROM comma_separated_expression_list BEGIN case_clauses END 
               (A.byCasesDed({disj=phrase,from_exps=SOME(comma_separated_expression_list),
                              arms=case_clauses,pos=getPos BY_CASESleft}))

athena.mlb

@@ -83,6 +83,7 @@ in
 	smt_output.sml
 	compiler.sml
 	server.sml 
+        simp.sml
 	topenv_part1.sml
 	topenv_part2.sml
 	definition_processor.sml

athena.sml

@@ -28,6 +28,10 @@ fun run() = let val _ = Options.first_time := true
             in runWithStarterFile(NONE) end 
 
 (**
+fun run() = let val _ = Options.first_time := true
+            in ExpressServer.startServerOnPort(10000) end 
+**)
+(**
 
 -- XSB-specific code, commented out by default:
 

base.sig

@@ -33,6 +33,7 @@ sig
     val writeString: string * char Array.array * int -> int 
     val remove : ''a * ''a list -> ''a list
     val removeAll : ''a list * ''a list -> ''a list
+    val removeAllEq : 'a list * 'a list * ('a * 'a -> bool) -> 'a list
     val removeEq : 'a * 'a list * ('a * 'a ->bool) -> 'a list
     val removeAndCheckMemEq : 'a * 'a list * ('a * 'a ->bool) -> ('a list * bool)
     val zip : 'a list * 'b list -> ('a * 'b) list

base.sml

@@ -223,13 +223,21 @@ fun removeAll(L1,L2) =
            loop(L1,L2)
        end
 
+
 fun removeEq(x,l,eq) = 
     let fun remove([],res) = res
           | remove(y::ys,res) = if eq(x,y) then remove(ys,res) else remove(ys,y::res)
         in
           remove(l,[])
     end
 
+fun removeAllEq(L1,L2,f) = 
+       let fun loop([],res) = res
+             | loop(x::more,res) = loop(more,removeEq(x,res,f))
+       in
+           loop(L1,L2)
+       end
+
 (* removeAndCheckMemEq also does not preserve order: *)
 
 fun removeAndCheckMemEq(x,l,eq) = 

client.py

@@ -0,0 +1,53 @@
+import sys
+sys.path.append('/mnt/c/code/python')
+from utils1 import *
+import socket
+
+def send_request_to_server(request: str,port=10000) -> str:
+    # Define server address and port
+    server_address = 'localhost'
+    # Create a TCP/IP socket
+    with socket.socket(socket.AF_INET, socket.SOCK_STREAM) as sock:
+        # Connect to the server
+        sock.connect((server_address, port))
+        try:
+            # Send the request string encoded as bytes
+            sock.sendall(request.encode('utf-8'))
+            # Receive the response from the server
+            response = sock.recv(4096)  # Buffer size is 4096 bytes
+            # Decode the response from bytes to a string
+            return response.decode('utf-8')
+        except Exception as e:
+            print(f"An error occurred: {e}")
+            return ""
+
+# Usage example
+# Usage example
+#response = send_request_to_server("Hello, server!")
+
+
+s = "(plus 1 2)"
+request = s
+b = s.encode('utf-8')
+port = 10000
+server_address = 'localhost'
+#sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
+
+
+s = '''let {_ := (process-input-from-string "declare A, B, C, D, E, F, G, H: Boolean")}
+  assume h := (A & B) {
+    (!both (!right-and h) (!left-and h))
+  }
+'''
+
+#send_request_to_server('(process-input-from-string "(declare (A B C D E F G H) Boolean)")')
+
+s = '''assume h := (A & B) 
+          (!both (!right-and h) (!left-and h))
+'''
+
+
+s = '''assume h := (A & B) 
+          (!both (!dn h) (!left-and h))
+'''
+

definition_processor.sml

@@ -79,9 +79,12 @@ val pprint =  TopEnv.pprint
 val top_assum_base = ABase.top_assum_base
 
 fun addPropToGlobalAb(p,mod_path,string_opt) = 
-    (top_assum_base := ABase.insert(p,!top_assum_base);
+  let 
+  in
+    (top_assum_base := ABase.insertAlongWithConjuncts(p,!top_assum_base);
      P.addToModuleAb(mod_path,p,string_opt);
-     top_assum_base := ABase.addAssertion(p,!top_assum_base))
+     top_assum_base := ABase.addAssertionAlongWithConjuncts(p,!top_assum_base))
+  end 
 
 fun addPropsToGlobalAb(props,mod_path,string_opt) = List.app (fn p => addPropToGlobalAb(p,mod_path,string_opt)) props
 val top_val_env = SV.top_val_env 
@@ -1281,7 +1284,7 @@ fun printVal(Semantics.propVal(p),(true,_)) =
 
 fun addProp(v as Semantics.propVal(p),env,eval_env,(is_ded,name_opt),mod_path,definition_sym_opt) = 
          if is_ded then
-            (top_assum_base := ABase.augment(!top_assum_base,[p]);  	     
+            (top_assum_base := ABase.insertAlongWithConjuncts(p,!top_assum_base);
              (case (name_opt,definition_sym_opt) of 
                  (SOME(name),_) => (Semantics.updateTopValEnv(env,name,v,true);Semantics.updateTopValEnv(eval_env,name,v,true);P.addToModuleAb(mod_path,p,SOME(S.name(name))))
                | (_,SOME(name)) => (Semantics.updateTopValEnv(env,name,v,true);Semantics.updateTopValEnv(eval_env,name,v,true);P.addToModuleAb(mod_path,p,SOME(S.name(name))))