Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: d84820f3 by Jonathan Graveline at 2018-05-17T22:07:55Z
From master
- - - - -
1 changed file:
- src/debruijn.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!"
View it on GitLab: https://gitlab.com/monnier/typer/commit/d84820f3637291c50fb2dca71af252148aac...
Afficher les réponses par date