Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)(* Extension to mutual inductive constructions by Christine Paulin for Coq V5.10.2 *)(* Extension to co-inductive constructions by Eduardo Gimenez *)(* Optimization of substitution functions by Chet Murthy *)(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)(* Hash-consing by Bruno Barras in Feb 1998 *)(* Restructuration of Coq of the type-checking kernel by Jean-Christophe Filliâtre, 1999 *)(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
(* This file defines the internal syntax of the Calculus of Inductive Constructions (CIC) terms together with constructors, destructors, iterators and basic functions *)
open Utilopen Namesopen UVarsopen Context
type existential_key = Evar.ttype metavariable = int
(* This defines the strategy to use for verifiying a Cast *)type cast_kind = VMcast | NATIVEcast | DEFAULTcast
(* This defines Cases annotations *)type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyletype case_printing = { style : case_style }
(* INVARIANT: * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)), * ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i) *)type case_info = { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) ci_npar : int; (* number of parameters of the above inductive type *) ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines the number of values that can be bound in a match-construct. NOTE: parameters of the inductive type are therefore excluded from the count *) ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines the number of values that can be applied to the constructor, in addition to the parameters of the related inductive type NOTE: "lets" are therefore excluded from the count NOTE: parameters of the inductive type are also excluded from the count *) ci_pp_info : case_printing (* not interpreted by the kernel *) }
(********************************************************************)(* Constructions as implemented *)(********************************************************************)
(* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *)type 'constr pexistential = existential_key * 'constr SList.ttype ('constr, 'types, 'r) prec_declaration = (Name.t,'r) pbinder_annot array * 'types array * 'constr arraytype ('constr, 'types, 'r) pfixpoint = (int array * int) * ('constr, 'types, 'r) prec_declarationtype ('constr, 'types, 'r) pcofixpoint = int * ('constr, 'types, 'r) prec_declarationtype 'a puniverses = 'a UVars.puniversestype pconstant = Constant.t puniversestype pinductive = inductive puniversestype pconstructor = constructor puniverses
type 'constr pcase_invert = | NoInvert | CaseInvert of { indices : 'constr array }
type ('constr,'r) pcase_branch = (Name.t,'r) Context.pbinder_annot array * 'constrtype ('types,'r) pcase_return = ((Name.t,'r) Context.pbinder_annot array * 'types) * 'r
type ('constr, 'types, 'univs, 'r) pcase = case_info * 'univs * 'constr array * ('types,'r) pcase_return * 'constr pcase_invert * 'constr * ('constr, 'r) pcase_branch array
(* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *)type ('constr, 'types, 'sort, 'univs, 'r) kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of (Name.t,'r) pbinder_annot * 'types * 'types | Lambda of (Name.t,'r) pbinder_annot * 'types * 'constr | LetIn of (Name.t,'r) pbinder_annot * 'constr * 'types * 'constr | App of 'constr * 'constr array | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'univs * 'constr array * ('types,'r) pcase_return * 'constr pcase_invert * 'constr * ('constr,'r) pcase_branch array | Fix of ('constr, 'types, 'r) pfixpoint | CoFix of ('constr, 'types, 'r) pcofixpoint | Proj of Projection.t * 'r * 'constr | Int of Uint63.t | Float of Float64.t | String of Pstring.t | Array of 'univs * 'constr array * 'constr * 'types
(* constr is the fixpoint of the previous type. *)type t = T of (t, t, Sorts.t, Instance.t, Sorts.relevance) kind_of_term [@@unboxed]type constr = ttype types = constr
type existential = existential_key * constr SList.t
type case_invert = constr pcase_inverttype case_return = (types,Sorts.relevance) pcase_returntype case_branch = (constr,Sorts.relevance) pcase_branchtype case = (constr, types, Instance.t, Sorts.relevance) pcasetype rec_declaration = (constr, types, Sorts.relevance) prec_declarationtype fixpoint = (constr, types, Sorts.relevance) pfixpointtype cofixpoint = (constr, types, Sorts.relevance) pcofixpointtype 'a binder_annot = ('a,Sorts.relevance) Context.pbinder_annot
(************************************************************************)(* kind_of_term = constructions as seen by the user *)(************************************************************************)
(* User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative term *)
let kind (T c) = c
let rec kind_nocast_gen kind c = match kind c with | Cast (c, _, _) -> kind_nocast_gen kind c | App (h, outer) as k -> (match kind_nocast_gen kind h with | App (h, inner) -> App (h, Array.append inner outer) | _ -> k) | k -> k
let kind_nocast c = kind_nocast_gen kind c
(**********************************************************************)(* Non primitive term destructors *)(**********************************************************************)
(* Destructor operations : partial functions Raise [DestKO] if the const has not the expected form *)
exception DestKO
let isMeta c = match kind c with Meta _ -> true | _ -> false
(* Destructs a type *)let isSort c = match kind c with | Sort _ -> true | _ -> false
let rec isprop c = match kind c with | Sort (Sorts.Prop | Sorts.Set) -> true | Cast (c,_,_) -> isprop c | _ -> false
let rec is_Prop c = match kind c with | Sort Sorts.Prop -> true | Cast (c,_,_) -> is_Prop c | _ -> false
let rec is_Set c = match kind c with | Sort Sorts.Set -> true | Cast (c,_,_) -> is_Set c | _ -> false
let rec is_Type c = match kind c with | Sort (Sorts.Type _) -> true | Cast (c,_,_) -> is_Type c | _ -> false
let iskind c = isprop c || is_Type c
(* Tests if an evar *)let isEvar c = match kind c with Evar _ -> true | _ -> falselet isEvar_or_Meta c = match kind c with | Evar _ | Meta _ -> true | _ -> false
let isCast c = match kind c with Cast _ -> true | _ -> false(* Tests if a de Bruijn index *)let isRel c = match kind c with Rel _ -> true | _ -> falselet isRelN n c = match kind c with Rel n' -> Int.equal n n' | _ -> false(* Tests if a variable *)let isVar c = match kind c with Var _ -> true | _ -> falselet isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false(* Tests if an inductive *)let isInd c = match kind c with Ind _ -> true | _ -> falselet isProd c = match kind c with | Prod _ -> true | _ -> falselet isLambda c = match kind c with | Lambda _ -> true | _ -> falselet isLetIn c = match kind c with LetIn _ -> true | _ -> falselet isApp c = match kind c with App _ -> true | _ -> falselet isConst c = match kind c with Const _ -> true | _ -> falselet isConstruct c = match kind c with Construct _ -> true | _ -> falselet isCase c = match kind c with Case _ -> true | _ -> falselet isProj c = match kind c with Proj _ -> true | _ -> falselet isFix c = match kind c with Fix _ -> true | _ -> falselet isCoFix c = match kind c with CoFix _ -> true | _ -> false
let isRef c = match kind c with | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false
(* Destructs a de Bruijn index *)let destRel c = match kind c with | Rel n -> n | _ -> raise DestKO
(* Destructs an existential variable *)let destMeta c = match kind c with | Meta n -> n | _ -> raise DestKO
(* Destructs a variable *)let destVar c = match kind c with | Var id -> id | _ -> raise DestKO
let destSort c = match kind c with | Sort s -> s | _ -> raise DestKO
(* Destructs a casted term *)let destCast c = match kind c with | Cast (t1,k,t2) -> (t1,k,t2) | _ -> raise DestKO
(* Destructs the product (x:t1)t2 *)let destProd c = match kind c with | Prod (x,t1,t2) -> (x,t1,t2) | _ -> raise DestKO
(* Destructs the abstraction [x:t1]t2 *)let destLambda c = match kind c with | Lambda (x,t1,t2) -> (x,t1,t2) | _ -> raise DestKO
(* Destructs the let [x:=b:t1]t2 *)let destLetIn c = match kind c with | LetIn (x,b,t1,t2) -> (x,b,t1,t2) | _ -> raise DestKO
(* Destructs an application *)let destApp c = match kind c with | App (f,a) -> (f, a) | _ -> raise DestKO
(* Destructs a constant *)let destConst c = match kind c with | Const kn -> kn | _ -> raise DestKO
(* Destructs an existential variable *)let destEvar c = match kind c with | Evar (_kn, _a as r) -> r | _ -> raise DestKO
(* Destructs a (co)inductive type named kn *)let destInd c = match kind c with | Ind (_kn, _a as r) -> r | _ -> raise DestKO
(* Destructs a constructor *)let destConstruct c = match kind c with | Construct (_kn, _a as r) -> r | _ -> raise DestKO
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)let destCase c = match kind c with | Case (ci,u,params,p,iv,c,v) -> (ci,u,params,p,iv,c,v) | _ -> raise DestKO
let destProj c = match kind c with | Proj (p, r, c) -> (p, r, c) | _ -> raise DestKO
let destFix c = match kind c with | Fix fix -> fix | _ -> raise DestKO
let destCoFix c = match kind c with | CoFix cofix -> cofix | _ -> raise DestKO
let destRef c = let open GlobRef in match kind c with | Var x -> VarRef x, UVars.Instance.empty | Const (c,u) -> ConstRef c, u | Ind (ind,u) -> IndRef ind, u | Construct (c,u) -> ConstructRef c, u | _ -> raise DestKO
let destArray c = match kind c with | Array (u,ar,def,ty) -> u,ar,def,ty | _ -> raise DestKO
(******************************************************************)(* Flattening and unflattening of embedded applications and casts *)(******************************************************************)
let decompose_app_list c = match kind c with | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[])
let decompose_app c = match kind c with | App (f,cl) -> (f, cl) | _ -> (c,[||])
(*********************)(* Term constructors *)(*********************)
(* Constructs a de Bruijn index with number n *)let rels = Array.init 17 (fun i -> T (Rel i))
let mkRel n = if 0<=n && n<=16 then rels.(n) else T (Rel n)
let mkSProp = T (Sort Sorts.sprop)let mkProp = T (Sort Sorts.prop)let mkSet = T (Sort Sorts.set)
(* Enforces: - applicative terms have at least one argument and the function is not itself an applicative term - stacks of VM or native casts are collapsed - small rels are shared - small sorts are shared*)let of_kind = function| Rel n when 0 <= n && n < Array.length rels -> rels.(n)| App (f, [||]) -> f| App (f, a) as k -> begin match kind f with | App (g, cl) -> T (App (g, Array.append cl a)) | _ -> T k end| Cast (c, knd, t) as k -> begin match kind c with | Cast (c, knd', _) when (knd == VMcast || knd == NATIVEcast) && knd == knd' -> T (Cast (c, knd, t)) | _ -> T k end| Sort Sorts.SProp -> mkSProp| Sort Sorts.Prop -> mkProp| Sort Sorts.Set -> mkSet| k -> T k
(* Construct a type *)let mkType u = of_kind @@ Sort (Sorts.sort_of_univ u)let mkSort s = of_kind @@ Sort s
(* Constructs the product (x:t1)t2 *)let mkProd (x,t1,t2) = of_kind @@ Prod (x,t1,t2)
(* Constructs the abstraction [x:t1]t2 *)let mkLambda (x,t1,t2) = of_kind @@ Lambda (x,t1,t2)
(* Constructs [x=c_1:t]c_2 *)let mkLetIn (x,c1,t,c2) = of_kind @@ LetIn (x,c1,t,c2)
let mkApp (f, a) = of_kind (App (f, a))
(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)(* (that means t2 is declared as the type of t1) *)let mkCast (t1,k,t2) = of_kind @@ Cast (t1,k,t2)
let map_puniverses f (x,u) = (f x, u)let in_punivs a = (a, UVars.Instance.empty)
(* Constructs a constant *)let mkConst c = of_kind @@ Const (in_punivs c)let mkConstU c = of_kind @@ Const c
(* Constructs an applied projection *)let mkProj (p,r,c) = of_kind @@ Proj (p,r,c)
(* Constructs an existential variable *)let mkEvar e = of_kind @@ Evar e
(* Constructs the ith (co)inductive type of the block named kn *)let mkInd m = of_kind @@ Ind (in_punivs m)let mkIndU m = of_kind @@ Ind m
(* Constructs the jth constructor of the ith (co)inductive type of the block named kn. *)let mkConstruct c = of_kind @@ Construct (in_punivs c)let mkConstructU c = of_kind @@ Construct clet mkConstructUi ((ind,u),i) = of_kind @@ Construct ((ind,i),u)
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)let mkCase (ci, u, params, p, iv, c, ac) = of_kind @@ Case (ci, u, params, p, iv, c, ac)
(* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] typarray = [|t1,...tn|] bodies = [|b1,...bn|] then
mkFix ((recindxs,i),(funnames,typarray,bodies))
constructs the ith function of the block
Fixpoint f1 [ctx1] : t1 := b1 with f2 [ctx2] : t2 := b2 ... with fn [ctxn] : tn := bn.
where the length of the jth context is ij.*)
let mkFix fix = of_kind @@ Fix fix
(* If funnames = [|f1,...fn|] typarray = [|t1,...tn|] bodies = [|b1,...bn|] then
mkCoFix (i,(funnames,typsarray,bodies))
constructs the ith function of the block
CoFixpoint f1 : t1 := b1 with f2 : t2 := b2 ... with fn : tn := bn.*)let mkCoFix cofix= of_kind @@ CoFix cofix
(* Constructs an existential variable named "?n" *)let mkMeta n = of_kind @@ Meta n
(* Constructs a Variable named id *)let mkVar id = of_kind @@ Var id
let mkRef (gr,u) = let open GlobRef in match gr with | ConstRef c -> mkConstU (c,u) | IndRef ind -> mkIndU (ind,u) | ConstructRef c -> mkConstructU (c,u) | VarRef x -> mkVar x
(* Constructs a primitive integer *)let mkInt i = of_kind @@ Int i
(* Constructs an array *)let mkArray (u,t,def,ty) = of_kind @@ Array (u,t,def,ty)
(* Constructs a primitive float number *)let mkFloat f = of_kind @@ Float f
(* Constructs a primitive string. *)let mkString s = of_kind @@ String s
module UnsafeMonomorphic = struct let mkConst = mkConst let mkInd = mkInd let mkConstruct = mkConstructend
(****************************************************************************)(* Functions to recur through subterms *)(****************************************************************************)
(* [fold f acc c] folds [f] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions; it is not recursive *)
let fold_invert f acc = function | NoInvert -> acc | CaseInvert {indices} -> Array.fold_left f acc indices
let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> acc | Cast (c,_,t) -> f (f acc c) t | Prod (_,t,c) -> f (f acc t) c | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l | Proj (_p,_r,c) -> f acc c | Evar (_,l) -> SList.Skip.fold f acc l | Case (_,_,pms,((_,p),_),iv,c,bl) -> Array.fold_left (fun acc (_, b) -> f acc b) (f (fold_invert f (f (Array.fold_left f acc pms) p) iv) c) bl | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl | Array(_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
(* [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *)
let iter_invert f = function | NoInvert -> () | CaseInvert {indices;} -> Array.iter f indices
let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> () | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l | Proj (_p,_r,c) -> f c | Evar (_,l) -> SList.Skip.iter f l | Case (_,_,pms,p,iv,c,bl) -> Array.iter f pms; f (snd @@ fst p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
(* [iter_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified *)
let iter_with_binders g f n c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> SList.Skip.iter (fun c -> f n c) l | Case (_,_,pms,(p,_),iv,c,bl) -> Array.Fun1.iter f n pms; f (iterate g (Array.length (fst p)) n) (snd p); iter_invert (f n) iv; f n c; Array.Fun1.iter (fun n (ctx, b) -> f (iterate g (Array.length ctx) n) b) n bl | Proj (_p,_r,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl | CoFix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl | Array(_u,t,def,ty) -> Array.iter (f n) t; f n def; f n ty
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions as [fold_constr] but it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *)
let fold_constr_with_binders g f n acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (_na,t,c) -> f (g n) (f n acc t) c | Lambda (_na,t,c) -> f (g n) (f n acc t) c | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_p,_r,c) -> f n acc c | Evar (_,l) -> SList.Skip.fold (f n) acc l | Case (_,_,pms,(p,_),iv,c,bl) -> let fold_ctx n accu (nas, c) = f (iterate g (Array.length nas) n) accu c in Array.fold_left (fold_ctx n) (f n (fold_invert (f n) (fold_ctx n (Array.fold_left (f n) acc pms) p) iv) c) bl | Fix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(_,tl,bl)) -> let n' = iterate g (Array.length tl) n in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
(* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *)
let map_under_context f d = let (nas, p) = d in let p' = f p in if p' == p then d else (nas, p')
let map_branches f bl = let bl' = Array.map (map_under_context f) bl in if Array.for_all2 (==) bl' bl then bl else bl'
let map_return_predicate f (p,r as v) = let p' = map_under_context f p in if p == p' then v else p', r
let map_under_context_with_binders g f l d = let (nas, p) = d in let l = iterate g (Array.length nas) l in let p' = f l p in if p' == p then d else (nas, p')
let map_branches_with_binders g f l bl = let bl' = Array.map (map_under_context_with_binders g f l) bl in if Array.for_all2 (==) bl' bl then bl else bl'
let map_return_predicate_with_binders g f l (p,r as v) = let p' = map_under_context_with_binders g f l p in if p == p' then v else p',r
let map_invert f = function | NoInvert -> NoInvert | CaseInvert {indices;} as orig -> let indices' = Array.Smart.map f indices in if indices == indices' then orig else CaseInvert {indices=indices';}
let map f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> c | Cast (b,k,t) -> let b' = f b in let t' = f t in if b'==b && t' == t then c else mkCast (b', k, t') | Prod (na,t,b) -> let b' = f b in let t' = f t in if b'==b && t' == t then c else mkProd (na, t', b') | Lambda (na,t,b) -> let b' = f b in let t' = f t in if b'==b && t' == t then c else mkLambda (na, t', b') | LetIn (na,b,t,k) -> let b' = f b in let t' = f t in let k' = f k in if b'==b && t' == t && k'==k then c else mkLetIn (na, b', t', k') | App (b,l) -> let b' = f b in let l' = Array.Smart.map f l in if b'==b && l'==l then c else mkApp (b', l') | Proj (p,r,t) -> let t' = f t in if t' == t then c else mkProj (p, r, t') | Evar (e,l) -> let l' = SList.Smart.map f l in if l'==l then c else mkEvar (e, l') | Case (ci,u,pms,p,iv,b,bl) -> let pms' = Array.Smart.map f pms in let b' = f b in let iv' = map_invert f iv in let p' = map_return_predicate f p in let bl' = map_branches f bl in if b'==b && iv'==iv && p'==p && bl'==bl && pms'==pms then c else mkCase (ci, u, pms', p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let tl' = Array.Smart.map f tl in let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.Smart.map f tl in let bl' = Array.Smart.map f bl in if tl'==tl && bl'==bl then c else mkCoFix (ln,(lna,tl',bl')) | Array(u,t,def,ty) -> let t' = Array.Smart.map f t in let def' = f def in let ty' = f ty in if def'==def && t==t' && ty==ty' then c else mkArray(u,t',def',ty')
(* Like {!map} but with an accumulator. *)
let fold_map_invert f acc = function | NoInvert -> acc, NoInvert | CaseInvert {indices;} as orig -> let acc, indices' = Array.Smart.fold_left_map f acc indices in if indices==indices' then acc, orig else acc, CaseInvert {indices=indices';}
let fold_map_under_context f accu d = let (nas, p) = d in let accu, p' = f accu p in if p' == p then accu, d else accu, (nas, p')
let fold_map_branches f accu bl = let accu, bl' = Array.Smart.fold_left_map (fold_map_under_context f) accu bl in if Array.for_all2 (==) bl' bl then accu, bl else accu, bl'
let fold_map_return_predicate f accu (p,r as v) = let accu, p' = fold_map_under_context f accu p in let v = if p == p' then v else p', r in accu, v
let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> accu, c | Cast (b,k,t) -> let accu, b' = f accu b in let accu, t' = f accu t in if b'==b && t' == t then accu, c else accu, mkCast (b', k, t') | Prod (na,t,b) -> let accu, b' = f accu b in let accu, t' = f accu t in if b'==b && t' == t then accu, c else accu, mkProd (na, t', b') | Lambda (na,t,b) -> let accu, b' = f accu b in let accu, t' = f accu t in if b'==b && t' == t then accu, c else accu, mkLambda (na, t', b') | LetIn (na,b,t,k) -> let accu, b' = f accu b in let accu, t' = f accu t in let accu, k' = f accu k in if b'==b && t' == t && k'==k then accu, c else accu, mkLetIn (na, b', t', k') | App (b,l) -> let accu, b' = f accu b in let accu, l' = Array.Smart.fold_left_map f accu l in if b'==b && l'==l then accu, c else accu, mkApp (b', l') | Proj (p,r,t) -> let accu, t' = f accu t in if t' == t then accu, c else accu, mkProj (p, r, t') | Evar (e,l) -> let accu, l' = SList.Smart.fold_left_map f accu l in if l'==l then accu, c else accu, mkEvar (e, l') | Case (ci,u,pms,p,iv,b,bl) -> let accu, pms' = Array.Smart.fold_left_map f accu pms in let accu, p' = fold_map_return_predicate f accu p in let accu, iv' = fold_map_invert f accu iv in let accu, b' = f accu b in let accu, bl' = fold_map_branches f accu bl in if pms'==pms && p'==p && iv'==iv && b'==b && bl'==bl then accu, c else accu, mkCase (ci, u, pms', p', iv', b', bl') | Fix (ln,(lna,tl,bl)) -> let accu, tl' = Array.Smart.fold_left_map f accu tl in let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let accu, tl' = Array.Smart.fold_left_map f accu tl in let accu, bl' = Array.Smart.fold_left_map f accu bl in if tl'==tl && bl'==bl then accu, c else accu, mkCoFix (ln,(lna,tl',bl')) | Array(u,t,def,ty) -> let accu, t' = Array.Smart.fold_left_map f accu t in let accu, def' = f accu def in let accu, ty' = f accu ty in if def'==def && t==t' && ty==ty' then accu, c else accu, mkArray(u,t',def',ty')
(* [map_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified *)
let map_with_binders g f l c0 = match kind c0 with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ | String _) -> c0 | Cast (c, k, t) -> let c' = f l c in let t' = f l t in if c' == c && t' == t then c0 else mkCast (c', k, t') | Prod (na, t, c) -> let t' = f l t in let c' = f (g l) c in if t' == t && c' == c then c0 else mkProd (na, t', c') | Lambda (na, t, c) -> let t' = f l t in let c' = f (g l) c in if t' == t && c' == c then c0 else mkLambda (na, t', c') | LetIn (na, b, t, c) -> let b' = f l b in let t' = f l t in let c' = f (g l) c in if b' == b && t' == t && c' == c then c0 else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, r, t) -> let t' = f l t in if t' == t then c0 else mkProj (p, r, t') | Evar (e, al) -> let al' = SList.Smart.map (fun c -> f l c) al in if al' == al then c0 else mkEvar (e, al') | Case (ci, u, pms, p, iv, c, bl) -> let pms' = Array.Fun1.Smart.map f l pms in let p' = map_return_predicate_with_binders g f l p in let iv' = map_invert (f l) iv in let c' = f l c in let bl' = map_branches_with_binders g f l bl in if pms' == pms && p' == p && iv' == iv && c' == c && bl' == bl then c0 else mkCase (ci, u, pms', p', iv', c', bl') | Fix (ln, (lna, tl, bl)) -> let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) | Array(u,t,def,ty) -> let t' = Array.Fun1.Smart.map f l t in let def' = f l def in let ty' = f l ty in if def'==def && t==t' && ty==ty' then c0 else mkArray(u,t',def',ty')
(*********************)(* Lifting *)(*********************)
(* The generic lifting function *)let rec exliftn el c = let open Esubst in match kind c with | Rel i -> let j = reloc_rel i el in if Int.equal i j then c else mkRel j | _ -> map_with_binders el_lift exliftn el c
(* Lifting the binding depth across k bindings *)
let liftn n k c = let open Esubst in match el_liftn (pred k) (el_shft n el_id) with | ELID -> c | el -> exliftn el c
let lift n = liftn n 1
type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool
type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
(* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose the structure [c2]) using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, [u] to compare universe instances, and [s] to compare sorts; Cast's, application associativity, binders name and Cases annotations are not taken into account. Note that as [kind1] and [kind2] are potentially different, we cannot use, in recursive case, the optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *)
let eq_invert eq iv1 iv2 = match iv1, iv2 with | NoInvert, NoInvert -> true | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false | CaseInvert {indices}, CaseInvert iv2 -> Array.equal eq indices iv2.indices
let eq_under_context eq (_nas1, p1) (_nas2, p2) = eq p1 p2
let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq_evars eq leq nargs t1 t2 = match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Int i1, Int i2 -> Uint63.equal i1 i2 | Float f1, Float f2 -> Float64.equal f1 f2 | String s1, String s2 -> Pstring.equal s1 s2 | Sort s1, Sort s2 -> leq_sorts s1 s2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 | Proj (p1,_,c1), Proj (p2,_,c2) -> Projection.CanOrd.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> eq_evars (e1, l1) (e2, l2) | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 | Case (ci1,u1,pms1,(p1,_r1),iv1,c1,bl1), Case (ci2,u2,pms2,(p2,_r2),iv2,c2,bl2) -> (* Ignore _r1/_r2: implied by comparing p1/p2 *) (** FIXME: what are we doing with u1 = u2 ? *) Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 && Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 && eq_invert (eq 0) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) -> leq_universes None u1 u2 && Array.equal_norefl (eq 0) t1 t2 && eq 0 def1 def2 && eq 0 ty1 ty2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ | CoFix _ | Int _ | Float _ | String _ | Array _), _ -> false
(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe instances and [s] to compare sorts; Cast's, application associativity, binders name and Cases annotations are not taken into account.
[compare_head_gen_with] is a variant taking kind-of-term functions, to expose subterms of [c1] and [c2], as arguments. *)
let compare_head_gen eq_universes eq_sorts eq_evars eq t1 t2 = compare_head_gen_leq_with kind kind eq_universes eq_sorts eq_evars eq eq t1 t2
(*******************************)(* alpha conversion functions *)(*******************************)
(* alpha conversion : ignore print names and casts *)
let eq_existential eq (evk1, args1) (evk2, args2) = Evar.equal evk1 evk2 && SList.equal eq args1 args2
let rec eq_constr nargs m n = (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal (eq_existential (eq_constr 0)) eq_constr nargs m n
let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *)
let eq_constr_univs univs m n = if m == n then true else let eq_universes _ = UGraph.check_eq_instances Sorts.Quality.equal univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq_sort Sorts.Quality.equal univs s1 s2 in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts (eq_existential (eq_constr' 0)) eq_constr' nargs m n in compare_head_gen eq_universes eq_sorts (eq_existential (eq_constr' 0)) eq_constr' 0 m n
let leq_constr_univs univs m n = if m == n then true else let eq_universes _ = UGraph.check_eq_instances Sorts.Quality.equal univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq_sort Sorts.Quality.equal univs s1 s2 in let leq_sorts s1 s2 = s1 == s2 || UGraph.check_leq_sort Sorts.Quality.equal univs s1 s2 in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts (eq_existential (eq_constr' 0)) eq_constr' nargs m n in let rec compare_leq nargs m n = compare_head_gen_leq_with kind kind eq_universes leq_sorts (eq_existential (eq_constr' 0)) eq_constr' leq_constr' nargs m n and leq_constr' nargs m n = m == n || compare_leq nargs m n in compare_leq 0 m n
(*******************)(* hash-consing *)(*******************)
(* Hash-consing of [constr] does not use the module [Hashcons] because [Hashcons] is not efficient on deep tree-like data structures. Indeed, [Hashcons] is based the (very efficient) generic hash function [Hashtbl.hash], which computes the hash key through a depth bounded traversal of the data structure to be hashed. As a consequence, for a deep [constr] like the natural number 1000 (S (S (... (S O)))), the same hash is assigned to all the sub [constr]s greater than the maximal depth handled by [Hashtbl.hash]. This entails a huge number of collisions in the hash table and leads to cubic hash-consing in this worst-case.
In order to compute a hash key that is independent of the data structure depth while being constant-time, an incremental hashing function must be devised. A standard implementation creates a cache of the hashing function by decorating each node of the hash-consed data structure with its hash key. In that case, the hash function can deduce the hash key of a toplevel data structure by a local computation based on the cache held on its substructures. Unfortunately, this simple implementation introduces a space overhead that is damageable for the hash-consing of small [constr]s (the most common case). One can think of an heterogeneous distribution of caches on smartly chosen nodes, but this is forbidden by the use of generic equality in Rocq source code. (Indeed, this forces each [constr] to have a unique canonical representation.)
Given that hash-consing proceeds inductively, we can nonetheless computes the hash key incrementally during hash-consing by changing a little the signature of the hash-consing function: it now returns both the hash-consed term and its hash key. This simple solution is implemented in the following code: it does not introduce a space overhead in [constr], that's why the efficiency is unchanged for small [constr]s. Besides, it does handle deep [constr]s without introducing an unreasonable number of collisions in the hash table. Some benchmarks make us think that this implementation of hash-consing is linear in the size of the hash-consed data structure for our daily use of Rocq.*)
let array_eqeq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) in aux 0)
let invert_eqeq iv1 iv2 = match iv1, iv2 with | NoInvert, NoInvert -> true | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false | CaseInvert {indices=i1}, CaseInvert {indices=i2} -> i1 == i2
let hasheq_ctx (nas1, c1) (nas2, c2) = array_eqeq nas1 nas2 && c1 == c2
let hasheq_kind t1 t2 = match t1, t2 with | Rel n1, Rel n2 -> n1 == n2 | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 | Sort s1, Sort s2 -> s1 == s2 | Cast (c1,k1,t1), Cast (c2,k2,t2) -> c1 == c2 && k1 == k2 && t1 == t2 | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,r1,c1), Proj(p2,r2,c2) -> p1 == p2 && r1 == r2 && c1 == c2 | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && SList.equal (==) l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 | Case (ci1,u1,pms1,(p1,r1),iv1,c1,bl1), Case (ci2,u2,pms2,(p2,r2),iv2,c2,bl2) -> (** FIXME: use deeper equality for contexts *) u1 == u2 && array_eqeq pms1 pms2 && ci1 == ci2 && hasheq_ctx p1 p2 && r1 == r2 && invert_eqeq iv1 iv2 && c1 == c2 && Array.equal hasheq_ctx bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 && array_eqeq lna1 lna2 && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) -> Int.equal ln1 ln2 && array_eqeq lna1 lna2 && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 | Int i1, Int i2 -> i1 == i2 | Float f1, Float f2 -> Float64.equal f1 f2 | String s1, String s2 -> Pstring.equal s1 s2 | Array(u1,t1,def1,ty1), Array(u2,t2,def2,ty2) -> u1 == u2 && def1 == def2 && ty1 == ty2 && array_eqeq t1 t2 | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ | CoFix _ | Int _ | Float _ | String _ | Array _), _ -> false
let hasheq t1 t2 = hasheq_kind (kind t1) (kind t2)
(** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *)
module HashsetTerm = Hashset.Make(struct type t = constr let eq = hasheq end)
module HashsetTermArray = Hashset.Make(struct type t = constr array let eq = array_eqeq end)
let term_table = HashsetTerm.create 19991(* The associative table to hashcons terms. *)
let term_array_table = HashsetTermArray.create 4999(* The associative table to hashcons term arrays. *)
open Hashset.Combine
let hash_cast_kind = function| VMcast -> 0| NATIVEcast -> 1| DEFAULTcast -> 2
module CaseinfoHash =struct type t = case_info open Hashset.Combine let hash_pp_info info = let h1 = match info.style with | LetStyle -> 0 | IfStyle -> 1 | LetPatternStyle -> 2 | MatchStyle -> 3 in h1 let hash ~hind ci = let h1 = hind in let h2 = Int.hash ci.ci_npar in let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in let h5 = hash_pp_info ci.ci_pp_info in combine5 h1 h2 h3 h4 h5 let hashcons ci = let hind, ind = hcons_ind ci.ci_ind in hash ~hind ci, { ci with ci_ind = ind } let pp_info_equal info1 info2 = info1.style == info2.style let eq ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *) pp_info_equal ci.ci_pp_info ci'.ci_pp_info (* we use (=) on purpose *)end
module Hcaseinfo = Hashcons.Make(CaseinfoHash)
let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons ()
module Hannotinfo = struct type t = Name.t binder_annot let eq = eq_annot (fun na1 na2 -> na1 == na2) Sorts.relevance_equal let hashcons {binder_name=na;binder_relevance=r} = let hna, na = Name.hcons na in let h = Hashset.Combine.combinesmall (Sorts.relevance_hash r) hna in h, {binder_name=na;binder_relevance=r} endmodule Hannot = Hashcons.Make(Hannotinfo)
let hcons_annot = Hashcons.simple_hcons Hannot.generate Hannot.hcons ()
let dbg = CDebug.create ~name:"hcons" ()
module GenHCons(C:sig type t val kind : t -> (t, t, Sorts.t, Instance.t, Sorts.relevance) kind_of_term val self : t -> constr val refcount : t -> int
val via_hconstr : bool
module Tbl : sig val find_opt : t -> (int * constr) option val add : t -> int * constr -> unit end end) = structopen C
let steps = ref 0
let hashcons_array2 hcons a a' = assert (Array.length a = Array.length a'); CArray.Smart.fold_left_map_i (fun i h _ -> let hx, x = hcons (Array.unsafe_get a' i) in combine hx h, x) 0 a
let rec hash_term (t : t) : int * (constr,constr,_,_,_) kind_of_term = match kind t with | Var i -> let hi, i = Id.hcons i in (combinesmall 1 hi, Var i) | Sort s -> let hs, s = Sorts.hcons s in (combinesmall 2 hs, Sort s) | Cast (c, k, t) -> let hc, c = sh_rec c in let ht, t = sh_rec t in (combinesmall 3 (combine3 hc (hash_cast_kind k) ht), Cast (c, k, t)) | Prod (na,t,c) -> let hna, na = hcons_annot na and ht, t = sh_rec t and hc, c = sh_rec c in (combinesmall 4 (combine3 hna ht hc), Prod (na, t, c)) | Lambda (na,t,c) -> let hna, na = hcons_annot na and ht, t = sh_rec t and hc, c = sh_rec c in (combinesmall 5 (combine3 hna ht hc), Lambda (na, t, c)) | LetIn (na,b,t,c) -> let hna, na = hcons_annot na and hb, b = sh_rec b and ht, t = sh_rec t and hc, c = sh_rec c in (combinesmall 6 (combine4 hna hb ht hc), LetIn (na, b, t, c)) | App (c,l) -> let _, cl = destApp (self t) in let hc, c = sh_rec c in let hl, l = hash_term_array cl l in (combinesmall 7 (combine hl hc), App (c,l)) | Evar _ -> assert false | Const (c,u) -> let hc, c' = hcons_con c in let hu, u' = Instance.hcons u in (combinesmall 9 (combine hc hu), Const (c', u')) | Ind (ind,u) -> let hind, ind' = hcons_ind ind in let hu, u' = Instance.hcons u in (combinesmall 10 (combine hind hu), Ind (ind', u')) | Construct (c,u) -> let hc, c' = hcons_construct c in let hu, u' = Instance.hcons u in (combinesmall 11 (combine hc hu), Construct (c', u')) | Case (ci,u,pms,(p,r),iv,c,bl) -> (** FIXME: use a dedicated hashconsing structure *) let hcons_ctx (lna, c) = let hna, lna = hashcons_array2 hcons_annot lna lna in let hc, c = sh_rec c in combine hna hc, (lna, c) in (* XXX use hci? *) let _hci, ci = hcons_caseinfo ci in let hu, u = Instance.hcons u in let _,_,cpms,_,civ,_,cbl = destCase (self t) in let hpms,pms = hash_term_array cpms pms in let hp, p = hcons_ctx p in let hiv, iv = sh_invert civ iv in let hc, c = sh_rec c in let hbl, cbl = hashcons_array2 hcons_ctx cbl bl in let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in (combinesmall 12 hbl, Case (ci, u, pms, (p,r), iv, c, cbl)) | Fix (ln,(lna,tl,bl)) -> let _, (_,ctl,cbl) = destFix (self t) in let hbl,bl = hash_term_array cbl bl in let htl,tl = hash_term_array ctl tl in let hna, lna = Hashcons.hashcons_array hcons_annot lna in let h = combine3 hna hbl htl in (combinesmall 13 h, Fix (ln,(lna,tl,bl))) | CoFix(ln,(lna,tl,bl)) -> let _, (_,ctl,cbl) = destCoFix (self t) in let hbl,bl = hash_term_array cbl bl in let htl,tl = hash_term_array ctl tl in let hna, lna = Hashcons.hashcons_array hcons_annot lna in let h = combine3 hna hbl htl in (combinesmall 14 h, CoFix (ln,(lna,tl,bl))) | Meta n as t -> (combinesmall 15 n, t) | Rel n as t -> (combinesmall 16 n, t) | Proj (p,r,c) -> let hc, c' = sh_rec c in let hp, p' = Projection.hcons p in (combinesmall 17 (combine hp hc), Proj (p', r, c')) | Int i as t -> let (h,l) = Uint63.to_int2 i in (combinesmall 18 (combine h l), t) | Float f as t -> (combinesmall 19 (Float64.hash f), t) | String s as t -> (combinesmall 20 (Pstring.hash s), t) | Array (u,ar,def,ty) -> let _,car,_,_ = destArray (self t) in let hu, u = Instance.hcons u in let ht, t = hash_term_array car ar in let hdef, def = sh_rec def in let hty, ty = sh_rec ty in let h = combine4 hu ht hdef hty in (combinesmall 21 h, Array(u,t,def,ty))
and sh_invert civ iv = match civ, iv with | NoInvert, NoInvert -> 0, NoInvert | CaseInvert {indices=cindices}, CaseInvert {indices;} -> let ha, indices = hash_term_array cindices indices in combinesmall 1 ha, CaseInvert {indices;} | (NoInvert | CaseInvert _), _ -> assert false
and sh_rec_main t = let (h, y) = hash_term t in (h, HashsetTerm.repr h (T y) term_table)
and sh_rec t = incr steps; if refcount t = 1 then sh_rec_main t else match Tbl.find_opt t with | Some res -> res | None -> let res = sh_rec_main t in Tbl.add t res; res
(* Note : During hash-cons of arrays, we modify them *in place* *)
and hash_term_array ct t = let h, ct = hashcons_array2 sh_rec ct t in (h, HashsetTermArray.repr h ct term_array_table)
let hcons t = NewProfile.profile "Constr.hcons" (fun () -> sh_rec t) ()
let hcons t = steps := 0; let t = hcons t in dbg Pp.(fun () -> let open Hashset in let stats = HashsetTerm.stats term_table in v 0 ( str "via hconstr = " ++ bool via_hconstr ++ spc() ++ str "steps = " ++ int !steps ++ spc() ++ str "num_bindings = " ++ int stats.num_bindings ++ spc() ++ str "num_buckets = " ++ int stats.num_buckets ++ spc() ++ str "max_bucket_length = " ++ int stats.max_bucket_length ) ); t
end
module HCons = GenHCons(struct type t = constr let kind = kind let self x = x let refcount _ = 1
let via_hconstr = false
module Tbl = struct let find_opt _ = None let add _ _ : unit = assert false end end)
(* Make sure our statically allocated Rels (1 to 16) are considered as canonical, and hence hash-consed to themselves *)let () = ignore (HCons.hash_term_array rels rels)
let hcons = HCons.hcons
(* let hcons_types = hcons_constr *)
type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pttype named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pttype rel_context = rel_declaration listtype named_context = named_declaration list
(** Minimalistic constr printer, typically for debugging *)
let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) = let open Pp in let fixl = Array.mapi (fun i na -> (na.binder_name,t.(i),tl.(i),bl.(i))) lna in hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}")
let pr_puniverses p u = if UVars.Instance.is_empty u then p else Pp.(p ++ str"(*" ++ UVars.Instance.pr Sorts.raw_printer u ++ str"*)")
let rec debug_print c = let open Pp in match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" | Var id -> Id.print id | Sort s -> Sorts.debug_print s | Cast (c,_, t) -> hov 1 (str"(" ++ debug_print c ++ cut() ++ str":" ++ debug_print t ++ str")") | Prod ({binder_name=Name id;_},t,c) -> hov 1 (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++ spc() ++ debug_print c) | Prod ({binder_name=Anonymous;_},t,c) -> hov 0 (str"(" ++ debug_print t ++ str " ->" ++ spc() ++ debug_print c ++ str")") | Lambda (na,t,c) -> hov 1 (str"fun " ++ Name.print na.binder_name ++ str":" ++ debug_print t ++ str" =>" ++ spc() ++ debug_print c) | LetIn (na,b,t,c) -> hov 0 (str"let " ++ Name.print na.binder_name ++ str":=" ++ debug_print b ++ str":" ++ brk(1,2) ++ debug_print t ++ cut() ++ debug_print c) | App (c,l) -> hov 1 (str"(" ++ debug_print c ++ spc() ++ prlist_with_sep spc debug_print (Array.to_list l) ++ str")") | Evar (e,l) -> let pro = function None -> str "?" | Some c -> debug_print c in hov 1 (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ prlist_with_sep spc pro (SList.to_list l) ++str"}") | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")" | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" | Construct (((sp,i),j),u) -> str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" | Proj (p,_r,c) -> str"Proj(" ++ Projection.debug_print p ++ str"," ++ debug_print c ++ str")" | Case (_ci,_u,pms,(p,_),iv,c,bl) -> let pr_ctx (nas, c) = hov 2 (hov 0 (prvect (fun na -> Name.print na.binder_name ++ spc ()) nas ++ str "|-") ++ spc () ++ debug_print c) in v 0 (hv 0 (str"Case" ++ brk (1,1) ++ debug_print c ++ spc () ++ str "params" ++ brk (1,1) ++ prvect (fun x -> spc () ++ debug_print x) pms ++ spc () ++ str"return"++ brk (1,1) ++ pr_ctx p ++ debug_invert iv ++ spc () ++ str"with") ++ prvect (fun b -> spc () ++ pr_ctx b) bl ++ spc () ++ str"end") | Fix f -> debug_print_fix debug_print f | CoFix(i,(lna,tl,bl)) -> let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> Name.print na.binder_name ++ str":" ++ debug_print ty ++ cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" | Float i -> str"Float("++str (Float64.to_string i) ++ str")" | String s -> str"String("++str (Printf.sprintf "%S" (Pstring.to_string s)) ++ str")" | Array(u,t,def,ty) -> str"Array(" ++ prlist_with_sep pr_comma debug_print (Array.to_list t) ++ str" | " ++ debug_print def ++ str " : " ++ debug_print ty ++ str")@{" ++ UVars.Instance.pr Sorts.raw_printer u ++ str"}"
and debug_invert = let open Pp in function | NoInvert -> mt() | CaseInvert {indices;} -> spc() ++ str"Invert {indices=" ++ prlist_with_sep spc debug_print (Array.to_list indices) ++ str "} "