From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Feb 2018 01:02:17 +0100 Subject: Primitive integers This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux Co-authored-by: Benjamin Grégoire Co-authored-by: Vincent Laporte --- kernel/reduction.ml | 177 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 106 insertions(+), 71 deletions(-) (limited to 'kernel/reduction.ml') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 97cd4c00d7..61051c001d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -21,6 +21,7 @@ open CErrors open Util open Names open Constr +open Declarations open Vars open Environ open CClosure @@ -59,16 +60,23 @@ let compare_stack_shape stk1 stk2 = Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 + | Zprimitive(op1,_,rargs1, _kargs1)::s1, Zprimitive(op2,_,rargs2, _kargs2)::s2 -> + bal=0 && op1=op2 && List.length rargs1=List.length rargs2 && + compare_rec 0 s1 s2 | [], _ :: _ - | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false + | (Zproj _ | ZcaseT _ | Zfix _ | Zprimitive _) :: _, _ -> false in compare_rec 0 stk1 stk2 +type lft_fconstr = lift * fconstr + type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * constr * constr array * fconstr subs + | Zlprimitive of + CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args and lft_constr_stack = lft_constr_stack_elt list let rec zlapp v = function @@ -102,7 +110,10 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,p,br,e)::pstk)) + (l,Zlcase(ci,l,p,br,e)::pstk) + | (Zprimitive(op,c,rargs,kargs),(l,pstk)) -> + (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs, + List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk)) in snd (pure_rec lfts stk) @@ -127,10 +138,10 @@ let nf_betaiota env t = let whd_betaiotazeta env x = match kind x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _) -> x + Prod _|Lambda _|Fix _|CoFix _|Int _) -> x | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) @@ -141,10 +152,10 @@ let whd_betaiotazeta env x = let whd_all env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _) -> t + Prod _|Lambda _|Fix _|CoFix _|Int _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | Int _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos all env) (create_tab ()) (inject t) @@ -155,10 +166,10 @@ let whd_all env t = let whd_allnolet env t = match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| - Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) @@ -296,6 +307,15 @@ let rec skip_pattern n c = | Lambda (_, _, c) -> skip_pattern (pred n) c | _ -> raise IrregularPatternShape +let unfold_ref_with_args infos tab fl v = + match unfold_reference infos tab fl with + | Def def -> Some (def, v) + | Primitive op when check_native_args op v -> + let c = match fl with ConstKey c -> c | _ -> assert false in + let rargs, a, nargs, v = get_native_args1 op c v in + Some (whd_stack infos tab a (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) + | Undef _ | OpaqueDef _ | Primitive _ -> None + type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -355,28 +375,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try - let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> - (* else the oracle tells which constant is to be expanded *) + (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos.cnv_inf in let (app1,app2) = + let aux appr1 lft1 fl1 tab1 v1 appr2 lft2 fl2 tab2 v2 = + match unfold_ref_with_args infos.cnv_inf tab1 fl1 v1 with + | Some t1 -> ((lft1, t1), appr2) + | None -> match unfold_ref_with_args infos.cnv_inf tab2 fl2 v2 with + | Some t2 -> (appr1, (lft2, t2)) + | None -> raise NotConvertible + in if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then - match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> ((lft1, (def1, v1)), appr2) - | None -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> (appr1, (lft2, (def2, v2))) - | None -> raise NotConvertible) + aux appr1 lft1 fl1 infos.lft_tab v1 appr2 lft2 fl2 infos.rgt_tab v2 else - match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> (appr1, (lft2, (def2, v2))) - | None -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> ((lft1, (def1, v1)), appr2) - | None -> raise NotConvertible) - in - eqappr cv_pb l2r infos app1 app2 cuniv) + let (app2,app1) = aux appr2 lft2 fl2 infos.rgt_tab v2 appr1 lft1 fl1 infos.lft_tab v1 in + (app1,app2) + in + eqappr cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -400,31 +418,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = raise NotConvertible) | (FProj (p1,c1), t2) -> - (match unfold_projection infos.cnv_inf p1 with - | Some s1 -> + begin match unfold_projection infos.cnv_inf p1 with + | Some s1 -> eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv - | None -> - (match t2 with - | FFlex fl2 -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv - | None -> raise NotConvertible) - | _ -> raise NotConvertible)) - + | None -> + begin match t2 with + | FFlex fl2 -> + begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with + | Some t2 -> + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + | None -> raise NotConvertible + end + | _ -> raise NotConvertible + end + end + | (t1, FProj (p2,c2)) -> - (match unfold_projection infos.cnv_inf p2 with - | Some s2 -> + begin match unfold_projection infos.cnv_inf p2 with + | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv - | None -> - (match t1 with - | FFlex fl1 -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv - | None -> raise NotConvertible) - | _ -> raise NotConvertible)) - + | None -> + begin match t1 with + | FFlex fl1 -> + begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with + | Some t1 -> + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + | None -> raise NotConvertible + end + | _ -> raise NotConvertible + end + end + (* other constructors *) | (FLambda _, FLambda _) -> (* Inconsistency: we tolerate that v1, v2 contain shift and update but @@ -469,8 +493,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> - (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with - | Some def1 -> + begin match unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 with + | Some (def1,v1) -> (** By virtue of the previous case analyses, we know [c2] is rigid. Conversion check to rigid terms eventually implies full weak-head reduction, so instead of repeatedly performing small-step @@ -478,32 +502,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv - | None -> - match c2 with + | None -> + (match c2 with | FConstruct ((ind2,_j2),_u2) -> - (try - let v2, v1 = - eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) - + (try + let v2, v1 = + eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible) + end + | (c1, FFlex fl2) -> - (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with - | Some def2 -> + begin match unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 with + | Some (def2, v2) -> (** Symmetrical case of above. *) let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv - | None -> - match c1 with - | FConstruct ((ind1,_j1),_u1) -> - (try let v1, v2 = - eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) - + | None -> + match c1 with + | FConstruct ((ind1,_j1),_u1) -> + (try let v1, v2 = + eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | _ -> raise NotConvertible + end + (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then @@ -584,13 +610,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible + | FInt i1, FInt i2 -> + if Uint63.equal i1 i2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + else raise NotConvertible + (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ - | FProd _ | FEvar _), _ -> raise NotConvertible + | FProd _ | FEvar _ | FInt _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in @@ -613,7 +643,12 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = raise NotConvertible; let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 - | _ -> assert false) + | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) -> + if not (CPrimitives.equal op1 op2) then raise NotConvertible else + let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in + let fk (_,a1) (_,a2) cu = f a1 a2 cu in + List.fold_right2 fk kargs1 kargs2 cu2 + | ((Zlapp _ | Zlproj _ | Zlfix _| Zlcase _| Zlprimitive _), _) -> assert false) | _ -> cuniv in if compare_stack_shape stk1 stk2 then cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv -- cgit v1.2.3