Stefan pushed to branch unification at Stefan / Typer
Commits: 2bd4d49a by Stefan Monnier at 2016-09-12T17:06:17-04:00 * src/lexp.ml (push_susp): Use nosusp
* src/lparse.ml (get_type0, get_int): Remove (again). (_lexp_p_check.infer_lambda_body.ltp): Minor layout tweaks.
- - - - -
2 changed files:
- src/lexp.ml - src/lparse.ml
Changes:
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -323,14 +323,11 @@ let rec push_susp e s = (* Push a suspension one level down. *) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp - * rather than Susp. *) - | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) - push_susp e (scompose s' s) - | (Var _ | Metavar _) - -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) - if S.identity_p s - then e - else push_susp (mkSusp e s) S.identity + * rather than Susp. + * But we still have to handle them here, since push_susp is called + * in many other cases than just when we bump into a Susp. *) + | Susp (e,s') -> push_susp e (scompose s' s) + | (Var _ | Metavar _) -> nosusp (mkSusp e s)
let nosusp e = (* Return `e` without `Susp`. *) match e with
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -126,9 +126,10 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx)
-(* build type0 from ctx *) -let get_type0 ctx = build_var "Type" ctx -let get_int ctx = build_var "Int" ctx +(* FIXME: We need to keep track of the type of metavars. We could keep it + * in the `Metavar` constructor of the `lexp` type, but that's risky (it could + * be difficult to make sure it's the same for all occurrences of that + * metavar). *)
(* :-( *) let global_substitution = ref (empty_subst, []) @@ -313,13 +314,12 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = | lxp -> (unify_with_arrow lxp kind subst) in let nctx = env_extend ctx var Variable ltp in - let lbody = _lexp_p_check body lbtp nctx (i + 1) in Lambda(kind, var, ltp, lbody) + let lbody = _lexp_p_check body lbtp nctx (i + 1) in + Lambda(kind, var, ltp, lbody)
in - let subst, _ = !global_substitution - in - let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) - in + let subst, _ = !global_substitution in + let lexp_infer p ctx = _lexp_p_infer p ctx (i + 1) in match p with (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->(infer_lambda_body kind var body subst)
View it on GitLab: https://gitlab.com/monnier/typer/commit/2bd4d49a243a0d575615a8f09942a3687ad2...