# HG changeset patch
# User clasohm
# Date 804778793 -7200
# Node ID b28c6ecc3e6dc0dc28ed295a9bd938fff8dd2a89
# Parent  58e4d9221db7fa3b9d625872fa35a54b280ced58
added cargs for curried function application

diff -r 58e4d9221db7 -r b28c6ecc3e6d src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Jul 03 13:37:29 1995 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Mon Jul 03 15:39:53 1995 +0200
@@ -139,7 +139,7 @@
 
 val pure_types =
   map (fn t => (t, 0, NoSyn))
-    (terminals @ [logic, "type", "types", "sort", "classes", args,
+    (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
       "pttrn", "idt", "idts", "aprop", "asms", any, sprop]);
 
 val pure_syntax =
diff -r 58e4d9221db7 -r b28c6ecc3e6d src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Mon Jul 03 13:37:29 1995 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Jul 03 15:39:53 1995 +0200
@@ -18,6 +18,7 @@
   local open Ast in
     val logic: string
     val args: string
+    val cargs: string
     val any: string
     val sprop: string
     val typ_to_nonterm: typ -> string
@@ -77,6 +78,7 @@
 val logicT = Type (logic, []);
 
 val args = "args";
+val cargs = "cargs";
 
 val typeT = Type ("type", []);
 
diff -r 58e4d9221db7 -r b28c6ecc3e6d src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Jul 03 13:37:29 1995 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Jul 03 15:39:53 1995 +0200
@@ -55,7 +55,7 @@
 fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args)
   | appl_ast_tr asts = raise_ast "appl_ast_tr" asts;
 
-fun applC_ast_tr (asts as (f::args)) = Appl asts
+fun applC_ast_tr [f, args] = Appl (f :: unfold_ast "_cargs" args)
   | applC_ast_tr asts = raise_ast "applC_ast_tr" asts;
 
 
@@ -129,12 +129,8 @@
   | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
 
 fun applC_ast_tr' (f, []) = raise_ast "applC_ast_tr'" [f]
-  | applC_ast_tr' (f, arg::args) =
-      let (* fold curried function application *)
-          fun fold [] result = result
-            | fold (x :: xs) result =
-                fold xs (Appl [Constant "_applC", result, x]);
-      in fold args (Appl [Constant "_applC", f, arg]) end;
+  | applC_ast_tr' (f, args) =
+      Appl [Constant "_applC", f, fold_ast "_cargs" args];
 
 
 (* abstraction *)
@@ -289,20 +285,8 @@
     (*translate pt bottom-up*)
     fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
       | ast_of (Tip tok) = Variable (str_of_token tok);
-
-    (*unfold curried application top-down (needed for CPure)*)
-    fun unfold_applC (Node ("_applC", pts)) =
-          let (*translate (applC(applC(f,a),b),c) to (f,a,b,c)*)
-              fun unfold [Node ("_applC", pts), arg] = (unfold pts) @ [arg]
-                | unfold n = n
-          in Node ("_applC", map unfold_applC (unfold pts))
-                                (*top "_applC" is removed by applC_ast_tr;
-                                  note that arguments are unfolded separately*)
-          end
-      | unfold_applC (Node (a, pts)) = Node (a, map unfold_applC pts)
-      | unfold_applC tip = tip
   in
-    ast_of (unfold_applC pt)
+    ast_of pt
   end;
 
 
diff -r 58e4d9221db7 -r b28c6ecc3e6d src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jul 03 13:37:29 1995 +0200
+++ b/src/Pure/sign.ML	Mon Jul 03 15:39:53 1995 +0200
@@ -308,7 +308,7 @@
      | Ambigs(us) =>
          (warn();
           let val old_show_brackets = !show_brackets
-              val _ = show_brackets := true;
+              val dummy = show_brackets := true;
               val errs = cat_lines(map show_term us)
           in show_brackets := old_show_brackets;
              error("Error: More than one term is type correct:\n" ^ errs)
@@ -553,12 +553,16 @@
 
 val cpure = proto_pure
   |> add_syntax
-   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("_/ _",
-                                                    [max_pri-1, max_pri],
-                                                    max_pri-1)),
-    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("_/ _",
-                                                    [max_pri-1, max_pri],
-                                                    max_pri-1))]
+   [("",           "'a => cargs",                   Delimfix "_"),
+    ("_cargs",     "['a, cargs] => cargs",          Mixfix ("_/ _",
+                                                     [max_pri, max_pri],
+                                                     max_pri)),
+    ("_applC",     "[('b => 'a), cargs] => logic",  Mixfix ("(1_/ _)",
+                                                     [max_pri, max_pri],
+                                                     max_pri-1)),
+    ("_applC",     "[('b => 'a), cargs] => aprop",  Mixfix ("(1_/ _)",
+                                                     [max_pri, max_pri],
+                                                     max_pri-1))]
   |> add_name "CPure";
 
 end;