Stefan pushed to branch master at Stefan / Typer
Commits: 79d18902 by Stefan Monnier at 2016-11-23T23:24:09-05:00 Typecheck non-recursive Plet, as well as interactive exps
* src/REPL.ml (ilexp_parse): Check exps before running them.
* src/inverse_subst.ml (impossible): Move to lexp.ml.
* src/lexp.ml (impossible): Move from inverse_subst.ml. (push_susp): Fix the "plain" Builtin, along the line of the recent fix for the attributemap case.
* src/builtin.ml (declexpr_impl, decltype_impl): Only return a lexp, not its type.
* src/lparse.ml (elab_check_sort, elab_check_def): Add some debug prints. (infer_call): Compute the type of get_macro_impl's returned lexps. (lexp_decls_1): Typecheck non-recursive let-bindings. (is_builtin_macro): Use SMap.mem. (new_attribute_impl, add_attribute_impl, get_attribute_impl) (has_attribute_impl): Only return a lexp, not its type.
* src/opslexp.ml (check): Fix return type of `Let`. Fix scoping of the computed type of `Arrow`. Fix DB indices of the return type of `Cons`.
- - - - -
6 changed files:
- src/REPL.ml - src/builtin.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -131,7 +131,10 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in let ldecls, lctx = lexp_p_decls pdecls lctx in let lexprs = lexp_parse_all pexprs lctx in - (ldecls, lexprs), lctx + let meta_ctx, _ = !global_substitution in + List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx lctx) lxp)) + lexprs; + (ldecls, lexprs), lctx
let ieval lexps rctx = let (ldecls, lexprs) = lexps in
===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -167,7 +167,7 @@ let declexpr_impl loc largs ctx ftype = | None -> error loc "no expr available" in (* ltp and ftype should be the same let ltp = env_lookup_type ctx ((loc, vn), vi) in *) - lxp, ftype + lxp
let decltype_impl loc largs ctx ftype = @@ -178,7 +178,7 @@ let decltype_impl loc largs ctx ftype =
let ltype = DB.env_lookup_type ctx ((loc, vn), vi) in (* mkSusp prop (S.shift (var_i + 1)) *) - ltype, type0 + ltype
===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -84,7 +84,6 @@ let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; Var((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) -let impossible = Imm Sexp.Epsilon
(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables.
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -124,6 +124,7 @@ module VMap = Map.Make (struct type t = int let compare = compare end) type meta_subst = lexp VMap.t type constraints = (lexp * lexp) list let empty_meta_subst = VMap.empty +let impossible = Imm Sexp.Epsilon
let builtin_size = ref 0
@@ -208,11 +209,12 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e - | Builtin (l, ltp, Some table) - -> let table' = AttributeMap.map (fun lxp -> mkSusp lxp s) table in - mkBuiltin (l, (mkSusp ltp s), Some table') + | Builtin (l, ltp, otable) + -> let otable' = match otable with + | Some table -> Some (AttributeMap.map (fun lxp -> mkSusp lxp s) table) + | _ -> None in + mkBuiltin (l, (mkSusp ltp s), otable')
- | Builtin _ -> e | Let (l, defs, 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)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -94,7 +94,12 @@ let global_substitution = ref (empty_meta_subst, [])
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 + match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx + with e -> + print_string "Exception during whnf of "; + lexp_print lsort; + print_string "\n"; + raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let lexp_string e = lexp_string (L.clean meta_ctx e) in let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in @@ -133,13 +138,24 @@ let elab_check_def (ctx : elab_context) var lxp ltype = lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - if OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' then + if (try OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' + with e + -> print_string ("Exception while conversion-checking types:\n"); + lexp_print ltype; + print_string (" and "); + lexp_print ltype'; + print_string ("\n"); + lexp_error loc lxp + ("Exception while conversion-checking types " + ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); + raise e) + then 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; " because"; - lexp_string (OL.check meta_ctx lctx lxp) ^ " != " ^ lexp_string ltype]) + lexp_string ltype' ^ " != " ^ lexp_string ltype])
let ctx_extend (ctx: elab_context) (var : vdef option) def ltype = elab_check_proper_type ctx ltype var; @@ -709,11 +725,21 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = (* Aimplicit, FIXME: use a meta var if a default macro is not provided *) | sarg :: sargs, Arrow (Aimplicit, v, arg_type, _, ret_type) -> ((* get default attribute *) + (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in let default = Var((dloc, pname), pidx) in
(* lookup default attribute of ltp *) - let attr, attr_type = get_attribute_impl loc [default; arg_type] ctx arg_type in + let attr = get_attribute_impl loc [default; arg_type] ctx arg_type in + (* FIXME: The `default` attribute table shouldn't contain elements of + * type `Macro` but elements of type `something -> Sexp`. + * The point of the `Macro` type is to be able to distinguish + * a macro call from a function call, but here, we have no need + * to distinguish two cases. + * Better yet: let's not do any table lookup here. Instead, + * call a `default-arg-filler` function, implemented in Typer, + * just like `expand_macro_` function. That one can then look + * things up in a table and/or do anything else it wants. *) let v = lexp_expand_macro attr [] ctx in
(* get the sexp returned by the macro *) @@ -796,7 +822,11 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = | Pvar(l, name) when is_builtin_macro name -> let pargs = List.map pexp_parse sargs in let largs = lexp_parse_all pargs ctx in - (get_macro_impl loc name) loc largs ctx ltp + let e = (get_macro_impl loc name) loc largs ctx ltp in + let meta_ctx, _ = !global_substitution in + (* FIXME: We don't actually need to typecheck `e`, we just need + * to find its type. *) + (e, OL.check meta_ctx (ectx_to_lctx ctx) e)
(* true macro *) | _ -> handle_macro_call ()) @@ -936,8 +966,8 @@ and lexp_decls_1 let (lexp, ltp) = infer pexp nctx in (* Lexp decls are always recursive, so we have to shift by 1 to account * for the extra var (ourselves). *) - [(v, push_susp lexp (S.shift 1), ltp)], pdecls, - env_extend nctx v (LetDef lexp) ltp + [(v, mkSusp lexp (S.shift 1), ltp)], pdecls, + ctx_define nctx v lexp ltp
| Pexpr ((l, vname) as v, pexp) :: pdecls -> (try let (_, ltp) = SMap.find vname pending_decls in @@ -1012,8 +1042,7 @@ and get_macro_impl loc name = with Not_found -> fatal loc ("Builtin macro" ^ name ^ " not found")
and is_builtin_macro name = - try let _ = SMap.find name (make_macro_map ()) in true - with Not_found -> false + SMap.mem name (make_macro_map ())
(* -------------------------------------------------------------------------- * Special form implementation @@ -1023,8 +1052,7 @@ and new_attribute_impl loc largs ctx ftype = | [ltp] -> ltp | _ -> fatal loc "new-attribute expects a single Type argument" in
- let attr_table_type = get_predef "Attribute" ctx in - Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty), attr_table_type + Builtin ((loc, "new-attribute"), ltp, Some AttributeMap.empty)
and add_attribute_impl loc largs ctx ftype = let meta_ctx, _ = !global_substitution in @@ -1038,9 +1066,8 @@ and add_attribute_impl loc largs ctx ftype = | _ -> fatal loc "add-attribute expects a table as first argument" in
(* FIXME: Type check (attr: type == attr_type) *) - let attr_table_type = get_predef "Attribute" ctx in let table = AttributeMap.add var attr map in - Builtin ((loc, "add-attribute"), attr_type, Some table), attr_table_type + Builtin ((loc, "add-attribute"), attr_type, Some table)
and get_attribute_impl loc largs ctx ftype = let meta_ctx, _ = !global_substitution in @@ -1049,12 +1076,12 @@ and get_attribute_impl loc largs ctx ftype = | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in
- let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with - | Builtin (_, attr_type, Some map) -> map, attr_type + let map = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + | Builtin (_, attr_type, Some map) -> map | _ -> fatal loc "get-attribute expects a table as first argument" in
let lxp = AttributeMap.find var map in - lxp, attr_type + (lxp : lexp)
and has_attribute_impl loc largs ctx ftype = let meta_ctx, _ = !global_substitution in @@ -1068,9 +1095,9 @@ and has_attribute_impl loc largs ctx ftype = | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in
try let _ = AttributeMap.find var map in - (get_predef "True" ctx), (get_predef "Bool" ctx) + (get_predef "True" ctx) with Not_found -> - (get_predef "False" ctx), (get_predef "Bool" ctx) + (get_predef "False" ctx)
(* Only print var info *) and lexp_print_var_info ctx =
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -293,7 +293,7 @@ let rec check meta_ctx ctx e = (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v | Susp (e, s) -> check ctx (push_susp e s) - | Let (_, defs, e) + | Let (l, defs, e) -> let tmp_ctx = List.fold_left (fun ctx (v, e, t) -> (match lexp_whnf (check ctx t) ctx meta_ctx with @@ -309,12 +309,16 @@ let rec check meta_ctx ctx e = n - 1) (List.length defs) defs in let new_ctx = DB.lctx_extend_rec ctx defs in - check new_ctx e + mkSusp (check new_ctx e) + (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, l, t2) -> (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 meta_ctx, lexp_whnf k2 nctx meta_ctx with + (* BEWARE! `k2` can refer to `v`, but this should only happen + * if `v` is a TypeLevel, and in that case sort_compose + * should ignore `k2` and return TypeOmega anyway. *) + let k2 = mkSusp (check nctx t2) (S.substitute impossible) in + match lexp_whnf k1 ctx meta_ctx, lexp_whnf k2 ctx meta_ctx with | (Sort (_, s1), Sort (_, s2)) -> if ak == P.Aerasable && impredicative_erase then k2 else Sort (l, sort_compose l s1 s2) @@ -450,13 +454,13 @@ let rec check meta_ctx ctx e = | [] -> [] | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) :: indtype fargs (start_index - 1) in - let rec fieldargs fieldtypes = - match fieldtypes with - | [] -> Call (it, indtype fargs (List.length fieldtypes - + List.length fargs - 1)) - | (ak, vd, ftype) :: fieldtypes + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes + List.length fargs in + Call (mkSusp t (S.shift nargs), indtype fargs (nargs - 1)) + | (ak, vd, ftype) :: ftypes -> Arrow (ak, vd, ftype, lexp_location ftype, - fieldargs fieldtypes) in + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes
View it on GitLab: https://gitlab.com/monnier/typer/commit/79d189021f8517b38e6f0c2f94712a0efec3...
Afficher les réponses par date