src/Pure/Syntax/simple_syntax.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24487 e92b74b3a254
child 25999 f8bcd311d501
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      Pure/Syntax/simple_syntax.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Simple syntax for types and terms --- for bootstrapping Pure.
     6 *)
     7 
     8 signature SIMPLE_SYNTAX =
     9 sig
    10   val read_typ: string -> typ
    11   val read_term: string -> term
    12   val read_prop: string -> term
    13 end;
    14 
    15 structure SimpleSyntax: SIMPLE_SYNTAX =
    16 struct
    17 
    18 (* scanning tokens *)
    19 
    20 local
    21 
    22 val eof = Lexicon.EndToken;
    23 fun is_eof tk = tk = Lexicon.EndToken;
    24 
    25 val stopper = (eof, is_eof);
    26 val not_eof = not o is_eof;
    27 
    28 val lexicon = Scan.make_lexicon
    29   (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]);
    30 
    31 in
    32 
    33 fun read scan s =
    34   (case
    35       Symbol.explode s |>
    36       Lexicon.tokenize lexicon false |>
    37       Scan.read stopper scan of
    38     SOME x => x
    39   | NONE => error ("Malformed input: " ^ quote s));
    40 
    41 end;
    42 
    43 
    44 (* basic scanners *)
    45 
    46 fun $$ s = Scan.some (fn Lexicon.Token s' => if s = s' then SOME s else NONE | _ => NONE);
    47 fun enum1 s scan = scan -- Scan.repeat ($$ s |-- scan) >> op ::;
    48 fun enum2 s scan = scan -- Scan.repeat1 ($$ s |-- scan) >> op ::;
    49 
    50 val tfree = Scan.some (fn Lexicon.TFreeSy s => SOME s | _ => NONE);
    51 val ident = Scan.some (fn Lexicon.IdentSy s => SOME s | _ => NONE);
    52 val var =
    53   Scan.some (fn Lexicon.VarSy s => SOME (Lexicon.read_indexname (unprefix "?" s)) | _ => NONE);
    54 val long_ident = Scan.some (fn Lexicon.LongIdentSy s => SOME s | _ => NONE);
    55 val const = long_ident || ident;
    56 
    57 
    58 (* types *)
    59 
    60 (*
    61   typ  = typ1 => ... => typ1
    62        | typ1
    63   typ1 = typ2 const ... const
    64        | typ2
    65   typ2 = tfree
    66        | const
    67        | ( typ )
    68 *)
    69 
    70 fun typ x =
    71  (enum1 "=>" typ1 >> (op ---> o split_last)) x
    72 and typ1 x =
    73  (typ2 -- Scan.repeat const >> (fn (T, cs) => fold (fn c => fn U => Type (c, [U])) cs T)) x
    74 and typ2 x =
    75  (tfree >> (fn a => TFree (a, [])) ||
    76   const >> (fn c => Type (c, [])) ||
    77   $$ "(" |-- typ --| $$ ")") x;
    78 
    79 val read_typ = read typ;
    80 
    81 
    82 (* terms *)
    83 
    84 (*
    85   term  = !!ident :: typ. term
    86         | term1
    87   term1 = term2 ==> ... ==> term2
    88         | term2
    89   term2 = term3 == term2
    90         | term3 =?= term2
    91         | term3 && term2
    92         | term3
    93   term3 = ident :: typ
    94         | var :: typ
    95         | CONST const :: typ
    96         | %ident :: typ. term3
    97         | term4
    98   term4 = term5 ... term5
    99         | term5
   100   term5 = ident
   101         | var
   102         | CONST const
   103         | ( term )
   104 *)
   105 
   106 local
   107 
   108 val constraint = $$ "::" |-- typ;
   109 val idt = ident -- constraint;
   110 val bind = idt --| $$ ".";
   111 
   112 fun term env T x =
   113  ($$ "!!" |-- bind :|-- (fn v =>
   114    term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) ||
   115   term1 env T) x
   116 and term1 env T x =
   117  (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
   118   term2 env T) x
   119 and term2 env T x =
   120  (equal env "==" || equal env "=?=" ||
   121   term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   122   term3 env T) x
   123 and equal env eq x =
   124  (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
   125    Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   126 and term3 env T x =
   127  (idt >> Free ||
   128   var -- constraint >> Var ||
   129   $$ "CONST" |-- const -- constraint >> Const ||
   130   $$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
   131   term4 env T) x
   132 and term4 env T x =
   133  (term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb ||
   134   term5 env T) x
   135 and term5 env T x =
   136  (ident >> (fn a => Free (a, the_default T (AList.lookup (op =) env a))) ||
   137   var >> (fn xi => Var (xi, T)) ||
   138   $$ "CONST" |-- const >> (fn c => Const (c, T)) ||
   139   $$ "(" |-- term env T --| $$ ")") x;
   140 
   141 fun read_tm T s =
   142   let val t = read (term [] T) s in
   143     if can (Term.map_types Term.no_dummyT) t then t
   144     else error ("Unspecified types in input: " ^ quote s)
   145   end;
   146 
   147 in
   148 
   149 val read_term = read_tm dummyT;
   150 val read_prop = read_tm propT;
   151 
   152 end;
   153 
   154 end;
   155