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