src/Pure/Tools/am_util.ML
changeset 16842 5979c46853d1
parent 16781 663235466562
child 17799 1cc6e60bd5ff
     1.1 --- a/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/Tools/am_util.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -4,11 +4,11 @@
     1.4  *)
     1.5  
     1.6  signature AM_UTIL = sig
     1.7 -    
     1.8 +
     1.9      type naming = string -> int
    1.10  
    1.11      exception Parse of string
    1.12 -    exception Tokenize 
    1.13 +    exception Tokenize
    1.14  
    1.15      (* takes a naming for the constants *)
    1.16      val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
    1.17 @@ -25,7 +25,8 @@
    1.18  
    1.19  fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
    1.20    | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
    1.21 -  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) = (prod_ord term_ord term_ord) (a1, a2)
    1.22 +  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
    1.23 +      prod_ord term_ord term_ord (a1, a2)
    1.24    | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
    1.25    | term_ord (AbstractMachine.Const _, _) = LESS
    1.26    | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
    1.27 @@ -36,68 +37,72 @@
    1.28  
    1.29  type naming = string -> int
    1.30  
    1.31 -datatype token = TokenConst of string | TokenLeft | TokenRight | TokenVar of string | TokenLambda | TokenDot | TokenNone | TokenEq
    1.32 +datatype token =
    1.33 +  TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
    1.34 +  TokenLambda | TokenDot | TokenNone | TokenEq
    1.35  
    1.36  exception Tokenize;
    1.37  
    1.38  fun tokenize s =
    1.39      let
    1.40 -	val s = String.explode s
    1.41 -	fun str c = Char.toString c
    1.42 -	fun app s c = s^(str c)
    1.43 -	fun tz TokenNone [] = []
    1.44 -	  | tz x [] = [x]
    1.45 -	  | tz TokenNone (c::cs) = 
    1.46 -	    if Char.isSpace c then tz TokenNone cs
    1.47 -	    else if Char.isLower c then (tz (TokenVar (str c)) cs)
    1.48 -	    else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
    1.49 -	    else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
    1.50 -	    else if c = #"." then (TokenDot :: (tz TokenNone cs))
    1.51 -	    else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
    1.52 -	    else if c = #")" then (TokenRight :: (tz TokenNone cs))
    1.53 -	    else if c = #"=" then (TokenEq :: (tz TokenNone cs))
    1.54 -	    else raise Tokenize
    1.55 -	  | tz (TokenConst s) (c::cs) = 
    1.56 -	    if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
    1.57 -	    else (TokenConst s)::(tz TokenNone (c::cs))
    1.58 -	  | tz (TokenVar s) (c::cs) = 
    1.59 -	    if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
    1.60 -	    else (TokenVar s)::(tz TokenNone (c::cs))
    1.61 -	  | tz _ _ = raise Tokenize
    1.62 +        val s = String.explode s
    1.63 +        fun str c = Char.toString c
    1.64 +        fun app s c = s^(str c)
    1.65 +        fun tz TokenNone [] = []
    1.66 +          | tz x [] = [x]
    1.67 +          | tz TokenNone (c::cs) =
    1.68 +            if Char.isSpace c then tz TokenNone cs
    1.69 +            else if Char.isLower c then (tz (TokenVar (str c)) cs)
    1.70 +            else if Char.isAlphaNum c then (tz (TokenConst (str c)) cs)
    1.71 +            else if c = #"%" then (TokenLambda :: (tz TokenNone cs))
    1.72 +            else if c = #"." then (TokenDot :: (tz TokenNone cs))
    1.73 +            else if c = #"(" then (TokenLeft :: (tz TokenNone cs))
    1.74 +            else if c = #")" then (TokenRight :: (tz TokenNone cs))
    1.75 +            else if c = #"=" then (TokenEq :: (tz TokenNone cs))
    1.76 +            else raise Tokenize
    1.77 +          | tz (TokenConst s) (c::cs) =
    1.78 +            if Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
    1.79 +            else (TokenConst s)::(tz TokenNone (c::cs))
    1.80 +          | tz (TokenVar s) (c::cs) =
    1.81 +            if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
    1.82 +            else (TokenVar s)::(tz TokenNone (c::cs))
    1.83 +          | tz _ _ = raise Tokenize
    1.84      in
    1.85 -	tz TokenNone s
    1.86 +        tz TokenNone s
    1.87      end
    1.88  
    1.89  exception Parse of string;
    1.90  
    1.91 -fun cons x xs = if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x)) else (x::xs)
    1.92 +fun cons x xs =
    1.93 +  if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
    1.94 +  else (x::xs)
    1.95  
    1.96 -fun parse_pattern f pvars ((TokenConst c)::ts) = 
    1.97 +fun parse_pattern f pvars ((TokenConst c)::ts) =
    1.98      let
    1.99 -	val (pvars, ts, plist) = parse_pattern_list f pvars ts
   1.100 +        val (pvars, ts, plist) = parse_pattern_list f pvars ts
   1.101      in
   1.102 -	(pvars, ts, AbstractMachine.PConst (f c, plist))
   1.103 +        (pvars, ts, AbstractMachine.PConst (f c, plist))
   1.104      end
   1.105    | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
   1.106 -and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)	
   1.107 +and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
   1.108    | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
   1.109 -  | parse_pattern_single f pvars (TokenLeft::ts) = 
   1.110 +  | parse_pattern_single f pvars (TokenLeft::ts) =
   1.111      let
   1.112 -	val (pvars, ts, p) = parse_pattern f pvars ts
   1.113 +        val (pvars, ts, p) = parse_pattern f pvars ts
   1.114      in
   1.115 -	case ts of
   1.116 -	    TokenRight::ts => (pvars, ts, p)
   1.117 -	  | _ => raise (Parse "parse_pattern_single: closing bracket expected")
   1.118 +        case ts of
   1.119 +            TokenRight::ts => (pvars, ts, p)
   1.120 +          | _ => raise (Parse "parse_pattern_single: closing bracket expected")
   1.121      end
   1.122    | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
   1.123  and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
   1.124    | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
   1.125 -  | parse_pattern_list f pvars ts = 
   1.126 +  | parse_pattern_list f pvars ts =
   1.127      let
   1.128 -	val (pvars, ts, p) = parse_pattern_single f pvars ts
   1.129 -	val (pvars, ts, ps) = parse_pattern_list f pvars ts
   1.130 +        val (pvars, ts, p) = parse_pattern_single f pvars ts
   1.131 +        val (pvars, ts, ps) = parse_pattern_list f pvars ts
   1.132      in
   1.133 -	(pvars, ts, p::ps)
   1.134 +        (pvars, ts, p::ps)
   1.135      end
   1.136  
   1.137  fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
   1.138 @@ -105,66 +110,66 @@
   1.139  
   1.140  fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
   1.141    | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
   1.142 -  | parse_term_single f vars (TokenLeft::ts) = 
   1.143 +  | parse_term_single f vars (TokenLeft::ts) =
   1.144      let
   1.145 -	val (ts, term) = parse_term f vars ts
   1.146 +        val (ts, term) = parse_term f vars ts
   1.147      in
   1.148 -	case ts of 
   1.149 -	    TokenRight::ts => (ts, term)
   1.150 -	  | _ => raise Parse ("parse_term_single: closing bracket expected")
   1.151 +        case ts of
   1.152 +            TokenRight::ts => (ts, term)
   1.153 +          | _ => raise Parse ("parse_term_single: closing bracket expected")
   1.154      end
   1.155 -  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) = 
   1.156 +  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
   1.157      let
   1.158 -	val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
   1.159 +        val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
   1.160      in
   1.161 -	(ts, AbstractMachine.Abs term)
   1.162 +        (ts, AbstractMachine.Abs term)
   1.163      end
   1.164    | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
   1.165  and parse_term_list f vars [] = ([], [])
   1.166    | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
   1.167 -  | parse_term_list f vars ts = 
   1.168 +  | parse_term_list f vars ts =
   1.169      let
   1.170 -	val (ts, term) = parse_term_single f vars ts
   1.171 -	val (ts, terms) = parse_term_list f vars ts
   1.172 +        val (ts, term) = parse_term_single f vars ts
   1.173 +        val (ts, terms) = parse_term_list f vars ts
   1.174      in
   1.175 -	(ts, term::terms)
   1.176 +        (ts, term::terms)
   1.177      end
   1.178 -and parse_term f vars ts = 
   1.179 +and parse_term f vars ts =
   1.180      let
   1.181 -	val (ts, terms) = parse_term_list f vars ts
   1.182 +        val (ts, terms) = parse_term_list f vars ts
   1.183      in
   1.184 -	case terms of 
   1.185 -	    [] => raise (Parse "parse_term: no term found")
   1.186 -	  | (t::terms) => (ts, app_terms t terms)
   1.187 +        case terms of
   1.188 +            [] => raise (Parse "parse_term: no term found")
   1.189 +          | (t::terms) => (ts, app_terms t terms)
   1.190      end
   1.191  
   1.192 -fun read_rule f s = 
   1.193 +fun read_rule f s =
   1.194      let
   1.195 -	val t = tokenize s
   1.196 -	val (v, ts, pattern) = parse_pattern f [] t
   1.197 -	fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
   1.198 -	  | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
   1.199 +        val t = tokenize s
   1.200 +        val (v, ts, pattern) = parse_pattern f [] t
   1.201 +        fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
   1.202 +          | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
   1.203      in
   1.204 -	case ts of 
   1.205 -	    TokenEq::ts => 
   1.206 -	    let
   1.207 -		val (ts, term) = parse_term f (vars v) ts
   1.208 -	    in
   1.209 -		case ts of 
   1.210 -		    [] => (pattern, term)
   1.211 -		  | _ => raise (Parse "read_rule: still tokens left, end expected")
   1.212 -	    end
   1.213 -	  | _ => raise (Parse ("read_rule: = expected"))
   1.214 +        case ts of
   1.215 +            TokenEq::ts =>
   1.216 +            let
   1.217 +                val (ts, term) = parse_term f (vars v) ts
   1.218 +            in
   1.219 +                case ts of
   1.220 +                    [] => (pattern, term)
   1.221 +                  | _ => raise (Parse "read_rule: still tokens left, end expected")
   1.222 +            end
   1.223 +          | _ => raise (Parse ("read_rule: = expected"))
   1.224      end
   1.225  
   1.226 -fun read_term f g s = 
   1.227 +fun read_term f g s =
   1.228      let
   1.229 -	val t = tokenize s
   1.230 -	val (ts, term) = parse_term f g t
   1.231 +        val t = tokenize s
   1.232 +        val (ts, term) = parse_term f g t
   1.233      in
   1.234 -	case ts of 
   1.235 -	    [] => term
   1.236 -	  | _ => raise (Parse ("read_term: still tokens left, end expected"))
   1.237 +        case ts of
   1.238 +            [] => term
   1.239 +          | _ => raise (Parse ("read_term: still tokens left, end expected"))
   1.240      end
   1.241  
   1.242  end