src/Pure/Syntax/parse_tree.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 18 c9ec452ff08f
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/parse_tree.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     4
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
TODO:
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     6
  move parsetree to parser.ML
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     7
  move pt_to_ast before ast_to_term (sextension.ML (?))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     8
  delete this file
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
signature PARSE_TREE =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
sig
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    13
  structure Ast: AST
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  structure Lexicon: LEXICON
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    15
  local open Ast Lexicon in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    16
    datatype parsetree =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    17
      Node of string * parsetree list |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    18
      Tip of token
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    19
    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    23
functor ParseTreeFun(structure Ast: AST and Lexicon: LEXICON): PARSE_TREE =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    26
structure Ast = Ast;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
structure Lexicon = Lexicon;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    28
open Ast Lexicon;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    31
(* datatype parsetree *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    33
datatype parsetree =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    34
  Node of string * parsetree list |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    35
  Tip of token;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
(* pt_to_ast *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
fun pt_to_ast trf pt =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
    fun trans a args =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
      (case trf a of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
        None => mk_appl (Constant a) args
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    45
      | Some f => f args handle exn
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    46
          => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
    fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
      | ast_of (Tip tok) = Variable (str_of_token tok);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    51
    ast_of pt
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56