accomodate advanced trfuns;
authorwenzelm
Wed Jun 29 15:13:40 2005 +0200 (2005-06-29)
changeset 1661058bf09036a6d
parent 16609 c787112bba1f
child 16611 edb368e2878f
accomodate advanced trfuns;
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Jun 29 15:13:39 2005 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 29 15:13:40 2005 +0200
     1.3 @@ -193,9 +193,10 @@
     1.4      val mfix = List.concat (map mfix_of const_decls);
     1.5      val xconsts = map name_of const_decls;
     1.6      val binders = List.mapPartial binder const_decls;
     1.7 -    val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o SynTrans.mk_binder_tr);
     1.8 +    val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o
     1.9 +        apsnd K o SynTrans.mk_binder_tr);
    1.10      val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o
    1.11 -        apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap);
    1.12 +        apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
    1.13    in
    1.14      SynExt.syn_ext' true is_logtype
    1.15        mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 29 15:13:39 2005 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 29 15:13:40 2005 +0200
     2.3 @@ -42,27 +42,27 @@
     2.4        xprods: xprod list,
     2.5        consts: string list,
     2.6        prmodes: string list,
     2.7 -      parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
     2.8 +      parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
     2.9        parse_rules: (Ast.ast * Ast.ast) list,
    2.10 -      parse_translation: (string * ((term list -> term) * stamp)) list,
    2.11 -      print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    2.12 +      parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    2.13 +      print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    2.14        print_rules: (Ast.ast * Ast.ast) list,
    2.15 -      print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    2.16 +      print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    2.17        token_translation: (string * string * (string -> string * real)) list}
    2.18    val mfix_args: string -> int
    2.19    val escape_mfix: string -> string
    2.20    val syn_ext': bool -> (string -> bool) -> mfix list ->
    2.21 -    string list -> (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    2.22 -    (string * ((term list -> term) * stamp)) list *
    2.23 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    2.24 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    2.25 +    string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    2.26 +    (string * ((theory -> term list -> term) * stamp)) list *
    2.27 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    2.28 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    2.29      -> (string * string * (string -> string * real)) list
    2.30      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.31    val syn_ext: mfix list -> string list ->
    2.32 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    2.33 -    (string * ((term list -> term) * stamp)) list *
    2.34 -    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    2.35 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    2.36 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    2.37 +    (string * ((theory -> term list -> term) * stamp)) list *
    2.38 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    2.39 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    2.40      -> (string * string * (string -> string * real)) list
    2.41      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.42    val syn_ext_const_names: string list -> syn_ext
    2.43 @@ -72,6 +72,11 @@
    2.44      (string * ((term list -> term) * stamp)) list *
    2.45      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    2.46      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    2.47 +  val syn_ext_advanced_trfuns:
    2.48 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    2.49 +    (string * ((theory -> term list -> term) * stamp)) list *
    2.50 +    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    2.51 +    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    2.52    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    2.53    val standard_token_markers: string list
    2.54    val pure_ext: syn_ext
    2.55 @@ -323,12 +328,12 @@
    2.56      xprods: xprod list,
    2.57      consts: string list,
    2.58      prmodes: string list,
    2.59 -    parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    2.60 +    parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    2.61      parse_rules: (Ast.ast * Ast.ast) list,
    2.62 -    parse_translation: (string * ((term list -> term) * stamp)) list,
    2.63 -    print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    2.64 +    parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    2.65 +    print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    2.66      print_rules: (Ast.ast * Ast.ast) list,
    2.67 -    print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    2.68 +    print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    2.69      token_translation: (string * string * (string -> string * real)) list};
    2.70  
    2.71  
    2.72 @@ -361,9 +366,14 @@
    2.73  
    2.74  fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
    2.75  fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
    2.76 -fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
    2.77 +fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
    2.78  fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
    2.79  
    2.80 +fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
    2.81 +  let fun simple (name, (f, s)) = (name, (K f, s)) in
    2.82 +    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
    2.83 +  end;
    2.84 +
    2.85  fun stamp_trfun s (c, f) = (c, (f, s));
    2.86  fun mk_trfun tr = stamp_trfun (stamp ()) tr;
    2.87  fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;