From 5da0f107cb3332d5cd87fc352aef112f6b74fc97 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Apr 2016 16:31:01 +0200 Subject: Moving Ftactic and Geninterp to the engine folder. --- engine/geninterp.mli | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 engine/geninterp.mli (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli new file mode 100644 index 0000000000..0992db7a29 --- /dev/null +++ b/engine/geninterp.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun + +val generic_interp : (glob_generic_argument, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit -- cgit v1.2.3 From 8ad2627de29639b21473783195905dca6bb1c6ae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 18:33:28 +0200 Subject: Getting rid of the Geninterp.generic_interp function. --- engine/geninterp.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0992db7a29..0e7ed18471 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -21,7 +21,5 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -val generic_interp : (glob_generic_argument, Val.t) interp_fun - val register_interp0 : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit -- cgit v1.2.3 From de4b9b68445d9f3e48da789404cbdfcd89214585 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 Apr 2016 14:39:34 +0200 Subject: Moving the Val module to Geninterp. --- engine/geninterp.mli | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0e7ed18471..3c87b25121 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -11,6 +11,48 @@ open Names open Genarg +(** {6 Dynamic toplevel values} *) + +module Val : +sig + type 'a typ + + val create : string -> 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option + val repr : 'a typ -> string + val pr : 'a typ -> Pp.std_ppcmds + + val list_tag : t list typ + val opt_tag : t option typ + val pair_tag : (t * t) typ + + val inject : 'a tag -> 'a -> t + +end +(** Dynamic types for toplevel values. While the generic types permit to relate + objects at various levels of interpretation, toplevel values are wearing + their own type regardless of where they came from. This allows to use the + same runtime representation for several generic types. *) + +val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag +(** Retrieve the dynamic type associated to a toplevel genarg. *) + +val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit +(** Register the representation of a generic argument. If no tag is given as + argument, a new fresh tag with the same name as the argument is associated + to the generic type. *) + +(** {6 Interpretation functions} *) + module TacStore : Store.S type interp_sign = { -- cgit v1.2.3 From 4740e82e4af6d38e9cc55dfe1a05db87f73bf1e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 15:23:41 +0200 Subject: Removing external uses of Val.inject and making Geninterp.interp return Val.t --- engine/geninterp.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 3c87b25121..c92181027e 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -61,7 +61,7 @@ type interp_sign = { type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t -val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun val register_interp0 : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit -- cgit v1.2.3 From 729d838838d8df06395726477817620e2ae998bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 17:24:58 +0200 Subject: Interpretation function can return any untyped value. --- engine/geninterp.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli index c92181027e..5799862110 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -64,4 +64,4 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun val register_interp0 : - ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit -- cgit v1.2.3 From 8d3f0b614d7b2fb30f6e87b48a4fc5c0d286e49c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 4 May 2016 14:30:48 +0200 Subject: Normalizing the names of dynamic types to follow a typ_* scheme. --- engine/geninterp.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine/geninterp.mli') diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 5799862110..42e1e3784c 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -31,9 +31,9 @@ sig val repr : 'a typ -> string val pr : 'a typ -> Pp.std_ppcmds - val list_tag : t list typ - val opt_tag : t option typ - val pair_tag : (t * t) typ + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ val inject : 'a tag -> 'a -> t -- cgit v1.2.3