diff options
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 281 |
1 files changed, 0 insertions, 281 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml deleted file mode 100644 index 41cbcdaf..00000000 --- a/interp/genarg.ml +++ /dev/null @@ -1,281 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \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 Nameops -open Nametab -open Glob_term -open Topconstr -open Term -open Evd - -type argument_type = - (* Basic types *) - | BoolArgType - | IntArgType - | IntOrVarArgType - | StringArgType - | PreIdentArgType - | IntroPatternArgType - | IdentArgType of bool - | VarArgType - | RefArgType - (* Specific types *) - | SortArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType of bool * bool (* casted, TC resolution *) - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | List0ArgType of argument_type - | List1ArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string - -type 'a and_short_name = 'a * identifier located option -type 'a or_by_notation = - | AN of 'a - | ByNotation of (loc * string * Notation.delimiters option) - -let loc_of_or_by_notation f = function - | AN c -> f c - | ByNotation (loc,s,_) -> loc - -type glob_constr_and_expr = glob_constr * constr_expr option -type open_constr_expr = unit * constr_expr -type open_glob_constr = unit * glob_constr_and_expr - -type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern - -type 'a with_ebindings = 'a * open_constr bindings - -(* Dynamics but tagged by a type expression *) - -type 'a generic_argument = argument_type * Obj.t - -type rlevel -type glevel -type tlevel - -type intro_pattern_expr = - | IntroOrAndPattern of or_and_intro_pattern_expr - | IntroWildcard - | IntroRewrite of bool - | IntroIdentifier of identifier - | IntroFresh of identifier - | IntroForthcoming of bool - | IntroAnonymous -and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list - -let rec pr_intro_pattern (_,pat) = match pat with - | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll - | IntroWildcard -> str "_" - | IntroRewrite true -> str "->" - | IntroRewrite false -> str "<-" - | IntroIdentifier id -> pr_id id - | IntroFresh id -> str "?" ++ pr_id id - | IntroForthcoming true -> str "*" - | IntroForthcoming false -> str "**" - | IntroAnonymous -> str "?" - -and pr_or_and_intro_pattern = function - | [pl] -> - str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")" - | pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) - ++ str "]" - -let rawwit_bool = BoolArgType -let globwit_bool = BoolArgType -let wit_bool = BoolArgType - -let rawwit_int = IntArgType -let globwit_int = IntArgType -let wit_int = IntArgType - -let rawwit_int_or_var = IntOrVarArgType -let globwit_int_or_var = IntOrVarArgType -let wit_int_or_var = IntOrVarArgType - -let rawwit_string = StringArgType -let globwit_string = StringArgType -let wit_string = StringArgType - -let rawwit_pre_ident = PreIdentArgType -let globwit_pre_ident = PreIdentArgType -let wit_pre_ident = PreIdentArgType - -let rawwit_intro_pattern = IntroPatternArgType -let globwit_intro_pattern = IntroPatternArgType -let wit_intro_pattern = IntroPatternArgType - -let rawwit_ident_gen b = IdentArgType b -let globwit_ident_gen b = IdentArgType b -let wit_ident_gen b = IdentArgType b - -let rawwit_ident = rawwit_ident_gen true -let globwit_ident = globwit_ident_gen true -let wit_ident = wit_ident_gen true - -let rawwit_pattern_ident = rawwit_ident_gen false -let globwit_pattern_ident = globwit_ident_gen false -let wit_pattern_ident = wit_ident_gen false - -let rawwit_var = VarArgType -let globwit_var = VarArgType -let wit_var = VarArgType - -let rawwit_ref = RefArgType -let globwit_ref = RefArgType -let wit_ref = RefArgType - -let rawwit_quant_hyp = QuantHypArgType -let globwit_quant_hyp = QuantHypArgType -let wit_quant_hyp = QuantHypArgType - -let rawwit_sort = SortArgType -let globwit_sort = SortArgType -let wit_sort = SortArgType - -let rawwit_constr = ConstrArgType -let globwit_constr = ConstrArgType -let wit_constr = ConstrArgType - -let rawwit_constr_may_eval = ConstrMayEvalArgType -let globwit_constr_may_eval = ConstrMayEvalArgType -let wit_constr_may_eval = ConstrMayEvalArgType - -let rawwit_open_constr_gen (b1,b2) = OpenConstrArgType (b1,b2) -let globwit_open_constr_gen (b1,b2) = OpenConstrArgType (b1,b2) -let wit_open_constr_gen (b1,b2) = OpenConstrArgType (b1,b2) - -let rawwit_open_constr = rawwit_open_constr_gen (false,false) -let globwit_open_constr = globwit_open_constr_gen (false,false) -let wit_open_constr = wit_open_constr_gen (false,false) - -let rawwit_casted_open_constr = rawwit_open_constr_gen (true,false) -let globwit_casted_open_constr = globwit_open_constr_gen (true,false) -let wit_casted_open_constr = wit_open_constr_gen (true,false) - -let rawwit_open_constr_wTC = rawwit_open_constr_gen (false,true) -let globwit_open_constr_wTC = globwit_open_constr_gen (false,true) -let wit_open_constr_wTC = wit_open_constr_gen (false,true) - -let rawwit_constr_with_bindings = ConstrWithBindingsArgType -let globwit_constr_with_bindings = ConstrWithBindingsArgType -let wit_constr_with_bindings = ConstrWithBindingsArgType - -let rawwit_bindings = BindingsArgType -let globwit_bindings = BindingsArgType -let wit_bindings = BindingsArgType - -let rawwit_red_expr = RedExprArgType -let globwit_red_expr = RedExprArgType -let wit_red_expr = RedExprArgType - -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 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 unquote x = x - -type an_arg_of_this_type = Obj.t - -let in_generic t x = (t, Obj.repr x) - -let dyntab = ref ([] : (string * glevel generic_argument option) list) - -type ('a,'b) abstract_argument_type = argument_type - -let create_arg v s = - if List.mem_assoc s !dyntab then - anomaly ("Genarg.create: already declared generic argument " ^ s); - let t = ExtraArgType s in - dyntab := (s,Option.map (in_gen t) v) :: !dyntab; - (t,t,t) - -let exists_argtype s = List.mem_assoc s !dyntab - -let default_empty_argtype_value s = List.assoc s !dyntab - -let default_empty_value t = - let rec aux = function - | List0ArgType _ -> Some (in_gen t []) - | OptArgType _ -> Some (in_gen t None) - | PairArgType(t1,t2) -> - (match aux t1, aux t2 with - | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2)) - | _ -> None) - | ExtraArgType s -> default_empty_argtype_value s - | _ -> None in - match aux t with - | Some v -> Some (out_gen t v) - | None -> None |