Stefan pushed to branch master at Stefan / Typer
Commits: 3fcfd932 by Stefan Monnier at 2018-05-17T17:37:14Z Rewrite ctx2tup
* src/debruijn.ml (lct_view): Only allow LetDef in CVfix. (lctx_view): Adjust accordingly. * src/eval.ml (print_eval_result.from_lctx.from_lctx'): * src/opslexp.ml (lctx_to_subst.s2): Adjust accordingly. (mktup): Remove. (ctx2tup): Rewrite to build a let-nest with a (simpler) tuple inside.
- - - - -
4 changed files:
- src/debruijn.ml - src/eval.ml - src/opslexp.ml - src/util.ml
Changes:
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -338,21 +338,23 @@ let env_lookup_expr ctx (v : vref): lexp option = type lct_view = | CVempty | CVlet of vname option * varbind * ltype * lexp_context - | CVfix of (vname option * varbind * ltype) list * lexp_context + | CVfix of (vname option * lexp * ltype) list * lexp_context
let rec lctx_view lctx = match lctx with | Myers.Mnil -> CVempty | Myers.Mcons ((0, loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx) - | Myers.Mcons ((1, loname, odef, t), lctx, _, _) + | Myers.Mcons ((1, loname, LetDef def, t), lctx, _, _) -> let rec loop i lctx defs = match lctx with - | Myers.Mcons ((o, loname, odef, t), lctx, _, _) + | Myers.Mcons ((o, loname, LetDef def, t), lctx, _, _) when o = i - -> loop (i + 1) lctx ((loname, odef, t) :: defs) + -> loop (i + 1) lctx ((loname, def, t) :: defs) | _ -> CVfix (defs, lctx) in - loop 2 lctx [(loname, odef, t)] + loop 2 lctx [(loname, def, t)] + | Myers.Mcons ((_, _, _, _), _, _, _) + -> U.internal_error "Unexpected recursive non-LetDef!" | _ -> U.internal_error "Unexpected lexp_context shape!"
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2018 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -732,21 +732,16 @@ let from_lctx (lctx: lexp_context): runtime_env = rctx | CVfix (defs, lctx) -> let fvs = List.fold_left - (fun fvs (_, odef, _) - -> match odef with - | LetDef e - -> OL.fv_union fvs (OL.fv (L.clean e)) - | _ -> fvs) + (fun fvs (_, e, _) + -> OL.fv_union fvs (OL.fv (L.clean e))) OL.fv_empty defs in let rctx = from_lctx lctx in let (nrctx, evs, alldefs) - = List.fold_left (fun (rctx, evs, alldefs) (loname, odef, _) + = List.fold_left (fun (rctx, evs, alldefs) (loname, e, _) -> let rc = ref Vundefined in let nrctx = Myers.cons (roname loname, rc) rctx in - match odef with - | LetDef e -> (nrctx, (e, rc)::evs, alldefs) - | _ -> nrctx, [], false) + (nrctx, (e, rc)::evs, alldefs)) (rctx, [], true) defs in let _ = (* FIXME: Evaluate those defs that we can, even if not all defs
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -89,11 +89,8 @@ let rec lctx_to_subst lctx = | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in let s2 = lexp_defs_subst DB.dloc S.identity - (List.map (fun (oname, odef, t) - -> (maybev oname, - (match odef with LetDef e -> e - | _ -> L.impossible), - t)) + (List.map (fun (oname, e, t) + -> (maybev oname, e, t)) (List.rev defs)) in L.scompose s2 s1
@@ -926,40 +923,56 @@ and clean_map cases =
(** Turning a set of declarations into an object. **)
-let mktup types vals = - let loc = DB.dloc in - let cons_name = "cons" in - let cons_label = (loc, cons_name) in - let type_label = (loc, "record") in - Call (Cons (Inductive (loc, type_label, [], - SMap.add cons_name - (List.map (fun (oname, t) - -> (P.Aimplicit, oname, t)) - types) - SMap.empty), - cons_label), - List.map (fun v -> (P.Aimplicit, v)) vals) - let ctx2tup ctx nctx = + U.debug_msg ("Entering ctx2tup\n"); assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); - let rec get_ts_vs nctx types vals = - if nctx == ctx then (types, vals) else + let rec get_blocs nctx blocs = + if nctx == ctx then blocs else match DB.lctx_view nctx with - | DB.CVlet (oname, LetDef e, t, nctx) - -> get_ts_vs nctx ((oname, t) :: types) (e :: vals) - | DB.CVfix (defs, nctx) - -> let rec shift_vs rdefs types vals defs = match rdefs with - | [] -> get_ts_vs nctx types vals - | (oname, LetDef e, t) :: rdefs - -> let name = maybev oname in - let defs = (name, e, t) :: defs in - shift_vs rdefs ((oname, t) :: types) - (Let (DB.dloc, defs, e) :: vals) defs - | _ -> U.internal_error "ctx2tup: Non-letdef in recursive vars" in - shift_vs (List.rev defs) types vals [] + | DB.CVlet (_, _, _, nctx) as bloc -> get_blocs nctx (bloc :: blocs) + | DB.CVfix (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) | _ -> assert false in - let (types, vals) = get_ts_vs nctx [] [] in - mktup types vals + let rec mk_lets_and_tup blocs types = + let loc = U.dummy_location in + match blocs with + | [] + -> let cons_name = "cons" in + let cons_label = (loc, cons_name) in + let type_label = (loc, "record") in + let offset = List.length types in + let types = List.rev types in + U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n"); + Call (Cons (Inductive (loc, type_label, [], + SMap.add cons_name + (List.map (fun (oname, t) + -> (P.Aimplicit, oname, + (* FIXME: We need to shift + * for references outside + * of the blocs, but for + * references within the blocs, + * this means we refer to the + * let-binding i.s.o the tuple + * field (which would be both + * equivalent and preferable). *) + mkSusp t (S.shift offset))) + types) + SMap.empty), + cons_label), + List.map (fun (oname, t) + -> (P.Aimplicit, Var (maybev oname, offset))) + types) + | (DB.CVlet (oname, LetDef e, t, _) :: blocs) + -> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)], + mk_lets_and_tup blocs ((oname, t) :: types)) + | (DB.CVfix (defs, _) :: blocs) + -> Let (loc, List.map (fun (oname, e, t) -> (maybev oname, e, t)) defs, + mk_lets_and_tup blocs (List.append + (List.rev + (List.map (fun (oname, _, t) + -> (oname, t)) + defs)) + types)) in + mk_lets_and_tup (get_blocs nctx []) []
(* opslexp.ml ends here. *)
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -86,7 +86,7 @@ let msg_info = msg_message 3 "Info:"
(* Compiler Internal Debug print *) let debug_msg expr = - if 4 <= !_typer_verbose then expr else () + if 4 <= !_typer_verbose then (print_string expr; flush stdout) else ()
let not_implemented_error () = internal_error "not implemented"
View it on GitLab: https://gitlab.com/monnier/typer/commit/3fcfd932c135d1d6834b2d68968a6207d6a3...
Afficher les réponses par date