9 signature TYPE_EXT0 = |
9 signature TYPE_EXT0 = |
10 sig |
10 sig |
11 val sort_of_term: (sort -> sort) -> term -> sort |
11 val sort_of_term: (sort -> sort) -> term -> sort |
12 val term_sorts: (sort -> sort) -> term -> (indexname * sort) list |
12 val term_sorts: (sort -> sort) -> term -> (indexname * sort) list |
13 val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ |
13 val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ |
|
14 val type_constraint: typ -> term -> term |
14 val decode_term: (((string * int) * sort) list -> string * int -> sort) -> |
15 val decode_term: (((string * int) * sort) list -> string * int -> sort) -> |
15 (string -> bool * string) -> (string -> string option) -> |
16 (string -> bool * string) -> (string -> string option) -> |
16 (typ -> typ) -> (sort -> sort) -> term -> term |
17 (typ -> typ) -> (sort -> sort) -> term -> term |
17 val term_of_typ: bool -> typ -> term |
18 val term_of_typ: bool -> typ -> term |
18 val no_brackets: unit -> bool |
19 val no_brackets: unit -> bool |
103 in typ_of t end; |
104 in typ_of t end; |
104 |
105 |
105 |
106 |
106 (* decode_term -- transform parse tree into raw term *) |
107 (* decode_term -- transform parse tree into raw term *) |
107 |
108 |
|
109 fun type_constraint T t = |
|
110 if T = dummyT then t |
|
111 else Const ("_type_constraint_", T --> T) $ t; |
|
112 |
108 fun decode_term get_sort map_const map_free map_type map_sort tm = |
113 fun decode_term get_sort map_const map_free map_type map_sort tm = |
109 let |
114 let |
110 val sort_env = term_sorts map_sort tm; |
115 val sort_env = term_sorts map_sort tm; |
111 val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort; |
116 val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort; |
112 |
117 |
113 fun decode (Const ("_constrain", _) $ t $ typ) = |
118 fun decode (Const ("_constrain", _) $ t $ typ) = |
114 TypeInfer.constrain (decodeT typ) (decode t) |
119 type_constraint (decodeT typ) (decode t) |
115 | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) = |
120 | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) = |
116 if T = dummyT then Abs (x, decodeT typ, decode t) |
121 if T = dummyT then Abs (x, decodeT typ, decode t) |
117 else TypeInfer.constrain (decodeT typ --> dummyT) (Abs (x, map_type T, decode t)) |
122 else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t)) |
118 | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t) |
123 | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t) |
119 | decode (t $ u) = decode t $ decode u |
124 | decode (t $ u) = decode t $ decode u |
120 | decode (Const (a, T)) = |
125 | decode (Const (a, T)) = |
121 let val c = |
126 let val c = |
122 (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a)) |
127 (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a)) |