1.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/ml_types.ML Thu Jan 21 17:29:33 2016 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,215 +0,0 @@
1.4 -signature ML_TYPES = sig
1.5 - datatype ml_type =
1.6 - Var of string |
1.7 - Con of string * ml_type list |
1.8 - Tuple of ml_type list |
1.9 - Fun of ml_type * ml_type |
1.10 - Record of (string * ml_type) list
1.11 -
1.12 - val unit: ml_type
1.13 - val canonicalize: ml_type -> ml_type
1.14 -
1.15 - val read_ml_type: string -> ml_type
1.16 - val ml_type_of: Proof.context -> string -> ml_type
1.17 -
1.18 - val pretty: ml_type -> Pretty.T
1.19 -
1.20 - type env = (string * ml_type) list
1.21 - val subst: env -> ml_type -> ml_type
1.22 - val match: ml_type -> ml_type -> env -> env option
1.23 -
1.24 - val strip_fun: ml_type -> ml_type list * ml_type
1.25 -end
1.26 -
1.27 -structure ML_Types: ML_TYPES = struct
1.28 -
1.29 -datatype ml_type =
1.30 - Var of string |
1.31 - Con of string * ml_type list |
1.32 - Tuple of ml_type list |
1.33 - Fun of ml_type * ml_type |
1.34 - Record of (string * ml_type) list
1.35 -
1.36 -val unit = Con ("unit", [])
1.37 -
1.38 -type env = (string * ml_type) list
1.39 -
1.40 -fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
1.41 - | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
1.42 - | subst env (Tuple ts) = Tuple (map (subst env) ts)
1.43 - | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
1.44 - | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
1.45 -
1.46 -fun match (Var name) t env =
1.47 - (case AList.lookup op = env name of
1.48 - NONE => SOME ((name, t) :: env)
1.49 - | SOME t' => if t = t' then SOME env else NONE)
1.50 - | match (Fun (x1, y1)) (Fun (x2, y2)) env =
1.51 - Option.mapPartial (match y1 y2) (match x1 x2 env)
1.52 - | match (Con (name1, ts1)) (Con (name2, ts2)) env =
1.53 - if name1 = name2 then match_list ts1 ts2 env else NONE
1.54 - | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
1.55 - | match (Record fs1) (Record fs2) env =
1.56 - if map fst fs1 = map fst fs2 then
1.57 - match_list (map snd fs1) (map snd fs2) env
1.58 - else
1.59 - NONE
1.60 - | match _ _ _ = NONE
1.61 -and match_list [] [] env = SOME env
1.62 - | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
1.63 - | match_list _ _ _ = NONE
1.64 -
1.65 -fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
1.66 - | strip_fun t = ([], t)
1.67 -
1.68 -fun canonicalize (Var name) = Var name
1.69 - | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
1.70 - | canonicalize (Tuple []) = unit
1.71 - | canonicalize (Tuple [t]) = canonicalize t
1.72 - | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
1.73 - | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
1.74 - | canonicalize (Record []) = unit
1.75 - | canonicalize (Record es) = Record (sort_wrt fst (map (apsnd canonicalize) es))
1.76 -
1.77 -val pretty =
1.78 - let
1.79 - datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
1.80 -
1.81 - fun prec SVar _ = error "impossible"
1.82 - | prec SRoot _ = true
1.83 - | prec _ (Var _) = true
1.84 - | prec _ (Record _) = true
1.85 - | prec STuple (Con _) = true
1.86 - | prec STuple _ = false
1.87 - | prec SFun_Left (Con _) = true
1.88 - | prec SFun_Left (Tuple _) = true
1.89 - | prec SFun_Left (Fun _) = false
1.90 - | prec SCon (Con _) = true
1.91 - | prec SCon _ = false
1.92 -
1.93 - fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
1.94 -
1.95 - fun aux s t =
1.96 - (case t of
1.97 - Var id => [Pretty.str id]
1.98 - | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
1.99 - | Fun (arg, res) =>
1.100 - [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
1.101 - | Con (id, [t]) =>
1.102 - [aux SCon t, Pretty.brk 1, Pretty.str id]
1.103 - | Con (id, []) =>
1.104 - [Pretty.str id]
1.105 - | Con (id, ts) =>
1.106 - [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
1.107 - | Record es =>
1.108 - Pretty.str "{" :: Pretty.separate "," (map (fn (name, t) => Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1, aux SRoot t]) es) @ [Pretty.str "}"])
1.109 - |> Pretty.block |> par s t
1.110 - in
1.111 - aux SRoot o canonicalize
1.112 - end
1.113 -
1.114 -type token = ML_Lex.token_kind * string
1.115 -
1.116 -type 'a parser = token list -> 'a * token list
1.117 -
1.118 -fun kind k: string parser = Scan.one (equal k o fst) >> snd
1.119 -fun tok t: unit parser = Scan.one (equal t) >> K ()
1.120 -fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
1.121 -val open_parenthesis: unit parser = keyword "("
1.122 -val closed_parenthesis: unit parser = keyword ")"
1.123 -val open_brace: unit parser = keyword "{"
1.124 -val closed_brace: unit parser = keyword "}"
1.125 -val colon: unit parser = keyword ":"
1.126 -val comma: unit parser = keyword ","
1.127 -val arrow: unit parser = keyword "->"
1.128 -val asterisk: unit parser = tok (ML_Lex.Ident, "*")
1.129 -
1.130 -val ident: string parser =
1.131 - kind ML_Lex.Long_Ident ||
1.132 - Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
1.133 -
1.134 -fun intersep p sep =
1.135 - (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
1.136 -
1.137 -val typ =
1.138 - let
1.139 - (* code partly lifted from Spec_Check *)
1.140 - fun make_con [] = raise Empty
1.141 - | make_con [c] = c
1.142 - | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
1.143 -
1.144 - fun typ s = (func || tuple || typ_single) s
1.145 - and typ_arg s = (tuple || typ_single) s
1.146 - and typ_single s = (con || typ_basic) s
1.147 - and typ_basic s =
1.148 - (var
1.149 - || open_brace |-- record --| closed_brace
1.150 - || open_parenthesis |-- typ --| closed_parenthesis) s
1.151 - and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
1.152 - and var s = (kind ML_Lex.Type_Var >> Var) s
1.153 - and con s = ((con_nest
1.154 - || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
1.155 - || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
1.156 - >> (make_con o rev)) s
1.157 - and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
1.158 - and func s = (typ_arg --| arrow -- typ >> Fun) s
1.159 - and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
1.160 - and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
1.161 - >> (fn (t, tl) => Tuple (t :: tl))) s
1.162 - in typ end
1.163 -
1.164 -fun read_binding s =
1.165 - let
1.166 - val colon = (ML_Lex.Keyword, ":")
1.167 - val semicolon = (ML_Lex.Keyword, ";")
1.168 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
1.169 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
1.170 - val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
1.171 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
1.172 - val all = junk |-- Scan.finite stopper typ
1.173 - val (typ, rest) = all toks
1.174 - in
1.175 - if null rest then
1.176 - typ
1.177 - else
1.178 - error "Could not fully parse type"
1.179 - end
1.180 -
1.181 -fun read_ml_type s =
1.182 - let
1.183 - (* FIXME deduplicate *)
1.184 - val semicolon = (ML_Lex.Keyword, ";")
1.185 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
1.186 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
1.187 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
1.188 - val all = Scan.finite stopper typ
1.189 - val (typ, rest) = all toks
1.190 - in
1.191 - if null rest then
1.192 - typ
1.193 - else
1.194 - error "Could not fully parse type"
1.195 - end
1.196 -
1.197 -fun ml_type_of ctxt s =
1.198 - let
1.199 - (* code partly lifted from Spec_Check *)
1.200 - val return = Unsynchronized.ref NONE
1.201 - val s = "(fn () => (" ^ s ^ "))"
1.202 - val use_context: use_context =
1.203 - {tune_source = #tune_source ML_Env.local_context,
1.204 - name_space = #name_space ML_Env.local_context,
1.205 - str_of_pos = #str_of_pos ML_Env.local_context,
1.206 - print = fn r => return := SOME r,
1.207 - error = #error ML_Env.local_context}
1.208 - val _ =
1.209 - Context.setmp_thread_data (SOME (Context.Proof ctxt))
1.210 - (fn () => Secure.use_text use_context (0, "generated code") true s) ()
1.211 - val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
1.212 - in
1.213 - typ
1.214 - end
1.215 -
1.216 -end
1.217 -
1.218 -type ml_type = ML_Types.ml_type