diff --git a/definition_processor.sml b/definition_processor.sml index 319f779..482d2bf 100755 --- a/definition_processor.sml +++ b/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 diff --git a/lib/basic/hol_examples.ath b/lib/basic/hol_examples.ath index 7a64271..12c3383 100644 --- a/lib/basic/hol_examples.ath +++ b/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 := }|. +# In that case, instead of using a random function symbol to define , 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) diff --git a/lib/basic/rewriting.ath b/lib/basic/rewriting.ath index d36522b..a2bc92b 100644 --- a/lib/basic/rewriting.ath +++ b/lib/basic/rewriting.ath @@ -4701,5 +4701,3 @@ EOF (load-file "cc") - - diff --git a/lib/basic/util.ath b/lib/basic/util.ath index 4564fd7..077536d 100644 --- a/lib/basic/util.ath +++ b/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 }} \ No newline at end of file + | 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 |{ := }|") + } + | 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 +