diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-18 14:39:34 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:47:12 +0200 |
commit | de4b9b68445d9f3e48da789404cbdfcd89214585 (patch) | |
tree | aa383a63227fd77df70b8cc5c374ca7f08334ccf /engine | |
parent | d2f0db714bd2d393423cf2dcb4ed37913029e052 (diff) |
Moving the Val module to Geninterp.
Diffstat (limited to 'engine')
-rw-r--r-- | engine/geninterp.ml | 67 | ||||
-rw-r--r-- | engine/geninterp.mli | 42 |
2 files changed, 109 insertions, 0 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml index be4011cb6..9e866f0cf 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -11,6 +11,73 @@ open Genarg module TacStore = Store.Make(struct end) +(** Dynamic toplevel values *) + +module ValT = Dyn.Make(struct end) + +module Val = +struct + + type 'a typ = 'a ValT.tag + + 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 + + let eq = ValT.eq + let repr = ValT.repr + let create = ValT.create + + let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t) + + let list_tag = ValT.create "list" + let opt_tag = ValT.create "option" + let pair_tag = ValT.create "pair" + + let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with + | Base t -> Dyn (t, x) + | List tag -> Dyn (list_tag, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x))) + +end + +module ValReprObj = +struct + type ('raw, 'glb, 'top) obj = 'top Val.tag + let name = "valrepr" + let default _ = None +end + +module ValRepr = Register(ValReprObj) + +let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function +| ListArg t -> Val.List (val_tag t) +| OptArg t -> Val.Opt (val_tag t) +| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) +| ExtraArg s -> ValRepr.obj (ExtraArg s) + +let val_tag = function Topwit t -> val_tag t + +let register_val0 wit tag = + let tag = match tag with + | None -> + let name = match wit with + | ExtraArg s -> ArgT.repr s + | _ -> assert false + in + Val.Base (Val.create name) + | Some tag -> tag + in + ValRepr.register0 wit tag + +(** Interpretation functions *) + type interp_sign = { lfun : Val.t Id.Map.t; extra : TacStore.t } diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0e7ed1847..3c87b2512 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 = { |