Octobre 2016 - Typer - mailman.iro.umontreal.ca

Mutually recursive definitions of datatypes
by Stefan Monnier 01 Nov '16

01 Nov '16

Hi follow Typers (or should I say Typerers)? I bumped into a problem with the current Typer design and am looking for ideas to solve it. As you may know, datatypes (aka inductive types) are defined as *expressions* of the form inductive_ (<dummylabel> <args>) <constrs>... such as inductive_ (option (a: Type)) none (some a) but the <dummylabel> is just that (a label), not a variable. Same for the constructor names, they're just labels and not variables. So we usually bind this to a variable in a declaration, as in: Option = inductive_ (option (a: Type)) (none) (some a); and constructors have the form (inductive-cons <type> <label>), which again is just an anonymous expression which we then bind to a variable in declarations such as None = inductive-cons option none; Some = inductive-cons option some; This is very close to the usual "paper" definition of CIC and seems to work OK so far (tho we'll want to systematize those names, and Typer will have to work a bit harder at trying to hide those internal definitions so that it uses the "Option" and "Some" variables rather than their corresponding values in error messages). But I have a problem with mutual recursion. Typer allows mutual recursion in declarations via "forward type declarations". E.g. Nat : Type; Nat = inductive_ nat z (s Nat); The way mutual recursion works is that we first collect the types of all the mutual declarations (to build a new type environment), then type each declaration within this new environment. But this environment knows nothing about the *values* of those new variables. So if we do: Nat : Type; Z : Nat; Nat = inductive_ nat z (s Nat); Z = inductive-cons Nat z; Typer complains that it can't verify that the Nat argument to inductive-cons is indeed an inductive type (since all it knows is that Nat has type "Type" but it doesn't know its definition (yet)) and as a consequence it can't figure out the type of "Z". Of course, we can say "don't do that", and just force the user to move the constructor declarations to after the mutual recursion, but it's very problematic in practice. E.g. Typically, a type declaration will really use the "type" macro, so you write type Option a | None | Some a; which expands to Option = inductive_ (Option (a: Type)) (None) (Some a); None = inductive-cons option None; Some = inductive-cons option Some; So of course, two mutually recursive type declarations will look like Ta : Type; Tb : Type; type Ta | Ca1 Tb | Ca2; type Tb | Cb1 Ta | Cb2; which expands to Ta : Type; Tb : Type; Ta = inductive_ Ta (Ca1 Tb) Ca2; Ca1 = inductive-cons Ta Ca1; Ca2 = inductive-cons Ta Ca2; Tb = inductive_ Tb (Cb1 Ta) Ca2; Cb1 = inductive-cons Ta Cb1; Cb2 = inductive-cons Ta Cb2; At this point, you can see that it's difficult for the programmer (both the one using the "type" macro and the one defining it) to make sure the declarations occur after the mutual recursion. The best idea I had so far is to change the way mutual-recursion is handled such that the typing is each definition is not done in a context where we only know the type of other defs, but one where we also know the definition of all *previous* definitions. That might prove a bit tricky to code because of how we currently handle cases like A : Ta; B : Tb; B = DefB; A = DefA; where definitions don't come in the same order as declarations (so we want to type-check DefB before DefA even though A will come first in the environment since the relative ordering depends on the order of the type declarations). Stefan

3 2

[Git][monnier/typer][unification] * lparse.ml: Move Pmetavar from infer to check
by Stefan 31 Oct '16

31 Oct '16

Stefan pushed to branch unification at Stefan / Typer Commits: f4010f96 by Stefan Monnier at 2016-10-31T12:46:11-04:00 * lparse.ml: Move Pmetavar from infer to check - - - - - 1 changed file: - src/lparse.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -363,16 +363,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Cons(idt, sym), cons_type - | Pmetavar _ - -> let t = mkMetatype () in - let e = mkMetavar t in - (e, t) - | Phastype (_, pxp, ptp) -> let ltp = lexp_type_infer ptp ctx None trace in (_lexp_p_check pxp ltp ctx trace), ltp - | (Plambda _ | Pcase _) + | (Plambda _ | Pcase _ | Pmetavar _) -> let t = mkMetatype () in let lxp = _lexp_p_check p t ctx trace in (lxp, t) @@ -454,6 +449,8 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *) + | Pmetavar _ -> mkMetavar t + | _ -> lexp_p_infer_and_check p ctx t trace and lexp_p_infer_and_check pexp ctx t i = View it on GitLab: https://gitlab.com/monnier/typer/commit/f4010f969534693155443e22588514b8152…

1 0

[Git][monnier/typer][unification] 3 commits: * src/lparse.ml (_lexp_p_infer): Mostly cosmetic changes
by Stefan 31 Oct '16

31 Oct '16

Stefan pushed to branch unification at Stefan / Typer Commits: 815b8bce by Stefan Monnier at 2016-10-28T22:06:51-04:00 * src/lparse.ml (_lexp_p_infer): Mostly cosmetic changes * src/lparse.ml (elab_check_sort, elab_check_proper_type): Make `var` into `option` type. (lexp_type_infer): New function. (_lexp_p_infer): Re-layout and indent. Don't use OL.check to detect user errors. Check that Phastype's annotation is a proper type. (lexp_let_decls): Use fold_right. * GNUmakefile (BUILDDIR): New var. Use everywhere. - - - - - 31c63489 by Stefan Monnier at 2016-10-28T23:55:25-04:00 * src/lparse.ml (_lexp_p_infer): Fix return type of `Let` * src/opslexp.ml (lexp_defs_subst): New function. (lexp_whnf): Return original exp in `Case`. Complete commented out `Let` case. * tests/eval_test.ml ("Let2"): New test. - - - - - 33d80b67 by Stefan Monnier at 2016-10-31T12:43:25-04:00 Merge branch 'trunk' into unification - - - - - 4 changed files: - GNUmakefile - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,10 +1,12 @@ RM=rm -f +BUILDDIR := _build + SRC_FILES := $(wildcard ./src/*.ml) -CPL_FILES := $(wildcard ./_build/src/*.cmo) +CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -lflags -g -cflags -g -build-dir _build +OBFLAGS = -lflags -g -cflags -g -build-dir $(BUILDDIR) # COMPILE_MODE = native all: typer debug tests-build @@ -23,7 +25,7 @@ debug: # Build debug utils # ============================ ocamlbuild src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/debug_util.$(COMPILE_MODE) _build/debug_util + @mv $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util # interactive typer typer: @@ -31,22 +33,25 @@ typer: # Build typer # ============================ ocamlbuild src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/REPL.$(COMPILE_MODE) _build/typer + @mv $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer tests-build: # ============================ # Build tests # ============================ - @$(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) -I src $(OBFLAGS);) + @$(foreach test, $(TEST_FILES), \ + ocamlbuild $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) \ + -I src $(OBFLAGS);) @ocamlbuild tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/tests/utest_main.$(COMPILE_MODE) _build/tests/utests + @mv $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ + $(BUILDDIR)/tests/utests tests-run: - @./_build/tests/utests --verbose= 3 + @./$(BUILDDIR)/tests/utests --verbose= 3 test-file: ocamlbuild src/test.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/test.$(COMPILE_MODE) _build/test + @mv $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test # There is nothing here. I use this to test if opam integration works install: tests @@ -59,28 +64,29 @@ doc-tex: # Make implementation doc doc-ocaml: - ocamldoc -html -d _build/doc $(SRC_FILES) + ocamldoc -html -d $(BUILDDIR)/doc $(SRC_FILES) -# everything is expected to be compiled in the "./_build/" folder +# everything is expected to be compiled in the "./$(BUILDDIR)/" folder clean: - -rm -rf _build + -rm -rf $(BUILDDIR) .PHONY: typer debug tests run/typecheck: - @./_build/debug_util ./samples/test__.typer -typecheck + @./$(BUILDDIR)/debug_util ./samples/test__.typer -typecheck run/debug_util: - @./_build/debug_util ./samples/test__.typer -fmt-type=on -fmt-index=off -fmt-pretty=on + @./$(BUILDDIR)/debug_util ./samples/test__.typer \ + -fmt-type=on -fmt-index=off -fmt-pretty=on run/typer: - @./_build/typer + @./$(BUILDDIR)/typer run/tests: - @./_build/tests/utests --verbose= 1 + @./$(BUILDDIR)/tests/utests --verbose= 1 run/typer-file: - @./_build/typer ./samples/test__.typer + @./$(BUILDDIR)/typer ./samples/test__.typer run/test-file: - @./_build/test + @./$(BUILDDIR)/test ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -95,20 +95,26 @@ let value_fatal = debug_message fatal value_name value_string (* :-( *) let global_substitution = ref (empty_subst, []) -let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = +let elab_check_sort (ctx : elab_context) lsort var ltp = let meta_ctx, _ = !global_substitution in match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) - | k -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp ^ " : " ^ lexp_string lsort); - -let elab_check_proper_type (ctx : elab_context) ltp v = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp + | _ -> match var with + | None -> lexp_error (lexp_location ltp) ltp + ("`" ^ lexp_string ltp ^ "` is not a proper type") + | Some (l, name) + -> lexp_error l ltp + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp) + +let elab_check_proper_type (ctx : elab_context) ltp var = + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; - print_string ("` of var `" - ^ (let (_, name) = v in name) ^"`\n"); + (match var with + | None -> () + | Some (_, name) + -> print_string ("` of var `" ^ name ^"`\n")); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -124,7 +130,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is * convertible to `Type_0`, because it doesn't have access to lctx. *) if true (* OL.conv_p ltype ltype' *) then - elab_check_proper_type ctx ltype var + elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); @@ -132,7 +138,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = - elab_check_proper_type ctx ltype (maybev var); + elab_check_proper_type ctx ltype var; ectx_extend ctx var def ltype let ctx_define (ctx: elab_context) var lxp ltype = @@ -143,7 +149,7 @@ let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) var; + nctx (push_susp ltp (S.shift n)) (Some var); n - 1) (List.length decls) decls in @@ -223,149 +229,164 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let tloc = pexp_location p in let lexp_infer p ctx = _lexp_p_infer p ctx trace in - (* Save current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context *) + (* 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; _global_lexp_trace := trace; match p with - (* Block/String/Integer/Float *) - | Pimm v -> (Imm(v), - match v with - | Integer _ -> type_int - | Float _ -> type_float - | String _ -> type_string; - | _ -> pexp_error tloc p "Could not find type"; - dltype) - - (* Symbol i.e identifier *) - | Pvar (loc, name) ->( - 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 (* Return Macro[22] *) - - with Not_found -> - (print_lexp_ctx (ectx_to_lctx ctx); - pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); - (* Error recovery. The -1 index will raise an error later on *) - (make_var name (-1) loc), dltype)) - - (* Let, Variable declaration + local scope *) - | Plet(loc, decls, body) -> - let decls, nctx = _lexp_decls decls ctx trace in - let bdy, ltp = lexp_infer body nctx in - (lexp_let_decls decls bdy nctx trace), ltp - - (* ------------------------------------------------------------------ *) - | Parrow (kind, ovar, tp, loc, expr) -> - let ltp, _ = lexp_infer tp ctx in - let _ = elab_check_proper_type ctx ltp (maybev ovar) in - let nctx = ectx_extend ctx ovar Variable ltp in - - let lxp, _ = lexp_infer expr nctx in - let _ = elab_check_proper_type nctx lxp (maybev ovar) in - - let v = Arrow(kind, ovar, ltp, tloc, lxp) in - v, type0 - - (* Pinductive *) - | Pinductive (label, formal_args, ctors) -> - let nctx = ref ctx in - (* (arg_kind * pvar * pexp option) list *) - let formal = List.map (fun (kind, var, opxp) -> - let ltp, _ = match opxp with - | Some pxp -> _lexp_p_infer pxp !nctx trace - | None -> dltype, dltype in - - nctx := env_extend !nctx var Variable ltp; - (kind, var, ltp) - ) formal_args in - - let nctx = !nctx in - let ltp = List.fold_left (fun tp (kind, v, ltp) - -> (Arrow (kind, Some v, ltp, tloc, tp))) - (* FIXME: See OL.check for how to - * compute the real target sort - * (not always type0). *) - type0 (List.rev formal) in - - let map_ctor = lexp_parse_inductive ctors nctx trace in - let v = Inductive(tloc, label, formal, map_ctor) in - v, ltp - - | Pcall (fname, _args) -> - lexp_call fname _args ctx trace - - (* Pcons *) - | Pcons(t, sym) -> - let idt, _ = lexp_infer t ctx in - let (loc, cname) = sym in - let meta_ctx, _ = !global_substitution in - - (* Get constructor args *) - let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) - meta_ctx with - | Inductive(_, _, formal, ctor_def) as lxp -> ( - try formal, (SMap.find cname ctor_def) - with Not_found -> - lexp_error loc lxp - ("Constructor \"" ^ cname ^ "\" does not exist"); - [], []) - - | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in - - (* Build Arrow type. *) - let target = if formal = [] then - push_susp idt (S.shift (List.length args)) - else - let targs, _ = - List.fold_right - (fun (ak, v, _) (targs, i) - -> ((ak, Var (v, i)) :: targs, - i - 1)) - formal - ([], List.length formal + List.length args - 1) in - Call (push_susp idt (S.shift (List.length formal - + List.length args)), - targs) in - let cons_type - = List.fold_left (fun ltp (kind, v, tp) - -> Arrow (kind, v, tp, loc, ltp)) - target - (List.rev args) in - - (* Add Aerasable arguments. *) - let cons_type = List.fold_left - (fun ltp (kind, v, tp) - -> Arrow (Aerasable, Some v, tp, loc, ltp)) - cons_type (List.rev formal) in - - Cons(idt, sym), cons_type - - | Pmetavar _ - -> let t = mkMetatype () in - let e = mkMetavar t in - (e, t) - - | Phastype (_, pxp, ptp) - -> let ltp, _ = lexp_infer ptp ctx in - (_lexp_p_check pxp ltp ctx trace), ltp - - | (Plambda _ | Pcase _) - -> let t = mkMetatype () in - let lxp = _lexp_p_check p t ctx trace in - (lxp, t) - - -and lexp_let_decls decls (body: lexp) ctx i = - (* build the weird looking let *) - let decls = List.rev decls in - List.fold_left (fun lxp decls -> - Let(dloc, decls, lxp)) body decls + (* Block/String/Integer/Float. *) + | Pimm v + -> (Imm(v), + match v with + | Integer _ -> type_int + | Float _ -> type_float + | String _ -> type_string; + | _ -> pexp_error tloc p "Could not find type"; + dltype) + + (* Symbol i.e identifier. *) + | Pvar (loc, name) + -> (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 (* Return Macro[22] *) + + with Not_found -> + (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (* Error recovery. The -1 index will raise an error later on *) + (make_var name (-1) loc), dltype)) + + (* Let, Variable declaration + local scope. *) + | Plet (loc, decls, body) + -> let declss, nctx = _lexp_decls decls ctx trace in + let bdy, ltp = lexp_infer body nctx in + let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in + (lexp_let_decls declss bdy nctx trace), + mkSusp ltp s + + (* ------------------------------------------------------------------ *) + | Parrow (kind, ovar, tp, loc, expr) + -> let ltp = lexp_type_infer tp ctx ovar trace in + let nctx = ectx_extend ctx ovar Variable ltp in + + let lxp = lexp_type_infer expr nctx None trace in + + let v = Arrow(kind, ovar, ltp, tloc, lxp) in + v, type0 + + | Pinductive (label, formal_args, ctors) + -> let nctx = ref ctx in + (* (arg_kind * pvar * pexp option) list *) + let formal = List.map (fun (kind, var, opxp) + -> let ltp, _ = match opxp with + | Some pxp -> _lexp_p_infer pxp !nctx trace + | None -> dltype, dltype in + + nctx := env_extend !nctx var Variable ltp; + (kind, var, ltp)) + formal_args in + + let nctx = !nctx in + let ltp = List.fold_left (fun tp (kind, v, ltp) + -> (Arrow (kind, Some v, ltp, tloc, tp))) + (* FIXME: See OL.check for how to + * compute the real target sort + * (not always type0). *) + type0 (List.rev formal) in + + let map_ctor = lexp_parse_inductive ctors nctx trace in + let v = Inductive(tloc, label, formal, map_ctor) in + v, ltp + + (* This case can be inferred *) + (* | Plambda (kind, var, optype, body) + * -> let ltp, _ = match optype with + * | Some ptype -> lexp_infer ptype ctx + * (\* This case must have been lexp_p_check *\) + * | None -> pexp_error tloc p "Lambda require type annotation"; + * dltype, dltype in + * + * let nctx = env_extend ctx var Variable ltp in + * let lbody, lbtp = lexp_infer body nctx in + * + * let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in + * Lambda(kind, var, ltp, lbody), lambda_type *) + + | Pcall (fname, _args) -> lexp_call fname _args ctx trace + + | Pcons(t, sym) + -> let idt, _ = lexp_infer t ctx in + let (loc, cname) = sym in + let meta_ctx, _ = !global_substitution in + + (* Get constructor args. *) + let formal, args = match OL.lexp_whnf idt + (ectx_to_lctx ctx) meta_ctx with + | Inductive(_, _, formal, ctor_def) as lxp + -> (try formal, (SMap.find cname ctor_def) + with Not_found -> + lexp_error loc lxp + ("Constructor \"" ^ cname ^ "\" does not exist"); + [], []) + + | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in + + (* Build Arrow type. *) + let target = if formal = [] then + push_susp idt (S.shift (List.length args)) + else + let targs, _ + = List.fold_right + (fun (ak, v, _) (targs, i) + -> ((ak, Var (v, i)) :: targs, + i - 1)) + formal + ([], List.length formal + List.length args - 1) in + Call (push_susp idt (S.shift (List.length formal + + List.length args)), + targs) in + let cons_type + = List.fold_left (fun ltp (kind, v, tp) + -> Arrow (kind, v, tp, loc, ltp)) + target + (List.rev args) in + + (* Add Aerasable arguments. *) + let cons_type = List.fold_left + (fun ltp (kind, v, tp) + -> Arrow (Aerasable, Some v, tp, loc, ltp)) + cons_type (List.rev formal) in + + Cons(idt, sym), cons_type + + | Pmetavar _ + -> let t = mkMetatype () in + let e = mkMetavar t in + (e, t) + + | Phastype (_, pxp, ptp) + -> let ltp = lexp_type_infer ptp ctx None trace in + (_lexp_p_check pxp ltp ctx trace), ltp + + | (Plambda _ | Pcase _) + -> let t = mkMetatype () in + let lxp = _lexp_p_check p t ctx trace in + (lxp, t) + + | _ -> pexp_fatal tloc p "Unhandled Pexp" + +and lexp_type_infer pexp ectx var trace = + let t, s = _lexp_p_infer pexp ectx trace in + elab_check_sort ectx s var t; + t + +and lexp_let_decls declss (body: lexp) ctx i = + List.fold_right (fun decls lxp -> Let (dloc, decls, lxp)) + declss body and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = @@ -395,7 +416,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = | None -> mkMetatype () | Some paty -> let laty, lasort = lexp_infer paty ctx in - elab_check_sort ctx lasort var laty; + elab_check_sort ctx lasort (Some var) laty; laty in let arrow = Arrow (kind, None, arg, Util.dummy_location, body) in match Unif.unify arrow lxp subst with @@ -857,7 +878,7 @@ and lexp_decls_1 pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else (elab_check_sort nctx lsort v ltp; + else (elab_check_sort nctx lsort (Some v) ltp; lexp_decls_1 pdecls ectx (env_extend nctx v ForwardRef ltp) (SMap.add vname (l, ltp) pending_decls) ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -113,6 +113,11 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 +(* Extend a substitution S with a (mutually recursive) set + * of definitions DEFS. *) +let lexp_defs_subst l s defs = + List.fold_left (fun s (_, lexp, _) -> S.cons (Let (l, defs, lexp)) s) + s defs (* Reduce to weak head normal form. * WHNF implies: @@ -141,7 +146,6 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = prerr_endline ("[StackTrace] ------------------------------------------"); ()); match e with - (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! @@ -185,10 +189,20 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | _ -> Case (l, e', rt, branches, default)) + | _ -> Case (l, e, rt, branches, default)) | Metavar (idx, s, _, _) -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx with Not_found -> e) + + (* FIXME: + * - This should be correct, but requires improvements in conv_p + * to avoid inf-looping! + * - I'd really prefer to use "native" recursive substitutions, using + * ideally a trick similar to the db_offsets in lexp_context! + * + * | Let (l, defs, body) + * -> push_susp body (lexp_defs_subst l S.identity defs) *) + | e -> e in lexp_whnf e ctx ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -82,6 +82,15 @@ let _ = test_eval_eqv_named "let a = 10; x = 50; y = 60; b = 20; in a + b;" (* == *) "30" +let _ = test_eval_eqv_named + "Let2" + + "c = 3; e = 1; f = 2; d = 4;" + + "let TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + x = let a = 1; b = 2 in I + in (case x | I => c) : Int;" (* == *) "3" + (* Lambda * ------------------------ *) View it on GitLab: https://gitlab.com/monnier/typer/compare/a707155bbc7c5eeb6bdd6e70adcd07f2de…

1 0

[Git][monnier/typer][master] * src/opslexp.ml (lexp_defs_subst): Fix definition
by Stefan 29 Oct '16

29 Oct '16

Stefan pushed to branch master at Stefan / Typer Commits: cf261607 by Stefan Monnier at 2016-10-29T20:18:55-04:00 * src/opslexp.ml (lexp_defs_subst): Fix definition * src/lparse.ml (elab_check_sort): Improve error message. (elab_check_def): Use better location in error message. (build_var): Remove. (_lexp_p_infer): Improve error message. - - - - - 3 changed files: - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -93,13 +93,14 @@ let value_fatal = debug_message fatal value_name value_string let elab_check_sort (ctx : elab_context) lsort var ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) - | _ -> match var with + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + match var with | None -> lexp_error (lexp_location ltp) ltp - ("`" ^ lexp_string ltp ^ "` is not a proper type") + ("`" ^ typestr ^ "` is not a proper type") | Some (l, name) -> lexp_error l ltp ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ^ typestr) let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp @@ -118,7 +119,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let ltype' = try OL.check lctx lxp with e -> - lexp_error dloc lxp "Error while type-checking"; + lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is @@ -191,10 +192,6 @@ let ctx_define_rec (ctx: elab_context) decls = *) -let build_var name ctx = - let type0_idx = senv_lookup name ctx in - Var((dloc, name), type0_idx) - let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let trace = ((OL.Pexp p)::trace) in @@ -303,7 +300,9 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = ("Constructor \"" ^ cname ^ "\" does not exist"); [], []) - | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in + | lxp -> lexp_error loc lxp ("`" ^ lexp_string idt + ^ "` is not an inductive type"); + [], [] in (* Build Arrow type. *) let target = if formal = [] then ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -114,10 +114,25 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 (* Extend a substitution S with a (mutually recursive) set - * of definitions DEFS. *) -let lexp_defs_subst l s defs = - List.fold_left (fun s (_, lexp, _) -> S.cons (Let (l, defs, lexp)) s) - s defs + * of definitions DEFS. + * This is rather tricky. E.g. for + * + * (x₁ = e1; x₂ = e₂) + * + * Where x₁ will be DeBuijn #1 and x₂ will be DeBruijn #0, + * we want a substitution of the form + * + * (let x₂ = e₂ in e₂) · (let x₁ = e₁; x₂ = e₂ in e₁) · Id + * + * Because we want #2 in both e₂ and e₁ to refer to the nearest variable in + * the surrouding context, but the substitution for #0 (defined here as + * `let x₂ = e₂ in e₂`) will be interpreted in the remaining context, + * which already provides "x₁". + *) +let rec lexp_defs_subst l s defs = match defs with + | [] -> s + | (_, lexp, _) :: defs' + -> lexp_defs_subst l (S.cons (Let (l, defs, lexp)) s) defs' (* Reduce to weak head normal form. * WHNF implies: ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -91,6 +91,16 @@ let _ = test_eval_eqv_named x = let a = 1; b = 2 in I in (case x | I => c) : Int;" (* == *) "3" +let _ = test_eval_eqv_named + "Let3" + + "c = 3; e = 1; f = 2; d = 4;" + + "let TrueProp : Type; I : TrueProp; + TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + x = let a = 1; b = 2 in I + in (case x | I => c) : Int;" (* == *) "3" + (* Lambda * ------------------------ *) View it on GitLab: https://gitlab.com/monnier/typer/commit/cf261607d2c1e944834860f23b85eb83b74…

1 0

[Git][monnier/typer][master] * src/lparse.ml (_lexp_p_infer): Fix return type of `Let`
by Stefan 28 Oct '16

28 Oct '16

Stefan pushed to branch master at Stefan / Typer Commits: 31c63489 by Stefan Monnier at 2016-10-28T23:55:25-04:00 * src/lparse.ml (_lexp_p_infer): Fix return type of `Let` * src/opslexp.ml (lexp_defs_subst): New function. (lexp_whnf): Return original exp in `Case`. Complete commented out `Let` case. * tests/eval_test.ml ("Let2"): New test. - - - - - 3 changed files: - src/lparse.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -233,11 +233,12 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (make_var name (-1) loc), dltype)) (* Let, Variable declaration + local scope. *) - | Plet(loc, decls, body) - -> let decls, nctx = _lexp_decls decls ctx trace in + | Plet (loc, decls, body) + -> let declss, nctx = _lexp_decls decls ctx trace in let bdy, ltp = lexp_infer body nctx in - (* FIXME: Bring `ltp` back from `nctx` scope to `ctx` scope! *) - (lexp_let_decls decls bdy nctx trace), ltp + let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in + (lexp_let_decls declss bdy nctx trace), + mkSusp ltp s (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) @@ -334,7 +335,6 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = | Phastype (_, pxp, ptp) -> let ltp = lexp_type_infer ptp ctx None trace in - (* FIXME: Check proper type! *) (_lexp_p_check pxp ltp ctx trace), ltp | _ -> pexp_fatal tloc p "Unhandled Pexp" ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -113,6 +113,11 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool = and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 +(* Extend a substitution S with a (mutually recursive) set + * of definitions DEFS. *) +let lexp_defs_subst l s defs = + List.fold_left (fun s (_, lexp, _) -> S.cons (Let (l, defs, lexp)) s) + s defs (* Reduce to weak head normal form. * WHNF implies: @@ -131,7 +136,6 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) let rec lexp_whnf e (ctx : DB.lexp_context) = match e with - (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! @@ -175,7 +179,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | _ -> Case (l, e', rt, branches, default)) + | _ -> Case (l, e, rt, branches, default)) + + (* FIXME: + * - This should be correct, but requires improvements in conv_p + * to avoid inf-looping! + * - I'd really prefer to use "native" recursive substitutions, using + * ideally a trick similar to the db_offsets in lexp_context! + * + * | Let (l, defs, body) + * -> push_susp body (lexp_defs_subst l S.identity defs) *) + | e -> e ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -82,6 +82,15 @@ let _ = test_eval_eqv_named "let a = 10; x = 50; y = 60; b = 20; in a + b;" (* == *) "30" +let _ = test_eval_eqv_named + "Let2" + + "c = 3; e = 1; f = 2; d = 4;" + + "let TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + x = let a = 1; b = 2 in I + in (case x | I => c) : Int;" (* == *) "3" + (* Lambda * ------------------------ *) View it on GitLab: https://gitlab.com/monnier/typer/commit/31c63489f6a36c6f2a144cc9e7d1a0a0235…

1 0

[Git][monnier/typer][master] * src/lparse.ml (_lexp_p_infer): Mostly cosmetic changes
by Stefan 28 Oct '16

28 Oct '16

Stefan pushed to branch master at Stefan / Typer Commits: 815b8bce by Stefan Monnier at 2016-10-28T22:06:51-04:00 * src/lparse.ml (_lexp_p_infer): Mostly cosmetic changes * src/lparse.ml (elab_check_sort, elab_check_proper_type): Make `var` into `option` type. (lexp_type_infer): New function. (_lexp_p_infer): Re-layout and indent. Don't use OL.check to detect user errors. Check that Phastype's annotation is a proper type. (lexp_let_decls): Use fold_right. * GNUmakefile (BUILDDIR): New var. Use everywhere. - - - - - 2 changed files: - GNUmakefile - src/lparse.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -1,10 +1,12 @@ RM=rm -f +BUILDDIR := _build + SRC_FILES := $(wildcard ./src/*.ml) -CPL_FILES := $(wildcard ./_build/src/*.cmo) +CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -lflags -g -cflags -g -build-dir _build +OBFLAGS = -lflags -g -cflags -g -build-dir $(BUILDDIR) # COMPILE_MODE = native all: typer debug tests-build @@ -23,7 +25,7 @@ debug: # Build debug utils # ============================ ocamlbuild src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/debug_util.$(COMPILE_MODE) _build/debug_util + @mv $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util # interactive typer typer: @@ -31,22 +33,25 @@ typer: # Build typer # ============================ ocamlbuild src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/REPL.$(COMPILE_MODE) _build/typer + @mv $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer tests-build: # ============================ # Build tests # ============================ - @$(foreach test, $(TEST_FILES), ocamlbuild $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) -I src $(OBFLAGS);) + @$(foreach test, $(TEST_FILES), \ + ocamlbuild $(subst ./,,$(subst .ml,.$(COMPILE_MODE) ,$(test))) \ + -I src $(OBFLAGS);) @ocamlbuild tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/tests/utest_main.$(COMPILE_MODE) _build/tests/utests + @mv $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ + $(BUILDDIR)/tests/utests tests-run: - @./_build/tests/utests --verbose= 3 + @./$(BUILDDIR)/tests/utests --verbose= 3 test-file: ocamlbuild src/test.$(COMPILE_MODE) -I src $(OBFLAGS) - @mv _build/src/test.$(COMPILE_MODE) _build/test + @mv $(BUILDDIR)/src/test.$(COMPILE_MODE) $(BUILDDIR)/test # There is nothing here. I use this to test if opam integration works install: tests @@ -59,28 +64,29 @@ doc-tex: # Make implementation doc doc-ocaml: - ocamldoc -html -d _build/doc $(SRC_FILES) + ocamldoc -html -d $(BUILDDIR)/doc $(SRC_FILES) -# everything is expected to be compiled in the "./_build/" folder +# everything is expected to be compiled in the "./$(BUILDDIR)/" folder clean: - -rm -rf _build + -rm -rf $(BUILDDIR) .PHONY: typer debug tests run/typecheck: - @./_build/debug_util ./samples/test__.typer -typecheck + @./$(BUILDDIR)/debug_util ./samples/test__.typer -typecheck run/debug_util: - @./_build/debug_util ./samples/test__.typer -fmt-type=on -fmt-index=off -fmt-pretty=on + @./$(BUILDDIR)/debug_util ./samples/test__.typer \ + -fmt-type=on -fmt-index=off -fmt-pretty=on run/typer: - @./_build/typer + @./$(BUILDDIR)/typer run/tests: - @./_build/tests/utests --verbose= 1 + @./$(BUILDDIR)/tests/utests --verbose= 1 run/typer-file: - @./_build/typer ./samples/test__.typer + @./$(BUILDDIR)/typer ./samples/test__.typer run/test-file: - @./_build/test + @./$(BUILDDIR)/test ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -90,19 +90,25 @@ let pexp_fatal = debug_message fatal pexp_name pexp_string let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string -let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = +let elab_check_sort (ctx : elab_context) lsort var ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) - -let elab_check_proper_type (ctx : elab_context) ltp v = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp + | _ -> match var with + | None -> lexp_error (lexp_location ltp) ltp + ("`" ^ lexp_string ltp ^ "` is not a proper type") + | Some (l, name) + -> lexp_error l ltp + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp) + +let elab_check_proper_type (ctx : elab_context) ltp var = + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; - print_string ("` of var `" - ^ (let (_, name) = v in name) ^"`\n"); + (match var with + | None -> () + | Some (_, name) + -> print_string ("` of var `" ^ name ^"`\n")); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -118,7 +124,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = (* FIXME: conv_p fails too often, e.g. it fails to see that `Type` is * convertible to `Type_0`, because it doesn't have access to lctx. *) if true (* OL.conv_p ltype ltype' *) then - elab_check_proper_type ctx ltype var + elab_check_proper_type ctx ltype (Some var) else (debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ (lexp_string lxp) ^ "!: " ^ (lexp_string ltype); @@ -126,7 +132,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = - elab_check_proper_type ctx ltype (maybev var); + elab_check_proper_type ctx ltype var; ectx_extend ctx var def ltype let ctx_define (ctx: elab_context) var lxp ltype = @@ -137,7 +143,7 @@ let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) var; + nctx (push_susp ltp (S.shift n)) (Some var); n - 1) (List.length decls) decls in @@ -195,152 +201,152 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let tloc = pexp_location p in let lexp_infer p ctx = _lexp_p_infer p ctx trace in - (* Save current trace in a global variable. If an error occur, - we will be able to retrieve the most recent trace and context *) + (* 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; _global_lexp_trace := trace; match p with - (* Block/String/Integer/Float *) - | Pimm v -> (Imm(v), - match v with - | Integer _ -> type_int - | Float _ -> type_float - | String _ -> type_string; - | _ -> pexp_error tloc p "Could not find type"; - dltype) - - (* Symbol i.e identifier *) - | Pvar (loc, name) ->( - 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 (* Return Macro[22] *) - - with Not_found -> - (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); - (* Error recovery. The -1 index will raise an error later on *) - (make_var name (-1) loc), dltype)) - - (* Let, Variable declaration + local scope *) - | Plet(loc, decls, body) -> - let decls, nctx = _lexp_decls decls ctx trace in - let bdy, ltp = lexp_infer body nctx in - (lexp_let_decls decls bdy nctx trace), ltp - - (* ------------------------------------------------------------------ *) - | Parrow (kind, ovar, tp, loc, expr) -> - let ltp, _ = lexp_infer tp ctx in - let _ = elab_check_proper_type ctx ltp (maybev ovar) in - let nctx = ectx_extend ctx ovar Variable ltp in - - let lxp, _ = lexp_infer expr nctx in - let _ = elab_check_proper_type nctx lxp (maybev ovar) in - - let v = Arrow(kind, ovar, ltp, tloc, lxp) in - v, type0 - - (* Pinductive *) - | Pinductive (label, formal_args, ctors) -> - let nctx = ref ctx in - (* (arg_kind * pvar * pexp option) list *) - let formal = List.map (fun (kind, var, opxp) -> - let ltp, _ = match opxp with - | Some pxp -> _lexp_p_infer pxp !nctx trace - | None -> dltype, dltype in - - nctx := env_extend !nctx var Variable ltp; - (kind, var, ltp) - ) formal_args in - - let nctx = !nctx in - let ltp = List.fold_left (fun tp (kind, v, ltp) - -> (Arrow (kind, Some v, ltp, tloc, tp))) - (* FIXME: See OL.check for how to - * compute the real target sort - * (not always type0). *) - type0 (List.rev formal) in - - let map_ctor = lexp_parse_inductive ctors nctx trace in - let v = Inductive(tloc, label, formal, map_ctor) in - v, ltp - - (* This case can be inferred *) - | Plambda (kind, var, optype, body) -> - let ltp, _ = match optype with - | Some ptype -> lexp_infer ptype ctx - (* This case must have been lexp_p_check *) - | None -> pexp_error tloc p "Lambda require type annotation"; - dltype, dltype in - - let nctx = env_extend ctx var Variable ltp in - let lbody, lbtp = lexp_infer body nctx in - - let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in - Lambda(kind, var, ltp, lbody), lambda_type - - | Pcall (fname, _args) -> - lexp_call fname _args ctx trace - - (* Pcons *) - | Pcons(t, sym) -> - let idt, _ = lexp_infer t ctx in - let (loc, cname) = sym in - - (* Get constructor args *) - let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with - | Inductive(_, _, formal, ctor_def) as lxp -> ( - try formal, (SMap.find cname ctor_def) - with Not_found -> - lexp_error loc lxp - ("Constructor \"" ^ cname ^ "\" does not exist"); - [], []) - - | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in - - (* Build Arrow type. *) - let target = if formal = [] then - push_susp idt (S.shift (List.length args)) - else - let targs, _ = - List.fold_right - (fun (ak, v, _) (targs, i) - -> ((ak, Var (v, i)) :: targs, - i - 1)) - formal - ([], List.length formal + List.length args - 1) in - Call (push_susp idt (S.shift (List.length formal - + List.length args)), - targs) in - let cons_type - = List.fold_left (fun ltp (kind, v, tp) - -> Arrow (kind, v, tp, loc, ltp)) - target - (List.rev args) in - - (* Add Aerasable arguments. *) - let cons_type = List.fold_left - (fun ltp (kind, v, tp) - -> Arrow (Aerasable, Some v, tp, loc, ltp)) - cons_type (List.rev formal) in - - Cons(idt, sym), cons_type - - | Phastype (_, pxp, ptp) - -> let ltp, _ = lexp_infer ptp ctx in - (_lexp_p_check pxp ltp ctx trace), ltp - - | _ -> pexp_fatal tloc p "Unhandled Pexp" - - -and lexp_let_decls decls (body: lexp) ctx i = - (* build the weird looking let *) - let decls = List.rev decls in - List.fold_left (fun lxp decls -> - Let(dloc, decls, lxp)) body decls + (* Block/String/Integer/Float. *) + | Pimm v + -> (Imm(v), + match v with + | Integer _ -> type_int + | Float _ -> type_float + | String _ -> type_string; + | _ -> pexp_error tloc p "Could not find type"; + dltype) + + (* Symbol i.e identifier. *) + | Pvar (loc, name) + -> (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 (* Return Macro[22] *) + + with Not_found -> + (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (* Error recovery. The -1 index will raise an error later on *) + (make_var name (-1) loc), dltype)) + + (* Let, Variable declaration + local scope. *) + | Plet(loc, decls, body) + -> let decls, nctx = _lexp_decls decls ctx trace in + let bdy, ltp = lexp_infer body nctx in + (* FIXME: Bring `ltp` back from `nctx` scope to `ctx` scope! *) + (lexp_let_decls decls bdy nctx trace), ltp + + (* ------------------------------------------------------------------ *) + | Parrow (kind, ovar, tp, loc, expr) + -> let ltp = lexp_type_infer tp ctx ovar trace in + let nctx = ectx_extend ctx ovar Variable ltp in + + let lxp = lexp_type_infer expr nctx None trace in + + let v = Arrow(kind, ovar, ltp, tloc, lxp) in + v, type0 + + | Pinductive (label, formal_args, ctors) + -> let nctx = ref ctx in + (* (arg_kind * pvar * pexp option) list *) + let formal = List.map (fun (kind, var, opxp) + -> let ltp, _ = match opxp with + | Some pxp -> _lexp_p_infer pxp !nctx trace + | None -> dltype, dltype in + + nctx := env_extend !nctx var Variable ltp; + (kind, var, ltp)) + formal_args in + + let nctx = !nctx in + let ltp = List.fold_left (fun tp (kind, v, ltp) + -> (Arrow (kind, Some v, ltp, tloc, tp))) + (* FIXME: See OL.check for how to + * compute the real target sort + * (not always type0). *) + type0 (List.rev formal) in + + let map_ctor = lexp_parse_inductive ctors nctx trace in + let v = Inductive(tloc, label, formal, map_ctor) in + v, ltp + + (* This case can be inferred *) + | Plambda (kind, var, optype, body) + -> let ltp, _ = match optype with + | Some ptype -> lexp_infer ptype ctx + (* This case must have been lexp_p_check *) + | None -> pexp_error tloc p "Lambda require type annotation"; + dltype, dltype in + + let nctx = env_extend ctx var Variable ltp in + let lbody, lbtp = lexp_infer body nctx in + + let lambda_type = Arrow(kind, None, ltp, tloc, lbtp) in + Lambda(kind, var, ltp, lbody), lambda_type + + | Pcall (fname, _args) -> lexp_call fname _args ctx trace + + | Pcons(t, sym) + -> let idt, _ = lexp_infer t ctx in + let (loc, cname) = sym in + + (* Get constructor args. *) + let formal, args = match OL.lexp_whnf idt (ectx_to_lctx ctx) with + | Inductive(_, _, formal, ctor_def) as lxp + -> (try formal, (SMap.find cname ctor_def) + with Not_found -> + lexp_error loc lxp + ("Constructor \"" ^ cname ^ "\" does not exist"); + [], []) + + | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in + + (* Build Arrow type. *) + let target = if formal = [] then + push_susp idt (S.shift (List.length args)) + else + let targs, _ + = List.fold_right + (fun (ak, v, _) (targs, i) + -> ((ak, Var (v, i)) :: targs, + i - 1)) + formal + ([], List.length formal + List.length args - 1) in + Call (push_susp idt (S.shift (List.length formal + + List.length args)), + targs) in + let cons_type + = List.fold_left (fun ltp (kind, v, tp) + -> Arrow (kind, v, tp, loc, ltp)) + target + (List.rev args) in + + (* Add Aerasable arguments. *) + let cons_type = List.fold_left + (fun ltp (kind, v, tp) + -> Arrow (Aerasable, Some v, tp, loc, ltp)) + cons_type (List.rev formal) in + + Cons(idt, sym), cons_type + + | Phastype (_, pxp, ptp) + -> let ltp = lexp_type_infer ptp ctx None trace in + (* FIXME: Check proper type! *) + (_lexp_p_check pxp ltp ctx trace), ltp + + | _ -> pexp_fatal tloc p "Unhandled Pexp" + +and lexp_type_infer pexp ectx var trace = + let t, s = _lexp_p_infer pexp ectx trace in + elab_check_sort ectx s var t; + t + +and lexp_let_decls declss (body: lexp) ctx i = + List.fold_right (fun decls lxp -> Let (dloc, decls, lxp)) + declss body and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = @@ -366,7 +372,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = let _ = match aty with | Some paty -> let laty, lasort = _lexp_p_infer paty ctx trace in - elab_check_sort ctx lasort var laty; + elab_check_sort ctx lasort (Some var) laty; () (* FIXME: Check `conv_p aty ltp`! *) | _ -> () in @@ -749,7 +755,7 @@ and lexp_decls_1 pending_defs then (error l ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 pdecls ectx nctx pending_decls pending_defs) - else (elab_check_sort nctx lsort v ltp; + else (elab_check_sort nctx lsort (Some v) ltp; lexp_decls_1 pdecls ectx (env_extend nctx v ForwardRef ltp) (SMap.add vname (l, ltp) pending_decls) View it on GitLab: https://gitlab.com/monnier/typer/commit/815b8bce72d931b9c41e82c360a4f09475b…

1 0

[Git][monnier/typer][unification] Infer implicit args; Give type to metavars
by Stefan 28 Oct '16

28 Oct '16

Stefan pushed to branch unification at Stefan / Typer Commits: a707155b by Stefan Monnier at 2016-10-28T14:55:10-04:00 Infer implicit args; Give type to metavars * src/lexp.ml (lexp): Add type to `Metavar`. (lexp_unparse): (somewhat) Handle Metavar and Sort. * src/lparse.ml (global_substitution): Move, so elab_check_sort can use it. (mkMetavar): Add type arg. (mkMetalevel, mkMetatype): New functions. (elab_check_sort._lexp_p_infer): Use them. (_lexp_p_check.unify_with_arrow): Use the explicit arg type if present. (elab_check_sort.lexp_call.handle_fun_args): Infer missing implicit arg. * src/opslexp.ml (lexp_whnf): Rewrite to reduce diff w.r.t `trunk`. (check): Add case of `Metavar`. * src/unification.ml (mkMetavar): Remove. * tests/eval_test.ml ("Lists"): Remove explicit-implicit args. * tests/unify_test.ml: Remove unsupported `case` on integers. * tests/utest_lib.ml (for_all_tests): Remove try/with which hides the better backtrace one gets with OCAMLRUNPARAM=b. - - - - - 7 changed files: - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml - tests/eval_test.ml - tests/unify_test.ml - tests/utest_lib.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -76,7 +76,9 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * (vdef option * lexp) option (* Default. *) - | Metavar of int * subst * vdef + (* The substitution `s` only applies to the lexp associated + * with the metavar's index (i.e. its "value"), not to the ltype. *) + | Metavar of int * subst * vdef * ltype (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -136,7 +138,7 @@ let rec mkSusp e s = match e with | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v - | Metavar (vn, s', vd) -> Metavar (vn, scompose s' s, vd) + | Metavar (vn, s', vd, t) -> Metavar (vn, scompose s' s, vd, mkSusp t s) | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -289,7 +291,7 @@ let rec lexp_location e = | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> l + | Metavar (_,_,(l,_), _) -> l (********* Normalizing a term *********) @@ -585,11 +587,19 @@ let rec lexp_unparse lxp = | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch) - (* - | SortLevel of sort_level - | Sort of U.location * sort *) + (* | _ as e -> Pimm (Symbol(lexp_location e, "<")) *) + + (* FIXME: The cases below are all broken! *) + | Metavar (idx, subst, (loc, name), _) + -> Pimm (Symbol (loc, "?<" ^ name ^ "-" ^ string_of_int idx ^ ">")) - | _ as e -> Pimm (Symbol(lexp_location e, "Type")) + | SortLevel (SLz) -> Pimm (Integer (U.dummy_location, 0)) + | SortLevel (SLsucc sl) -> Pcall (Pimm (Symbol (U.dummy_location, "<S>")), + [pexp_unparse (lexp_unparse sl)]) + | Sort (l, StypeOmega) -> Pimm (Symbol (l, "<SortOmega>")) + | Sort (l, StypeLevel) -> Pimm (Symbol (l, "<SortLevel>")) + | Sort (l, Stype sl) -> Pcall (Pimm (Symbol (l, "<Type>")), + [pexp_unparse (lexp_unparse sl)]) let rec subst_string s = match s with | S.Identity -> "Id" @@ -701,7 +711,8 @@ and _lexp_to_str ctx exp = | Var ((loc, name), idx) -> name ^ (index idx) ; - | Metavar (idx, subst, (loc, name)) -> "?" ^ name ^ (index idx) (*TODO : print subst*) + | Metavar (idx, subst, (loc, name), _) + -> "?" ^ name ^ (index idx) (*TODO : print subst*) | Let (_, decls, body) -> (* Print first decls without indent *) ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -92,12 +92,16 @@ let pexp_fatal = debug_message fatal pexp_name pexp_string let pexp_error = debug_message error pexp_name pexp_string let value_fatal = debug_message fatal value_name value_string +(* :-( *) +let global_substitution = ref (empty_subst, []) + let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = - match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx with | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ltp + | k -> lexp_error l ltp ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ^ lexp_string ltp ^ " : " ^ lexp_string lsort); let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp @@ -191,17 +195,18 @@ let build_var name ctx = let type0_idx = senv_lookup name ctx in Var((dloc, name), type0_idx) -(* FIXME: We need to keep track of the type of metavars. We could keep it - * in the `Metavar` constructor of the `lexp` type, but that's risky (it could - * be difficult to make sure it's the same for all occurrences of that - * metavar). *) +let mkMetavar t = + let meta = Unif.create_metavar () in + let name = "__metavar" (* ^ (string_of_int meta) *) in + Metavar (meta, S.Identity, (Util.dummy_location, name), t) -(* :-( *) -let global_substitution = ref (empty_subst, []) +let mkMetalevel () = + let meta = Unif.create_metavar () in + let name = "__metalevel" (* ^ (string_of_int meta) *) in + Metavar (meta, S.Identity, (Util.dummy_location, name), + Sort (dummy_location, StypeLevel)) -let mkMetavar () = let meta = Unif.create_metavar () - in let name = "__Metavar_" ^ (string_of_int meta) - in Metavar (meta, S.Identity, (Util.dummy_location, name)) +let mkMetatype () = mkMetavar (mkMetalevel ()) let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Debug_fun.do_debug (fun () -> @@ -342,19 +347,18 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Cons(idt, sym), cons_type | Pmetavar _ - -> let meta = mkMetavar () in (*TODO *) - let type_ = mkMetavar () in - lexp_warning dloc meta "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned"; - (meta, type_) (* FIXME return the right type *) + -> let t = mkMetatype () in + let e = mkMetavar t in + (e, t) | Phastype (_, pxp, ptp) -> let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx trace), ltp | (Plambda _ | Pcase _) - -> let meta = mkMetavar () in - let lxp = _lexp_p_check p meta ctx trace in - (lxp, meta) + -> let t = mkMetatype () in + let lxp = _lexp_p_check p t ctx trace in + (lxp, t) and lexp_let_decls decls (body: lexp) ctx i = @@ -385,11 +389,17 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = _global_lexp_ctx := ctx; _global_lexp_trace := trace; - let unify_with_arrow lxp kind subst = - let arg, body = mkMetavar (), mkMetavar () - in let arrow = Arrow (kind, None, arg, Util.dummy_location, body) - in match Unif.unify arrow lxp subst with - | Some(subst) -> global_substitution := subst; arg, body + let unify_with_arrow lxp kind var aty subst = + let body = mkMetatype () in + let arg = match aty with + | None -> mkMetatype () + | Some paty + -> let laty, lasort = lexp_infer paty ctx in + elab_check_sort ctx lasort var laty; + laty in + let arrow = Arrow (kind, None, arg, Util.dummy_location, body) in + match Unif.unify arrow lxp subst with + | Some subst -> global_substitution := subst; arg, body | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp ^ " and " ^ lexp_string arrow @@ -401,15 +411,10 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* Read var type from the provided type *) let meta_ctx, _ = !global_substitution in let ltp, lbtp = match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | lxp -> unify_with_arrow lxp kind subst in - - let _ = match aty with - | Some paty - -> let laty, lasort = lexp_infer paty ctx in - elab_check_sort ctx lasort var laty; - () (* FIXME: Check `conv_p aty ltp`! *) - | _ -> () in + | Arrow(kind, _, ltp, _, lbtp) + (* FIXME: Check `conv_p aty ltp`! *) + -> ltp, lbtp + | lxp -> unify_with_arrow lxp kind var aty subst in let nctx = env_extend ctx var Variable ltp in let lbody = lexp_check body lbtp nctx in @@ -629,10 +634,10 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((Aexplicit, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | Arrow _ as t -> - debug_messages fatal (sexp_location sarg) "Expected non-explicit arg" [ - "ltype : " ^ (lexp_string t); - "s-exp arg: " ^ (sexp_string sarg);] + | Arrow (kind, _, arg_type, _, ret_type) + -> let larg = mkMetavar arg_type in + handle_fun_args ((kind, larg) :: largs) (sarg::sargs) + (L.mkSusp ret_type (S.substitute larg)) | t -> print_lexp_ctx (ectx_to_lctx ctx); ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -130,7 +130,8 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) -let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = +let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = + let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); @@ -146,38 +147,37 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf e' ctx meta_ctx) - | Susp (e, s) -> lexp_whnf (push_susp e s) ctx meta_ctx - | Call (e, []) -> lexp_whnf e ctx meta_ctx + | Some e' -> lexp_whnf e' ctx) + | Susp (e, s) -> lexp_whnf (push_susp e s) ctx + | Call (e, []) -> lexp_whnf e ctx | Call (e, (((_, arg)::args) as xs)) -> - (match lexp_whnf e ctx meta_ctx with + (match lexp_whnf e ctx with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx meta_ctx)), + lexp_whnf (Call (push_susp body (S.substitute (lexp_whnf arg ctx)), args)) - ctx meta_ctx + ctx | Call (e', xs1) -> Call (e', List.append xs1 xs) | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf e ctx meta_ctx in + let e' = lexp_whnf e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.Cons (L.mkSusp (lexp_whnf arg ctx meta_ctx) (S.shift d), s), + (S.Cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d), s), d + 1)) (S.identity, 0) aargs in - lexp_whnf (push_susp branch subst) ctx meta_ctx + lexp_whnf (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) - ctx meta_ctx + -> lexp_whnf (push_susp default (S.substitute e')) ctx | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); @@ -186,9 +186,13 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> Case (l, e', rt, branches, default)) - | Metavar (idx, _, _) -> lexp_whnf (L.VMap.find idx meta_ctx) ctx meta_ctx + | Metavar (idx, s, _, _) + -> (try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + with Not_found -> e) | e -> e + in lexp_whnf e ctx + (********* Testing if a lexp is properly typed *********) @@ -408,6 +412,9 @@ let rec check ctx e = | _ -> (U.msg_error "TC" (lexp_location e) "Cons of a non-inductive type!"; B.type_int)) + | Metavar (idx, s, _, t) + -> try check ctx (push_susp (L.VMap.find idx meta_ctx) s) + with Not_found -> t (*********** Type erasure, before evaluation. *****************) ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -9,8 +9,8 @@ open Inverse_subst (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) -let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar -let mkMetavar subst vdef = Metavar (create_metavar (), subst, vdef) +let create_metavar () = global_last_metavar := !global_last_metavar + 1; + !global_last_metavar (* For convenience *) type return_type = (substitution * constraints) option @@ -25,9 +25,10 @@ let associate (meta: int) (lxp: lexp) (subst: substitution) *) let find_or_none (value: lexp) (map: substitution) : lexp option = match value with - | Metavar (idx, _, _) -> (if VMap.mem idx map - then Some (VMap.find idx map) - else None) + | Metavar (idx, _, _, _) + -> if VMap.mem idx map + then Some (VMap.find idx map) + else None | _ -> None (** Zip while applying a function, returns <code>None</code> list if l1 & l2 have different size*) @@ -215,15 +216,15 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type match find_or_none metavar s with | Some (lxp_) -> unify lxp_ lxp s | None -> (match metavar with - | Metavar (_, subst_, _) -> (match inverse subst_ with + | Metavar (_, subst_, _, _) -> (match inverse subst_ with | Some s' -> Some (associate value (mkSusp lxp s') s, []) | None -> None) | _ -> None) in match (meta, lxp) with - | (Metavar (val1, s1, _), Metavar (val2, s2, _)) when val1 = val2 -> + | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 -> Some ((subst, [])) - | (Metavar (v, s1, _), _) -> find_or_unify meta v lxp subst + | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst | (_, _) -> None (** Unify a Call (call) and a lexp (lxp) ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -226,14 +226,16 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lists" - "my_list = cons (a := Int) 1 - (cons (a := Int) 2 - (cons (a := Int) 3 - (cons (a := Int) 4 (nil (a := Int)))))" - - "length (a := Int) my_list; - head (a := Int) my_list; - head (a := Int) (tail (a := Int) my_list)" + (* FIXME: This doesn't signal an error, even we don't yet have the code + * to handle the `nil` below! *) + "my_list = cons 1 + (cons 2 + (cons 3 + (cons 4 nil)))" + + "length my_list; + head my_list; + head (tail my_list)" "4; 1; 2" ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -61,13 +61,12 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" -let str_case = "i = case 0 -| 1 => 2 -| 0 => 42 -| _ => 5" -let str_case2 = "i = case 0 -| 0 => 12 -| _ => 12" +let str_case = "i = case True +| True => 2 +| False => 42" +let str_case2 = "i = case nil(a := Int) +| nil => 12 +| _ => 24" let str_let = "i = let a = 5 in a + 1" let str_let2 = "j = let b = 5 in b" let str_lambda = "sqr = lambda (x : Int) -> x * x;" @@ -166,7 +165,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_type , input_type_t , Equivalent) (* 44 *) - ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) + ::(Metavar (0, S.Identity, (Util.dummy_location, "M"), type0), + Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *) ::[] @@ -179,7 +179,7 @@ let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = | None -> (Nothing, res, lxp1, lxp2) in tmp -let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = +let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: substitution): bool = let r, _, _, _ = test_input lxp1 lxp2 subst in if r = res then true else false ===================================== tests/utest_lib.ml ===================================== --- a/tests/utest_lib.ml +++ b/tests/utest_lib.ml @@ -182,16 +182,16 @@ let for_all_tests sk tmap tk = if (must_run_title tk) then ( let tv = StringMap.find tk tmap in flush stdout; - try + (* try *) let r = tv () in if r = 0 then( ut_string2 (green ^ "[ OK] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset)) else( ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset); _ret_code := failure ()) - with e -> - _ret_code := failure (); - unexpected_throw sk tk e) else () + (* with e -> + * _ret_code := failure (); + * unexpected_throw sk tk e *)) else () let for_all_sections sk = let tmap, tst = StringMap.find sk (!_global_sections) in View it on GitLab: https://gitlab.com/monnier/typer/commit/a707155bbc7c5eeb6bdd6e70adcd07f2ded…

1 0

[Git][monnier/typer][unification] Fix some of the tests
by Stefan 27 Oct '16

27 Oct '16

Stefan pushed to branch unification at Stefan / Typer Commits: 89c67665 by Stefan Monnier at 2016-10-27T21:03:13-04:00 Fix some of the tests - - - - - 3 changed files: - src/lparse.ml - tests/lparse_test.ml - tests/unify_test.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -244,7 +244,8 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = lxp, ltp (* Return Macro[22] *) with Not_found -> - (pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); + (print_lexp_ctx (ectx_to_lctx ctx); + pexp_error loc p ("The variable: `" ^ name ^ "` was not declared"); (* Error recovery. The -1 index will raise an error later on *) (make_var name (-1) loc), dltype)) ===================================== tests/lparse_test.ml ===================================== --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -30,7 +30,7 @@ let generate_tests (name: string) (test input_gen fmt tester) (* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda x : α -> x; +let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; res = id 3;" let generate_lexp_from_str str = ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -58,7 +58,7 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = ) str_lst (* Inputs for the test *) -let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_induct = "Nat : Type; Nat = inductive_ (dNat) (zero) (succ Nat)" let str_int_3 = "i = 3" let str_int_4 = "i = 4" let str_case = "i = case 0 View it on GitLab: https://gitlab.com/monnier/typer/commit/89c6766524018b315a7ecc69a3adc690179…

1 0

[Git][monnier/typer][unification] 3 commits: Get rid of unused `it` field in Case; various extra type checks
by Stefan 27 Oct '16

27 Oct '16

Stefan pushed to branch unification at Stefan / Typer Commits: 18f58429 by Stefan Monnier at 2016-10-19T16:15:43-04:00 Get rid of unused `it` field in Case; various extra type checks * src/lparse.ml (_lexp_p_check): Check the lambda's type annotations are indeed types. (lexp_case): Check that the subject is indeed of inductive type. (lexp_call): Remove unused `from_lctx`. (lexp_read_pattern): Remove unused `exp` arg. * src/lexp.ml (lexp): Remove unused "base inductive type" field from `Case`. - - - - - a459a1ea by Stefan Monnier at 2016-10-20T15:28:17-04:00 Fix various typing and inference problems with `Case` * GNUmakefile (OBFLAGS): Add debug info. * src/elexp.ml (elexp): Add binding of scrutinee in the default branch. (elexp_string.maybe_str): Adjust print code accordingly. * src/eval.ml (eval_case): Bind scrutinee in the default branch. * src/lexp.ml (lexp): Add binding of scrutinee in the default branch. (push_susp, _lexp_to_str): Adjust accordingly. (lexp_unparse): Adjust to pexp changes. * src/lparse.ml (elab_check_proper_type): Use lexp_print to get db indexes. (ctx_extend): New function. (_lexp_p_infer): Check that arrow's args are types. (lexp_case): Rewrite; fix problems with scoping. (lexp_read_pattern, lexp_read_pattern_args): Remove. * src/opslexp.ml (lexp_whnf): Adjust to new `Case`. Preserve the non-whnf in the sub-parts we return. (check): Check that erasable inductive type fields have a proper type. Don't assume call_split returns whnf elements. Adjust to new `Case`. (clean_maybe): Adjust to new `Case`. * src/pexp.ml (ppat): Rename Ppatvar to Ppatsym since it can be either a var or a constructor. Drop arg_kind from Ppatcons. (pexp_p_pat_arg): Only recognize := as explicit-implicit. (pexp_u_pat_arg): Only use := for explicit-implicit. - - - - - 07f429b3 by Stefan Monnier at 2016-10-27T20:37:32-04:00 Merge branch 'trunk' into unification - - - - - 9 changed files: - DESIGN - GNUmakefile - src/elexp.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml - src/unification.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1710,9 +1710,20 @@ So we'd define numbers = numbers' 0 * Papers -** BigBang: Designing a statically typed scripting language -** Dependently typed Racket -** Dependently typed Haskell +** Macros and tactics +*** Rtac +[1] Dissertation: +https://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory/ +[2] ESOP'16: +https://gmalecha.github.io/publication/2016/01/01/extensible-and-efficient-automation-through-reflective-tactics/ +[3] ITP'14: +https://gmalecha.github.io/publication/2014/07/14/compositional-computational-reflection/ +*** ssreflect +*** Mtac +** Other +*** BigBang: Designing a statically typed scripting language +*** Dependently typed Racket +*** Dependently typed Haskell "My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/) Still working @@ -1720,36 +1731,36 @@ on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)" -** On Irrelevance and Algorithmic Equality in Predicative Type Theory, +*** On Irrelevance and Algorithmic Equality in Predicative Type Theory, Andreas Abel & Gabriel Scherer, FOSSACS 2011. -** "A few constructions on constructors" -** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani -** http://homotopytypetheory.org/book/ -** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages +*** "A few constructions on constructors" +*** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani +*** http://homotopytypetheory.org/book/ +*** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%22… -** Propositions as Sessions, Philip Wadler -** A few constructions on constructors, by Conor et al. -** Constructive selection principle (Markov's principle) +*** Propositions as Sessions, Philip Wadler +*** A few constructions on constructors, by Conor et al. +*** Constructive selection principle (Markov's principle) http://www.encyclopediaofmath.org/index.php/Constructive_selection_principle https://en.wikipedia.org/wiki/Markov%27s_principle -** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 -** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf -** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau -** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete +*** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 +*** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf +*** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau +*** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete data types. F. Blanqui, T. Hardin and P. Weis. ESOP'07. -** The Nemerle language -** "A Theory of Typed Hygienic Macros" de David Herman +*** The Nemerle language +*** "A Theory of Typed Hygienic Macros" de David Herman http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf -** http://www.mpi-sws.org/~beta/mtac/ -** Non-strictly positive and elimination +*** http://www.mpi-sws.org/~beta/mtac/ +*** Non-strictly positive and elimination "Inductively defined types", by Thierry Coquand and Christine Paulin, COLOG'88, LNCS 417 -** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. +*** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. http://arxiv.org/pdf/1112.3833v1 -** Strong Normalization for Coq (CiC). +*** Strong Normalization for Coq (CiC). http://www.cs.rice.edu/~emw4/uniform-lr.pdf -** Irrelevant/erasable args +*** Irrelevant/erasable args *** The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Bruno Barras and Bruno Bernardo, fossacs08. @@ -1779,7 +1790,7 @@ Finally we show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. -** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 +*** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 The Girard-Reynolds polymorphic λ-calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are strongly normalizing with respect to β-reductions. Girard demonstrated that @@ -1793,10 +1804,10 @@ impredicativity is essential to the argument; predicative variants of the polymorphic λ-calculus admit non-parametric operations without sacrificing normalization. -** Idris (Edwin Brady) -** http://albatross-lang.sourceforge.net -** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf -** Read +*** Idris (Edwin Brady) +*** http://albatross-lang.sourceforge.net +*** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf +*** Read *** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] *** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -4,7 +4,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -build-dir _build +OBFLAGS = -lflags -g -cflags -g -build-dir _build # COMPILE_MODE = native all: typer debug tests-build ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -52,8 +52,9 @@ type elexp = | Lambda of vdef * elexp | Call of elexp * elexp list | Cons of symbol - | Case of U.location * elexp * - (U.location * (vdef option) list * elexp) SMap.t * elexp option + | Case of U.location * elexp + * (U.location * (vdef option) list * elexp) SMap.t + * (vdef option * elexp) option (* Type place-holder just in case *) | Type (* Inductive takes a slot in the env that is why it need to be here *) @@ -90,8 +91,10 @@ let rec elexp_print lxp = print_string (elexp_string lxp) and elexp_string lxp = let maybe_str lxp = match lxp with - | Some lxp -> " | _ => " ^ (elexp_string lxp) - | None -> "" in + | Some (v, lxp) + -> " | " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ elexp_string lxp + | None -> "" in let str_decls d = List.fold_left (fun str ((_, s), lxp) -> ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -384,7 +384,9 @@ and eval_case ctx i loc target pat dflt = (* Run default *) with Not_found -> (match dflt with - | Some lxp -> _eval lxp ctx i + | Some (var, lxp) + -> let var' = match var with None -> None | Some (_, n) -> Some n in + _eval lxp (add_rte_variable var' v ctx) i | _ -> error loc "Match Failure") and build_arg_list args ctx i = ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -41,8 +41,19 @@ type label = symbol (*************** Elaboration to Lexp *********************) -(* Pour la propagation des types bidirectionnelle, tout va dans `infer`, - * sauf Lambda et Case qui vont dans `check`. Je crois. *) +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + type ltype = lexp and subst = lexp S.subst and lexp = @@ -62,10 +73,9 @@ type ltype = lexp * ((arg_kind * vdef option * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp - * ltype (* The base inductive type over which we switch. *) * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t - * lexp option (* Default. *) + * (vdef option * lexp) option (* Default. *) | Metavar of int * subst * vdef (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref @@ -276,7 +286,7 @@ let rec lexp_location e = | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l | Cons (_,(l,_)) -> l - | Case (l,_,_,_,_,_) -> l + | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l @@ -284,7 +294,7 @@ let rec lexp_location e = (********* Normalizing a term *********) -let vdummy = (U.dummy_location, "dummy") +let vdummy = (U.dummy_location, "<anon>") let maybev mv = match mv with None -> vdummy | Some v -> v let rec push_susp e s = (* Push a suspension one level down. *) @@ -321,8 +331,8 @@ let rec push_susp e s = (* Push a suspension one level down. *) cases in Inductive (l, label, nargs, ncases) | Cons (it, name) -> Cons (mkSusp it s, name) - | Case (l, e, it, ret, cases, default) - -> Case (l, mkSusp e s, mkSusp it s, mkSusp ret s, + | Case (l, e, ret, cases, default) + -> Case (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left (fun s carg -> match carg with @@ -333,7 +343,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) cases, match default with | None -> default - | Some e -> Some (mkSusp e s)) + | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -550,23 +560,28 @@ let rec lexp_unparse lxp = ) (SMap.bindings ctor) in Pinductive(label, pfargs, ctor) - | Case (loc, target, tltp, bltp, branches, default) -> + | Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with - | [] -> Ppatvar (loc, str), lexp_unparse bch + | [] -> Ppatsym (loc, str), lexp_unparse bch | _ -> - let pat_args = List.map (fun (kind, vdef) -> - match vdef with - | Some vdef -> Some (kind, vdef), Ppatvar(vdef) - | None -> None, Ppatany(loc)) args + let pat_args + = List.map (fun (kind, vdef) + -> match vdef with + | Some vdef -> Some vdef, Ppatsym vdef + | None -> None, Ppatany loc) + args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch ) (SMap.bindings branches) in let pbranch = match default with - | Some dft -> (Ppatany(loc), lexp_unparse dft)::pbranch + | Some (v,dft) -> ((match v with + | None -> Ppatany loc + | Some vdef -> Ppatsym vdef), + lexp_unparse dft)::pbranch | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch) @@ -773,7 +788,7 @@ and _lexp_to_str ctx exp = (keyword "inductive_") ^ " (" ^ name ^ args_str ^") " ^ (lexp_str_ctor ctx ctors) - | Case (_, target, tpe, _ret, map, dflt) ->( + | Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_to_str target) (* FIXME: `tpe' is the *base* type of `target`. E.g. if `target` * is a `List Int`, then `tpe` will be `List`. @@ -792,8 +807,10 @@ and _lexp_to_str ctx exp = match dflt with | None -> str - | Some df -> - str ^ nl ^ (make_indent 1) ^ "| _ => " ^ (lexp_to_stri 1 df)) + | Some (v, df) -> + str ^ nl ^ (make_indent 1) + ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ (lexp_to_stri 1 df)) | Builtin ((_, name), _) -> name ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -96,14 +96,15 @@ let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with | Sort (_, _) -> () (* All clear! *) | _ -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp) let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp - with e -> print_string ("Exception while checking type `" - ^ lexp_string ltp ^ "` of var `" ^ - (let (_, name) = v in name) ^"`\n"); + with e -> print_string "Exception while checking type `"; + lexp_print ltp; + print_string ("` of var `" + ^ (let (_, name) = v in name) ^"`\n"); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -126,6 +127,10 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) +let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = + elab_check_proper_type ctx ltype (maybev var); + ectx_extend ctx var def ltype + let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; env_extend ctx var (LetDef lxp) ltype @@ -252,9 +257,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in + let _ = elab_check_proper_type ctx ltp (maybev ovar) in let nctx = ectx_extend ctx ovar Variable ltp in let lxp, _ = lexp_infer expr nctx in + let _ = elab_check_proper_type nctx lxp (maybev ovar) in let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -305,7 +312,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in - (* build Arrow type *) + (* Build Arrow type. *) let target = if formal = [] then push_susp idt (S.shift (List.length args)) else @@ -325,7 +332,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = target (List.rev args) in - (* Add Aerasable argument *) + (* Add Aerasable arguments. *) let cons_type = List.fold_left (fun ltp (kind, v, tp) -> Arrow (Aerasable, Some v, tp, loc, ltp)) @@ -333,13 +340,14 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = Cons(idt, sym), cons_type - | Pmetavar _ -> (let meta = mkMetavar () (*TODO *) - and type_ = mkMetavar () - in lexp_warning dloc meta "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned"; - (meta, type_) (* FIXME return the right type *)) + | Pmetavar _ + -> let meta = mkMetavar () in (*TODO *) + let type_ = mkMetavar () in + lexp_warning dloc meta "<LEXP_P_INFER>(Pmetavar case) Check output : may be wrong lexp/type returned"; + (meta, type_) (* FIXME return the right type *) - | Phastype (_, pxp, ptp) -> - let ltp, _ = lexp_infer ptp ctx in + | Phastype (_, pxp, ptp) + -> let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx trace), ltp | (Plambda _ | Pcase _) @@ -347,8 +355,6 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = let lxp = _lexp_p_check p meta ctx trace in (lxp, meta) - | _ -> pexp_fatal tloc p "Unhandled Pexp" - and lexp_let_decls decls (body: lexp) ctx i = (* build the weird looking let *) @@ -390,31 +396,38 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = dltype, dltype in - let infer_lambda_body kind var body subst = - (* Read var type from the provided type *) - let ltp, lbtp = match nosusp t (* t is captured *) with - | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp - | lxp -> (unify_with_arrow lxp kind subst) - in - let nctx = env_extend ctx var Variable ltp in - let lbody = _lexp_p_check body lbtp nctx trace in - Lambda(kind, var, ltp, lbody) + let infer_lambda_body kind var aty body subst = + (* Read var type from the provided type *) + let meta_ctx, _ = !global_substitution in + let ltp, lbtp = match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp + | lxp -> unify_with_arrow lxp kind subst in + + let _ = match aty with + | Some paty + -> let laty, lasort = lexp_infer paty ctx in + elab_check_sort ctx lasort var laty; + () (* FIXME: Check `conv_p aty ltp`! *) + | _ -> () in + + let nctx = env_extend ctx var Variable ltp in + let lbody = lexp_check body lbtp nctx in + Lambda(kind, var, ltp, lbody) in let subst, _ = !global_substitution in - let lexp_infer p ctx = _lexp_p_infer p ctx trace in match p with - | Plambda (kind, var, argtyp, body) (* FIXME: Check argtyp! *) - -> infer_lambda_body kind var body subst + | Plambda (kind, var, aty, body) + -> infer_lambda_body kind var aty body subst - (* This is mostly for the case where no branches are provided *) - | Pcase (loc, target, patterns) - -> lexp_case t (loc, target, patterns) ctx trace + (* This is mostly for the case where no branches are provided *) + | Pcase (loc, target, branches) + -> lexp_case t (loc, target, branches) ctx trace - (* handle pcall here * ) - | Pcall (fname, _args) -> *) + (* FIXME: Handle *macro* pcalls here! *) + (* | Pcall (fname, _args) -> *) - | _ -> lexp_p_infer_and_check p ctx t trace + | _ -> lexp_p_infer_and_check p ctx t trace and lexp_p_infer_and_check pexp ctx t i = let (e, inferred_t) = _lexp_p_infer pexp ctx i in @@ -428,8 +441,6 @@ and lexp_p_infer_and_check pexp ctx t i = | Some subst -> global_substitution := subst | None -> debug_msg ( - let print_lxp str = - print_string (lexp_string str) in Debug_fun.do_debug (fun () -> prerr_endline ("0 pxp " ^ pexp_string pexp); ()); @@ -441,45 +452,126 @@ and lexp_p_infer_and_check pexp ctx t i = e (* Lexp.case can sometimes be inferred, but we prefer to always check. *) -and lexp_case rtype (loc, target, patterns) ctx i = +and lexp_case rtype (loc, target, ppatterns) ctx i = (* FIXME: check if case is exhaustive *) (* Helpers *) - let lexp_infer p ctx = _lexp_p_infer p ctx i in + let lexp_infer p ctx = _lexp_p_infer p ctx i in + + let pat_string p = sexp_string (pexp_u_pat p) in - let uniqueness_warn name = - warning loc ("Pattern " ^ name ^ " is a duplicate." ^ - " It will override previous pattern.") in + let uniqueness_warn pat = + warning (pexp_pat_location pat) + ("Pattern " ^ pat_string pat + ^ " is a duplicate. It will override previous pattern.") in - let check_uniqueness loc name map = - try let _ = SMap.find name map in uniqueness_warn name + let check_uniqueness pat name map = + try let _ = SMap.find name map in uniqueness_warn pat with e -> () in (* get target and its type *) let tlxp, tltp = lexp_infer target ctx in + let meta_ctx, _ = !global_substitution in + (* FIXME: We need to be careful with whnf: while the output is equivalent + * to the input, it's not necessarily as readable. So try to reuse the + * "non-whnf" form whenever possible. *) + let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx) meta_ctx) with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let it, targs = call_split tltp in + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) meta_ctx with + | Inductive (_, _, fargs, constructors) + -> assert (List.length fargs = List.length targs); + constructors + | _ -> lexp_error (pexp_location target) tlxp + ("Can't `case` on objects of this type: " + ^ lexp_string tltp); + SMap.empty in (* Read patterns one by one *) - let fold_fun (merged, dflt) (pat, exp) = - (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat exp tlxp ctx i in + let fold_fun (lbranches, dflt) (pat, pexp) = - (* parse using pattern context *) + let add_default v = + (if dflt != None then uniqueness_warn pat); + let nctx = ctx_extend ctx v Variable tltp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in - let exp = _lexp_p_check exp rtype' nctx i in - - if name = "_" then ( - (if dflt != None then uniqueness_warn name); - merged, (Some exp)) - else ( - check_uniqueness iloc name merged; - let merged = SMap.add name (iloc, arg, exp) merged in - merged, dflt) in + let lexp = _lexp_p_check pexp rtype' nctx i in + lbranches, Some (v, lexp) in + + let add_branch pctor pargs = + let loc = pexp_location pctor in + let lctor, _ = _lexp_p_infer pctor ctx i in + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with + | Cons (it', (_, cons_name)) + -> let _ = if OL.conv_p it' it then () + else lexp_error loc lctor + ("Expected pattern of type `" + ^ lexp_string it ^ "` but got `" + ^ lexp_string it' ^ "`") in + let _ = check_uniqueness pat cons_name lbranches in + let cons_args + = try SMap.find cons_name constructors + with Not_found + -> lexp_error loc lctor + ("`" ^ (lexp_string it) + ^ "` does not have a `" + ^ cons_name ^ "` constructor"); + [] in + + let subst = List.fold_right (fun (_, t) s -> S.cons t s) + targs S.identity in + let rec make_nctx ctx fargs s pargs cargs = match pargs, cargs with + | [], [] -> ctx, List.rev fargs + | (_, pat)::_, [] + -> lexp_error loc lctor + "Too many arguments to the constructor"; + make_nctx ctx fargs s [] [] + | (None, Ppatany _)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, None)::fargs) + (ssink vdummy s) pargs cargs + | (None, Ppatsym v)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx (Some v) Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, Some v)::fargs) + (ssink v s) pargs cargs + | (_, Ppatcons (p, _))::pargs, cargs + -> lexp_error (pexp_location p) lctor + "Nested patterns not supported!"; + make_nctx ctx fargs s pargs cargs + | pargs, (ak, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((ak, None)::fargs) + (ssink vdummy s) pargs cargs in + let nctx, fargs = make_nctx ctx [] subst pargs cons_args in + let rtype' = mkSusp rtype + (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + let lexp = _lexp_p_check pexp rtype' nctx i in + SMap.add cons_name (loc, fargs, lexp) lbranches, + dflt + | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt + in + + match pat with + | Ppatany _ -> add_default None + | Ppatsym ((_, name) as var) + -> (try let idx = senv_lookup name ctx in + let meta_ctx, _ = !global_substitution in + match OL.lexp_whnf (Var (var, idx)) + (ectx_to_lctx ctx) meta_ctx with + | Cons _ (* It's indeed a constructor! *) + -> add_branch (Pvar var) [] + | _ -> add_default (Some var) (* A named default branch. *) + with Not_found -> add_default (Some var)) + + | Ppatcons (pctor, pargs) -> add_branch pctor pargs in let (lpattern, dflt) = - List.fold_left fold_fun (SMap.empty, None) patterns in + List.fold_left fold_fun (SMap.empty, None) ppatterns in - Case (loc, tlxp, tltp, rtype, lpattern, dflt) + Case (loc, tlxp, rtype, lpattern, dflt) (* Identify Call Type and return processed call *) and lexp_call (func: pexp) (sargs: sexp list) ctx i = @@ -498,13 +590,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let lexp_infer p ctx = _lexp_p_infer p ctx i in let lexp_check p ltp ctx = _lexp_p_check p ltp ctx i in - let from_lctx ctx = try (from_lctx ctx) - with e ->( - debug_messages error loc - "Could not convert lexp context into rte context" []; - print_eval_trace None; - raise e) in - (* Vanilla : sqr is inferred and (lambda x -> x * x) is returned * Macro : sqr is returned * Constructor : a constructor is returned @@ -625,104 +710,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall () -(* Read a pattern and create the equivalent representation *) -and lexp_read_pattern pattern exp target ctx trace: - ((string * location * (arg_kind * vdef option) list) * elab_context) = - - match pattern with - | Ppatany (loc) -> (* Catch all expression nothing to do. *) - ("_", loc, []), ctx - - | Ppatvar ((loc, name) as var) ->( - try( - let idx = senv_lookup name ctx in - match env_lookup_expr ctx ((loc, name), idx) with - (* We are matching a constructor. *) - | Some (Cons _) -> (name, loc, []), ctx - - (* name is defined but is not a constructor *) - (* it technically could be ... (expr option) *) - (* What about Var -> Cons ? *) - | _ -> let nctx = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - (* Would it not make a default match too? *) - with Not_found -> - (* Create a variable containing target. *) - let nctx = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - | Ppatcons (ctor, args) -> - (* Get cons argument types. *) - let lctor, _ = _lexp_p_infer ctor ctx trace in - let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with - | Cons (it, (loc, cons_name)) - -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) - meta_ctx with - | Inductive(_, (_, label), _, map) - -> (try SMap.find cons_name map - with Not_found - -> warning loc ("`" ^ (lexp_string it) ^ "` does not hold a `" - ^ cons_name ^ "` constructor"); []) - | it -> fatal loc - ("`" ^ (lexp_string it) ^ "` is not an inductive type!") in - - (* FIXME: Don't remove them, add them without names! *) - (* FIXME: Add support for explicit-implicit fields! *) - (* Remove non explicit argument. *) - let rec remove_nexplicit args acc = - match args with - | [] -> List.rev acc - | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) - | hd::tl -> remove_nexplicit tl acc in - - let cons_args = remove_nexplicit cons_args [] in - - (* read pattern args *) - let args, nctx = lexp_read_pattern_args args cons_args ctx in - (cons_name, loc, args), nctx - | _ -> warning (pexp_location ctor) - ("Invalid constructor `" ^ (pexp_string ctor) ^ "`"); - - ("_", pexp_location ctor, []), ctx - -(* Read patterns inside a constructor *) -and lexp_read_pattern_args args (args_type : lexp list) ctx: - (((arg_kind * vdef option) list) * elab_context)= - - let length_type = List.length args_type in - let length_pat = List.length args in - - let make_list elem size = - let rec loop i acc = - if i < size then loop (i + 1) (elem::acc) else acc - in loop 0 [] in - - let args_type = if length_type != length_pat then - make_list dltype length_pat else args_type in - - (if length_type != length_pat then warning dloc "Size Mismatch"); - - let rec loop args args_type acc ctx = - match args, args_type with - | [], _ -> (List.rev acc), ctx - | hd::tl, ltp::type_tl -> ( - let (_, pat) = hd in - match pat with - (* Nothing to do *) - | Ppatany (loc) -> loop tl type_tl ((Aexplicit, None)::acc) ctx - | Ppatvar ((loc, name) as var) -> - (* Add var *) - let nctx = env_extend ctx var Variable ltp in - let nacc = (Aexplicit, Some var)::acc in - loop tl type_tl nacc nctx - | _ -> error dloc "Constructor inside a Constructor"; - loop tl type_tl ((Aexplicit, None)::acc) ctx) - | _ -> typer_unreachable "unreachable branch" - - in loop args args_type [] ctx - (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = Debug_fun.do_debug (fun () -> ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -159,8 +159,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = args)) ctx meta_ctx | Call (e', xs1) -> Call (e', List.append xs1 xs) - | e' -> Call (e', xs)) - | Case (l, e, bt, rt, branches, default) -> + | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) + | Case (l, e, rt, branches, default) -> + let e' = lexp_whnf e ctx meta_ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in @@ -174,15 +175,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = lexp_whnf (push_susp branch subst) ctx meta_ctx with Not_found -> match default - with | Some default -> lexp_whnf default ctx meta_ctx + with | Some (v,default) + -> lexp_whnf (push_susp default (S.substitute e')) + ctx meta_ctx | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); - Case (l, e, bt, rt, branches, default) in - (match lexp_whnf e ctx meta_ctx with + Case (l, e, rt, branches, default) in + (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | e' -> Case (l, e', bt, rt, branches, default)) + | _ -> Case (l, e', rt, branches, default)) | Metavar (idx, _, _) -> lexp_whnf (L.VMap.find idx meta_ctx) ctx meta_ctx | e -> e @@ -222,6 +225,7 @@ let sort_compose l s1 s2 = (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) let rec check ctx e = (* let mustfind = assert_type e t in *) + let meta_ctx = VMap.empty in match e with | Imm (Float (_, _)) -> B.type_float | Imm (Integer (_, _)) -> B.type_int @@ -244,7 +248,7 @@ let rec check ctx e = | Let (_, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) - -> (match lexp_whnf (check ctx t) ctx VMap.empty with + -> (match lexp_whnf (check ctx t) ctx meta_ctx with | Sort (_, Stype _) -> () | _ -> (U.msg_error "TC" (lexp_location t) "Def type is not a type!"; ())); @@ -261,7 +265,7 @@ let rec check ctx e = -> (let k1 = check ctx t1 in let nctx = DB.lexp_ctx_cons ctx 0 v Variable t1 in let k2 = check nctx t2 in - match lexp_whnf k1 ctx VMap.empty, lexp_whnf k2 nctx VMap.empty with + match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 nctx meta_ctx with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase then k2 else Sort (l, sort_compose l s1 s2) @@ -272,7 +276,7 @@ let rec check ctx e = "Not a proper type"; Sort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) - -> ((match lexp_whnf (check ctx t) ctx VMap.empty with + -> ((match lexp_whnf (check ctx t) ctx meta_ctx with | Sort _ -> () | _ -> (U.msg_error "TC" (lexp_location t) "Formal arg type is not a type!"; ())); @@ -284,7 +288,7 @@ let rec check ctx e = -> let ft = check ctx f in List.fold_left (fun ft (ak,arg) -> let at = check ctx arg in - match lexp_whnf ft ctx VMap.empty with + match lexp_whnf ft ctx meta_ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (U.msg_error "TC" (lexp_location arg) @@ -307,19 +311,20 @@ let rec check ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (if ak == P.Aerasable && impredicative_erase - then level - else match lexp_whnf (check ctx t) ctx VMap.empty with - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> sort_level_max 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; - SortLevel SLz), + (match lexp_whnf (check ctx t) ctx meta_ctx with + | Sort _ when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max 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) case in @@ -331,12 +336,13 @@ let rec check ctx e = arg_loop args (DB.lctx_extend ctx (Some v) Variable t)) in let tct = arg_loop args ctx in tct - | Case (l, e, it, ret, branches, default) - -> let rec call_split e = - match e with - | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + | Case (l, e, ret, branches, default) + -> let rec call_split e = match e with + | Call (f, args) -> (f, args) | _ -> (e,[]) in - (match call_split (lexp_whnf (check ctx e) ctx VMap.empty) with + let etype = lexp_whnf (check ctx e) ctx meta_ctx in + let it, aargs = call_split etype in + (match lexp_whnf it ctx meta_ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -370,12 +376,14 @@ let rec check ctx e = assert_type branch ret (check nctx branch)) branches; (match default with - | Some d -> assert_type d ret (check ctx d) + | Some (v, d) + -> assert_type d (mkSusp ret (S.shift 1)) + (check (DB.lctx_extend ctx v (LetDef e) etype) d) | _ -> ()) | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret | Cons (t, (_, name)) - -> (match lexp_whnf t ctx VMap.empty with + -> (match lexp_whnf t ctx meta_ctx with | Inductive (l, _, fargs, constructors) as it -> let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -424,7 +432,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Call(fct, args) -> E.Call((erase_type fct), (filter_arg_list args)) - | L.Case(l, target, _, _, cases, default) -> + | L.Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), (clean_maybe default)) @@ -452,7 +460,7 @@ and clean_decls decls = and clean_maybe lxp = match lxp with - | Some lxp -> Some (erase_type lxp) + | Some (v, lxp) -> Some (v, erase_type lxp) | None -> None and clean_map cases = @@ -482,4 +490,4 @@ let pol_string xp = match xp with let pol_name xp = match xp with | Pexp p -> P.pexp_name p - | Elexp e -> E.elexp_name e \ No newline at end of file + | Elexp e -> E.elexp_name e ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -57,8 +57,8 @@ and ppat = (* This data type allows nested patterns, but in reality we don't * support them. I.e. we don't want Ppatcons within Ppatcons. *) | Ppatany of location - | Ppatvar of pvar - | Ppatcons of pexp * ((arg_kind * symbol) option * ppat) list + | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) + | Ppatcons of pexp * (symbol option * ppat) list and pdecl = | Ptype of symbol * pexp (* identifier : expr *) @@ -83,7 +83,7 @@ let rec pexp_location e = let rec pexp_pat_location e = match e with | Ppatany l -> l - | Ppatvar (l,_) -> l + | Ppatsym (l,_) -> l | Ppatcons (e, _) -> pexp_location e (* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" @@ -241,29 +241,23 @@ and pexp_u_ind_arg arg = match arg with and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) - | Node (Symbol (_, "_:-_"), [Symbol f; Symbol s]) - -> (Some (Aexplicit, f), Ppatvar s) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s]) - -> (Some (Aimplicit, f), Ppatvar s) - | Node (Symbol (_, "_:≡_"), [Symbol f; Symbol s]) - -> (Some (Aerasable, f), Ppatvar s) + -> (Some f, Ppatsym s) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; (None, Ppatany loc) -and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp = +and pexp_u_pat_arg (arg : symbol option * ppat) : sexp = match arg with | (None, p) -> pexp_u_pat p - | (Some (k, ((l,_) as n)), p) -> - Node (Symbol (l, match k with Aexplicit -> "_:-_" - | Aimplicit -> "_:=_" - | Aerasable -> "_:≡_"), + | (Some ((l,_) as n), p) -> + Node (Symbol (l, "_:=_"), (* FIXME: the label is wrong! *) [Symbol (pexp_u_id (Some n)); pexp_u_pat p]) and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l - | Symbol s -> Ppatvar s + | Symbol s -> Ppatsym s | Node (c, args) -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in @@ -271,7 +265,7 @@ and pexp_p_pat (s : sexp) : ppat = match s with and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") - | Ppatvar s -> Symbol s + | Ppatsym s -> Symbol s | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args) and pexp_p_decls e: pdecl list = ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -258,12 +258,13 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = in let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = match lxp_opt1, lxp_opt2 with - | Some lxp1, Some lxp2 -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst + | Some (_, lxp1), Some (_, lxp2) + -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst | _, _ -> None in match (case, lxp) with - | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) - -> match_lxp_opt lxpopt lxopt2 ((lt11, lt21)::(lt12, lt22)::[]) smap smap2 subst + | (Case (_, lxp, lt12, smap, lxpopt), Case (_, lxp2, lt22, smap2, lxopt2)) + -> match_lxp_opt lxpopt lxopt2 ((lt12, lt22)::[]) smap smap2 subst | (Case _, _) -> Some (subst, [(case, lxp)]) | (_, _) -> None View it on GitLab: https://gitlab.com/monnier/typer/compare/df86998fccce430164dcc9784bc09aef26…

1 0

[Git][monnier/typer][master] Fix various typing and inference problems with `Case`
by Stefan 20 Oct '16

20 Oct '16

Stefan pushed to branch master at Stefan / Typer Commits: a459a1ea by Stefan Monnier at 2016-10-20T15:28:17-04:00 Fix various typing and inference problems with `Case` * GNUmakefile (OBFLAGS): Add debug info. * src/elexp.ml (elexp): Add binding of scrutinee in the default branch. (elexp_string.maybe_str): Adjust print code accordingly. * src/eval.ml (eval_case): Bind scrutinee in the default branch. * src/lexp.ml (lexp): Add binding of scrutinee in the default branch. (push_susp, _lexp_to_str): Adjust accordingly. (lexp_unparse): Adjust to pexp changes. * src/lparse.ml (elab_check_proper_type): Use lexp_print to get db indexes. (ctx_extend): New function. (_lexp_p_infer): Check that arrow's args are types. (lexp_case): Rewrite; fix problems with scoping. (lexp_read_pattern, lexp_read_pattern_args): Remove. * src/opslexp.ml (lexp_whnf): Adjust to new `Case`. Preserve the non-whnf in the sub-parts we return. (check): Check that erasable inductive type fields have a proper type. Don't assume call_split returns whnf elements. Adjust to new `Case`. (clean_maybe): Adjust to new `Case`. * src/pexp.ml (ppat): Rename Ppatvar to Ppatsym since it can be either a var or a constructor. Drop arg_kind from Ppatcons. (pexp_p_pat_arg): Only recognize := as explicit-implicit. (pexp_u_pat_arg): Only use := for explicit-implicit. - - - - - 8 changed files: - DESIGN - GNUmakefile - src/elexp.ml - src/eval.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/pexp.ml Changes: ===================================== DESIGN ===================================== --- a/DESIGN +++ b/DESIGN @@ -1710,9 +1710,20 @@ So we'd define numbers = numbers' 0 * Papers -** BigBang: Designing a statically typed scripting language -** Dependently typed Racket -** Dependently typed Haskell +** Macros and tactics +*** Rtac +[1] Dissertation: +https://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory/ +[2] ESOP'16: +https://gmalecha.github.io/publication/2016/01/01/extensible-and-efficient-automation-through-reflective-tactics/ +[3] ITP'14: +https://gmalecha.github.io/publication/2014/07/14/compositional-computational-reflection/ +*** ssreflect +*** Mtac +** Other +*** BigBang: Designing a statically typed scripting language +*** Dependently typed Racket +*** Dependently typed Haskell "My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/) Still working @@ -1720,36 +1731,36 @@ on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)" -** On Irrelevance and Algorithmic Equality in Predicative Type Theory, +*** On Irrelevance and Algorithmic Equality in Predicative Type Theory, Andreas Abel & Gabriel Scherer, FOSSACS 2011. -** "A few constructions on constructors" -** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani -** http://homotopytypetheory.org/book/ -** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages +*** "A few constructions on constructors" +*** How to Make Ad Hoc Proof Automation Less Ad Hoc, Beta Ziliani +*** http://homotopytypetheory.org/book/ +*** CMU's 2013 Fall: 15-819 Advanced Topics in Programming Languages http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%22… -** Propositions as Sessions, Philip Wadler -** A few constructions on constructors, by Conor et al. -** Constructive selection principle (Markov's principle) +*** Propositions as Sessions, Philip Wadler +*** A few constructions on constructors, by Conor et al. +*** Constructive selection principle (Markov's principle) http://www.encyclopediaofmath.org/index.php/Constructive_selection_principle https://en.wikipedia.org/wiki/Markov%27s_principle -** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 -** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf -** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau -** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete +*** size-change termination, Lee, Jones and Ben-Amram, doi:10.1145/360204.360210 +*** A Predicative Analysis of Structural Recursion, Andreas Abel and Thorsten Altenkirch, http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf +*** A New Look at Generalized Rewriting in Type Theory, Matthieu Sozeau +*** http://moca.inria.fr/ On the implementation of construction functions for non-free concrete data types. F. Blanqui, T. Hardin and P. Weis. ESOP'07. -** The Nemerle language -** "A Theory of Typed Hygienic Macros" de David Herman +*** The Nemerle language +*** "A Theory of Typed Hygienic Macros" de David Herman http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf -** http://www.mpi-sws.org/~beta/mtac/ -** Non-strictly positive and elimination +*** http://www.mpi-sws.org/~beta/mtac/ +*** Non-strictly positive and elimination "Inductively defined types", by Thierry Coquand and Christine Paulin, COLOG'88, LNCS 417 -** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. +*** Dependently Typed Programming based on Automated Theorem Proving, Alasdair Armstrong, Simon Foster, and Georg Struth. http://arxiv.org/pdf/1112.3833v1 -** Strong Normalization for Coq (CiC). +*** Strong Normalization for Coq (CiC). http://www.cs.rice.edu/~emw4/uniform-lr.pdf -** Irrelevant/erasable args +*** Irrelevant/erasable args *** The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Bruno Barras and Bruno Bernardo, fossacs08. @@ -1779,7 +1790,7 @@ Finally we show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. -** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 +*** Parametricity and variants of Girard's J operator, Robert Harper and John C. Mitchell, Journal Information Processing Letters archive, Volume 70 Issue 1, April 01, 1999 The Girard-Reynolds polymorphic λ-calculus is generally regarded as a calculus of parametric polymorphism in which all well-formed terms are strongly normalizing with respect to β-reductions. Girard demonstrated that @@ -1793,10 +1804,10 @@ impredicativity is essential to the argument; predicative variants of the polymorphic λ-calculus admit non-parametric operations without sacrificing normalization. -** Idris (Edwin Brady) -** http://albatross-lang.sourceforge.net -** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf -** Read +*** Idris (Edwin Brady) +*** http://albatross-lang.sourceforge.net +*** Idris's Effects http://eb.host.cs.st-andrews.ac.uk/drafts/dep-eff.pdf +*** Read *** (Co)Iteration for higher-order nested datatypes, Andreas Abel and Ralph Matthes, [Abel03] *** Inductive Families Need Not Store Their Indices, Edwin Brady, Conor McBride and James McKinna. http://www.cs.st-andrews.ac.uk/~eb/writings/types2003.pdf ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -4,7 +4,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./_build/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -build-dir _build +OBFLAGS = -lflags -g -cflags -g -build-dir _build # COMPILE_MODE = native all: typer debug tests-build ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -52,8 +52,9 @@ type elexp = | Lambda of vdef * elexp | Call of elexp * elexp list | Cons of symbol - | Case of U.location * elexp * - (U.location * (vdef option) list * elexp) SMap.t * elexp option + | Case of U.location * elexp + * (U.location * (vdef option) list * elexp) SMap.t + * (vdef option * elexp) option (* Type place-holder just in case *) | Type (* Inductive takes a slot in the env that is why it need to be here *) @@ -90,8 +91,10 @@ let rec elexp_print lxp = print_string (elexp_string lxp) and elexp_string lxp = let maybe_str lxp = match lxp with - | Some lxp -> " | _ => " ^ (elexp_string lxp) - | None -> "" in + | Some (v, lxp) + -> " | " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ elexp_string lxp + | None -> "" in let str_decls d = List.fold_left (fun str ((_, s), lxp) -> ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -363,7 +363,9 @@ and eval_case ctx i loc target pat dflt = (* Run default *) with Not_found -> (match dflt with - | Some lxp -> _eval lxp ctx i + | Some (var, lxp) + -> let var' = match var with None -> None | Some (_, n) -> Some n in + _eval lxp (add_rte_variable var' v ctx) i | _ -> error loc "Match Failure") and build_arg_list args ctx i = ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -41,8 +41,19 @@ type label = symbol (*************** Elaboration to Lexp *********************) -(* Pour la propagation des types bidirectionnelle, tout va dans `infer`, - * sauf Lambda et Case qui vont dans `check`. Je crois. *) +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + type ltype = lexp and subst = lexp S.subst and lexp = @@ -64,7 +75,7 @@ type ltype = lexp | Case of U.location * lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t - * lexp option (* Default. *) + * (vdef option * lexp) option (* Default. *) (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -276,7 +287,7 @@ let rec lexp_location e = (********* Normalizing a term *********) -let vdummy = (U.dummy_location, "dummy") +let vdummy = (U.dummy_location, "<anon>") let maybev mv = match mv with None -> vdummy | Some v -> v let rec push_susp e s = (* Push a suspension one level down. *) @@ -325,7 +336,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) cases, match default with | None -> default - | Some e -> Some (mkSusp e s)) + | Some (v,e) -> Some (v, mkSusp e (ssink (maybev v) s))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -546,19 +557,24 @@ let rec lexp_unparse lxp = let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with - | [] -> Ppatvar (loc, str), lexp_unparse bch + | [] -> Ppatsym (loc, str), lexp_unparse bch | _ -> - let pat_args = List.map (fun (kind, vdef) -> - match vdef with - | Some vdef -> Some (kind, vdef), Ppatvar(vdef) - | None -> None, Ppatany(loc)) args + let pat_args + = List.map (fun (kind, vdef) + -> match vdef with + | Some vdef -> Some vdef, Ppatsym vdef + | None -> None, Ppatany loc) + args (* FIXME: Rather than a Pcons we'd like to refer to an existing * binding with that value! *) in Ppatcons (Pcons (bt, (loc, str)), pat_args), lexp_unparse bch ) (SMap.bindings branches) in let pbranch = match default with - | Some dft -> (Ppatany(loc), lexp_unparse dft)::pbranch + | Some (v,dft) -> ((match v with + | None -> Ppatany loc + | Some vdef -> Ppatsym vdef), + lexp_unparse dft)::pbranch | None -> pbranch in Pcase (loc, lexp_unparse target, pbranch) @@ -776,8 +792,10 @@ and _lexp_to_str ctx exp = match dflt with | None -> str - | Some df -> - str ^ nl ^ (make_indent 1) ^ "| _ => " ^ (lexp_to_stri 1 df)) + | Some (v, df) -> + str ^ nl ^ (make_indent 1) + ^ "| " ^ (match v with None -> "_" | Some (_,name) -> name) + ^ " => " ^ (lexp_to_stri 1 df)) | Builtin ((_, name), _) -> name ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -94,14 +94,15 @@ let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *) | _ -> lexp_error l ltp - ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_string ltp) + ("Type of `" ^ name ^ "` is not a proper type: " + ^ lexp_string ltp) let elab_check_proper_type (ctx : elab_context) ltp v = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp - with e -> print_string ("Exception while checking type `" - ^ lexp_string ltp ^ "` of var `" ^ - (let (_, name) = v in name) ^"`\n"); + with e -> print_string "Exception while checking type `"; + lexp_print ltp; + print_string ("` of var `" + ^ (let (_, name) = v in name) ^"`\n"); print_lexp_ctx (ectx_to_lctx ctx); raise e @@ -124,6 +125,10 @@ let elab_check_def (ctx : elab_context) var lxp ltype = " because"; (lexp_string (OL.check lctx lxp)) ^ "!= " ^ (lexp_string ltype);]) +let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = + elab_check_proper_type ctx ltype (maybev var); + ectx_extend ctx var def ltype + let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; env_extend ctx var (LetDef lxp) ltype @@ -229,9 +234,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) -> let ltp, _ = lexp_infer tp ctx in + let _ = elab_check_proper_type ctx ltp (maybev ovar) in let nctx = ectx_extend ctx ovar Variable ltp in let lxp, _ = lexp_infer expr nctx in + let _ = elab_check_proper_type nctx lxp (maybev ovar) in let v = Arrow(kind, ovar, ltp, tloc, lxp) in v, type0 @@ -294,7 +301,7 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = | lxp -> lexp_error loc lxp "Not an Inductive Type"; [], [] in - (* build Arrow type *) + (* Build Arrow type. *) let target = if formal = [] then push_susp idt (S.shift (List.length args)) else @@ -382,47 +389,113 @@ and lexp_case rtype (loc, target, ppatterns) ctx i = (* FIXME: check if case is exhaustive *) (* Helpers *) - let lexp_infer p ctx = _lexp_p_infer p ctx i in + let lexp_infer p ctx = _lexp_p_infer p ctx i in - let uniqueness_warn name = - warning loc ("Pattern " ^ name ^ " is a duplicate." ^ - " It will override previous pattern.") in + let pat_string p = sexp_string (pexp_u_pat p) in - let check_uniqueness loc name map = - try let _ = SMap.find name map in uniqueness_warn name + let uniqueness_warn pat = + warning (pexp_pat_location pat) + ("Pattern " ^ pat_string pat + ^ " is a duplicate. It will override previous pattern.") in + + let check_uniqueness pat name map = + try let _ = SMap.find name map in uniqueness_warn pat with e -> () in (* get target and its type *) let tlxp, tltp = lexp_infer target ctx in - let rec call_split e = - match e with - | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + (* FIXME: We need to be careful with whnf: while the output is equivalent + * to the input, it's not necessarily as readable. So try to reuse the + * "non-whnf" form whenever possible. *) + let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) with + | Call (f, args) -> (f, args) | _ -> (e,[]) in - let it, targs = call_split (OL.lexp_whnf tltp (ectx_to_lctx ctx)) in - let _ = match it with - | Inductive (_, _, fargs, _) - -> assert (List.length fargs = List.length targs); () + let it, targs = call_split tltp in + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with + | Inductive (_, _, fargs, constructors) + -> assert (List.length fargs = List.length targs); + constructors | _ -> lexp_error (pexp_location target) tlxp ("Can't `case` on objects of this type: " - ^ lexp_string tltp) in + ^ lexp_string tltp); + SMap.empty in (* Read patterns one by one *) - let fold_fun (lbranches, dflt) (pat, exp) = - (* Create pattern context *) - let (name, iloc, arg), nctx = lexp_read_pattern pat tlxp ctx i in + let fold_fun (lbranches, dflt) (pat, pexp) = - (* parse using pattern context *) + let add_default v = + (if dflt != None then uniqueness_warn pat); + let nctx = ctx_extend ctx v Variable tltp in let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - M.length (ectx_to_lctx ctx))) in - let exp = _lexp_p_check exp rtype' nctx i in - - if name = "_" then ( - (if dflt != None then uniqueness_warn name); - lbranches, (Some exp) - ) else ( - check_uniqueness iloc name lbranches; - let lbranches = SMap.add name (iloc, arg, exp) lbranches in - lbranches, dflt) in + let lexp = _lexp_p_check pexp rtype' nctx i in + lbranches, Some (v, lexp) in + + let add_branch pctor pargs = + let loc = pexp_location pctor in + let lctor, _ = _lexp_p_infer pctor ctx i in + match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + | Cons (it', (_, cons_name)) + -> let _ = if OL.conv_p it' it then () + else lexp_error loc lctor + ("Expected pattern of type `" + ^ lexp_string it ^ "` but got `" + ^ lexp_string it' ^ "`") in + let _ = check_uniqueness pat cons_name lbranches in + let cons_args + = try SMap.find cons_name constructors + with Not_found + -> lexp_error loc lctor + ("`" ^ (lexp_string it) + ^ "` does not have a `" + ^ cons_name ^ "` constructor"); + [] in + + let subst = List.fold_right (fun (_, t) s -> S.cons t s) + targs S.identity in + let rec make_nctx ctx fargs s pargs cargs = match pargs, cargs with + | [], [] -> ctx, List.rev fargs + | (_, pat)::_, [] + -> lexp_error loc lctor + "Too many arguments to the constructor"; + make_nctx ctx fargs s [] [] + | (None, Ppatany _)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, None)::fargs) + (ssink vdummy s) pargs cargs + | (None, Ppatsym v)::pargs, (Aexplicit, _, fty)::cargs + -> let nctx = ctx_extend ctx (Some v) Variable (mkSusp fty s) in + make_nctx nctx ((Aexplicit, Some v)::fargs) + (ssink v s) pargs cargs + | (_, Ppatcons (p, _))::pargs, cargs + -> lexp_error (pexp_location p) lctor + "Nested patterns not supported!"; + make_nctx ctx fargs s pargs cargs + | pargs, (ak, _, fty)::cargs + -> let nctx = ctx_extend ctx None Variable (mkSusp fty s) in + make_nctx nctx ((ak, None)::fargs) + (ssink vdummy s) pargs cargs in + let nctx, fargs = make_nctx ctx [] subst pargs cons_args in + let rtype' = mkSusp rtype + (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + let lexp = _lexp_p_check pexp rtype' nctx i in + SMap.add cons_name (loc, fargs, lexp) lbranches, + dflt + | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt + in + + match pat with + | Ppatany _ -> add_default None + | Ppatsym ((_, name) as var) + -> (try let idx = senv_lookup name ctx in + match OL.lexp_whnf (Var (var, idx)) (ectx_to_lctx ctx) with + | Cons _ (* It's indeed a constructor! *) + -> add_branch (Pvar var) [] + | _ -> add_default (Some var) (* A named default branch. *) + with Not_found -> add_default (Some var)) + + | Ppatcons (pctor, pargs) -> add_branch pctor pargs in let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in @@ -543,102 +616,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* FIXME: Handle special-forms here as well! *) | _ -> handle_funcall () -(* Read a pattern and create the equivalent representation *) -and lexp_read_pattern pattern target ctx trace - : ((string * location * (arg_kind * vdef option) list) - * elab_context) = - match pattern with - | Ppatany (loc) (* Catch all expression, nothing to do. *) - -> ("_", loc, []), ctx - - | Ppatvar ((loc, name) as var) ->( - try( - let idx = senv_lookup name ctx in - match env_lookup_expr ctx ((loc, name), idx) with - (* We are matching a constructor. *) - | Some (Cons _) -> (name, loc, []), ctx - - (* name is defined but is not a constructor *) - (* it technically could be ... (expr option) *) - (* What about Var -> Cons ? *) - | _ -> let nctx = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - (* Would it not make a default match too? *) - with Not_found -> - (* Create a variable containing target. *) - let nctx = ctx_define ctx var target dltype in - (name, loc, []), nctx) - - | Ppatcons (ctor, args) - -> (* Get cons argument types. *) - let lctor, _ = _lexp_p_infer ctor ctx trace in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with - | Cons (it, (loc, cons_name)) - -> let cons_args = match OL.lexp_whnf it (ectx_to_lctx ctx) with - | Inductive(_, (_, label), _, map) - -> (try SMap.find cons_name map - with Not_found - -> warning loc ("`" ^ (lexp_string it) ^ "` does not hold a `" - ^ cons_name ^ "` constructor"); []) - | it -> fatal loc - ("`" ^ (lexp_string it) ^ "` is not an inductive type!") in - - (* FIXME: Don't remove them, add them without names! *) - (* FIXME: Add support for explicit-implicit fields! *) - (* Remove non explicit argument. *) - let rec remove_nexplicit args acc = - match args with - | [] -> List.rev acc - | (Aexplicit, _, ltp)::tl -> remove_nexplicit tl (ltp::acc) - | hd::tl -> remove_nexplicit tl acc in - - let cons_args = remove_nexplicit cons_args [] in - - (* read pattern args *) - let args, nctx = lexp_read_pattern_args args cons_args ctx in - (cons_name, loc, args), nctx - | _ -> warning (pexp_location ctor) - ("Invalid constructor `" ^ (pexp_string ctor) ^ "`"); - - ("_", pexp_location ctor, []), ctx - -(* Read patterns inside a constructor *) -and lexp_read_pattern_args args (args_type : lexp list) ctx: - (((arg_kind * vdef option) list) * elab_context)= - - let length_type = List.length args_type in - let length_pat = List.length args in - - let make_list elem size = - let rec loop i acc = - if i < size then loop (i + 1) (elem::acc) else acc - in loop 0 [] in - - let args_type = if length_type != length_pat then - make_list dltype length_pat else args_type in - - (if length_type != length_pat then warning dloc "Size Mismatch"); - - let rec loop args args_type acc ctx = - match args, args_type with - | [], _ -> (List.rev acc), ctx - | hd::tl, ltp::type_tl -> ( - let (_, pat) = hd in - match pat with - (* Nothing to do *) - | Ppatany (loc) -> loop tl type_tl ((Aexplicit, None)::acc) ctx - | Ppatvar ((loc, name) as var) -> - (* Add var *) - let nctx = env_extend ctx var Variable ltp in - let nacc = (Aexplicit, Some var)::acc in - loop tl type_tl nacc nctx - | _ -> error dloc "Constructor inside a Constructor"; - loop tl type_tl ((Aexplicit, None)::acc) ctx) - | _ -> typer_unreachable "unreachable branch" - - in loop args args_type [] ctx - (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = let lexp_parse p ctx = _lexp_p_infer p ctx i in ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -150,8 +150,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with args)) ctx | Call (e', xs1) -> Call (e', List.append xs1 xs) - | e' -> Call (e', xs)) + | e' -> Call (e, xs)) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> + let e' = lexp_whnf e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in @@ -165,15 +166,16 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with lexp_whnf (push_susp branch subst) ctx with Not_found -> match default - with | Some default -> lexp_whnf default ctx + with | Some (v,default) + -> lexp_whnf (push_susp default (S.substitute e')) ctx | _ -> U.msg_error "WHNF" l ("Unhandled constructor " ^ name ^ "in case expression"); Case (l, e, rt, branches, default) in - (match lexp_whnf e ctx with + (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | e' -> Case (l, e', rt, branches, default)) + | _ -> Case (l, e', rt, branches, default)) | e -> e @@ -297,19 +299,20 @@ let rec check ctx e = let level, _ = List.fold_left (fun (level, ctx) (ak, v, t) -> - (if ak == P.Aerasable && impredicative_erase - then level - else match lexp_whnf (check ctx t) ctx with - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> sort_level_max 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; - SortLevel SLz), + (match lexp_whnf (check ctx t) ctx with + | Sort _ when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + (* FIXME: scoping of level vars! *) + -> sort_level_max 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) case in @@ -322,11 +325,12 @@ let rec check ctx e = let tct = arg_loop args ctx in tct | Case (l, e, ret, branches, default) - -> let rec call_split e = - match e with - | Call (f, args) -> let (f',args') = call_split f in (f', args' @ args) + -> let rec call_split e = match e with + | Call (f, args) -> (f, args) | _ -> (e,[]) in - (match call_split (lexp_whnf (check ctx e) ctx) with + let etype = lexp_whnf (check ctx e) ctx in + let it, aargs = call_split etype in + (match lexp_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -360,7 +364,9 @@ let rec check ctx e = assert_type branch ret (check nctx branch)) branches; (match default with - | Some d -> assert_type d ret (check ctx d) + | Some (v, d) + -> assert_type d (mkSusp ret (S.shift 1)) + (check (DB.lctx_extend ctx v (LetDef e) etype) d) | _ -> ()) | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); ret @@ -442,7 +448,7 @@ and clean_decls decls = and clean_maybe lxp = match lxp with - | Some lxp -> Some (erase_type lxp) + | Some (v, lxp) -> Some (v, erase_type lxp) | None -> None and clean_map cases = ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -57,8 +57,8 @@ and ppat = (* This data type allows nested patterns, but in reality we don't * support them. I.e. we don't want Ppatcons within Ppatcons. *) | Ppatany of location - | Ppatvar of pvar - | Ppatcons of pexp * ((arg_kind * symbol) option * ppat) list + | Ppatsym of pvar (* A named default pattern, or a 0-ary constructor. *) + | Ppatcons of pexp * (symbol option * ppat) list and pdecl = | Ptype of symbol * pexp (* identifier : expr *) @@ -83,7 +83,7 @@ let rec pexp_location e = let rec pexp_pat_location e = match e with | Ppatany l -> l - | Ppatvar (l,_) -> l + | Ppatsym (l,_) -> l | Ppatcons (e, _) -> pexp_location e (* In the following "pexp_p" the prefix for "parse a sexp, returning a pexp" @@ -241,29 +241,23 @@ and pexp_u_ind_arg arg = match arg with and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) - | Node (Symbol (_, "_:-_"), [Symbol f; Symbol s]) - -> (Some (Aexplicit, f), Ppatvar s) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s]) - -> (Some (Aimplicit, f), Ppatvar s) - | Node (Symbol (_, "_:≡_"), [Symbol f; Symbol s]) - -> (Some (Aerasable, f), Ppatvar s) + -> (Some f, Ppatsym s) | _ -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; (None, Ppatany loc) -and pexp_u_pat_arg (arg : (arg_kind * symbol) option * ppat) : sexp = +and pexp_u_pat_arg (arg : symbol option * ppat) : sexp = match arg with | (None, p) -> pexp_u_pat p - | (Some (k, ((l,_) as n)), p) -> - Node (Symbol (l, match k with Aexplicit -> "_:-_" - | Aimplicit -> "_:=_" - | Aerasable -> "_:≡_"), + | (Some ((l,_) as n), p) -> + Node (Symbol (l, "_:=_"), (* FIXME: the label is wrong! *) [Symbol (pexp_u_id (Some n)); pexp_u_pat p]) and pexp_p_pat (s : sexp) : ppat = match s with | Symbol (l, "_") -> Ppatany l - | Symbol s -> Ppatvar s + | Symbol s -> Ppatsym s | Node (c, args) -> Ppatcons (pexp_parse c, List.map pexp_p_pat_arg args) | _ -> let l = sexp_location s in @@ -271,7 +265,7 @@ and pexp_p_pat (s : sexp) : ppat = match s with and pexp_u_pat (p : ppat) : sexp = match p with | Ppatany l -> Symbol (l, "_") - | Ppatvar s -> Symbol s + | Ppatsym s -> Symbol s | Ppatcons (c, args) -> Node (pexp_unparse c, List.map pexp_u_pat_arg args) and pexp_p_decls e: pdecl list = View it on GitLab: https://gitlab.com/monnier/typer/commit/a459a1ea02e2f91d70af6397744438d27d3…

1 0