Elimination of fully-functorial style.
authorpaulson
Fri Feb 16 17:18:51 1996 +0100 (1996-02-16)
changeset 15104588ba1b1438
parent 1509 7f693bb0d7dd
child 1511 09354d37a5ab
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Feb 16 16:56:04 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Feb 16 17:18:51 1996 +0100
     1.3 @@ -6,70 +6,65 @@
     1.4  *)
     1.5  
     1.6  signature SYN_EXT0 =
     1.7 -sig
     1.8 +  sig
     1.9    val typeT: typ
    1.10    val constrainC: string
    1.11 -end;
    1.12 +  end;
    1.13  
    1.14  signature SYN_EXT =
    1.15 -sig
    1.16 +  sig
    1.17    include SYN_EXT0
    1.18 -  structure Ast: AST
    1.19 -  local open Ast in
    1.20 -    val logic: string
    1.21 -    val args: string
    1.22 -    val cargs: string
    1.23 -    val any: string
    1.24 -    val sprop: string
    1.25 -    val typ_to_nonterm: typ -> string
    1.26 -    datatype xsymb =
    1.27 -      Delim of string |
    1.28 -      Argument of string * int |
    1.29 -      Space of string |
    1.30 -      Bg of int | Brk of int | En
    1.31 -    datatype xprod = XProd of string * xsymb list * string * int
    1.32 -    val max_pri: int
    1.33 -    val chain_pri: int
    1.34 -    val delims_of: xprod list -> string list
    1.35 -    datatype mfix = Mfix of string * typ * string * int list * int
    1.36 -    datatype syn_ext =
    1.37 -      SynExt of {
    1.38 -        logtypes: string list,
    1.39 -        xprods: xprod list,
    1.40 -        consts: string list,
    1.41 -        parse_ast_translation: (string * (ast list -> ast)) list,
    1.42 -        parse_rules: (ast * ast) list,
    1.43 -        parse_translation: (string * (term list -> term)) list,
    1.44 -        print_translation: (string * (term list -> term)) list,
    1.45 -        print_rules: (ast * ast) list,
    1.46 -        print_ast_translation: (string * (ast list -> ast)) list}
    1.47 -    val mk_syn_ext: bool -> string list -> mfix list ->
    1.48 -      string list -> (string * (ast list -> ast)) list *
    1.49 -      (string * (term list -> term)) list *
    1.50 -      (string * (term list -> term)) list * (string * (ast list -> ast)) list
    1.51 -      -> (ast * ast) list * (ast * ast) list -> syn_ext
    1.52 -    val syn_ext: string list -> mfix list -> string list ->
    1.53 -      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
    1.54 -      (string * (term list -> term)) list * (string * (ast list -> ast)) list
    1.55 -      -> (ast * ast) list * (ast * ast) list -> syn_ext
    1.56 -    val syn_ext_logtypes: string list -> syn_ext
    1.57 -    val syn_ext_const_names: string list -> string list -> syn_ext
    1.58 -    val syn_ext_rules: string list -> (ast * ast) list * (ast * ast) list -> syn_ext
    1.59 -    val syn_ext_trfuns: string list ->
    1.60 -      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
    1.61 -      (string * (term list -> term)) list * (string * (ast list -> ast)) list
    1.62 -      -> syn_ext
    1.63 -    val pure_ext: syn_ext
    1.64 -  end
    1.65 -end;
    1.66 +  val logic: string
    1.67 +  val args: string
    1.68 +  val cargs: string
    1.69 +  val any: string
    1.70 +  val sprop: string
    1.71 +  val typ_to_nonterm: typ -> string
    1.72 +  datatype xsymb =
    1.73 +    Delim of string |
    1.74 +    Argument of string * int |
    1.75 +    Space of string |
    1.76 +    Bg of int | Brk of int | En
    1.77 +  datatype xprod = XProd of string * xsymb list * string * int
    1.78 +  val max_pri: int
    1.79 +  val chain_pri: int
    1.80 +  val delims_of: xprod list -> string list
    1.81 +  datatype mfix = Mfix of string * typ * string * int list * int
    1.82 +  datatype syn_ext =
    1.83 +    SynExt of {
    1.84 +      logtypes: string list,
    1.85 +      xprods: xprod list,
    1.86 +      consts: string list,
    1.87 +      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.88 +      parse_rules: (Ast.ast * Ast.ast) list,
    1.89 +      parse_translation: (string * (term list -> term)) list,
    1.90 +      print_translation: (string * (term list -> term)) list,
    1.91 +      print_rules: (Ast.ast * Ast.ast) list,
    1.92 +      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list}
    1.93 +  val mk_syn_ext: bool -> string list -> mfix list ->
    1.94 +    string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.95 +    (string * (term list -> term)) list *
    1.96 +    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.97 +    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.98 +  val syn_ext: string list -> mfix list -> string list ->
    1.99 +    (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
   1.100 +    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
   1.101 +    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   1.102 +  val syn_ext_logtypes: string list -> syn_ext
   1.103 +  val syn_ext_const_names: string list -> string list -> syn_ext
   1.104 +  val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   1.105 +  val syn_ext_trfuns: string list ->
   1.106 +    (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
   1.107 +    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
   1.108 +    -> syn_ext
   1.109 +  val pure_ext: syn_ext
   1.110 +  end;
   1.111  
   1.112 -functor SynExtFun(structure Lexicon: LEXICON and Ast: AST): SYN_EXT =
   1.113 +structure SynExt : SYN_EXT =
   1.114  struct
   1.115  
   1.116 -structure Ast = Ast;
   1.117  open Lexicon Ast;
   1.118  
   1.119 -
   1.120  (** misc definitions **)
   1.121  
   1.122  (* syntactic categories *)
   1.123 @@ -277,12 +272,12 @@
   1.124      logtypes: string list,
   1.125      xprods: xprod list,
   1.126      consts: string list,
   1.127 -    parse_ast_translation: (string * (ast list -> ast)) list,
   1.128 -    parse_rules: (ast * ast) list,
   1.129 +    parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
   1.130 +    parse_rules: (Ast.ast * Ast.ast) list,
   1.131      parse_translation: (string * (term list -> term)) list,
   1.132      print_translation: (string * (term list -> term)) list,
   1.133 -    print_rules: (ast * ast) list,
   1.134 -    print_ast_translation: (string * (ast list -> ast)) list};
   1.135 +    print_rules: (Ast.ast * Ast.ast) list,
   1.136 +    print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list};
   1.137  
   1.138  
   1.139  (* syn_ext *)
   1.140 @@ -338,3 +333,4 @@
   1.141    ([], []);
   1.142  
   1.143  end;
   1.144 +