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/a707155bbc7c5eeb6bdd6e70adcd07f2ded...