WIP

alpha.sml

@@ -26,25 +26,80 @@ datatype certificate = ruleApp of {rule:symbol, args: alpha_val list}
                      | composition of {left: certificate, right: certificate}
                      | pickAny of {eigen_var: symbol, actual_fresh: variable, body: certificate}
                      | conclude of {expected_conc: prop, body: certificate}
+                     | block of certificate list 
+
+val trivial_cert = ruleApp({rule=S.symbol("BOGUS_RULE"),args=[]})
 
 fun simpleCert(ruleApp(_)) = true
   | simpleCert(_) = false 
 
+fun compsToBlocks(D) = 
+  let fun B(composition({left,right})) = (B left)@(B right)
+	| B(D) = [D] 
+      fun c2b(D as composition(_)) = block(map c2b (B D))
+	| c2b(assumeProof({hyp,body})) = assumeProof({hyp=hyp,body=c2b(body)})
+	| c2b(supAbProof({hyp,body})) = supAbProof({hyp=hyp,body=c2b(body)})
+	| c2b(pickAny({eigen_var,actual_fresh,body})) = pickAny({eigen_var=eigen_var,actual_fresh=actual_fresh,body=c2b(body)})
+	| c2b(conclude({expected_conc,body})) = conclude({expected_conc=expected_conc,body=c2b(body)})
+	| c2b(block(Ds)) = block(map c2b Ds)
+	| c2b(D) = D
+  in
+     c2b(D)
+  end
+
+fun certToStringNaive(D) = 
+  let fun argToString(term(t)) = AT.toStringDefault(t)
+        | argToString(sent(p)) = Prop.makeTPTPPropSimple(p)
+      fun argsToString(args) = Basic.printListStr(args,argToString,", ")
+      fun f(ruleApp({rule,args,...})) = "[" ^ (S.name rule) ^ " on " ^ (argsToString args) ^ "]"
+	| f(assumeProof({hyp as hypothesis(name_opt,p),body})) = "assume " ^ (Prop.makeTPTPPropSimple p) ^ " { " ^ (f body) ^ " } "
+        | f(supAbProof({hyp as hypothesis(name_opt,p),body})) = "suppose-absurd " ^ (Prop.makeTPTPPropSimple p) ^ " { " ^ (f body) ^ " } "
+        | f(block(proofs)) = " BLOCK_START " ^ Basic.printListStr(proofs,f," || ") ^ " BLOCK_END "
+	| f(composition({left,right})) = (f left) ^ " ;; " ^ (f right)
+        | f(D) = "NOT IMPLEMENTED YET"
+  in
+     f(D)
+  end
+
+fun hasSubproof(D,pred) = 
+   let fun find(D) = 
+             if pred(D) then let val _ = print("\nFOUND TARGET PROOF: " ^ (certToStringNaive D) ^ "\n") in true end else 
+             (case D of 
+                 composition({left,right}) => find(left) orelse find(right)
+  	       | assumeProof({body,...}) => find(body)
+  	       | supAbProof({body,...}) => find(body)
+  	       | pickAny({body,...}) => find(body)
+  	       | conclude({body,...}) => find(body)
+               | block(certs) => Basic.exists(certs,find)
+	       | _ => false)
+   in 
+      find D 
+   end
+
+fun compFree(D) = 
+     if hasSubproof(D,fn D' => (case D' of composition(_) => true | _ => false))
+     then false else true 
+
 fun certToString(D) = 
   let val spaces = Basic.spaces
       fun argToString(term(t)) = AT.toStringDefault(t)
-        | argToString(sent(p)) = Prop.makeTPTPProp(p)
+        | argToString(sent(p)) = Prop.makeTPTPPropSimple(p)
       fun argsToString(args) = Basic.printListStr(args,argToString,", ")
       fun c2s(ruleApp({rule,args,...}),offset) = (spaces offset) ^ (S.name rule) ^ " on " ^ (argsToString args)
 	| c2s(assumeProof({hyp as hypothesis(name_opt,p),body}),offset) = 
-	      (spaces offset) ^ "assume " ^ (Prop.makeTPTPProp p) ^ "\n" ^ (c2s(body,offset+2))
+	      (spaces offset) ^ "assume " ^ (Prop.makeTPTPPropSimple p) ^ " {\n" ^ (c2s(body,offset+2)) ^ "\n" ^ (spaces (offset + 1)) ^"}"
 	| c2s(supAbProof({hyp as hypothesis(name_opt,p),body}),offset) = 
-	      (spaces offset) ^ "suppose-absurd " ^ (Prop.makeTPTPProp p) ^ "\n" ^ (c2s(body,offset+2))
-	| c2s(composition({left,right}),offset) = (c2s(left,offset)) ^ "\n" ^ (c2s(right,offset))
+	      (spaces offset) ^ "suppose-absurd " ^ (Prop.makeTPTPPropSimple p) ^ "\n" ^ (c2s(body,offset+2))
+	| c2s(composition({left,right}),offset) = (c2s(left,offset+2)) ^ ";\n" ^ (c2s(right,offset+2)) 
+	| c2s(block([D]),offset) = c2s(D,offset) 
+	| c2s(block(D1::(more as (_::_))),offset) = c2s(D1,offset) ^ ";\n" ^ (c2s(block(more),offset))
 	| c2s(conclude({expected_conc,body}),offset) = 
-             (spaces offset) ^ (Prop.makeTPTPProp expected_conc) ^ " BY " ^ (if simpleCert(body) then c2s(body,0) else ("\n" ^ c2s(body,offset + 2)))
+             (spaces offset) ^ (Prop.makeTPTPPropSimple expected_conc) ^ " BY " ^ (if simpleCert(body) then c2s(body,0) else ("\n" ^ c2s(body,offset + 2)))
+      val D' = compsToBlocks(D)
   in
-    "\n" ^ (c2s(D,0))
+    (case D' of 
+        block(_)  => "{\n" ^ (c2s(D',2)) ^ "\n}"
+      | _ => (c2s(D',0)))
   end              
 
 type alpha_ded_info = {proof: certificate, conc: Prop.prop, fa: Prop.prop list} 
@@ -358,6 +413,11 @@ and evDed(method_app as A.BMethAppDed({method,arg1,arg2,pos}),env,ab) =
            in
               doBindings(bindings,[],env)
            end
+  | evDed(D,env,ab) = 
+          let val _ = print("\n***************************************** UNHANDLED CERT CASE: " ^ (A.unparseDed(D)) ^ "\n")
+          in
+             (evalDed(D,env,ab),{proof=trivial_cert,conc=Prop.true_prop,fa=[]})
+          end
 (*******************************************************************************************************************************************************************************
   | evDed(A.letDed({bindings,body,pos}),env,ab) =       
        let fun doLetDed([]:A.binding list,env1,ab1) = evDed(body,env1,ab1)

names.sml

@@ -176,6 +176,9 @@ val applyExtractedSortSubFun_symbol = Symbol.symbol applyExtractedSortSubFun_nam
 val fsymsInFunDefTableFun_name = "defined-fsyms"
 val fsymsInFunDefTableFun_symbol = Symbol.symbol fsymsInFunDefTableFun_name
 
+val getAlphaCertFun_name = "get-alpha-cert"
+val getAlphaCertFun_symbol = Symbol.symbol getAlphaCertFun_name
+
 val subtermsFun_name = "subterms"
 val subtermsFun_symbol = Symbol.symbol subtermsFun_name
 

prop.sig

@@ -197,6 +197,7 @@ sig
    val sizeLst: prop list -> int 
 
    val makeTPTPProp: prop -> string 
+   val makeTPTPPropSimple: prop -> string 
    val makeTPTPPropList: prop list -> string list 
    val makePolyTPTPProp: prop -> string 
    val makeTSTPProp: prop -> string 

prop.sml

@@ -2085,6 +2085,50 @@ fun makeTPTPProp(P) =
      f P'
   end
 
+fun makeTPTPPropSimple(P) = 
+  let val P' = alphaRename(P)
+      val (lp,rp,comma,blank) = ("(",")",","," ")
+      val fvars = freeVars(P')
+      fun f(P_in as atom({term=t,...})) = 
+            let val bc = isBooleanConstant(P_in)
+		val is_bc = not(bc = "") 
+            in
+	       if is_bc then bc else 
+	       (case AthTerm.isApp(t) of
+                  SOME(g,[]) => (Basic.fsymRenamer(MS.name(g)))
+                | SOME(g,args) => let val is_eq = msymEq(g,N.mequal_logical_symbol)
+				      val gname = if is_eq then "=" else (Basic.fsymRenamer(MS.name(g)))
+                                      val arg_strings = map (fn t => AT.makeTPTPTerm(t,fvars)) args 
+                                      val str = if is_eq then 
+                                                   (case arg_strings of 
+                                                       [s1,s2] => lp^s1^blank^gname^blank^s2^rp)
+                                                else gname^lp^(Basic.printListStr(arg_strings,fn x => x,comma))^rp 
+			          in
+                                    str 
+		                  end
+                | _ => (case AT.isVarOpt(t) of
+                           SOME(v) => if Basic.isMemberEq(v,fvars,ATV.athTermVarEq) then
+                                         (Basic.varRenamer(ATV.name(v)))
+                                       else Basic.failLst(["Quantified Boolean variables are not allowed in TPTP formulas."])
+                        | _ => raise Basic.Never))
+            end
+        | f(neg({arg,...})) = " ~ ("^f(arg)^")"
+        | f(conj({args,...})) = fLst(args," & ")
+        | f(disj({args,...})) = fLst(args," | ")
+        | f(cond({ant=P1,con=P2,...})) =  "("^f(P1)^" => "^f(P2)^")"
+        | f(biCond({left=P1,right=P2,...})) = "("^f(P1)^" <=> "^f(P2)^")"
+        | f(uGen({qvar,body,...})) = "! [ " ^ (AthTerm.makeConservativeName(ATV.name(qvar)))^" ] : ( "^f(body)^")"
+        | f(eGen({qvar,body,...})) = "? [ " ^ (AthTerm.makeConservativeName(ATV.name(qvar)))^" ] : ( "^f(body)^")"
+        | f(eGenUnique({qvar,body,...})) = 
+		Basic.failLst(["Translation to TPTP failed on exists-unique sentence."])
+      and fLst([],_) = ""
+        | fLst([P],_) = f(P)
+        | fLst(P1::(rest as (_::_)),sep) = "("^(f P1)^sep^(fLst(rest,sep))^")"
+  in
+     f P'
+  end
+
+
 fun makeTPTPPropList(props) = List.map makeTPTPProp props
 
 fun makeTSTPProp(P) = 

semantics.sml

@@ -3232,7 +3232,6 @@ and
                      val v2 = evPhrase(arg2,env,ab)
                      val ab' = if A.isDeduction(arg1) then putValIntoAB(v1,ab) else ab
                      val ab'' = if A.isDeduction(arg2) then putValIntoAB(v2,ab') else ab'
-                     val _ = print("\nEXECUTING THIS PRIM BINARY METHOD: " ^ (Symbol.name method_code))
                  in
                     M(v1,v2,env,ab'') 
                  end handle PrimError(msg) => evError(msg,SOME(pos))

topenv_part1.sml

@@ -677,6 +677,21 @@ fun rootFun([v],(env,ab),{pos_ar,file}) =
   | rootFun(vals,_,{pos_ar,file}) = evError(wrongArgNumber(N.root_name,length(vals),1),
                                             SOME(Array.sub(pos_ar,0)))
 
+
+fun getAlphaCertFun(v1,v2,env,ab) = 
+  (case (v1,v2) of 
+     (closMethodVal(A.methodExp({params=[],body,pos,name}),env_ref),
+      closUFunVal(continuation_body,parameter,close_env,{name=cont_name,prec,...})) => 
+         let val (method_res,ded_info as {proof,conc,fa,...}) = Alpha.evalDedAlpha(body,env_ref,ab)
+             val proof_str = Alpha.certToString(proof)
+             val proof_ath_str = MLStringToAthString(proof_str)
+             val res = evalClosure(v2,[proof_ath_str],ab,NONE)
+         in
+            res 
+         end
+   | (v1,closUFunVal(_)) => primError(wrongArgKind(N.getAlphaCertFun_name,1,closMethodLCType,v1))
+   | (_,v2) => primError(wrongArgKind(N.getAlphaCertFun_name,2,closUFunType,v2)))
+
 fun mergeSortPrimBFun(v1,v2,env,ab) =  
       (case v1 of 
           listVal(vals) =>
@@ -723,6 +738,7 @@ fun mergeSortPrimBFun'(v1,v2,env,ab) =
                            listVal(Basic.mergeSortBuiltIn(vals,compare))
                         end))
 
+
 fun unparseFun([closMethodVal(A.methodExp({params=[],body,pos,name}),env_ref)],env,ab) = 
       let val proof_str = A.unparseDed(body)
       in

topenv_part2.sml

@@ -3738,6 +3738,7 @@ val init_val_bindings = [(N.not_symbol,propConVal(A.notCon)),(N.and_symbol,propC
                          (N.unifiable_sort_fun_symbol,primBFunVal(unifiableSortsPrimBFun,default_bfv_pa_for_procs N.unifiable_sort_fun_name)),
                          (N.built_in_merge_sort_symbol',primBFunVal(mergeSortPrimBFun,default_bfv_pa_for_procs N.built_in_merge_sort_name')),
                          (N.built_in_merge_sort_symbol,primBFunVal(mergeSortPrimBFun',default_bfv_pa_for_procs N.built_in_merge_sort_name)),
+                         (N.getAlphaCertFun_symbol,primBFunVal(getAlphaCertFun,default_bfv_pa_for_procs N.getAlphaCertFun_name)),
                          (N.uspecPrimMethod_symbol,SV.primBMethodVal(uSpecPrimBMethod,N.uspecPrimMethod_symbol)),
                          (N.proofErrorMethod_symbol,SV.primUMethodVal(proofErrorPrimUMethod,N.proofErrorMethod_symbol)),
                          (N.compErrorFun_symbol,primUFunVal(compErrorPrimUFun,default_ufv_pa_for_procs N.compErrorFun_name)),