diff options
| author | Pierre-Marie Pédrot | 2018-09-19 09:13:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-19 09:13:38 +0200 |
| commit | 44b8c4ec9acad33002b080ed0aefb214124db440 (patch) | |
| tree | 96f950c47701467e0c41fa24a7e21f9524977a0b /kernel/clambda.ml | |
| parent | 98aedc543d31ca89428e9789fd76529a7409b7cb (diff) | |
| parent | 736842d4cde09c667837dee8a633ff98ecf6a820 (diff) | |
Merge PR #8447: Cleaning in the retroknowledge
Diffstat (limited to 'kernel/clambda.ml')
| -rw-r--r-- | kernel/clambda.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/clambda.ml b/kernel/clambda.ml index ff977416df..31dede6f5d 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -661,11 +661,11 @@ let rec lambda_of_constr env c = (* translation of the argument *) let la = lambda_of_constr env a in - let entry = mkInd ind in + let gr = GlobRef.IndRef ind in let la = try Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge - entry la + gr la with Not_found -> la in (* translation of the type *) @@ -723,7 +723,7 @@ and lambda_of_app env f args = (try (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge - (mkConstU (kn,u)) in + (GlobRef.ConstRef kn) in let args = lambda_of_args env 0 args in f args with Not_found -> @@ -736,6 +736,7 @@ and lambda_of_app env f args = | Construct (c,_) -> let tag, nparams, arity = Renv.get_construct_info env c in let nargs = Array.length args in + let gr = GlobRef.ConstructRef c in if Int.equal (nparams + arity) nargs then (* fully applied *) (* spiwack: *) (* 1/ tries to compile the constructor in an optimal way, @@ -750,7 +751,7 @@ and lambda_of_app env f args = try Retroknowledge.get_vm_constant_static_info env.global_env.retroknowledge - f args + gr args with NotClosed -> (* 2/ if the arguments are not all closed (this is expectingly (and it is currently the case) the only @@ -771,7 +772,7 @@ and lambda_of_app env f args = let args = lambda_of_args env nparams rargs in Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f args + gr args with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) @@ -784,7 +785,7 @@ and lambda_of_app env f args = (try (Retroknowledge.get_vm_constant_dynamic_info env.global_env.retroknowledge - f) args + gr) args with Not_found -> if nparams <= nargs then (* got all parameters *) makeblock tag 0 arity args |