Commit 29ec4764 authored by Axel Simon's avatar Axel Simon
Browse files

finish data types with type variables

parent 126fdf68
......@@ -420,7 +420,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
env
end
val env = List.foldl genFlow envNeutral l
(*val _ = TextIO.print ("**** all envs:\n" ^ E.toString env)*)
(*val _ = TextIO.print ("**** all envs:\n" ^ E.topToString env)*)
in
E.return (1,env)
end
......@@ -476,7 +476,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
val (nts, env) = List.foldl pushField ([], env) l
(*val _ = TextIO.print ("**** rec exp, single fields:\n" ^ E.toString env ^ "\n")*)
val env = E.reduceToRecord (nts, env)
(*val _ = TextIO.print ("**** rec exp, combined:\n" ^ E.toString env ^ "\n")*)
(*val _ = TextIO.print ("**** rec exp, combined:\n" ^ E.topToString env ^ "\n")*)
in
env
end
......@@ -556,7 +556,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| SOME t =>
let
val env = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), env)
val env = E.genConstructorFlow env
val env = E.genConstructorFlow (false,env)
in
env
end
......@@ -697,17 +697,40 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| infPat (st,env) (AST.IDpat v) =
let
val (t, env) = E.pushLambdaVar' (v,env)
val t' = newFlow t
val env = E.meetBoolean (BD.meetVarImpliesVar (bvar t, bvar t'), env)
in
(1, E.pushType (false, t, env))
(1, E.pushType (false, t', env))
end
| infPat (st,env) (AST.CONpat (c, SOME p)) =
let
val (n,envPat) = infPat (st,env) p
val envPat = E.pushTop envPat
val envPat = E.reduceToFunction (envPat,1)
val envCon = E.popKappa envPat
val envCon = infExp (st,envCon) (AST.CONexp c)
val dcon = SymMap.lookup (conParents, c)
val { tdVars = vs, tdCons = cs } = SymMap.lookup (typeDefs, dcon)
val vs = SymMap.listItems vs
val t =
case SymMap.lookup (cs, c) of
NONE => raise S.UnificationFailure (
"pattern with constructor " ^
SymbolTable.getString(!SymbolTables.conTable, c) ^
" requires an argument")
| SOME t => t
val envCon = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), envCon)
val envCon = E.genConstructorFlow (true,envCon)
val env = E.meetFlow (envCon,envPat)
(*val (pStr, si) = E.topToStringSI (envPat, TVar.emptyShowInfo)
val (cStr, si) = E.topToStringSI (envCon, si)
val (rStr, si) = E.topToStringSI (env, si)
val _ = TextIO.print ("**** pattern: payload to type is:\n" ^ pStr)
val _ = TextIO.print ("**** pattern: constructor type is:\n" ^ cStr)
val _ = TextIO.print ("**** pattern: resulting type is:\n" ^ rStr)*)
val env = E.reduceToResult env
in
(n, env)
......@@ -719,7 +742,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
| infLit (st,env) (AST.FLTlit f) = E.pushType (false, FLOAT, env)
| infLit (st,env) (AST.STRlit str) = E.pushType (false, STRING, env)
| infLit (st,env) (AST.VEClit str) =
E.pushType (false, VEC (CONST (String.size str)), env)
E.pushType (false, VEC (CONST (getBitpatLitLength str)), env)
(*enforce the size constraints of the primitives*)
val primEnv = E.primitiveEnvironment (Primitives.getSymbolTypes (),
......
......@@ -48,7 +48,7 @@ structure Environment : sig
(* For a function from a type containing several type variables to an
algoebraic data type, generate implications from the arguments of the
algebraic data type to the argument of this function. *)
val genConstructorFlow : environment -> environment
val genConstructorFlow : (bool * environment) -> environment
(*given an occurrence of a symbol at a position, push its type onto the
stack and return if an instance of this type must be used; arguments are
......@@ -86,7 +86,7 @@ structure Environment : sig
(*stack: [..., tn, ..., t2, t1, t0] -> [..., SUM (tn,..t0)]*)
val reduceToSum : int * environment -> environment
(*stack: [...,t1,t2,...,tn] -> [...,(t1, ... t n-1) -> t2]*)
(*stack: [...,t1,t2,...,tn] -> [...,(t1, ... t n-1) -> tn]*)
val reduceToFunction : environment * int -> environment
(*stack: [...,t1 -> t2] -> [...t2]*)
......@@ -706,14 +706,14 @@ end = struct
val (monoTVars, monoBVars) = Scope.getMonoVars env
val (usesTVars, usesBVars) = Scope.getVarsUses (sym, env)
val funBVars = texpBVarset (t,usesBVars)
val funBVars = BD.union (monoBVars, usesBVars)
val funBVars = BD.union (texpBVarset (t,usesBVars),
BD.union (monoBVars, usesBVars))
val (scs, state) = env
val bFun = BD.projectOnto (funBVars,Scope.getFlow state)
val bFunRem = if reduceToMono then BD.projectOnto (monoBVars,bFun)
else bFun
(*val _ = TextIO.print ("projecting for " ^ SymbolTable.getString(!SymbolTables.varTable, sym) ^ ": " ^ showType t ^ " onto " ^ BD.setToString funBVars ^ ", mono " ^ BD.setToString monoBVars ^"\n")*)
val groupTVars = texpVarset (t,Scope.getVars env)
val sCons = SC.filter (groupTVars, Scope.getSize state)
val state = Scope.setSize sCons (Scope.setFlow bFunRem state)
......@@ -794,22 +794,14 @@ end = struct
fun meetSizeConstraint (update, (scs, state)) =
(scs, Scope.setSize (update (Scope.getSize state)) state)
fun genConstructorFlow env = case Scope.unwrap env of
(KAPPA {ty=FUN ([t], ALG (_,vs))}, env) =>
fun genConstructorFlow (contra, env) = case Scope.unwrap env of
(KAPPA {ty=FUN ([t], ALG (_,vs))}, _) =>
let
val dtVars = List.map (fn v => case v of
VAR p => p
| _ => raise InferenceBug) vs
val (posFlags, negFlags) =
fieldBVarsets (t,(BD.emptySet, BD.emptySet))
val env = meetBoolean (BD.meetVarSetOne posFlags o
BD.meetVarSetZero negFlags, env)
val env = List.foldl (fn ((v,f),env) =>
List.foldl (fn ((co,fv),env) => if co
then meetBoolean (BD.meetVarImpliesVar (f,fv), env)
else meetBoolean (BD.meetVarImpliesVar (fv,f), env))
env (Types.texpBVarsetFor v t)
) env dtVars
val flow = texpConstructorFlow dtVars contra t
val env = meetBoolean (fn bFun => BD.meet (flow,bFun), env)
in
env
end
......
......@@ -89,45 +89,37 @@ structure Types = struct
in (tV false (e, bs))
end
fun texpBVarsetFor var e = let
fun tV co (FUN (f1, f2), bs) = tV co (f2, List.foldl (tV (not co)) bs f1)
| tV co (SYN (syn, t), bs) = tV co (t, bs)
| tV co (ZENO, bs) = bs
| tV co (FLOAT, bs) = bs
| tV co (STRING, bs) = bs
| tV co (UNIT, bs) = bs
| tV co (VEC t, bs) = tV co (t, bs)
| tV co (CONST c, bs) = bs
| tV co (ALG (ty, l), bs) = List.foldl (tV co) bs l
| tV co (RECORD (v,b,l), bs) =
(co,b) :: List.foldl (tVF co) bs l
| tV co (MONAD (r,f,t), bs) =
tV co (r, tV (not co) (f, tV co (t, bs)))
| tV co (VAR (v,b), bs) =
if TVar.eq (v,var) then ((co,b) :: bs) else bs
and tVF co (RField {name = n, fty = t, exists = b}, bs) =
(co,b) :: tV co (t, bs)
in (tV false (e, []))
end
fun fieldBVarsets (e, pn) = let
fun tV pn (FUN (f1, f2)) = tV (List.foldl (fn (t,pn) => tV pn t) pn f1) f2
| tV pn (SYN (syn, t)) = tV pn t
| tV pn (ZENO) = pn
| tV pn (FLOAT) = pn
| tV pn (STRING) = pn
| tV pn (UNIT) = pn
| tV pn (VEC t) = tV pn t
| tV pn (CONST c) = pn
| tV pn (ALG (ty, l)) = List.foldl (fn (t,pn) => tV pn t) pn l
| tV (p,n) (RECORD (_,b,l)) =
List.foldl (fn (f,pn) => tVF pn f) (p, BD.addToSet (b,n)) l
| tV pn (MONAD (r,f,t)) = tV (tV (tV pn r) f) t
| tV (p,n) (VAR (_,b)) = (p, BD.addToSet(b,n))
and tVF (p,n) (RField {name, fty = t, exists = b}) =
tV (BD.addToSet (b,p), n) t
in (tV pn e)
end
(* Generate a Boolean function that describes the flow between the type
variables of an algebraic data type, e.g. tree[a.1], and its constructors,
e.g. Node {l.4:tree[a.2], key.5:int, r.6:tree[a.3], b.7}. When the Boolean
flag is False, the generated flow is 1->2 and 1->3 for turning an
expression to a datatype. If the flag is True, the flow is revered, which
is used when dissecting a data type. In every case, record fields are all
required and no other fields are allowed, e.g. 4 and 5 and 6 and not 7. *)
fun texpConstructorFlow vars co e = let
fun tCF co (FUN (f1, f2), bFun) = tCF co (f2, List.foldl (tCF (not co)) bFun f1)
| tCF co (SYN (syn, t), bFun) = tCF co (t, bFun)
| tCF co (ZENO, bFun) = bFun
| tCF co (FLOAT, bFun) = bFun
| tCF co (STRING, bFun) = bFun
| tCF co (UNIT, bFun) = bFun
| tCF co (VEC t, bFun) = tCF co (t, bFun)
| tCF co (CONST c, bFun) = bFun
| tCF co (ALG (ty, l), bFun) = List.foldl (tCF co) bFun l
| tCF co (RECORD (v,b,l), bFun) =
BD.meetVarZero b (List.foldl (tCFF co) bFun l)
| tCF co (MONAD (r,f,t), bFun) =
tCF co (r, tCF (not co) (f, tCF co (t, bFun)))
| tCF co (VAR (v,b), bFun) =
case List.find (fn (var,_) => TVar.eq(var,v)) vars of
NONE => raise LangTypesBug
| SOME (_,bVar) => if co
then BD.meetVarImpliesVar (b,bVar) bFun
else BD.meetVarImpliesVar (bVar,b) bFun
and tCFF co (RField {name = n, fty = t, exists = b}, bFun) =
BD.meetVarOne b (tCF co (t, bFun))
in (tCF co (e, BD.empty))
end
fun fieldOfBVar (v, e) = let
fun takeIfSome (t,fo) = case ff t of SOME f => SOME f | NONE => fo
......
......@@ -29,9 +29,6 @@ val decode = do
addrsz='0',
lock='0',
segment=DS,
mod='00',
reg/opcode='000',
rm='000',
ptrty=32}; #TODO: check
p64
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment