Stefan pushed to branch graveline at Stefan / Typer
Commits: 93aa39b9 by Stefan Monnier at 2018-07-24T02:19:08Z Fix exponential blowup witnessed when loading a module
* src/lexp.ml (hcs_table): New memoization table. (mkSusp_memo): New function.
- - - - - 9f8cd189 by Stefan Monnier at 2018-07-24T02:19:28Z Merge branch 'trunk' into graveline
- - - - -
1 changed file:
- src/lexp.ml
Changes:
===================================== src/lexp.ml ===================================== @@ -210,20 +210,44 @@ let mkCall (f, es) * Maybe it would be cleaner to just move subst.ml into lexp.ml * and be done with it. *)
+(* FIXME: We'd like to make this table "weak" to avoid memory leaks, + * but Weak.Make doesn't cut it because we need to index with a pair + * that is transient and hence immediately GC'd. *) +let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 + +(* When building the type of a tuple (x1=e1, x2=e2, ..., xn=en) + * we end up building substitutions of the form + * + * ((Susp e3 (((Susp e2 (e1 · id)) · e1 · id) + * · e1 · id)) + * · ((Susp e2 (e1 · id)) · e1 · id) + * · e1 · id) + * + * with exponential size (but lots of sharing). So it's indispensible + * to memoize the computation to avoid the exponential waste of time. + * + * FIXME: I still don't understand why we build substitutions + * of such a shape! *) + let rec mkSusp e s = if S.identity_p s then e else (* We apply the substitution eagerly to some terms. * There's no deep technical rason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) match e with - (* FIXME: `Builtin` shouuld be treated like `Imm`. *) | Imm _ -> e | Builtin _ -> e - | Susp (e, s') -> mkSusp e (scompose s' s) + | Susp (e, s') -> mkSusp_memo e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) | _ -> hc (Susp (e, s)) -and scompose s1 s2 = S.compose mkSusp s1 s2 +and mkSusp_memo e s + = if Hashtbl.mem hcs_table (e, s) + then Hashtbl.find hcs_table (e, s) + else let res = mkSusp e s in + Hashtbl.add hcs_table (e, s) res; + res +and scompose s1 s2 = S.compose mkSusp_memo s1 s2 and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) (fun e o -> mkSusp e (S.shift o)) s l v
View it on GitLab: https://gitlab.com/monnier/typer/compare/c08685e0ce77c75f735237ba17db20535e4...
Afficher les réponses par date