Hol2 (#17)

* Sorts of the form (Fun S_1 ... S_n T) now accepted

* Sorts of the form (Fun S_1 ... S_n T) now accepted truly everywhere

* Arbitrary app terms accepted now

* Audo-adding lifted symbol versions

* WIP

* WIP

* (app increment^ 4) now returns (increment 4)

* Handled unary app cases

* Restored infix_parser.sml

* Overloaded and input-expanded symbols now also do term lifting as needed

* uspec now accepts higher-order values as the second argument

* WIP

* WIP

* Explicit app's of lifted symbols are now auto-simplifed in AT.makeApp1 rather than the evaluator level

* WIP

* Added primitive method functor-identity

* Examples in sf/code/hol4.ath working

* Proper 'app' sort checking for unary, binary, and general applications

* Small cleanup

* Checking in lib/basic/hol_examples.ath

* Implemented promotion of anonymous lambdas

abstract_syntax.sml

@@ -404,7 +404,12 @@ fun inapplicable(phrase) =
   (case phrase of
       exp(taggedConSym(_)) => true
     | exp(numExp(_)) => true
-    | exp(termVarExp(_)) => true
+    | exp(termVarExp({user_sort,...})) =>
+           (case user_sort of 
+               NONE => true
+             | SOME(sort) => (case SymTerm.isTaggedApp(sort) of
+                                 SOME(f,_,args) => not(MS.modSymEq(f,Names.fun_name_msym))
+				| _ => true))
     | exp(quotedIdeExp(_)) => true
     | exp(unitExp(_)) => true
     | exp(charExp(_)) => true

ath_term.sig

@@ -304,6 +304,7 @@ sentence variables. **)
    val applyLst: FTerm.sub * (variable list) * (fsymbol * sort) list * term list -> term list 
 
    val evaluateString:(string -> unit) ref
+   val fauxTermToPrettyString: int * fsymbol * term list -> string 
 
 end
 

ath_term.sml

@@ -2008,11 +2008,32 @@ fun makeAppAndReturnSortSub(f,terms) = makeAppAndReturnSortSubCore(f,terms)
 					failLst(["Unable to infer a sort for the term: \n"^
  			                         (fauxTermToPrettyString(0,f,terms))])
 
+fun sortsMatch(fun_sort,arg_sorts) = 
+   (case Data.funSortArity(fun_sort) of 
+       SOME(n) => n = length(arg_sorts)
+     | _ => false)
+
+fun getFunctorSignature(f,args) = 
+   if  MS.modSymEq(f,Names.app_fsym_mname) then 
+         let val actual_args = tl args 
+             val (fun_sort, arg_sorts, res_sort) = D.makeFunSort(actual_args)
+             val lifted_app_sym_opt = (case (hd args) of 
+                                          (t as App({root,args=[],...})) => 
+                                            if Data.isLiftedFSym(root) andalso sortsMatch(getSort(t),arg_sorts) then SOME(MS.unlift(root)) else NONE
+			                | _ => NONE)
+         in
+            ((fun_sort::arg_sorts,res_sort,true,false),lifted_app_sym_opt)
+         end 
+   else (D.getSignature(f),NONE)
+
 fun makeApp1(f,terms,from_side) = 
 	if Util.notNumeric(f) then 
-           let val (param_sorts,result_sort,is_poly,has_pred_based_sorts) = D.getSignature(f)
+           let val ((param_sorts,result_sort,is_poly,has_pred_based_sorts),lifted_app_sym_opt) = getFunctorSignature(f,terms)
            in
-            if has_pred_based_sorts then
+            (case lifted_app_sym_opt of 
+               SOME(g) => makeApp1(g,tl terms,from_side)
+             | _ => 
+             if has_pred_based_sorts then
               ((makeAppNormally(f,terms,from_side,param_sorts,result_sort,is_poly,has_pred_based_sorts))
                 handle _ => 
                   let fun loop([],_,arg_sorts',tccs) = (rev(arg_sorts'),tccs)
@@ -2065,7 +2086,7 @@ fun makeApp1(f,terms,from_side) =
                                    poly_constants=new_poly_constants_and_their_sorts'',bits=orTermWords(terms',root_word)})
 	        in
 		   res
-		end
+		end)
            end
 	else 
             let
@@ -2077,7 +2098,7 @@ fun makeAppBinary(f,term1,term2,from_side) =  makeApp1(f,[term1,term2],from_side
 
 fun makeAppUnary(f,term,from_side) =  
 	if Util.notNumeric(f) then 
-           let val (param_sorts,result_sort,is_poly,has_pred_based_sorts) = D.getSignature(f)
+           let val ((param_sorts,result_sort,is_poly,has_pred_based_sorts),lifted_app_sym_opt) = getFunctorSignature(f,[term])
            in
              if has_pred_based_sorts then
  	        let val arg_sort = getSort term

athena.grm

@@ -23,7 +23,7 @@ fun getPos((l,p)) = {line=l,pos=p,file=(!Paths.current_file)}
        LPAREN | RPAREN | COMMA | CLAIM | LEFT_BRACKET | RIGHT_BRACKET | SET | ARROW | WILDCARD | SOME_CHAR |
        FUNCTION | METHOD | MATCH | LET | LET_UPPER | DLET | TRY | DTRY | APPLY_METHOD | SOME_VAR | SEQ | DSEQ | SOME_VECTOR | MAP_BEGIN | MAP_END | 
        EQUAL_SIGN | ASSERT | ASSERT_CLOSE | ASSUME | ASSUME_LET | SUPPOSE_ABSURD | SUPPOSE_ABSURD_LET | ON | PROVE | 
-       DMATCH | EITHER | ABSURD | MP | DN | EQUIV | LEFT_IFF | RIGHT_IFF | BOTH  | ASGN | BY_CASES | 
+       DMATCH | EITHER | ABSURD | MP | DN | EQUIV | LEFT_IFF | RIGHT_IFF | BOTH  | ASGN | BY_CASES | FUN | 
        META_ID | SOME_SYMBOL | LEFT_AND | RIGHT_AND | CD | VAL_OF | VAR | FUN_ARROW | DATATYPE | DATATYPES | DEFINE_SORT | 
        SOME_LIST | SOME_CELL | SOME_SUB | SOME_TABLE | SOME_MAP | DEFINE | POUND | STRUCTURE | STRUCTURES | DOMAIN | WHERE | PROVIDED | 
        DECLARE | DDECLARE | DIRECTIVE_PREFIX | EGEN | BEGIN | WHILE | CLEAR | THE | DEFINE_SYMBOL | DOMAINS | OVER  | 
@@ -1051,6 +1051,11 @@ user_sort: QUOTE_SYMBOL ID (SymTerm.makeTaggedVar(Symbol.symbol(ID),getPos(QUOTE
                  in
                    SymTerm.makeTaggedApp(A.makeMS(ID,SOME id_pos),id_pos,one_or_more_user_sorts)
                  end)
+         | LPAREN FUN one_or_more_user_sorts RPAREN 
+		(let val id_pos = getPos(FUNleft)
+                 in 
+                   SymTerm.makeTaggedApp(A.makeMS("Fun",SOME id_pos),id_pos,one_or_more_user_sorts)
+                 end)
 
 one_or_more_user_sorts: user_sort ([user_sort])
                       | user_sort one_or_more_user_sorts (user_sort::one_or_more_user_sorts)
@@ -1466,6 +1471,11 @@ athena_object_type:
                        in 
                           SymTerm.makeTaggedConstant(A.makeMS(ID,SOME id_pos),id_pos)
                        end)
+                  | LPAREN FUN one_or_more_athena_object_types RPAREN
+                       (let val id_pos = getPos(FUNleft)
+                        in
+                           SymTerm.makeTaggedApp(A.makeMS("Fun",SOME id_pos),id_pos,one_or_more_athena_object_types)
+                        end)
                   | LPAREN ID one_or_more_athena_object_types RPAREN
                        (let val id_pos = getPos(IDleft)
                         in

athena.grm.sig

@@ -80,6 +80,7 @@ val RIGHT_AND:  'a * 'a -> (svalue,'a) token
 val LEFT_AND:  'a * 'a -> (svalue,'a) token
 val SOME_SYMBOL:  'a * 'a -> (svalue,'a) token
 val META_ID:  'a * 'a -> (svalue,'a) token
+val FUN:  'a * 'a -> (svalue,'a) token
 val BY_CASES:  'a * 'a -> (svalue,'a) token
 val ASGN:  'a * 'a -> (svalue,'a) token
 val BOTH:  'a * 'a -> (svalue,'a) token