Commit 126fdf68 authored by Axel Simon's avatar Axel Simon
Browse files

broke type inference for the greater good

parent ddb9fd14
......@@ -56,7 +56,7 @@ end = struct
| DECODEdecl d => insertDecode d
| LETRECdecl d => valuedecls := d::(!valuedecls)
| EXPORTdecl es => exports := !exports@es
| DATATYPEdecl (n, cons) =>
| DATATYPEdecl (n, tvars, cons) =>
(datatypes := (n, cons)::(!datatypes)
;updateConstructors (n, cons))
......
......@@ -46,7 +46,7 @@ functor MkAst (Core: AST_CORE) = struct
MARKdecl of decl mark
| GRANULARITYdecl of IntInf.int
| TYPEdecl of syn_bind * ty
| DATATYPEdecl of con_bind * (con_bind * ty option) list
| DATATYPEdecl of con_bind * ty_bind list * (con_bind * ty option) list
| DECODEdecl of var_bind * decodepat list * (exp, (exp * exp) list) Sum.t
| LETRECdecl of var_bind * var_bind list * exp
| EXPORTdecl of var_use list
......@@ -54,7 +54,7 @@ functor MkAst (Core: AST_CORE) = struct
and ty =
MARKty of ty mark
| BITty of IntInf.int
| NAMEDty of syn_use
| NAMEDty of syn_use * (ty_use * ty) list
| RECORDty of (field_bind * ty) list
and exp =
......@@ -130,9 +130,11 @@ functor MkAst (Core: AST_CORE) = struct
seq (separate (map var_use es, " "))]
| TYPEdecl (t, tyexp) =>
seq [str "type", space, syn_bind t, space, ty tyexp]
| DATATYPEdecl (t, decls) =>
| DATATYPEdecl (t, tvars, decls) =>
align
[seq [str "type", space, con_bind t],
[seq ([str "type", space, con_bind t] @
(if List.null tvars then [] else [str "[",
seq (separate (map ty_bind tvars, ",")), str "]"])),
indent 3 (alignPrefix (map condecl decls, "| "))]
| DECODEdecl (n, ps, Sum.INL e) =>
align
......@@ -188,9 +190,14 @@ functor MkAst (Core: AST_CORE) = struct
case t of
MARKty t' => ty (#tree t')
| BITty i => int i
| NAMEDty alias => Core.syn_use alias
| NAMEDty (alias, args) =>
seq (Core.syn_use alias ::
(if List.null args then [] else [str "[",
seq (separate (map tyArgs args, ",")), str "]"]))
| RECORDty fields => list (map (tuple2 (field_bind, ty)) fields)
and tyArgs (tvName, t) = seq [Core.ty_use tvName, str "=", ty t]
and pat t =
case t of
MARKpat t' => pat (#tree t')
......
......@@ -101,7 +101,8 @@ Program
Decl
: "granularity" "=" Int => (markDecl (FULL_SPAN, PT.GRANULARITYdecl Int))
| "export" "=" Qid* => (markDecl (FULL_SPAN, PT.EXPORTdecl Qid))
| "type" Name "=" ConDecls => (markDecl (FULL_SPAN, PT.DATATYPEdecl (Name, ConDecls)))
| "type" Name "=" ConDecls => (markDecl (FULL_SPAN, PT.DATATYPEdecl (Name, [], ConDecls)))
| "type" Name "[" Name ("," Name)* "]" "=" ConDecls => (markDecl (FULL_SPAN, PT.DATATYPEdecl (Name1, Name2 :: SR, ConDecls)))
| "type" Name "=" Ty => (markDecl (FULL_SPAN, PT.TYPEdecl (Name, Ty)))
| "val" Name Name* "=" Exp => (markDecl (FULL_SPAN, PT.LETRECdecl (Name1, Name2, Exp)))
| "val" Sym Name* "=" Exp => (markDecl (FULL_SPAN, PT.LETRECdecl (Sym, Name, Exp)))
......@@ -123,11 +124,20 @@ ConDecl
Ty
: Int => (mark PT.MARKty (FULL_SPAN, PT.BITty Int))
| Qid => (mark PT.MARKty (FULL_SPAN, PT.NAMEDty Qid))
| "|" Int "|" => (mark PT.MARKty (FULL_SPAN, PT.BITty Int))
| Qid =>
(mark PT.MARKty (FULL_SPAN, PT.NAMEDty (Qid,[])))
| Qid "[" TyBind ("," TyBind)* "]"=>
(mark PT.MARKty (FULL_SPAN, PT.NAMEDty (Qid,TyBind :: SR)))
| "{" Name ":" Ty ("," Name ":" Ty)* "}" =>
(mark PT.MARKty (FULL_SPAN, PT.RECORDty ((Name, Ty)::SR)))
;
TyBind
: Qid "=" Ty => ((Qid,Ty))
| Qid => ((Qid,PT.NAMEDty (Qid,[])))
;
DecodePat
: BitPat => (BitPat)
| TokPat => (mark PT.MARKdecodepat (FULL_SPAN, PT.TOKENdecodepat TokPat))
......
This diff is collapsed.
......@@ -131,7 +131,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(* define a second traversal that is a full inference of the tree *)
(*local helper function to infer types for a binding group*)
val maxIter = 3
val maxIter = 1
fun calcSubset printWarn env =
let
fun checkUsage sym (s, unstable) =
......@@ -548,17 +548,15 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
let
val dcon = SymMap.lookup (conParents, c)
val { tdVars = vs, tdCons = cs } = SymMap.lookup (typeDefs, dcon)
val vs = SymMap.listItems vs
val tArgOpt = SymMap.lookup (cs, c)
val env =
case tArgOpt of
NONE => E.pushType (true, ALG (dcon, List.map VAR vs), env)
| SOME t =>
let
val (posFlags, negFlags) =
fieldBVarsets (t,(BD.emptySet, BD.emptySet))
val env = E.meetBoolean (BD.meetVarSetOne posFlags o
BD.meetVarSetZero negFlags, env)
val env = E.pushType (true, FUN ([t],ALG (dcon, List.map VAR vs)), env)
val env = E.genConstructorFlow env
in
env
end
......
......@@ -109,7 +109,7 @@ end = struct
PT.MARKdecl {span, tree} => regDecl span tree
| PT.DECODEdecl (n, pats, _) => regDec s n
| PT.LETRECdecl (n, _, _) => ignore (newVar (s,n))
| PT.DATATYPEdecl (n, ds) => (regTy s n; app (regCon s) ds)
| PT.DATATYPEdecl (n, tvars, ds) => (regTy s n; app (regCon s) ds)
| PT.TYPEdecl (n, _) => regTy s n
| _ => ()
......@@ -133,9 +133,15 @@ end = struct
| PT.GRANULARITYdecl i => AST.GRANULARITYdecl i
| PT.TYPEdecl (tb, t) =>
AST.TYPEdecl (useType (s,{span=s, tree=tb}), convTy s t)
| PT.DATATYPEdecl (tb, l) =>
AST.DATATYPEdecl
(useType (s, {span=s, tree=tb}), List.map (convCondecl s) l)
| PT.DATATYPEdecl (tb, tvars, l) =>
let
val _ = ST.typeTable := VI.push (!ST.typeTable)
val tvSyms = List.map (fn t => newType (s,t)) tvars
val rhs = List.map (convCondecl s) l
val _ = ST.typeTable := VI.pop (!ST.typeTable)
in
AST.DATATYPEdecl (useType (s, {span=s, tree=tb}), tvSyms, rhs)
end
| PT.DECODEdecl dd => AST.DECODEdecl (convDecodeDecl s dd)
| PT.LETRECdecl vd => AST.LETRECdecl (convLetrecDecl s vd)
......@@ -187,7 +193,12 @@ end = struct
case t of
PT.MARKty m => AST.MARKty (convMark convTy m)
| PT.BITty i => AST.BITty i
| PT.NAMEDty n => AST.NAMEDty (useType (s,n))
| PT.NAMEDty (n, args) =>
let
fun convPair (var,ty) = (useType (s,var), convTy s ty)
in
AST.NAMEDty (useType (s,n), List.map convPair args)
end
| PT.RECORDty fs =>
AST.RECORDty (checkDupFields s
(List.map (fn (f,t) => (newField (s,f), convTy s t)) fs))
......
......@@ -18,6 +18,7 @@ end = struct
structure S = SymMap
structure D = SymMap
structure C = SymMap
structure V = SymMap
structure T = Types
structure BD = BooleanDomain
......@@ -32,6 +33,38 @@ end = struct
typeDefs: datatype_map,
conParents: constructor_map}
fun typeInfoToString ({tsynDefs,typeDefs = tdm,conParents = cm} : type_info) =
let
fun showTd (d, {tdVars = varMap, tdCons = cons}) =
let
val dStr = TypeInfo.getString (!SymbolTables.typeTable, d)
val (args,_,si) = List.foldl (fn ((v,tVar),(str,sep,si)) =>
let
val vStr = TypeInfo.getString (!SymbolTables.typeTable,v)
val (tStr, si) = T.showTypeSI (T.VAR tVar, si)
in
(vStr ^ "=" ^ tStr ^ sep ^ str, ",", si)
end) ("", "", TVar.emptyShowInfo) (V.listItemsi varMap)
fun conInfo ((c,tOpt),(sep,si,str)) =
let
val cStr = ConInfo.getString (!SymbolTables.conTable, c)
val (tStr,si) = case tOpt of
NONE => ("",si)
| SOME t => T.showTypeSI (t,si)
in
("\n | ", si, str ^ sep ^
cStr ^ (if isSome tOpt then " of " else "") ^ tStr)
end
val (_,_,consStr) = List.foldl conInfo ("\n = ",si,"")
(SymMap.listItemsi cons)
in
"type " ^ dStr ^ "[" ^ args ^ "]" ^ consStr
end
in
List.foldl (fn ((td,str)) => str ^ showTd td ^ "\n")
"" (D.listItemsi tdm)
end
fun resolveTypeInfoPass (errStrm, ast) = let
val vars = !SymbolTables.varTable
val cons = !SymbolTables.conTable
......@@ -51,66 +84,86 @@ end = struct
fun fwdDecl (s, d) =
case d of
AST.MARKdecl {span, tree} => fwdDecl (span, tree)
| AST.DATATYPEdecl (d,l) =>
(dtyTable :=
D.insert
(!dtyTable,
d,
{tdVars=[], tdCons=D.empty}))
| AST.DATATYPEdecl (d, tvars, l) =>
let
fun addTVar (tv, varMap) = case V.find (varMap,tv) of
NONE => V.insert (varMap, tv, (T.freshTVar (), BD.freshBVar ()))
| SOME _ => varMap
val varMap = List.foldl addTVar (case D.find (!dtyTable,d) of
NONE => V.empty
| SOME {tdVars=varMap, tdCons} => varMap) tvars
in
(dtyTable := D.insert (!dtyTable, d,
{tdVars=varMap, tdCons=C.empty}))
end
| _ => ()
fun vDecl (s, d) =
case d of
AST.MARKdecl {span, tree} => vDecl (span, tree)
| AST.TYPEdecl (v, t) => synTable := S.insert (!synTable, v, vType (s,t))
| AST.DATATYPEdecl (d,l) =>
| AST.TYPEdecl (v, t) =>
synTable := S.insert (!synTable, v, vType V.empty (s,t))
| AST.DATATYPEdecl (d, tvars, l) =>
(case D.lookup (!dtyTable,d) of
{tdVars=_, tdCons=cons} =>
(dtyTable := D.insert (!dtyTable, d,
{tdVars = [], tdCons = vCondecl cons (s,d,l)})))
{tdVars=tvs, tdCons=cons} =>
(dtyTable := D.insert (!dtyTable, d,
{tdVars = tvs, tdCons = vCondecl cons (s,d,tvs,l)}))
)
| _ => ()
and vType (s, t) =
and vType tvs (s, t) =
case t of
AST.MARKty {span, tree} => vType (span,tree)
AST.MARKty {span, tree} => vType tvs (span,tree)
| AST.BITty i => T.VEC (T.CONST (IntInf.toInt i))
| AST.NAMEDty n =>
| AST.NAMEDty (n, args) =>
(case S.find (!synTable, n) of
SOME t => T.SYN (n, T.setFlagsToTop t)
SOME t => T.SYN (n, t)
| NONE => (case D.find (!dtyTable, n) of
SOME {tdVars=vs,tdCons=_} => T.ALG (n, map Types.VAR vs)
| NONE => (Error.errorAt
(errStrm, s,
["type synonym or data type ",
TypeInfo.getString (types, n),
" not declared "]); T.UNIT)))
SOME {tdVars=varMap,tdCons=_} =>
let
val argMap =
List.foldl SymMap.insert' SymMap.empty args
fun findType v = case SymMap.find (argMap,v) of
SOME t => vType tvs (s, t)
| NONE => case V.find (tvs,v) of
SOME varPair => T.VAR varPair
| NONE => (Error.errorAt
(errStrm, s,
["unknown type variable ",
TypeInfo.getString (types, v),
" in argument "]); T.UNIT)
in
T.ALG (n, List.map findType (V.listKeys varMap))
end
| NONE => (case V.find (tvs,n) of
SOME varPair => T.VAR varPair
| NONE => (Error.errorAt
(errStrm, s,
["type synonym or data type ",
TypeInfo.getString (types, n),
" not declared "]); T.UNIT))))
| AST.RECORDty l =>
T.RECORD
(Types.freshTVar (), BD.freshBVar (),
List.foldl Substitutions.insertField []
(List.map (vField s) l))
and vField s (n, ty) =
T.RField {name=n, fty=vType (s, ty), exists=BD.freshBVar ()}
and vCondecl sm (s,d,l) =
case l of
[] => sm
| (c, arg)::l =>
(case C.find (!conTable, c) of
SOME d =>
Error.errorAt
(errStrm, s,
["constructor ",
Atom.toString (ConInfo.getAtom (cons,c)),
" already used in ",
Atom.toString (TypeInfo.getAtom (types,d))])
| NONE =>
(conTable := C.insert (!conTable, c, d))
;D.insert
(vCondecl sm (s,d,l),
c,
Option.map (fn t => vType (s, t)) arg))
(List.map (vField s tvs) l))
and vField s tvs (n, ty) =
T.RField {name=n, fty=vType tvs (s, ty), exists=BD.freshBVar ()}
and vCondecl sm (s,d,tvs,l) = List.foldl (fn ((c, arg), sm) =>
(case C.find (!conTable, c) of
SOME d =>
Error.errorAt
(errStrm, s,
["constructor ",
Atom.toString (ConInfo.getAtom (cons,c)),
" already used in ",
Atom.toString (TypeInfo.getAtom (types,d))])
| NONE =>
(conTable := C.insert (!conTable, c, d))
;D.insert (sm, c, Option.map (fn t => vType tvs (s, t)) arg))
) sm l
val declList = ast
val s = SymbolTable.noSpan
......@@ -118,7 +171,14 @@ end = struct
in
(app (fn d => fwdDecl (s,d)) declList
;app (fn d => vDecl (s,d)) declList
;{tsynDefs= !synTable, typeDefs= !dtyTable, conParents= !conTable} : type_info)
;let
val res = {tsynDefs= !synTable,
typeDefs= !dtyTable,
conParents= !conTable} : type_info
(*val _ = TextIO.print (typeInfoToString res)*)
in
res
end)
end
val resolveTypeInfoPass =
......
......@@ -45,12 +45,17 @@ structure Environment : sig
(* push the width of a decode onto the stack*)
val pushWidth : VarInfo.symid * environment -> environment
(*given an occurrence of a symbol at a position, push its type onto the
(* 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
(*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
the symbol to look up, the position it occurred and a list of symbols that
denote the current context/function (the latter is ignored if the symbol
already has a type) *)
val pushSymbol : VarInfo.symid * Error.span * environment -> environment
already has a type) *) val pushSymbol : VarInfo.symid * Error.span *
environment -> environment
val getUsages : VarInfo.symid * environment -> Error.span list
......@@ -783,12 +788,33 @@ end = struct
end
fun meetBoolean (update, env as (scs, state)) =
(scs, Scope.setFlow (update (Scope.getFlow state)) state)
handle (BD.Unsatisfiable bVar) => flowError (bVar, NONE, [env])
(scs, Scope.setFlow (update (Scope.getFlow state)) state)
handle (BD.Unsatisfiable bVar) => flowError (bVar, NONE, [env])
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) =>
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
in
env
end
| _ => raise InferenceBug
fun pushSymbol (sym, span, env) =
(case Scope.lookup (sym,env) of
(_, SIMPLE {ty = t}) =>
......
......@@ -89,6 +89,27 @@ 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
......@@ -197,7 +218,7 @@ structure Types = struct
type condescr = texp option SymMap.map
type typedescr = { tdVars : (tvar * BD.bvar) list,
type typedescr = { tdVars : (TVar.tvar * BD.bvar) SymMap.map,
tdCons : condescr }
fun showTypeSI (ty, showInfo) = let
......@@ -220,13 +241,14 @@ structure Types = struct
| sT (p, FLOAT) = "float"
| sT (p, STRING) = "string"
| sT (p, UNIT) = "()"
| sT (p, VEC t) = "[" ^ sT (0, t) ^ "]"
| sT (p, VEC t) = "|" ^ sT (0, t) ^ "|"
| sT (p, CONST c) = Int.toString(c)
| sT (p, ALG (ty, l)) = let
val conStr = SymbolTable.getString(!SymbolTables.typeTable, ty)
in if List.null l then conStr else br (p, p_tyn,
List.foldl (fn (s1,s2) => s1 ^ " " ^ s2) conStr (
List.map (fn e => sT (p_tyn+1, e)) l))
in if List.null l then conStr else conStr ^ "[" ^ #2 (
List.foldl (fn (t,(sep,str)) => (",",sT (0, t) ^ sep ^ str))
("","") l
) ^ "]"
end
| sT (p, RECORD (v,b,l)) = "{" ^ List.foldl (op ^) "" (List.map sTF l) ^
showVar v ^
......
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