added cargs for curried function application
authorclasohm
Mon Jul 03 15:39:53 1995 +0200 (1995-07-03)
changeset 1178b28c6ecc3e6d
parent 1177 58e4d9221db7
child 1179 7678408f9751
added cargs for curried function application
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Mon Jul 03 13:37:29 1995 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon Jul 03 15:39:53 1995 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  
     1.5  val pure_types =
     1.6    map (fn t => (t, 0, NoSyn))
     1.7 -    (terminals @ [logic, "type", "types", "sort", "classes", args,
     1.8 +    (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
     1.9        "pttrn", "idt", "idts", "aprop", "asms", any, sprop]);
    1.10  
    1.11  val pure_syntax =
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Jul 03 13:37:29 1995 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Jul 03 15:39:53 1995 +0200
     2.3 @@ -18,6 +18,7 @@
     2.4    local open Ast in
     2.5      val logic: string
     2.6      val args: string
     2.7 +    val cargs: string
     2.8      val any: string
     2.9      val sprop: string
    2.10      val typ_to_nonterm: typ -> string
    2.11 @@ -77,6 +78,7 @@
    2.12  val logicT = Type (logic, []);
    2.13  
    2.14  val args = "args";
    2.15 +val cargs = "cargs";
    2.16  
    2.17  val typeT = Type ("type", []);
    2.18  
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Jul 03 13:37:29 1995 +0200
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon Jul 03 15:39:53 1995 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4  fun appl_ast_tr [f, args] = Appl (f :: unfold_ast "_args" args)
     3.5    | appl_ast_tr asts = raise_ast "appl_ast_tr" asts;
     3.6  
     3.7 -fun applC_ast_tr (asts as (f::args)) = Appl asts
     3.8 +fun applC_ast_tr [f, args] = Appl (f :: unfold_ast "_cargs" args)
     3.9    | applC_ast_tr asts = raise_ast "applC_ast_tr" asts;
    3.10  
    3.11  
    3.12 @@ -129,12 +129,8 @@
    3.13    | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
    3.14  
    3.15  fun applC_ast_tr' (f, []) = raise_ast "applC_ast_tr'" [f]
    3.16 -  | applC_ast_tr' (f, arg::args) =
    3.17 -      let (* fold curried function application *)
    3.18 -          fun fold [] result = result
    3.19 -            | fold (x :: xs) result =
    3.20 -                fold xs (Appl [Constant "_applC", result, x]);
    3.21 -      in fold args (Appl [Constant "_applC", f, arg]) end;
    3.22 +  | applC_ast_tr' (f, args) =
    3.23 +      Appl [Constant "_applC", f, fold_ast "_cargs" args];
    3.24  
    3.25  
    3.26  (* abstraction *)
    3.27 @@ -289,20 +285,8 @@
    3.28      (*translate pt bottom-up*)
    3.29      fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
    3.30        | ast_of (Tip tok) = Variable (str_of_token tok);
    3.31 -
    3.32 -    (*unfold curried application top-down (needed for CPure)*)
    3.33 -    fun unfold_applC (Node ("_applC", pts)) =
    3.34 -          let (*translate (applC(applC(f,a),b),c) to (f,a,b,c)*)
    3.35 -              fun unfold [Node ("_applC", pts), arg] = (unfold pts) @ [arg]
    3.36 -                | unfold n = n
    3.37 -          in Node ("_applC", map unfold_applC (unfold pts))
    3.38 -                                (*top "_applC" is removed by applC_ast_tr;
    3.39 -                                  note that arguments are unfolded separately*)
    3.40 -          end
    3.41 -      | unfold_applC (Node (a, pts)) = Node (a, map unfold_applC pts)
    3.42 -      | unfold_applC tip = tip
    3.43    in
    3.44 -    ast_of (unfold_applC pt)
    3.45 +    ast_of pt
    3.46    end;
    3.47  
    3.48  
     4.1 --- a/src/Pure/sign.ML	Mon Jul 03 13:37:29 1995 +0200
     4.2 +++ b/src/Pure/sign.ML	Mon Jul 03 15:39:53 1995 +0200
     4.3 @@ -308,7 +308,7 @@
     4.4       | Ambigs(us) =>
     4.5           (warn();
     4.6            let val old_show_brackets = !show_brackets
     4.7 -              val _ = show_brackets := true;
     4.8 +              val dummy = show_brackets := true;
     4.9                val errs = cat_lines(map show_term us)
    4.10            in show_brackets := old_show_brackets;
    4.11               error("Error: More than one term is type correct:\n" ^ errs)
    4.12 @@ -553,12 +553,16 @@
    4.13  
    4.14  val cpure = proto_pure
    4.15    |> add_syntax
    4.16 -   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("_/ _",
    4.17 -                                                    [max_pri-1, max_pri],
    4.18 -                                                    max_pri-1)),
    4.19 -    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("_/ _",
    4.20 -                                                    [max_pri-1, max_pri],
    4.21 -                                                    max_pri-1))]
    4.22 +   [("",           "'a => cargs",                   Delimfix "_"),
    4.23 +    ("_cargs",     "['a, cargs] => cargs",          Mixfix ("_/ _",
    4.24 +                                                     [max_pri, max_pri],
    4.25 +                                                     max_pri)),
    4.26 +    ("_applC",     "[('b => 'a), cargs] => logic",  Mixfix ("(1_/ _)",
    4.27 +                                                     [max_pri, max_pri],
    4.28 +                                                     max_pri-1)),
    4.29 +    ("_applC",     "[('b => 'a), cargs] => aprop",  Mixfix ("(1_/ _)",
    4.30 +                                                     [max_pri, max_pri],
    4.31 +                                                     max_pri-1))]
    4.32    |> add_name "CPure";
    4.33  
    4.34  end;