Mercurial > urweb
changeset 168:25b169416ea8
Storing datatype constructors in type references past monoize
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 29 Jul 2008 15:43:17 -0400 |
parents | 2be573fec9a6 |
children | 2232ab355f66 |
files | src/cjr.sml src/cjr_env.sml src/cjr_print.sml src/cjrize.sml src/core_env.sig src/core_env.sml src/mono.sml src/mono_env.sig src/mono_env.sml src/mono_print.sml src/mono_reduce.sml src/mono_shake.sml src/mono_util.sig src/mono_util.sml src/monoize.sml |
diffstat | 15 files changed, 89 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cjr.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/cjr.sml Tue Jul 29 15:43:17 2008 -0400 @@ -33,7 +33,7 @@ TTop | TFun of typ * typ | TRecord of int - | TDatatype of int + | TDatatype of int * (string * int * typ option) list | TFfi of string * string withtype typ = typ' located
--- a/src/cjr_env.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/cjr_env.sml Tue Jul 29 15:43:17 2008 -0400 @@ -122,8 +122,8 @@ let val env = pushDatatype env x n xncs in - foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype n, loc) - | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype n, loc)), loc)) + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc) + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc)) env xncs end | DStruct (n, xts) => pushStruct env n xts
--- a/src/cjr_print.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/cjr_print.sml Tue Jul 29 15:43:17 2008 -0400 @@ -53,7 +53,7 @@ val debug = ref false -val dummyTyp = (TDatatype 0, ErrorMsg.dummySpan) +val dummyTyp = (TDatatype (0, []), ErrorMsg.dummySpan) fun p_typ' par env (t, loc) = case t of @@ -69,7 +69,7 @@ space, string "__lws_", string (Int.toString i)] - | TDatatype n => + | TDatatype (n, _) => (box [string "struct", space, string ("__lwd_" ^ #1 (E.lookupDatatype env n) ^ "_" ^ Int.toString n ^ "*")] @@ -445,7 +445,7 @@ string "})"] end - | TDatatype i => + | TDatatype (i, _) => let val (x, xncs) = E.lookupDatatype env i
--- a/src/cjrize.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/cjrize.sml Tue Jul 29 15:43:17 2008 -0400 @@ -84,7 +84,21 @@ in ((L'.TRecord si, loc), sm) end - | L.TNamed n => ((L'.TDatatype n, loc), sm) + | L.TDatatype (n, xncs) => + let + val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => + case to of + NONE => ((x, n, NONE), sm) + | SOME t => + let + val (t, sm) = cifyTyp (t, sm) + in + ((x, n, SOME t), sm) + end) + sm xncs + in + ((L'.TDatatype (n, xncs), loc), sm) + end | L.TFfi mx => ((L'.TFfi mx, loc), sm) val dummye = (L'.EPrim (Prim.Int 0), ErrorMsg.dummySpan)
--- a/src/core_env.sig Tue Jul 29 15:25:42 2008 -0400 +++ b/src/core_env.sig Tue Jul 29 15:43:17 2008 -0400 @@ -42,6 +42,9 @@ val pushCNamed : env -> string -> int -> Core.kind -> Core.con option -> env val lookupCNamed : env -> int -> string * Core.kind * Core.con option + val pushDatatype : env -> string -> int -> (string * int * Core.con option) list -> env + val lookupDatatype : env -> int -> string * (string * int * Core.con option) list + val pushERel : env -> string -> Core.con -> env val lookupERel : env -> int -> string * Core.con
--- a/src/core_env.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/core_env.sml Tue Jul 29 15:43:17 2008 -0400 @@ -61,6 +61,8 @@ relC : (string * kind) list, namedC : (string * kind * con option) IM.map, + datatypes : (string * (string * int * con option) list) IM.map, + relE : (string * con) list, namedE : (string * con * exp option * string) IM.map } @@ -69,6 +71,8 @@ relC = [], namedC = IM.empty, + datatypes = IM.empty, + relE = [], namedE = IM.empty } @@ -77,6 +81,8 @@ {relC = (x, k) :: #relC env, namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), + datatypes = #datatypes env, + relE = map (fn (x, c) => (x, lift c)) (#relE env), namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)} @@ -88,6 +94,8 @@ {relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), + datatypes = #datatypes env, + relE = #relE env, namedE = #namedE env} @@ -96,10 +104,26 @@ NONE => raise UnboundNamed n | SOME x => x +fun pushDatatype (env : env) x n xncs = + {relC = #relC env, + namedC = #namedC env, + + datatypes = IM.insert (#datatypes env, n, (x, xncs)), + + relE = #relE env, + namedE = #namedE env} + +fun lookupDatatype (env : env) n = + case IM.find (#datatypes env, n) of + NONE => raise UnboundNamed n + | SOME x => x + fun pushERel (env : env) x t = {relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + relE = (x, t) :: #relE env, namedE = #namedE env} @@ -111,6 +135,8 @@ {relC = #relC env, namedC = #namedC env, + datatypes = #datatypes env, + relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t, eo, s))} @@ -124,6 +150,7 @@ DCon (x, n, k, c) => pushCNamed env x n k (SOME c) | DDatatype (x, n, xncs) => let + val env = pushDatatype env x n xncs val env = pushCNamed env x n (KType, loc) NONE in foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
--- a/src/mono.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono.sml Tue Jul 29 15:43:17 2008 -0400 @@ -32,7 +32,7 @@ datatype typ' = TFun of typ * typ | TRecord of (string * typ) list - | TNamed of int + | TDatatype of int * (string * int * typ option) list | TFfi of string * string withtype typ = typ' located
--- a/src/mono_env.sig Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_env.sig Tue Jul 29 15:43:17 2008 -0400 @@ -34,8 +34,8 @@ exception UnboundRel of int exception UnboundNamed of int - val pushTNamed : env -> string -> int -> Mono.typ option -> env - val lookupTNamed : env -> int -> string * Mono.typ option + val pushDatatype : env -> string -> int -> (string * int * Mono.typ option) list -> env + val lookupDatatype : env -> int -> string * (string * int * Mono.typ option) list val pushERel : env -> string -> Mono.typ -> env val lookupERel : env -> int -> string * Mono.typ
--- a/src/mono_env.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_env.sml Tue Jul 29 15:43:17 2008 -0400 @@ -36,32 +36,32 @@ exception UnboundNamed of int type env = { - namedT : (string * typ option) IM.map, + datatypes : (string * (string * int * typ option) list) IM.map, relE : (string * typ) list, namedE : (string * typ * exp option * string) IM.map } val empty = { - namedT = IM.empty, + datatypes = IM.empty, relE = [], namedE = IM.empty } -fun pushTNamed (env : env) x n co = - {namedT = IM.insert (#namedT env, n, (x, co)), +fun pushDatatype (env : env) x n xncs = + {datatypes = IM.insert (#datatypes env, n, (x, xncs)), relE = #relE env, namedE = #namedE env} -fun lookupTNamed (env : env) n = - case IM.find (#namedT env, n) of +fun lookupDatatype (env : env) n = + case IM.find (#datatypes env, n) of NONE => raise UnboundNamed n | SOME x => x fun pushERel (env : env) x t = - {namedT = #namedT env, + {datatypes = #datatypes env, relE = (x, t) :: #relE env, namedE = #namedE env} @@ -71,7 +71,7 @@ handle Subscript => raise UnboundRel n fun pushENamed (env : env) x n t eo s = - {namedT = #namedT env, + {datatypes = #datatypes env, relE = #relE env, namedE = IM.insert (#namedE env, n, (x, t, eo, s))} @@ -85,10 +85,10 @@ case d of DDatatype (x, n, xncs) => let - val env = pushTNamed env x n NONE + val env = pushDatatype env x n xncs in - foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TNamed n, loc) NONE "" - | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TNamed n, loc)), loc) NONE "") + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype (n, xncs), loc) NONE "" + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype (n, xncs), loc)), loc) NONE "") env xncs end | DVal (x, n, t, e, s) => pushENamed env x n t (SOME e) s
--- a/src/mono_print.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_print.sml Tue Jul 29 15:43:17 2008 -0400 @@ -53,11 +53,11 @@ space, p_typ env t]) xcs, string "}"] - | TNamed n => + | TDatatype (n, _) => if !debug then - string (#1 (E.lookupTNamed env n) ^ "__" ^ Int.toString n) + string (#1 (E.lookupDatatype env n) ^ "__" ^ Int.toString n) else - string (#1 (E.lookupTNamed env n)) + string (#1 (E.lookupDatatype env n)) | TFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] and p_typ env = p_typ' false env @@ -164,7 +164,7 @@ fun p_datatype env (x, n, cons) = let - val env = E.pushTNamed env x n NONE + val env = E.pushDatatype env x n cons in box [string "datatype", space,
--- a/src/mono_reduce.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_reduce.sml Tue Jul 29 15:43:17 2008 -0400 @@ -62,7 +62,7 @@ fun bind (env, b) = case b of - U.Decl.NamedT (x, n, co) => E.pushTNamed env x n co + U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs | U.Decl.RelE (x, t) => E.pushERel env x t | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
--- a/src/mono_shake.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_shake.sml Tue Jul 29 15:43:17 2008 -0400 @@ -56,7 +56,7 @@ fun typ (c, s) = case c of - TNamed n => + TDatatype (n, _) => if IS.member (#con s, n) then s else
--- a/src/mono_util.sig Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_util.sig Tue Jul 29 15:43:17 2008 -0400 @@ -45,7 +45,7 @@ structure Exp : sig datatype binder = - NamedT of string * int * Mono.typ option + Datatype of string * int * (string * int * Mono.typ option) list | RelE of string * Mono.typ | NamedE of string * int * Mono.typ * Mono.exp option * string
--- a/src/mono_util.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/mono_util.sml Tue Jul 29 15:43:17 2008 -0400 @@ -57,7 +57,7 @@ in joinL compareFields (xts1, xts2) end - | (TNamed n1, TNamed n2) => Int.compare (n1, n2) + | (TDatatype (n1, _), TDatatype (n2, _)) => Int.compare (n1, n2) | (TFfi (m1, x1), TFfi (m2, x2)) => join (String.compare (m1, m2), fn () => String.compare (x1, x2)) | (TFun _, _) => LESS @@ -66,8 +66,8 @@ | (TRecord _, _) => LESS | (_, TRecord _) => GREATER - | (TNamed _, _) => LESS - | (_, TNamed _) => GREATER + | (TDatatype _, _) => LESS + | (_, TDatatype _) => GREATER and compareFields ((x1, t1), (x2, t2)) = join (String.compare (x1, x2), @@ -95,7 +95,7 @@ (x, t'))) xts, fn xts' => (TRecord xts', loc)) - | TNamed _ => S.return2 cAll + | TDatatype _ => S.return2 cAll | TFfi _ => S.return2 cAll in mft @@ -125,7 +125,7 @@ structure Exp = struct datatype binder = - NamedT of string * int * typ option + Datatype of string * int * (string * int * typ option) list | RelE of string * typ | NamedE of string * int * typ * exp option * string @@ -324,8 +324,8 @@ case #1 d' of DDatatype (x, n, xncs) => let - val ctx = bind (ctx, NamedT (x, n, NONE)) - val t = (TNamed n, #2 d') + val ctx = bind (ctx, Datatype (x, n, xncs)) + val t = (TDatatype (n, xncs), #2 d') in foldl (fn ((x, n, to), ctx) => let
--- a/src/monoize.sml Tue Jul 29 15:25:42 2008 -0400 +++ b/src/monoize.sml Tue Jul 29 15:43:17 2008 -0400 @@ -33,7 +33,7 @@ structure L = Core structure L' = Mono -val dummyTyp = (L'.TNamed 0, E.dummySpan) +val dummyTyp = (L'.TDatatype (0, []), E.dummySpan) fun monoName env (all as (c, loc)) = let @@ -65,7 +65,14 @@ (L'.TFfi ("Basis", "string"), loc) | L.CRel _ => poly () - | L.CNamed n => (L'.TNamed n, loc) + | L.CNamed n => + let + val (_, xncs) = Env.lookupDatatype env n + + val xncs = map (fn (x, n, to) => (x, n, Option.map (monoType env) to)) xncs + in + (L'.TDatatype (n, xncs), loc) + end | L.CFfi mx => (L'.TFfi mx, loc) | L.CApp _ => poly () | L.CAbs _ => poly () @@ -115,7 +122,7 @@ | L'.TFfi ("Basis", "float") => (L'.EFfiApp ("Basis", name ^ "ifyFloat", [e]), loc) | L'.TRecord [] => (L'.EPrim (Prim.String ""), loc) - | L'.TNamed _ => (L'.EPrim (Prim.String "A"), loc) + | L'.TDatatype _ => (L'.EPrim (Prim.String "A"), loc) | _ => (E.errorAt loc "Don't know how to encode attribute type"; Print.eprefaces' [("Type", MonoPrint.p_typ MonoEnv.empty tAll)];