Elimination of fully-functorial style.
authorpaulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 151109354d37a5ab
parent 1510 4588ba1b1438
child 1512 ce37c64244c0
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_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:18:51 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:24:51 1996 +0100
     1.3 @@ -6,47 +6,38 @@
     1.4  *)
     1.5  
     1.6  signature SYN_TRANS0 =
     1.7 -sig
     1.8 +  sig
     1.9    val eta_contract: bool ref
    1.10    val mk_binder_tr: string * string -> string * (term list -> term)
    1.11    val mk_binder_tr': string * string -> string * (term list -> term)
    1.12    val dependent_tr': string * string -> term list -> term
    1.13 -end;
    1.14 +  end;
    1.15  
    1.16  signature SYN_TRANS1 =
    1.17 -sig
    1.18 +  sig
    1.19    include SYN_TRANS0
    1.20 -  structure Parser: PARSER
    1.21 -  local open Parser.SynExt.Ast in
    1.22 -    val constrainAbsC: string
    1.23 -    val pure_trfuns:
    1.24 -      (string * (ast list -> ast)) list *
    1.25 +  val constrainAbsC: string
    1.26 +  val pure_trfuns:
    1.27 +      (string * (Ast.ast list -> Ast.ast)) list *
    1.28        (string * (term list -> term)) list *
    1.29        (string * (term list -> term)) list *
    1.30 -      (string * (ast list -> ast)) list
    1.31 -  end
    1.32 -end;
    1.33 +      (string * (Ast.ast list -> Ast.ast)) list
    1.34 +  end;
    1.35  
    1.36  signature SYN_TRANS =
    1.37 -sig
    1.38 +  sig
    1.39    include SYN_TRANS1
    1.40 -  local open Parser Parser.SynExt Parser.SynExt.Ast in
    1.41 -    val abs_tr': term -> term
    1.42 -    val prop_tr': bool -> term -> term
    1.43 -    val appl_ast_tr': ast * ast list -> ast
    1.44 -    val applC_ast_tr': ast * ast list -> ast
    1.45 -    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
    1.46 -    val ast_to_term: (string -> (term list -> term) option) -> ast -> term
    1.47 -  end
    1.48 -end;
    1.49 +  val abs_tr': term -> term
    1.50 +  val prop_tr': bool -> term -> term
    1.51 +  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.52 +  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.53 +  val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    1.54 +  val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
    1.55 +  end;
    1.56  
    1.57 -functor SynTransFun(structure TypeExt: TYPE_EXT and Parser: PARSER
    1.58 -  sharing TypeExt.SynExt = Parser.SynExt): SYN_TRANS =
    1.59 +structure SynTrans : SYN_TRANS =
    1.60  struct
    1.61 -
    1.62 -structure Parser = Parser;
    1.63 -open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser;
    1.64 -
    1.65 +open TypeExt Lexicon Ast SynExt Parser;
    1.66  
    1.67  (** parse (ast) translations **)
    1.68  
    1.69 @@ -313,5 +304,4 @@
    1.70      term_of ast
    1.71    end;
    1.72  
    1.73 -
    1.74  end;
     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 16 17:18:51 1996 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 16 17:24:51 1996 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  infix |-> <-| <->;
     2.5  
     2.6  signature BASIC_SYNTAX =
     2.7 -sig
     2.8 +  sig
     2.9    include AST0
    2.10    include SYN_TRANS0
    2.11    include MIXFIX0
    2.12 @@ -17,10 +17,10 @@
    2.13      op |-> of 'a * 'a |
    2.14      op <-| of 'a * 'a |
    2.15      op <-> of 'a * 'a
    2.16 -end;
    2.17 +  end;
    2.18  
    2.19  signature SYNTAX =
    2.20 -sig
    2.21 +  sig
    2.22    include AST1
    2.23    include LEXICON0
    2.24    include SYN_EXT0
    2.25 @@ -28,7 +28,6 @@
    2.26    include SYN_TRANS1
    2.27    include MIXFIX1
    2.28    include PRINTER0
    2.29 -  sharing type ast = Parser.SynExt.Ast.ast
    2.30    datatype 'a trrule =
    2.31      op |-> of 'a * 'a |
    2.32      op <-| of 'a * 'a |
    2.33 @@ -62,18 +61,12 @@
    2.34    val simple_string_of_typ: typ -> string
    2.35    val simple_pprint_typ: typ -> pprint_args -> unit
    2.36    val ambiguity_level: int ref
    2.37 -end;
    2.38 +  end;
    2.39  
    2.40 -functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
    2.41 -  and SynTrans: SYN_TRANS and Mixfix: MIXFIX and Printer: PRINTER
    2.42 -  sharing Mixfix.SynExt = SynTrans.Parser.SynExt = TypeExt.SynExt = Printer.SynExt)
    2.43 -  : SYNTAX =
    2.44 +structure Syntax : SYNTAX =
    2.45  struct
    2.46  
    2.47 -structure SynExt = TypeExt.SynExt;
    2.48 -structure Parser = SynTrans.Parser;
    2.49 -structure Lexicon = Parser.Lexicon;
    2.50 -open Lexicon SynExt SynExt.Ast Parser TypeExt SynTrans Mixfix Printer;
    2.51 +open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    2.52  
    2.53  
    2.54  (** tables of translation functions **)
     3.1 --- a/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:18:51 1996 +0100
     3.2 +++ b/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:24:51 1996 +0100
     3.3 @@ -6,28 +6,22 @@
     3.4  *)
     3.5  
     3.6  signature TYPE_EXT0 =
     3.7 -sig
     3.8 +  sig
     3.9    val raw_term_sorts: term -> (indexname * sort) list
    3.10    val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ
    3.11 -end;
    3.12 +  end;
    3.13  
    3.14  signature TYPE_EXT =
    3.15 -sig
    3.16 +  sig
    3.17    include TYPE_EXT0
    3.18 -  structure SynExt: SYN_EXT
    3.19 -  local open SynExt SynExt.Ast in
    3.20 -    val term_of_typ: bool -> typ -> term
    3.21 -    val tappl_ast_tr': ast * ast list -> ast
    3.22 -    val type_ext: syn_ext
    3.23 -  end
    3.24 -end;
    3.25 +  val term_of_typ: bool -> typ -> term
    3.26 +  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    3.27 +  val type_ext: SynExt.syn_ext
    3.28 +  end;
    3.29  
    3.30 -functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT =
    3.31 +structure TypeExt : TYPE_EXT =
    3.32  struct
    3.33 -
    3.34 -structure SynExt = SynExt;
    3.35 -open Lexicon SynExt SynExt.Ast;
    3.36 -
    3.37 +open Lexicon SynExt Ast;
    3.38  
    3.39  (** raw_term_sorts **)
    3.40  
    3.41 @@ -182,5 +176,4 @@
    3.42     [("fun", fun_ast_tr')])
    3.43    ([], []);
    3.44  
    3.45 -
    3.46  end;