Simple syntax for types and terms --- for bootstrapping Pure.
authorwenzelm
Mon Aug 13 00:17:57 2007 +0200 (2007-08-13)
changeset 24236d8b05073edc7
parent 24235 aea5c389a2f5
child 24237 4bf3e084d9b5
Simple syntax for types and terms --- for bootstrapping Pure.
src/Pure/Syntax/simple_syntax.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Mon Aug 13 00:17:57 2007 +0200
     1.3 @@ -0,0 +1,136 @@
     1.4 +(*  Title:      Pure/Syntax/simple_syntax.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Simple syntax for types and terms --- for bootstrapping Pure.
     1.9 +*)
    1.10 +
    1.11 +signature SIMPLE_SYNTAX =
    1.12 +sig
    1.13 +  val read_typ: string -> typ
    1.14 +  val read_term: string -> term
    1.15 +  val read_prop: string -> term
    1.16 +end;
    1.17 +
    1.18 +structure SimpleSyntax: SIMPLE_SYNTAX =
    1.19 +struct
    1.20 +
    1.21 +(* scanning tokens *)
    1.22 +
    1.23 +local
    1.24 +
    1.25 +val eof = Lexicon.EndToken;
    1.26 +fun is_eof tk = tk = Lexicon.EndToken;
    1.27 +
    1.28 +val stopper = (eof, is_eof);
    1.29 +val not_eof = not o is_eof;
    1.30 +
    1.31 +val lexicon = Scan.make_lexicon
    1.32 +  (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "CONST"]);
    1.33 +
    1.34 +in
    1.35 +
    1.36 +fun read scan s =
    1.37 +  (case
    1.38 +      Symbol.explode s |>
    1.39 +      Lexicon.tokenize lexicon false |> filter not_eof |>
    1.40 +      Scan.read stopper scan of
    1.41 +    SOME x => x
    1.42 +  | NONE => error ("Bad input: " ^ quote s));
    1.43 +
    1.44 +end;
    1.45 +
    1.46 +
    1.47 +(* basic scanners *)
    1.48 +
    1.49 +fun $$ s = Scan.some (fn Lexicon.Token s' => if s = s' then SOME s else NONE | _ => NONE);
    1.50 +fun enum1 s scan = scan -- Scan.repeat ($$ s |-- scan) >> op ::;
    1.51 +fun enum2 s scan = scan -- Scan.repeat1 ($$ s |-- scan) >> op ::;
    1.52 +
    1.53 +val tfree = Scan.some (fn Lexicon.TFreeSy s => SOME s | _ => NONE);
    1.54 +val ident = Scan.some (fn Lexicon.IdentSy s => SOME s | _ => NONE);
    1.55 +val long_ident = Scan.some (fn Lexicon.LongIdentSy s => SOME s | _ => NONE);
    1.56 +val const = long_ident || ident;
    1.57 +
    1.58 +
    1.59 +(* types *)
    1.60 +
    1.61 +(*
    1.62 +  typ  = typ1 => ... => typ1
    1.63 +  typ1 = typ2 const ... const
    1.64 +  typ2 = tfree | const | "(" typ ")"
    1.65 +*)
    1.66 +
    1.67 +fun typ x =
    1.68 + (enum1 "=>" typ1 >> (op ---> o split_last)) x
    1.69 +and typ1 x =
    1.70 + (typ2 -- Scan.repeat const >> (fn (T, cs) => fold (fn c => fn U => Type (c, [U])) cs T)) x
    1.71 +and typ2 x =
    1.72 + (tfree >> (fn a => TFree (a, [])) ||
    1.73 +  const >> (fn c => Type (c, [])) ||
    1.74 +  $$ "(" |-- typ --| $$ ")") x;
    1.75 +
    1.76 +val read_typ = read typ;
    1.77 +
    1.78 +
    1.79 +(* terms *)
    1.80 +
    1.81 +(*
    1.82 +  term  = !!ident :: typ. term
    1.83 +        | term1
    1.84 +  term1 = term2 ==> ... ==> term2
    1.85 +        | term2
    1.86 +  term2 = term3 == term2
    1.87 +        | term3 =?= term2
    1.88 +        | term3
    1.89 +  term3 = ident :: typ
    1.90 +        | CONST const :: typ
    1.91 +        | %ident :: typ. term3
    1.92 +        | term4
    1.93 +  term4 = term5 ... term5
    1.94 +        | term5
    1.95 +  term5 = ident
    1.96 +        | CONST const
    1.97 +        | "(" term ")"
    1.98 +*)
    1.99 +
   1.100 +local
   1.101 +
   1.102 +val constraint = $$ "::" |-- typ;
   1.103 +val var = ident -- constraint;
   1.104 +val bind = var --| $$ ".";
   1.105 +
   1.106 +in
   1.107 +
   1.108 +fun term env T x =
   1.109 + ($$ "!!" |-- bind :|-- (fn v =>
   1.110 +   term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) ||
   1.111 +  term1 env T) x
   1.112 +and term1 env T x =
   1.113 + (enum2 "==>" (term2 env propT) >> foldr1 (fn (A, B) => Term.implies $ A $ B) ||
   1.114 +  term2 env T) x
   1.115 +and term2 env T x =
   1.116 + (equal env "==" || equal env "=?=" || term3 env T) x
   1.117 +and equal env eq x =
   1.118 + (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
   1.119 +   Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   1.120 +and term3 env T x =
   1.121 + (var >> Free ||
   1.122 +  $$ "CONST" |-- const -- constraint >> Const ||
   1.123 +  $$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
   1.124 +  term4 env T) x
   1.125 +and term4 env T x =
   1.126 + (term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb ||
   1.127 +  term5 env T) x
   1.128 +and term5 env T x =
   1.129 + (ident >> (fn a => Free (a, the_default T (AList.lookup (op =) env a))) ||
   1.130 +  $$ "CONST" |-- const >> (fn c => Const (c, T)) ||
   1.131 +  $$ "(" |-- term env T --| $$ ")") x;
   1.132 +
   1.133 +val read_term = read (term [] dummyT);
   1.134 +val read_prop = read (term [] propT);
   1.135 +
   1.136 +end;
   1.137 +
   1.138 +end;
   1.139 +