Stefan pushed to branch master at Stefan / Typer

Commits: 915ca70f by Stefan Monnier at 2016-09-07T12:37:50-04:00 * src/opslexp.ml (lexp_whnf): Add various missing cases.

- - - - -

2 changed files:

- src/lparse.ml - src/opslexp.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -433,7 +433,8 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = "Explicit arg to non-function") in

let handle_funcall () = - + (* Here we use lexp_whnf on actual code, but it's OK + * because we only use the result when it's a "predefined constant". *) match OL.lexp_whnf body ctx with | Builtin((_, "Built-in"), _) -> ( @@ -455,13 +456,15 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = lexp_error loc "Use of "Built-in" in user code"; dlxp, dltype)

- | e -> + | _ -> (* Process Arguments *) let largs, ret_type = handle_fun_args [] sargs ltp in Call (body, List.rev largs), ret_type in

let handle_macro_call () = - (* Get the macro *) + (* FIXME: We shouldn't look at `body` here at all: + * Instead, we should pass `body` (along with `arg`) to + * a `typer__expand_macro` function predefined in types.typer. *) let lxp = match OL.lexp_whnf body ctx with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | lxp ->

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -112,15 +112,56 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * - Not a Call (Call _). * - Not a Call (_, []). * - Not a Case (Cons _). - * - Not a Call (MetaSet, ..). - *) + * FIXME: This should be memoized! + * + * BEWARE: As a general rule lexp_whnf should not be used on actual *code* + * but only on *types*. If you must use it on code, be sure to use its + * return value as little as possible since WHNF will inherently introduce + * call-by-name behavior. *) let rec lexp_whnf e ctx = match e with + (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match DB.env_lookup_expr ctx v with | None -> e - (* FIXME: We shouldn't do this blindly for recursive definitions! *) + (* We can do this blindly even for recursive definitions! + * IOW the risk of inf-looping should only show up when doing + * things like full normalization (e.g. lexp_conv_p). *) | Some e' -> lexp_whnf e' ctx) | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - (* FIXME: Obviously incomplete! *) + | Call (e, []) -> lexp_whnf e ctx + | Call (e, (((_, arg)::args) as xs)) -> + (match lexp_whnf e ctx with + | Lambda (_, _, _, body) -> + (* Here we apply whnf to the arg eagerly to kind of stay closer + * to the idea of call-by-value, although in this context + * we can't really make sure we always reduce the arg to a value. *) + lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx)), + args)) + ctx + | Call (e', xs1) -> Call (e', List.append xs1 xs) + | e' -> Call (e', xs)) + | Case (l, e, bt, rt, branches, default) -> + let reduce name aargs = + try + let (_, _, branch) = SMap.find name branches in + let (subst, _) + = List.fold_left + (fun (s,d) (_, arg) -> + (S.Cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d), s), + d + 1)) + (S.identity, 0) + aargs in + lexp_whnf (push_susp branch subst) ctx + with Not_found + -> match default + with | Some default -> lexp_whnf default ctx + | _ -> U.msg_error "WHNF" l + ("Unhandled constructor " ^ + name ^ "in case expression"); + Case (l, e, bt, rt, branches, default) in + (match lexp_whnf e ctx with + | Cons (_, (_, name)) -> reduce name [] + | Call (Cons (_, (_, name)), aargs) -> reduce name aargs + | e' -> Case (l, e', bt, rt, branches, default)) | e -> e

View it on GitLab: https://gitlab.com/monnier/typer/commit/915ca70f0c8c394e2b7cf724129c34b1c2b8...