Typer Août 2017

typer@iro.umontreal.ca

1 participants
7 discussions

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][master] Add `define-operator`
by Stefan 22 Aoû '17

22 Aoû '17

Stefan pushed to branch master at Stefan / Typer Commits: e5ac4157 by Stefan Monnier at 2017-08-22T13:10:07-04:00 Add `define-operator` * src/elab.ml (sdform_define_operator): New function. (lexp_decls_macro): Adjust to extra value in context. (lexp_decls_1): Add case for `define-operator`. (elaborate): Treat blocks like immediates. (sform_immediate): Add case for blocks. * src/debruijn.ml (elab_context): Add grammar into the context. * btl/pervasive.typer (List_nth): New function. (quote1): Fix definition. (if_then_else_): Define as a macro. * src/grammar.ml (default_grammar): Move if/then/else... to pervasive.typer. * src/sexp.ml (token): New type alias. * tests/sexp_test.ml: Remove if/then/else test. * tests/eval_test.ml ("Block", "define-operator"): New tests. - - - - - 8 changed files: - btl/builtins.typer - btl/pervasive.typer - src/debruijn.ml - src/elab.ml - src/grammar.ml - src/sexp.ml - tests/eval_test.ml - tests/sexp_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -98,7 +98,7 @@ Float_* = Built-in "Float.*" (Float -> Float -> Float); Float_/ = Built-in "Float./" (Float -> Float -> Float); Float_to_string = Built-in "Float.to_string" (Float -> String); -Bool = typecons (Boolean) (true) (false); +Bool = typecons (Bool) (true) (false); true = datacons Bool true; false = datacons Bool false; ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -79,6 +79,14 @@ List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs; +List_nth : (a : Type) ≡> Int -> List a -> a -> a; +List_nth = lambda n -> lambda xs -> lambda d -> case xs + | nil => d + | cons x xs + => case Int_<= n 0 + | true => x + | false => List_nth (n - 1) xs d; + %%%% A more flexible `lambda` %% An Sexp which we use to represents an error. @@ -158,12 +166,25 @@ K x y = x; %% %% => x +%% Takes an Sexp `x` as argument and return an Sexp which represents code +%% which will construct an Sexp equivalent to `x` at run-time. +%% This is basically "cross stage persistence" for Sexp. quote1 : Sexp -> Sexp; quote1 x = let k = K x; + qlist : List Sexp -> Sexp; + qlist xs = case xs + | nil => Sexp_symbol "nil" + | cons x xs => Sexp_node (Sexp_symbol "cons") + (cons (quote1 x) + (cons (qlist xs) nil)); node op y = case (Sexp_eq op (Sexp_symbol "uquote")) | true => List_head Sexp_error y - | false => Sexp_node (quote1 op) (List_map quote1 y) - in Sexp_dispatch x node k k k k k; + | false => Sexp_node (Sexp_symbol "##Sexp.node") + (cons (quote1 op) + (cons (qlist y) nil)); + symbol s = Sexp_node (Sexp_symbol "##Sexp.symbol") + (cons (Sexp_string s) nil) + in Sexp_dispatch x node symbol k k k k; %% quote definition quote = macro (lambda x -> quote1 (List_head Sexp_error x)); @@ -323,6 +344,21 @@ Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop)); +%%%% If + +define-operator if () 2; +define-operator then 2 1; +define-operator else 1 66; + +if_then_else_ + = macro (lambda args -> + let e1 = List_nth 0 args Sexp_error; + e2 = List_nth 1 args Sexp_error; + e3 = List_nth 2 args Sexp_error; + in quote (case uquote e1 + | true => uquote e2 + | false => uquote e3)); + %%%% Test test1 : Option Int; test2 : Option Int; ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -108,18 +108,22 @@ type lctx_length = db_ridx (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) -type elab_context = senv_type * lexp_context * (scope_level * lctx_length) +type elab_context + = Grammar.grammar * senv_type * lexp_context * (scope_level * lctx_length) -let get_size ctx = let ((n, _), lctx, _) = ctx in +let get_size ctx = let (_, (n, _), lctx, _) = ctx in assert (n = M.length lctx); n -(* Extract the lexp context from the context used during elaboration. *) +let ectx_to_grm (ectx : elab_context) : Grammar.grammar = + let (grm,_, _, _) = ectx in grm + + (* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_, lctx, _) = ectx in lctx + let (_,_, lctx, _) = ectx in lctx -let ectx_to_scope_level ((_, _, (sl, _)) : elab_context) : scope_level = sl +let ectx_to_scope_level ((_, _, _, (sl, _)) : elab_context) : scope_level = sl -let ectx_local_scope_size (((n, _), _, (_, slen)) as ectx: elab_context) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen)) as ectx: elab_context) : int = get_size ectx - slen (* internal definitions @@ -132,11 +136,12 @@ let _make_myers = M.nil (* Public methods: DO USE * ---------------------------------- *) -let empty_elab_context : elab_context = (_make_senv_type, _make_myers, (0, 0)) +let empty_elab_context : elab_context + = (Grammar.default_grammar, _make_senv_type, _make_myers, (0, 0)) (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = - let ((n, map), _, _) = ctx in + let (_, (n, map), _, _) = ctx in n - (SMap.find name map) - 1 let lexp_ctx_cons (ctx : lexp_context) offset d v t = @@ -156,9 +161,9 @@ let lctx_extend (ctx : lexp_context) (def: vname option) (v: varbind) (t: lexp) let env_extend_rec r (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (loc, name) = def in - let ((n, map), env, sl) = ctx in + let (grm, (n, map), env, sl) = ctx in let nmap = SMap.add name n map in - ((n + 1, nmap), + (grm, (n + 1, nmap), lexp_ctx_cons env r (Some def) v t, sl) @@ -167,8 +172,8 @@ let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_ext let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) : elab_context = match def with - | None -> let ((n, map), lctx, sl) = ectx in - ((n + 1, map), lexp_ctx_cons lctx 0 None v t, sl) + | None -> let (grm, (n, map), lctx, sl) = ectx in + (grm, (n + 1, map), lexp_ctx_cons lctx 0 None v t, sl) | Some def -> env_extend ectx def v t let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = @@ -181,19 +186,19 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let ((n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl) = ctx in let senv', _ = List.fold_left (fun (senv, i) ((_, vname), _, _) -> SMap.add vname i senv, i + 1) (senv, n) defs in - ((n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) let ectx_new_scope ectx : elab_context = - let (senv, lctx, (scope, _)) = ectx in - (senv, lctx, (scope + 1, Myers.length lctx)) + let (grm, senv, lctx, (scope, _)) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx)) let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = - let (_, _, sl) = ectx in sl + let (_, _, _, sl) = ectx in sl let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -251,6 +251,20 @@ let mkDummy_infer ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (mkDummy_check ctx loc t, t) +let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context = + match sargs with + | [Symbol (_, name); l; r] + -> let level s = match s with + | Symbol (_, "") -> None + | Integer (_, n) -> Some n + | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in + let (grm, a, b, c) = ctx in + (SMap.add name (level l, level r) grm, a, b, c) + | [o; _; _] + -> sexp_error (sexp_location o) "Expecting a symbol"; ctx + | _ + -> sexp_error loc "define-operator expects 3 argument"; ctx + let elab_varref ctx ((loc, name) as id) = let idx = senv_lookup name ctx in let lxp = make_var name idx loc in @@ -267,11 +281,8 @@ let rec elaborate ctx se ot = (* Break the inf-recursion! *) else elab_varref ctx id - (* Rewrite BLOCK to `typer-block BLOCK`. *) - | Block (l,_,_) -> elaborate ctx (Node (Symbol (l, "typer-block"), [se])) ot - (* Rewrite IMM to `typer-immediate IMM`. *) - | (Integer _ | Float _ | String _) + | (Integer _ | Float _ | String _ | Block _) -> let l = sexp_location se in elaborate ctx (Node (Symbol (l, "typer-immediate"), [se])) ot @@ -756,7 +767,6 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) let macro = lexp_eval ctx macro_funct in let args = [macro; BI.o2v_list sargs] in - (* FIXME: Don't `mkCall + eval` but use eval_call instead! *) (* FIXME: Make a proper `Var`. *) EV.eval_call loc (EL.Var ((DB.dloc, "expand_macro"), 0)) ([], []) macro_expand args @@ -784,6 +794,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (vname * sexp) list) : (vname * lexp * ltype) list * elab_context = + (* Preserve the new operators added to nctx. *) + let ectx = let (_, a, b, c) = ectx in + let (grm, _, _, _) = nctx in + (grm, a, b, c) in let (declmap, nctx) = List.fold_right (fun ((_, vname) as v, pexp) (map, nctx) -> @@ -793,9 +807,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | (o, v', ForwardRef, t) -> 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 + let (grm, ec, lc, sl) = nctx in (IMap.add i (v, e, t) map, - (ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) + (grm, ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in @@ -863,7 +877,8 @@ and lexp_decls_1 | [Symbol ((l, vname) as v); sexp] when SMap.is_empty pending_decls -> assert (pending_defs == []); - assert (ectx == nctx); + (* Used to be true before we added define-operator. *) + (* assert (ectx == nctx); *) let (lexp, ltp) = infer sexp (ectx_new_scope nctx) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) @@ -897,17 +912,22 @@ and lexp_decls_1 | _ -> error l "Invalid definition syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + | Node (Symbol (l, "define-operator"), args) :: sdecls + (* FIXME: Move this to a "special form"! *) + -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None) + pending_decls pending_defs + | Node (Symbol ((l, _) as v), sargs) :: sdecls - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - lexp_decls_1 (sdecl' :: sdecls) ectx nctx - pending_decls pending_defs + -> (* expand macro and get the generated declarations *) + let sdecl' = lexp_decls_macro v sargs nctx in + lexp_decls_1 (sdecl' :: sdecls) ectx nctx + pending_decls pending_defs | sexp :: sdecls -> error (sexp_location sexp) "Invalid declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs -and lexp_p_decls (sdecls : sexp list) ctx +and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = match sdecls with | [] -> [], ctx @@ -1109,6 +1129,11 @@ let sform_immediate ctx loc sargs ot = | [(String _) as se] -> mkImm (se), Inferred DB.type_string | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int | [(Float _) as se] -> mkImm (se), Inferred DB.type_float + | [Block (sl, pts, el)] + -> let (grm, _, _, _) = 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 loc ("Non-immediate passed to ##typer-immediate"); sform_dummy_ret ctx loc) ===================================== src/grammar.ml ===================================== --- a/src/grammar.ml +++ b/src/grammar.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Stefan Monnier <monnier(a)iro.umontreal.ca> * Keywords: languages, lisp, dependent types. @@ -82,13 +82,13 @@ let default_grammar : grammar = (",", Some 41, Some 41); ("::", Some 167, Some 17); (":::", Some 168, Some 16); - ("then", Some 2, Some 1); + (* ("then", Some 2, Some 1); *) (";", Some 14, Some 14); ("type", None, Some 30); ("=", Some 28, Some 29); (":=", Some 170, Some 15); ("in", Some 3, Some 67); - ("else", Some 1, Some 66); + (* ("else", Some 1, Some 66); *) ("|", Some 54, Some 54); (")", Some 0, None); ("->", Some 118, Some 99); @@ -98,6 +98,6 @@ let default_grammar : grammar = (":", Some 79, Some 79); ("lambda", None, Some 118); ("case", None, Some 42); - ("if", None, Some 2); + (* ("if", None, Some 2); *) ("(", None, Some 0) ] ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -36,6 +36,7 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Integer of location * integer | Float of location * float | Node of sexp * sexp list +type token = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location @@ -191,7 +192,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) largs rargs false, []) -let sexp_parse_all grm tokens limit = +let sexp_parse_all grm tokens limit : sexp * token list = let level = match limit with | None -> min_int | Some token -> @@ -224,7 +225,7 @@ let sexp_u_list (ss : sexp list) : sexp = | (s :: ss) -> Node (s, ss) (* Parse all the Sexp *) -let sexp_parse_all_to_list grm tokens limit = +let sexp_parse_all_to_list grm tokens limit : sexp list = let rec sexp_parse_impl grm tokens limit acc = match tokens with (* We are done parsing *) ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -400,6 +400,27 @@ let _ = test_eval_eqv_named "2;" let _ = test_eval_eqv_named + "Block" + + "a = 2" + + "a + 1;" + "{a + 1};" + +let _ = test_eval_eqv_named + "define-operator" + + "define-operator IF () 2; + define-operator THEN 2 1; + define-operator ELSE 1 66; + IF_THEN_ELSE_ = if_then_else_;" + + "{IF true THEN 2 ELSE 3};" + (* FIXME: the new grammar is not used at top-level yet! *) + (* "if true then 2 else 3;" *) + "{if true then 2 else 3};" + +let _ = test_eval_eqv_named "Type Alias" "ListInt = List Int;" "" (* == *) "" (* run all tests *) ===================================== tests/sexp_test.ml ===================================== --- a/tests/sexp_test.ml +++ b/tests/sexp_test.ml @@ -37,7 +37,6 @@ let test_sexp_eqv dcode1 dcode2 = let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" let _ = test_sexp_eqv "(x := y)" "_:=_ x y" -let _ = test_sexp_eqv "if A then B else C -> D" "if A then B else (C -> D)" let _ = test_sexp_eqv "A : B -> C" "A : (B -> C)" let _ = test_sexp_eqv "f __\\; y" "(f (__\\;) y)" let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2" View it on GitLab: https://gitlab.com/monnier/typer/commit/e5ac4157d46d7d915a1f32c9953aaf10c7b… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/e5ac4157d46d7d915a1f32c9953aaf10c7b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/opslexp.ml (check'): Fix handling of erasable datatype args.
by Stefan 06 Aoû '17

06 Aoû '17

Stefan pushed to branch master at Stefan / Typer Commits: b41d99a9 by Stefan Monnier at 2017-08-06T09:20:07-04:00 * src/opslexp.ml (check'): Fix handling of erasable datatype args. - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -452,10 +452,7 @@ let rec check' erased ctx e = "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match lexp_whnf (check_type DB.set_empty ctx t) ctx with - | Sort _ -> () - | _ -> (U.msg_error "TC" (lexp_location t) - "Formal arg type is not a type!"; ())); + -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, Some v, t, l, check (dbset_push ak erased) (DB.lctx_extend ctx (Some v) Variable t) @@ -480,42 +477,46 @@ let rec check' erased ctx e = ft)) ft args | Inductive (l, label, args, cases) - -> let rec arg_loop args ctx = + -> let rec arg_loop ctx erased args = match args with | [] -> let level = SMap.fold (fun _ case level -> - let level, _ = + let level, _, _ = List.fold_left - (fun (level, ctx) (ak, v, t) -> + (fun (level, ctx, erased) (ak, v, t) -> (* FIXME: DB.set_empty seems wrong! *) - (match lexp_whnf (check_type DB.set_empty ctx t) - ctx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> mkSLlub ctx level level' - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ctx; - (* U.internal_error "Oops"; *) - level), - DB.lctx_extend ctx v Variable t) - (level, ctx) + ((match lexp_whnf (check_type erased ctx t) + ctx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> mkSLlub ctx level level' + | tt -> U.msg_error "TC" (lexp_location t) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + DB.print_lexp_ctx ctx; + (* U.internal_error "Oops"; *) + level), + DB.lctx_extend ctx v Variable t, + DB.set_sink 1 erased)) + (level, ctx, erased) case in level) cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> mkArrow (ak, Some v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in - let tct = arg_loop args ctx in + -> let _k = check_type DB.set_empty ctx t in + mkArrow (ak, Some v, t, lexp_location t, + arg_loop (DB.lctx_extend ctx (Some v) Variable t) + (dbset_push ak erased) + args) in + let tct = arg_loop ctx erased args in tct | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) View it on GitLab: https://gitlab.com/monnier/typer/commit/b41d99a9ee13d0f3c3a7fab6a81a9fbc557… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/b41d99a9ee13d0f3c3a7fab6a81a9fbc557… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch report/scheme-2017
by Stefan 06 Aoû '17

06 Aoû '17

Stefan deleted branch report/scheme-2017 at Stefan / Typer --- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml (elaborate): Explain lack of typer-funcall
by Stefan 03 Aoû '17

03 Aoû '17

Stefan pushed to branch master at Stefan / Typer Commits: 2759acf9 by Stefan Monnier at 2017-08-03T16:45:57-04:00 * src/elab.ml (elaborate): Explain lack of typer-funcall - - - - - 1 changed file: - src/elab.ml Changes: ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -285,6 +285,12 @@ let rec elaborate ctx se ot = (BI.get_predef "Macro" ctx)) then 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! + * Maybe I should only elaborate `func` above if it's a symbol + * (and maybe even use `elaborate_varref` rather than indirecting + * through `typr-identifier`)? *) elab_call ctx ft args and infer (p : sexp) (ctx : elab_context): lexp * ltype = View it on GitLab: https://gitlab.com/monnier/typer/commit/2759acf955952dd5b645cc545f360e105fa… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/2759acf955952dd5b645cc545f360e105fa… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 2 commits: * src/elab.ml: Make `elaborate` the core function
by Stefan 03 Aoû '17

03 Aoû '17

Stefan pushed to branch master at Stefan / Typer Commits: 5c157c20 by Stefan Monnier at 2017-08-03T15:36:36-04:00 * src/elab.ml: Make `elaborate` the core function (elaborate): Rewrite, using code from `infer` and `check`. (infer): Rewrite, delegating to `elaborate`. (check): Rewrite, delegating to `elaborate`. (elab_varref): Rename from `infer_varref` and adjust return type. (elab_special_form): Rename from `parse_special_form`; adjust return type. (elab_macro_call): Rename from `handle_macro_call`; adjust return type. (elab_call): Rename from `infer_call`; adjust return type. (sform_lambda): Adjust now that `elaborate` can return Lazy. - - - - - f36cbd42 by Stefan Monnier at 2017-08-03T15:49:39-04:00 * src/elab.ml (sform_immediate): New special form (register_special_forms): Register it. (elaborate): Use it for immediates. - - - - - 1 changed file: - src/elab.ml Changes: ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -88,11 +88,11 @@ let lexp_warning = debug_message warning lexp_name lexp_string let lexp_error = debug_message error lexp_name lexp_string let value_fatal = debug_message fatal value_name value_string -(** Builtin Macros i.e, special forms. *) +(** Type info returned by elaboration. *) type sform_type = - | Inferred of ltype - | Checked - | Lazy + | Checked (* Checked that the expression has the requested type. *) + | Inferred of ltype (* Hasn't looked as the requested type. *) + | Lazy (* Hasn't looked as the requested type, nor inferred a type. *) type special_forms_map = (elab_context -> location -> sexp list -> ltype option @@ -251,62 +251,57 @@ let mkDummy_infer ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (mkDummy_check ctx loc t, t) -let infer_varref ctx ((loc, name) as id) +let elab_varref ctx ((loc, name) as id) = let idx = senv_lookup name ctx in let lxp = make_var name idx loc in let ltp = env_lookup_type ctx (id, idx) in - (lxp, ltp) - -let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = - - match p with - | Symbol ((loc, name) as id) - -> if not (name = "typer-identifier") then - infer (Node (Symbol (loc, "typer-identifier"), [p])) ctx - (* Break the inf-recursion! *) - else infer_varref ctx id - - | Node (se, []) -> infer se ctx - - | Node (func, args) - -> let (f, t) as ft = infer func ctx in - if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then - parse_special_form ctx f args None - else if (OL.conv_p (ectx_to_lctx ctx) t - (BI.get_predef "Macro" ctx)) then - let t = newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (sexp_location func) in - let lxp = handle_macro_call ctx f args t in - (lxp, t) - else - infer_call ctx ft args - - (* Block/String/Integer/Float. *) - | Integer _ -> (mkImm (p), DB.type_int) - | Float _ -> (mkImm (p), DB.type_float) - | String _ -> (mkImm (p), DB.type_string) - | Block _ -> infer (Node (Symbol (sexp_location p, "typer-block"), [p])) - ctx - -and parse_special_form ctx f args ot = + (lxp, Inferred ltp) + +(* Infer or check, as the case may be. *) +let rec elaborate ctx se ot = + match se with + (* Rewrite SYM to `typr-identifier SYM`. *) + | Symbol ((loc, name) as id) + -> if not (name = "typer-identifier") then + elaborate ctx (Node (Symbol (loc, "typer-identifier"), [se])) ot + (* Break the inf-recursion! *) + else elab_varref ctx id + + (* Rewrite BLOCK to `typer-block BLOCK`. *) + | Block (l,_,_) -> elaborate ctx (Node (Symbol (l, "typer-block"), [se])) ot + + (* Rewrite IMM to `typer-immediate IMM`. *) + | (Integer _ | Float _ | String _) + -> let l = sexp_location se in + elaborate ctx (Node (Symbol (l, "typer-immediate"), [se])) ot + + | Node (se, []) -> elaborate ctx se ot + + | Node (func, args) + -> 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 + else if (OL.conv_p (ectx_to_lctx ctx) t + (BI.get_predef "Macro" ctx)) then + elab_macro_call ctx f args ot + else + elab_call ctx ft args + +and infer (p : sexp) (ctx : elab_context): lexp * ltype = + match elaborate ctx p None with + | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" + | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) + | (e, Inferred t) -> (e, t) + +and elab_special_form ctx f args ot = let loc = lexp_location f in match OL.lexp_whnf f (ectx_to_lctx ctx) with | Builtin ((_, name), _, _) -> (* Special form. *) - let (e, ot') = (get_special_form name) ctx loc args ot in - (* `ot` is None if we're inferring and `Some t` if we're checking. *) - (match (ot, ot') with - | (Some t, Checked) -> (e, t) - | _ -> let inferred_t = match ot' with - | Inferred t -> t - | _ -> OL.get_type (ectx_to_lctx ctx) e in - match ot with - | None -> (e, inferred_t) - | Some t -> let e = check_inferred ctx e inferred_t t in - (e, t)) + (get_special_form name) ctx loc args ot | _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - mkDummy_infer ctx loc + sform_dummy_ret ctx loc (* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = @@ -413,29 +408,12 @@ and unify_with_arrow ctx tloc lxp kind var aty | Some [] -> arg, body and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = - - match p with - | Symbol (l,name) - -> check (Node (Symbol (l, "typer-identifier"), [p])) t ctx - - | Node (se, []) -> check se t ctx - - | Node (func, args) - -> let (f, ft) = infer func ctx in - if (OL.conv_p (ectx_to_lctx ctx) ft type_special_form) then - let (e, _) = parse_special_form ctx f args (Some t) in e - else if (OL.conv_p (ectx_to_lctx ctx) ft - (BI.get_predef "Macro" ctx)) then - handle_macro_call ctx f args t - else - let (e, inferred_t) = infer_call ctx (f, ft) args in - check_inferred ctx e inferred_t t - - | _ -> infer_and_check p ctx t - -and infer_and_check pexp ctx t = - let (e, inferred_t) = infer pexp ctx in - check_inferred ctx e inferred_t t + let (e, ot) = elaborate ctx p (Some t) in + match ot with + | Checked -> e + | _ -> let inferred_t = match ot with Inferred t -> t + | _ -> OL.get_type (ectx_to_lctx ctx) e in + check_inferred ctx e inferred_t t (* This is a crucial function: take an expression `e` of type `inferred_t` * and convert it into something of type `t`. Currently the only conversion @@ -613,93 +591,92 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) -and handle_macro_call ctx func args t = +and elab_macro_call ctx func args ot = + let t + = match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + (lexp_location func) + | Some t -> t in let sxp = match lexp_expand_macro (lexp_location func) func args ctx (Some t) with | Vsexp (sxp) -> sxp | v -> value_fatal (lexp_location func) v "Macros should return a Sexp" in - - check sxp t ctx + elaborate ctx sxp ot (* Identify Call Type and return processed call. *) -and infer_call ctx (func, ltp) (sargs: sexp list) = - let loc = lexp_location func in - - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned - * Macro : sqr is returned - * Constructor : a constructor is returned - * Anonymous : lambda *) - - let rec handle_fun_args largs sargs pending ltp = - let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in - match sargs, ltp' with - | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) - when SMap.mem aname pending - -> let sarg = SMap.find aname pending in - let larg = check sarg arg_type ctx in - handle_fun_args ((ak, larg) :: largs) sargs - (SMap.remove aname pending) - (L.mkSusp ret_type (S.substitute larg)) - - | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, - Arrow (ak, _, arg_type, _, ret_type) - when (aname = "_") - (* Explicit-implicit argument. *) - -> let larg = check sarg arg_type ctx in - handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) - - | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, - Arrow _ - -> if SMap.mem aname pending then - sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); - handle_fun_args largs sargs (SMap.add aname sarg pending) ltp - - | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ - -> sexp_error l - ("Explicit arg `" ^ aname ^ "` to non-function " - ^ "(type = " ^ (lexp_string ltp) ^ ")"); - handle_fun_args largs sargs pending ltp - - (* Aerasable *) - | _, Arrow ((Aerasable | Aimplicit) as ak, v, arg_type, _, ret_type) - (* Don't instantiate after the last explicit arg: the rest is done, - * when needed in infer_and_check (via instantiate_implicit). *) - when not (sargs = [] && SMap.is_empty pending) - -> let larg = get_implicit_arg - ctx (match sargs with - | [] -> loc - | sarg::_ -> sexp_location sarg) - (match v with Some (_, name) -> name | _ -> "v") - arg_type in - handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) - | [], _ - -> (if not (SMap.is_empty pending) then - let pending = SMap.bindings pending in - let loc = match pending with - | (_, sarg)::_ -> sexp_location sarg - | _ -> assert false in - lexp_error loc func - ("Explicit actual args `" - ^ String.concat ", " (List.map (fun (l, _) -> l) - pending) - ^ "` have no matching formal args")); - largs, ltp - - | sarg :: sargs, _ - -> let (arg_type, ret_type) = match ltp' with - | Arrow (ak, _, arg_type, _, ret_type) - -> assert (ak = Aexplicit); (arg_type, ret_type) - | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Aexplicit (dloc, "<anon>") None in - let larg = check sarg arg_type ctx in - handle_fun_args ((Aexplicit, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) in - - let largs, ret_type = handle_fun_args [] sargs SMap.empty ltp in - mkCall (func, List.rev largs), ret_type +and elab_call ctx (func, ltp) (sargs: sexp list) = + let loc = lexp_location func in + + let rec handle_fun_args largs sargs pending ltp = + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in + match sargs, ltp' with + | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) + when SMap.mem aname pending + -> let sarg = SMap.find aname pending in + let larg = check sarg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs + (SMap.remove aname pending) + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, + Arrow (ak, _, arg_type, _, ret_type) + when (aname = "_") + (* Explicit-implicit argument. *) + -> let larg = check sarg arg_type ctx in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + + | (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, + Arrow _ + -> if SMap.mem aname pending then + sexp_error l ("Duplicate explicit arg `" ^ aname ^ "`"); + handle_fun_args largs sargs (SMap.add aname sarg pending) ltp + + | (Node (Symbol (_, "_:=_"), Symbol (l, aname) :: _)) :: sargs, _ + -> sexp_error l + ("Explicit arg `" ^ aname ^ "` to non-function " + ^ "(type = " ^ (lexp_string ltp) ^ ")"); + handle_fun_args largs sargs pending ltp + + (* Aerasable *) + | _, Arrow ((Aerasable | Aimplicit) as ak, v, arg_type, _, ret_type) + (* Don't instantiate after the last explicit arg: the rest is done, + * when needed in infer_and_check (via instantiate_implicit). *) + when not (sargs = [] && SMap.is_empty pending) + -> let larg = get_implicit_arg + ctx (match sargs with + | [] -> loc + | sarg::_ -> sexp_location sarg) + (match v with Some (_, name) -> name | _ -> "v") + arg_type in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) + | [], _ + -> (if not (SMap.is_empty pending) then + let pending = SMap.bindings pending in + let loc = match pending with + | (_, sarg)::_ -> sexp_location sarg + | _ -> assert false in + lexp_error loc func + ("Explicit actual args `" + ^ String.concat ", " (List.map (fun (l, _) -> l) + pending) + ^ "` have no matching formal args")); + largs, ltp + + | sarg :: sargs, _ + -> let (arg_type, ret_type) = match ltp' with + | Arrow (ak, _, arg_type, _, ret_type) + -> assert (ak = Aexplicit); (arg_type, ret_type) + | _ -> unify_with_arrow ctx (sexp_location sarg) + ltp' Aexplicit (dloc, "<anon>") None in + let larg = check sarg arg_type ctx in + handle_fun_args ((Aexplicit, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) in + + let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in + (mkCall (func, List.rev largs), Inferred ret_type) (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1121,6 +1098,19 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error 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_int + | [(Float _) as se] -> mkImm (se), Inferred DB.type_float + | [se] + -> (sexp_error loc ("Non-immediate passed to ##typer-immediate"); + sform_dummy_ret ctx loc) + | _ + -> (sexp_error 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)] @@ -1161,9 +1151,7 @@ let sform_identifier ctx loc sargs ot = (* Normal identifier. *) | [Symbol id] - -> (try let (e, t) = infer_varref ctx id in - (e, Inferred t) - + -> (try elab_varref ctx id with Not_found -> (let (loc, name) = id in sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); @@ -1177,13 +1165,6 @@ let sform_identifier ctx loc sargs ot = -> (sexp_error loc ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc) -(* Infer or check, as the case may be. *) -let elaborate ctx pe ot = - match ot with - | Some t -> (check pe t ctx, Checked) - | None -> let (le, lt) = infer pe ctx in - (le, Inferred lt) - let var_of_ovar l ov = match ov with | None -> (l, "<anon>") | Some v -> v @@ -1207,10 +1188,8 @@ let rec sform_lambda kind ctx loc sargs ot = 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 + | Inferred lt2 -> Inferred (mkArrow (kind, Some arg, lt1, loc, lt2)) + | _ -> alt) in (match ot with | None -> mklam (match olt1 with @@ -1231,11 +1210,11 @@ let rec sform_lambda kind ctx loc sargs ot = ^ lexp_string lt1 ^ "`")); mklam lt1 (Some lt2) - | Arrow (ak2, v, lt1, _, lt2) when kind = Aexplicit + | Arrow (ak2, ov, 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 + -> let v = var_of_ovar loc ov 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? *) @@ -1243,8 +1222,10 @@ let rec sform_lambda kind ctx loc sargs ot = (* 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) + (mkLambda (ak2, v, lt1, lam), + match alt with + | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2')) + | _ -> alt) | lt -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 @@ -1325,6 +1306,7 @@ let register_special_forms () = [ ("Built-in", sform_built_in); ("typer-identifier", sform_identifier); + ("typer-immediate", sform_immediate); ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); View it on GitLab: https://gitlab.com/monnier/typer/compare/27dd27dc9e57f84a56a06c830a47020112… --- View it on GitLab: https://gitlab.com/monnier/typer/compare/27dd27dc9e57f84a56a06c830a47020112… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml: Make symbols into shorthands for `typer-identifier SYM`
by Stefan 03 Aoû '17

03 Aoû '17

Stefan pushed to branch master at Stefan / Typer Commits: 27dd27dc by Stefan Monnier at 2017-08-03T14:25:36-04:00 * src/elab.ml: Make symbols into shorthands for `typer-identifier SYM` (newMetalevel, newMetatype): Take a lexp_context i.s.o elab_context. (infer_varref): New function, extracted from `infer`. (infer): Make symbols into shorthands for `typer-identifier SYM` and blocks into shorthands for `typer-block BLOCK`. (check): Same rewrite for symbols. (sform_identifier): New functions, using code extracted from `infer` and `check`. (register_special_forms): Use it to implement `typer-identifier`. - - - - - 2 changed files: - src/elab.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -236,51 +236,35 @@ let newMetavar (ctx : lexp_context) sl l name t= let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.Identity, (l, name)) -let newMetalevel (ctx : elab_context) sl = - newMetavar (ectx_to_lctx ctx) sl Util.dummy_location "l" type_level +let newMetalevel (ctx : lexp_context) sl = + newMetavar ctx sl Util.dummy_location "l" type_level -let newMetatype (ctx : elab_context) sl loc - = newMetavar (ectx_to_lctx ctx) sl loc - "t" (mkSort (loc, Stype (newMetalevel ctx sl))) +let newMetatype (ctx : lexp_context) sl loc + = newMetavar ctx sl loc "t" (mkSort (loc, Stype (newMetalevel ctx sl))) (* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) -let mkDummy_type ctx loc = newMetatype ctx dummy_scope_level loc +let mkDummy_type ctx loc = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "dummy" t let mkDummy_infer ctx loc = - let t = newMetatype ctx dummy_scope_level loc in (mkDummy_check ctx loc t, t) + let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in + (mkDummy_check ctx loc t, t) -let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = +let infer_varref ctx ((loc, name) as id) + = let idx = senv_lookup name ctx in + let lxp = make_var name idx loc in + let ltp = env_lookup_type ctx (id, idx) in + (lxp, ltp) - let tloc = sexp_location p in +let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = match p 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 SMap.find name (! BI.lmap) - with Not_found - -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); - mkDummy_infer ctx l - else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); - mkDummy_infer ctx l) - - (* Symbol i.e identifier. *) - | Symbol (loc, name) - when String.length name < 1 || String.get name 0 != '?' - -> (try - let idx = senv_lookup name ctx in - let lxp = make_var name idx loc in - - (* Search type. *) - let ltp = env_lookup_type ctx ((loc, name), idx) in - lxp, ltp - - with Not_found -> - (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); - mkDummy_infer ctx loc)) + | Symbol ((loc, name) as id) + -> if not (name = "typer-identifier") then + infer (Node (Symbol (loc, "typer-identifier"), [p])) ctx + (* Break the inf-recursion! *) + else infer_varref ctx id | Node (se, []) -> infer se ctx @@ -290,29 +274,19 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = parse_special_form ctx f args None else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype ctx (ectx_to_scope_level ctx) + let t = newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else infer_call ctx ft args - | Symbol (_, name) - -> assert (String.length name >= 1 || String.get name 0 = '?'); - let t = newMetatype ctx (ectx_to_scope_level ctx) (sexp_location p) in - let lxp = check p t ctx in - (lxp, t) - (* Block/String/Integer/Float. *) - | v - -> (mkImm (v), - match v with - | Integer _ -> DB.type_int - | Float _ -> DB.type_float - | String _ -> DB.type_string; - | _ -> sexp_error tloc "Could not find type"; - mkDummy_type ctx tloc) - + | Integer _ -> (mkImm (p), DB.type_int) + | Float _ -> (mkImm (p), DB.type_float) + | String _ -> (mkImm (p), DB.type_string) + | Block _ -> infer (Node (Symbol (sexp_location p, "typer-block"), [p])) + ctx and parse_special_form ctx f args ot = let loc = lexp_location f in @@ -395,7 +369,8 @@ and infer_type pexp ectx var = match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel - ectx (ectx_to_scope_level ectx)))) + (ectx_to_lctx ectx) + (ectx_to_scope_level ectx)))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -417,10 +392,10 @@ and lexp_let_decls declss (body: lexp) ctx = and unify_with_arrow ctx tloc lxp kind var aty = let arg = match aty with - | None -> newMetatype ctx (ectx_to_scope_level ctx) tloc + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc | Some laty -> laty in let nctx = ectx_extend ctx (Some var) Variable arg in - let body = newMetatype nctx (ectx_to_scope_level ctx) tloc in + let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in let arrow = mkArrow (kind, Some var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with @@ -440,6 +415,9 @@ and unify_with_arrow ctx tloc lxp kind var aty and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = match p with + | Symbol (l,name) + -> check (Node (Symbol (l, "typer-identifier"), [p])) t ctx + | Node (se, []) -> check se t ctx | Node (func, args) @@ -453,24 +431,6 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = let (e, inferred_t) = infer_call ctx (f, ft) args in check_inferred ctx e inferred_t t - | Symbol (l, name) when String.length name >= 1 - && String.get name 0 = '?' - -> let name = if name = "?" then "v" else - (sexp_error l "Named metavars not supported (yet)"; - 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 she 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 - (* FIXME: `t` is defined in ctx instead of octx. - * We need something like: - * let t = push_inv_subst t (S.shift ctx_shift) in *) - mkSusp (newMetavar octx (ectx_to_scope_level ctx) l name t) - (S.shift ctx_shift) - | _ -> infer_and_check p ctx t and infer_and_check pexp ctx t = @@ -1024,7 +984,7 @@ and get_attribute ctx loc largs = with Not_found -> None and sform_dummy_ret ctx loc = - let t = newMetatype ctx dummy_scope_level loc in + let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t, Inferred t) @@ -1114,7 +1074,8 @@ let sform_typecons ctx loc sargs ot = let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l | None -> let (l,_) = var in - newMetatype ctx (ectx_to_scope_level ctx) l in + newMetatype (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) l in parse_formals sformals ((kind, var, ltp) :: rformals) (env_extend ctx var Variable ltp) in @@ -1160,6 +1121,62 @@ let sform_arrow kind ctx loc sargs ot = | _ -> sexp_error loc "##_->_ takes two arguments"; 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 `" ^ name ^ "`"); + sform_dummy_ret ctx loc + else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); + sform_dummy_ret ctx loc) + + | [Symbol (loc, name)] + when String.length name >= 1 && String.get name 0 = '?' + -> assert (String.length name >= 1 && String.get name 0 = '?'); + let name = if name = "?" then "" else + (sexp_error loc "Named metavars not supported (yet)"; + 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 she 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 t = match ot with + | None -> newMetatype octx sl loc + (* FIXME: `t` is defined in ctx instead of octx. + * We need something like: + * let t = push_inv_subst t (S.shift ctx_shift) in *) + | Some t -> t in + (mkSusp (newMetavar octx sl loc name t) subst, + match ot with Some _ -> Checked | None -> Lazy) + + (* Normal identifier. *) + | [Symbol id] + -> (try let (e, t) = infer_varref ctx id in + (e, Inferred t) + + with Not_found -> + (let (loc, name) = id in + sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); + sform_dummy_ret ctx loc)) + + | [se] + -> (sexp_error loc ("Non-symbol passed to ##typer-identifier"); + sform_dummy_ret ctx loc) + + | _ + -> (sexp_error loc ("Too many args to ##typer-identifier"); + sform_dummy_ret ctx loc) + (* Infer or check, as the case may be. *) let elaborate ctx pe ot = match ot with @@ -1198,7 +1215,8 @@ let rec sform_lambda kind ctx loc sargs ot = (match ot with | None -> mklam (match olt1 with | Some lt1 -> lt1 - | None -> newMetatype ctx (ectx_to_scope_level ctx) loc) + | None -> newMetatype (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) loc) None (* Read var type from the provided type *) | Some t @@ -1249,7 +1267,7 @@ let rec sform_case ctx loc sargs ot = match sargs with let pcases = List.map parse_case scases in let t = match ot with | Some t -> t - | None -> newMetatype ctx (ectx_to_scope_level ctx) loc in + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t) @@ -1306,6 +1324,7 @@ let register_special_forms () = List.iter add_special_form [ ("Built-in", sform_built_in); + ("typer-identifier", sform_identifier); ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -67,11 +67,11 @@ let unify_and res op = match res with (****************************** Top level unify *************************************) -(** Dispatch to the right unifyer. +(** Dispatch to the right unifier. If (<code>_unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) - The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) + The metavar unifier is the end rule, it can't call unify with its parameter (changing their order) *) let rec unify (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) View it on GitLab: https://gitlab.com/monnier/typer/commit/27dd27dc9e57f84a56a06c830a470201127… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/27dd27dc9e57f84a56a06c830a470201127… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2017