Stefan pushed to branch master at Stefan / Typer
Commits: 183cf9cd by Stefan Monnier at 2016-11-24T10:45:13-05:00 * src/lparse.ml (_lexp_expr_str): Typecheck the expressions
* src/debug.ml (debug_pexp_print): Use pexp_name.
* src/lexp.ml (push_susp.): Fix longstanding typo.
* src/lparse.ml (default_rctx): Use from_lctx. (_lexp_expr_str): Typecheck the expressions.
- - - - -
4 changed files:
- src/debug.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml
Changes:
===================================== src/debug.ml ===================================== --- a/src/debug.ml +++ b/src/debug.ml @@ -120,19 +120,7 @@ let debug_pexp_print ptop = loc_print loc; print_string "]\t"; pexp_print pex in - match ptop with - | Pimm _ -> print_info "Pimm " l ptop - | Pvar (_,_) -> print_info "Pvar " l ptop - | Phastype (_,_,_) -> print_info "Phastype " l ptop - | Pmetavar (_, _) -> print_info "Pmetavar " l ptop - | Plet (_, _, _) -> print_info "Plet " l ptop - | Parrow (_, _, _, _, _) -> print_info "Parrow " l ptop - | Plambda (_,_, _, _) -> print_info "Plambda " l ptop - | Pcall (_, _) -> print_info "Pcall " l ptop - | Pinductive (_, _, _) -> print_info "Pinductive " l ptop - | Pcons (_,_) -> print_info "Pcons " l ptop - | Pcase (_, _, _) -> print_info "Pcase " l ptop - (*| _ -> print_info "Not Impl " l ptop *) + print_info (pexp_name ptop) l ptop
let debug_pexp_decls decls = let loc_print l = print_string "["; loc_print l; print_string "] " in
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -219,7 +219,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> 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, mkSusp e s', mkSusp ty s) :: ndefs)) + (v, mkSusp def s', mkSusp ty s) :: ndefs)) (s, []) defs in mkLet (l, ndefs, mkSusp e s') | Arrow (ak, v, t1, l, t2)
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -1160,9 +1160,7 @@ let default_lctx, default_rctx = with e -> warning dloc "Predef not found"; lctx in - let rctx = make_runtime_ctx in - let rctx = eval_decls_toplevel (List.map OL.clean_decls d) rctx in - lctx, rctx + lctx, from_lctx lctx
(* String Parsing * --------------------------------------------------------- *) @@ -1170,8 +1168,13 @@ let default_lctx, default_rctx = (* Lexp helper *) let _lexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) (ctx: elab_context) = - let pxps = _pexp_expr_str str tenv grm limit in - lexp_parse_all pxps ctx + let pxps = _pexp_expr_str str tenv grm limit in + let lexps = lexp_parse_all pxps ctx in + let meta_ctx, _ = !global_substitution in + List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx ctx) lxp)) + lexps; + lexps +
(* specialized version *) let lexp_expr_str str lctx =
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -54,7 +54,7 @@ let lookup_value = DB.lctx_lookup_value * * (x₁ = e1; x₂ = e₂) * - * Where x₁ will be DeBuijn #1 and x₂ will be DeBruijn #0, + * Where x₁ will be DeBruijn #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
View it on GitLab: https://gitlab.com/monnier/typer/commit/183cf9cdd3fadc0d8fc5aece95420f4a3a75...