diff options
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 70 | ||||
-rw-r--r-- | interp/constrintern.mli | 67 | ||||
-rw-r--r-- | interp/coqlib.ml | 51 | ||||
-rw-r--r-- | interp/coqlib.mli | 17 | ||||
-rw-r--r-- | interp/topconstr.ml | 7 |
5 files changed, 174 insertions, 38 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0057edad6..36a219a61 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,15 +24,32 @@ open Nametab open Notation open Inductiveops -(* To interpret implicits and arg scopes of recursive variables in - inductive types and recursive definitions *) -type var_internalisation_type = Inductive | Recursive | Method - -type var_internalisation_data = - var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list - -type implicits_env = (identifier * var_internalisation_data) list -type full_implicits_env = identifier list * implicits_env +(* To interpret implicits and arg scopes of variables in inductive + types and recursive definitions and of projection names in records *) + +type var_internalization_type = Inductive | Recursive | Method + +type var_internalization_data = + (* type of the "free" variable, for coqdoc, e.g. while typing the + constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + var_internalization_type * + (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" + in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) + identifier list * + (* signature of impargs of the variable *) + Impargs.implicits_list * + (* subscopes of the args of the variable *) + scope_name option list + +type internalization_env = + (identifier * var_internalization_data) list + +type full_internalization_env = + (* a superset of the list of variables that may be automatically + inserted and that must not occur as binders *) + identifier list * + (* mapping of the variables to their internalization data *) + internalization_env type raw_binder = (name * binding_kind * rawconstr option * rawconstr) @@ -155,6 +172,35 @@ let error_inductive_parameter_not_implicit loc = "the 'return' clauses; they must be replaced by '_' in the 'in' clauses.")) (**********************************************************************) +(* Pre-computing the implicit arguments and arguments scopes needed *) +(* for interpretation *) + +let empty_internalization_env = ([],[]) + +let set_internalization_env_params ienv params = + let nparams = List.length params in + if nparams = 0 then + ([],ienv) + else + let ienv_with_implicit_params = + List.map (fun (id,(ty,_,impl,scopes)) -> + let sub_impl,_ = list_chop nparams impl in + let sub_impl' = List.filter is_status_implicit sub_impl in + (id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in + (params, ienv_with_implicit_params) + +let compute_internalization_data env ty typ impls = + let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in + (ty, [], impl, compute_arguments_scope typ) + +let compute_full_internalization_env env ty params idl typl impll = + set_internalization_env_params + (list_map3 + (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) + idl typl impll) + params + +(**********************************************************************) (* Contracting "{ _ }" in notations *) let rec wildcards ntn n = @@ -368,7 +414,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l (* [id] a goal variable *) RVar (loc,id), [], [], [] -let find_appl_head_data (_,_,_,(_,impls)) = function +let find_appl_head_data _ = function | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] | x -> x,[],[],[] @@ -1405,12 +1451,12 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in pattern_of_rawconstr c -let interp_aconstr impls (vars,varslist) a = +let interp_aconstr ?(impls=([],[])) (vars,varslist) a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, []) - false (([],[]),Environ.named_context env,vl,([],impls)) a in + false (([],[]),Environ.named_context env,vl,impls) a in (* Translate and check that [c] has all its free variables bound in [vars] *) let a = aconstr_of_rawconstr vars c in (* Returns [a] and the ordered list of variables with their scopes *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b39f6e18b..b08b8dd1f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -33,19 +33,42 @@ open Pretyping - insert existential variables for implicit arguments *) -(* To interpret implicits and arg scopes of recursive variables in - inductive types and recursive definitions; mention of a list of - implicits arguments in the ``rel'' part of [env]; the second - argument associates a list of implicit positions and scopes to - identifiers declared in the [rel_context] of [env] *) +(* To interpret implicits and arg scopes of recursive variables while + internalizing inductive types and recursive definitions, and also + projection while typing records. -type var_internalisation_type = Inductive | Recursive | Method + the third and fourth arguments associate a list of implicit + positions and scopes to identifiers declared in the [rel_context] + of [env] *) -type var_internalisation_data = - var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list +type var_internalization_type = Inductive | Recursive | Method -type implicits_env = (identifier * var_internalisation_data) list -type full_implicits_env = identifier list * implicits_env +type var_internalization_data = + var_internalization_type * + identifier list * + Impargs.implicits_list * + scope_name option list + +(* A map of free variables to their implicit arguments and scopes *) +type internalization_env = + (identifier * var_internalization_data) list + +(* Contains also a list of identifiers to automatically apply to the variables*) +type full_internalization_env = + identifier list * internalization_env + +val empty_internalization_env : full_internalization_env + +val compute_internalization_data : env -> var_internalization_type -> + types -> Impargs.manual_explicitation list -> var_internalization_data + +val set_internalization_env_params : + internalization_env -> identifier list -> full_internalization_env + +val compute_full_internalization_env : env -> + var_internalization_type -> + identifier list -> identifier list -> types list -> + Impargs.manual_explicitation list list -> full_internalization_env type manual_implicits = (explicitation * (bool * bool * bool)) list @@ -60,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr val intern_type : evar_map -> env -> constr_expr -> rawconstr val intern_gen : bool -> evar_map -> env -> - ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr val intern_pattern : env -> cases_pattern_expr -> @@ -69,12 +92,12 @@ val intern_pattern : env -> cases_pattern_expr -> val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list -(*s Composing internalisation with pretyping *) +(*s Composing internalization with pretyping *) (* Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> - ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr (* Particular instances *) @@ -82,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env -> val interp_constr : evar_map -> env -> constr_expr -> constr -val interp_type : evar_map -> env -> ?impls:full_implicits_env -> +val interp_type : evar_map -> env -> ?impls:full_internalization_env -> constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr -val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> +val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr (* Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> - ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits + ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> - env -> ?impls:full_implicits_env -> + env -> ?impls:full_internalization_env -> constr_expr -> types * manual_implicits val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> - env -> ?impls:full_implicits_env -> + env -> ?impls:full_internalization_env -> constr_expr -> constr * manual_implicits val interp_casted_constr_evars : evar_defs ref -> env -> - ?impls:full_implicits_env -> constr_expr -> types -> constr + ?impls:full_internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> +val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -147,8 +170,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Interprets into a abbreviatable constr *) -val interp_aconstr : implicits_env -> identifier list * identifier list - -> constr_expr -> interpretation +val interp_aconstr : ?impls:full_internalization_env -> + identifier list * identifier list -> constr_expr -> interpretation (* Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 90432a4a4..1ca82e35c 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -215,9 +215,11 @@ type coq_eq_data = { trans: constr; congr: constr } -type coq_rewrite_data = { - rrec : constr option; - rect : constr option +(* Data needed for discriminate and injection *) +type coq_inversion_data = { + inv_eq : constr; (* : forall params, t -> Prop *) + inv_ind : constr; (* : forall params P y, eq params y -> P y *) + inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } let lazy_init_constant dir id = lazy (init_constant dir id) @@ -234,6 +236,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym" let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans" let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" +let coq_eq_congr_canonical = + lazy_init_constant ["Logic"] "f_equal_canonical_form" let build_coq_eq_data () = let _ = check_required_library logic_module_name in { @@ -245,11 +249,18 @@ let build_coq_eq_data () = congr = Lazy.force coq_eq_congr } let build_coq_eq () = Lazy.force coq_eq_eq +let build_coq_eq_refl () = Lazy.force coq_eq_refl let build_coq_eq_sym () = Lazy.force coq_eq_sym let build_coq_f_equal2 () = Lazy.force coq_f_equal2 let build_coq_sym_eq = build_coq_eq_sym (* compatibility *) +let build_coq_inversion_eq_data () = + let _ = check_required_library logic_module_name in { + inv_eq = Lazy.force coq_eq_eq; + inv_ind = Lazy.force coq_eq_ind; + inv_congr = Lazy.force coq_eq_congr_canonical } + (* Heterogenous equality on Type *) let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq" @@ -260,6 +271,8 @@ let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect" let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym" let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr" let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans" +let coq_jmeq_congr_canonical = + lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form" let build_coq_jmeq_data () = let _ = check_required_library jmeq_module_name in { @@ -270,6 +283,17 @@ let build_coq_jmeq_data () = trans = Lazy.force coq_jmeq_trans; congr = Lazy.force coq_jmeq_congr } +let join_jmeq_types eq = + mkLambda(Name (id_of_string "A"),Termops.new_Type(), + mkLambda(Name (id_of_string "x"),mkRel 1, + mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|]))) + +let build_coq_inversion_jmeq_data () = + let _ = check_required_library logic_module_name in { + inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq); + inv_ind = Lazy.force coq_jmeq_ind; + inv_congr = Lazy.force coq_jmeq_congr_canonical } + (* Specif *) let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" @@ -284,6 +308,7 @@ let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect" let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans" +let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form" let build_coq_identity_data () = let _ = check_required_library datatypes_module_name in { @@ -294,6 +319,25 @@ let build_coq_identity_data () = trans = Lazy.force coq_identity_trans; congr = Lazy.force coq_identity_congr } +let build_coq_inversion_identity_data () = + let _ = check_required_library datatypes_module_name in + let _ = check_required_library logic_type_module_name in { + inv_eq = Lazy.force coq_identity_eq; + inv_ind = Lazy.force coq_identity_ind; + inv_congr = Lazy.force coq_identity_congr_canonical } + +(* Equality to true *) +let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true" +let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind" +let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr" + +let build_coq_inversion_eq_true_data () = + let _ = check_required_library datatypes_module_name in + let _ = check_required_library logic_module_name in { + inv_eq = Lazy.force coq_eq_true_eq; + inv_ind = Lazy.force coq_eq_true_ind; + inv_congr = Lazy.force coq_eq_true_congr } + (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" @@ -332,6 +376,7 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj let coq_eq_ref = lazy (init_reference ["Logic"] "eq") let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq") +let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true") let coq_existS_ref = lazy (anomaly "use coq_existT_ref") let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_not_ref = lazy (init_reference ["Logic"] "not") diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 8b0384960..6bb79c8b6 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -58,6 +58,9 @@ val check_required_library : string list -> unit val logic_module : dir_path val logic_type_module : dir_path +val datatypes_module_name : string list +val logic_module_name : string list + (* Natural numbers *) val nat_path : full_path val glob_nat : global_reference @@ -119,9 +122,22 @@ val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : constr delayed (* = [(build_coq_eq_data()).refl] *) val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : constr delayed +(* Data needed for discriminate and injection *) + +type coq_inversion_data = { + inv_eq : constr; (* : forall params, t -> Prop *) + inv_ind : constr; (* : forall params P y, eq params y -> P y *) + inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *) +} + +val build_coq_inversion_eq_data : coq_inversion_data delayed +val build_coq_inversion_identity_data : coq_inversion_data delayed +val build_coq_inversion_jmeq_data : coq_inversion_data delayed +val build_coq_inversion_eq_true_data : coq_inversion_data delayed (* Specif *) val build_coq_sumbool : constr delayed @@ -154,6 +170,7 @@ val build_coq_ex : constr delayed val coq_eq_ref : global_reference lazy_t val coq_identity_ref : global_reference lazy_t val coq_jmeq_ref : global_reference lazy_t +val coq_eq_true_ref : global_reference lazy_t val coq_existS_ref : global_reference lazy_t val coq_existT_ref : global_reference lazy_t val coq_not_ref : global_reference lazy_t diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 04715d51b..df48458e6 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -856,12 +856,17 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c) let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r -let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l) let mkCastC (a,k) = CCast (dummy_loc,a,k) let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b) +let mkAppC (f,l) = + let l = List.map (fun x -> (x,None)) l in + match f with + | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l) + | _ -> CApp (dummy_loc, (None, f), l) + let rec mkCProdN loc bll c = match bll with | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> |