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