diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 21:04:00 +0000 |
commit | bd7da353ea503423206e329af7a56174cb39f435 (patch) | |
tree | 275cce39ed6fb899660155a43ab0987c4f83025b /interp | |
parent | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (diff) |
Splitted up Genarg in four different levels:
1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.
The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/genarg.ml | 292 | ||||
-rw-r--r-- | interp/genarg.mli | 316 | ||||
-rw-r--r-- | interp/genintern.ml | 82 | ||||
-rw-r--r-- | interp/genintern.mli | 43 | ||||
-rw-r--r-- | interp/interp.mllib | 4 | ||||
-rw-r--r-- | interp/stdarg.ml | 36 |
6 files changed, 136 insertions, 637 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml deleted file mode 100644 index c0526d508..000000000 --- a/interp/genarg.ml +++ /dev/null @@ -1,292 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Util -open Names - -type argument_type = - (* Basic types *) - | IntOrVarArgType - | IntroPatternArgType - | IdentArgType of bool - | VarArgType - | RefArgType - (* Specific types *) - | GenArgType - | SortArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType of bool - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | List0ArgType of argument_type - | List1ArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string - -let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| IntOrVarArgType, IntOrVarArgType -> true -| IntroPatternArgType, IntroPatternArgType -> true -| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 -| VarArgType, VarArgType -> true -| RefArgType, RefArgType -> true -| GenArgType, GenArgType -> true -| SortArgType, SortArgType -> true -| ConstrArgType, ConstrArgType -> true -| ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true -| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2 -| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2 -| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 -| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> - argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r -| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 -| _ -> false - -type ('raw, 'glob, 'top) genarg_type = argument_type - -type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type -(** Alias for concision *) - -(* Dynamics but tagged by a type expression *) - -type rlevel -type glevel -type tlevel - -type 'a generic_argument = argument_type * Obj.t -type raw_generic_argument = rlevel generic_argument -type glob_generic_argument = glevel generic_argument -type typed_generic_argument = tlevel generic_argument - -let rawwit t = t -let glbwit t = t -let topwit t = t - -let wit_list0 t = List0ArgType t - -let wit_list1 t = List1ArgType t - -let wit_opt t = OptArgType t - -let wit_pair t1 t2 = PairArgType (t1,t2) - -let in_gen t o = (t,Obj.repr o) -let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen" -let genarg_tag (s,_) = s - -let fold_list0 f = function - | (List0ArgType t, l) -> - List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) - | _ -> failwith "Genarg: not a list0" - -let fold_list1 f = function - | (List1ArgType t, l) -> - List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) - | _ -> failwith "Genarg: not a list1" - -let fold_opt f a = function - | (OptArgType t, l) -> - (match Obj.magic l with - | None -> a - | Some x -> f (in_gen t x)) - | _ -> failwith "Genarg: not a opt" - -let fold_pair f = function - | (PairArgType (t1,t2), l) -> - let (x1,x2) = Obj.magic l in - f (in_gen t1 x1) (in_gen t2 x2) - | _ -> failwith "Genarg: not a pair" - -let app_list0 f = function - | (List0ArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not a list0" - -let app_list1 f = function - | (List1ArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not a list1" - -let app_opt f = function - | (OptArgType t as u, l) -> - let o = Obj.magic l in - (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o)) - | _ -> failwith "Genarg: not an opt" - -let app_pair f1 f2 = function - | (PairArgType (t1,t2) as u, l) -> - let (o1,o2) = Obj.magic l in - let o1 = out_gen t1 (f1 (in_gen t1 o1)) in - let o2 = out_gen t2 (f2 (in_gen t2 o2)) in - (u, Obj.repr (o1,o2)) - | _ -> failwith "Genarg: not a pair" - -let has_type (t, v) u = argument_type_eq t u - -let unquote x = x - -type an_arg_of_this_type = Obj.t - -let in_generic t x = (t, Obj.repr x) - -type ('a,'b) abstract_argument_type = argument_type -type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type -type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type - -(** New interface for genargs. *) - -type glob_sign = { - ltacvars : Id.t list * Id.t list; - ltacrecvars : (Id.t * Nametab.ltac_constant) list; - gsigma : Evd.evar_map; - genv : Environ.env } - -module TacStore = Store.Make(struct end) - -type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; - extra : TacStore.t } - -type ('raw, 'glb, 'top) arg0 = { - arg0_rprint : 'raw -> std_ppcmds; - arg0_gprint : 'glb -> std_ppcmds; - arg0_tprint : 'top -> std_ppcmds; - arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb; - arg0_subst : Mod_subst.substitution -> 'glb -> 'glb; - arg0_interp : interp_sign -> - Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top; -} - -let default_arg0 name = { - arg0_rprint = (fun _ -> str "<abstract>"); - arg0_gprint = (fun _ -> str "<abstract>"); - arg0_tprint = (fun _ -> str "<abstract>"); - arg0_glob = (fun _ _ -> failwith ("undefined globalizer for " ^ name)); - arg0_subst = (fun _ _ -> failwith ("undefined substitutor for " ^ name)); - arg0_interp = (fun _ _ _ -> failwith ("undefined interpreter for " ^ name)); -} - -let default_uniform_arg0 name = { - arg0_rprint = (fun _ -> str "<abstract>"); - arg0_gprint = (fun _ -> str "<abstract>"); - arg0_tprint = (fun _ -> str "<abstract>"); - arg0_glob = (fun ist x -> (ist, x)); - arg0_subst = (fun _ x -> x); - arg0_interp = (fun _ gl x -> (gl.Evd.sigma, x)); -} - -let arg0_map = ref (String.Map.empty : (Obj.t * Obj.t option) String.Map.t) -(** First component is the argument itself, second is the default raw - inhabitant. *) - -let make0 def name arg = - let () = - if String.Map.mem name !arg0_map then - Errors.anomaly (str "Genarg " ++ str name ++ str " already defined") - in - let arg = Obj.repr arg in - let def = Obj.magic def in - let () = arg0_map := String.Map.add name (arg, def) !arg0_map in - ExtraArgType name - -let get_obj name = - let (obj, _) = String.Map.find name !arg0_map in - (Obj.obj obj : (Obj.t, Obj.t, Obj.t) arg0) - -(** For now, the following functions are quite dummy and should only be applied - to an extra argument type, otherwise, they will badly fail. *) - -let arg_gen = function -| ExtraArgType name -> Obj.magic (get_obj name) -| _ -> assert false - -let rec raw_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_rprint v -| _ -> assert false (* TODO *) - -let rec glb_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_gprint v -| _ -> assert false (* TODO *) - -let rec top_print (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - obj.arg0_rprint v -| _ -> assert false (* TODO *) - -let rec globalize ist (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - let (ist, ans) = obj.arg0_glob ist v in - (ist, (tpe, ans)) -| _ -> assert false (* TODO *) - -let rec substitute subst (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - (tpe, obj.arg0_subst subst v) -| _ -> assert false (* TODO *) - -let rec interpret ist gl (tpe, v) = match tpe with -| ExtraArgType name -> - let obj = get_obj name in - let (ist, ans) = obj.arg0_interp ist gl v in - (ist, (tpe, ans)) -| _ -> assert false (* TODO *) - -(** Compatibility layer *) - -let create_arg v s = make0 v s (default_arg0 s) - -let default_empty_value t = - let rec aux = function - | List0ArgType _ -> Some (Obj.repr []) - | OptArgType _ -> Some (Obj.repr None) - | PairArgType(t1,t2) -> - (match aux t1, aux t2 with - | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) - | _ -> None) - | ExtraArgType s -> - let (_, def) = String.Map.find s !arg0_map in - def - | _ -> None in - match aux t with - | Some v -> Some (Obj.obj v) - | None -> None - -(** Hackish part *) - -let arg0_names = ref (String.Map.empty : string String.Map.t) -(** We use this table to associate a name to a given witness, to use it with - the extension mechanism. This is REALLY ad-hoc, but I do not know how to - do so nicely either. *) - -let register_name0 t name = match t with -| ExtraArgType s -> - let () = assert (not (String.Map.mem s !arg0_names)) in - arg0_names := String.Map.add s name !arg0_names -| _ -> failwith "register_name0" - -let get_name0 name = - String.Map.find name !arg0_names diff --git a/interp/genarg.mli b/interp/genarg.mli deleted file mode 100644 index 629bd62a7..000000000 --- a/interp/genarg.mli +++ /dev/null @@ -1,316 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Loc -open Pp -open Names - -(** The route of a generic argument, from parsing to evaluation. -In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. - -{% \begin{%}verbatim{% }%} - parsing in_raw out_raw - char stream ---> raw_object ---> raw_object generic_argument -------+ - encapsulation decaps| - | - V - raw_object - | - globalization | - V - glob_object - | - encaps | - in_glob | - V - glob_object generic_argument - | - out in out_glob | - object <--- object generic_argument <--- object <--- glob_object <---+ - | decaps encaps interp decaps - | - V -effective use -{% \end{%}verbatim{% }%} - -To distinguish between the uninterpreted (raw), globalized and -interpreted worlds, we annotate the type [generic_argument] by a -phantom argument which is either [constr_expr], [glob_constr] or -[constr]. - -Transformation for each type : -{% \begin{%}verbatim{% }%} -tag raw open type cooked closed type - -BoolArgType bool bool -IntArgType int int -IntOrVarArgType int or_var int -StringArgType string (parsed w/ "") string -PreIdentArgType string (parsed w/o "") (vernac only) -IdentArgType true identifier identifier -IdentArgType false identifier (pattern_ident) identifier -IntroPatternArgType intro_pattern_expr intro_pattern_expr -VarArgType identifier located identifier -RefArgType reference global_reference -QuantHypArgType quantified_hypothesis quantified_hypothesis -ConstrArgType constr_expr constr -ConstrMayEvalArgType constr_expr may_eval constr -OpenConstrArgType open_constr_expr open_constr -ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings -BindingsArgType constr_expr bindings constr bindings -List0ArgType of argument_type -List1ArgType of argument_type -OptArgType of argument_type -ExtraArgType of string '_a '_b -{% \end{%}verbatim{% }%} -*) - -(** {5 Generic types} *) - -type ('raw, 'glob, 'top) genarg_type -(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized - one, and ['top] the internalized one. *) - -type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type -(** Alias for concision when the three types agree. *) - -val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type -(** Create a new generic type of argument: force to associate - unique ML types at each of the three levels. FIXME: almost deprecated. *) - -(** {5 Specialized types} *) - -(** All of [rlevel], [glevel] and [tlevel] must be non convertible - to ensure the injectivity of the type inference from type - ['co generic_argument] to [('a,'co) abstract_argument_type]; - this guarantees that, for 'co fixed, the type of - out_gen is monomorphic over 'a, hence type-safe -*) - -type rlevel -type glevel -type tlevel - -type ('a, 'co) abstract_argument_type -(** Type at level ['co] represented by an OCaml value of type ['a]. *) - -type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type -(** Specialized type at raw level. *) - -type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type -(** Specialized type at globalized level. *) - -type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type -(** Specialized type at internalized level. *) - -(** {6 Projections} *) - -val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type -(** Projection on the raw type constructor. *) - -val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type -(** Projection on the globalized type constructor. *) - -val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type -(** Projection on the internalized type constructor. *) - -(** {5 Generic arguments} *) - -type 'a generic_argument -(** A inhabitant of ['level generic_argument] is a inhabitant of some type at - level ['level], together with the representation of this type. *) - -type raw_generic_argument = rlevel generic_argument -type glob_generic_argument = glevel generic_argument -type typed_generic_argument = tlevel generic_argument - -(** {6 Constructors} *) - -val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument -(** [in_gen t x] embeds an argument of type [t] into a generic argument. *) - -val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a -(** [out_gen t x] recovers an argument of type [t] from a generic argument. It - fails if [x] has not the right dynamic type. *) - -val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool -(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that - [out_gen t v] will not raise a dynamic type exception. *) - -(** {6 Manipulation of generic arguments} - -Those functions fail if they are applied to an argument which has not the right -dynamic type. *) - -val fold_list0 : - ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c - -val fold_list1 : - ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c - -val fold_opt : - ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c - -val fold_pair : - ('a generic_argument -> 'a generic_argument -> 'c) -> - 'a generic_argument -> 'c - -(** [app_list0] fails if applied to an argument not of tag [List0 t] - for some [t]; it's the responsability of the caller to ensure it *) - -val app_list0 : ('a generic_argument -> 'b generic_argument) -> -'a generic_argument -> 'b generic_argument - -val app_list1 : ('a generic_argument -> 'b generic_argument) -> -'a generic_argument -> 'b generic_argument - -val app_opt : ('a generic_argument -> 'b generic_argument) -> -'a generic_argument -> 'b generic_argument - -val app_pair : - ('a generic_argument -> 'b generic_argument) -> - ('a generic_argument -> 'b generic_argument) - -> 'a generic_argument -> 'b generic_argument - -(** {6 High-level creation} *) - -(** {5 Genarg environments} *) - -type glob_sign = { - ltacvars : Id.t list * Id.t list; - ltacrecvars : (Id.t * Nametab.ltac_constant) list; - gsigma : Evd.evar_map; - genv : Environ.env } - -module TacStore : Store.S - -type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; - extra : TacStore.t } - -(** {5 Generic arguments} *) - -type ('raw, 'glb, 'top) arg0 = { - arg0_rprint : 'raw -> std_ppcmds; - (** Printing at raw level function. *) - arg0_gprint : 'glb -> std_ppcmds; - (** Printing at glob level function. *) - arg0_tprint : 'top -> std_ppcmds; - (** Printing at top level function. *) - arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb; - (** Globalization function. *) - arg0_subst : Mod_subst.substitution -> 'glb -> 'glb; - (** Substitution function. *) - arg0_interp : interp_sign -> - Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top; - (** Intepretation function. *) -} - -val make0 : 'raw option -> string -> ('raw, 'glb, 'top) arg0 -> - ('raw, 'glb, 'top) genarg_type -(** [make0 def name arg] create a generic argument named [name] with the - manipulation functions defined in [arg], and with a default empty value - [def]. FIXME: [def] is related to parsing and should be put elsewhere. *) - -val default_arg0 : string -> ('raw, 'glb, 'top) arg0 -(** A default [arg0] with a given name. Printing functions print a dummy value - and glob/subst/interp all fail. *) - -val default_uniform_arg0 : string -> ('a, 'a, 'a) arg0 -(** A default uniform [arg0] with a given name. Printing functions print a dummy - value and glob/subst/interp are all identity. *) - -val arg_gen : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) arg0 -(** Create the manipulation functions for any generic argument type. *) - -(** {5 Generic manipulation functions} - - Those functions are the counterparts of [arg0] fields, but they apply on any - generic argument. - - FIXME: only partially implemented for now. *) - -val raw_print : rlevel generic_argument -> std_ppcmds -val glb_print : glevel generic_argument -> std_ppcmds -val top_print : tlevel generic_argument -> std_ppcmds - -val globalize : glob_sign -> - rlevel generic_argument -> glob_sign * glevel generic_argument - -val substitute : Mod_subst.substitution -> - glevel generic_argument -> glevel generic_argument - -val interpret : interp_sign -> Goal.goal Evd.sigma -> - glevel generic_argument -> Evd.evar_map * tlevel generic_argument - -(** {6 Type reification} *) - -type argument_type = - (** Basic types *) - | IntOrVarArgType - | IntroPatternArgType - | IdentArgType of bool - | VarArgType - | RefArgType - (** Specific types *) - | GenArgType - | SortArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType of bool - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | List0ArgType of argument_type - | List1ArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string - -val argument_type_eq : argument_type -> argument_type -> bool - -val genarg_tag : 'a generic_argument -> argument_type - -val unquote : ('a, 'co) abstract_argument_type -> argument_type - -(** {5 Basic generic type constructors} *) - -(** {6 Parameterized types} *) - -val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type -val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type -val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type -val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> - ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type - -(** {5 Magic used by the parser} *) - -(** [in_generic] is used in combination with camlp4 [Gramext.action] magic - - [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument] - - where |a|_l is the interpretation of a at level l - - [in_generic] is not typable; we replace the second argument by an absurd - type (with no introduction rule) -*) -type an_arg_of_this_type - -val in_generic : - argument_type -> an_arg_of_this_type -> 'co generic_argument - -val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option - -val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit -(** Used by the extension to give a name to types. The string should be the - absolute path of the argument witness, e.g. - [register_name0 wit_toto "MyArg.wit_toto"]. *) - -val get_name0 : string -> string -(** Return the absolute path of a given witness. *) diff --git a/interp/genintern.ml b/interp/genintern.ml new file mode 100644 index 000000000..00ea3a71b --- /dev/null +++ b/interp/genintern.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Names +open Mod_subst +open Genarg + +type glob_sign = { + ltacvars : Id.t list * Id.t list; + ltacrecvars : (Id.t * Nametab.ltac_constant) list; + gsigma : Evd.evar_map; + genv : Environ.env } + +type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb +type 'glb subst_fun = substitution -> 'glb -> 'glb + +let arg0_intern_map = + ref (String.Map.empty : (Obj.t, Obj.t) intern_fun String.Map.t) +let arg0_subst_map = + ref (String.Map.empty : Obj.t subst_fun String.Map.t) + +let get_intern0 name = + try String.Map.find name !arg0_intern_map + with Not_found -> + Errors.anomaly (str "intern0 function not found: " ++ str name) + +let get_subst0 name = + try String.Map.find name !arg0_subst_map + with Not_found -> + Errors.anomaly (str "subst0 function not found: " ++ str name) + +(** For now, the following functions are quite dummy and should only be applied + to an extra argument type, otherwise, they will badly fail. *) + +let rec obj_intern t = match t with +| ExtraArgType s -> get_intern0 s +| _ -> assert false + +let intern t = Obj.magic (obj_intern (unquote (rawwit t))) + +let generic_intern ist v = + let t = genarg_tag v in + let (ist, ans) = obj_intern t ist (Unsafe.prj v) in + (ist, Unsafe.inj t ans) + +(** Substitution functions *) + +let rec obj_substitute t = match t with +| ExtraArgType s -> get_subst0 s +| _ -> assert false + +let substitute t = Obj.magic (obj_substitute (unquote (rawwit t))) + +let generic_substitute subs v = + let t = genarg_tag v in + let ans = obj_substitute t subs (Unsafe.prj v) in + Unsafe.inj t ans + +(** Registering functions *) + +let register_intern0 arg f = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_intern_map then + Errors.anomaly (str "intern0 function already registered: " ++ str s) + else + arg0_intern_map := String.Map.add s (Obj.magic f) !arg0_intern_map +| _ -> assert false + +let register_subst0 arg f = match unquote (rawwit arg) with +| ExtraArgType s -> + if String.Map.mem s !arg0_subst_map then + Errors.anomaly (str "subst0 function already registered: " ++ str s) + else + arg0_subst_map := String.Map.add s (Obj.magic f) !arg0_subst_map +| _ -> assert false diff --git a/interp/genintern.mli b/interp/genintern.mli new file mode 100644 index 000000000..25050fe7c --- /dev/null +++ b/interp/genintern.mli @@ -0,0 +1,43 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Mod_subst +open Genarg + +type glob_sign = { + ltacvars : Id.t list * Id.t list; + ltacrecvars : (Id.t * Nametab.ltac_constant) list; + gsigma : Evd.evar_map; + genv : Environ.env } + +(** {5 Internalization functions} *) + +type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb +(** The type of functions used for internalizing generic arguments. *) + +val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun + +val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun + +(** {5 Substitution functions} *) + +type 'glb subst_fun = substitution -> 'glb -> 'glb +(** The type of functions used for substituting generic arguments. *) + +val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun + +val generic_substitute : glob_generic_argument subst_fun + +(** Registering functions *) + +val register_intern0 : ('raw, 'glb, 'top) genarg_type -> + ('raw, 'glb) intern_fun -> unit + +val register_subst0 : ('raw, 'glb, 'top) genarg_type -> + 'glb subst_fun -> unit diff --git a/interp/interp.mllib b/interp/interp.mllib index 77e2e5c00..7f14fe42b 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,11 +1,10 @@ +Genintern Constrexpr_ops Notation_ops Topconstr Ppextend Notation Dumpglob -Genarg -Stdarg Syntax_def Smartlocate Reserve @@ -17,4 +16,5 @@ Constrextern Coqlib Discharge Declare +Stdarg Constrarg diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 1216e06b1..6f2ff6ec4 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -9,41 +9,23 @@ open Pp open Genarg -let def_uniform name pr = { (default_uniform_arg0 name) with - arg0_rprint = pr; - arg0_gprint = pr; - arg0_tprint = pr; -} - let wit_unit : unit uniform_genarg_type = - let pr_unit _ = str "()" in - let arg = def_uniform "unit" pr_unit in - make0 None "unit" arg + make0 None "unit" let wit_bool : bool uniform_genarg_type = - let pr_bool b = str (if b then "true" else "false") in - let arg = def_uniform "bool" pr_bool in - make0 None "bool" arg - -let () = register_name0 wit_bool "Stdarg.wit_bool" + make0 None "bool" let wit_int : int uniform_genarg_type = - let pr_int = int in - let arg = def_uniform "int" pr_int in - make0 None "int" arg - -let () = register_name0 wit_int "Stdarg.wit_int" + make0 None "int" let wit_string : string uniform_genarg_type = - let pr_string s = str "\"" ++ str s ++ str "\"" in - let arg = def_uniform "string" pr_string in - make0 None "string" arg - -let () = register_name0 wit_string "Stdarg.wit_string" + make0 None "string" let wit_pre_ident : string uniform_genarg_type = - let pr_pre_ident = str in - let arg = def_uniform "preident" pr_pre_ident in - make0 None "preident" arg + make0 None "preident" +let () = register_name0 wit_unit "Stdarg.wit_unit" +let () = register_name0 wit_bool "Stdarg.wit_bool" +let () = register_name0 wit_int "Stdarg.wit_int" +let () = register_name0 wit_string "Stdarg.wit_string" let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" |