Stefan pushed to branch master at Stefan / Typer
Commits: c5c90c6f by Stefan Monnier at 2016-12-06T22:57:47-05:00 Fix types with multiple args; refine closedness test
* GNUmakefile (OBFLAGS): Use `-tag`.
* btl/builtins.typer (expand_dmacro_): Remove redundant explicit args. (sexp_dispatch_): Name the arguments.
* emacs/typer-mode.el (typer-smie-rules): Tweak rule for `=`.
* src/eval.ml (not_closed): Rename from closed_dbset_p. Return a list. (from_lctx): Add `meta_ctx` arg. `clean` exps before passing to `fv`.
* src/lexp.ml (push_susp) <Inductive>: Don't reverse type's args. <Case>: Don't skip unnamed fields. (clean) <Let>: Fix up typo. <Inductive>: Don't reverse type's args. <Case>: Don't skip unnamed fields.
* src/lparse.ml (check_case.add_branch): Substitution was built in the wrong order. (lexp_expand_macro_): Check closeness of the macro definition.
- - - - -
6 changed files:
- GNUmakefile - btl/builtins.typer - emacs/typer-mode.el - src/eval.ml - src/lexp.ml - src/lparse.ml
Changes:
===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)
-OBFLAGS = -lflags -g -cflags -g -build-dir $(BUILDDIR) +OBFLAGS = -tag debug -tag profile -build-dir $(BUILDDIR) # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -147,19 +147,20 @@ expand_dmacro_ : Macro -> List Sexp -> List Sexp; expand_dmacro_ m args = case m | DMacro_ f => (f args) % Wrap a Macro in a list of Sexp if Macro_ is used - | Macro_ f => cons (a := Sexp) (f args) (nil (a := Sexp)); + | Macro_ f => cons (f args) nil;
sexp_dispatch_ = Built-in "sexp_dispatch_" ( - (a : Type) ≡> - Sexp - -> (Sexp -> List Sexp -> a) - -> (String -> a) - -> (String -> a) - -> (Int -> a) - -> (Float -> a) - -> (List Sexp -> a) - -> a - ); + (a : Type) ≡> + Sexp + -> (node : Sexp -> List Sexp -> a) + -> (symbol : String -> a) + -> (string : String -> a) + -> (int : Int -> a) + -> (float : Float -> a) + -> (block : List Sexp -> a) + -> a + ); +
% ----------------------------------------------------- % Monads
===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -157,6 +157,7 @@ ;; along the lines of what's done in Tuareg. (pcase (cons kind token) (`(:before . "|") (smie-rule-parent)) + (`(:after . "=") 2) ))
;;;###autoload
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -623,28 +623,30 @@ module CMap (struct type t = lexp_context let hash = Hashtbl.hash let equal = (==) end) let ctx_memo = CMap.create 1000
-let closed_dbset_p rctx ((o, vm) : DB.set) = - VMap.for_all (fun i () -> let (_, rc) = Myers.nth (i + o) rctx in - match !rc with Vundefined -> false | _ -> true) - vm +let not_closed rctx ((o, vm) : DB.set) = + VMap.fold (fun i () nc -> let (_, rc) = Myers.nth (i + o) rctx in + match !rc with Vundefined -> (i+o)::nc | _ -> nc) + vm []
let closed_p rctx (fvs, mvs) = - closed_dbset_p rctx fvs + not_closed rctx fvs = [] (* FIXME: Handle metavars! *) && VMap.is_empty mvs
-let rec from_lctx (lctx: lexp_context): runtime_env = +let rec from_lctx meta_ctx (lctx: lexp_context): runtime_env = (* FIXME: `eval` with a disabled runIO. *) let from_lctx' (lctx: lexp_context): runtime_env = match lctx with | Myers.Mnil -> Myers.nil | Myers.Mcons ((0, loname, def, _), lctx, _, _) - -> let rctx = from_lctx lctx in + -> let rctx = from_lctx meta_ctx lctx in Myers.cons (roname loname, ref (match def with | LetDef e - when closed_p rctx (OL.fv e) - -> eval (OL.erase_type e) rctx + -> let e = L.clean meta_ctx e in + if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined | _ -> Vundefined)) rctx | Myers.Mcons ((1, loname, LetDef e, _), lctx, _, _) @@ -652,11 +654,12 @@ let rec from_lctx (lctx: lexp_context): runtime_env = match lctx with | Myers.Mcons ((o, loname, LetDef e, _), lctx, _, _) when o = i - -> getdefs (i + 1) lctx ((loname, e) :: rdefs) + -> let e = L.clean meta_ctx e in + getdefs (i + 1) lctx ((loname, e) :: rdefs) (OL.fv_union fvs (OL.fv e)) | _ -> (lctx, rdefs, fvs) in let (lctx, rdefs, fvs) = getdefs 2 lctx [(loname, e)] OL.fv_empty in - let rctx = from_lctx lctx in + let rctx = from_lctx meta_ctx lctx in let (nrctx, evs) = List.fold_left (fun (rctx, evs) (loname, e) -> let rc = ref Vundefined in @@ -677,5 +680,5 @@ let rec from_lctx (lctx: lexp_context): runtime_env = r
(* build a rctx from a ectx. *) -let from_ectx (ctx: elab_context): runtime_env = - from_lctx (ectx_to_lctx ctx) +let from_ectx meta_ctx (ctx: elab_context): runtime_env = + from_lctx meta_ctx (ectx_to_lctx ctx)
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -243,6 +243,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) (s, []) args in + let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -257,11 +258,9 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e) - -> let s' = L.fold_left (fun s carg - -> match carg with - | (_,None) -> s - | (_,Some v) -> ssink v s) - s cargs in + -> let s' = L.fold_left + (fun s (_,ov) -> ssink (maybev ov) s) + s cargs in (l, cargs, mkSusp e s')) cases, match default with @@ -296,7 +295,7 @@ let clean meta_ctx e = -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) -> (ssink v s, - (v, clean s' e, clean s ty) :: ndefs)) + (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in mkLet (l, ndefs, clean s' e) | Arrow (ak, v, t1, l, t2) @@ -308,6 +307,7 @@ let clean meta_ctx e = -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, (ak, v, clean s t) :: nargs)) (s, []) args in + let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -322,11 +322,9 @@ let clean meta_ctx e = | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) - -> let s' = L.fold_left (fun s carg - -> match carg with - | (_,None) -> s - | (_,Some v) -> ssink v s) - s cargs in + -> let s' = L.fold_left + (fun s (_,ov) -> ssink (maybev ov) s) + s cargs in (l, cargs, clean s' e)) cases, match default with
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -578,8 +578,8 @@ and check_case rtype (loc, target, ppatterns) ctx = ^ cons_name ^ "` constructor"); [] in
- let subst = List.fold_right (fun (_, t) s -> S.cons t s) - targs S.identity in + let subst = List.fold_left (fun s (_, t) -> S.cons t s) + S.identity targs in let rec make_nctx ctx (* elab context. *) s (* Pending substitution. *) pargs (* Pattern arguments. *) @@ -830,8 +830,21 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type =
(* FIXME: Don't `mkCall + eval` but use eval_call instead! *) let macro = mkCall (macro_expand, args) in + let meta_ctx, _ = !global_substitution in + let macro = L.clean meta_ctx macro in let emacro = OL.erase_type macro in - let rctx = EV.from_ectx ctx in + let rctx = EV.from_ectx meta_ctx ctx in + + if not (EV.closed_p rctx (OL.fv macro)) then + (let (fvs, _) = OL.fv macro in + let nc = EV.not_closed rctx fvs in + lexp_error (lexp_location macro_funct) macro_funct + ("Macro function is not closed: " + ^ String.concat + " " (List.map (fun i -> match Myers.nth i rctx with + | (Some n,_) -> n + | _ -> "<anon>") + nc)));
(* eval macro *) let vxp = try EV._eval emacro rctx ([], []) @@ -1182,7 +1195,7 @@ let default_ectx lctx in lctx
-let default_rctx = EV.from_ectx default_ectx +let default_rctx = EV.from_ectx VMap.empty default_ectx
(* String Parsing * --------------------------------------------------------- *)
View it on GitLab: https://gitlab.com/monnier/typer/commit/c5c90c6f6b568bf46429edc49b7480fbd592...