diff options
Diffstat (limited to 'contrib')
22 files changed, 729 insertions, 998 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 04852da664..8eeb8b642d 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -130,7 +130,7 @@ let mk_open_instance id gl m t= RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try - Pretyping.understand evmap env (raux m rawt) + Pretyping.Default.understand evmap env (raux m rawt) with _ -> error "Untypable instance, maybe higher-order non-prenex quantification" in Sign.decompose_lam_n_assum m ntt diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index cb43a45ed9..8fcdb5d90a 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -400,7 +400,7 @@ let inspect n = add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) - (Pretyping.understand Evd.empty (Global.env()) + (Pretyping.Default.understand Evd.empty (Global.env()) (RRef(dummy_loc, IndRef(kn,0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 19b06a30d3..d2f71bfc2f 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -34,7 +34,7 @@ let get_hyp_by_name g name = let evd = project g in let env = pf_env g in try (let judgment = - Pretyping.understand_judgment + Pretyping.Default.understand_judgment evd env (RVar(zz, name)) in ("hyp",judgment.uj_type)) (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up... diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index f973548457..36ebaff11f 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -34,6 +34,7 @@ open Pfedit open Topconstr open Rawterm open Pretyping +open Pretyping.Default open Safe_typing open Constrintern open Hiddentac diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v index 14990a24c5..6face72d11 100644 --- a/contrib/subtac/FixSub.v +++ b/contrib/subtac/FixSub.v @@ -21,7 +21,7 @@ End FixPoint. End Well_founded. -Check Fix_sub. +(*Check Fix_sub.*) Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, (fun x => Q) (proj1_sig x)) diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli new file mode 100644 index 0000000000..671d6f3619 --- /dev/null +++ b/contrib/subtac/context.mli @@ -0,0 +1,5 @@ +type t = Term.rel_declaration list +val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c +val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c +val id_of_name : Names.name -> Names.identifier +val subst_env : 'a -> 'b -> 'a * 'b diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4 index f435219936..095e5fafc9 100644 --- a/contrib/subtac/g_eterm.ml4 +++ b/contrib/subtac/g_eterm.ml4 @@ -23,5 +23,5 @@ TACTIC EXTEND eterm [ "eterm" ] -> [ (fun gl -> let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in - Eterm.etermtac (Global.env ()) (evm, t) gl) ] + Eterm.etermtac (evm, t) gl) ] END diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/g_subtac.ml4 index 43214c87bd..d9c7a8c023 100644 --- a/contrib/subtac/sparser.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -49,7 +49,7 @@ GEXTEND Gram ; END -(* type wf_proof_type_argtype = (Scoq.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *) +(* type wf_proof_type_argtype = (Subtac_utils.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *) (* let (wit_subtac_wf_proof_type : wf_proof_type_argtype), *) (* (globwit_subtac_wf_proof_type : wf_proof_type_argtype), *) @@ -63,7 +63,7 @@ let (wit_subtac_gallina_loc : gallina_loc_argtype), (rawwit_subtac_gallina_loc : gallina_loc_argtype) = Genarg.create_arg "subtac_gallina_loc" -(* type subtac_recdef_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *) +(* type subtac_recdef_argtype = (Subtac_utils.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type *) (* let (wit_subtac_recdef : subtac_recdef_argtype), *) (* (globwit_subtac_recdef : subtac_recdef_argtype), *) diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml deleted file mode 100644 index d338c34452..0000000000 --- a/contrib/subtac/interp.ml +++ /dev/null @@ -1,666 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Global -open Pp -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Rawterm -open Evarconv -open Pattern -open Dyn -open Pretyping - -open Subtac_coercion -open Scoq -open Coqlib -open Printer -open Subtac_errors -open Context -open Eterm - -type recursion_info = { - arg_name: name; - arg_type: types; (* A *) - args_after : rel_context; - wf_relation: constr; (* R : A -> A -> Prop *) - wf_proof: constr; (* : well_founded R *) - f_type: types; (* f: A -> Set *) - f_fulltype: types; (* Type with argument and wf proof product first *) -} - -let my_print_rec_info env t = - str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++ - str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++ - str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++ - str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ - str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ - str "Full type: " ++ my_print_constr env t.f_fulltype - -(* Taken from pretyping.ml *) -let evd_comb0 f isevars = - let (evd',x) = f !isevars in - isevars := evd'; - x -let evd_comb1 f isevars x = - let (evd',y) = f !isevars x in - isevars := evd'; - y -let evd_comb2 f isevars x y = - let (evd',z) = f !isevars x y in - isevars := evd'; - z -let evd_comb3 f isevars x y z = - let (evd',t) = f !isevars x y z in - isevars := evd'; - t - -(************************************************************************) -(* This concerns Cases *) -open Declarations -open Inductive -open Inductiveops - -(************************************************************************) - -let mt_evd = Evd.empty - -let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) - -(* Utilisé pour inférer le prédicat des Cases *) -(* Semble exagérement fort *) -(* Faudra préférer une unification entre les types de toutes les clauses *) -(* et autoriser des ? à rester dans le résultat de l'unification *) - -let evar_type_fixpoint loc env isevars lna lar vdefj = - let lt = Array.length vdefj in - if Array.length lar = lt then - for i = 0 to lt-1 do - if not (e_cumul env isevars (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env (evars_of !isevars) - i lna vdefj lar - done - -let check_branches_message loc env isevars c (explft,lft) = - for i = 0 to Array.length explft - 1 do - if not (e_cumul env isevars lft.(i) explft.(i)) then - let sigma = evars_of !isevars in - error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) - done - -(* coerce to tycon if any *) -let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j - | Some typ -> evd_comb2 (Subtac_coercion.inh_conv_coerce_to loc env) isevars j typ - -let push_rels vars env = List.fold_right push_rel vars env - -let strip_meta id = (* For Grammar v7 compatibility *) - let s = string_of_id id in - if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) - else id - -let pretype_id loc env (lvar,unbndltacvars) id = - let id = strip_meta id in (* May happen in tactics defined by Grammar *) - try - let (n,typ) = lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = type_app (lift n) typ } - with Not_found -> - try - List.assoc id lvar - with Not_found -> - try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } - with Not_found -> - try (* To build a nicer ltac error message *) - match List.assoc id unbndltacvars with - | None -> user_err_loc (loc,"", - str (string_of_id id ^ " ist not bound to a term")) - | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 - with Not_found -> - error_var_not_found_loc loc id - -(* make a dependent predicate from an undependent one *) - -let make_dep_of_undep env (IndType (indf,realargs)) pj = - let n = List.length realargs in - let rec decomp n p = - if n=0 then p else - match kind_of_term p with - | Lambda (_,_,c) -> decomp (n-1) c - | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) - in - let sign,s = decompose_prod_n n pj.uj_type in - let ind = build_dependent_inductive env indf in - let s' = mkProd (Anonymous, ind, s) in - let ccl = lift 1 (decomp n pj.uj_val) in - let ccl' = mkLambda (Anonymous, ind, ccl) in - {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} - -(*************************************************************************) -(* Main pretyping function *) - -let pretype_ref isevars env ref = - let c = constr_of_global ref in - make_judge c (Retyping.get_type_of env Evd.empty c) - -let pretype_sort = function - | RProp c -> judge_of_prop_contents c - | RType _ -> judge_of_new_Type () - -let my_print_tycon env = function - Some t -> my_print_constr env t - | None -> str "None" - -(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *) -(* in environment [env], with existential variables [(evars_of isevars)] and *) -(* the type constraint tycon *) -let rec pretype tycon env isevars lvar c = - trace (str "pretype for " ++ (my_print_rawconstr env c) ++ - str " and tycon "++ my_print_tycon env tycon ++ - str " in environment: " ++ my_print_env env); - match c with - - | RRef (loc,ref) -> - inh_conv_coerce_to_tycon loc env isevars - (pretype_ref isevars env ref) - tycon - - | RVar (loc, id) -> - inh_conv_coerce_to_tycon loc env isevars - (pretype_id loc env lvar id) - tycon - - | REvar (loc, ev, instopt) -> - (* Ne faudrait-il pas s'assurer que hyps est bien un - sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.map (evars_of !isevars) ev) in - let args = match instopt with - | None -> instance_from_named_context hyps - | Some inst -> failwith "Evar subtitutions not implemented" in - let c = mkEvar (ev, args) in - let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in - inh_conv_coerce_to_tycon loc env isevars j tycon - - | RPatVar (loc,(someta,n)) -> - anomaly "Found a pattern variable in a rawterm to type" - - | RHole (loc,k) -> - let ty = - match tycon with - | Some ty -> ty - | None -> - e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in - { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } - - | RRec (loc,fixkind,names,bl,lar,vdef) -> - let rec type_bl env ctxt = function - [] -> ctxt - | (na,None,ty)::bl -> - let ty' = pretype_type empty_valcon env isevars lvar ty in - let dcl = (na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,Some bd,ty)::bl -> - let ty' = pretype_type empty_valcon env isevars lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in - let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in - let ctxtv = Array.map (type_bl env empty_rel_context) bl in - let larj = - array_map2 - (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) isevars lvar ar) - ctxtv lar in - let lara = Array.map (fun a -> a.utj_val) larj in - let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in - let nbfix = Array.length lar in - let names = Array.map (fun id -> Name id) names in - (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types (names,ftys,[||]) env in - let vdefj = - array_map2_i - (fun i ctxt def -> - (* we lift nbfix times the type in tycon, because of - * the nbfix variables pushed to newenv *) - let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) - (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon ty) nenv isevars lvar def in - { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) - ctxtv vdef in - evar_type_fixpoint loc env isevars names ftys vdefj; - let fixj = - match fixkind with - | RFix (vn,i) -> - let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in - (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkFix fix) ftys.(i) - | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env isevars fixj tycon - - | RSort (loc,s) -> - inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon - - | RApp (loc,f,args) -> - let fj = pretype empty_tycon env isevars lvar f in - let floc = loc_of_rawconstr f in - let rec apply_rec env n resj = function - | [] -> resj - | c::rest -> - let argloc = loc_of_rawconstr c in - let resj = evd_comb1 (inh_app_fun env) isevars resj in - let resty = - whd_betadeltaiota env (evars_of !isevars) resj.uj_type in - match kind_of_term resty with - | Prod (na,c1,c2) -> - let hj = pretype (mk_tycon c1) env isevars lvar c in - let newresj = - { uj_val = applist (j_val resj, [j_val hj]); - uj_type = subst1 hj.uj_val c2 } in - apply_rec env (n+1) newresj rest - - | _ -> - let hj = pretype empty_tycon env isevars lvar c in - error_cant_apply_not_functional_loc - (join_loc floc argloc) env (evars_of !isevars) - resj [hj] - in let resj = apply_rec env 1 fj args in - inh_conv_coerce_to_tycon loc env isevars resj tycon - - | RLambda(loc,name,c1,c2) -> - let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in - let dom_valcon = valcon_of_tycon dom in - let j = pretype_type dom_valcon env isevars lvar c1 in - let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) isevars lvar c2 in - judge_of_abstraction env name j j' - - | RProd(loc,name,c1,c2) -> - let j = pretype_type empty_valcon env isevars lvar c1 in - let var = (name,j.utj_val) in - let env' = push_rel_assum var env in - let j' = pretype_type empty_valcon env' isevars lvar c2 in - let resj = - try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in - inh_conv_coerce_to_tycon loc env isevars resj tycon - - | RLetIn(loc,name,c1,c2) -> - let j = pretype empty_tycon env isevars lvar c1 in - let t = refresh_universes j.uj_type in - let var = (name,Some j.uj_val,t) in - let tycon = option_app (lift 1) tycon in - let j' = pretype tycon (push_rel var env) isevars lvar c2 in - { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; - uj_type = subst1 j.uj_val j'.uj_type } - - | RLetTuple (loc,nal,(na,po),c,d) -> - let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type - with Not_found -> - let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) cj - in - let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn,_ = get_arity env indf in - let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let nar = List.length arsgn in - (match po with - | Some p -> - let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar (evars_of !isevars) pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) - let p = it_mkLambda_or_LetIn ccl psign in - let inst = - (Array.to_list cs.cs_concl_realargs) - @[build_dependent_constructor cs] in - let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env (evars_of !isevars) lp inst in - let fj = pretype (mk_tycon fty) env_f isevars lvar d in - let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in - mkCase (ci, p, cj.uj_val,[|f|]) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } - - | None -> - let tycon = option_app (lift cs.cs_nargs) tycon in - let fj = pretype tycon env_f isevars lvar d in - let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar (evars_of !isevars) fj.uj_type in - let ccl = - if noccur_between 1 cs.cs_nargs ccl then - lift (- cs.cs_nargs) ccl - else - error_cant_find_case_type_loc loc env (evars_of !isevars) - cj.uj_val in - let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in - mkCase (ci, p, cj.uj_val,[|f|] ) - in - { uj_val = v; uj_type = ccl }) - - | RIf (loc,c,(na,po),b1,b2) -> - let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type - with Not_found -> - let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) cj in - let cstrs = get_constructors env indf in - if Array.length cstrs <> 2 then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors"); - - (* Make dependencies from arity signature possible ! *) - let arsgn,_ = get_arity env indf in - let arsgn = List.map (fun (n,b,t) -> - debug 2 (str "If case arg: " ++ Nameops.pr_name n); - (n,b,t)) arsgn in - let nar = List.length arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let pred,p = match po with - | Some p -> - let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar (evars_of !isevars) pj.utj_val in - let pred = it_mkLambda_or_LetIn ccl psign in - pred, lift (- nar) (beta_applist (pred,[cj.uj_val])) - | None -> - let p = match tycon with - | Some ty -> ty - | None -> - e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) - in - it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let f cs b = - let n = rel_context_length cs.cs_args in - let pi = liftn n 2 pred in - let pi = beta_applist (pi, [build_dependent_constructor cs]) in - let csgn = - List.map (fun (n,b,t) -> - match n with - Name _ -> (n, b, t) - | Anonymous -> (Name (id_of_string "H"), b, t)) - cs.cs_args - in - let env_c = push_rels csgn env in - let bj = pretype (Some pi) env_c isevars lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in - let b1 = f cstrs.(0) b1 in - let b2 = f cstrs.(1) b2 in - let pred = nf_evar (evars_of !isevars) pred in - let p = nf_evar (evars_of !isevars) p in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env IfStyle mis in - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) - in - { uj_val = v; uj_type = p } - - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc - ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) - tycon env (* loc *) (po,tml,eqns) - - | RCast(loc,c,k,t) -> - let tj = pretype_type empty_tycon env isevars lvar t in - let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in - (* User Casts are for helping pretyping, experimentally not to be kept*) - (* ... except for Correctness *) - let v = mkCast (cj.uj_val, k, tj.utj_val) in - let cj = { uj_val = v; uj_type = tj.utj_val } in - inh_conv_coerce_to_tycon loc env isevars cj tycon - - | RDynamic (loc,d) -> - if (tag d) = "constr" then - let c = Pretyping.constr_out d in - let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in - j - (*inh_conv_coerce_to_tycon loc env isevars j tycon*) - else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic")) - -(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *) -and pretype_type valcon env isevars lvar = function - | RHole loc -> - (match valcon with - | Some v -> - let s = - let sigma = evars_of !isevars in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | Evar v when is_Type (existential_type sigma v) -> - evd_comb1 (define_evar_as_sort) isevars v - | _ -> anomaly "Found a type constraint which is not a type" - in - { utj_val = v; - utj_type = s } - | None -> - let s = new_Type_sort () in - { utj_val = e_new_evar isevars env ~src:loc (mkSort s); - utj_type = s}) - | c -> - let j = pretype empty_tycon env isevars lvar c in - let loc = loc_of_rawconstr c in - let tj = evd_comb1 (inh_coerce_to_sort loc env) isevars j in - match valcon with - | None -> tj - | Some v -> - if e_cumul env isevars v tj.utj_val then tj - else - (debug 2 (str "here we are"); - error_unexpected_type_loc - (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v) - - - -let merge_evms x y = - Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y - -let interp env isevars c tycon = - let j = pretype tycon env isevars ([],[]) c in - j.uj_val, j.uj_type - -let find_with_index x l = - let rec aux i = function - (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let list_split_at index l = - let rec aux i acc = function - hd :: tl when i = index -> (List.rev acc), tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - -open Vernacexpr - -let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env -let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env - -let env_with_binders env isevars l = - let rec aux ((env, rels) as acc) = function - Topconstr.LocalRawDef ((loc, name), def) :: tl -> - let rawdef = coqintern !isevars env def in - let coqdef, deftyp = interp env isevars rawdef empty_tycon in - let reldecl = (name, Some coqdef, deftyp) in - aux (push_rel reldecl env, reldecl :: rels) tl - | Topconstr.LocalRawAssum (bl, typ) :: tl -> - let rawtyp = coqintern !isevars env typ in - let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in - let acc = - List.fold_left (fun (env, rels) (loc, name) -> - let reldecl = (name, None, coqtyp) in - (push_rel reldecl env, - reldecl :: rels)) - (env, rels) bl - in aux acc tl - | [] -> acc - in aux (env, []) l - -let subtac_process env isevars id l c tycon = - let evars () = evars_of !isevars in - let _ = trace (str "Creating env with binders") in - let env_binders, binders_rel = env_with_binders env isevars l in - let _ = trace (str "New env created:" ++ my_print_context env_binders) in - let tycon = - match tycon with - None -> empty_tycon - | Some t -> - let t = coqintern !isevars env_binders t in - let _ = trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) in - let coqt, ttyp = interp env_binders isevars t empty_tycon in - let _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) in - mk_tycon coqt - in - let c = coqintern !isevars env_binders c in - let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in - let coqc, ctyp = interp env_binders isevars c tycon in - let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ - str "Coq type: " ++ my_print_constr env_binders ctyp) - in - let _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) in - - let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel - and fullctyp = it_mkProd_or_LetIn ctyp binders_rel - in - let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in - let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in - - let _ = trace (str "After evar normalization: " ++ spc () ++ - str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () - ++ str "Coq type: " ++ my_print_constr env fullctyp) - in - let evm = non_instanciated_map env isevars in - let _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in - evm, fullcoqc, fullctyp - -let pretype_gen isevars env lvar kind c = - let c' = match kind with - | OfType exptyp -> - let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env isevars lvar c).uj_val - | IsType -> - (pretype_type empty_valcon env isevars lvar c).utj_val in - nf_evar (evars_of !isevars) c' - -(* [check_evars] fails if some unresolved evar remains *) -(* it assumes that the defined existentials have already been substituted - (should be done in unsafe_infer and unsafe_infer_type) *) - -let check_evars env initial_sigma isevars c = - let sigma = evars_of !isevars in - let rec proc_rec c = - match kind_of_term c with - | Evar (ev,args) -> - assert (Evd.in_dom sigma ev); - if not (Evd.in_dom initial_sigma ev) then - let (loc,k) = evar_source ev !isevars in - let _ = trace (str "Evar " ++ int ev ++ str " not solved, applied to args : " ++ - Scoq.print_args env args ++ str " in evar map: " ++ - Evd.pr_evar_map sigma) - in - error_unsolvable_implicit loc env sigma k - | _ -> iter_constr proc_rec c - in - proc_rec c(*; - let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in - if pbs <> [] then begin - pperrnl - (str"TYPING OF "++Termops.print_constr_env env c++fnl()++ - prlist_with_sep fnl - (fun (pb,c1,c2) -> - Termops.print_constr c1 ++ - (if pb=Reduction.CUMUL then str " <="++ spc() - else str" =="++spc()) ++ - Termops.print_constr c2) - pbs ++ fnl()) - end*) - -(* TODO: comment faire remonter l'information si le typage a resolu des - variables du sigma original. il faudrait que la fonction de typage - retourne aussi le nouveau sigma... -*) - -let understand_judgment isevars env c = - let j = pretype empty_tycon env isevars ([],[]) c in - let j = j_nf_evar (evars_of !isevars) j in - check_evars env (Evd.evars_of !isevars) isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j - -(* Raw calls to the unsafe inference machine: boolean says if we must - fail on unresolved evars; the unsafe_judgment list allows us to - extend env with some bindings *) - -let ise_pretype_gen fail_evar isevars env lvar kind c : Evd.open_constr = - let c = pretype_gen isevars env lvar kind c in - if fail_evar then check_evars env (Evd.evars_of !isevars) isevars c; - let c = nf_evar (evars_of !isevars) c in - let evm = non_instanciated_map env isevars in - (evm, c) - -(** Entry points of the high-level type synthesis algorithm *) - -let understand_gen kind isevars env c = - ise_pretype_gen false isevars env ([],[]) kind c - -let understand isevars env ?expected_type:exptyp c = - ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c - -let understand_type isevars env c = - ise_pretype_gen false isevars env ([],[]) IsType c - -let understand_ltac isevars env lvar kind c = - ise_pretype_gen false isevars env lvar kind c - -let understand_tcc isevars env ?expected_type:exptyp c = - ise_pretype_gen false isevars env ([],[]) (OfType exptyp) c - - - diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index c34338236d..12755960ef 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -33,7 +33,7 @@ open Dyn open Vernacexpr open Subtac_coercion -open Scoq +open Subtac_utils open Coqlib open Printer open Subtac_errors @@ -46,7 +46,7 @@ let require_library dirpath = let subtac_one_fixpoint env isevars (f, decl) = let ((id, n, bl, typ, body), decl) = - Interp_fixpoint.rewrite_fixpoint env [] (f, decl) + Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) in let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++ Ppconstr.pr_constr_expr body) @@ -125,13 +125,13 @@ let subtac (loc, command) = let isevars = ref (create_evar_defs Evd.empty) in (match expr with ProveBody (bl, c) -> - let evm, c, ctyp = Interp.subtac_process env isevars id bl c None in + let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in trace (str "Starting proof"); Command.start_proof id goal_kind c hook; trace (str "Started proof"); | DefineBody (bl, _, c, tycon) -> - let evm, c, ctyp = Interp.subtac_process env isevars id bl c tycon in + let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c tycon in let tac = Eterm.etermtac (evm, c) in trace (str "Starting proof"); Command.start_proof id goal_kind ctyp hook; diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli new file mode 100644 index 0000000000..a0d2fb2b9e --- /dev/null +++ b/contrib/subtac/subtac.mli @@ -0,0 +1,14 @@ +val require_library : string -> unit +val subtac_one_fixpoint : + 'a -> + 'b -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c +val subtac_fixpoint : 'a -> 'b -> unit +val subtac : Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 015eb5d171..c605314018 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -22,7 +22,7 @@ open Retyping open Evd open Global -open Scoq +open Subtac_utils open Coqlib open Printer open Subtac_errors @@ -33,340 +33,343 @@ open Pp let pair_of_array a = (a.(0), a.(1)) let make_name s = Name (id_of_string s) -exception NoCoercion +module Coercion = struct -let rec disc_subset x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Ind i -> - let len = Array.length l in - let sig_ = Lazy.force sig_ in - if len = 2 && i = Term.destInd sig_.typ - then - let (a, b) = pair_of_array l in - Some (a, b) - else None - | _ -> None) - | _ -> None - -and disc_exist env x = - trace (str "Disc_exist: " ++ my_print_constr env x); - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Construct c -> - if c = Term.destConstruct (Lazy.force sig_).intro - then Some (l.(0), l.(1), l.(2), l.(3)) - else None - | _ -> None) - | _ -> None + exception NoCoercion + let rec disc_subset x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + let sig_ = Lazy.force sig_ in + if len = 2 && i = Term.destInd sig_.typ + then + let (a, b) = pair_of_array l in + Some (a, b) + else None + | _ -> None) + | _ -> None + + and disc_exist env x = + trace (str "Disc_exist: " ++ my_print_constr env x); + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Construct c -> + if c = Term.destConstruct (Lazy.force sig_).intro + then Some (l.(0), l.(1), l.(2), l.(3)) + else None + | _ -> None) + | _ -> None -let disc_proj_exist env x = - trace (str "disc_proj_exist: " ++ my_print_constr env x); - match kind_of_term x with - | App (c, l) -> - (if Term.eq_constr c (Lazy.force sig_).proj1 - && Array.length l = 3 - then disc_exist env l.(2) - else None) - | _ -> None + let disc_proj_exist env x = + trace (str "disc_proj_exist: " ++ my_print_constr env x); + match kind_of_term x with + | App (c, l) -> + (if Term.eq_constr c (Lazy.force sig_).proj1 + && Array.length l = 3 + then disc_exist env l.(2) + else None) + | _ -> None -let sort_rel s1 s2 = - match s1, s2 with - Prop Pos, Prop Pos -> Prop Pos - | Prop Pos, Prop Null -> Prop Null - | Prop Null, Prop Null -> Prop Null - | Prop Null, Prop Pos -> Prop Pos - | Type _, Prop Pos -> Prop Pos - | Type _, Prop Null -> Prop Null - | _, Type _ -> s2 -let rec mu env isevars t = - let rec aux v = - match disc_subset v with - Some (u, p) -> - let f, ct = aux u in - (Some (fun x -> - app_opt f (mkApp ((Lazy.force sig_).proj1, - [| u; p; x |]))), - ct) - | None -> (None, t) - in aux t + let sort_rel s1 s2 = + match s1, s2 with + Prop Pos, Prop Pos -> Prop Pos + | Prop Pos, Prop Null -> Prop Null + | Prop Null, Prop Null -> Prop Null + | Prop Null, Prop Pos -> Prop Pos + | Type _, Prop Pos -> Prop Pos + | Type _, Prop Null -> Prop Null + | _, Type _ -> s2 -and coerce loc env isevars (x : Term.constr) (y : Term.constr) - : (Term.constr -> Term.constr) option - = - trace (str "Coerce called for " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y); + let rec mu env isevars t = + let rec aux v = + match disc_subset v with + Some (u, p) -> + let f, ct = aux u in + (Some (fun x -> + app_opt f (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |]))), + ct) + | None -> (None, t) + in aux t - let rec coerce_unify env x y = - if e_cumul env isevars x y then ( - trace (str "Unified " ++ (my_print_constr env x) ++ + and coerce loc env isevars (x : Term.constr) (y : Term.constr) + : (Term.constr -> Term.constr) option + = + trace (str "Coerce called for " ++ (my_print_constr env x) ++ str " and "++ my_print_constr env y); - None - ) else coerce' env x y (* head recutions needed *) - and coerce' env x y : (Term.constr -> Term.constr) option = - let subco () = subset_coerce env x y in - trace (str "coerce' from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y); - match (kind_of_term x, kind_of_term y) with - | Sort s, Sort s' -> - (match s, s' with - Prop x, Prop y when x = y -> None - | Prop _, Type _ -> None - | Type x, Type y when x = y -> None (* false *) - | _ -> subco ()) - | Prod (name, a, b), Prod (name', a', b') -> - let c1 = coerce_unify env a' a in - let env' = push_rel (name', None, a') env in - let c2 = coerce_unify env' b b' in - (match c1, c2 with - None, None -> failwith "subtac.coerce': Should have detected equivalence earlier" - | _, _ -> - Some - (fun f -> - mkLambda (name', a', - app_opt c2 - (mkApp (Term.lift 1 f, - [| app_opt c1 (mkRel 1) |]))))) - - | App (c, l), App (c', l') -> - (match kind_of_term c, kind_of_term c' with - Ind i, Ind i' -> - let len = Array.length l in - let existS = Lazy.force existS in - if len = Array.length l' && len = 2 - && i = i' && i = Term.destInd existS.typ - then - begin (* Sigma types *) - debug 1 (str "In coerce sigma types"); - let (a, pb), (a', pb') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let remove_head c = - let (_, _, x) = Term.destProd c in - x - in - let b, b' = remove_head pb, remove_head pb' in - let env' = push_rel (make_name "x", None, a) env in - let c2 = coerce_unify env' b b' in - match c1, c2 with - None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt c1 (mkApp (existS.proj1, - [| a; pb; x |])), - app_opt c2 (mkApp (existS.proj2, - [| a; pb'; x |])) - in - mkApp (existS.intro, [| x ; y |])) - end - else subco () - | _ -> subco ()) - | _, _ -> subco () - and subset_coerce env x y = - match disc_subset x with - Some (u, p) -> - let c = coerce_unify env u y in - let f x = - app_opt c (mkApp ((Lazy.force sig_).proj1, - [| u; p; x |])) - in Some f - | None -> - match disc_subset y with - Some (u, p) -> - let c = coerce_unify env x u in - Some - (fun x -> - let cx = app_opt c x in - let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |])) - in - (mkApp - ((Lazy.force sig_).intro, - [| u; p; cx; evar |]))) - | None -> raise NoCoercion - in coerce_unify env x y + let rec coerce_unify env x y = + if e_cumul env isevars x y then ( + trace (str "Unified " ++ (my_print_constr env x) ++ + str " and "++ my_print_constr env y); + None + ) else coerce' env x y (* head recutions needed *) + and coerce' env x y : (Term.constr -> Term.constr) option = + let subco () = subset_coerce env x y in + trace (str "coerce' from " ++ (my_print_constr env x) ++ + str " to "++ my_print_constr env y); + match (kind_of_term x, kind_of_term y) with + | Sort s, Sort s' -> + (match s, s' with + Prop x, Prop y when x = y -> None + | Prop _, Type _ -> None + | Type x, Type y when x = y -> None (* false *) + | _ -> subco ()) + | Prod (name, a, b), Prod (name', a', b') -> + let c1 = coerce_unify env a' a in + let env' = push_rel (name', None, a') env in + let c2 = coerce_unify env' b b' in + (match c1, c2 with + None, None -> failwith "subtac.coerce': Should have detected equivalence earlier" + | _, _ -> + Some + (fun f -> + mkLambda (name', a', + app_opt c2 + (mkApp (Term.lift 1 f, + [| app_opt c1 (mkRel 1) |]))))) + + | App (c, l), App (c', l') -> + (match kind_of_term c, kind_of_term c' with + Ind i, Ind i' -> + let len = Array.length l in + let existS = Lazy.force existS in + if len = Array.length l' && len = 2 + && i = i' && i = Term.destInd existS.typ + then + begin (* Sigma types *) + debug 1 (str "In coerce sigma types"); + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let c1 = coerce_unify env a a' in + let remove_head c = + let (_, _, x) = Term.destProd c in + x + in + let b, b' = remove_head pb, remove_head pb' in + let env' = push_rel (make_name "x", None, a) env in + let c2 = coerce_unify env' b b' in + match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun x -> + let x, y = + app_opt c1 (mkApp (existS.proj1, + [| a; pb; x |])), + app_opt c2 (mkApp (existS.proj2, + [| a; pb'; x |])) + in + mkApp (existS.intro, [| x ; y |])) + end + else subco () + | _ -> subco ()) + | _, _ -> subco () -let coerce_itf loc env isevars hj c1 = - let {uj_val = v; uj_type = t} = hj in - let evars = ref isevars in - let coercion = coerce loc env evars t c1 in - !evars, {uj_val = app_opt coercion v; - uj_type = t} - -(* Taken from pretyping/coercion.ml *) + and subset_coerce env x y = + match disc_subset x with + Some (u, p) -> + let c = coerce_unify env u y in + let f x = + app_opt c (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |])) + in Some f + | None -> + match disc_subset y with + Some (u, p) -> + let c = coerce_unify env x u in + Some + (fun x -> + let cx = app_opt c x in + let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |])) + in + (mkApp + ((Lazy.force sig_).intro, + [| u; p; cx; evar |]))) + | None -> raise NoCoercion + in coerce_unify env x y -(* Typing operations dealing with coercions *) + let coerce_itf loc env isevars hj c1 = + let {uj_val = v; uj_type = t} = hj in + let evars = ref isevars in + let coercion = coerce loc env evars t c1 in + !evars, {uj_val = app_opt coercion v; + uj_type = t} + + (* Taken from pretyping/coercion.ml *) -let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) + (* Typing operations dealing with coercions *) -(* Here, funj is a coercion therefore already typed in global context *) -let apply_coercion_args env argl funj = - let rec apply_rec acc typ = function - | [] -> { uj_val = applist (j_val funj,argl); - uj_type = typ } - | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env Evd.empty typ) with - | Prod (_,c1,c2) -> - (* Typage garanti par l'appel à app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" - in - apply_rec [] funj.uj_type argl + let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) -exception NoCoercion + (* Here, funj is a coercion therefore already typed in global context *) + let apply_coercion_args env argl funj = + let rec apply_rec acc typ = function + | [] -> { uj_val = applist (j_val funj,argl); + uj_type = typ } + | h::restl -> + (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *) + match kind_of_term (whd_betadeltaiota env Evd.empty typ) with + | Prod (_,c1,c2) -> + (* Typage garanti par l'appel à app_coercion*) + apply_rec (h::acc) (subst1 h c2) restl + | _ -> anomaly "apply_coercion_args" + in + apply_rec [] funj.uj_type argl -(* appliquer le chemin de coercions de patterns p *) + exception NoCoercion -let apply_pattern_coercion loc pat p = - List.fold_left - (fun pat (co,n) -> - let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in - Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) - pat p + (* appliquer le chemin de coercions de patterns p *) -(* raise Not_found if no coercion found *) -let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in - apply_pattern_coercion loc pat p + let apply_pattern_coercion loc pat p = + List.fold_left + (fun pat (co,n) -> + let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in + Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) + pat p -(* appliquer le chemin de coercions p à hj *) + (* raise Not_found if no coercion found *) + let inh_pattern_coerce_to loc pat ind1 ind2 = + let i1 = inductive_class_of ind1 in + let i2 = inductive_class_of ind2 in + let p = lookup_pattern_path_between (i1,i2) in + apply_pattern_coercion loc pat p -let apply_coercion env p hj typ_cl = - try - fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if isid then - { uj_val = ja.uj_val; uj_type = jres.uj_type } - else - jres), - jres.uj_type) - (hj,typ_cl) p) - with _ -> anomaly "apply_coercion" + (* appliquer le chemin de coercions p à hj *) -let inh_app_fun env isevars j = - let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in - match kind_of_term t with - | Prod (_,_,_) -> (isevars,j) - | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',t) = define_evar_as_arrow isevars ev in - (isevars',{ uj_val = j.uj_val; uj_type = t }) - | _ -> - (try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_fun_from i1 in - (isevars,apply_coercion env p j t) - with Not_found -> - try - let coercef, t = mu env isevars t in - (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t }) - with NoCoercion -> - (isevars,j)) + let apply_coercion env p hj typ_cl = + try + fst (List.fold_left + (fun (ja,typ_cl) i -> + let fv,isid = coercion_value i in + let argl = (class_args_of typ_cl)@[ja.uj_val] in + let jres = apply_coercion_args env argl fv in + (if isid then + { uj_val = ja.uj_val; uj_type = jres.uj_type } + else + jres), + jres.uj_type) + (hj,typ_cl) p) + with _ -> anomaly "apply_coercion" -let inh_tosort_force loc env isevars j = - try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in - (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) - with Not_found -> - error_not_a_type_loc loc env (evars_of isevars) j + let inh_app_fun env isevars j = + let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in + match kind_of_term t with + | Prod (_,_,_) -> (isevars,j) + | Evar ev when not (is_defined_evar isevars ev) -> + let (isevars',t) = define_evar_as_arrow isevars ev in + (isevars',{ uj_val = j.uj_val; uj_type = t }) + | _ -> + (try + let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let p = lookup_path_to_fun_from i1 in + (isevars,apply_coercion env p j t) + with Not_found -> + try + let coercef, t = mu env isevars t in + (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t }) + with NoCoercion -> + (isevars,j)) -let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in - match kind_of_term typ with - | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) - | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',s) = define_evar_as_sort isevars ev in - (isevars',{ utj_val = j.uj_val; utj_type = s }) - | _ -> - inh_tosort_force loc env isevars j + let inh_tosort_force loc env isevars j = + try + let t,i1 = class_of1 env (evars_of isevars) j.uj_type in + let p = lookup_path_to_sort_from i1 in + let j1 = apply_coercion env p j t in + (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) + with Not_found -> + error_not_a_type_loc loc env (evars_of isevars) j -let inh_coerce_to_fail env isevars c1 hj = - let hj' = - try - let t1,i1 = class_of1 env (evars_of isevars) c1 in - let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in - let p = lookup_path_between (i2,i1) in - apply_coercion env p hj t2 - with Not_found -> raise NoCoercion - in - try (the_conv_x_leq env hj'.uj_type c1 isevars, hj') - with Reduction.NotConvertible -> raise NoCoercion + let inh_coerce_to_sort loc env isevars j = + let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in + match kind_of_term typ with + | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) + | Evar ev when not (is_defined_evar isevars ev) -> + let (isevars',s) = define_evar_as_sort isevars ev in + (isevars',{ utj_val = j.uj_val; utj_type = s }) + | _ -> + inh_tosort_force loc env isevars j -let rec inh_conv_coerce_to_fail env isevars hj c1 = - let {uj_val = v; uj_type = t} = hj in - try (the_conv_x_leq env t c1 isevars, hj) - with Reduction.NotConvertible -> - (try - inh_coerce_to_fail env isevars c1 hj - with NoCoercion -> - (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), - kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with - | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = whd_betadeltaiota env (evars_of isevars) v in - let (evd',b) = - match kind_of_term v' with - | Lambda (_,v1,v2) -> - (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *) - with Reduction.NotConvertible -> (isevars, false)) - | _ -> (isevars,false) in - if b - then - let (x,v1,v2) = destLambda v' in - let env1 = push_rel (x,None,v1) env in - let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' + let inh_coerce_to_fail env isevars c1 hj = + let hj' = + try + let t1,i1 = class_of1 env (evars_of isevars) c1 in + let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in + let p = lookup_path_between (i2,i1) in + apply_coercion env p hj t2 + with Not_found -> raise NoCoercion + in + try (the_conv_x_leq env hj'.uj_type c1 isevars, hj') + with Reduction.NotConvertible -> raise NoCoercion + + let rec inh_conv_coerce_to_fail env isevars hj c1 = + let {uj_val = v; uj_type = t} = hj in + try (the_conv_x_leq env t c1 isevars, hj) + with Reduction.NotConvertible -> + (try + inh_coerce_to_fail env isevars c1 hj + with NoCoercion -> + (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), + kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with + | Prod (_,t1,t2), Prod (name,u1,u2) -> + let v' = whd_betadeltaiota env (evars_of isevars) v in + let (evd',b) = + match kind_of_term v' with + | Lambda (_,v1,v2) -> + (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *) + with Reduction.NotConvertible -> (isevars, false)) + | _ -> (isevars,false) in + if b + then + let (x,v1,v2) = destLambda v' in + let env1 = push_rel (x,None,v1) env in + let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' {uj_val = v2; uj_type = t2 } u2 in - (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val); - uj_type = mkProd (x, v1, h2.uj_type) }) - else - (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) - (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) - (* has type (name:u1)u2 (with v' recursively obtained) *) - let name = (match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = push_rel (name,None,u1) env in - let (evd',h1) = - inh_conv_coerce_to_fail env1 isevars - {uj_val = mkRel 1; uj_type = (lift 1 u1) } - (lift 1 t1) in - let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' - { uj_val = mkApp (lift 1 v, [|h1.uj_val|]); - uj_type = subst1 h1.uj_val t2 } + (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val); + uj_type = mkProd (x, v1, h2.uj_type) }) + else + (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) + (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *) + (* has type (name:u1)u2 (with v' recursively obtained) *) + let name = (match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name) in + let env1 = push_rel (name,None,u1) env in + let (evd',h1) = + inh_conv_coerce_to_fail env1 isevars + {uj_val = mkRel 1; uj_type = (lift 1 u1) } + (lift 1 t1) in + let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' + { uj_val = mkApp (lift 1 v, [|h1.uj_val|]); + uj_type = subst1 h1.uj_val t2 } u2 - in - (evd'', - { uj_val = mkLambda (name, u1, h2.uj_val); - uj_type = mkProd (name, u1, h2.uj_type) }) - | _ -> raise NoCoercion)) + in + (evd'', + { uj_val = mkLambda (name, u1, h2.uj_val); + uj_type = mkProd (name, u1, h2.uj_type) }) + | _ -> raise NoCoercion)) -(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to loc env isevars cj t = - trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ - str " and "++ my_print_constr env t); - let (evd',cj') = - try - inh_conv_coerce_to_fail env isevars cj t - with NoCoercion -> - try - coerce_itf loc env isevars cj t + (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) + let inh_conv_coerce_to loc env isevars cj t = + trace (str "inh_conv_coerce_to called for " ++ (my_print_constr env cj.uj_type) ++ + str " and "++ my_print_constr env t); + let (evd',cj') = + try + inh_conv_coerce_to_fail env isevars cj t with NoCoercion -> - let sigma = evars_of isevars in - debug 2 (str "No coercion found"); - error_actual_type_loc loc env sigma cj t - in - (evd',{ uj_val = cj'.uj_val; uj_type = t }) + try + coerce_itf loc env isevars cj t + with NoCoercion -> + let sigma = evars_of isevars in + debug 2 (str "No coercion found"); + error_actual_type_loc loc env sigma cj t + in + (evd',{ uj_val = cj'.uj_val; uj_type = t }) +end diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli new file mode 100644 index 0000000000..53a8d21338 --- /dev/null +++ b/contrib/subtac/subtac_coercion.mli @@ -0,0 +1 @@ +module Coercion : Coercion.S diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 34eff9a176..64aee76119 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -34,15 +34,14 @@ open Mod_subst open Printer open Inductiveops open Syntax_def -open Pretyping open Tacinterp open Vernacexpr open Notation -open Interp -open Scoq - +module SPretyping = Subtac_pretyping.Pretyping +open Subtac_utils +open Pretyping (*********************************************************************) (* Functions to parse and interpret constructions *) @@ -50,11 +49,10 @@ open Scoq let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = - let c' = Constrintern.intern_gen (kind=Pretyping.IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c'' = Interp_fixpoint.rewrite_cases c' in - understand_gen kind isevars env c'' + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in + let c'' = Subtac_interp_fixpoint.rewrite_cases c' in + Evd.evars_of !isevars, SPretyping.pretype_gen isevars env ([],[]) kind c'' - let interp_constr isevars env c = interp_gen (OfType None) isevars env c @@ -65,10 +63,14 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = - understand_tcc isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c) + SPretyping.pretype_gen isevars env ([], []) (OfType None) + (Constrintern.intern_constr (Evd.evars_of !isevars) env c) let interp_constr_judgment isevars env c = - understand_judgment isevars env (Constrintern.intern_constr (Evd.evars_of !isevars) env c) + let s, j = SPretyping.understand_judgment_tcc (Evd.evars_of !isevars) env + (Constrintern.intern_constr (Evd.evars_of !isevars) env c) + in + Evd.create_evar_defs s, j (* try to find non recursive definitions *) @@ -118,7 +120,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed and protos = List.map (fun ((f, n, _, _, _),_) -> f,n) lnameargsardef in let lnameargsardef = - List.map (fun (f, d) -> Interp_fixpoint.rewrite_fixpoint env0 protos (f, d)) + List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d)) lnameargsardef in let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli new file mode 100644 index 0000000000..23a03290c8 --- /dev/null +++ b/contrib/subtac/subtac_command.mli @@ -0,0 +1,103 @@ +module SPretyping : + sig + module Cases : + sig + val compile_cases : + Util.loc -> + (Evarutil.type_constraint -> + Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) * + Evd.evar_defs ref -> + Evarutil.type_constraint -> + Environ.env -> + Rawterm.rawconstr option * + (Rawterm.rawconstr * + (Names.name * + (Util.loc * Names.inductive * Names.name list) option)) + list * + (Util.loc * Names.identifier list * Rawterm.cases_pattern list * + Rawterm.rawconstr) + list -> Environ.unsafe_judgment + end + val understand_tcc : + Evd.evar_map -> + Environ.env -> + ?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr + val understand_ltac : + Evd.evar_map -> + Environ.env -> + Pretyping.var_map * Pretyping.unbound_ltac_var_map -> + Pretyping.typing_constraint -> + Rawterm.rawconstr -> Evd.evar_defs * Term.constr + val understand : + Evd.evar_map -> + Environ.env -> + ?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr + val understand_type : + Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr + val understand_gen : + Pretyping.typing_constraint -> + Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr + val understand_judgment : + Evd.evar_map -> + Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment + val understand_judgment_tcc : + Evd.evar_map -> + Environ.env -> + Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment + val pretype : + Evarutil.type_constraint -> + Environ.env -> + Evd.evar_defs ref -> + Pretyping.var_map * (Names.identifier * Names.identifier option) list -> + Rawterm.rawconstr -> Environ.unsafe_judgment + val pretype_type : + Evarutil.val_constraint -> + Environ.env -> + Evd.evar_defs ref -> + Pretyping.var_map * (Names.identifier * Names.identifier option) list -> + Rawterm.rawconstr -> Environ.unsafe_type_judgment + val pretype_gen : + Evd.evar_defs ref -> + Environ.env -> + Pretyping.var_map * (Names.identifier * Names.identifier option) list -> + Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr + end +val interp_gen : + Pretyping.typing_constraint -> + Evd.evar_defs ref -> + Environ.env -> + ?impls:Constrintern.full_implicits_env -> + ?allow_soapp:bool -> + ?ltacvars:Constrintern.ltac_sign -> + Topconstr.constr_expr -> Evd.evar_map * Term.constr +val interp_constr : + Evd.evar_defs ref -> + Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr +val interp_type : + Evd.evar_defs ref -> + Environ.env -> + ?impls:Constrintern.full_implicits_env -> + Topconstr.constr_expr -> Evd.evar_map * Term.constr +val interp_casted_constr : + Evd.evar_defs ref -> + Environ.env -> + ?impls:Constrintern.full_implicits_env -> + Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr +val interp_open_constr : + Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr +val interp_constr_judgment : + Evd.evar_defs ref -> + Environ.env -> + Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment +val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list +val collect_non_rec : + Environ.env -> + Names.identifier list -> + ('a * Term.types) list -> + 'b list -> + 'c list -> + (Names.identifier * ('a * Term.types) * 'b) list * + (Names.identifier array * ('a * Term.types) array * 'b array * 'c array) +val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds +val build_recursive : + (Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_errors.mli b/contrib/subtac/subtac_errors.mli new file mode 100644 index 0000000000..8d75b9c017 --- /dev/null +++ b/contrib/subtac/subtac_errors.mli @@ -0,0 +1,15 @@ +type term_pp = Pp.std_ppcmds +type subtyping_error = + UncoercibleInferType of Util.loc * term_pp * term_pp + | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp + | UncoercibleRewrite of term_pp * term_pp +type typing_error = + NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp + | NonConvertible of Util.loc * term_pp * term_pp + | NonSigma of Util.loc * term_pp + | IllSorted of Util.loc * term_pp +exception Subtyping_error of subtyping_error +exception Typing_error of typing_error +exception Debug_msg of string +val typing_error : typing_error -> 'a +val subtyping_error : subtyping_error -> 'a diff --git a/contrib/subtac/interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml index 8191357091..c668c3503b 100644 --- a/contrib/subtac/interp_fixpoint.ml +++ b/contrib/subtac/subtac_interp_fixpoint.ml @@ -23,7 +23,7 @@ open Dyn open Topconstr open Subtac_coercion -open Scoq +open Subtac_utils open Coqlib open Printer open Subtac_errors diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli new file mode 100644 index 0000000000..5a84b27730 --- /dev/null +++ b/contrib/subtac/subtac_interp_fixpoint.mli @@ -0,0 +1,42 @@ +val mkAppExplC : + Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr +val mkSubset : + Names.name Util.located -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val mkProj1 : + Topconstr.constr_expr -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val mkProj2 : + Topconstr.constr_expr -> + Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr +val list_of_local_binders : + Topconstr.local_binder list -> + (Names.name Util.located * Topconstr.constr_expr) list +val abstract_constr_expr_bl : + Topconstr.constr_expr -> + (Names.name Util.located * Topconstr.constr_expr) list -> + Topconstr.constr_expr +val pr_binder_list : + (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds +val rewrite_rec_calls : 'a -> 'b -> 'b +val rewrite_fixpoint : + 'a -> + 'b -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c -> + (Names.identifier * (int * Topconstr.recursion_order_expr) * + Topconstr.local_binder list * Topconstr.constr_expr * + Topconstr.constr_expr) * + 'c +val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list +val rewrite_cases_aux : + Util.loc * Rawterm.rawconstr option * + (Rawterm.rawconstr * + (Names.name * (Util.loc * Names.inductive * Names.name list) option)) + list * + (Util.loc * Names.identifier list * Rawterm.cases_pattern list * + Rawterm.rawconstr) + list -> Rawterm.rawconstr +val rewrite_cases : Rawterm.rawconstr -> Rawterm.rawconstr diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml new file mode 100644 index 0000000000..8dd6f9b8fe --- /dev/null +++ b/contrib/subtac/subtac_pretyping.ml @@ -0,0 +1,146 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Global +open Pp +open Util +open Names +open Sign +open Evd +open Term +open Termops +open Reductionops +open Environ +open Type_errors +open Typeops +open Libnames +open Classops +open List +open Recordops +open Evarutil +open Pretype_errors +open Rawterm +open Evarconv +open Pattern +open Dyn + +open Subtac_coercion +open Subtac_utils +open Coqlib +open Printer +open Subtac_errors +open Context +open Eterm + +module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion) +open Pretyping + +type recursion_info = { + arg_name: name; + arg_type: types; (* A *) + args_after : rel_context; + wf_relation: constr; (* R : A -> A -> Prop *) + wf_proof: constr; (* : well_founded R *) + f_type: types; (* f: A -> Set *) + f_fulltype: types; (* Type with argument and wf proof product first *) +} + +let my_print_rec_info env t = + str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++ + str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++ + str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++ + str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ + str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ + str "Full type: " ++ my_print_constr env t.f_fulltype +(* trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *) +(* str " and tycon "++ my_print_tycon env tycon ++ *) +(* str " in environment: " ++ my_print_env env); *) + +let merge_evms x y = + Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y + +let interp env isevars c tycon = + let j = pretype tycon env isevars ([],[]) c in + j.uj_val, j.uj_type + +let find_with_index x l = + let rec aux i = function + (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl + | [] -> raise Not_found + in aux 0 l + +let list_split_at index l = + let rec aux i acc = function + hd :: tl when i = index -> (List.rev acc), tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_at: Invalid argument" + in aux 0 [] l + +open Vernacexpr + +let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env +let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env + +let env_with_binders env isevars l = + let rec aux ((env, rels) as acc) = function + Topconstr.LocalRawDef ((loc, name), def) :: tl -> + let rawdef = coqintern !isevars env def in + let coqdef, deftyp = interp env isevars rawdef empty_tycon in + let reldecl = (name, Some coqdef, deftyp) in + aux (push_rel reldecl env, reldecl :: rels) tl + | Topconstr.LocalRawAssum (bl, typ) :: tl -> + let rawtyp = coqintern !isevars env typ in + let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in + let acc = + List.fold_left (fun (env, rels) (loc, name) -> + let reldecl = (name, None, coqtyp) in + (push_rel reldecl env, + reldecl :: rels)) + (env, rels) bl + in aux acc tl + | [] -> acc + in aux (env, []) l + +let subtac_process env isevars id l c tycon = + let evars () = evars_of !isevars in + let _ = trace (str "Creating env with binders") in + let env_binders, binders_rel = env_with_binders env isevars l in + let _ = trace (str "New env created:" ++ my_print_context env_binders) in + let tycon = + match tycon with + None -> empty_tycon + | Some t -> + let t = coqintern !isevars env_binders t in + let _ = trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) in + let coqt, ttyp = interp env_binders isevars t empty_tycon in + let _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) in + mk_tycon coqt + in + let c = coqintern !isevars env_binders c in + let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in + let coqc, ctyp = interp env_binders isevars c tycon in + let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ + str "Coq type: " ++ my_print_constr env_binders ctyp) + in + let _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) in + + let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel + and fullctyp = it_mkProd_or_LetIn ctyp binders_rel + in + let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in + let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in + + let _ = trace (str "After evar normalization: " ++ spc () ++ + str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () + ++ str "Coq type: " ++ my_print_constr env fullctyp) + in + let evm = non_instanciated_map env isevars in + let _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in + evm, fullcoqc, fullctyp diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli new file mode 100644 index 0000000000..97e56ecb24 --- /dev/null +++ b/contrib/subtac/subtac_pretyping.mli @@ -0,0 +1,12 @@ +open Term +open Environ +open Names +open Sign +open Evd +open Global +open Topconstr + +module Pretyping : Pretyping.S + +val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> + constr_expr -> constr_expr option -> evar_map * constr * types diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/subtac_utils.ml index eb9888c161..eb9888c161 100644 --- a/contrib/subtac/scoq.ml +++ b/contrib/subtac/subtac_utils.ml diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli new file mode 100644 index 0000000000..5bbd4639eb --- /dev/null +++ b/contrib/subtac/subtac_utils.mli @@ -0,0 +1,53 @@ +val contrib_name : string +val subtac_dir : string list +val fix_sub_module : string +val fixsub_module : string list +val init_constant : string list -> string -> Term.constr +val init_reference : string list -> string -> Libnames.global_reference +val fixsub : Term.constr lazy_t +val make_ref : string -> Libnames.reference +val well_founded_ref : Libnames.reference +val acc_ref : Libnames.reference +val acc_inv_ref : Libnames.reference +val fix_sub_ref : Libnames.reference +val lt_wf_ref : Libnames.reference +val sig_ref : Libnames.reference +val proj1_sig_ref : Libnames.reference +val proj2_sig_ref : Libnames.reference +val build_sig : unit -> Coqlib.coq_sigma_data +val sig_ : Coqlib.coq_sigma_data lazy_t +val eqind : Term.constr lazy_t +val eqind_ref : Libnames.global_reference lazy_t +val refl_equal_ref : Libnames.global_reference lazy_t +val boolind : Term.constr lazy_t +val sumboolind : Term.constr lazy_t +val natind : Term.constr lazy_t +val intind : Term.constr lazy_t +val existSind : Term.constr lazy_t +val existS : Coqlib.coq_sigma_data lazy_t +val well_founded : Term.constr lazy_t +val fix : Term.constr lazy_t +val extconstr : Term.constr -> Topconstr.constr_expr +val extsort : Term.sorts -> Topconstr.constr_expr +val my_print_constr : Environ.env -> Term.constr -> Pp.std_ppcmds +val my_print_context : Environ.env -> Pp.std_ppcmds +val my_print_env : Environ.env -> Pp.std_ppcmds +val my_print_rawconstr : Environ.env -> Rawterm.rawconstr -> Pp.std_ppcmds +val debug_level : int ref +val debug : int -> Pp.std_ppcmds -> unit +val debug_msg : int -> Pp.std_ppcmds -> Pp.std_ppcmds +val trace : Pp.std_ppcmds -> unit +val wf_relations : (Term.constr, Term.constr lazy_t) Hashtbl.t +val std_relations : unit Lazy.t +type binders = Topconstr.local_binder list +val app_opt : ('a -> 'a) option -> 'a -> 'a +val print_args : Environ.env -> Term.constr array -> Pp.std_ppcmds +val make_existential : + Util.loc -> Environ.env -> Evd.evar_defs ref -> Term.types -> Term.constr +val make_existential_expr : Util.loc -> 'a -> 'b -> Topconstr.constr_expr +val string_of_hole_kind : Evd.hole_kind -> string +val non_instanciated_map : Environ.env -> Evd.evar_defs ref -> Evd.evar_map +val global_kind : Decl_kinds.logical_kind +val goal_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind +val global_fix_kind : Decl_kinds.logical_kind +val goal_fix_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind |