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