diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 12:41:26 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/nativelambda.ml | |
parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r-- | kernel/nativelambda.ml | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 297ac6b99..179d8d58b 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -639,26 +639,21 @@ and lambda_of_app env sigma f args = let tag, nparams, arity = Renv.get_construct_info env c in let expected = nparams + arity in let nargs = Array.length args in + let prefix = get_mind_prefix !global_env (fst (fst c)) in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info (!global_env).retroknowledge f args - with NotClosed -> assert false -(* - let rargs = Array.sub args nparams arity in - let b_args = Array.map str_const rargs in - Bspecial ((Retroknowledge.get_vm_constant_dynamic_info - (!global_env).retroknowledge - f), - b_args) - *) + with NotClosed -> + let args = lambda_of_args env sigma nparams args in + Retroknowledge.get_native_constant_dynamic_info + (!global_env).retroknowledge f prefix c args with Not_found -> let args = lambda_of_args env sigma nparams args in makeblock !global_env c tag args else - let prefix = get_mind_prefix !global_env (fst (fst c)) in mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args) | _ -> let f = lambda_of_constr env sigma f in @@ -695,3 +690,17 @@ let lambda_of_constr env sigma c = let mk_lazy c = mkLapp Llazy [|c|] + +(** Retroknowledge, to be removed once we move to primitive machine integers *) +let compile_static_int31 fc args = + if not fc then raise Not_found else + Luint (UintVal + (Uint31.of_int (Array.fold_left + (fun temp_i -> fun t -> match kind_of_term t with + | Construct (_,d) -> 2*temp_i+d-1 + | _ -> raise NotClosed) + 0 args))) + +let compile_dynamic_int31 fc prefix c args = + if not fc then raise Not_found else + Luint (UintDigits (prefix,c,args)) |