# 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;