Merge pull request #18 from AthenaFoundation/hol2

Hol2

definition_processor.sml

@@ -3460,7 +3460,7 @@ fun setFlag(flag as {name,pos=flag_pos}:AbstractSyntax.param,value as (str,pos))
      myPrint("\n"^Options.setBooleanFlag(Options.auto_assert_selector_axioms,Names.auto_assert_selector_axioms_flag,str,pos)^"\n")
   else 
   if Symbol.symEq(name,Names.silent_mode_flag_symbol) then 
-     myPrint("\n"^Options.setBooleanFlag(Options.silent_mode,Names.silent_mode_flag_name,str,pos)^"\n")
+     myPrint(Options.setBooleanFlag(Options.silent_mode,Names.silent_mode_flag_name,str,pos))
   else myPrint("\n"^(Symbol.name(name))^" is not a flag.\n")
  end
 

lib/basic/hol_examples.ath

@@ -160,3 +160,72 @@ define increment-thrice := (compose* [increment increment increment])
            [2 3 4]))
 
 # Basically, it allows anonymous lambdas in any context that expects a term of sort (Fun ...). 
+# lambda-promote can also be invoked explicitly, and it also goes by the alias "hol-fun".
+# Moreover, in addition to a closure, it can also be given as argument a map of the form |{'foo := <some-closure>}|. 
+# In that case, instead of using a random function symbol to define <some-closure>, Athena will use the name "foo".
+# For example: (lambda-promote |{'cube := lambda (x) (x * x * x)}|) will introduce a function symbol named cube,
+# define that symbol with axioms based on the given lambda (and bind the name "cube-def" to those axioms), and then
+# return that symbol. Thus, for example:
+
+(hol-fun |{ 'cube := lambda (x) (x * x * x)}|)
+
+# can be seen as equivalent to first executing the following prelude commands: 
+# 
+# declare cube: [Int] -> Int 
+# assert* cube-def := [(cube x = x * x * x)]
+#
+# and then finally returning the newly introduced symbol cube. Recall that a symbol like cube will be automatically
+# coerced into a lifted version, cube^, in any context that requires a functor argument (a term of sort (Fun ...)),
+# which means that the result of (hol-fun |{ 'cube := lambda (x) (x * x * x)}|) can be directly used as an argument
+# to a higher-order function that expects a functor. 
+
+#**************************** Functor Identity ****************************
+
+# The only axiom schema that is needed for higher-order logic is this:
+# (forall f1:(Fun 'S_1 ...'S_n T) f2:(Fun 'S_1 ...'S_n T) . f1 = f2 <==> forall x_1:S_1 ... x_n:S_n . (f1 x_1 ... x_n) = (f2 x_1 ... x_n))
+# This needs to be an axiom schema since n can be any nonnegative integer. This is captured by the primitive method functor-identity
+# defined in rewriting.ath, which takes n as an argument as returns the corresponding instance of the above axiom scheme. For example:
+
+(!functor-identity 2)
+
+# Should return: 
+
+# Theorem: (forall ?v3266:(Fun 'S 'T 'U)
+#            (forall ?v3267:(Fun 'S 'T 'U)
+#              (iff (= ?v3266:(Fun 'S 'T 'U)
+#                      ?v3267:(Fun 'S 'T 'U))
+#                   (forall ?v3268:'S
+#                     (forall ?v3269:'T
+#                       (= (app ?v3266:(Fun 'S 'T 'U)
+#                               ?v3268:'S
+#                               ?v3269:'T)
+#                          (app ?v3267:(Fun 'S 'T 'U)
+#                               ?v3268:'S
+#                               ?v3269:'T)))))))
+
+# Now let 'square' be the functor lambda (x) (x * x) and let 'quad' be the functor lambda (x) (x * x * x * x),
+# and let's use functor-identity to show that (compose square square) is identical to quad. The proof needs
+# the associativity of multiplication, so let's assert that for now since it's not our focus: 
+
+assert (associative *)
+
+# Here is the goal:
+
+define goal :=  (= (compose (hol-fun |{'square := lambda (x) (x * x)}|) 
+                            (hol-fun lambda (x) (x * x)))
+                   (hol-fun |{ 'quad := lambda (x) (x * x * x * x)}|))
+
+# Note that in the second argument to compose we simply wrote (hol-fun lambda (x) (x * x)), whereas in 
+# the first argument we wrote (hol-fun |{'square := lambda (x) (x * x)}|). A name only needs to be given once,
+# so we don't need to repeat that. Now here is the proof:
+
+conclude goal 
+  let {functor-identity-condition := (!right-iff (!uspec* (!functor-identity 1)
+                                                          [(compose square^ square^) quad^]));
+       extensional-identity := pick-any x:Real
+                                 (!chain [(app (compose square^ square^) x)
+                                        = (square square x)                  [compose-def]
+                                        = ((x * x) * (x * x))                [square-def]
+                                        = (x * (x * (x * x)))                [(associative *)]
+                                        = (quad x)                           [quad-def]])}
+    (!mp functor-identity-condition extensional-identity)

lib/basic/rewriting.ath

@@ -4701,5 +4701,3 @@ EOF
 
 (load-file "cc")
 
-
-

lib/basic/util.ath

@@ -5050,7 +5050,7 @@ define (drop-quotes str) :=
      (loop str [])
 
 
-define (promote-aux f) := 
+define (promote-aux f ht name) := 
   let {arity := (arity-of f);
        fresh-args := (map (lambda (_) (fresh-var)) (1 to arity));
        fresh-arg-names := (map var->string fresh-args);
@@ -5078,4 +5078,81 @@ define (promote-aux f) :=
 
 define (lambda-promote f) :=
   check {(symbol? (val->string f)) => f
-       | else => try { (promote-aux f) | f }}  
+       | else => try { (promote-aux f "") | f }}
+
+define (silent-on) :=
+  (process-input-from-string "(set-flag silent-mode \"on\")");
+
+define (silent-off) :=
+  (process-input-from-string "(set-flag silent-mode \"off\")");  
+
+define (execute-command cmd) :=
+   let {_ := (silent-on);
+        _ := (process-input-from-string cmd)}
+     (silent-off)         
+
+define (execute-commands cmds) := 
+  (map-proc execute-command cmds)
+
+define lambda-promote :=        
+  let {ht := (HashTable.table 111);
+       promote-aux :=
+               lambda (closure-or-sub)
+                  let {[name closure] := check {(map? closure-or-sub) =>
+                                                     match (Map.key-values closure-or-sub) {
+                                                       ([[k v]] where (&& (meta-id? k) (proc? v))) => [(tail (val->string k)) v]
+                                                     | _ => (error "The map given to a lambda promoter should be of the form |{<meta-identifier> := <closure>}|")
+                                                     }
+                                              | else => ["" closure-or-sub]};
+                       arity := (arity-of closure);
+                       fresh-args := (map (lambda (_) (fresh-var)) (1 to arity));
+                       fresh-arg-names := (map var->string fresh-args);
+                       eqn := (= (app-proc closure fresh-args) ?res);
+                       fingerprint := (close eqn);
+                       _ := ()
+                      }
+                    match try {(HashTable.lookup ht fingerprint) | ()} {
+                       () => let {result-sort := (sort-of (rhs eqn));
+                                  arg-sort-pairs := (map (lambda (v)
+                                                           [(var->string v) (sort-of v)])
+                                                         (dedup (filter (vars (lhs eqn))
+                                  (lambda (v) (member? (var->string v) fresh-arg-names)))));
+                                  arg-sort-map := (Map.make arg-sort-pairs);
+                                  arg-sorts := (map (lambda (v)
+                                                      (arg-sort-map v))
+                                                    fresh-arg-names);
+                                  sort-params := (get-sort-params (add result-sort arg-sorts));
+                                  sym-name := check {(null? name) => (make-fresh-symbol-name)
+                                                     | else => name};
+                                  sort-param-open := check {(null? sort-params) => "" | else => " ( "};
+                                  sort-param-close := check {(null? sort-params) => "" | else => " ) "};       
+                                  declare-cmd := (join "declare " sym-name ": " sort-param-open (separate sort-params ", ") " "
+                                                       sort-param-close " [" (drop-quotes (separate arg-sorts " ")) "] -> "
+                                                       (drop-quotes result-sort));
+                                  fresh-arg-names' := (map (lambda (fn) (join "?" fn)) fresh-arg-names);       
+                                  assert-cmd := (join "assert* " sym-name "-def := [(= (" sym-name " "
+                                                      (separate fresh-arg-names' " ") ") "
+                                                      (val->string (app-proc closure fresh-args)) ")]");
+                                  _ := (silent-on);
+                                  _ := (seq (process-input-from-string declare-cmd) (process-input-from-string assert-cmd));
+                                  _ := (silent-off);                                  
+                                  _ := (process-input-from-string "(set-flag silent-mode \"off\")");
+                                  res := (evaluate (join sym-name "^"));
+                                  _ := (HashTable.add ht [fingerprint res])
+                                 }
+                               res
+                     | cached-symbol => let {_ := check {(null? name) => ()
+                                                       | else => let {cmd := (join "(define " name " " (val->string cached-symbol) ")");
+                                                                      _ := (silent-on);
+                                                                      _ := (process-input-from-string cmd)}
+                                                                   (silent-off)}}
+                                          cached-symbol
+                    }
+      }
+    lambda (f)         
+      check {(symbol? (val->string f)) => f
+       | else => try { (promote-aux f) | f }}
+
+
+define hol-fun := lambda-promote
+