Stefan pushed to branch master at Stefan / Typer

Commits: 257dc966 by Stefan Monnier at 2017-07-07T16:04:55-04:00 * src/elab.el (sform_lambda): CPS refactor the end

- - - - - a2bd9afc by Stefan Monnier at 2017-07-07T16:22:32-04:00 * src/elab.ml (sform_lambda): Auto-add implicit lambda wrappers

(var_of_ovar): New function.

- - - - - fc6835a1 by Stefan Monnier at 2017-07-07T16:30:42-04:00 * btl/pervasive.typer: Let lambda_->_ infer the needed lambda_≡>_!

* btl/builtins.typer (Eq_comm): Same here.

- - - - -

3 changed files:

- btl/builtins.typer - btl/pervasive.typer - src/elab.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -54,10 +54,9 @@ Eq_cast = Built-in "Eq.cast" %% Commutativity of equality! Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; -Eq_comm = lambda l ≡> lambda t ≡> lambda x ≡> lambda y ≡> lambda p -> - Eq_cast (f := lambda xy -> Eq (t := t) xy x) - (p := p) - Eq_refl; +Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) + (p := p) + Eq_refl;

%% General recursion!! %% Whether this breaks onsistency or not is a good question.

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -39,27 +39,26 @@ none = datacons Option none; %%% Good 'ol combinators

I : (a : Type) ≡> a -> a; -I = lambda a ≡> lambda x -> x; +I x = x;

K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; -K = lambda a ≡> lambda x -> lambda b ≡> lambda y -> x; +K x = lambda y -> x;

%%%% List functions

List_length : (a : Type) ≡> List a -> Int; -List_length = lambda a ≡> lambda xs -> case xs +List_length xs = case xs | nil => 0 | cons hd tl => (1 + (List_length tl));

List_reverse : (a : Type) ≡> List a -> List a -> List a; -List_reverse = lambda a ≡> lambda l -> lambda t -> case l +List_reverse l = lambda t -> case l | nil => t | cons hd tl => List_reverse tl (cons hd t);

List_concat : (a : Type) ≡> List a -> List a -> List a; -List_concat = lambda a ≡> lambda l -> lambda t -> - List_reverse (List_reverse l nil) t; +List_concat l = lambda t -> List_reverse (List_reverse l nil) t;

%% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: @@ -67,37 +66,37 @@ List_concat = lambda a ≡> lambda l -> lambda t -> %% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; %% - Return an Option/Error. List_head1 : (a : Type) ≡> List a -> Option a; -List_head1 = lambda a ≡> lambda xs -> case xs +List_head1 xs = case xs | nil => none | cons hd tl => some hd;

List_head : (a : Type) ≡> a -> List a -> a; -List_head = lambda a ≡> lambda x -> lambda xs -> case xs +List_head x = lambda xs -> case xs | cons x _ => x | nil => x;

List_tail : (a : Type) ≡> List a -> List a; -List_tail = lambda a ≡> lambda xs -> case xs +List_tail xs = case xs | nil => nil | cons hd tl => tl;

List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; -List_map = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs +List_map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs);

List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; -List_foldl = lambda a ≡> lambda b ≡> lambda f -> lambda i -> lambda xs -> case xs +List_foldl f = lambda i -> lambda xs -> case xs | nil => i | cons x xs => List_foldl f (f i x) xs;

List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; -List_foldr = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> lambda i -> case xs +List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i);

List_find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; -List_find = lambda a ≡> lambda f -> lambda xs -> case xs +List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs;

@@ -107,19 +106,19 @@ List_find = lambda a ≡> lambda f -> lambda xs -> case xs Sexp_error = Sexp_symbol "<error>";

Sexp_to_list : Sexp -> List Sexp -> List Sexp; -Sexp_to_list = lambda s -> lambda exceptions - -> let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in - Sexp_dispatch - s - (node := lambda head -> lambda tail - -> case List_find (Sexp_eq head) exceptions - | some _ => singleton () - | none => cons head tail) - (symbol := lambda s - -> case String_eq "" s - | true => nil - | false => singleton ()) - singleton singleton singleton singleton; +Sexp_to_list s = lambda exceptions -> + let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in + Sexp_dispatch + s + (node := lambda head -> lambda tail + -> case List_find (Sexp_eq head) exceptions + | some _ => singleton () + | none => cons head tail) + (symbol := lambda s + -> case String_eq "" s + | true => nil + | false => singleton ()) + singleton singleton singleton singleton;

multiarg_lambda = %% let bodytail = cons body nil;

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -1154,7 +1154,11 @@ let elaborate ctx pe ot = | None -> let (le, lt) = infer pe ctx in (le, Inferred lt)

-let sform_lambda kind ctx loc sargs ot = +let var_of_ovar l ov = match ov with + | None -> (l, "<anon>") + | Some v -> v + +let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody] -> let (arg, ost1) = match sarg with @@ -1168,44 +1172,58 @@ let sform_lambda kind ctx loc sargs ot = | Some st -> Some (infer_type st ctx (Some arg)) | _ -> None in

- let lt1, olt2 = - match ot with - | None -> ((match olt1 with - | Some lt1 -> lt1 - | None -> newMetatype loc), - None) - (* Read var type from the provided type *) - | Some t - -> let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind - -> (match olt1 with - | None -> () - | Some lt1' - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); - (lt1, Some lt2) - (* FIXME: If `t` is an implicit arrow and `kind` is Aexplicit, - * then auto-add a corresponding Lambda wrapper! *) - | lt - -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 - in (lt1, Some lt2) in - - let nctx = env_extend ctx arg Variable lt1 in - let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (kind, arg, lt1, lbody), - match alt with - | Lazy -> Lazy - | Checked -> Checked - | Inferred lt2 - -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) + let mklam lt1 olt2 = + let nctx = env_extend ctx arg Variable lt1 in + let (lbody, alt) = elaborate nctx sbody olt2 in + (mkLambda (kind, arg, lt1, lbody), + match alt with + | Lazy -> Lazy (* FIXME: Impossible! *) + | Checked -> Checked + | Inferred lt2 + -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2))) in + + (match ot with + | None -> mklam (match olt1 with + | Some lt1 -> lt1 + | None -> newMetatype loc) + None + (* Read var type from the provided type *) + | Some t + -> let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind + -> (match olt1 with + | None -> () + | Some lt1' + -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') + then lexp_error (lexp_location lt1') lt1' + ("Type mismatch! Context expected `" + ^ lexp_string lt1 ^ "`")); + mklam lt1 (Some lt2) + + | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit + (* `t` is an implicit arrow and `kind` is Aexplicit, + * so auto-add a corresponding Lambda wrapper! + * FIXME: This should be moved to a macro. *) + -> let v = var_of_ovar loc v in + (* FIXME: Here we end up adding a local variable `v` whose + * name is lot lexically present, so there's a risk of + * name capture. We should make those vars anonymous? *) + let nctx = env_extend ctx v Variable lt1 in + (* FIXME: Don't go back to sform_lambda, but use an internal + * loop to avoid re-computing olt1 each time. *) + let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in + assert (alt == Checked); + (mkLambda (ak2, v, lt1, lam), Checked) + + | lt + -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 + in mklam lt1 (Some lt2))

| _ -> sexp_error loc ("##lambda_"^(match kind with Aexplicit -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>") - ^"_ takes two arguments"; + ^"_ takes two arguments"); sform_dummy_ret loc

let rec sform_case ctx loc sargs ot = match sargs with

View it on GitLab: https://gitlab.com/monnier/typer/compare/630b1bf079bca7ee7e5b7a9df7e1673da80...

--- View it on GitLab: https://gitlab.com/monnier/typer/compare/630b1bf079bca7ee7e5b7a9df7e1673da80... You're receiving this email because of your account on gitlab.com.