diff options
Diffstat (limited to 'pretyping')
31 files changed, 567 insertions, 308 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index b713d7812e..2c7b689c04 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -52,7 +52,8 @@ type cbv_value = | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor Univ.puniverses * cbv_value array - | PRIMITIVE of CPrimitives.t * constr * cbv_value array + | PRIMITIVE of CPrimitives.t * pconstant * cbv_value array + | ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context @@ -98,6 +99,8 @@ let rec shift_value n = function CONSTR (c, Array.map (shift_value n) args) | PRIMITIVE(op,c,args) -> PRIMITIVE(op,c,Array.map (shift_value n) args) + | ARRAY (u,t,ty) -> + ARRAY(u, Parray.map (shift_value n) t, shift_value n ty) let shift_value n v = if Int.equal n 0 then v else shift_value n v @@ -170,7 +173,7 @@ let strip_appl head stack = | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack) | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack) | PRIMITIVE(op,c,app) -> (PRIMITIVE(op,c,[||]), stack_app app stack) - | VAL _ | STACK _ | CBN _ | LAM _ -> (head, stack) + | VAL _ | STACK _ | CBN _ | LAM _ | ARRAY _ -> (head, stack) (* Tests if fixpoint reduction is possible. *) @@ -209,6 +212,7 @@ module VNativeEntries = type elem = cbv_value type args = cbv_value array type evd = unit + type uinstance = Univ.Instance.t let get = Array.get @@ -228,6 +232,11 @@ module VNativeEntries = | _ -> raise Primred.NativeDestKO) | _ -> raise Primred.NativeDestKO + let get_parray () e = + match e with + | ARRAY(_u,t,_ty) -> t + | _ -> raise Primred.NativeDestKO + let mkInt env i = VAL(0, mkInt i) let mkFloat env f = VAL(0, mkFloat f) @@ -327,6 +336,9 @@ module VNativeEntries = let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) = get_f_class_constructors env in CONSTR(Univ.in_punivs nan, [||]) + + let mkArray env u t ty = + ARRAY (u,t,ty) end module VredNative = RedNative(VNativeEntries) @@ -368,7 +380,10 @@ and reify_value = function (* reduction under binders *) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) | PRIMITIVE(op,c,args) -> - mkApp(c, Array.map reify_value args) + mkApp(mkConstU c, Array.map reify_value args) + | ARRAY (u,t,ty) -> + let t, def = Parray.to_array t in + mkArray(u, Array.map reify_value t, reify_value def, reify_value ty) and apply_env env t = match kind t with @@ -458,6 +473,15 @@ let rec norm_head info env t stack = | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) | Construct c -> (CONSTR(c, [||]), stack) + | Array(u,t,def,ty) -> + let ty = cbv_stack_term info TOP env ty in + let len = Array.length t in + let t = + Parray.init (Uint63.of_int len) + (fun i -> cbv_stack_term info TOP env t.(i)) + (cbv_stack_term info TOP env def) in + (ARRAY (u,t,ty), stack) + (* neutral cases *) | (Sort _ | Meta _ | Ind _ | Int _ | Float _) -> (VAL(0, t), stack) | Prod _ -> (CBN(t,env), stack) @@ -468,7 +492,12 @@ and norm_head_ref k info env stack normt t = | Declarations.Def body -> if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack - | Declarations.Primitive op -> (PRIMITIVE(op,t,[||]),stack) + | Declarations.Primitive op -> + let c = match normt with + | ConstKey c -> c + | RelKey _ | VarKey _ -> assert false + in + (PRIMITIVE(op,c,[||]),stack) | Declarations.OpaqueDef _ | Declarations.Undef _ -> if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt t),stack) @@ -538,7 +567,7 @@ and cbv_stack_value info env = function | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl) (* primitive apply to arguments *) - | (PRIMITIVE(op,c,[||]), APP(appl,stk)) -> + | (PRIMITIVE(op,(_,u as c),[||]), APP(appl,stk)) -> let nargs = CPrimitives.arity op in let len = Array.length appl in if nargs <= len then @@ -549,7 +578,7 @@ and cbv_stack_value info env = function if nargs < len then stack_app (Array.sub appl nargs (len - nargs)) stk else stk in - match VredNative.red_prim info.env () op args with + match VredNative.red_prim info.env () op u args with | Some (CONSTR (c, args)) -> (* args must be moved to the stack to allow future reductions *) cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk) @@ -585,7 +614,7 @@ and cbv_value_cache info ref = let v = cbv_stack_term info TOP (subs_id 0) body in Declarations.Def v with - | Environ.NotEvaluableConst (Environ.IsPrimitive op) -> Declarations.Primitive op + | Environ.NotEvaluableConst (Environ.IsPrimitive (_u,op)) -> Declarations.Primitive op | Not_found | Environ.NotEvaluableConst _ -> Declarations.Undef None in KeyTable.add info.tab ref v; v @@ -643,7 +672,12 @@ and cbv_norm_value info = function (* reduction under binders *) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map (cbv_norm_value info) args) | PRIMITIVE(op,c,args) -> - mkApp(c,Array.map (cbv_norm_value info) args) + mkApp(mkConstU c,Array.map (cbv_norm_value info) args) + | ARRAY (u,t,ty) -> + let ty = cbv_norm_value info ty in + let t, def = Parray.to_array t in + let def = cbv_norm_value info def in + mkArray(u, Array.map (cbv_norm_value info) t, def, ty) (* with profiling *) let cbv_norm infos constr = diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index d7804edf6d..409f4c0f70 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -36,7 +36,8 @@ type cbv_value = | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor Univ.puniverses * cbv_value array - | PRIMITIVE of CPrimitives.t * Constr.t * cbv_value array + | PRIMITIVE of CPrimitives.t * pconstant * cbv_value array + | ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value and cbv_stack = | TOP diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 656739657d..419eeaa92a 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -406,10 +406,16 @@ let matches_core env sigma allow_bound_rels | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> List.fold_left2 (sorec ctx env) subst args1 args2 | PInt i1, Int i2 when Uint63.equal i1 i2 -> subst + | PFloat f1, Float f2 when Float64.equal f1 f2 -> subst + + | PArray(pt,pdef,pty), Array(_u,t,def,ty) + when Array.length pt = Array.length t -> + sorec ctx env (sorec ctx env (Array.fold_left2 (sorec ctx env) subst pt t) pdef def) pty ty + | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _ - | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _), _ -> raise PatternMatchingFailure + | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _ | PArray _), _ -> raise PatternMatchingFailure in sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c @@ -527,6 +533,13 @@ let sub_match ?(closed=true) env sigma pat c = aux env term mk_ctx next with Retyping.RetypeError _ -> next () end + | Array(u, t, def, ty) -> + let next_mk_ctx = function + | def :: ty :: l -> mk_ctx (mkArray(u, Array.of_list l, def, ty)) + | _ -> assert false + in + let sub = (env,def) :: (env,ty) :: subargs env t in + try_aux sub next_mk_ctx next | Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ -> next () in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 02c04c2300..7fcb0795bd 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -809,6 +809,12 @@ and detype_r d flags avoid env sigma t = | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef | Int i -> GInt i | Float f -> GFloat f + | Array(u,t,def,ty) -> + let t = Array.map (detype d flags avoid env sigma) t in + let def = detype d flags avoid env sigma def in + let ty = detype d flags avoid env sigma ty in + let u = detype_instance sigma u in + GArray(u, t, def, ty) and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try @@ -1096,6 +1102,14 @@ let rec subst_glob_constr env subst = DAst.map (function let k' = smartmap_cast_type (subst_glob_constr env subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + | GArray (u,t,def,ty) as raw -> + let def' = subst_glob_constr env subst def + and t' = Array.Smart.map (subst_glob_constr env subst) t + and ty' = subst_glob_constr env subst ty + in + if def' == def && t' == t && ty' == ty then raw else + GArray(u,t',def',ty') + ) (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0206d4e70d..2feae8cc25 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -130,7 +130,7 @@ let flex_kind_of_term flags env evd c sk = | Evar ev -> if is_frozen flags ev then Rigid else Flexible ev - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false @@ -212,7 +212,7 @@ let occur_rigidly flags env evd (evk,_) t = (match aux c with | Rigid b -> Rigid b | _ -> Reducible) - | Meta _ | Fix _ | CoFix _ | Int _ | Float _ -> Reducible + | Meta _ | Fix _ | CoFix _ | Int _ | Float _ | Array _ -> Reducible in match aux t with | Rigid b -> b @@ -898,7 +898,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) let rec is_unnamed (hd, args) = match EConstr.kind i hd with - | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _) -> + | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _|Array _) -> Stack.not_purely_applicative args | (CoFix _|Meta _|Rel _)-> true | Evar _ -> Stack.not_purely_applicative args @@ -1019,7 +1019,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Ind _, Ind _ | Construct _, Construct _ | Int _, Int _ - | Float _, Float _ -> + | Float _, Float _ + | Array _, Array _ -> rigids env evd sk1 term1 sk2 term2 | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) @@ -1064,9 +1065,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Evar _ | Lambda _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Array _ | Evar _ | Lambda _), _ -> UnifFailure (evd,NotSameHead) - | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) -> + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Array _ | Evar _ | Lambda _) -> UnifFailure (evd,NotSameHead) | Case _, _ -> UnifFailure (evd,NotSameHead) | Proj _, _ -> UnifFailure (evd,NotSameHead) @@ -1333,6 +1334,12 @@ let thin_evars env sigma sign c = let c' = applyrec (env,0) c in (!sigma, c') +exception NotFoundInstance of exn +let () = CErrors.register_handler (function + | NotFoundInstance e -> + Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e) + | _ -> None) + let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in @@ -1410,11 +1417,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = refresh_universes ~status:Evd.univ_flexible (Some true) env_evar_unf evd evty else evd, evty in - let (evd, ev) = new_evar_instance sign evd evty ~filter instance in - let evk = fst (destEvar evd ev) in + let (evd, evk) = new_pure_evar sign evd evty ~filter in evsref := (evk,evty,inst,prefer_abstraction)::!evsref; fixed := Evar.Set.add evk !fixed; - evd, ev + evd, mkEvar (evk, instance) in let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in if debug_ho_unification () then @@ -1478,7 +1484,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) - with e -> user_err (Pp.str "Cannot find an instance") + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + Exninfo.iraise (NotFoundInstance e, info) else ((if debug_ho_unification () then let evi = Evd.find evd evk in diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 71edcaa231..f33030d6a4 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -180,26 +180,71 @@ let define_evar_as_sort env evd (ev,args) = constraint on its domain and codomain. If the input constraint is an evar instantiate it with the product of 2 new evars. *) +let rec presplit env sigma c = + let c = Reductionops.whd_all env sigma c in + match EConstr.kind sigma c with + | App (h,args) when isEvar sigma h -> + let sigma, lam = define_evar_as_lambda env sigma (destEvar sigma h) in + (* XXX could be just whd_all -> no recursion? *) + presplit env sigma (mkApp (lam, args)) + | _ -> sigma, c + let split_tycon ?loc env evd tycon = - let rec real_split evd c = - let t = Reductionops.whd_all env evd c in - match EConstr.kind evd t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev (* ev is undefined because of whd_all *) -> - let (evd',prod) = define_evar_as_product env evd ev in - let (na,dom,rng) = destProd evd prod in - let anon = {na with binder_name = Anonymous} in - evd',(anon, dom, rng) - | App (c,args) when isEvar evd c -> - let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in - real_split evd' (mkApp (lam,args)) - | _ -> error_not_product ?loc env evd c - in - match tycon with - | None -> evd,(make_annot Anonymous Relevant,None,None) - | Some c -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) + match tycon with + | None -> evd,(make_annot Anonymous Relevant,None,None) + | Some c -> + let evd, c = presplit env evd c in + let evd, na, dom, rng = match EConstr.kind evd c with + | Prod (na,dom,rng) -> evd, na, dom, rng + | Evar ev -> + let (evd,prod) = define_evar_as_product env evd ev in + let (na,dom,rng) = destProd evd prod in + let anon = {na with binder_name = Anonymous} in + evd, anon, dom, rng + | _ -> + (* XXX no error to allow later coercion? Not sure if possible with funclass *) + error_not_product ?loc env evd c + in + evd, (na, mk_tycon dom, mk_tycon rng) + + +let define_pure_evar_as_array env sigma evk = + let evi = Evd.find_undefined sigma evk in + let evenv = evar_env env evi in + let evksrc = evar_source evk sigma in + let src = subterm_source evk ~where:Domain evksrc in + let sigma, (ty,u) = new_type_evar evenv sigma univ_flexible ~src ~filter:(evar_filter evi) in + let concl = Reductionops.whd_all evenv sigma evi.evar_concl in + let s = destSort sigma concl in + (* array@{u} ty : Type@{u} <= Type@{s} *) + let sigma = Evd.set_leq_sort env sigma u (ESorts.kind sigma s) in + let u = Option.get (Univ.Universe.level (Sorts.univ_of_sort u)) in + let ar = Typeops.type_of_array env (Univ.Instance.of_array [|u|]) in + let sigma = Evd.define evk (mkApp (EConstr.of_constr ar, [| ty |])) sigma in + sigma + +let is_array_const env sigma c = + match EConstr.kind sigma c with + | Const (cst,_) -> + (match env.Environ.retroknowledge.Retroknowledge.retro_array with + | None -> false + | Some cst' -> Constant.equal cst cst') + | _ -> false + +let split_as_array env sigma0 = function + | None -> sigma0, None + | Some c -> + let sigma, c = presplit env sigma0 c in + match EConstr.kind sigma c with + | App (h,[|ty|]) when is_array_const env sigma h -> sigma, Some ty + | Evar ev -> + let sigma = define_pure_evar_as_array env sigma (fst ev) in + let ty = match EConstr.kind sigma c with + | App (_,[|ty|]) -> ty + | _ -> assert false + in + sigma, Some ty + | _ -> sigma0, None let valcon_of_tycon x = x let lift_tycon n = Option.map (lift n) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index a4169c2298..e5c3f8baa1 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -35,6 +35,11 @@ val split_tycon : ?loc:Loc.t -> env -> evar_map -> type_constraint -> evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) +val split_as_array : env -> evar_map -> type_constraint -> + evar_map * type_constraint +(** If the constraint can be made to look like [array A] return [A], + otherwise return [None] (this makes later coercion possible). *) + val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 348d7c0b2f..79839099f7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -698,10 +698,9 @@ let make_projectable_subst aliases sigma evi args = *) let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = - let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in + let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in let t_in_env = whd_evar evd t_in_env in - let (evk, _) = destEvar evd evar_in_env in - let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in + let evd = define_fun env evd None (evk, inst_in_env) t_in_env in let ctxt = named_context_of_val sign in let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in let evar_in_sign = mkEvar (evk, inst_in_sign) in @@ -770,9 +769,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let (evd, ev2_in_sign) = - new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in - let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in - (evd, ev2_in_sign, ev2_in_env) + new_pure_evar sign2 evd ev2ty_in_sign ~filter:filter2 ~src in + let ev2_in_env = (ev2_in_sign, inst2_in_env) in + (evd, mkEvar (ev2_in_sign, inst2_in_sign), ev2_in_env) let restrict_upon_filter evd evk p args = let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 05abb86f46..81a62a7048 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -110,7 +110,8 @@ let new_evar env sigma ?src ?naming typ = let instance = rel_list (nb_rel env.renamed_env) inst_vars in let (subst, _, sign) = Lazy.force env.extra in let typ' = csubst_subst subst typ in - new_evar_instance sign sigma typ' ?src ?naming instance + let (sigma, evk) = new_pure_evar sign sigma typ' ?src ?naming in + (sigma, mkEvar (evk, instance)) let new_type_evar env sigma ~src = let sigma, s = Evd.new_sort_variable Evd.univ_flexible_alg sigma in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 342175a512..5bd26be823 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -168,9 +168,12 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with f c1 c2 && cast_type_eq f t1 t2 | GInt i1, GInt i2 -> Uint63.equal i1 i2 | GFloat f1, GFloat f2 -> Float64.equal f1 f2 + | GArray (u1, t1, def1, ty1), GArray (u2, t2, def2, ty2) -> + Array.equal f t1 t2 && f def1 def2 && f ty1 ty2 && + Option.equal (List.equal glob_level_eq) u1 u2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | - GInt _ | GFloat _), _ -> false + GInt _ | GFloat _ | GArray _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -231,6 +234,11 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = map_cast_type f k in GCast (comp1,comp2) + | GArray (u,t,def,ty) -> + let comp1 = Array.map_left f t in + let comp2 = f def in + let comp3 = f ty in + GArray (u,comp1,comp2,comp3) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) as x -> x ) @@ -263,6 +271,7 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c + | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc ) let fold_return_type_with_binders f g v acc (na,tyopt) = @@ -305,6 +314,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c + | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index bccc30ad62..526eac6f1e 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -92,6 +92,7 @@ type 'a glob_constr_r = | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type | GInt of Uint63.t | GFloat of Float64.t + | GArray of glob_level list option * 'a glob_constr_g array * 'a glob_constr_g * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 98cfbf7fa7..d1ac0862ed 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -79,7 +79,7 @@ and kind_of_head env t = | Proj (p,c) -> RigidHead RigidOther | Case (_,_,_,c,_) -> aux k [] c true - | Int _ | Float _ -> ConstructorHead + | Int _ | Float _ | Array _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in try aux k [] (List.nth l n) true diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0e7fac35f1..5be8f9f83c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -207,7 +207,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | ra::rest -> (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) - | Imbr _ -> (None,rest) + | Nested _ -> (None,rest) | _ -> (None, rest)) in (match optionpos with @@ -280,7 +280,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let optionpos = match dest_recarg recarg with | Norec -> None - | Imbr _ -> None + | Nested _ -> None | Mrec (_,i) -> fvect.(i) in (match optionpos with diff --git a/pretyping/keys.ml b/pretyping/keys.ml index 1e4f2f2340..7a7099c195 100644 --- a/pretyping/keys.ml +++ b/pretyping/keys.ml @@ -27,6 +27,7 @@ type key = | KRel | KInt | KFloat + | KArray module KeyOrdered = struct type t = key @@ -44,6 +45,7 @@ module KeyOrdered = struct | KRel -> 7 | KInt -> 8 | KFloat -> 9 + | KArray -> 10 let compare gr1 gr2 = match gr1, gr2 with @@ -138,6 +140,7 @@ let constr_key kind c = | LetIn _ -> KLet | Int _ -> KInt | Float _ -> KFloat + | Array _ -> KArray in Some (aux c) with Not_found -> None @@ -155,6 +158,7 @@ let pr_key pr_global = function | KRel -> str"Rel" | KInt -> str"Int" | KFloat -> str"Float" + | KArray -> str"Array" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 89bd7e196f..3f68e3c78f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -214,6 +214,7 @@ let rec nf_val env sigma v typ = | Vconst n -> construct_of_constr_const env sigma n typ | Vint64 i -> i |> Uint63.of_int64 |> mkInt | Vfloat64 f -> f |> Float64.of_float |> mkFloat + | Varray t -> nf_array env sigma t typ | Vblock b -> let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in let args = nf_bargs env sigma b ctyp in @@ -317,13 +318,12 @@ and nf_atom_type env sigma atom = | Avar id -> mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> - let () = if Typeops.should_invert_case env ans.asw_ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.") - in let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in + let iv = if Typeops.should_invert_case env ans.asw_ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in @@ -343,7 +343,7 @@ and nf_atom_type env sigma atom = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs a in - mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase + mkCase(ans.asw_ci, p, iv, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in let tt = Array.map fst tt and rt = Array.map snd tt in @@ -442,6 +442,14 @@ and nf_evar env sigma evk args = evar node *) mkEvar (evk, List.rev args), ty +and nf_array env sigma t typ = + let ty, allargs = app_type env typ in + let typ_elem = allargs.(0) in + let t, vdef = Parray.to_array t in + let t = Array.map (fun v -> nf_val env sigma v typ_elem) t in + let u = snd (destConst ty) in + mkArray(u, t, nf_val env sigma vdef typ_elem, typ_elem) + let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value0 sigma; Nativelambda.evars_metas = Evd.meta_type0 sigma } diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 1dfb8b2cd1..f6d61f4892 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -41,6 +41,7 @@ type constr_pattern = | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t | PFloat of Float64.t + | PArray of constr_pattern array * constr_pattern * constr_pattern (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4aedeb43e3..8c3d624f0f 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -64,10 +64,13 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Uint63.equal i1 i2 | PFloat f1, PFloat f2 -> Float64.equal f1 f2 +| PArray (t1, def1, ty1), PArray (t2, def2, ty2) -> + Array.equal constr_pattern_eq t1 t2 && constr_pattern_eq def1 def2 + && constr_pattern_eq ty1 ty2 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _ - | PFloat _), _ -> false + | PFloat _ | PArray _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = @@ -93,6 +96,8 @@ let rec occur_meta_pattern = function (occur_meta_pattern p) || (occur_meta_pattern c) || (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) + | PArray (t,def,ty) -> + Array.exists occur_meta_pattern t || occur_meta_pattern def || occur_meta_pattern ty | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ | PInt _ | PFloat _ -> false @@ -121,6 +126,8 @@ let rec occurn_pattern n = function Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl | PCoFix (_,(_,tl,bl)) -> Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl + | PArray (t,def,ty) -> + Array.exists (occurn_pattern n) t || occurn_pattern n def || occurn_pattern n ty let noccurn_pattern n c = not (occurn_pattern n c) @@ -139,7 +146,8 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ | PInt _ | PFloat _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") + | PCoFix _ | PInt _ | PFloat _ | PArray _ -> + anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> GlobRef.ConstRef sp @@ -217,7 +225,10 @@ let pattern_of_constr env sigma t = PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | Int i -> PInt i - | Float f -> PFloat f in + | Float f -> PFloat f + | Array (_u, t, def, ty) -> + PArray (Array.map (pattern_of_constr env) t, pattern_of_constr env def, pattern_of_constr env ty) + in pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -238,6 +249,7 @@ let map_pattern_with_binders g f l = function | PCoFix (ln,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | PArray (t,def,ty) -> PArray (Array.map (f l) t, f l def, f l ty) (* Non recursive *) | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ | PInt _ | PFloat _ as x) -> x @@ -359,6 +371,12 @@ let rec subst_pattern env sigma subst pat = let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) + | PArray (t,def,ty) -> + let t' = Array.Smart.map (subst_pattern env sigma subst) t in + let def' = subst_pattern env sigma subst def in + let ty' = subst_pattern env sigma subst ty in + if def' == def && t' == t && ty' == ty then pat + else PArray (t',def',ty') let mkPLetIn na b t c = PLetIn(na,b,t,c) let mkPProd na t u = PProd(na,t,u) @@ -502,7 +520,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GInt i -> PInt i | GFloat f -> PFloat f - | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ -> + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GArray _ -> err ?loc (Pp.str "Non supported pattern.")) and pat_of_glob_in_context metas vars decls c = diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 414663c826..207ffc7b86 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -66,6 +66,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function | CErrors.UserError _ | TypeError _ | PretypeError _ + | Reductionops.AnomalyInConversion _ | Nametab.GlobalizationError _ -> true | _ -> false diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e4403d5bf4..b9825b6a92 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -508,6 +508,7 @@ type pretyper = { pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun; pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; + pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun; pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun; } @@ -549,6 +550,8 @@ let eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t = self.pretype_int self n ?loc ~program_mode ~poly resolve_tc tycon env sigma | GFloat f -> self.pretype_float self f ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GArray (u,t,def,ty) -> + self.pretype_array self (u,t,def,ty) ?loc ~program_mode ~poly resolve_tc tycon env sigma let eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t = self.pretype_type self t ~program_mode ~poly resolve_tc tycon env sigma @@ -1196,24 +1199,6 @@ struct sigma, { uj_val = v; uj_type = tval } in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon - let pretype_int self i = - fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> - let resj = - try Typing.judge_of_int !!env i - with Invalid_argument _ -> - user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") - in - discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon - - let pretype_float self f = - fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> - let resj = - try Typing.judge_of_float !!env f - with Invalid_argument _ -> - user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") - in - discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon - (* [pretype_type valcon env sigma c] coerces [c] into a type *) let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with | GHole (knd, naming, None) -> @@ -1255,6 +1240,52 @@ let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEn ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v end + let pretype_int self i = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let resj = + try Typing.judge_of_int !!env i + with Invalid_argument _ -> + user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") + in + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + + let pretype_float self f = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let resj = + try Typing.judge_of_float !!env f + with Invalid_argument _ -> + user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") + in + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + + let pretype_array self (u,t,def,ty) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let sigma, tycon' = split_as_array !!env sigma tycon in + let sigma, jty = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon' env sigma ty in + (* XXX not sure if we need to be this complex, I wrote this while + being confused by broken universe substitutions *) + let sigma, u = match Univ.Universe.level (Sorts.univ_of_sort jty.utj_type) with + | Some u -> + let sigma = Evd.make_nonalgebraic_variable sigma u in + sigma, u + | None -> + let sigma, u = Evd.new_univ_level_variable UState.univ_flexible sigma in + let sigma = Evd.set_leq_sort !!env sigma jty.utj_type + (Sorts.sort_of_univ (Univ.Universe.make u)) + in + sigma, u + in + let sigma, jdef = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon jty.utj_val) env sigma def in + let pretype_elem = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon jty.utj_val) env in + let sigma, jt = Array.fold_left_map pretype_elem sigma t in + let u = Univ.Instance.of_array [| u |] in + let ta = EConstr.of_constr @@ Typeops.type_of_array !!env u in + let j = { + uj_val = EConstr.mkArray(EInstance.make u, Array.map (fun j -> j.uj_val) jt, jdef.uj_val, jty.utj_val); + uj_type = EConstr.mkApp(ta,[|jdef.uj_type|]) + } in + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + end (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *) @@ -1281,6 +1312,7 @@ let default_pretyper = pretype_cast = pretype_cast; pretype_int = pretype_int; pretype_float = pretype_float; + pretype_array = pretype_array; pretype_type = pretype_type; } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 8be7b1477b..c03374c59f 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -163,6 +163,7 @@ type pretyper = { pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun; pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; + pretype_array : pretyper -> glob_level list option * glob_constr array * glob_constr * glob_constr -> unsafe_judgment pretype_fun; pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun; } (** Type of pretyping algorithms in open-recursion style. A typical way to diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 07154d4e03..c31ecc135c 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,8 +1,8 @@ Geninterp Locus Locusops -Pretype_errors Reductionops +Pretype_errors Inductiveops Arguments_renaming Retyping diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index a8e934d3c6..e6e5ad8dd4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -54,34 +54,29 @@ let structure_table = let projection_table = Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs" -(* TODO: could be unify struc_typ and struc_tuple ? *) - -type struc_tuple = - constructor * proj_kind list * Constant.t option list - -let register_structure env (id,kl,projs) = - let open Declarations in - let ind = fst id in - let mib, mip = Inductive.lookup_mind_specif env ind in - let n = mib.mind_nparams in - let struc = - { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in +let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) = structure_table := Indmap.add ind struc !structure_table; projection_table := List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc)) projs !projection_table -let subst_structure subst (id, kl, projs as obj) = +let subst_structure subst struc = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) List.Smart.map (Option.Smart.map (subst_constant subst)) - projs + struc.s_PROJ in - let id' = Globnames.subst_constructor subst id in - if projs' == projs && id' == id then obj else - (id',kl,projs') + let id' = Globnames.subst_constructor subst struc.s_CONST in + if projs' == struc.s_PROJ && id' == struc.s_CONST + then struc + else { struc with s_CONST = id'; s_PROJ = projs' } + +let rebuild_structure env struc = + let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in + let npars = mib.Declarations.mind_nparams in + { struc with s_EXPECTEDPARAM = npars } let lookup_structure indsp = Indmap.find indsp !structure_table @@ -185,7 +180,7 @@ let rec cs_pattern_of_constr env t = | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Proj (p, c) -> - let { Environ.uj_type = ty } = Typeops.infer env c in + let ty = Retyping.get_type_of_constr env c in let _, params = Inductive.find_rectype env ty in Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 955a4e7aae..3be60d5e62 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -27,13 +27,12 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : proj_kind list; - s_PROJ : Constant.t option list } - -type struc_tuple = - constructor * proj_kind list * Constant.t option list + s_PROJ : Constant.t option list; +} -val register_structure : Environ.env -> struc_tuple -> unit -val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple +val register_structure : struc_typ -> unit +val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ +val rebuild_structure : Environ.env -> struc_typ -> struc_typ (** [lookup_structure isp] returns the struc_typ associated to the inductive path [isp] if it corresponds to a structure, otherwise diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 18a0637efa..fdc770dba6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -422,8 +422,8 @@ struct let get_next_primitive_args kargs stk = let rec nargs = function | [] -> 0 - | CPrimitives.Kwhnf :: _ -> 0 - | _ :: s -> 1 + nargs s + | (CPrimitives.Kwhnf | CPrimitives.Karg) :: _ -> 0 + | CPrimitives.Kparam :: s -> 1 + nargs s in let n = nargs kargs in (List.skipn (n+1) kargs, strip_n_app n stk) @@ -436,15 +436,11 @@ type state = constr * constr Stack.t type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr -type contextual_stack_reduction_function = +type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = - evar_map -> constr -> constr * constr list type state_reduction_function = env -> evar_map -> state -> state -type local_state_reduction_function = evar_map -> state -> state let pr_state env sigma (tm,sk) = let open Pp in @@ -572,14 +568,6 @@ let reduce_and_refold_fix recfun env sigma fix sk = (fun _ (t,sk') -> recfun (t,sk')) [] sigma raw_answer sk -let fix_recarg ((recindices,bodynum),_) stack = - assert (0 <= bodynum && bodynum < Array.length recindices); - let recargnum = Array.get recindices bodynum in - try - Some (recargnum, Stack.nth stack recargnum) - with Not_found -> - None - open Primred module CNativeEntries = @@ -588,6 +576,7 @@ struct type elem = EConstr.t type args = EConstr.t array type evd = evar_map + type uinstance = EConstr.EInstance.t let get = Array.get @@ -601,6 +590,11 @@ struct | Float f -> f | _ -> raise Primred.NativeDestKO + let get_parray evd e = + match EConstr.kind evd e with + | Array(_u,t,def,_ty) -> Parray.of_array t def + | _ -> raise Not_found + let mkInt env i = mkInt i @@ -611,12 +605,12 @@ struct let (ct,cf) = get_bool_constructors env in mkConstruct (if b then ct else cf) - let mkCarry env b e = - let int_ty = mkConst @@ get_int_type env in - let (c0,c1) = get_carry_constructors env in - mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|]) + let mkCarry env b e = + let int_ty = mkConst @@ get_int_type env in + let (c0,c1) = get_carry_constructors env in + mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|]) - let mkIntPair env e1 e2 = + let mkIntPair env e1 e2 = let int_ty = mkConst @@ get_int_type env in let c = get_pair_constructor env in mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|]) @@ -699,6 +693,11 @@ struct let (_pNormal,_nNormal,_pSubn,_nSubn,_pZero,_nZero,_pInf,_nInf,nan) = get_f_class_constructors env in mkConstruct nan + + let mkArray env u t ty = + let (t,def) = Parray.to_array t in + mkArray(u,t,def,ty) + end module CredNative = RedNative(CNativeEntries) @@ -767,7 +766,7 @@ let rec whd_state_gen flags env sigma = let body = EConstr.of_constr body in whrec (body, stack) end - | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack -> + | exception NotEvaluableConst (IsPrimitive (u,p)) when Stack.check_native_args p stack -> let kargs = CPrimitives.kind p in let (kargs,o) = Stack.get_next_primitive_args kargs stack in (* Should not fail thanks to [check_native_args] *) @@ -841,9 +840,9 @@ let rec whd_state_gen flags env sigma = |_ -> fold () else fold () - | Int _ | Float _ -> + | Int _ | Float _ | Array _ -> begin match Stack.strip_app stack with - | (_, Stack.Primitive(p,kn,rargs,kargs)::s) -> + | (_, Stack.Primitive(p,(_, u as kn),rargs,kargs)::s) -> let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in if more_to_reduce then let (kargs,o) = Stack.get_next_primitive_args kargs s in @@ -858,10 +857,11 @@ let rec whd_state_gen flags env sigma = with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *) in let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in - begin match CredNative.red_prim env sigma p args with - | Some t -> whrec (t,s) - | None -> ((mkApp (mkConstU kn, args), s)) - end + let s = extra_args @ s in + begin match CredNative.red_prim env sigma p u args with + | Some t -> whrec (t,s) + | None -> ((mkApp (mkConstU kn, args), s)) + end | _ -> fold () end @@ -942,7 +942,7 @@ let local_whd_state_gen flags _env sigma = else s | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ - | Int _ | Float _ -> s + | Int _ | Float _ | Array _ -> s in whrec @@ -1085,12 +1085,25 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV +(* NOTE: We absorb anomalies happening in the conversion tactic, which + is a bit ugly. This is mostly due to efficiency both in tactics and + in the conversion machinery itself. It is not uncommon for a tactic + to send some ill-typed term to the engine. + + We would usually say that a tactic that converts ill-typed terms is + buggy, but fixing the tactic could have a very large runtime cost + *) +exception AnomalyInConversion of exn + +let _ = CErrors.register_handler (function + | AnomalyInConversion e -> + Some Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) + | _ -> None) + let report_anomaly (e, info) = let e = - if is_anomaly e then - let msg = Pp.(str "Conversion test raised an anomaly:" ++ - spc () ++ CErrors.print e) in - UserError (None, msg) + if is_anomaly e then AnomalyInConversion e else e in Exninfo.iraise (e, info) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 58fff49faa..0f288cdd46 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -23,6 +23,7 @@ val debug_RAKAM : unit -> bool module CredNative : Primred.RedNative with type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map + and type uinstance = EInstance.t (** Machinery to customize the behavior of the reduction *) module ReductionBehaviour : sig @@ -111,15 +112,11 @@ type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr -type contextual_stack_reduction_function = +type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = - evar_map -> constr -> constr * constr list type state_reduction_function = env -> evar_map -> state -> state -type local_state_reduction_function = evar_map -> state -> state val pr_state : env -> evar_map -> state -> Pp.t @@ -129,11 +126,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -(*i -val stack_reduction_of_reduction : - 'a reduction_function -> 'a state_reduction_function -i*) -val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a val whd_state_gen : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state @@ -166,13 +158,13 @@ val whd_allnolet : reduction_function val whd_betalet : reduction_function (** Removes cast and put into applicative form *) -val whd_nored_stack : contextual_stack_reduction_function -val whd_beta_stack : contextual_stack_reduction_function -val whd_betaiota_stack : contextual_stack_reduction_function -val whd_betaiotazeta_stack : contextual_stack_reduction_function -val whd_all_stack : contextual_stack_reduction_function -val whd_allnolet_stack : contextual_stack_reduction_function -val whd_betalet_stack : contextual_stack_reduction_function +val whd_nored_stack : stack_reduction_function +val whd_beta_stack : stack_reduction_function +val whd_betaiota_stack : stack_reduction_function +val whd_betaiotazeta_stack : stack_reduction_function +val whd_all_stack : stack_reduction_function +val whd_allnolet_stack : stack_reduction_function +val whd_betalet_stack : stack_reduction_function val whd_nored_state : state_reduction_function val whd_beta_state : state_reduction_function @@ -241,7 +233,6 @@ val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool val contract_fix : evar_map -> fixpoint -> constr -val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> Constant.t tableKey -> bool @@ -292,3 +283,5 @@ val whd_betaiota_deltazeta_for_iota_state : (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr + +exception AnomalyInConversion of exn diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb518bc2f9..4bd22e76cb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -157,6 +157,9 @@ let retype ?(polyprop=true) sigma = | Sort _ | Prod _ -> mkSort (sort_of env cstr) | Int _ -> EConstr.of_constr (Typeops.type_of_int env) | Float _ -> EConstr.of_constr (Typeops.type_of_float env) + | Array(u, _, _, ty) -> + let arr = EConstr.of_constr @@ Typeops.type_of_array env (EInstance.kind sigma u) in + mkApp(arr, [|ty|]) and sort_of env t = match EConstr.kind sigma t with @@ -257,6 +260,9 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = (* Makes an unsafe judgment from a constr *) let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c } +let get_type_of_constr ?polyprop ?lax env ?(uctx=UState.from_env env) c = + EConstr.Unsafe.to_constr (get_type_of ?polyprop ?lax env (Evd.from_ctx uctx) (EConstr.of_constr c)) + (* Returns sorts of a context *) let sorts_of_context env evc ctxt = let rec aux = function @@ -301,8 +307,7 @@ let relevance_of_term env sigma c = | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> Relevanceops.relevance_of_projection env p - | Int _ | Float _ -> Sorts.Relevant - + | Int _ | Float _ | Array _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant in diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 16bc251c2a..2e19ffdfcd 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -30,6 +30,10 @@ exception RetypeError of retype_error val get_type_of : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types +(** No-evar version of [get_type_of] *) +val get_type_of_constr : ?polyprop:bool -> ?lax:bool + -> env -> ?uctx:UState.t -> Constr.t -> Constr.types + val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index baa32565f6..e4b5dc1edf 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -358,30 +358,6 @@ let reference_eval env sigma = function let x = Name default_dependent_ident -let make_elim_fun (names,(nbfix,lv,n)) u largs = - let lu = List.firstn n largs in - let p = List.length lv in - let lyi = List.map fst lv in - let la = - List.map_i (fun q aq -> - (* k from the comment is q+1 *) - try mkRel (p+1-(List.index Int.equal (n-q) lyi)) - with Not_found -> aq) - 0 (List.map (Vars.lift p) lu) - in - fun i -> - match names.(i) with - | None -> None - | Some (minargs,ref) -> - let body = applist (mkEvalRef ref u, la) in - let g = - List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> - let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in - let tij' = Vars.substl (List.rev subst) tij in - let x = make_annot x Sorts.Relevant in (* TODO relevance *) - mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some (minargs,g) - (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) @@ -467,16 +443,6 @@ let substl_checking_arity env subst sigma c = type fix_reduction_result = NotReducible | Reduced of (constr * constr list) -let reduce_fix whdfun sigma fix stack = - match fix_recarg fix (Stack.append_app_list stack Stack.empty) with - | None -> NotReducible - | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = whdfun sigma recarg in - let stack' = List.assign stack recargnum (applist recarg') in - (match EConstr.kind sigma recarg'hd with - | Construct _ -> Reduced (contract_fix sigma fix, stack') - | _ -> NotReducible) - let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in @@ -484,22 +450,6 @@ let contract_fix_use_function env sigma f let lbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) -let reduce_fix_use_function env sigma f whfun fix stack = - match fix_recarg fix (Stack.append_app_list stack Stack.empty) with - | None -> NotReducible - | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = - if EConstr.isRel sigma recarg then - (* The recarg cannot be a local def, no worry about the right env *) - (recarg, []) - else - whfun recarg in - let stack' = List.assign stack recargnum (applist recarg') in - (match EConstr.kind sigma recarg'hd with - | Construct _ -> - Reduced (contract_fix_use_function env sigma f fix,stack') - | _ -> NotReducible) - let contract_cofix_use_function env sigma f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in @@ -574,34 +524,23 @@ let match_eval_ref_value env sigma constr stack = env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | _ -> None -let special_red_case env sigma whfun (ci, p, iv, c, lf) = - let rec redrec s = - let (constr, cargs) = whfun s in - match match_eval_ref env sigma constr cargs with - | Some (ref, u) -> - (match reference_opt_value env sigma ref u with - | None -> raise Redelimination - | Some gvalue -> - if reducible_mind_case sigma gvalue then - reduce_mind_case_use_function constr env sigma - {mP=p; mconstr=gvalue; mcargs=cargs; - mci=ci; mlf=lf} - else - redrec (applist(gvalue, cargs))) - | None -> - if reducible_mind_case sigma constr then - reduce_mind_case sigma - {mP=p; mconstr=constr; mcargs=cargs; - mci=ci; mlf=lf} - else - raise Redelimination - in - redrec c +let push_app sigma (hd, stk as p) = match EConstr.kind sigma hd with +| App (hd, args) -> + (hd, Array.fold_right (fun x accu -> x :: accu) args stk) +| _ -> p let recargs = function | EvalVar _ | EvalRel _ | EvalEvar _ -> None | EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c) +let fix_recarg ((recindices,bodynum),_) stack = + assert (0 <= bodynum && bodynum < Array.length recindices); + let recargnum = Array.get recindices bodynum in + try + Some (recargnum, List.nth stack recargnum) + with Failure _ -> + None + let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = (match EConstr.kind sigma recarg'hd with | Construct _ -> @@ -609,24 +548,9 @@ let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = Reduced (List.nth stack' proj_narg, stack) | _ -> NotReducible) -let reduce_proj env sigma whfun whfun' c = - let rec redrec s = - match EConstr.kind sigma s with - | Proj (proj, c) -> - let c' = try redrec c with Redelimination -> c in - let constr, cargs = whfun c' in - (match EConstr.kind sigma constr with - | Construct _ -> - let proj_narg = Projection.npars proj + Projection.arg proj in - List.nth cargs proj_narg - | _ -> raise Redelimination) - | Case (n,p,iv,c,brs) -> - let c' = redrec c in - let p = (n,p,iv,c',brs) in - (try special_red_case env sigma whfun' p - with Redelimination -> mkCase p) - | _ -> raise Redelimination - in redrec c +let rec beta_applist sigma accu c stk = match EConstr.kind sigma c, stk with +| Lambda (_, _, c), arg :: stk -> beta_applist sigma (arg :: accu) c stk +| _ -> substl accu c, stk let whd_nothing_for_iota env sigma s = let rec whrec (x, stack as s) = @@ -650,17 +574,17 @@ let whd_nothing_for_iota env sigma s = (match constant_opt_value_in env (const, u) with | Some body -> whrec (EConstr.of_constr body, stack) | None -> s) - | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack + | LetIn (_,b,_,c) -> whrec (beta_applist sigma [b] c stack) | Cast (c,_,_) -> whrec (c, stack) - | App (f,cl) -> whrec (f, Stack.append_app cl stack) + | App (f,cl) -> whrec (f, Array.fold_right (fun c accu -> c :: accu) cl stack) | Lambda (na,t,c) -> - (match Stack.decomp stack with - | Some (a,m) -> stacklam whrec [a] sigma c m + (match stack with + | a :: stack -> whrec (beta_applist sigma [a] c stack) | _ -> s) | x -> s in - EConstr.decompose_app sigma (Stack.zip sigma (whrec (s,Stack.empty))) + whrec s (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind constants by keeping the name of the constants in the recursive calls; @@ -703,21 +627,17 @@ let rec red_elim_const env sigma ref u largs = try match reference_eval env sigma ref with | EliminationCases n when nargs >= n -> let c = reference_value env sigma ref u in - let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let whfun = whd_simpl_stack env sigma in - (special_red_case env sigma whfun (EConstr.destCase sigma c'), lrest), nocase + let c', lrest = whd_nothing_for_iota env sigma (c, largs) in + (special_red_case env sigma (EConstr.destCase sigma c'), lrest), nocase | EliminationProj n when nargs >= n -> let c = reference_value env sigma ref u in - let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let whfun = whd_construct_stack env sigma in - let whfun' = whd_simpl_stack env sigma in - (reduce_proj env sigma whfun whfun' c', lrest), nocase + let c', lrest = whd_nothing_for_iota env sigma (c, largs) in + (reduce_proj env sigma c', lrest), nocase | EliminationFix (min,minfxargs,infos) when nargs >= min -> let c = reference_value env sigma ref u in - let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in - let whfun = whd_construct_stack env sigma in - (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with + let d, lrest = whd_nothing_for_iota env sigma (c, largs) in + let f = ([|Some (minfxargs,ref)|],infos), u, largs in + (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> @@ -729,10 +649,9 @@ let rec red_elim_const env sigma ref u largs = let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in descend (destEvalRefU sigma c') lrest in let (_, midargs as s) = descend (ref,u) largs in - let d, lrest = whd_nothing_for_iota env sigma (applist s) in - let f = make_elim_fun refinfos u midargs in - let whfun = whd_construct_stack env sigma in - (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with + let d, lrest = whd_nothing_for_iota env sigma s in + let f = refinfos, u, midargs in + (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> @@ -755,32 +674,30 @@ and reduce_params env sigma stack l = | _ -> raise Redelimination) stack l - (* reduce to whd normal form or to an applied constant that does not hide a reducible iota/fix/cofix redex (the "simpl" tactic) *) and whd_simpl_stack env sigma = let open ReductionBehaviour in let rec redrec s = - let (x, stack) = decompose_app_vect sigma s in - let stack = Array.to_list stack in - let s' = (x, stack) in + let s' = push_app sigma s in + let (x, stack) = s' in match EConstr.kind sigma x with | Lambda (na,t,c) -> (match stack with | [] -> s' - | a :: rest -> redrec (beta_applist sigma (x, stack))) - | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack)) - | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack)) - | Cast (c,_,_) -> redrec (applist(c, stack)) + | a :: rest -> redrec (beta_applist sigma [a] c rest)) + | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack) + | App (f,cl) -> assert false (* see push_app above *) + | Cast (c,_,_) -> redrec (c, stack) | Case (ci,p,iv,c,lf) -> (try - redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack)) + redrec (special_red_case env sigma (ci,p,iv,c,lf), stack) with Redelimination -> s') | Fix fix -> - (try match reduce_fix (whd_construct_stack env) sigma fix stack with - | Reduced s' -> redrec (applist s') + (try match reduce_fix env sigma fix stack with + | Reduced s' -> redrec s' | NotReducible -> s' with Redelimination -> s') @@ -800,11 +717,11 @@ and whd_simpl_stack env sigma = (match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') + | Reduced s' -> redrec s' | NotReducible -> s') | _ -> match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') + | Reduced s' -> redrec s' | NotReducible -> s') else s' with Redelimination -> s') @@ -814,7 +731,7 @@ and whd_simpl_stack env sigma = | Some (ref, u) -> (try let sapp, nocase = red_elim_const env sigma ref u stack in - let hd, _ as s'' = redrec (applist(sapp)) in + let hd, _ as s'' = redrec sapp in let rec is_case x = match EConstr.kind sigma x with | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x | App (hd, _) -> is_case hd @@ -827,10 +744,102 @@ and whd_simpl_stack env sigma = in redrec +and reduce_fix env sigma fix stack = + match fix_recarg fix stack with + | None -> NotReducible + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg') = whd_construct_stack env sigma recarg in + let stack' = List.assign stack recargnum (applist recarg') in + (match EConstr.kind sigma recarg'hd with + | Construct _ -> Reduced (contract_fix sigma fix, stack') + | _ -> NotReducible) + +and reduce_fix_use_function env sigma f fix stack = + match fix_recarg fix stack with + | None -> NotReducible + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg') = + if EConstr.isRel sigma recarg then + (* The recarg cannot be a local def, no worry about the right env *) + (recarg, []) + else + whd_construct_stack env sigma recarg in + let stack' = List.assign stack recargnum (applist recarg') in + (match EConstr.kind sigma recarg'hd with + | Construct _ -> + let (names, (nbfix, lv, n)), u, largs = f in + let lu = List.firstn n largs in + let p = List.length lv in + let lyi = List.map fst lv in + let la = + List.map_i (fun q aq -> + (* k from the comment is q+1 *) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) + with Not_found -> Vars.lift p aq) + 0 lu + in + let f i = match names.(i) with + | None -> None + | Some (minargs,ref) -> + let body = applist (mkEvalRef ref u, la) in + let g = + List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> + let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in + let tij' = Vars.substl (List.rev subst) tij in + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) + in Some (minargs,g) + in + Reduced (contract_fix_use_function env sigma f fix,stack') + | _ -> NotReducible) + +and reduce_proj env sigma c = + let rec redrec s = + match EConstr.kind sigma s with + | Proj (proj, c) -> + let c' = try redrec c with Redelimination -> c in + let constr, cargs = whd_construct_stack env sigma c' in + (match EConstr.kind sigma constr with + | Construct _ -> + let proj_narg = Projection.npars proj + Projection.arg proj in + List.nth cargs proj_narg + | _ -> raise Redelimination) + | Case (n,p,iv,c,brs) -> + let c' = redrec c in + let p = (n,p,iv,c',brs) in + (try special_red_case env sigma p + with Redelimination -> mkCase p) + | _ -> raise Redelimination + in redrec c + +and special_red_case env sigma (ci, p, iv, c, lf) = + let rec redrec s = + let (constr, cargs) = whd_simpl_stack env sigma s in + match match_eval_ref env sigma constr cargs with + | Some (ref, u) -> + (match reference_opt_value env sigma ref u with + | None -> raise Redelimination + | Some gvalue -> + if reducible_mind_case sigma gvalue then + reduce_mind_case_use_function constr env sigma + {mP=p; mconstr=gvalue; mcargs=cargs; + mci=ci; mlf=lf} + else + redrec (gvalue, cargs)) + | None -> + if reducible_mind_case sigma constr then + reduce_mind_case sigma + {mP=p; mconstr=constr; mcargs=cargs; + mci=ci; mlf=lf} + else + raise Redelimination + in + redrec (push_app sigma (c, [])) + (* reduce until finding an applied constructor or fail *) and whd_construct_stack env sigma s = - let (constr, cargs as s') = whd_simpl_stack env sigma s in + let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in if reducible_mind_case sigma constr then s' else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> @@ -855,13 +864,13 @@ let try_red_product env sigma c = | App (f,l) -> (match EConstr.kind sigma f with | Fix fix -> - let stack = Stack.append_app l Stack.empty in - (match fix_recarg fix stack with + (match fix_recarg fix (Array.to_list l) with | None -> raise Redelimination | Some (recargnum,recarg) -> let recarg' = redrec env recarg in - let stack' = Stack.assign stack recargnum recarg' in - simpfun (Stack.zip sigma (f,stack'))) + let l = Array.copy l in + let () = Array.set l recargnum recarg' in + simpfun (mkApp (f, l))) | _ -> simpfun (mkApp (redrec env f, l))) | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> @@ -973,19 +982,19 @@ let whd_simpl_orelse_delta_but_fix env sigma c = if List.length stack <= npars then (* Do not show the eta-expanded form *) s' - else redrec (applist (c, stack)) - | _ -> redrec (applist(c, stack))) + else redrec (c, stack) + | _ -> redrec (c, stack)) | None -> s' in let simpfun = clos_norm_flags betaiota env sigma in simpfun (applist (redrec c)) -let hnf_constr = whd_simpl_orelse_delta_but_fix +let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) (* The "simpl" reduction tactic *) let whd_simpl env sigma c = - applist (whd_simpl_stack env sigma c) + applist (whd_simpl_stack env sigma (c, [])) let simpl env sigma c = strong whd_simpl env sigma c @@ -1267,11 +1276,10 @@ let one_step_reduce env sigma c = | Cast (c,_,_) -> redrec (c,stack) | Case (ci,p,iv,c,lf) -> (try - (special_red_case env sigma (whd_simpl_stack env sigma) - (ci,p,iv,c,lf), stack) + (special_red_case env sigma (ci,p,iv,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (try match reduce_fix (whd_construct_stack env) sigma fix stack with + (try match reduce_fix env sigma fix stack with | Reduced s' -> s' | NotReducible -> raise NotStepReducible with Redelimination -> raise NotStepReducible) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b4a1153731..756ccd3438 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -332,6 +332,23 @@ let judge_of_int env v = let judge_of_float env v = Environ.on_judgment EConstr.of_constr (judge_of_float env v) +let judge_of_array env sigma u tj defj tyj = + let ulev = match Univ.Instance.to_array u with + | [|u|] -> u + | _ -> assert false + in + let sigma = Evd.set_leq_sort env sigma tyj.utj_type + (Sorts.sort_of_univ (Univ.Universe.make ulev)) + in + let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in + let sigma = check_one sigma defj in + let sigma = Array.fold_left check_one sigma tj in + let arr = EConstr.of_constr @@ type_of_array env u in + let j = make_judge (mkArray(EInstance.make u, Array.map j_val tj, defj.uj_val, tyj.utj_val)) + (mkApp (arr, [|tyj.utj_val|])) + in + sigma, j + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env sigma cstr = @@ -455,6 +472,13 @@ let rec execute env sigma cstr = | Float f -> sigma, judge_of_float env f + | Array(u,t,def,ty) -> + let sigma, tyj = execute env sigma ty in + let sigma, tyj = type_judgment env sigma tyj in + let sigma, defj = execute env sigma def in + let sigma, tj = execute_array env sigma t in + judge_of_array env sigma (EInstance.kind sigma u) tj defj tyj + and execute_recdef env sigma (names,lar,vdef) = let sigma, larj = execute_array env sigma lar in let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ef58f41489..a26c981cb9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -564,7 +564,7 @@ let is_rigid_head sigma flags t = match EConstr.kind sigma t with | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst) | Ind (i,u) -> true - | Construct _ | Int _ | Float _ -> true + | Construct _ | Int _ | Float _ | Array _ -> true | Fix _ | CoFix _ -> true | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _) @@ -659,7 +659,7 @@ let rec is_neutral env sigma ts t = | Evar _ | Meta _ -> true | Case (_, p, _, c, _) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c - | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false + | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) | Fix _ -> false (* This is an approximation *) | App _ -> assert false @@ -1819,6 +1819,15 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) + | Array(_u,t,def,ty) -> + (try + matchrec def + with ex when precatchable_exception ex -> + try + matchrec ty + with ex when precatchable_exception ex -> + iter_fail matchrec t) + | Cast (_, _, _) (* Is this expected? *) | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> user_err Pp.(str "Match_subterm"))) @@ -1887,6 +1896,9 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Lambda (_,t,c) -> bind (matchrec t) (matchrec c) + | Array(_u,t,def,ty) -> + bind (bind (bind_iter matchrec t) (matchrec def)) (matchrec ty) + | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *) | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index efe1efd74e..e5fa9bada1 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -170,6 +170,7 @@ and nf_whd env sigma whd typ = mkApp(capp,args) | Vint64 i -> i |> Uint63.of_int64 |> mkInt | Vfloat64 f -> f |> Float64.of_float |> mkFloat + | Varray t -> nf_array env sigma t typ | Vatom_stk(Aid idkey, stk) -> constr_type_of_idkey env sigma idkey stk | Vatom_stk(Aind ((mi,i) as ind), stk) -> @@ -261,12 +262,6 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> assert (from = 0) ; - let ci = sw.sw_annot.Vmvalues.ci in - let () = if Typeops.should_invert_case env ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.") - in let ((mind,_ as ind), u), allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in @@ -274,7 +269,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in + let p, relevance = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env sigma ind mib mip u params p in (* calcul des branches *) @@ -286,7 +281,12 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk + let ci = Inductiveops.make_case_info env ind relevance RegularStyle in + let iv = if Typeops.should_invert_case env ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in + nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in @@ -296,17 +296,17 @@ and nf_stk ?from:(from=0) env sigma c t stk = and nf_predicate env sigma ind mip params v pT = match kind (whd_allnolet env pT) with | LetIn (name,b,t,pT) -> - let body = + let body, rel = nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in - mkLetIn (name,b,t,body) + mkLetIn (name,b,t,body), rel | Prod (name,dom,codom) -> begin match whd_val v with | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let body = + let body, rel = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - mkLambda(name,dom,body) + mkLambda(name,dom,body), rel | _ -> assert false end | _ -> @@ -321,8 +321,10 @@ and nf_predicate env sigma ind mip params v pT = let dom = mkApp(mkIndU ind,Array.append params rargs) in let r = Inductive.relevance_of_inductive env (fst ind) in let name = make_annot name r in - let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in - mkLambda(name,dom,body) + let env = push_rel (LocalAssum (name,dom)) env in + let body = nf_vtype env sigma vb in + let rel = Retyping.relevance_of_type env sigma (EConstr.of_constr body) in + mkLambda(name,dom,body), rel | _ -> assert false and nf_args env sigma vargs ?from:(f=0) t = @@ -399,6 +401,14 @@ and nf_cofix env sigma cf = let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in mkCoFix (init,(names,cft,cfb)) +and nf_array env sigma t typ = + let ty, allargs = decompose_appvect (whd_all env typ) in + let typ_elem = allargs.(0) in + let t, vdef = Parray.to_array t in + let t = Array.map (fun v -> nf_val env sigma v typ_elem) t in + let u = snd (destConst ty) in + mkArray(u, t, nf_val env sigma vdef typ_elem, typ_elem) + let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); |