diff options
| author | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 17:58:01 +0200 |
| commit | 3599d05a5b3664764f19a794dc69c4e28f2e135d (patch) | |
| tree | ee65c9840649332663491ead6073f1323f4a6fb5 /kernel/clambda.ml | |
| parent | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (diff) | |
| parent | 277563ab74a0529c330343479a063f808baa6db4 (diff) | |
Merge PR #7908: Projections use index representation
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index f1b6f3dffc..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() ++ pr_con 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,10 +708,8 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let pb = lookup_projection p env.global_env in - let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,Projection.constant p,lc) + Lproj (Projection.repr p,lc) and lambda_of_app env f args = match Constr.kind f with |