Stefan pushed to branch master at Stefan / Typer

Commits: 09e86649 by Stefan Monnier at 2017-07-07T22:38:37-04:00 * src/elab.ml (lexp_check_decls): Drop unused `ltype` from `defs`

(lexp_decls_1): Drop corresponding info from pending_defs and pending_decls.

- - - - - 17f4f72a by Stefan Monnier at 2017-07-07T22:39:25-04:00 * btl/pervasive.typer: Move some defs to benefit from multiarg λ

- - - - -

3 changed files:

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

Changes:

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -36,14 +36,6 @@ Option = typecons (Option (a : Type)) (none) (some a); some = datacons Option some; none = datacons Option none;

-%%% Good 'ol combinators - -I : (a : Type) ≡> a -> a; -I x = x; - -K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; -K x = lambda y -> x; - %%%% List functions

List_length : (a : Type) ≡> List a -> Int; @@ -52,14 +44,6 @@ List_length xs = case xs | cons hd tl => (1 + (List_length tl));

-List_reverse : (a : Type) ≡> List a -> List a -> List a; -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 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: %% - Provide a default value : (a : Type) ≡> a -> List a -> a; @@ -85,11 +69,6 @@ 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 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 f = lambda xs -> lambda i -> case xs | nil => i @@ -100,7 +79,7 @@ List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs;

-%%%% A more flexible `lambda`. +%%%% A more flexible `lambda`

%% An Sexp which we use to represents an error. Sexp_error = Sexp_symbol "<error>"; @@ -121,34 +100,11 @@ Sexp_to_list s = lambda exceptions -> singleton singleton singleton singleton;

multiarg_lambda = - %% let bodytail = cons body nil; - %% mklam = lambda (a : Type) ≡> lambda (_ : a) - %% -> Sexp_node (Sexp_symbol "##lambda_->_") - %% (cons arg bodytail) in - %% Sexp_dispatch - %% arg - %% (node := (lambda head -> lambda tail -> - %% Sexp_dispatch - %% head - %% (symbol := (lambda s -> case String_eq s "_:_" - %% | true -> mklam () - %% | false -> case String_eq s "_::_" - %% | true - %% -> Sexp_node (Sexp_symbol "##lambda_=>_") - %% (cons (Sexp_node - %% (Sexp_symbol "_:_") - %% tail) - %% bodytail) - %% | false -> case String_eq s "_:::_" - %% | true - %% -> Sexp_node (Sexp_symbol "##lambda_≡>_") - %% (cons (Sexp_node - %% (Sexp_symbol "_:_") - %% tail) - %% bodytail) - %% | false -> mklam ())) - %% mklam mklam mklam mklam mklam)) - %% mklam mklam mklam mklam mklam + %% This macro lets `lambda_->_` (and siblings) accept multiplke arguments. + %% TODO: We could additionally turn + %% `lambda (x :: t) y -> e` into `lambda (x : t) => lambda y -> e` + %% thus providing an alternate syntax for lambdas which doesn't use + %% => and ≡>. let exceptions = List_map Sexp_symbol (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in lambda name -> @@ -171,6 +127,29 @@ lambda_->_ = macro (multiarg_lambda "##lambda_->_"); lambda_=>_ = macro (multiarg_lambda "##lambda_=>_"); lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_");

+%%%% More list functions + +List_reverse : (a : Type) ≡> List a -> List a -> List a; +List_reverse l 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 l t = List_reverse (List_reverse l nil) t; + +List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +List_foldl f i xs = case xs + | nil => i + | cons x xs => List_foldl f (f i x) xs; + +%%% Good 'ol combinators + +I : (a : Type) ≡> a -> a; +I x = x; + +K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; +K x y = x; + %%%% Quasi-Quote macro

%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) @@ -344,4 +323,15 @@ Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop));

+%%%% Test +test1 : Option Int; +test2 : Option Int; +test3 : Option Int; +test4 : Option Int; +test1 = test2; +test2 = none; +test4 = test1; +test3 = test4; + + %%% pervasive.typer ends here.

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -621,7 +621,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt - (* FIXME: is `ct` is Special-Form or Macro, pass pargs to it + (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it * and try again with the result. *) | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt in @@ -817,7 +817,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) (* Print each generated decls *) and sexp_decls_macro_print sxp_decls = match sxp_decls with - | Node(Symbol (_, "_;_"), decls) -> + | Node (Symbol (_, "_;_"), decls) -> List.iter (fun sxp -> sexp_decls_macro_print sxp) decls | e -> sexp_print e; print_string "\n"

@@ -835,20 +835,19 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp =

and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) - (defs : (vname * sexp * ltype) list) + (defs : (vname * sexp) list) : (vname * lexp * ltype) list * elab_context = let (declmap, nctx) = List.fold_right - (fun ((_, vname) as v, pexp, ltp) (map, nctx) -> + (fun ((_, vname) as v, pexp) (map, nctx) -> let i = senv_lookup vname nctx in assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (o, v', ForwardRef, t) - -> let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in - assert (t == ltp); - let e = check pexp adjusted_ltp nctx in + -> let adjusted_t = push_susp t (S.shift (i + 1)) in + let e = check pexp adjusted_t nctx in let (ec, lc, sl) = nctx in - (IntMap.add i (v, e, ltp) map, + (IntMap.add i (v, e, t) map, (ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IntMap.empty, nctx) in @@ -860,13 +859,13 @@ and lexp_decls_1 (sdecls : sexp list) (ectx : elab_context) (* External ctx. *) (nctx : elab_context) (* New context. *) - (pending_decls : (location * ltype) SMap.t) (* Pending type decls. *) - (pending_defs : (vname * sexp * ltype) list) (* Pending definitions. *) + (pending_decls : location SMap.t) (* Pending type decls. *) + (pending_defs : (vname * sexp) list) (* Pending definitions. *) : (vname * lexp * ltype) list * sexp list * elab_context =

match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, (l, _)) = SMap.choose pending_decls in + let (s, l) = SMap.choose pending_decls in error l ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); @@ -885,15 +884,16 @@ and lexp_decls_1 | [Symbol ((l, vname) as v); stp] -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then + (* Don't burp: take'em all and unify! *) (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) - else if List.exists (fun ((_, vname'), _, _) -> vname = vname') + else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx (env_extend nctx v ForwardRef ltp) - (SMap.add vname (l, ltp) pending_decls) + (SMap.add vname l pending_decls) pending_defs | _ -> error l "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) @@ -912,18 +912,18 @@ and lexp_decls_1 ctx_define nctx v lexp ltp

| [Symbol ((l, vname) as v); sexp] - -> (try let (_, ltp) = SMap.find vname pending_decls in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp, ltp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, nctx - else - lexp_decls_1 sdecls ectx nctx pending_decls pending_defs - - with Not_found -> - error l ("`" ^ vname ^ "` defined but not declared!"); + -> if SMap.mem vname pending_decls then + let pending_decls = SMap.remove vname pending_decls in + let pending_defs = ((v, sexp) :: pending_defs) in + if SMap.is_empty pending_decls then + let nctx = ectx_new_scope nctx in + let decls, nctx = lexp_check_decls ectx nctx pending_defs in + decls, sdecls, nctx + else + lexp_decls_1 sdecls ectx nctx pending_decls pending_defs + + else + (error l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)

| [Node (Symbol s, args) as d; body]

===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -20,15 +20,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-(* FIXME/TODO: - * - Give more control over the way we strip parentheses. - * E.g. allow some infix operators to keep track whether their args where - * parenthesized or not. Some uses may also want to "not-strip" parentheses - * so as to distinguish "((a b))" from "(a b)". - * - Add another level of tokenizing/parsing: on the first level "M.a" - * can be parsed as one token, and then on the second level, it would - * turn into a call to "." with two arguments. *) - open Util open Prelexer open Grammar

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

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