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 --- tactics/term_dnet.ml | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) (limited to 'tactics') diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e273891500..e8a66f1889 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -44,6 +44,7 @@ struct | DCase of case_info * 't * 't * 't array | DFix of int array * int * 't array * 't array | DCoFix of int * 't array * 't array + | DInt of Uint63.t (* special constructors only inside the left-hand side of DCtx or DApp. Used to encode lists of foralls/letins/apps as contexts *) @@ -61,6 +62,7 @@ struct | DCase (_,t1,t2,ta) -> str "case" | DFix _ -> str "fix" | DCoFix _ -> str "cofix" + | DInt _ -> str "INT" | DCons ((t,dopt),tl) -> f t ++ (match dopt with Some t' -> str ":=" ++ f t' | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl @@ -72,7 +74,7 @@ struct *) let map f = function - | (DRel | DSort | DNil | DRef _) as c -> c + | (DRel | DSort | DNil | DRef _ | DInt _) as c -> c | DCtx (ctx,c) -> DCtx (f ctx, f c) | DLambda (t,c) -> DLambda (f t, f c) | DApp (t,u) -> DApp (f t,f u) @@ -145,6 +147,10 @@ struct else c | DCoFix _, _ -> -1 | _, DCoFix _ -> 1 + | DInt i1, DInt i2 -> Uint63.compare i1 i2 + + | DInt _, _ -> -1 | _, DInt _ -> 1 + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> let c = cmp t1 t2 in if Int.equal c 0 then @@ -157,7 +163,7 @@ struct | DNil, DNil -> 0 let fold f acc = function - | (DRel | DNil | DSort | DRef _) -> acc + | (DRel | DNil | DSort | DRef _ | DInt _) -> acc | DCtx (ctx,c) -> f (f acc ctx) c | DLambda (t,c) -> f (f acc t) c | DApp (t,u) -> f (f acc t) u @@ -169,7 +175,7 @@ struct | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u let choose f = function - | (DRel | DSort | DNil | DRef _) -> invalid_arg "choose" + | (DRel | DSort | DNil | DRef _ | DInt _) -> invalid_arg "choose" | DCtx (ctx,c) -> f ctx | DLambda (t,c) -> f t | DApp (t,u) -> f u @@ -185,7 +191,8 @@ struct if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0) then invalid_arg "fold2:compare" else match c1,c2 with - | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc + | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _ + | DInt _, DInt _) -> acc | (DCtx (c1,t1), DCtx (c2,t2) | DApp (c1,t1), DApp (c2,t2) | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 @@ -198,14 +205,15 @@ struct | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in if not (Int.equal (compare dummy_cmp (head c1) (head c2)) 0) then invalid_arg "map2_t:compare" else match c1,c2 with - | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc -> + | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _ + | DInt _, DInt _) as cc -> let (c,_) = cc in c | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) @@ -219,10 +227,10 @@ struct | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false let terminal = function - | (DRel | DSort | DNil | DRef _) -> true + | (DRel | DSort | DNil | DRef _ | DInt _) -> true | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> false @@ -315,6 +323,7 @@ struct (pat_of_constr f) (Array.map pat_of_constr ca) | Proj (p,c) -> Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) + | Int i -> Term (DInt i) and ctx_of_constr ctx c = match Constr.kind c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c -- cgit v1.2.3