Stefan pushed to branch master at Stefan / Typer

Commits: b10e7943 by Stefan Monnier at 2017-03-08T23:43:02-05:00 Improve type inference and add `.` macro.

For tuples and `.` macro to work, type inference needed to be improved. This improvement is to annotate metavars so they can't accidentally refer to local vars. IOW rather than "grafted", they're now "logical". This also refined slightly the inversion of substitutions, tho I'm not sure it makes an actual difference in the end.

* btl/pervasive.typer (BoolMod): Prototype of a Bool module. (Pair): New type. (__.__): New macro.

* emacs/typer-mode.el (typer-smie-rules): Add dangling `in` rule, as used in OCaml. Don't move up to the parent when indenting a `case` or `lambda` with a `case`'s branch.

* src/debruijn.ml (scope_level, lctx_length): New types. (elab_context): Add scope data. (make_elab_context): Rename to empty_elab_context. (ectx_new_scope, ectx_get_scope): New functions.

* src/debug_util.ml (main.ctx_to_cctx): Remove, use ectx_to_lctx instead.

* src/inverse_subst.ml (dummy_var): Remove. (substIR): Add destination count. (transfo.transfo): Refine the transformation so it is reversible. (inverse): Check success.

* src/lexp.ml (lexp_name): Move so we can use lexp_string for "trivial" cases. (subst_string): Use it to avoid pathological cases.

* src/lparse.ml (_global_lexp_ctx): Remove. (check): Shift metavars so they can't refer to vars from within the scope. (infer_call.handle_fun_args): Unify two branches. (lexp_decls_1, sform_letin): Introduce new scope for metavars.

* src/pexp.ml (pexp_p_actual_arg): Remove, unused. (pexp_p_decls): Use sexp_u_list.

* tests/eval_test.ml: Add test of the `.` notation.

- - - - -

11 changed files:

- btl/builtins.typer - btl/pervasive.typer - emacs/typer-mode.el - src/debruijn.ml - src/debug_util.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/pexp.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -126,7 +126,7 @@ cons = datacons List cons;

%%%% Macro-related definitions

-%% block_ = Built-in "block_" (List Pretoken -> Sexp); +%% Sexp_block= Built-in "Sexp.block" (List Pretoken -> Sexp); Sexp_symbol = Built-in "Sexp.symbol" (String -> Sexp); Sexp_string = Built-in "Sexp.string" (String -> Sexp); Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); @@ -139,7 +139,7 @@ macro = datacons Macro macro;

Macro_expand : Macro -> List Sexp -> Sexp; Macro_expand m args = case m - | macro f => (f args); + | macro f => f args;

Sexp_dispatch = Built-in "Sexp.dispatch" ( (a : Type) ≡>

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -218,6 +218,40 @@ length = List_length; head = List_head1; tail = List_tail;

+%%%% Tuples + +%% Sample tuple: a module holding Bool and its constructors. +BoolMod = (##datacons (typecons _ (cons (t :: ?) (true :: ?) (false :: ?))) + cons) + (_ := Bool) (_ := true) (_ := false); + +Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); + +__.__ = + let mksel o f = + let constructor = Sexp_node (Sexp_symbol "##datacons") + (cons (Sexp_symbol "?") + (cons (Sexp_symbol "cons") + nil)); + pattern = Sexp_node constructor + (cons (Sexp_node (Sexp_symbol "_:=_") + (cons f (cons (Sexp_symbol "v") + nil))) + nil); + branch = Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons (Sexp_symbol "v") nil)); + in Sexp_node (Sexp_symbol "case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons o (cons branch nil))) + nil) + in macro (lambda args + -> case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + %%%% Logic

%% False should be one of the many empty types.

===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -172,10 +172,12 @@ ;; along the lines of what's done in Tuareg. (pcase (cons kind token) (`(:before . "|") (smie-rule-parent (if (smie-rule-parent-p "type") 2))) + (`(:after . "in") (if (smie-rule-hanging-p) (smie-rule-parent))) (`(:before . "(") (if (smie-rule-hanging-p) (smie-rule-parent))) (`(:before . ,(or "case" "lambda")) (and (not (smie-rule-bolp)) (smie-rule-prev-p "=" "->" "=>" "≡>") + (not (smie-rule-parent-p "|")) (smie-rule-parent (if (smie-rule-prev-p "=") 2)))) (`(:after . "=") 2) (`(:after . ,(or "->" "=>" "≡>"))

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -104,13 +104,20 @@ type scope = db_ridx SMap.t (* Map<String, db_ridx>*) type senv_length = int (* it is not the map true length *) type senv_type = senv_length * scope

+(* Scope level is used to detect "out of scope" metavars. + * See http://okmij.org/ftp/ML/generalization.html + * The lctx_length keeps track of the lctx's length when that scope level was + * entered in order to know by how much to shift metavars. *) +type scope_level = int +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 +type elab_context = senv_type * lexp_context * (scope_level * lctx_length)

(* 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

(* internal definitions * ---------------------------------- *) @@ -122,16 +129,14 @@ let _make_myers = M.nil (* Public methods: DO USE * ---------------------------------- *)

-let make_elab_context = (_make_senv_type, _make_myers) - -let get_roffset ctx = let (_, _, (_, rof)) = ctx in rof +let empty_elab_context : elab_context = (_make_senv_type, _make_myers, (0, 0))

-let get_size ctx = let ((n, _), _) = ctx in n +let get_size ctx = let ((n, _), _, _) = ctx in n

(* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = - let ((n, map), _) = ctx in - n - (SMap.find name map) - 1 + let ((n, map), _, _) = ctx in + n - (SMap.find name map) - 1

let lexp_ctx_cons (ctx : lexp_context) offset d v t = assert (offset >= 0 @@ -150,18 +155,19 @@ 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) = ctx in + let ((n, map), env, sl) = ctx in let nmap = SMap.add name n map in ((n + 1, nmap), - lexp_ctx_cons env r (Some def) v t) + lexp_ctx_cons env r (Some def) v t, + sl)

let env_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec 0 ctx def v t

let ectx_extend (ectx: elab_context) (def: vname option) (v: varbind) (t: lexp) : elab_context = match def with - | None -> let ((n, map), lctx) = ectx in - ((n + 1, map), lexp_ctx_cons lctx 0 None v t) + | None -> let ((n, map), lctx, sl) = ectx in + ((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) = @@ -174,12 +180,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) = ctx in + let ((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) + ((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 ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = + let (_, _, sl) = ectx in sl

let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -410,13 +410,10 @@ let main () = ) flexps));

(* get typecheck context *) - let lctx_to_cctx (lctx: elab_context) = - let (_, env) = ctx in env in - (if (get_p_option "typecheck") then( print_string (make_title " TYPECHECK ");

- let cctx = lctx_to_cctx ctx in + let cctx = ectx_to_lctx ctx in (* run type check *) List.iter (fun (_, lxp, _) -> let _ = OL.check VMap.empty cctx lxp in ())

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -208,7 +208,7 @@ let make_float loc depth args_val = match args_val with

let string_eq loc depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) - | _ -> error loc "string_eq expects 2 strings" + | _ -> error loc "String.= expects 2 strings"

let sexp_eq loc depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) @@ -266,8 +266,8 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type | Builtin ((_, str)) -> Vbuiltin (str)

(* Return a value stored in env *) - | Var((loc, name), idx) as e -> - eval_var ctx e ((loc, name), idx) + | Var((loc, name), idx) as e + -> eval_var ctx e ((loc, name), idx)

(* Nodes *) (* ---------------- *)

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -51,15 +51,14 @@ module S = Subst

type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *)

-let dummy_var = Var((dummy_location, "DummyVar"), -1) - -type substIR = ((int * int) list * int) +type substIR = ((int * int) list * int * int)

(** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) let transfo (s: lexp S.subst) : substIR option = - let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = + let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int) (imp_cnt : int) + : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) match v with | Var (_, v) -> v @@ -70,15 +69,17 @@ let transfo (s: lexp S.subst) : substIR option = in match s with | S.Cons (Var _ as v, s) -> - (match transfo s off_acc (idx + 1) with - | Some (tail, off) -> let newVar = shiftVar v off_acc + (match transfo s off_acc (idx + 1) imp_cnt with + | Some (tail, off, imp) -> let newVar = shiftVar v off_acc in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off) - | None -> None) - | S.Shift (s, offset) -> transfo s (offset + off_acc) idx - | S.Identity -> Some ([], off_acc) (* End of recursion *) + else Some (((shiftVar v off_acc), idx)::tail, off, imp) + | None -> None) + | S.Cons (Imm (Sexp.Symbol (_, "")), s) + -> transfo s off_acc (idx + 1) (imp_cnt + 1) + | S.Shift (s, offset) -> transfo s (offset + off_acc) idx imp_cnt + | S.Identity -> Some ([], off_acc, imp_cnt) (* End of recursion *) | _ -> None (* Error *) - in transfo s 0 0 + in transfo s 0 0 0

(* Inverse *)

@@ -110,7 +111,7 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = in let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) match l with - | [] -> Some (genDummyVar 0 nbVar S.identity) + | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) @@ -122,23 +123,32 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = | None -> None | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s)))

- | (idx1, val1)::(idx2, val2)::tail -> - (match fill_after ((idx2, val2)::tail) nbVar shift with - | None -> None - | Some s -> Some (S.cons (mkVar val1) s)) + | (idx1, val1)::(idx2, val2)::tail + -> (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) s))

- | (idx1, val1)::[] when (idx1 + 1) < nbVar -> - Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift))) + | (idx1, val1)::[] when (idx1 + 1) < nbVar + -> Some (S.cons (mkVar val1) + (genDummyVar (idx1 + 1) nbVar (S.shift shift)))

- | (idx1, val1)::[] -> - Some (S.cons (mkVar val1) (S.shift shift)) + | (idx1, val1)::[] + -> Some (S.cons (mkVar val1) (S.shift shift))

- | [] -> - Some (S.shift shift) + | [] + -> Some (S.shift shift) in match fill_after l nbVar shift with | None -> None | Some s -> fill_before l s nbVar

+let is_identity s = + let rec is_identity s acc = + match s with + | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) + | S.Shift(S.Identity, shift) -> acc = shift + | _ -> S.identity_p s + in is_identity s 0 + (** Compute the inverse, if there is one, of the substitution.

<code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> @@ -147,6 +157,21 @@ let inverse (s: lexp S.subst) : lexp S.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None - | Some (cons_lst, shift_val) -> - let size = sizeOf cons_lst - in fill (sort cons_lst) shift_val size + | Some (cons_lst, shift_val, imp_cnt) + -> let size = imp_cnt + sizeOf cons_lst in + (* print_string ("imp_cnt = " ^ string_of_int imp_cnt + * ^ "; shift_val = " ^ string_of_int shift_val + * ^ "; size = " ^ string_of_int size + * ^ "\n"); *) + let res = fill (sort cons_lst) shift_val size in + (match res with + | Some s1 + -> if is_identity (Lexp.scompose s s1) + || is_identity (Lexp.scompose s1 s) then () + else (print_string ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) + | _ -> ()); + res

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -346,24 +346,6 @@ let clean meta_ctx e = with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e

-let lexp_name e = - match e with - | Imm _ -> "Imm" - | Var _ -> "Var" - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" - | Inductive _ -> "typecons" - | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" - | Metavar _ -> "Metavar" - | Sort _ -> "Sort" - | SortLevel _ -> "SortLevel" - let sdatacons = Symbol (U.dummy_location, "##datacons") let stypecons = Symbol (U.dummy_location, "##typecons")

@@ -491,7 +473,25 @@ and lexp_string lxp = sexp_string (lexp_unparse lxp) and subst_string s = match s with | S.Identity -> "Id" | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" - | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s + | S.Cons (l, s) -> lexp_name l ^ " · " ^ subst_string s + +and lexp_name e = + match e with + | Imm _ -> lexp_string e + | Var _ -> lexp_string e + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" + | Inductive _ -> "typecons" + | Susp _ -> "Susp" + | Builtin (_, _, None) -> "Builtin" + | Builtin _ -> "AttributeTable" + | Metavar _ -> "Metavar" + | Sort _ -> "Sort" + | SortLevel _ -> "SortLevel"

(* ------------------------------------------------------------------------- *) (* Printing *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -60,7 +60,6 @@ let make_var name index loc = (* dummies *) let dloc = dummy_location

-let _global_lexp_ctx = ref make_elab_context let _parsing_internals = ref false let btl_folder = ref "./btl/"

@@ -248,10 +247,6 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

let tloc = sexp_location p in

- (* Save current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context. *) - _global_lexp_ctx := ctx; - match p with | Symbol (l,name) when String.length name >= 1 && String.get name 0 == '#' @@ -446,11 +441,18 @@ 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,"?") -> newMetavar l "v" t - | Symbol (l, name) when String.length name > 1 + | Symbol (l, name) when String.length name >= 1 && String.get name 0 = '?' - -> sexp_error l "Named metavars not supported (yet)"; - newMetavar l name t + -> let name = if name = "?" then "v" else + (sexp_error l "Named metavars not supported (yet)"; + String.sub name 1 (String.length name)) in + let (_, slen) = ectx_get_scope ctx 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 `t` or not. If the user wants ? to be able to refer to + * `t`, then she should explicitly write (y : ? t). *) + mkSusp (newMetavar l name t) (S.shift ((get_size ctx) - slen))

| _ -> infer_and_check p ctx t

@@ -458,7 +460,7 @@ and infer_and_check pexp ctx t = let (e, inferred_t) = infer pexp ctx in check_inferred ctx e inferred_t t

-(* This is a crucial function: take an expression `e` of type `inferred_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 * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) @@ -715,16 +717,15 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = ^ "` have no matching formal args")); largs, ltp

- | sarg :: sargs, Arrow (Aexplicit, _, arg_type, _, ret_type) - -> let larg = check sarg arg_type ctx in + | 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)) - - | sarg :: sargs, t - -> print_lexp_ctx (ectx_to_lctx ctx); - lexp_fatal (sexp_location sarg) t - ("Explicit arg `" ^ sexp_string sarg - ^ "` to non-function (type = " ^ lexp_string ltp ^ ")") in + (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 @@ -850,9 +851,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) -> let adjusted_ltp = push_susp ltp (S.shift (i + 1)) in assert (t == ltp); let e = check pexp adjusted_ltp nctx in - let (ec, lc) = nctx in + let (ec, lc, sl) = nctx in (IntMap.add i (v, e, ltp) map, - (ec, Myers.set_nth i (o, v', LetDef e, t) lc)) + (ec, Myers.set_nth i (o, v', LetDef e, t) lc, sl)) | _ -> U.internal_error "Defining same slot!") defs (IntMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IntMap.bindings declmap)) in @@ -876,7 +877,7 @@ and lexp_decls_1 [], [], nctx

| Ptype ((l, vname) as v, ptp) :: pdecls - -> let ltp = infer_type ptp nctx (Some v) in + -> let ltp = infer_type ptp (ectx_new_scope nctx) (Some v) in if SMap.mem vname pending_decls then (error l ("Variable `" ^ vname ^ "` declared twice!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) @@ -893,7 +894,7 @@ and lexp_decls_1 when SMap.is_empty pending_decls -> assert (pending_defs == []); assert (ectx == nctx); - let (lexp, ltp) = infer pexp nctx in + let (lexp, ltp) = infer pexp (ectx_new_scope nctx) in (* Lexp decls are always recursive, so we have to shift by 1 to account * for the extra var (ourselves). *) [(v, mkSusp lexp (S.shift 1), ltp)], pdecls, @@ -904,6 +905,7 @@ and lexp_decls_1 let pending_decls = SMap.remove vname pending_decls in let pending_defs = ((v, pexp, 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, pdecls, nctx else @@ -1216,7 +1218,7 @@ let sform_letin ctx loc sargs ot = match sargs with -> let pdecls = pexp_p_decls sdecls in let declss, nctx = lexp_p_decls pdecls ctx in (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody nctx in + let bdy, ltp = infer sbody (ectx_new_scope nctx) in let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in (lexp_let_decls declss bdy nctx, Inferred (mkSusp ltp s)) @@ -1316,7 +1318,7 @@ let default_ectx warning dloc "Predef not found"; in

(* Empty context *) - let lctx = make_elab_context in + let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx -> if String.get key 0 = '-' then ctx else ctx_define ctx (dloc, key) e t)

===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -54,16 +54,6 @@ let rec pexp_pat_location e = match e with | Ppatsym (l,_) -> l | Ppatcons (e, _) -> sexp_location e

-and pexp_p_actual_arg arg : (arg_kind * pvar option * sexp) = - match arg with - | Node (Symbol (_, ":≡"), [Symbol s; e]) - -> (Aerasable, Some s, e) - | Node (Symbol (_, ":="), [Symbol s; e]) - -> (Aimplicit, Some s, e) - | Node (Symbol (_, ":-"), [Symbol s; e]) - -> (Aexplicit, Some s, e) - | e -> (Aexplicit, None, e) - and pexp_p_formal_arg arg : (arg_kind * pvar * sexp option) = match arg with | Node (Symbol (_, "_:::_"), [Symbol s; e]) @@ -149,18 +139,16 @@ and pexp_p_decls e: pdecl list = | Symbol (_, "") -> [] | Node (Symbol (_, ("_;_" | "_;" | ";_")), decls) -> List.concat (List.map pexp_p_decls decls) - | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype(s, t)] - | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr(s, t)] + | Node (Symbol (_, "_:_"), [Symbol s; t]) -> [Ptype (s, t)] + | Node (Symbol (_, "_=_"), [Symbol s; t]) -> [Pexpr (s, t)] | Node (Symbol (l, "_=_"), [Node (Symbol s, args) as d; t]) -> + (* FIXME: Hardcode "lambda_->_"! *) [Pexpr (s, Node (Symbol (sexp_location d, "lambda_->_"), - [(match args with - | [] -> Sexp.dummy_epsilon - | arg::args -> Node (arg, args)); - t]))] + [sexp_u_list args; t]))] (* everything else is considered a macro * An error will be produced during lexp_parsing if the macro does not exist * once expanded the Pmcall macro will produce a list of pdecl *) - | Node (Symbol (l, op), args) -> [Pmcall((l, op), args)] + | Node (Symbol (l, op), args) -> [Pmcall ((l, op), args)] | _ -> print_string ((sexp_name e) ^ ": ""); sexp_print e; print_string ""\n"; pexp_error (sexp_location e) ("Unknown declaration"); []

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -372,12 +372,19 @@ let _ = test_eval_eqv_named p : P; p = lambda a ≡> lambda x notx -> notx x; tP : Decidable P; - tP = (datacons Decidable true) (prop := P) (p := p);" + tP = (datacons Decidable true) (prop := P) (p := p); + + ptest : Pair Int String; + ptest = (##datacons Pair cons) (x := 4) (y := "hello"); + + px = case ptest | (##datacons ? cons) (x := v) => v; + + py = ptest.y;"

"case tP | (datacons ? true) (p := _) => 3 - | (datacons ? false) (p := _) => 4;" - "3;" + | (datacons ? false) (p := _) => 4; px; py" + "3; 4; "hello";"

let _ = test_eval_eqv_named "Y"

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