src/Pure/Tools/am_util.ML
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14)
changeset 16842 5979c46853d1
parent 16781 663235466562
child 17799 1cc6e60bd5ff
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Tools/am_util.ML
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 signature AM_UTIL = sig
     7 
     8     type naming = string -> int
     9 
    10     exception Parse of string
    11     exception Tokenize
    12 
    13     (* takes a naming for the constants *)
    14     val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
    15 
    16     (* takes a naming for the constants and one for the free variables *)
    17     val read_term : naming -> naming -> string -> AbstractMachine.term
    18 
    19     val term_ord : AbstractMachine.term * AbstractMachine.term -> order
    20 
    21 end
    22 
    23 structure AM_Util : AM_UTIL =
    24 struct
    25 
    26 fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
    27   | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
    28   | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
    29       prod_ord term_ord term_ord (a1, a2)
    30   | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
    31   | term_ord (AbstractMachine.Const _, _) = LESS
    32   | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
    33   | term_ord (AbstractMachine.Var _, _) = LESS
    34   | term_ord (AbstractMachine.App _, AbstractMachine.Abs _) = LESS
    35   | term_ord (AbstractMachine.App _, _) = GREATER
    36   | term_ord (AbstractMachine.Abs _, _) = LESS
    37 
    38 type naming = string -> int
    39 
    40 datatype token =
    41   TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
    42   TokenLambda | TokenDot | TokenNone | TokenEq
    43 
    44 exception Tokenize;
    45 
    46 fun tokenize s =
    47     let
    48         val s = String.explode s
    49         fun str c = Char.toString c
    50         fun app s c = s^(str c)
    51         fun tz TokenNone [] = []
    52           | tz x [] = [x]
    53           | tz TokenNone (c::cs) =
    54             if Char.isSpace c then tz TokenNone cs
    55             else if Char.isLower c then (tz (TokenVar (str c)) cs)
    56             else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
    57             else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
    58             else if c = #"." then (TokenDot :: (tz TokenNone cs))
    59             else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
    60             else if c = #")" then (TokenRight :: (tz TokenNone cs))
    61             else if c = #"=" then (TokenEq :: (tz TokenNone cs))
    62             else raise Tokenize
    63           | tz (TokenConst s) (c::cs) =
    64             if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
    65             else (TokenConst s)::(tz TokenNone (c::cs))
    66           | tz (TokenVar s) (c::cs) =
    67             if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
    68             else (TokenVar s)::(tz TokenNone (c::cs))
    69           | tz _ _ = raise Tokenize
    70     in
    71         tz TokenNone s
    72     end
    73 
    74 exception Parse of string;
    75 
    76 fun cons x xs =
    77   if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
    78   else (x::xs)
    79 
    80 fun parse_pattern f pvars ((TokenConst c)::ts) =
    81     let
    82         val (pvars, ts, plist) = parse_pattern_list f pvars ts
    83     in
    84         (pvars, ts, AbstractMachine.PConst (f c, plist))
    85     end
    86   | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
    87 and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
    88   | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
    89   | parse_pattern_single f pvars (TokenLeft::ts) =
    90     let
    91         val (pvars, ts, p) = parse_pattern f pvars ts
    92     in
    93         case ts of
    94             TokenRight::ts => (pvars, ts, p)
    95           | _ => raise (Parse "parse_pattern_single: closing bracket expected")
    96     end
    97   | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
    98 and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
    99   | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
   100   | parse_pattern_list f pvars ts =
   101     let
   102         val (pvars, ts, p) = parse_pattern_single f pvars ts
   103         val (pvars, ts, ps) = parse_pattern_list f pvars ts
   104     in
   105         (pvars, ts, p::ps)
   106     end
   107 
   108 fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
   109   | app_terms x [] = x
   110 
   111 fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
   112   | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
   113   | parse_term_single f vars (TokenLeft::ts) =
   114     let
   115         val (ts, term) = parse_term f vars ts
   116     in
   117         case ts of
   118             TokenRight::ts => (ts, term)
   119           | _ => raise Parse ("parse_term_single: closing bracket expected")
   120     end
   121   | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
   122     let
   123         val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
   124     in
   125         (ts, AbstractMachine.Abs term)
   126     end
   127   | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
   128 and parse_term_list f vars [] = ([], [])
   129   | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
   130   | parse_term_list f vars ts =
   131     let
   132         val (ts, term) = parse_term_single f vars ts
   133         val (ts, terms) = parse_term_list f vars ts
   134     in
   135         (ts, term::terms)
   136     end
   137 and parse_term f vars ts =
   138     let
   139         val (ts, terms) = parse_term_list f vars ts
   140     in
   141         case terms of
   142             [] => raise (Parse "parse_term: no term found")
   143           | (t::terms) => (ts, app_terms t terms)
   144     end
   145 
   146 fun read_rule f s =
   147     let
   148         val t = tokenize s
   149         val (v, ts, pattern) = parse_pattern f [] t
   150         fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
   151           | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
   152     in
   153         case ts of
   154             TokenEq::ts =>
   155             let
   156                 val (ts, term) = parse_term f (vars v) ts
   157             in
   158                 case ts of
   159                     [] => (pattern, term)
   160                   | _ => raise (Parse "read_rule: still tokens left, end expected")
   161             end
   162           | _ => raise (Parse ("read_rule: = expected"))
   163     end
   164 
   165 fun read_term f g s =
   166     let
   167         val t = tokenize s
   168         val (ts, term) = parse_term f g t
   169     in
   170         case ts of
   171             [] => term
   172           | _ => raise (Parse ("read_term: still tokens left, end expected"))
   173     end
   174 
   175 end