src/Pure/Syntax/simple_syntax.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 46214 8534f949548e
child 56245 84fc7dfa3cd4
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     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
    84   term3 = ident :: typ
    85         | var :: typ
    86         | CONST const :: typ
    87         | %ident :: typ. term3
    88         | term4
    89   term4 = term5 ... term5
    90         | term5
    91   term5 = ident
    92         | var
    93         | CONST const
    94         | ( term )
    95 *)
    96 
    97 local
    98 
    99 val constraint = $$ "::" |-- typ;
   100 val idt = ident -- constraint;
   101 val bind = idt --| $$ ".";
   102 
   103 fun term env T x =
   104  ($$ "!!" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) ||
   105   term1 env T) x
   106 and term1 env T x =
   107  (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||
   108   term2 env T) x
   109 and term2 env T x =
   110  (equal env "==" ||
   111   term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
   112   term3 env T) x
   113 and equal env eq x =
   114  (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
   115    Const (eq, Term.fastype_of t --> Term.fastype_of u --> propT) $ t $ u)) x
   116 and term3 env T x =
   117  (idt >> Free ||
   118   var -- constraint >> Var ||
   119   $$ "CONST" |-- const -- constraint >> Const ||
   120   $$ "%" |-- bind :|-- (fn v => term3 (v :: env) dummyT >> lambda (Free v)) ||
   121   term4 env T) x
   122 and term4 env T x =
   123  (term5 env dummyT -- Scan.repeat1 (term5 env dummyT) >> Term.list_comb ||
   124   term5 env T) x
   125 and term5 env T x =
   126  (ident >> (fn a => Free (a, the_default T (AList.lookup (op =) env a))) ||
   127   var >> (fn xi => Var (xi, T)) ||
   128   $$ "CONST" |-- const >> (fn c => Const (c, T)) ||
   129   $$ "(" |-- term env T --| $$ ")") x;
   130 
   131 fun read_tm T s =
   132   let val t = read (term [] T) s in
   133     if can (Term.map_types Term.no_dummyT) t then t
   134     else error ("Unspecified types in input: " ^ quote s)
   135   end;
   136 
   137 in
   138 
   139 val read_term = read_tm dummyT;
   140 val read_prop = read_tm propT;
   141 
   142 end;
   143 
   144 end;
   145