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