From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/retroknowledge.ml | 189 ++++++++++++++++++++++------------------------- 1 file changed, 87 insertions(+), 102 deletions(-) (limited to 'kernel/retroknowledge.ml') diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index bbb8491e..cc307f14 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* entry]. *) module Proactive = Map.Make (struct type t = field let compare = compare end) type proactive = entry Proactive.t -(* the reactive knowledge is represented as a functionaly map - from the type of terms (actually it is the terms whose outermost - layer is unfolded (typically by Term.kind_of_term)) to the - type reactive_end which is a record containing all the kind of reactive - information needed *) -(* todo: because of the bug with output state, reactive_end should eventually - contain no function. A forseen possibility is to make it a map from - a finite type describing the fields to the field of proactive retroknowledge - (and then to make as many functions as needed in environ.ml) *) +(* The [reactive] knowledge contains the mapping + [entry->field]. Fields are later to be interpreted as a + [reactive_info]. *) + +module EntryOrd = +struct + type t = entry + let compare = Constr.compare +end -module Reactive = - Map.Make (struct type t = entry let compare = compare end) +module Reactive = Map.Make (EntryOrd) -type reactive_end = {(*information required by the compiler of the VM *) +type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : (*fastcomputation flag -> continuation -> result *) (bool->Cbytecodes.comp_env->constr array -> @@ -119,11 +117,27 @@ type reactive_end = {(*information required by the compiler of the VM *) (* fastcomputation flag -> cont -> result *) vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; (* tag (= compiled int for instance) -> result *) - vm_decompile_const : (int -> Term.constr) option} + vm_decompile_const : (int -> Term.constr) option; + + native_compiling : + (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> + Nativeinstr.lambda) option; + + native_constant_static : + (bool -> constr array -> Nativeinstr.lambda) option; + native_constant_dynamic : + (bool -> Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda array -> Nativeinstr.lambda) option; + native_before_match : (bool -> Nativeinstr.prefix -> constructor -> + Nativeinstr.lambda -> Nativeinstr.lambda) option -and reactive = reactive_end Reactive.t +} + + + +and reactive = field Reactive.t and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive} @@ -150,125 +164,96 @@ let initial_retroknowledge = proactive = initial_proactive; reactive = initial_reactive } -let empty_reactive_end = +let empty_reactive_info = { vm_compiling = None ; vm_constant_static = None; vm_constant_dynamic = None; vm_before_match = None; - vm_decompile_const = None } + vm_decompile_const = None; + native_compiling = None; + native_constant_static = None; + native_constant_dynamic = None; + native_before_match = None; + } +(* adds a binding [entry<->field]. *) +let add_field knowledge field entry = + {knowledge with + proactive = Proactive.add field entry knowledge.proactive; + reactive = Reactive.add entry field knowledge.reactive} (* acces functions for proactive retroknowledge *) -let add_field knowledge field value = - {knowledge with proactive = Proactive.add field value knowledge.proactive} - let mem knowledge field = Proactive.mem field knowledge.proactive -let remove knowledge field = - {knowledge with proactive = Proactive.remove field knowledge.proactive} - let find knowledge field = Proactive.find field knowledge.proactive +let (dispatch,dispatch_hook) = Hook.make () - +let dispatch_reactive entry retroknowledge = + Hook.get dispatch retroknowledge entry (Reactive.find entry retroknowledge.reactive) (*access functions for reactive retroknowledge*) (* used for compiling of functions (add, mult, etc..) *) let get_vm_compiling_info knowledge key = - match (Reactive.find key knowledge.reactive).vm_compiling + match (dispatch_reactive key knowledge).vm_compiling with | None -> raise Not_found | Some f -> f knowledge.flags.fastcomputation (* used for compilation of fully applied constructors *) let get_vm_constant_static_info knowledge key = - match (Reactive.find key knowledge.reactive).vm_constant_static + match (dispatch_reactive key knowledge).vm_constant_static with | None -> raise Not_found | Some f -> f knowledge.flags.fastcomputation (* used for compilation of partially applied constructors *) let get_vm_constant_dynamic_info knowledge key = - match (Reactive.find key knowledge.reactive).vm_constant_dynamic + match (dispatch_reactive key knowledge).vm_constant_dynamic with | None -> raise Not_found | Some f -> f knowledge.flags.fastcomputation let get_vm_before_match_info knowledge key = - match (Reactive.find key knowledge.reactive).vm_before_match + match (dispatch_reactive key knowledge).vm_before_match with | None -> raise Not_found | Some f -> f knowledge.flags.fastcomputation let get_vm_decompile_constant_info knowledge key = - match (Reactive.find key knowledge.reactive).vm_decompile_const + match (dispatch_reactive key knowledge).vm_decompile_const with | None -> raise Not_found | Some f -> f +let get_native_compiling_info knowledge key = + match (dispatch_reactive key knowledge).native_compiling + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation +(* used for compilation of fully applied constructors *) +let get_native_constant_static_info knowledge key = + match (dispatch_reactive key knowledge).native_constant_static + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation -(* functions manipulating reactive knowledge *) -let add_vm_compiling_info knowledge value nfo = - {knowledge with reactive = - try - Reactive.add value - {(Reactive.find value (knowledge.reactive)) with vm_compiling = Some nfo} - knowledge.reactive - with Not_found -> - Reactive.add value {empty_reactive_end with vm_compiling = Some nfo} - knowledge.reactive - } - -let add_vm_constant_static_info knowledge value nfo = - {knowledge with reactive = - try - Reactive.add value - {(Reactive.find value (knowledge.reactive)) with vm_constant_static = Some nfo} - knowledge.reactive - with Not_found -> - Reactive.add value {empty_reactive_end with vm_constant_static = Some nfo} - knowledge.reactive - } - -let add_vm_constant_dynamic_info knowledge value nfo = - {knowledge with reactive = - try - Reactive.add value - {(Reactive.find value (knowledge.reactive)) with vm_constant_dynamic = Some nfo} - knowledge.reactive - with Not_found -> - Reactive.add value {empty_reactive_end with vm_constant_dynamic = Some nfo} - knowledge.reactive - } - -let add_vm_before_match_info knowledge value nfo = - {knowledge with reactive = - try - Reactive.add value - {(Reactive.find value (knowledge.reactive)) with vm_before_match = Some nfo} - knowledge.reactive - with Not_found -> - Reactive.add value {empty_reactive_end with vm_before_match = Some nfo} - knowledge.reactive - } - -let add_vm_decompile_constant_info knowledge value nfo = - {knowledge with reactive = - try - Reactive.add value - {(Reactive.find value (knowledge.reactive)) with vm_decompile_const = Some nfo} - knowledge.reactive - with Not_found -> - Reactive.add value {empty_reactive_end with vm_decompile_const = Some nfo} - knowledge.reactive - } +(* used for compilation of partially applied constructors *) +let get_native_constant_dynamic_info knowledge key = + match (dispatch_reactive key knowledge).native_constant_dynamic + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation -let clear_info knowledge value = - {knowledge with reactive = Reactive.remove value knowledge.reactive} +let get_native_before_match_info knowledge key = + match (dispatch_reactive key knowledge).native_before_match + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation -- cgit v1.2.3