diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 02:56:14 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 03:01:58 +0100 |
commit | 820a282fde5cb4233116ce2cda927fda2f36097d (patch) | |
tree | 9893efb3b59d836a61b09853a0c94ba798e9c0b2 /lib/genarg.ml | |
parent | d3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e (diff) |
Moving val_cast to Tacinterp.
Diffstat (limited to 'lib/genarg.ml')
-rw-r--r-- | lib/genarg.ml | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 58d83ce7a..37b31a511 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -285,50 +285,7 @@ let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function | ExtraArg s -> match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn -exception CastError of argument_type * Val.t - -let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> None - | Some Refl -> Some x - -let try_prj wit v = match prj (val_tag wit) v with -| None -> raise (CastError (untype wit, v)) -| Some x -> x - -let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c = -fun wit v -> match wit with -| ExtraArg _ -> try_prj wit v -| ListArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.List tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - List.map map v - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end -| OptArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Opt tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - Option.map map v - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end -| PairArg (t1, t2) -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Pair (tag1, tag2) -> - let (v1, v2) = v in - let v1 = Val.Dyn (tag1, v1) in - let v2 = Val.Dyn (tag2, v2) in - (val_cast t1 v1, val_cast t2 v2) - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end - let val_tag = function Topwit t -> val_tag t -let val_cast = function Topwit t -> val_cast t (** Registering genarg-manipulating functions *) |