src/Pure/Syntax/parse_tree.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 18 c9ec452ff08f
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     1 (*  Title:      Pure/Syntax/parse_tree.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 TODO:
     6   move parsetree to parser.ML
     7   move pt_to_ast before ast_to_term (sextension.ML (?))
     8   delete this file
     9 *)
    10 
    11 signature PARSE_TREE =
    12 sig
    13   structure Ast: AST
    14   structure Lexicon: LEXICON
    15   local open Ast Lexicon in
    16     datatype parsetree =
    17       Node of string * parsetree list |
    18       Tip of token
    19     val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
    20   end
    21 end;
    22 
    23 functor ParseTreeFun(structure Ast: AST and Lexicon: LEXICON): PARSE_TREE =
    24 struct
    25 
    26 structure Ast = Ast;
    27 structure Lexicon = Lexicon;
    28 open Ast Lexicon;
    29 
    30 
    31 (* datatype parsetree *)
    32 
    33 datatype parsetree =
    34   Node of string * parsetree list |
    35   Tip of token;
    36 
    37 
    38 (* pt_to_ast *)
    39 
    40 fun pt_to_ast trf pt =
    41   let
    42     fun trans a args =
    43       (case trf a of
    44         None => mk_appl (Constant a) args
    45       | Some f => f args handle exn
    46           => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));
    47 
    48     fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
    49       | ast_of (Tip tok) = Variable (str_of_token tok);
    50   in
    51     ast_of pt
    52   end;
    53 
    54 
    55 end;
    56