Stefan pushed to branch main at Stefan / Typer

Commits: 4421b8e7 by Stefan Monnier at 2023-03-21T23:25:52-04:00 Fix an inf-loop during elaboration

When `typer-identifier` is redefined as something else than a special form or a macro, we got into an inf-loop when elaborating X because we would rewrite to (typer_identifier X), which would then be taken as a function call, which recursively elaborates its arg X, ...

* src/elab.ml (sform_immediate, sform_identifier): Move before `elaborate`. (elab_via): New function. (elaborate): Use it.

- - - - -

1 changed file:

- src/elab.ml

Changes:

===================================== src/elab.ml ===================================== @@ -602,24 +602,125 @@ let wrapLambda ne vname t _l e = let elab_p_id ((l,name) : symbol) : vname = (Symbol (l, name), match name with "_" -> None | _ -> Some name)

+let rec sform_immediate ctx loc sargs ot = + match sargs with + | [(String _) as se] -> mkImm (se), Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_integer + | [(Float _) as se] -> mkImm (se), Inferred DB.type_float + | [Block (_location, pts)] + -> let grm = ectx_get_grammar ctx in + let tokens = lex default_stt pts in + let (se, _) = sexp_parse_all grm tokens None in + elaborate ctx se ot + | [_se] + -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); + sform_dummy_ret ctx loc) + | _ + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); + sform_dummy_ret ctx loc) + + +and sform_identifier ctx loc sargs ot = + match sargs with + | [Symbol (l,name)] + when String.length name >= 1 && String.get name 0 == '#' + -> if String.length name > 2 && String.get name 1 == '#' then + let name = string_sub name 2 (String.length name) in + try let (e, t) = SMap.find name (! BI.lmap) in + (e, Inferred t) + with + | Not_found + -> sexp_error l {|Unknown builtin "%s"|} name; + sform_dummy_ret ctx loc + else + (sexp_error l {|Invalid special identifier "%s"|} name; + sform_dummy_ret ctx loc) + + | [Symbol (_loc, name)] + when String.length name >= 1 && String.get name 0 = '?' + -> let name = if name = "?" then "" else + string_sub name 1 (String.length name) in + (* Shift the var so it can't refer to the local vars. + * This is used so that in cases like "lambda t (y : ?) ... " + * type inference can guess ? without having to wonder whether it + * can refer to `t` or not. If the user wants ? to be able to refer + * to `t`, then they should explicitly write (y : ? t). *) + let ctx_shift = ectx_local_scope_size ctx in + let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in + let sl = ectx_to_scope_level ctx in + let subst = S.shift ctx_shift in + let (_, _, rmmap) = ectx_get_scope ctx in + if not (name = "") && SMap.mem name (!rmmap) then + let idx = SMap.find name (!rmmap) in + match (metavar_lookup idx) with + | MVar (sl',_,_) + -> if sl = sl' then + (mkMetavar (idx, subst, (loc, Some name)), Lazy) + else + (* FIXME: The variable is from another scope_level! It + means that `subst` is not the right substitution for + the metavar! *) + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" + ^^ " repeated at a different scope level!") + | MVal _ + -> (* FIXME: We face the same problem as above, but here, + the situation is worse, we don't even know the scope + level! *) + fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" + else + let t = match ot with + | None -> newMetatype octx sl loc + | Some t + (* `t` is defined in ctx instead of octx. *) + -> Inverse_subst.apply_inv_subst t subst in + let mv = newShiftedInstanceMetavar ctx (loc, Some name) t in + (if not (name = "") then + let idx = + match lexp_lexp' mv with + | Metavar (idx, _, _) -> idx + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in + rmmap := SMap.add name idx (!rmmap)); + (mv, match ot with Some _ -> Checked | None -> Lazy) + + (* Normal identifier. *) + | [Symbol (_n, name)] + -> elab_varref ctx (loc, name) + + | [_se] + -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); + sform_dummy_ret ctx loc) + + | _ + -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); + sform_dummy_ret ctx loc) + +and elab_via head default ctx se ot = + match elab_varref ctx head with + | (f, Inferred t) + -> if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then + elab_special_form ctx f [se] ot + else if (OL.conv_p (ectx_to_lctx ctx) t + (BI.get_predef "Macro" ctx)) then + elab_macro_call ctx f [se] ot + else + default ctx se [se] ot + | _ -> default ctx se [se] ot + (* Infer or check, as the case may be. *) -let rec elaborate ctx se ot = +and elaborate ctx se ot = let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) - | Symbol ((loc, name) as _id) - -> if not (name = "typer-identifier") then - elaborate ctx (Node (loc, Symbol (loc, "typer-identifier"), [se])) ot - (* Break the inf-recursion! *) - else elab_varref ctx (se, name) + | Symbol _ + -> elab_via (se, "typer-identifier") sform_identifier ctx se ot

(* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) - -> let l = sexp_location se in - elaborate ctx (Node (l, Symbol (l, "typer-immediate"), [se])) ot + -> elab_via (se, "typer-immediate") sform_immediate ctx se ot

| Node (_, se, []) -> elaborate ctx se ot

| Node (_, func, args) + (* FIXME: Use (or merge with) `elab_via`! *) -> let (f, t) as ft = infer func ctx in if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then elab_special_form ctx f args ot @@ -628,8 +729,9 @@ let rec elaborate ctx se ot = elab_macro_call ctx f args ot else (* FIXME: I'd like to do something like: - * elaborate ctx (Node (Symbol (l, "typer-funcall"), func::args)) ot - * but that forces `typer-funcall` to elaborate `func` a second time! + * elab_via (l, "typer-funcall") sform_call ctx se ot + * but that would force `typer-funcall` to elaborate `func` + * a second time! * Maybe I should only elaborate `func` above if it's a symbol * (and maybe even use `elab_varref` rather than indirecting * through `typer-identifier`)? *) @@ -1611,98 +1713,6 @@ let sform_arrow kind ctx loc sargs _ot = | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc

-let sform_immediate ctx loc sargs ot = - match sargs with - | [(String _) as se] -> mkImm (se), Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se), Inferred DB.type_integer - | [(Float _) as se] -> mkImm (se), Inferred DB.type_float - | [Block (_location, pts)] - -> let grm = ectx_get_grammar ctx in - let tokens = lex default_stt pts in - let (se, _) = sexp_parse_all grm tokens None in - elaborate ctx se ot - | [_se] - -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); - sform_dummy_ret ctx loc) - | _ - -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); - sform_dummy_ret ctx loc) - - -let sform_identifier ctx loc sargs ot = - match sargs with - | [Symbol (l,name)] - when String.length name >= 1 && String.get name 0 == '#' - -> if String.length name > 2 && String.get name 1 == '#' then - let name = string_sub name 2 (String.length name) in - try let (e, t) = SMap.find name (! BI.lmap) in - (e, Inferred t) - with - | Not_found - -> sexp_error l {|Unknown builtin "%s"|} name; - sform_dummy_ret ctx loc - else - (sexp_error l {|Invalid special identifier "%s"|} name; - sform_dummy_ret ctx loc) - - | [Symbol (_loc, name)] - when String.length name >= 1 && String.get name 0 = '?' - -> let name = if name = "?" then "" else - string_sub name 1 (String.length name) in - (* Shift the var so it can't refer to the local vars. - * This is used so that in cases like "lambda t (y : ?) ... " - * type inference can guess ? without having to wonder whether it - * can refer to `t` or not. If the user wants ? to be able to refer - * to `t`, then they should explicitly write (y : ? t). *) - let ctx_shift = ectx_local_scope_size ctx in - let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in - let sl = ectx_to_scope_level ctx in - let subst = S.shift ctx_shift in - let (_, _, rmmap) = ectx_get_scope ctx in - if not (name = "") && SMap.mem name (!rmmap) then - let idx = SMap.find name (!rmmap) in - match (metavar_lookup idx) with - | MVar (sl',_,_) - -> if sl = sl' then - (mkMetavar (idx, subst, (loc, Some name)), Lazy) - else - (* FIXME: The variable is from another scope_level! It - means that `subst` is not the right substitution for - the metavar! *) - fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" - ^^ " repeated at a different scope level!") - | MVal _ - -> (* FIXME: We face the same problem as above, but here, - the situation is worse, we don't even know the scope - level! *) - fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" - else - let t = match ot with - | None -> newMetatype octx sl loc - | Some t - (* `t` is defined in ctx instead of octx. *) - -> Inverse_subst.apply_inv_subst t subst in - let mv = newShiftedInstanceMetavar ctx (loc, Some name) t in - (if not (name = "") then - let idx = - match lexp_lexp' mv with - | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in - rmmap := SMap.add name idx (!rmmap)); - (mv, match ot with Some _ -> Checked | None -> Lazy) - - (* Normal identifier. *) - | [Symbol (_n, name)] - -> elab_varref ctx (loc, name) - - | [_se] - -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); - sform_dummy_ret ctx loc) - - | _ - -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); - sform_dummy_ret ctx loc) - let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody]

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4421b8e7aaad4ebf4e2eb753d5bb48d3c4...