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