diff options
| author | Gaëtan Gilbert | 2018-07-10 15:25:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:18 +0200 |
| commit | 076bb351257dfd3c605c010d95484f224bef5e56 (patch) | |
| tree | a03ae69145ed806d4c97ca9de7d3b560b34b6478 /kernel/clambda.ml | |
| parent | d03deb978a6747a9fb6ce33cb6ed5063d36c7b42 (diff) | |
VM: don't duplicate projection narg information in lproj/kproj
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index d2f59c432b..7c00e40fb0 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -111,9 +111,9 @@ let rec pp_lam lam = (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ str")") - | Lproj(i,kn,arg) -> + | Lproj(p,arg) -> hov 1 - (str "(proj#" ++ int i ++ spc() ++ Projection.Repr.print kn ++ str "(" ++ pp_lam arg + (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg ++ str ")") | Luint _ -> str "(uint)" @@ -205,9 +205,9 @@ let rec map_lam_with_binders g f n lam = | Lprim(kn,ar,op,args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Lprim(kn,ar,op,args') - | Lproj(i,kn,arg) -> + | Lproj(p,arg) -> let arg' = f n arg in - if arg == arg' then lam else Lproj(i,kn,arg') + if arg == arg' then lam else Lproj(p,arg') | Luint u -> let u' = map_uint g f n u in if u == u' then lam else Luint u' @@ -376,7 +376,7 @@ let rec occurrence k kind lam = let kind = occurrence_args k kind ltypes in let _ = occurrence_args (k+Array.length ids) false lbodies in kind - | Lproj(_,_,arg) -> + | Lproj(_,arg) -> occurrence k kind arg | Luint u -> occurrence_uint k kind u @@ -708,9 +708,8 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let n = Projection.arg p in let lc = lambda_of_constr env c in - Lproj (n,Projection.repr p,lc) + Lproj (Projection.repr p,lc) and lambda_of_app env f args = match Constr.kind f with |