1 signature ML_TYPES = sig
4 Con of string * ml_type list |
5 Tuple of ml_type list |
6 Fun of ml_type * ml_type |
7 Record of (string * ml_type) list
10 val canonicalize: ml_type -> ml_type
12 val read_ml_type: string -> ml_type
13 val ml_type_of: Proof.context -> string -> ml_type
15 val pretty: ml_type -> Pretty.T
17 type env = (string * ml_type) list
18 val subst: env -> ml_type -> ml_type
19 val match: ml_type -> ml_type -> env -> env option
21 val strip_fun: ml_type -> ml_type list * ml_type
24 structure ML_Types: ML_TYPES = struct
28 Con of string * ml_type list |
29 Tuple of ml_type list |
30 Fun of ml_type * ml_type |
31 Record of (string * ml_type) list
33 val unit = Con ("unit", [])
35 type env = (string * ml_type) list
37 fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
38 | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
39 | subst env (Tuple ts) = Tuple (map (subst env) ts)
40 | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
41 | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
43 fun match (Var name) t env =
44 (case AList.lookup op = env name of
45 NONE => SOME ((name, t) :: env)
46 | SOME t' => if t = t' then SOME env else NONE)
47 | match (Fun (x1, y1)) (Fun (x2, y2)) env =
48 Option.mapPartial (match y1 y2) (match x1 x2 env)
49 | match (Con (name1, ts1)) (Con (name2, ts2)) env =
50 if name1 = name2 then match_list ts1 ts2 env else NONE
51 | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
52 | match (Record fs1) (Record fs2) env =
53 if map fst fs1 = map fst fs2 then
54 match_list (map snd fs1) (map snd fs2) env
58 and match_list [] [] env = SOME env
59 | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
60 | match_list _ _ _ = NONE
62 fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
63 | strip_fun t = ([], t)
65 fun canonicalize (Var name) = Var name
66 | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
67 | canonicalize (Tuple []) = unit
68 | canonicalize (Tuple [t]) = canonicalize t
69 | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
70 | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
71 | canonicalize (Record []) = unit
72 | canonicalize (Record es) = Record (sort_wrt fst (map (apsnd canonicalize) es))
76 datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
78 fun prec SVar _ = error "impossible"
80 | prec _ (Var _) = true
81 | prec _ (Record _) = true
82 | prec STuple (Con _) = true
83 | prec STuple _ = false
84 | prec SFun_Left (Con _) = true
85 | prec SFun_Left (Tuple _) = true
86 | prec SFun_Left (Fun _) = false
87 | prec SCon (Con _) = true
90 fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
94 Var id => [Pretty.str id]
95 | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
97 [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
99 [aux SCon t, Pretty.brk 1, Pretty.str id]
103 [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
105 Pretty.str "{" :: Pretty.separate "," (map (fn (name, t) => Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1, aux SRoot t]) es) @ [Pretty.str "}"])
106 |> Pretty.block |> par s t
108 aux SRoot o canonicalize
111 type token = ML_Lex.token_kind * string
113 type 'a parser = token list -> 'a * token list
115 fun kind k: string parser = Scan.one (equal k o fst) >> snd
116 fun tok t: unit parser = Scan.one (equal t) >> K ()
117 fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
118 val open_parenthesis: unit parser = keyword "("
119 val closed_parenthesis: unit parser = keyword ")"
120 val open_brace: unit parser = keyword "{"
121 val closed_brace: unit parser = keyword "}"
122 val colon: unit parser = keyword ":"
123 val comma: unit parser = keyword ","
124 val arrow: unit parser = keyword "->"
125 val asterisk: unit parser = tok (ML_Lex.Ident, "*")
127 val ident: string parser =
128 kind ML_Lex.Long_Ident ||
129 Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
132 (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
136 (* code partly lifted from Spec_Check *)
137 fun make_con [] = raise Empty
139 | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
141 fun typ s = (func || tuple || typ_single) s
142 and typ_arg s = (tuple || typ_single) s
143 and typ_single s = (con || typ_basic) s
146 || open_brace |-- record --| closed_brace
147 || open_parenthesis |-- typ --| closed_parenthesis) s
148 and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
149 and var s = (kind ML_Lex.Type_Var >> Var) s
150 and con s = ((con_nest
151 || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
152 || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
153 >> (make_con o rev)) s
154 and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
155 and func s = (typ_arg --| arrow -- typ >> Fun) s
156 and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
157 and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
158 >> (fn (t, tl) => Tuple (t :: tl))) s
163 val colon = (ML_Lex.Keyword, ":")
164 val semicolon = (ML_Lex.Keyword, ";")
165 fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
166 val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
167 val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
168 val stopper = Scan.stopper (K semicolon) (equal semicolon)
169 val all = junk |-- Scan.finite stopper typ
170 val (typ, rest) = all toks
175 error "Could not fully parse type"
180 (* FIXME deduplicate *)
181 val semicolon = (ML_Lex.Keyword, ";")
182 fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
183 val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
184 val stopper = Scan.stopper (K semicolon) (equal semicolon)
185 val all = Scan.finite stopper typ
186 val (typ, rest) = all toks
191 error "Could not fully parse type"
194 fun ml_type_of ctxt s =
196 (* code partly lifted from Spec_Check *)
197 val return = Unsynchronized.ref NONE
198 val s = "(fn () => (" ^ s ^ "))"
199 val use_context: use_context =
200 {tune_source = #tune_source ML_Env.local_context,
201 name_space = #name_space ML_Env.local_context,
202 str_of_pos = #str_of_pos ML_Env.local_context,
203 print = fn r => return := SOME r,
204 error = #error ML_Env.local_context}
206 Context.setmp_thread_data (SOME (Context.Proof ctxt))
207 (fn () => Secure.use_text use_context (0, "generated code") true s) ()
208 val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
215 type ml_type = ML_Types.ml_type