diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 1617 |
1 files changed, 654 insertions, 963 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bb0e74bb..2d1e297f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml,v 1.123.2.5 2005/11/29 21:40:52 letouzey Exp $ *) +(* $Id: pretyping.ml 8695 2006-04-10 16:33:52Z msozeau $ *) open Pp open Util @@ -20,6 +20,7 @@ open Environ open Type_errors open Typeops open Libnames +open Nameops open Classops open List open Recordops @@ -27,86 +28,18 @@ open Evarutil open Pretype_errors open Rawterm open Evarconv -open Coercion open Pattern open Dyn +type typing_constraint = OfType of types option | IsType +type var_map = (identifier * unsafe_judgment) list +type unbound_ltac_var_map = (identifier * identifier option) list (************************************************************************) (* This concerns Cases *) open Declarations open Inductive open Inductiveops -open Instantiate - -let lift_context n l = - let k = List.length l in - list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l - -let transform_rec loc env sigma (pj,c,lf) indt = - let p = pj.uj_val in - let (indf,realargs) = dest_ind_type indt in - let (ind,params) = dest_ind_family indf in - let (mib,mip) = lookup_mind_specif env ind in - let recargs = mip.mind_recargs in - let mI = mkInd ind in - let ci = make_default_case_info env (if Options.do_translate() then RegularStyle else MatchStyle) ind in - let nconstr = Array.length mip.mind_consnames in - if Array.length lf <> nconstr then - (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in - error_number_branches_loc loc env sigma cj nconstr); - let tyi = snd ind in - if mis_is_recursive_subset [tyi] recargs then - let dep = - is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in - let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in - let depFvec = Array.init mib.mind_ntypes init_depFvec in - (* build now the fixpoint *) - let lnames,_ = get_arity env indf in - let nar = List.length lnames in - let nparams = mip.mind_nparams in - let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in - let branches = - array_map3 - (fun f t reca -> - whd_beta - (Indrec.make_rec_branch_arg env sigma - (nparams,depFvec,nar+1) - f t reca)) - (Array.map (lift (nar+2)) lf) constrs (dest_subterms recargs) - in - let deffix = - it_mkLambda_or_LetIn_name env - (lambda_create env - (applist (mI,List.append (List.map (lift (nar+1)) params) - (extended_rel_list 0 lnames)), - mkCase (ci, lift (nar+2) p, mkRel 1, branches))) - (lift_rel_context 1 lnames) - in - if noccurn 1 deffix then - whd_beta (applist (pop deffix,realargs@[c])) - else - let ind = applist (mI,(List.append - (List.map (lift nar) params) - (extended_rel_list 0 lnames))) in - let typPfix = - it_mkProd_or_LetIn_name env - (prod_create env - (ind, - (if dep then - let ext_lnames = (Anonymous,None,ind)::lnames in - let args = extended_rel_list 0 ext_lnames in - whd_beta (applist (lift (nar+1) p, args)) - else - let args = extended_rel_list 1 lnames in - whd_beta (applist (lift (nar+1) p, args))))) - lnames in - let fix = - mkFix (([|nar|],0), - ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in - applist (fix,realargs@[c]) - else - mkCase (ci, p, c, lf) (************************************************************************) @@ -114,909 +47,667 @@ let transform_rec loc env sigma (pj,c,lf) indt = let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = create "constr" -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 (the_conv_x_leq 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 (the_conv_x_leq 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 -> inh_conv_coerce_to loc env isevars j typ - -let push_rels vars env = List.fold_right push_rel vars env - -(* -let evar_type_case isevars env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c - in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) -*) - -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_reference 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 () - -(* [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 = function - - | 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 = (Evd.map (evars_of isevars) ev).evar_hyps 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) -> - (match tycon with - | Some ty -> - { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty } - | None -> error_unsolvable_implicit loc env (evars_of isevars) k) - - | 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 as vni) -> - let fix = (vni,(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 = 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 - (* - let apply_one_arg (floc,tycon,jl) c = - let (dom,rng) = split_tycon floc env isevars tycon in - let cj = pretype dom env isevars lvar c in - let rng_tycon = option_app (subst1 cj.uj_val) rng in - let argloc = loc_of_rawconstr c in - (join_loc floc argloc,rng_tycon,(argloc,cj)::jl) in - let _,_,jl = - List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in - let jl = List.rev jl in - let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in - *) - inh_conv_coerce_to_tycon loc env isevars resj tycon - - | RLambda(loc,name,c1,c2) -> - let (name',dom,rng) = 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 = Evarutil.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 = type_app (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) as indt) = - 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 - let cs = build_dependent_constructor cs 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 }) - - (* Special Case for let constructions to avoid exponential behavior *) - | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle -> - let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs) as indt) = - 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 j = match po with - | Some p -> - let pj = pretype empty_tycon env isevars lvar p in - let dep = is_dependent_elimination env pj.uj_type indf in - let ar = - arity_of_case_predicate env indf dep (Type (new_univ())) in - let _ = the_conv_x_leq env isevars pj.uj_type ar in - let pj = j_nf_evar (evars_of isevars) pj in - let pj = if dep then pj else make_dep_of_undep env indt pj in - let (bty,rsty) = - Indrec.type_rec_branches - false env (evars_of isevars) indt pj.uj_val cj.uj_val - in - if Array.length bty <> 1 then - error_number_branches_loc - loc env (evars_of isevars) cj (Array.length bty); - let fj = - let tyc = bty.(0) in - pretype (mk_tycon tyc) env isevars lvar f - in - let fv = j_val fj in - let ft = fj.uj_type in - check_branches_message loc env isevars cj.uj_val (bty,[|ft|]); - let v = - let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env st mis in - mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|]) - in - { uj_val = v; uj_type = rsty } - - | None -> - (* get type information from type of branches *) - let expbr = Cases.branch_scheme env isevars false indf in - if Array.length expbr <> 1 then - error_number_branches_loc loc env (evars_of isevars) - cj (Array.length expbr); - let expti = expbr.(0) in - let fj = pretype (mk_tycon expti) env isevars lvar f in - let use_constraint () = - (* get type information from constraint *) - (* warning: if the constraint comes from an evar type, it *) - (* may be Type while Prop or Set would be expected *) - match tycon with - | Some pred -> - let arsgn = make_arity_signature env true indf in - let pred = lift (List.length arsgn) pred in - let pred = - it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) - arsgn in - false, pred - | None -> - let sigma = evars_of isevars in - error_cant_find_case_type_loc loc env sigma cj.uj_val - in - let ok, p = - try - let pred = - Cases.pred_case_ml - env (evars_of isevars) false indt (0,fj.uj_type) - in - if has_undefined_isevars isevars pred then - use_constraint () - else - true, pred - with Cases.NotInferable _ -> - use_constraint () - in - let p = nf_evar (evars_of isevars) p in - let (bty,rsty) = - Indrec.type_rec_branches - false env (evars_of isevars) indt p cj.uj_val - in - let _ = option_app (the_conv_x_leq env isevars rsty) tycon in - let fj = - if ok then fj - else pretype (mk_tycon bty.(0)) env isevars lvar f - in - let fv = fj.uj_val in - let ft = fj.uj_type in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env st mis in - mkCase (ci, (nf_betaiota p), cj.uj_val,[|fv|] ) - in - { uj_val = v; uj_type = rsty } in - - (* Build the LetTuple form for v8 *) - let c = - let (ind,params) = dest_ind_family indf in - let rtntypopt, indnalopt = match po with - | None -> None, (Anonymous,None) - | Some p -> - let pj = pretype empty_tycon env isevars lvar p in - let dep = is_dependent_elimination env pj.uj_type indf in - let rec decomp_lam_force n avoid l p = - (* avoid is not exhaustive ! *) - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> - decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = Nameops.next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in - let (nal,p,avoid) = - decomp_lam_force (List.length realargs) [] [] p in - let na,rtntyp,_ = - if dep then decomp_lam_force 1 avoid [] p - else [Anonymous],p,[] in - let intyp = - if List.for_all - (function - | Anonymous -> true - | Name id -> not (occur_rawconstr id rtntyp)) nal - then (* No dependency in realargs *) - None - else - let args = List.map (fun _ -> Anonymous) params @ nal in - Some (dummy_loc,ind,args) in - (Some rtntyp,(List.hd na,intyp)) in - let cs = (get_constructors env indf).(0) in - match indnalopt with - | (na,None) -> (* Represented as a let *) - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p) else - match p with - | RLambda (_,(Name id as na),_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> - decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = Nameops.next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dummy_loc,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dummy_loc,p,[a]))) in - let (nal,d) = decomp_lam_force cs.cs_nargs [] [] f in - RLetTuple (loc,nal,(na,rtntypopt),c,d) - | _ -> (* Represented as a match *) - let detype_eqn constr construct_nargs branch = - let name_cons = function - | Anonymous -> fun l -> l - | Name id -> fun l -> id::l in - let make_pat na avoid b ids = - PatVar (dummy_loc,na), - name_cons na avoid,name_cons na ids - in - let rec buildrec ids patlist avoid n b = - if n=0 then - (dummy_loc, ids, - [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - b) - else - match b with - | RLambda (_,x,_,b) -> - let pat,new_avoid,new_ids = make_pat x avoid b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) b - - | RLetIn (_,x,_,b) -> - let pat,new_avoid,new_ids = make_pat x avoid b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) b - - | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) - buildrec ids patlist avoid n c - - | _ -> (* eta-expansion *) - (* nommage de la nouvelle variable *) - let id = Nameops.next_ident_away (id_of_string "x") avoid in - let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in - let pat,new_avoid,new_ids = - make_pat (Name id) avoid new_b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) new_b - - in - buildrec [] [] [] construct_nargs branch in - let eqn = detype_eqn (ind,1) cs.cs_nargs f in - RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],[eqn]) - in - xx := Some c; - (* End building the v8 syntax *) - j +(** Miscellaneous interpretation functions *) + +let interp_sort = function + | RProp c -> Prop c + | RType _ -> new_Type_sort () + +let interp_elimination_sort = function + | RProp Null -> InProp + | RProp Pos -> InSet + | RType _ -> InType - | RIf (loc,c,(na,po),b1,b2) -> - let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs) as indt) = - try find_rectype env (evars_of isevars) cj.uj_type +module type S = +sig + + module Cases : Cases.S + + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + val allow_anonymous_refs : bool ref + + (* Generic call to the interpreter from rawconstr to open_constr, leaving + unresolved holes as evars and returning the typing contexts of + these evars. Work as [understand_gen] for the rest. *) + + val understand_tcc : + evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr + + val understand_tcc_evars : + evar_defs ref -> env -> typing_constraint -> rawconstr -> constr + + (* More general entry point with evars from ltac *) + + (* Generic call to the interpreter from rawconstr to constr, failing + unresolved holes in the rawterm cannot be instantiated. + + In [understand_ltac sigma env ltac_env constraint c], + + sigma : initial set of existential variables (typically dependent subgoals) + ltac_env : partial substitution of variables (used for the tactic language) + constraint : tell if interpreted as a possibly constrained term or a type + *) + + val understand_ltac : + evar_map -> env -> var_map * unbound_ltac_var_map -> + typing_constraint -> rawconstr -> evar_defs * constr + + (* Standard call to get a constr from a rawconstr, resolving implicit args *) + + val understand : evar_map -> env -> ?expected_type:Term.types -> + rawconstr -> constr + + (* Idem but the rawconstr is intended to be a type *) + + val understand_type : evar_map -> env -> rawconstr -> constr + + (* A generalization of the two previous case *) + + val understand_gen : typing_constraint -> evar_map -> env -> + rawconstr -> constr + + (* Idem but returns the judgment of the understood term *) + + val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + + (* Idem but do not fail on unresolved evars *) + + val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + + (*i*) + (* Internal of Pretyping... + * Unused outside, but useful for debugging + *) + val pretype : + type_constraint -> env -> evar_defs ref -> + var_map * (identifier * identifier option) list -> + rawconstr -> unsafe_judgment + + val pretype_type : + val_constraint -> env -> evar_defs ref -> + var_map * (identifier * identifier option) list -> + rawconstr -> unsafe_type_judgment + + val pretype_gen : + evar_defs ref -> env -> + var_map * (identifier * identifier option) list -> + typing_constraint -> rawconstr -> constr + + (*i*) +end + +module Pretyping_F (Coercion : Coercion.S) = struct + + module Cases = Cases.Cases_F(Coercion) + + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + let allow_anonymous_refs = ref false + + 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 + + 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 t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t + + let push_rels vars env = List.fold_right push_rel vars env + + (* + let evar_type_case isevars env ct pt lft p c = + let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c + in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) + *) + + 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 -> - 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 impossible *) - let arsgn,_ = get_arity env indf in - let arsgn = List.map (fun (_,b,t) -> (Anonymous,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 -> new_isevar isevars env (loc,InternalHole) (new_Type ()) + 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 "variable " ++ pr_id id ++ str " should be 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 () + + (* [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 : type_constraint) env isevars lvar = function + | 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 (None, ty) -> ty + | None | Some _ -> + 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 length = List.length args in + let ftycon = + match tycon with + None -> None + | Some (None, ty) -> mk_abstr_tycon length ty + | Some (Some (init, cur), ty) -> + Some (Some (length + init, length + cur), ty) + in + let fj = pretype empty_tycon env isevars lvar f in + let floc = loc_of_rawconstr f in + let rec apply_rec env n resj tycon = function + | [] -> resj + | c::rest -> + let argloc = loc_of_rawconstr c in + let resj = evd_comb1 (Coercion.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 value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in + let typ' = nf_isevar !isevars typ in + let tycon = + option_app + (fun (abs, ty) -> + match abs with + None -> + isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' + (abs, ty); + (abs, ty) + | Some (init, cur) -> + isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' + (abs, ty); + (Some (init, pred cur), ty)) + tycon + in + apply_rec env (n+1) + { uj_val = nf_isevar !isevars value; + uj_type = nf_isevar !isevars typ' } + (option_app (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) 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 ftycon = option_app (lift_abstr_tycon_type (-1)) ftycon in + let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in + let resj = + match kind_of_term resj.uj_val with + | App (f,args) when isInd f -> + let sigma = evars_of !isevars in + let t = Retyping.type_of_applied_inductive env sigma (destInd f) args in + let s = snd (splay_arity env sigma t) in + on_judgment_type (set_inductive_level env s) resj + (* Rem: no need to send sigma: no head evar, it's an arity *) + | _ -> resj 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 = lift_tycon 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 = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn 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 (_,b,t) -> (Anonymous,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 } - - | ROrderedCase (loc,st,po,c,lf,x) -> - let isrec = (st = MatchStyle) in - let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs) as indt) = - 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 (dep,pj) = match po with - | Some p -> - let pj = pretype empty_tycon env isevars lvar p in - let dep = is_dependent_elimination env pj.uj_type indf in - let ar = - arity_of_case_predicate env indf dep (Type (new_univ())) in - let _ = the_conv_x_leq env isevars pj.uj_type ar in - (dep, pj) - | None -> - (* get type information from type of branches *) - let expbr = Cases.branch_scheme env isevars isrec indf in - let rec findtype i = - if i >= Array.length lf - then - (* get type information from constraint *) - (* warning: if the constraint comes from an evar type, it *) - (* may be Type while Prop or Set would be expected *) - match tycon with - | Some pred -> - let arsgn = make_arity_signature env true indf in - let pred = lift (List.length arsgn) pred in - let pred = - it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) - arsgn in - (true, - Retyping.get_judgment_of env (evars_of isevars) pred) - | None -> - let sigma = evars_of isevars in - error_cant_find_case_type_loc loc env sigma cj.uj_val - else - try - let expti = expbr.(i) in - let fj = - pretype (mk_tycon expti) env isevars lvar lf.(i) in - let pred = - Cases.pred_case_ml (* eta-expanse *) - env (evars_of isevars) isrec indt (i,fj.uj_type) in - if has_undefined_isevars isevars pred then findtype (i+1) - else - let pty = - Retyping.get_type_of env (evars_of isevars) pred in - let pj = { uj_val = pred; uj_type = pty } in -(* - let _ = option_app (the_conv_x_leq env isevars pred) tycon - in -*) - (true,pj) - with Cases.NotInferable _ -> findtype (i+1) in - findtype 0 - in - let pj = j_nf_evar (evars_of isevars) pj in - let pj = if dep then pj else make_dep_of_undep env indt pj in - let (bty,rsty) = - Indrec.type_rec_branches - isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in - let _ = option_app (the_conv_x_leq env isevars rsty) tycon in - if Array.length bty <> Array.length lf then - error_number_branches_loc loc env (evars_of isevars) - cj (Array.length bty) - else - let lfj = - array_map2 - (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar f) bty - lf in - let lfv = Array.map j_val lfj in - let lft = Array.map (fun j -> j.uj_type) lfj in - check_branches_message loc env isevars cj.uj_val (bty,lft); - let v = - if isrec - then - transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt - else + 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 = lift_tycon 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"); + + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + (* Make dependencies from arity signature impossible *) + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else 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 + let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in + let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred; + uj_type = typ} tycon + in + jtyp.uj_val, jtyp.uj_type + | None -> + let p = match tycon with + | Some (None, ty) -> ty + | None | Some _ -> + e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) + in + it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in + let pred = nf_evar (evars_of !isevars) pred in + let p = nf_evar (evars_of !isevars) p in + (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) + let f cs b = + let n = rel_context_length cs.cs_args in + let pi = lift n pred in (* liftn n 2 pred ? *) + let pi = beta_applist (pi, [build_dependent_constructor cs]) in + let csgn = + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args + else + 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 +(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *) + let bj = pretype (mk_tycon 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 v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env st mis in - mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val, - Array.map (fun j-> j.uj_val) lfj) - in - (* Build the Cases form for v8 *) - let c = - let (ind,params) = dest_ind_family indf in - let (mib,mip) = lookup_mind_specif env ind in - let recargs = mip.mind_recargs in - let mI = mkInd ind in - let nconstr = Array.length mip.mind_consnames in - let tyi = snd ind in - if isrec && mis_is_recursive_subset [tyi] recargs then - Some (Detyping.detype (false,env) - (ids_of_context env) (names_of_rel_context env) - (nf_evar (evars_of isevars) v)) - else - (* Translate into a "match ... with" *) - let rtntypopt, indnalopt = match po with - | None -> None, (Anonymous,None) - | Some p -> - let rec decomp_lam_force n avoid l p = - (* avoid is not exhaustive ! *) - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> - decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = Nameops.next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in - let (nal,p,avoid) = - decomp_lam_force (List.length realargs) [] [] p in - let na,rtntyopt,_ = - if dep then decomp_lam_force 1 avoid [] p - else [Anonymous],p,[] in - let intyp = - if nal=[] then None else - let args = List.map (fun _ -> Anonymous) params @ nal in - Some (dummy_loc,ind,args) in - (Some rtntyopt,(List.hd na,intyp)) in - let rawbranches = - array_map3 (fun bj b cstr -> - let rec strip n r = if n=0 then r else - match r with - | RLambda (_,_,_,t) -> strip (n-1) t - | RLetIn (_,_,_,t) -> strip (n-1) t - | _ -> assert false in - let n = rel_context_length cstr.cs_args in - try - let _,ccl = decompose_lam_n_assum n bj.uj_val in - if noccur_between 1 n ccl then Some (strip n b) else None - with _ -> (* Not eta-expanded or not reduced *) None) - lfj lf (get_constructors env indf) in - if st = IfStyle & snd indnalopt = None - & rawbranches.(0) <> None && rawbranches.(1) <> None then - (* Translate into a "if ... then ... else" *) - (* TODO: translate into a "if" even if po is dependent *) - Some (RIf (loc,c,(fst indnalopt,rtntypopt), - out_some rawbranches.(0),out_some rawbranches.(1))) - else - let detype_eqn constr construct_nargs branch = - let name_cons = function - | Anonymous -> fun l -> l - | Name id -> fun l -> id::l in - let make_pat na avoid b ids = - PatVar (dummy_loc,na), - name_cons na avoid,name_cons na ids - in - let rec buildrec ids patlist avoid n b = - if n=0 then - (dummy_loc, ids, - [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - b) - else - match b with - | RLambda (_,x,_,b) -> - let pat,new_avoid,new_ids = make_pat x avoid b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) b - - | RLetIn (_,x,_,b) -> - let pat,new_avoid,new_ids = make_pat x avoid b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) b - - | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) - buildrec ids patlist avoid n c - - | _ -> (* eta-expansion *) - (* nommage de la nouvelle variable *) - let id = Nameops.next_ident_away (id_of_string "x") avoid in - let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in - let pat,new_avoid,new_ids = - make_pat (Name id) avoid new_b ids in - buildrec new_ids (pat::patlist) new_avoid (n-1) new_b - - in - buildrec [] [] [] construct_nargs branch in - let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in - let get_consnarg j = - let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in - let _,t = decompose_prod_n_assum mip.mind_nparams typi in - List.rev (fst (decompose_prod_assum t)) in - let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in - let consnargsl = Array.map List.length consnargs in - let constructs = Array.init (Array.length lf) (fun i -> (ind,i+1)) in - let eqns = array_map3 detype_eqn constructs consnargsl lf in - Some (RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],Array.to_list eqns)) in - x := c; - (* End build the Cases form for v8 *) - { uj_val = v; - uj_type = rsty } - - | 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,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, 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 = constr_out d in - let j = (Retyping.get_judgment_of env (evars_of isevars) c) 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_valcon 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 = 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 (Coercion.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 + error_unexpected_type_loc + (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v + + 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 + 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 sigma env c = + let isevars = ref (create_evar_defs sigma) in + let j = pretype empty_tycon env isevars ([],[]) c in + let j = j_nf_evar (evars_of !isevars) j in + check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); 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) -> - 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 = new_isevar isevars env loc (mkSort s); - utj_type = s}) - | c -> - let j = pretype empty_tycon env isevars lvar c in - let tj = inh_coerce_to_sort env isevars j in - match valcon with - | None -> tj - | Some v -> - if the_conv_x_leq env isevars v tj.utj_val then tj - else - error_unexpected_type_loc - (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v - - -let unsafe_infer tycon isevars env lvar constr = - let j = pretype tycon env isevars lvar constr in - j_nf_evar (evars_of isevars) j - -let unsafe_infer_type valcon isevars env lvar constr = - let tj = pretype_type valcon env isevars lvar constr in - tj_nf_evar (evars_of isevars) tj - -(* If fail_evar is false, [process_evars] builds a meta_map with the - unresolved Evar that were not in initial sigma; otherwise it fail - on the first unresolved Evar not already in the initial sigma. *) -(* [fail_evar] says how to process unresolved evars: - * true -> raise an error message - * false -> convert them into new Metas (casted with their type) - *) -(* assumes the defined existentials have been replaced in c (should be - done in unsafe_infer and unsafe_infer_type) *) -let check_evars fail_evar 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 as k) -> - assert (Evd.in_dom sigma ev); - if not (Evd.in_dom initial_sigma ev) then - (if fail_evar then - let (loc,k) = evar_source ev isevars in - error_unsolvable_implicit loc env sigma k) - | _ -> iter_constr proc_rec c - in - proc_rec c - -(* 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... -*) - -(* constr with holes *) -type open_constr = evar_map * constr - -let ise_resolve_casted_gen fail_evar sigma env lvar typ c = - let isevars = create_evar_defs sigma in - let j = unsafe_infer (mk_tycon typ) isevars env lvar c in - check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type)); - (evars_of isevars, j) - -let ise_resolve_casted sigma env typ c = - ise_resolve_casted_gen true sigma env ([],[]) typ c - -(* Raw calls to the unsafe inference machine: boolean says if we must fail - on unresolved evars, or replace them by Metas; the unsafe_judgment list - allows us to extend env with some bindings *) -let ise_infer_gen fail_evar sigma env lvar exptyp c = - let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - let isevars = create_evar_defs sigma in - let j = unsafe_infer tycon isevars env lvar c in - check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type)); - (evars_of isevars, j) - -let ise_infer_type_gen fail_evar sigma env lvar c = - let isevars = create_evar_defs sigma in - let tj = unsafe_infer_type empty_valcon isevars env lvar c in - check_evars fail_evar env sigma isevars tj.utj_val; - (evars_of isevars, tj) -type var_map = (identifier * unsafe_judgment) list + let understand_judgment_tcc isevars env c = + let j = pretype empty_tycon env isevars ([],[]) c in + let sigma = evars_of !isevars in + let j = j_nf_evar sigma j in + j -let understand_judgment sigma env c = - snd (ise_infer_gen true sigma env ([],[]) None c) + (* 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 understand_type_judgment sigma env c = - snd (ise_infer_type_gen true sigma env ([],[]) c) + let ise_pretype_gen fail_evar sigma env lvar kind c = + let isevars = ref (Evd.create_evar_defs sigma) in + let c = pretype_gen isevars env lvar kind c in + if fail_evar then check_evars env sigma isevars c; + !isevars, c -let understand sigma env c = - let _, c = ise_infer_gen true sigma env ([],[]) None c in - c.uj_val + (** Entry points of the high-level type synthesis algorithm *) -let understand_type sigma env c = - let _,c = ise_infer_type_gen true sigma env ([],[]) c in - c.utj_val + let understand_gen kind sigma env c = + snd (ise_pretype_gen true sigma env ([],[]) kind c) -let understand_gen_ltac sigma env lvar ~expected_type:exptyp c = - let _, c = ise_infer_gen true sigma env lvar exptyp c in - c.uj_val + let understand sigma env ?expected_type:exptyp c = + snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c) -let understand_gen sigma env lvar ~expected_type:exptyp c = - let _, c = ise_infer_gen true sigma env (lvar,[]) exptyp c in - c.uj_val + let understand_type sigma env c = + snd (ise_pretype_gen true sigma env ([],[]) IsType c) -let understand_gen_tcc sigma env lvar exptyp c = - let metamap, c = ise_infer_gen false sigma env (lvar,[]) exptyp c in - metamap, c.uj_val + let understand_ltac sigma env lvar kind c = + ise_pretype_gen false sigma env lvar kind c + + let understand_tcc_evars isevars env kind c = + pretype_gen isevars env ([],[]) kind c -let interp_sort = function - | RProp c -> Prop c - | RType _ -> new_Type_sort () + let understand_tcc sigma env ?expected_type:exptyp c = + let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in + Evd.evars_of ev, t +end -let interp_elimination_sort = function - | RProp Null -> InProp - | RProp Pos -> InSet - | RType _ -> InType +module Default : S = Pretyping_F(Coercion.Default) |