src/Pure/sign.ML
changeset 922 196ca0973a6d
parent 901 77795af99315
child 926 9d1348498c36
     1.1 --- a/src/Pure/sign.ML	Thu Mar 02 12:07:20 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Mar 03 11:48:05 1995 +0100
     1.3 @@ -61,7 +61,9 @@
     1.4      val add_name: string -> sg -> sg
     1.5      val make_draft: sg -> sg
     1.6      val merge: sg * sg -> sg
     1.7 +    val proto_pure: sg
     1.8      val pure: sg
     1.9 +    val cpure: sg
    1.10      val const_of_class: class -> string
    1.11      val class_of_const: string -> class
    1.12    end
    1.13 @@ -179,10 +181,16 @@
    1.14  
    1.15  (** pretty printing of terms and types **)
    1.16  
    1.17 -fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
    1.18 +fun pretty_term (Sg {syn, stamps, ...}) =
    1.19 +  let val curried = "CPure" mem (map ! stamps);
    1.20 +  in Syntax.pretty_term curried syn end;
    1.21 +
    1.22  fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
    1.23  
    1.24 -fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
    1.25 +fun string_of_term (Sg {syn, stamps, ...}) = 
    1.26 +  let val curried = "CPure" mem (map ! stamps);
    1.27 +  in Syntax.string_of_term curried syn end;
    1.28 +
    1.29  fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
    1.30  
    1.31  fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
    1.32 @@ -516,7 +524,7 @@
    1.33  
    1.34  (** the Pure signature **)
    1.35  
    1.36 -val pure =
    1.37 +val proto_pure =
    1.38    make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
    1.39    |> add_types
    1.40     (("fun", 2, NoSyn) ::
    1.41 @@ -537,7 +545,24 @@
    1.42      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
    1.43      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.44      ("TYPE", "'a itself", NoSyn)]
    1.45 +  |> add_name "ProtoPure";
    1.46 +
    1.47 +val pure = proto_pure
    1.48 +  |> add_syntax
    1.49 +   [("_appl",     "[('b => 'a), args] => logic",    Mixfix ("(1_/(1'(_')))",
    1.50 +                                                    [max_pri, 0], max_pri)),
    1.51 +    ("_appl",     "[('b => 'a), args] => aprop",    Mixfix ("(1_/(1'(_')))",
    1.52 +                                                    [max_pri, 0], max_pri))]
    1.53    |> add_name "Pure";
    1.54  
    1.55 +val cpure = proto_pure
    1.56 +  |> add_syntax
    1.57 +   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("(1_ (1_))",
    1.58 +                                                    [max_pri-1, max_pri],
    1.59 +                                                    max_pri-1)),
    1.60 +    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("(1_ (1_))",
    1.61 +                                                    [max_pri-1, max_pri],
    1.62 +                                                    max_pri-1))]
    1.63 +  |> add_name "CPure";
    1.64  
    1.65  end;