added stamp_trfun, mk_trfun, eq_trfun;
authorwenzelm
Sat Apr 16 18:58:30 2005 +0200 (2005-04-16)
changeset 15754f867c48de2e1
parent 15753 eb014dfc57ee
child 15755 50ac97ebe7d8
added stamp_trfun, mk_trfun, eq_trfun;
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Apr 16 18:58:18 2005 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Apr 16 18:58:30 2005 +0200
     1.3 @@ -11,6 +11,9 @@
     1.4    val constrainC: string
     1.5    val typeT: typ
     1.6    val max_pri: int
     1.7 +  val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
     1.8 +  val mk_trfun: string * 'a -> string * ('a * stamp)
     1.9 +  val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
    1.10  end;
    1.11  
    1.12  signature SYN_EXT =
    1.13 @@ -36,38 +39,41 @@
    1.14        xprods: xprod list,
    1.15        consts: string list,
    1.16        prmodes: string list,
    1.17 -      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.18 +      parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.19        parse_rules: (Ast.ast * Ast.ast) list,
    1.20 -      parse_translation: (string * (term list -> term)) list,
    1.21 -      print_translation: (string * (bool -> typ -> term list -> term)) list,
    1.22 +      parse_translation: (string * ((term list -> term) * stamp)) list,
    1.23 +      print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    1.24        print_rules: (Ast.ast * Ast.ast) list,
    1.25 -      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.26 +      print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.27        token_translation: (string * string * (string -> string * real)) list}
    1.28    val mfix_args: string -> int
    1.29    val escape_mfix: string -> string
    1.30    val syn_ext': bool -> (string -> bool) -> mfix list ->
    1.31 -    string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.32 -    (string * (term list -> term)) list *
    1.33 -    (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.34 +    string list -> (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    1.35 +    (string * ((term list -> term) * stamp)) list *
    1.36 +    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.37 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    1.38      -> (string * string * (string -> string * real)) list
    1.39      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.40    val syn_ext: mfix list -> string list ->
    1.41 -    (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    1.42 -    (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.43 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    1.44 +    (string * ((term list -> term) * stamp)) list *
    1.45 +    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.46 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list
    1.47      -> (string * string * (string -> string * real)) list
    1.48      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.49    val syn_ext_const_names: string list -> syn_ext
    1.50    val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.51    val syn_ext_trfuns:
    1.52 -    (string * (Ast.ast list -> Ast.ast)) list *
    1.53 -    (string * (term list -> term)) list *
    1.54 -    (string * (bool -> typ -> term list -> term)) list *
    1.55 -    (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
    1.56 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    1.57 +    (string * ((term list -> term) * stamp)) list *
    1.58 +    (string * ((bool -> typ -> term list -> term) * stamp)) list *
    1.59 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    1.60    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    1.61    val pure_ext: syn_ext
    1.62  end;
    1.63  
    1.64 -structure SynExt : SYN_EXT =
    1.65 +structure SynExt: SYN_EXT =
    1.66  struct
    1.67  
    1.68  
    1.69 @@ -313,13 +319,13 @@
    1.70      xprods: xprod list,
    1.71      consts: string list,
    1.72      prmodes: string list,
    1.73 -    parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.74 +    parse_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.75      parse_rules: (Ast.ast * Ast.ast) list,
    1.76 -    parse_translation: (string * (term list -> term)) list,
    1.77 -    print_translation: (string * (bool -> typ -> term list -> term)) list,
    1.78 +    parse_translation: (string * ((term list -> term) * stamp)) list,
    1.79 +    print_translation: (string * ((bool -> typ -> term list -> term) * stamp)) list,
    1.80      print_rules: (Ast.ast * Ast.ast) list,
    1.81 -    print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.82 -    token_translation: (string * string * (string -> string * real)) list}
    1.83 +    print_ast_translation: (string * ((Ast.ast list -> Ast.ast) * stamp)) list,
    1.84 +    token_translation: (string * string * (string -> string * real)) list};
    1.85  
    1.86  
    1.87  (* syn_ext *)
    1.88 @@ -354,6 +360,10 @@
    1.89  fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
    1.90  fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
    1.91  
    1.92 +fun stamp_trfun s (c, f) = (c, (f, s));
    1.93 +fun mk_trfun tr = stamp_trfun (stamp ()) tr;
    1.94 +fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
    1.95 +
    1.96  
    1.97  (* pure_ext *)
    1.98