diff options
144 files changed, 2687 insertions, 508 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index c370a77ea0..ef606c9a75 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -101,11 +101,17 @@ let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. Try with to see test-suite/coqchk/include.v *) +let eq_nested_types ty1 ty2 = match ty1, ty2 with +| NestedInd ind1, NestedInd ind2 -> eq_ind_chk ind1 ind2 +| NestedInd _, _ -> false +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive _, _ -> false + let eq_recarg a1 a2 = match a1, a2 with | Norec, Norec -> true | Mrec i1, Mrec i2 -> eq_ind_chk i1 i2 - | Imbr i1, Imbr i2 -> eq_ind_chk i1 i2 - | (Norec | Mrec _ | Imbr _), _ -> false + | Nested ty1, Nested ty2 -> eq_nested_types ty1 ty2 + | (Norec | Mrec _ | Nested _), _ -> false let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) diff --git a/checker/values.ml b/checker/values.ml index 178a3d8624..38cb243f80 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -152,7 +152,8 @@ let rec v_constr = [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) [|v_uint63|]; (* Int *) - [|Float64|] (* Int *) + [|Float64|]; (* Float *) + [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *) |]) and v_prec = Tuple ("prec_declaration", @@ -235,7 +236,7 @@ let v_template_universes = v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = - v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *) let v_cst_def = v_sum "constant_def" 0 @@ -259,8 +260,11 @@ let v_cb = v_tuple "constant_body" v_bool; v_typing_flags|] +let v_nested = v_sum "nested" 0 + [|[|v_ind|] (* NestedInd *);[|v_cst|] (* NestedPrimitive *)|] + let v_recarg = v_sum "recarg" 1 (* Norec *) - [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] + [|[|v_ind|] (* Mrec *);[|v_nested|] (* Nested *)|] let rec v_wfp = Sum ("wf_paths",0, [|[|Int;Int|]; (* Rtree.Param *) @@ -317,7 +321,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" let v_prim_ind = v_enum "prim_ind" 6 (* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *) -let v_prim_type = v_enum "prim_type" 2 +let v_prim_type = v_enum "prim_type" 3 (* Number of constructors of prim_type in "kernel/cPrimitives.ml" *) let v_retro_action = diff --git a/dev/ci/user-overlays/11604-persistent-arrays.sh b/dev/ci/user-overlays/11604-persistent-arrays.sh new file mode 100644 index 0000000000..aec5c4fa3d --- /dev/null +++ b/dev/ci/user-overlays/11604-persistent-arrays.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "11604" ] || [ "$CI_BRANCH" = "persistent-arrays" ]; then + + unicoq_CI_REF=persistent-arrays + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + + elpi_CI_REF=persistent-arrays + elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi + + #relation_algebra_CI_REF=persistent-arrays + #relation_algebra_CI_GITURL=https://github.com/maximedenes/relation-algebra + + coqhammer_CI_REF=persistent-arrays + coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer + + metacoq_CI_REF=persistent-arrays + metacoq_CI_GITURL=https://github.com/maximedenes/metacoq + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3df6f986ce..ea90e83a83 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -50,13 +50,8 @@ let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) -let prrecarg = function - | Declarations.Norec -> str "Norec" - | Declarations.Mrec (mind,i) -> - str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" - | Declarations.Imbr (mind,i) -> - str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) +let prrecarg = Declareops.pp_recarg +let ppwf_paths x = pp (Declareops.pp_wf_paths x) let get_current_context () = try Vernacstate.Declare.get_current_context () @@ -316,6 +311,7 @@ let constr_display csr = "Int("^(Uint63.to_string i)^")" | Float f -> "Float("^(Float64.to_string f)^")" + | Array (u,t,def,ty) -> "Array("^(array_display t)^","^(term_display def)^","^(term_display ty)^")@{" ^universes_display u^"\n" and array_display v = "[|"^ @@ -450,6 +446,16 @@ let print_pure_constr csr = print_string ("Int("^(Uint63.to_string i)^")") | Float f -> print_string ("Float("^(Float64.to_string f)^")") + | Array (u,t,def,ty) -> + print_string "Array("; + Array.iter (fun x -> box_display x; print_space()) t; + print_string "|"; + box_display def; + print_string ":"; + box_display ty; + print_string ")@{"; + universes_display u; + print_string "}" and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 73cf1b0195..aa650fbdc8 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -17,6 +17,8 @@ let ppripos (ri,pos) = print_string ("getglob "^(Constant.to_string kn)^"\n") | Reloc_proj_name p -> print_string ("proj "^(Projection.Repr.to_string p)^"\n") + | Reloc_caml_prim op -> + print_string ("caml primitive "^CPrimitives.to_string op) ); print_flush () @@ -85,6 +87,7 @@ and ppwhd whd = | Vconstr_block b -> ppvblock b | Vint64 i -> printf "int64(%LiL)" i | Vfloat64 f -> printf "float64(%.17g)" f + | Varray t -> ppvarray t | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s @@ -100,6 +103,20 @@ and ppvblock b = print_string")"; close_box() +and ppvarray t = + let length = Parray.length_int t in + open_hbox(); + print_string "[|"; + for i = 0 to length - 2 do + ppvalues (Parray.get t (Uint63.of_int i)); + print_string "; " + done; + ppvalues (Parray.get t (Uint63.of_int (length - 1))); + print_string " | "; + ppvalues (Parray.default t); + print_string " |]"; + close_box() + and ppvalues v = open_hovbox 0;ppwhd (whd_val v);close_box(); print_flush() diff --git a/doc/changelog/01-kernel/11604-persistent-arrays.rst b/doc/changelog/01-kernel/11604-persistent-arrays.rst new file mode 100644 index 0000000000..fbade033d2 --- /dev/null +++ b/doc/changelog/01-kernel/11604-persistent-arrays.rst @@ -0,0 +1,6 @@ +- **Added:** + Built-in support for persistent arrays, which expose a functional + interface but are implemented using an imperative data structure, for + better performance. + (`#11604 <https://github.com/coq/coq/pull/11604>`_, + by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index e0eec2ae2d..323da93f3e 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -617,3 +617,38 @@ the Calculus of Inductive Constructions}}, year = 2019, institution = {Chalmers and Gothenburg University}, } + +@inproceedings{ConchonFilliatre07wml, + author = {Sylvain Conchon and Jean-Christophe Filliâtre}, + title = {A Persistent Union-Find Data Structure}, + booktitle = {ACM SIGPLAN Workshop on ML}, + publisher = {ACM Press}, + pages = {37--45}, + year = 2007, + address = {Freiburg, Germany}, + month = {October}, + topics = {team, lri}, + type_publi = {icolcomlec}, + type_digiteo = {conf_isbn}, + x-pdf = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, + url = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf}, + abstract = { The problem of disjoint sets, also known as union-find, + consists in maintaining a partition of a finite set within a data + structure. This structure provides two operations: a function find + returning the class of an element and a function union merging two + classes. An optimal and imperative solution is known since 1975. + However, the imperative nature of this data structure may be a + drawback when it is used in a backtracking algorithm. This paper + details the implementation of a persistent union-find data structure + as efficient as its imperative counterpart. To achieve this result, + our solution makes heavy use of imperative features and thus it is a + significant example of a data structure whose side effects are + safely hidden behind a persistent interface. To strengthen this + last claim, we also detail a formalization using the Coq proof + assistant which shows both the correctness of our solution and its + observational persistence. }, + x-equipes = {demons PROVAL}, + x-type = {article}, + x-support = {actes_aux}, + x-cle-support = {ML} +} diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index dc8f131209..727177b23a 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -40,9 +40,8 @@ These primitive declarations are regular axioms. As such, they must be trusted a Print Assumptions one_minus_one_is_zero. -The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement -dedicated, efficient, rules to reduce the applications of these primitive -operations. +The reduction machines implement dedicated, efficient rules to reduce the +applications of these primitive operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` @@ -105,3 +104,53 @@ Literal values (of type :g:`Float64.t`) are extracted to literal OCaml values (of type :g:`float`) written in hexadecimal notation and wrapped into the :g:`Float64.of_float` constructor, e.g.: :g:`Float64.of_float (0x1p+0)`. + +.. _primitive-arrays: + +Primitive Arrays +---------------- + +The language of terms features persistent arrays as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`PArray` module): + +.. coqdoc:: + + Primitive array := #array_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, elements in an array can be accessed and updated using the +:g:`PArray.get` and :g:`PArray.set` functions, declared and specified as +follows: + +.. coqdoc:: + + Primitive get := #array_get. + Primitive set := #array_set. + Notation "t .[ i ]" := (get t i). + Notation "t .[ i <- a ]" := (set t i a). + + Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. + Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. + +The complete set of such operators can be obtained looking at the :g:`PArray` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient rules to reduce the applications of these primitive +operations. + +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Parray` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq (see ``kernel/parray.ml``). + +Primitive arrays expose a functional interface, but they are internally +implemented using a persistent data structure :cite:`ConchonFilliatre07wml`. +Update and access to an element in the most recent copy of an array are +constant time operations. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 4badb20295..f39c50238a 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -15,6 +15,7 @@ theories/extraction/ExtrOcamlBigIntConv.v theories/extraction/ExtrOcamlChar.v theories/extraction/ExtrOCamlInt63.v theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOCamlPArray.v theories/extraction/ExtrOcamlIntConv.v theories/extraction/ExtrOcamlNatBigInt.v theories/extraction/ExtrOcamlNatInt.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ab615d5f65..7c1328916b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -709,4 +709,11 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq812.v theories/Compat/Coq813.v </dd> + + <dt> <b>Array</b>: + Persistent native arrays + </dt> + <dd> + theories/Array/PArray.v + </dd> </dl> diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 32eb63a818..334c23c963 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -77,6 +77,7 @@ let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2)) let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 let mkInt i = of_kind (Int i) let mkFloat f = of_kind (Float f) +let mkArray (u,t,def,ty) = of_kind (Array (u,t,def,ty)) let mkRef (gr,u) = let open GlobRef in match gr with | ConstRef c -> mkConstU (c,u) @@ -366,6 +367,7 @@ let iter_with_full_binders sigma g f n c = Array.iter (f n) tl; let n' = Array.fold_left2_i (fun i n na t -> g (LocalAssum (na,lift i t)) n) n lna tl in Array.iter (f n') bl + | Array (_u,t,def,ty) -> Array.Fun1.iter f n t; f n def; f n ty let iter_with_binders sigma g f n c = let f l c = f l (of_constr c) in @@ -546,18 +548,21 @@ let universes_of_constr sigma c = let rec aux s c = match kind sigma c with | Const (c, u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s | Sort u -> - let sort = ESorts.kind sigma u in - if Sorts.is_small sort then s - else - let u = Sorts.univ_of_sort sort in - LSet.fold LSet.add (Universe.levels u) s + let sort = ESorts.kind sigma u in + if Sorts.is_small sort then s + else + let u = Sorts.univ_of_sort sort in + LSet.fold LSet.add (Universe.levels u) s | Evar (k, args) -> - let concl = Evd.evar_concl (Evd.find sigma k) in - fold sigma aux (aux s concl) c + let concl = Evd.evar_concl (Evd.find sigma k) in + fold sigma aux (aux s concl) c + | Array (u,_,_,_) -> + let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in + fold sigma aux s c | _ -> fold sigma aux s c in aux LSet.empty c @@ -762,7 +767,7 @@ let kind_of_type sigma t = match kind sigma t with | (Rel _ | Meta _ | Var _ | Evar _ | Const _ | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) -> AtomicType (t,[||]) - | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" + | (Lambda _ | Construct _ | Int _ | Float _ | Array _) -> failwith "Not a type" module Unsafe = struct diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 2bf8f69af7..d0f675319d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -135,6 +135,7 @@ val mkArrow : t -> Sorts.relevance -> t -> t val mkArrowR : t -> t -> t val mkInt : Uint63.t -> t val mkFloat : Float64.t -> t +val mkArray : EInstance.t * t array * t * t -> t val mkRef : GlobRef.t * EInstance.t -> t diff --git a/engine/namegen.ml b/engine/namegen.ml index 1cf5be10ae..fb9f6db0ea 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i).binder_name with Name id -> id | _ -> assert false) - | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None + | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ | Array _ -> None in hdrec c @@ -166,6 +166,7 @@ let hdchar env sigma c = | Meta _ | Case _ -> "y" | Int _ -> "i" | Float _ -> "f" + | Array _ -> "a" in hdrec 0 c diff --git a/engine/termops.ml b/engine/termops.ml index f6d0807823..e5231ef9cd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -659,6 +659,12 @@ let map_constr_with_binders_left_to_right sigma g f l c = if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then c else mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.map_left (f l) t in + let def' = f l def in + let ty' = f l ty in + if def' == def && t' == t && ty' == ty then c + else mkArray(u,t',def',ty') let map_under_context_with_full_binders sigma g f l n d = let open EConstr in @@ -738,6 +744,11 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.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 cstr else mkArray (u,t', def',ty') let map_constr_with_full_binders sigma g f = map_constr_with_full_binders_gen false sigma g f diff --git a/engine/univSubst.ml b/engine/univSubst.ml index f06aeaf54e..335c2e5e68 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -151,6 +151,13 @@ let nf_evars_and_universes_opt_subst f subst = let univs' = Instance.subst_fn lsubst univs in if univs' == univs then Constr.map aux c else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br)) + | Array (u,elems,def,ty) -> + let u' = Univ.Instance.subst_fn lsubst u in + let elems' = CArray.Smart.map aux elems in + let def' = aux def in + let ty' = aux ty in + if u == u' && elems == elems' && def == def' && ty == ty' then c + else mkArray (u',elems',def',ty') | _ -> Constr.map aux c in aux diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 9c4b78f4ed..c98e05370e 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -115,6 +115,7 @@ and constr_expr_r = | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr + | CArray of instance_expr option * constr_expr array * constr_expr * constr_expr and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3d99e1d227..ce8e7d3c2c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -174,10 +174,14 @@ let rec constr_expr_eq e1 e2 = | CDelimiters(s1,e1), CDelimiters(s2,e2) -> String.equal s1 s2 && constr_expr_eq e1 e2 + | CArray(u1,t1,def1,ty1), CArray(u2,t2,def2,ty2) -> + Array.equal constr_expr_eq t1 t2 && + constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 && + eq_universes u1 u2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _ ), _ -> false + | CGeneralization _ | CDelimiters _ | CArray _), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_ast explicitation_eq) e1 e2 && @@ -353,6 +357,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + | CArray (_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty ) let free_vars_of_constr_expr c = @@ -439,6 +444,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) + | CArray (u, t, def, ty) -> + CArray (u, Array.map (f e) t, f e def, f e ty) ) (* Used in constrintern *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b087431e85..95df626d4c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1095,6 +1095,9 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) + | GArray(u,t,def,ty) -> + CArray(u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + in insert_entry_coercion coercion (CAst.make ?loc c) and extern_typ ?impargs (subentry,(_,scopes)) = @@ -1469,6 +1472,9 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i | PFloat f -> GFloat f + | PArray(t,def,ty) -> + let glob_of = glob_of_pat avoid env sigma in + GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d95554de56..987aa63392 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -772,7 +772,7 @@ let rec adjust_env env = function | NCast (c,_) -> adjust_env env c | NApp _ -> restart_no_binders env | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NInt _ | NFloat _ + | NRec _ | NSort _ | NInt _ | NFloat _ | NArray _ | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = @@ -2204,6 +2204,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) + | CArray(u,t,def,ty) -> + DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) diff --git a/interp/impargs.ml b/interp/impargs.ml index c6405b40fc..db102470b0 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -236,7 +236,7 @@ let rec is_rigid_head sigma t = match kind sigma t with | Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i))) | _ -> is_rigid_head sigma f) | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ - | Prod _ | Meta _ | Cast _ | Int _ | Float _ -> assert false + | Prod _ | Meta _ | Cast _ | Int _ | Float _ | Array _ -> assert false let is_rigid env sigma t = let open Context.Rel.Declaration in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 54065e8b35..6422e184b5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -92,9 +92,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Uint63.equal i1 i2 | NFloat f1, NFloat f2 -> Float64.equal f1 f2 +| NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> + Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2 + && eq_notation_constr vars ty1 ty2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false + | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -249,6 +252,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat | NRef x -> GRef (x,None) | NInt i -> GInt i | NFloat f -> GFloat f + | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -472,6 +476,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = if arg != None then has_ltac := true; NHole (w, naming, arg) | GRef (r,_) -> NRef r + | GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -675,6 +680,14 @@ let rec subst_notation_constr subst bound raw = let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') + | NArray (t,def,ty) -> + let def' = subst_notation_constr subst bound def + and t' = Array.Smart.map (subst_notation_constr subst bound) t + and ty' = subst_notation_constr subst bound ty + in + if def' == def && t' == t && ty' == ty then raw else + NArray(t',def',ty') + let subst_interpretation subst (metas,pat) = let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) @@ -1254,9 +1267,16 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2 + | GArray(_u,t,def,ty), NArray(nt,ndef,nty) -> + if Int.equal (Array.length t) (Array.length nt) then + let sigma = match_in u alp metas sigma def ndef in + let sigma = match_in u alp metas sigma ty nty in + Array.fold_left2 (match_in u alp metas) sigma t nt + else raise No_match + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _ | GInt _ | GFloat _), _ -> raise No_match + | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match and match_in u = match_ true u diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 4e9b8bbb17..82238b71b7 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -45,6 +45,7 @@ type notation_constr = | NCast of notation_constr * notation_constr cast_type | NInt of Uint63.t | NFloat of Float64.t + | NArray of notation_constr array * notation_constr * notation_constr (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 306643f758..814cdfe1d8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -75,6 +75,8 @@ void init_arity () { arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= + arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]= + arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]= arity[PROJ]=2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 7588c1ce07..9921208e04 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -22,6 +22,7 @@ #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> +#include <caml/callback.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -111,7 +112,8 @@ if (sp - num_args < coq_stack_threshold) { \ /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } - +#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } +#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } /* Register optimization. Some compilers underestimate the use of the local variables representing @@ -1771,6 +1773,71 @@ value coq_interprete Next; } + + Instruct(ISINT_CAML_CALL2) { + value arg; + print_instr("ISINT_CAML_CALL2"); + if (Is_uint63(accu)) { + pc++; + print_int(*pc); + arg = sp[0]; + Setup_for_caml_call; + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; + } + + Instruct(ISARRAY_CAML_CALL1) { + print_instr("ISARRAY_CAML_CALL1"); + if (Is_coq_array(accu)) { + pc++; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback(Field(coq_global_data, *pc),accu); + Restore_after_caml_call; + pc++; + } + else pc += *pc; + Next; + } + + Instruct(ISARRAY_INT_CAML_CALL2) { + value arg; + print_instr("ISARRAY_INT_CAML_CALL2"); + if (Is_coq_array(accu) && Is_uint63(sp[0])) { + pc++; + arg = sp[0]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; + } + + Instruct(ISARRAY_INT_CAML_CALL3) { + value arg1; + value arg2; + print_instr("ISARRAY_INT_CAML_CALL3"); + if (Is_coq_array(accu) && Is_uint63(sp[0])) { + pc++; + arg1 = sp[0]; + arg2 = sp[1]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2); + Restore_after_caml_call; + sp += 2; + pc++; + } else pc += *pc; + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index b027673ac7..86ae6295fd 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -33,6 +33,9 @@ #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #define Is_double(v) (Tag_val(v) == Double_tag) +/* coq array */ +#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) + /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 9640efd8eb..a23ef8fdca 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -350,6 +350,7 @@ and fterm = | FEvar of existential * fconstr subs | FInt of Uint63.t | FFloat of Float64.t + | FArray of Univ.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED @@ -456,7 +457,7 @@ let rec lft_fconstr n ft = | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FCaseInvert _ | FProd _ - | FLetIn _ | FEvar _ | FCLOS _ -> {mark=ft.mark; term=FLIFT(n,ft)} + | FLetIn _ | FEvar _ | FCLOS _ | FArray _ -> {mark=ft.mark; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -518,11 +519,13 @@ let mk_clos e t = | Construct kn -> {mark = mark Cstr Unknown; term = FConstruct kn } | Int i -> {mark = mark Cstr Unknown; term = FInt i} | Float f -> {mark = mark Cstr Unknown; term = FFloat f} - | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _|Array _) -> {mark = mark Red Unknown; term = FCLOS(t,e)} let inject c = mk_clos (subs_id 0) c +(************************************************************************) + (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) let mk_clos_vect env v = match v with @@ -558,7 +561,7 @@ let ref_value_cache ({ i_cache = cache; _ }) tab ref = in Def (inject body) with - | NotEvaluableConst (IsPrimitive op) (* Const *) -> Primitive op + | NotEvaluableConst (IsPrimitive (_u,op)) (* Const *) -> Primitive op | Not_found (* List.assoc *) | NotEvaluableConst _ (* Const *) -> Undef None @@ -626,7 +629,7 @@ let rec to_constr lfts v = subst_constr subs f) | FEvar ((ev,args),env) -> let subs = comp_subs lfts env in - mkEvar(ev,List.map (fun a -> subst_constr subs a) args) + mkEvar(ev, List.map (fun a -> subst_constr subs a) args) | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FInt i -> @@ -634,6 +637,11 @@ let rec to_constr lfts v = | FFloat f -> Constr.mkFloat f + | FArray (u,t,ty) -> + let ty = to_constr lfts ty in + let init i = to_constr lfts (Parray.get t (Uint63.of_int i)) in + mkArray(u,Array.init (Parray.length_int t) init, to_constr lfts (Parray.default t),ty) + | FCLOS (t,env) -> if is_subs_id env && is_lift_id lfts then t else @@ -931,57 +939,6 @@ let unfold_projection info p = Some (Zproj (Projection.repr p)) else None -(*********************************************************************) -(* A machine that inspects the head of a term until it finds an - atom or a subterm that may produce a redex (abstraction, - constructor, cofix, letin, constant), or a neutral term (product, - inductive) *) -let rec knh info m stk = - match m.term with - | FLIFT(k,a) -> knh info a (zshift k stk) - | FCLOS(t,e) -> knht info e t (zupdate info m stk) - | FLOCKED -> assert false - | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) - | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) - | FFix(((ri,n),_),_) -> - (match get_nth_arg m ri.(n) stk with - (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') - | (None, stk') -> (m,stk')) - | FProj (p,c) -> - (match unfold_projection info p with - | None -> (m, stk) - | Some s -> knh info c (s :: zupdate info m stk)) - -(* cases where knh stops *) - | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _| - FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _) -> - (m, stk) - -(* The same for pure terms *) -and knht info e t stk = - match kind t with - | App(a,b) -> - knht info e a (append_stack (mk_clos_vect e b) stk) - | Case(ci,p,NoInvert,t,br) -> - knht info e t (ZcaseT(ci, p, br, e)::stk) - | Case(ci,p,CaseInvert{univs;args},t,br) -> - let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in - { mark = mark Red Unknown; term }, stk - | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk - | Cast(a,_,_) -> knht info e a stk - | Rel n -> knh info (clos_rel e n) stk - | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk - | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk) - | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk - | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk - | Prod (n, t, c) -> - { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk - | LetIn (n,b,t,c) -> - { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk - | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk - -let inject c = mk_clos (subs_id 0) c - (************************************************************************) (* Reduction of Native operators *) @@ -992,6 +949,7 @@ module FNativeEntries = type elem = fconstr type args = fconstr array type evd = unit + type uinstance = Univ.Instance.t let get = Array.get @@ -1005,6 +963,11 @@ module FNativeEntries = | FFloat f -> f | _ -> raise Primred.NativeDestKO + let get_parray () e = + match [@ocaml.warning "-4"] e.term with + | FArray (_u,t,_ty) -> t + | _ -> raise Not_found + let dummy = {mark = mark Norm KnownR; term = FRel 0} let current_retro = ref Retroknowledge.empty @@ -1133,6 +1096,17 @@ module FNativeEntries = frefl := { mark = mark Cstr KnownR; term = FConstruct (Univ.in_punivs crefl) } | None -> defined_refl := false + let defined_array = ref false + + let farray = ref dummy + + let init_array retro = + match retro.Retroknowledge.retro_array with + | Some c -> + defined_array := true; + farray := { mark = mark Norm KnownR; term = FFlex (ConstKey (Univ.in_punivs c)) } + | None -> defined_array := false + let init env = current_retro := env.retroknowledge; init_int !current_retro; @@ -1143,7 +1117,8 @@ module FNativeEntries = init_cmp !current_retro; init_f_cmp !current_retro; init_f_class !current_retro; - init_refl !current_retro + init_refl !current_retro; + init_array !current_retro let check_env env = if not (!current_retro == env.retroknowledge) then init env @@ -1180,6 +1155,10 @@ module FNativeEntries = check_env env; assert (!defined_f_class) + let check_array env = + check_env env; + assert (!defined_array) + let mkInt env i = check_int env; { mark = mark Cstr KnownR; term = FInt i } @@ -1269,10 +1248,70 @@ module FNativeEntries = let mkNaN env = check_f_class env; !fNaN + + let mkArray env u t ty = + check_array env; + { mark = mark Whnf KnownR; term = FArray (u,t,ty)} + end module FredNative = RedNative(FNativeEntries) +(*********************************************************************) +(* A machine that inspects the head of a term until it finds an + atom or a subterm that may produce a redex (abstraction, + constructor, cofix, letin, constant), or a neutral term (product, + inductive) *) +let rec knh info m stk = + match m.term with + | FLIFT(k,a) -> knh info a (zshift k stk) + | FCLOS(t,e) -> knht info e t (zupdate info m stk) + | FLOCKED -> assert false + | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) + | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) + | FFix(((ri,n),_),_) -> + (match get_nth_arg m ri.(n) stk with + (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') + | (None, stk') -> (m,stk')) + | FProj (p,c) -> + (match unfold_projection info p with + | None -> (m, stk) + | Some s -> knh info c (s :: zupdate info m stk)) + +(* cases where knh stops *) + | (FFlex _|FLetIn _|FConstruct _|FEvar _|FCaseInvert _| + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _|FInt _|FFloat _|FArray _) -> + (m, stk) + +(* The same for pure terms *) +and knht info e t stk = + match kind t with + | App(a,b) -> + knht info e a (append_stack (mk_clos_vect e b) stk) + | Case(ci,p,NoInvert,t,br) -> + knht info e t (ZcaseT(ci, p, br, e)::stk) + | Case(ci,p,CaseInvert{univs;args},t,br) -> + let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in + { mark = mark Red Unknown; term }, stk + | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk + | Cast(a,_,_) -> knht info e a stk + | Rel n -> knh info (clos_rel e n) stk + | Proj (p, c) -> knh info { mark = mark Red Unknown; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _ | Int _|Float _) -> (mk_clos e t, stk) + | CoFix cfx -> { mark = mark Cstr Unknown; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { mark = mark Cstr Unknown; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { mark = mark Whnf KnownR; term = FProd (n, mk_clos e t, c, e) }, stk + | LetIn (n,b,t,c) -> + { mark = mark Red Unknown; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { mark = mark Red Unknown; term = FEvar (ev, e) }, stk + | Array(u,t,def,ty) -> + let len = Array.length t in + let ty = mk_clos e ty in + let t = Parray.init (Uint63.of_int len) (fun i -> mk_clos e t.(i)) (mk_clos e def) in + let term = FArray (u,t,ty) in + knh info { mark = mark Cstr Unknown; term } stk + (************************************************************************) let conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) ref @@ -1286,7 +1325,7 @@ let rec knr info tab m stk = (match get_args n tys f e stk with Inl e', s -> knit info tab e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) -> + | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with | Def v -> kni info tab v stk | Primitive op when check_native_args op stk -> @@ -1335,15 +1374,16 @@ let rec knr info tab m stk = (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FInt _ | FFloat _ -> + | FInt _ | FFloat _ | FArray _ -> (match [@ocaml.warning "-4"] strip_update_shift_app m stk with - | (_, _, Zprimitive(op,c,rargs,nargs)::s) -> + | (_, _, Zprimitive(op,(_,u as c),rargs,nargs)::s) -> let (rargs, nargs) = skip_native_args (m::rargs) nargs in begin match nargs with | [] -> let args = Array.of_list (List.rev rargs) in - begin match FredNative.red_prim (info_env info) () op args with - | Some m -> kni info tab m s + begin match FredNative.red_prim (info_env info) () op u args with + | Some m -> + kni info tab m s | None -> let f = {mark = mark Whnf KnownR; term = FFlex (ConstKey c)} in let m = {mark = mark Whnf KnownR; term = FApp(f,args)} in @@ -1471,7 +1511,8 @@ and norm_head info tab m = | FProj (p,c) -> mkProj (p, kl info tab c) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ - | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ | FFloat _ -> term_of_fconstr m + | FApp _ | FCaseT _ | FCaseInvert _ | FLIFT _ | FCLOS _ | FInt _ + | FFloat _ | FArray _ -> term_of_fconstr m (* Initialization and then normalization *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c1e5f12df7..ada0fc9780 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -118,6 +118,7 @@ type fterm = | FEvar of existential * fconstr subs | FInt of Uint63.t | FFloat of Float64.t + | FArray of Univ.Instance.t * fconstr Parray.t * fconstr | FLIFT of int * fconstr | FCLOS of constr * fconstr subs | FLOCKED diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index c4036e9677..314cb54d1d 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Univ + type t = | Int63head0 | Int63tail0 @@ -51,6 +53,13 @@ type t = | Float64ldshiftexp | Float64next_up | Float64next_down + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength let parse = function | "int63_head0" -> Int63head0 @@ -95,6 +104,13 @@ let parse = function | "float64_ldshiftexp" -> Float64ldshiftexp | "float64_next_up" -> Float64next_up | "float64_next_down" -> Float64next_down + | "array_make" -> Arraymake + | "array_get" -> Arrayget + | "array_default" -> Arraydefault + | "array_set" -> Arrayset + | "array_length" -> Arraylength + | "array_copy" -> Arraycopy + | "array_reroot" -> Arrayreroot | _ -> raise Not_found let equal (p1 : t) (p2 : t) = @@ -143,6 +159,13 @@ let hash = function | Float64eq -> 40 | Float64lt -> 41 | Float64le -> 42 + | Arraymake -> 43 + | Arrayget -> 44 + | Arraydefault -> 45 + | Arrayset -> 46 + | Arraycopy -> 47 + | Arrayreroot -> 48 + | Arraylength -> 49 (* Should match names in nativevalues.ml *) let to_string = function @@ -188,28 +211,66 @@ let to_string = function | Float64ldshiftexp -> "ldshiftexp" | Float64next_up -> "next_up" | Float64next_down -> "next_down" + | Arraymake -> "arraymake" + | Arrayget -> "arrayget" + | Arraydefault -> "arraydefault" + | Arrayset -> "arrayset" + | Arraycopy -> "arraycopy" + | Arrayreroot -> "arrayreroot" + | Arraylength -> "arraylength" + +type const = + | Arraymaxlength -type prim_type = - | PT_int63 - | PT_float64 +let const_to_string = function + | Arraymaxlength -> "arraymaxlength" + +let const_of_string = function + | "array_max_length" -> Arraymaxlength + | _ -> raise Not_found -type 'a prim_ind = +let const_univs = function + | Arraymaxlength -> AUContext.empty + +type 'a prim_type = + | PT_int63 : unit prim_type + | PT_float64 : unit prim_type + | PT_array : (Instance.t * ind_or_type) prim_type + +and 'a prim_ind = | PIT_bool : unit prim_ind - | PIT_carry : prim_type prim_ind - | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_carry : ind_or_type prim_ind + | PIT_pair : (ind_or_type * ind_or_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind | PIT_f_class : unit prim_ind -type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex - -type ind_or_type = +and ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type - | PITT_type : prim_type -> ind_or_type + | PITT_type : 'a prim_type * 'a -> ind_or_type + | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *) + +let one_univ = + AUContext.make Names.[|Name (Id.of_string "u")|] Constraint.empty + +let typ_univs (type a) (t : a prim_type) = match t with + | PT_int63 -> AUContext.empty + | PT_float64 -> AUContext.empty + | PT_array -> one_univ + +type prim_type_ex = PTE : 'a prim_type -> prim_type_ex + +type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex let types = - let int_ty = PITT_type PT_int63 in - let float_ty = PITT_type PT_float64 in + let int_ty = PITT_type (PT_int63, ()) in + let float_ty = PITT_type (PT_float64, ()) in + let array_ty = + PITT_type + (PT_array, + (Instance.of_array [|Level.var 0|], + PITT_param 1)) + in function | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul @@ -217,25 +278,144 @@ let types = | Int63lsr | Int63lsl | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> - [int_ty; int_ty; PITT_ind (PIT_carry, PT_int63)] + [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] | Int63mulc | Int63diveucl -> - [int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] | Int63div21 -> - [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (PT_int63, PT_int63))] + [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] | Float64opp | Float64abs | Float64sqrt | Float64next_up | Float64next_down -> [float_ty; float_ty] | Float64ofInt63 -> [int_ty; float_ty] | Float64normfr_mantissa -> [float_ty; int_ty] - | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (PT_float64, PT_int63))] + | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))] | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())] | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())] | Float64add | Float64sub | Float64mul | Float64div -> [float_ty; float_ty; float_ty] | Float64ldshiftexp -> [float_ty; int_ty; float_ty] + | Arraymake -> [int_ty; PITT_param 1; array_ty] + | Arrayget -> [array_ty; int_ty; PITT_param 1] + | Arraydefault -> [array_ty; PITT_param 1] + | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] + | Arraycopy -> [array_ty; array_ty] + | Arrayreroot -> [array_ty; array_ty] + | Arraylength -> [array_ty; int_ty] + +let one_param = + (* currently if there's a parameter it's always this *) + let a_annot = Context.nameR (Names.Id.of_string "A") in + let ty = Constr.mkType (Universe.make (Level.var 0)) in + Context.Rel.Declaration.[LocalAssum (a_annot, ty)] + +let params = function + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down -> [] + + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> one_param + +let nparams x = List.length (params x) + +let univs = function + | Int63head0 + | Int63tail0 + | Int63add + | Int63sub + | Int63mul + | Int63div + | Int63mod + | Int63lsr + | Int63lsl + | Int63land + | Int63lor + | Int63lxor + | Int63addc + | Int63subc + | Int63addCarryC + | Int63subCarryC + | Int63mulc + | Int63diveucl + | Int63div21 + | Int63addMulDiv + | Int63eq + | Int63lt + | Int63le + | Int63compare + | Float64opp + | Float64abs + | Float64eq + | Float64lt + | Float64le + | Float64compare + | Float64classify + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp + | Float64next_up + | Float64next_down -> AUContext.empty + + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> one_univ type arg_kind = | Kparam (* not needed for the evaluation of the primitive when it reduces *) @@ -247,17 +427,21 @@ type args_red = arg_kind list (* Invariant only argument of type int63, float or an inductive can have kind Kwhnf *) -let arity t = List.length (types t) - 1 +let arity t = let sign = types t in nparams t + List.length sign - 1 let kind t = - let rec aux n = if n <= 0 then [] else Kwhnf :: aux (n - 1) in - aux (arity t) + let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in + let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in + params (nparams t) @ List.map args (CList.drop_last (types t)) + +let types t = params t, types t (** Special Entries for Register **) type op_or_type = | OT_op of t - | OT_type of prim_type + | OT_type : 'a prim_type -> op_or_type + | OT_const of const let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_bool -> "bool" @@ -267,24 +451,40 @@ let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_f_cmp -> "f_cmp" | PIT_f_class -> "f_class" -let prim_type_to_string = function +let prim_type_to_string (type a) (ty : a prim_type) = match ty with | PT_int63 -> "int63_type" | PT_float64 -> "float64_type" + | PT_array -> "array_type" let op_or_type_to_string = function | OT_op op -> to_string op | OT_type t -> prim_type_to_string t + | OT_const c -> const_to_string c let prim_type_of_string = function - | "int63_type" -> PT_int63 - | "float64_type" -> PT_float64 + | "int63_type" -> PTE PT_int63 + | "float64_type" -> PTE PT_float64 + | "array_type" -> PTE PT_array | _ -> raise Not_found let op_or_type_of_string s = - try OT_type (prim_type_of_string s) - with Not_found -> OT_op (parse s) + match prim_type_of_string s with + | PTE ty -> OT_type ty + | exception Not_found -> + begin try OT_op (parse s) + with Not_found -> OT_const (const_of_string s) + end let parse_op_or_type ?loc s = try op_or_type_of_string s with Not_found -> CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist.")) + +let op_or_type_univs = function + | OT_op t -> univs t + | OT_type t -> typ_univs t + | OT_const c -> const_univs c + +let body_of_prim_const = function + | Arraymaxlength -> + Constr.mkInt (Parray.max_length) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index a5db51111f..5e5fad9f04 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -51,6 +51,13 @@ type t = | Float64ldshiftexp | Float64next_up | Float64next_down + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength (** Can raise [Not_found]. Beware that this is not exactly the reverse of [to_string] below. *) @@ -58,8 +65,11 @@ val parse : string -> t val equal : t -> t -> bool +type const = + | Arraymaxlength + type arg_kind = - | Kparam (* not needed for the elavuation of the primitive*) + | Kparam (* not needed for the evaluation of the primitive*) | Kwhnf (* need to be reduced in whnf before reducing the primitive *) | Karg (* no need to be reduced in whnf *) @@ -70,32 +80,49 @@ val hash : t -> int val to_string : t -> string val arity : t -> int +(** Including parameters *) + +val nparams : t -> int val kind : t -> args_red +(** Includes parameters *) (** Special Entries for Register **) -type prim_type = - | PT_int63 - | PT_float64 - -(** Can raise [Not_found] *) -val prim_type_of_string : string -> prim_type -val prim_type_to_string : prim_type -> string +type 'a prim_type = + | PT_int63 : unit prim_type + | PT_float64 : unit prim_type + | PT_array : (Univ.Instance.t * ind_or_type) prim_type -type 'a prim_ind = +and 'a prim_ind = | PIT_bool : unit prim_ind - | PIT_carry : prim_type prim_ind - | PIT_pair : (prim_type * prim_type) prim_ind + | PIT_carry : ind_or_type prim_ind + | PIT_pair : (ind_or_type * ind_or_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind | PIT_f_class : unit prim_ind +and ind_or_type = + | PITT_ind : 'a prim_ind * 'a -> ind_or_type + | PITT_type : 'a prim_type * 'a -> ind_or_type + | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *) + +val typ_univs : 'a prim_type -> Univ.AUContext.t + +type prim_type_ex = PTE : 'a prim_type -> prim_type_ex + type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex +(** Can raise [Not_found] *) +val prim_type_of_string : string -> prim_type_ex +val prim_type_to_string : 'a prim_type -> string + type op_or_type = | OT_op of t - | OT_type of prim_type + | OT_type : 'a prim_type -> op_or_type + | OT_const of const + +val op_or_type_univs : op_or_type -> Univ.AUContext.t val prim_ind_to_string : 'a prim_ind -> string @@ -105,8 +132,12 @@ val op_or_type_to_string : op_or_type -> string val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type -type ind_or_type = - | PITT_ind : 'a prim_ind * 'a -> ind_or_type - | PITT_type : prim_type -> ind_or_type +val univs : t -> Univ.AUContext.t + +val types : t -> Constr.rel_context * ind_or_type list +(** Parameters * Reduction relevant arguments and output type + + XXX we could reify universes in ind_or_type (currently polymorphic types + like array are assumed to use universe 0). *) -val types : t -> ind_or_type list +val body_of_prim_const : const -> Constr.t diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 25ec250367..74405a0105 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -61,6 +61,7 @@ type instruction = | Kensurestackcapacity of int | Kbranch of Label.t (* jump to label *) | Kprim of CPrimitives.t * pconstant option + | Kcamlprim of CPrimitives.t * Label.t | Kareint of int and bytecodes = instruction list @@ -147,6 +148,10 @@ let rec pp_instr i = | Kprim (op, id) -> str (CPrimitives.to_string op) ++ str " " ++ (match id with Some (id,_u) -> Constant.print id | None -> str "") + | Kcamlprim (op, lbl) -> + str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ + pp_lbl lbl + | Kareint n -> str "areint " ++ int n and pp_bytecodes c = diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f1d441ca76..b703058fb7 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -60,7 +60,7 @@ type instruction = | Kbranch of Label.t (** jump to label, is it needed ? *) | Kprim of CPrimitives.t * pconstant option - + | Kcamlprim of CPrimitives.t * Label.t | Kareint of int and bytecodes = instruction list diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 59ae8c0745..7bff377238 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -516,6 +516,18 @@ let rec get_alias env kn = | BCalias kn' -> get_alias env kn' | _ -> kn) +(* Some primitives are not implemented natively by the VM, but calling OCaml + code instead *) +let is_caml_prim = let open CPrimitives in function + | Arraymake + | Arrayget + | Arraydefault + | Arrayset + | Arraycopy + | Arrayreroot + | Arraylength -> true + | _ -> false + (* sz is the size of the local stack *) let rec compile_lam env cenv lam sz cont = set_max_stack_size sz; @@ -775,6 +787,27 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont + | Lprim (Some (kn,u), op, args) when is_caml_prim op -> + let arity = CPrimitives.arity op in + let nparams = CPrimitives.nparams op in + let nargs = arity - nparams in + assert (arity = Array.length args && arity <= 4); + let (jump, cont) = make_branch cont in + let lbl_default = Label.create () in + let default = + let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = + if Univ.Instance.is_empty u then cont + else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) + in + Klabel lbl_default :: + Kpush :: + if Int.equal nparams 0 then cont + else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) + in + fun_code := [Ksequence(default, !fun_code)]; + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + | Lprim (kn, op, args) -> comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d855dbf2bb..6b4daabf0c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -30,6 +30,7 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t | Reloc_proj_name of Projection.Repr.t + | Reloc_caml_prim of CPrimitives.t let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 @@ -40,6 +41,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with | Reloc_getglobal _, _ -> false | Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2 | Reloc_proj_name _, _ -> false +| Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2 +| Reloc_caml_prim _, _ -> false let hash_reloc_info r = let open Hashset.Combine in @@ -48,6 +51,7 @@ let hash_reloc_info r = | Reloc_const c -> combinesmall 2 (hash_structured_constant c) | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p) + | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p) module RelocTable = Hashtbl.Make(struct type t = reloc_info @@ -199,6 +203,10 @@ let slot_for_proj_name env p = enter env (Reloc_proj_name p); out_int env 0 +let slot_for_caml_prim env op = + enter env (Reloc_caml_prim op); + out_int env 0 + (* Emission of one instruction *) let nocheck_prim_op = function @@ -252,6 +260,11 @@ let check_prim_op = function | Float64ldshiftexp -> opCHECKLDSHIFTEXP | Float64next_up -> opCHECKNEXTUPFLOAT | Float64next_down -> opCHECKNEXTDOWNFLOAT + | Arraymake -> opISINT_CAML_CALL2 + | Arrayget -> opISARRAY_INT_CAML_CALL2 + | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> + opISARRAY_CAML_CALL1 let emit_instr env = function | Klabel lbl -> define_label env lbl @@ -349,6 +362,11 @@ let emit_instr env = function out env (check_prim_op op); slot_for_getglobal env q + | Kcamlprim (op,lbl) -> + out env (check_prim_op op); + out_label env lbl; + slot_for_caml_prim env op + | Kareint 1 -> out env opISINT | Kareint 2 -> out env opAREINT2; @@ -415,6 +433,7 @@ let subst_reloc s ri = | Reloc_const sc -> Reloc_const (subst_strcst s sc) | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p) + | Reloc_caml_prim _ -> ri let subst_patches subst p = let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 209d741ba8..c4262f3380 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -16,6 +16,7 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t | Reloc_proj_name of Projection.Repr.t + | Reloc_caml_prim of CPrimitives.t type patches type emitcodes diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 0d77cae077..6690a379ce 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -542,6 +542,14 @@ let makeblock tag nparams arity args = Lval(val_of_block Obj.last_non_constant_constructor_tag args) else Lmakeblock(tag, args) +let makearray args def = + try + let p = Array.map get_value args in + Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def)) + with Not_found -> + let ar = Lmakeblock(0, args) in (* build the ocaml array *) + let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *) + Lmakeblock(0,[|kind|]) (* the reference *) (* Compiling constants *) @@ -568,8 +576,13 @@ let expand_prim kn op arity = let lambda_of_prim kn op args = let arity = CPrimitives.arity op in - if Array.length args >= arity then prim kn op args - else mkLapp (expand_prim kn op arity) args + match Int.compare (Array.length args) arity with + | 0 -> prim kn op args + | x when x > 0 -> + let prim_args = Array.sub args 0 arity in + let extra_args = Array.sub args arity (Array.length args - arity) in + mkLapp(prim kn op prim_args) extra_args + | _ -> mkLapp (expand_prim kn op arity) args (*i Global environment *) @@ -768,6 +781,9 @@ let rec lambda_of_constr env c = | Int i -> Luint i | Float f -> Lfloat f + | Array(_u, t,def,_ty) -> + let def = lambda_of_constr env def in + makearray (lambda_of_args env 0 t) def and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/constr.ml b/kernel/constr.ml index d0598bdad1..1837a39764 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -109,6 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Proj of Projection.t * 'constr | Int of Uint63.t | Float of Float64.t + | Array of 'univs * 'constr array * 'constr * 'types (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term @@ -246,6 +247,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with (* Constructs a primitive integer *) let mkInt i = Int i +(* Constructs an array *) +let mkArray (u,t,def,ty) = Array (u,t,def,ty) + (* Constructs a primitive float number *) let mkFloat f = Float f @@ -485,6 +489,8 @@ let fold f acc c = match kind c with 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 @@ -508,6 +514,7 @@ let iter f c = match kind c with | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f 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 @@ -532,6 +539,8 @@ let iter_with_binders g f n c = match kind c with | 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 @@ -560,6 +569,8 @@ let fold_constr_with_binders g f n acc c = 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 @@ -705,6 +716,12 @@ let map_gen userview f c = match kind c with 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') let map_user_view = map_gen true let map = map_gen false @@ -773,6 +790,12 @@ let fold_map f accu c = match kind c with 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 @@ -835,6 +858,12 @@ let map_with_binders g f l c0 = match kind c0 with 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 *) @@ -877,6 +906,7 @@ let fold_with_full_binders g f n acc c = let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl 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 type 'univs instance_compare_fn = (GlobRef.t * int) option -> @@ -935,9 +965,13 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t && 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 _), _ -> false + | CoFix _ | Int _ | Float _| Array _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -1129,6 +1163,9 @@ let constr_ord_int f t1 t2 = | Int i1, Int i2 -> Uint63.compare i1 i2 | Int _, _ -> -1 | _, Int _ -> 1 | Float f1, Float f2 -> Float64.total_compare f1 f2 + | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) -> + (((Array.compare f) =? f) ==? f) t1 t2 def1 def2 ty1 ty2 + | Array _, _ -> -1 | _, Array _ -> 1 let rec compare m n= constr_ord_int compare m n @@ -1222,9 +1259,11 @@ let hasheq t1 t2 = && array_eqeq bl1 bl2 | Int i1, Int i2 -> i1 == i2 | Float f1, Float f2 -> Float64.equal f1 f2 + | 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 _), _ -> false + | Fix _ | CoFix _ | Int _ | Float _ | Array _), _ -> false (** 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 *) @@ -1332,6 +1371,13 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let (h,l) = Uint63.to_int2 i in (t, combinesmall 18 (combine h l)) | Float f -> (t, combinesmall 19 (Float64.hash f)) + | Array (u,t,def,ty) -> + let u, hu = sh_instance u in + let t, ht = hash_term_array t in + let def, hdef = sh_rec def in + let ty, hty = sh_rec ty in + let h = combine4 hu ht hdef hty in + (Array(u,t,def,ty), combinesmall 20 h) and sh_invert = function | NoInvert -> NoInvert, 0 @@ -1413,6 +1459,8 @@ let rec hash t = combinesmall 17 (combine (Projection.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) + | Array(u,t,def,ty) -> + combinesmall 20 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty)) and hash_invert = function | NoInvert -> 0 @@ -1566,6 +1614,9 @@ let rec debug_print c = str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" | Float i -> str"Float("++str (Float64.to_string i) ++ 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")@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str"}" and debug_invert = let open Pp in function | NoInvert -> mt() diff --git a/kernel/constr.mli b/kernel/constr.mli index 0c151bb43c..62f2555a7e 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -84,6 +84,9 @@ val mkVar : Id.t -> constr (** Constructs a machine integer *) val mkInt : Uint63.t -> constr +(** Constructs an array *) +val mkArray : Univ.Instance.t * constr array * constr * types -> constr + (** Constructs a machine float number *) val mkFloat : Float64.t -> constr @@ -246,6 +249,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Proj of Projection.t * 'constr | Int of Uint63.t | Float of Float64.t + | Array of 'univs * 'constr array * 'constr * 'types (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index f41585e93a..185fb9f5a4 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -63,6 +63,15 @@ let set_global v = global_data.glob_len <- global_data.glob_len + 1; n +(* Initialization of OCaml primitives *) +let parray_make = set_global Vmvalues.parray_make +let parray_get = set_global Vmvalues.parray_get +let parray_get_default = set_global Vmvalues.parray_get_default +let parray_set = set_global Vmvalues.parray_set +let parray_copy = set_global Vmvalues.parray_copy +let parray_reroot = set_global Vmvalues.parray_reroot +let parray_length = set_global Vmvalues.parray_length + (* table pour les structured_constant et les annotations des switchs *) module SConstTable = Hashtbl.Make (struct @@ -119,6 +128,17 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n +let slot_for_caml_prim = + let open CPrimitives in function + | Arraymake -> parray_make + | Arrayget -> parray_get + | Arraydefault -> parray_get_default + | Arrayset -> parray_set + | Arraycopy -> parray_copy + | Arrayreroot -> parray_reroot + | Arraylength -> parray_length + | _ -> assert false + let slot_for_proj_name key = try ProjNameTable.find proj_name_tbl key with Not_found -> @@ -182,6 +202,7 @@ and eval_to_patch env (buff,pl,fv) = | Reloc_const sc -> slot_for_str_cst sc | Reloc_getglobal kn -> slot_for_getglobal env kn | Reloc_proj_name p -> slot_for_proj_name p + | Reloc_caml_prim op -> slot_for_caml_prim op in let tc = patch buff pl slots in let vm_env = diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 68bd1cbac9..7609c1a64d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -55,7 +55,7 @@ type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) | OpaqueDef of 'opaque (** or an opaque global definition *) - | Primitive of CPrimitives.t (** or a primitive operation *) + | Primitive of CPrimitives.t (** or a primitive operation *) type universes = | Monomorphic of Univ.ContextSet.t @@ -116,11 +116,14 @@ type 'opaque constant_body = { } (** {6 Representation of mutual inductive types in the kernel } *) +type nested_type = +| NestedInd of inductive +| NestedPrimitive of Constant.t type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive +| Norec +| Mrec of inductive +| Nested of nested_type type wf_paths = recarg Rtree.t diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 3de2cb00a4..326bf0d6ad 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -156,21 +156,47 @@ let hcons_const_body cb = } (** {6 Inductive types } *) +let eq_nested_type t1 t2 = match t1, t2 with +| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2 +| NestedInd _, _ -> false +| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2 +| NestedPrimitive _, _ -> false let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true +| Norec, _ -> false | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false +| Mrec _, _ -> false +| Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2 +| Nested _, _ -> false + +let pp_recarg = let open Pp in function + | Declarations.Norec -> str "Norec" + | Declarations.Mrec (mind,i) -> + str "Mrec[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]" + | Declarations.(Nested (NestedInd (mind,i))) -> + str "Nested[" ++ Names.MutInd.print mind ++ pr_comma () ++ int i ++ str "]" + | Declarations.(Nested (NestedPrimitive c)) -> + str "Nested[" ++ Names.Constant.print c ++ str "]" + +let pp_wf_paths x = Rtree.pp_tree pp_recarg x + +let subst_nested_type sub ty = match ty with +| NestedInd (kn,i) -> + let kn' = subst_mind sub kn in + if kn==kn' then ty else NestedInd (kn',i) +| NestedPrimitive c -> + let c',_ = subst_con sub c in + if c==c' then ty else NestedPrimitive c' let subst_recarg sub r = match r with | Norec -> r | Mrec (kn,i) -> let kn' = subst_mind sub kn in if kn==kn' then r else Mrec (kn',i) - | Imbr (kn,i) -> - let kn' = subst_mind sub kn in - if kn==kn' then r else Imbr (kn',i) + | Nested ty -> + let ty' = subst_nested_type sub ty in + if ty==ty' then r else Nested ty' let mk_norec = Rtree.mk_node Norec [||] diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 01e4429e7e..4ab8d45e60 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -46,6 +46,9 @@ val is_opaque : 'a constant_body -> bool val eq_recarg : recarg -> recarg -> bool +val pp_recarg : recarg -> Pp.t +val pp_wf_paths : wf_paths -> Pp.t + val subst_recarg : substitution -> recarg -> recarg val mk_norec : wf_paths diff --git a/kernel/entries.ml b/kernel/entries.ml index e0b678621a..ae64112e33 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -91,8 +91,7 @@ type parameter_entry = Id.Set.t option * types in_universes_entry * inline type primitive_entry = { - prim_entry_type : types option; - prim_entry_univs : Univ.ContextSet.t; (* always monomorphic *) + prim_entry_type : types in_universes_entry option; prim_entry_content : CPrimitives.op_or_type; } diff --git a/kernel/environ.ml b/kernel/environ.ml index 0ae6f242f6..e75ccbb252 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -503,7 +503,7 @@ let constant_type env (kn,u) = type const_evaluation_result = | NoBody | Opaque - | IsPrimitive of CPrimitives.t + | IsPrimitive of Univ.Instance.t * CPrimitives.t exception NotEvaluableConst of const_evaluation_result @@ -535,7 +535,7 @@ let constant_value_in env (kn,u) = subst_instance_constr u b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) - | Primitive p -> raise (NotEvaluableConst (IsPrimitive p)) + | Primitive p -> raise (NotEvaluableConst (IsPrimitive (u,p))) let constant_opt_value_in env cst = try Some (constant_value_in env cst) diff --git a/kernel/environ.mli b/kernel/environ.mli index f489b13a3b..5cb56a2a29 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -225,7 +225,7 @@ val type_in_type_constant : Constant.t -> env -> bool type const_evaluation_result = | NoBody | Opaque - | IsPrimitive of CPrimitives.t + | IsPrimitive of Univ.Instance.t * CPrimitives.t exception NotEvaluableConst of const_evaluation_result val constant_type : env -> Constant.t puniverses -> types constrained diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 0a9f137c45..67a672c349 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -157,6 +157,10 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; + "ISINT_CAML_CALL2"; + "ISARRAY_CAML_CALL1"; + "ISARRAY_INT_CAML_CALL2"; + "ISARRAY_INT_CAML_CALL3"; "STOP" |] diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9da6c7842e..a27ff41a1c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -165,7 +165,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in push_rel decl env in let ra_env' = - (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: + (Nested (NestedInd mi),(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in (* New index of the inductive types *) let newidx = n + auxntyp in @@ -241,6 +241,9 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) + | Const (c,_) when is_primitive_positive_container env c -> + if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) + else check_positive_nested_primitive ienv nmr (c, largs) | _err -> (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives @@ -298,7 +301,16 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr in - (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) + (nmr',(Rtree.mk_rec [|mk_paths (Nested (NestedInd mi)) irecargs|]).(0)) + + and check_positive_nested_primitive (env,n,ntypes,ra_env) nmr (c, largs) = + (* We model the primitive type c X1 ... Xn as if it had one constructor + C : X1 -> ... -> Xn -> c X1 ... Xn + The subterm relation is defined for each primitive in `inductive.ml`. *) + let ra_env = List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + let ienv = (env,n,ntypes,ra_env) in + let nmr',recargs = List.fold_left_map (check_pos ienv) nmr largs in + (nmr', (Rtree.mk_rec [| mk_paths (Nested (NestedPrimitive c)) [| recargs |] |]).(0)) (** [check_constructors ienv check_head nmr c] checks the positivity condition in the type [c] of a constructor (i.e. that recursive diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c51d82ce07..d751d9875a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -464,11 +464,16 @@ let eq_wf_paths = Rtree.equal Declareops.eq_recarg let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 +| Norec, _ -> None | Mrec i1, Mrec i2 -| Imbr i1, Imbr i2 -| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None -| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None -| _ -> None +| Nested (NestedInd i1), Nested (NestedInd i2) +| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None +| Mrec _, _ -> None +| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Nested (NestedInd _), _ -> None +| Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) -> + if Names.Constant.equal c1 c2 then Some r1 else None +| Nested (NestedPrimitive _), _ -> None let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec @@ -551,8 +556,8 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | (Mrec i | Imbr i) -> eq_ind ind i - | Norec -> false + | Mrec i | Nested (NestedInd i) -> eq_ind ind i + | Norec | Nested (NestedPrimitive _) -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} [branches_specif renv c_spec ci] returns an array of x_s specs knowing @@ -603,7 +608,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in - let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in + let rc = Array.mapi (fun j t -> (Nested (NestedInd (mind,j)),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in (env, lra_ind @ ra_env) @@ -637,6 +642,11 @@ let abstract_mind_lc ntyps npars lc = in Array.map (substl make_abs) lc +let is_primitive_positive_container env c = + match env.retroknowledge.Retroknowledge.retro_array with + | Some c' when Constant.equal c c' -> true + | _ -> false + (* [get_recargs_approx env tree ind args] builds an approximation of the recargs tree for ind, knowing args. The argument tree is used to know when candidate nested types should be traversed, pruning the tree otherwise. This code is very @@ -657,8 +667,14 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> - build_recargs_nested ienv tree (ind_kn, largs) + | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' -> + build_recargs_nested ienv tree (ind_kn, largs) + | _ -> mk_norec + end + | Const (c,_) when is_primitive_positive_container env c -> + begin match dest_recarg tree with + | Nested (NestedPrimitive c') when Constant.equal c c' -> + build_recargs_nested_primitive ienv tree (c, largs) | _ -> mk_norec end | _err -> @@ -696,11 +712,21 @@ let get_recargs_approx env tree ind args = build_recargs_constructors ienv' trees.(j).(k) c') auxlcvect in - mk_paths (Imbr (mind,j)) paths + mk_paths (Nested (NestedInd (mind,j))) paths in let irecargs = Array.mapi mk_irecargs mib.mind_packets in (Rtree.mk_rec irecargs).(i) + and build_recargs_nested_primitive (env, ra_env) tree (c, largs) = + if eq_wf_paths tree mk_norec then tree + else + let ntypes = 1 in (* Primitive types are modelled by non-mutual inductive types *) + let ra_env = List.map (fun (r,t) -> (r,Rtree.lift ntypes t)) ra_env in + let ienv = (env, ra_env) in + let paths = List.map2 (build_recargs ienv) (dest_subterms tree).(0) largs in + let recargs = [| mk_paths (Nested (NestedPrimitive c)) [| paths |] |] in + (Rtree.mk_rec recargs).(0) + and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in @@ -829,8 +855,17 @@ let rec subterm_specif renv stack t = | Dead_code -> Dead_code | Not_subterm -> Not_subterm) - | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm + | Const c -> + begin try + let _ = Environ.constant_value_in renv.env c in Not_subterm + with + | NotEvaluableConst (IsPrimitive (_u,op)) when List.length l >= CPrimitives.arity op -> + primitive_specif renv op l + | NotEvaluableConst _ -> Not_subterm + end + + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Ind _ + | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Not_subterm (* Other terms are not subterms *) @@ -846,6 +881,24 @@ and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t +and primitive_specif renv op args = + let open CPrimitives in + match op with + | Arrayget | Arraydefault -> + (* t.[i] and default t can be seend as strict subterms of t, with a + potentially nested rectree. *) + let arg = List.nth args 1 in (* the result is a strict subterm of the second argument *) + let subt = subterm_specif renv [] arg in + begin match subt with + | Subterm (_s, wf) -> + let wf_args = (dest_subterms wf).(0) in + spec_of_tree (List.nth wf_args 0) (* first and only parameter of `array` *) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm + end + | _ -> Not_subterm + + (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm x tree = match Lazy.force x with @@ -1086,6 +1139,12 @@ let check_one_fix renv recpos trees def = | Sort _ | Int _ | Float _ -> assert (List.is_empty l) + | Array (_u, t,def,ty) -> + assert (List.is_empty l); + Array.iter (check_rec_call renv []) t; + check_rec_call renv [] def; + check_rec_call renv [] ty + (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () @@ -1278,7 +1337,7 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ | Int _ | Float _ -> + | Ind _ | Fix _ | Proj _ | Int _ | Float _ | Array _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9f865f8f01..78658dc4de 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -105,6 +105,13 @@ val check_case_info : env -> pinductive -> Sorts.relevance -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) +(** [is_primitive_positive_container env c] tells if the constant [c] is + registered as a primitive type that can be seen as a container where the + occurrences of its parameters are positive, in which case the positivity and + guard conditions are extended to allow inductive types to nest their subterms + in these containers. *) +val is_primitive_positive_container : env -> Constant.t -> bool + (** When [chk] is false, the guard condition is not actually checked. *) val check_fix : env -> fixpoint -> unit diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 71a3e95d25..8191a5b0f3 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -138,6 +138,13 @@ let rec infer_fterm cv_pb infos variances hd stk = let le = Esubst.subs_liftn n e in let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in infer_stack infos variances stk + | FArray (u,elemsdef,ty) -> + let variances = infer_generic_instance_eq variances u in + let variances = infer_fterm CONV infos variances ty [] in + let elems, def = Parray.to_array elemsdef in + let variances = infer_fterm CONV infos variances def [] in + let variances = infer_vect infos variances elems in + infer_stack infos variances stk | FCaseInvert (_,p,_,_,br,e) -> let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index cc9da3a2ce..41388d9f17 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -1,8 +1,8 @@ Names TransparentState Uint63 +Parray Float64 -CPrimitives Univ UGraph Esubst @@ -12,6 +12,7 @@ Context Constr Vars Term +CPrimitives Mod_subst Vmvalues Cbytecodes diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c8cee7db73..ae070e6f8e 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -259,6 +259,7 @@ type primitive = | Mk_proj | Is_int | Is_float + | Is_parray | Cast_accu | Upd_cofix | Force_cofix @@ -285,7 +286,8 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * pconstant) option + | MLparray_of_array + | Coq_primitive of CPrimitives.t * bool (* check for accu *) let eq_primitive p1 p2 = match p1, p2 with @@ -346,15 +348,15 @@ let primitive_hash = function | MLsub -> 31 | MLmul -> 32 | MLmagic -> 33 - | Coq_primitive (prim, None) -> combinesmall 34 (CPrimitives.hash prim) - | Coq_primitive (prim, Some (prefix,(kn,_))) -> - combinesmall 35 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) - | Mk_proj -> 36 - | MLarrayget -> 37 - | Mk_empty_instance -> 38 - | Mk_float -> 39 - | Is_float -> 40 + | Coq_primitive (prim, b) -> combinesmall 34 (combine (CPrimitives.hash prim) (Hashtbl.hash b)) + | Mk_proj -> 35 + | MLarrayget -> 36 + | Mk_empty_instance -> 37 + | Mk_float -> 38 + | Is_float -> 39 + | Is_parray -> 41 | MLnot -> 41 + | MLparray_of_array -> 42 type mllambda = | MLlocal of lname @@ -971,11 +973,14 @@ type prim_aux = let add_check cond targs args = let aux cond t a = - match a with - | PAml(MLint _) -> cond - | PAml ml -> + match t, a with + | CPrimitives.(PITT_type (PT_int63, _)), PAml(MLapp(MLprimitive Mk_uint, _)) -> cond + | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp(MLprimitive MLparray_of_array, _)) -> cond + | CPrimitives.(PITT_type (PT_array, _)), PAml(MLapp (MLglobal (Ginternal "get_value"),_)) -> cond + | CPrimitives.(PITT_type (prim_ty, _)), PAml ml -> (* FIXME: use explicit equality function *) - if List.mem (t, ml) cond then cond else (t, ml)::cond + let c = (CPrimitives.PTE prim_ty, ml) in + if List.mem c cond then cond else c::cond | _ -> cond in Array.fold_left2 aux cond targs args @@ -985,13 +990,15 @@ let extract_prim ml_of l = let cond = ref [] in let type_args p = let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in - Array.of_list (aux (CPrimitives.types p)) in + let params, sign = CPrimitives.types p in + List.length params, Array.of_list (aux sign) in let rec aux l = match l with | Lprim(prefix,kn,p,args) -> - let targs = type_args p in + let nparams, targs = type_args p in let args = Array.map aux args in - cond := add_check !cond targs args; + let checked_args = Array.init (Array.length args - nparams) (fun i -> args.(i+nparams)) in + cond := add_check !cond targs checked_args; PAprim(prefix,kn,p,args) | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l) | _ -> @@ -1006,31 +1013,48 @@ let cast_to_int v = | MLint _ -> v | _ -> MLapp(MLprimitive Val_to_int, [|v|]) -let compile_prim decl cond paux = +let ml_of_instance instance u = + let ml_of_level l = + match Univ.Level.var_index l with + | Some i -> + let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in + mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] + | None -> let i = push_symbol (SymbLevel l) in get_level_code i + in + let u = Univ.Instance.to_array u in + if Array.is_empty u then [||] + else let u = Array.map ml_of_level u in + [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] + +let compile_prim env decl cond paux = let rec opt_prim_aux paux = match paux with | PAprim(_prefix, _kn, op, args) -> - let args = Array.map opt_prim_aux args in - app_prim (Coq_primitive(op,None)) args + let n = CPrimitives.nparams op in + let args = Array.map opt_prim_aux (Array.sub args n (Array.length args - n)) in + app_prim (Coq_primitive(op, false)) args | PAml ml -> ml and naive_prim_aux paux = match paux with - | PAprim(prefix, kn, op, args) -> - app_prim (Coq_primitive(op, Some (prefix,kn))) (Array.map naive_prim_aux args) + | PAprim(prefix, (kn,u), op, args) -> + let uarg = ml_of_instance env.env_univ u in + let prim_const = mkMLapp (MLglobal (Gconstant(prefix,kn))) uarg in + let prim = mkMLapp (MLprimitive(Coq_primitive(op, true))) [|prim_const|] in + mkMLapp prim (Array.map naive_prim_aux args) | PAml ml -> ml in let compile_cond cond paux = match cond with | [] -> opt_prim_aux paux - | [CPrimitives.(PITT_type PT_int63), c1] -> + | [CPrimitives.(PTE PT_int63), c1] -> MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) | _ -> - let ci, cf = + let ci, co = let is_int = - function CPrimitives.(PITT_type PT_int63), _ -> true | _ -> false in + function CPrimitives.(PTE PT_int63), _ -> true | _ -> false in List.partition is_int cond in let condi = let cond = @@ -1038,21 +1062,25 @@ let compile_prim decl cond paux = (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|]) (MLint 0) ci in app_prim MLmagic [|cond|] in - let condf = match cf with + let condo = match co with | [] -> MLint 0 - | [_, c1] -> app_prim Is_float [|c1|] - | (_, c1) :: condf -> + | (CPrimitives.PTE ty, c1) :: condo -> + let check = match ty with + | CPrimitives.PT_float64 -> Is_float + | CPrimitives.PT_array -> Is_parray + | CPrimitives.PT_int63 -> assert false + in List.fold_left - (fun ml (_, c) -> app_prim MLand [| ml; app_prim Is_float [|c|]|]) - (app_prim Is_float [|c1|]) condf in - match ci, cf with + (fun ml (_, c) -> app_prim MLand [| ml; app_prim check [|c|]|]) + (app_prim check [|c1|]) condo in + match ci, co with | [], [] -> opt_prim_aux paux | _ :: _, [] -> MLif(condi, naive_prim_aux paux, opt_prim_aux paux) | [], _ :: _ -> - MLif(condf, opt_prim_aux paux, naive_prim_aux paux) + MLif(condo, opt_prim_aux paux, naive_prim_aux paux) | _ :: _, _ :: _ -> - let cond = app_prim MLand [|condf; app_prim MLnot [|condi|]|] in + let cond = app_prim MLand [|condo; app_prim MLnot [|condi|]|] in MLif(cond, opt_prim_aux paux, naive_prim_aux paux) in let add_decl decl body = @@ -1065,19 +1093,6 @@ let compile_prim decl cond paux = else add_decl decl (compile_cond cond paux) -let ml_of_instance instance u = - let ml_of_level l = - match Univ.Level.var_index l with - | Some i -> - let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in - mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] - | None -> let i = push_symbol (SymbLevel l) in get_level_code i - in - let u = Univ.Instance.to_array u in - if Array.is_empty u then [||] - else let u = Array.map ml_of_level u in - [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] - let rec ml_of_lam env l t = match t with | Lrel(id ,i) -> get_rel env id i @@ -1118,7 +1133,7 @@ let ml_of_instance instance u = | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in - compile_prim decl cond paux + compile_prim env decl cond paux | Lcase (annot,p,a,bs) -> (* let predicate_uid fv_pred = compilation of p let rec case_uid fv a_uid = @@ -1333,6 +1348,9 @@ let ml_of_instance instance u = MLconstruct(prefix,cn,tag,args) | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | Lfloat f -> MLapp(MLprimitive Mk_float, [|MLfloat f|]) + | Lparray (t,def) -> + let def = ml_of_lam env l def in + MLapp(MLprimitive MLparray_of_array, [| MLarray (Array.map (ml_of_lam env l) t); def |]) | Lval v -> let i = push_symbol (SymbValue v) in get_value_code i | Lsort s -> @@ -1777,6 +1795,7 @@ let pp_mllam fmt l = | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" | Is_float -> Format.fprintf fmt "is_float" + | Is_parray -> Format.fprintf fmt "is_parray" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" | Force_cofix -> Format.fprintf fmt "force_cofix" @@ -1803,11 +1822,10 @@ let pp_mllam fmt l = | MLmagic -> Format.fprintf fmt "Obj.magic" | MLarrayget -> Format.fprintf fmt "Array.get" | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" - | Coq_primitive (op,None) -> + | MLparray_of_array -> Format.fprintf fmt "parray_of_array" + | Coq_primitive (op, false) -> Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) - | Coq_primitive (op, Some (prefix,(c,_))) -> - Format.fprintf fmt "%s %a" (CPrimitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix,c))) + | Coq_primitive (op, true) -> Format.fprintf fmt "%s" (CPrimitives.to_string op) in Format.fprintf fmt "@[%a@]" pp_mllam l diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 31a716a786..01e9550ec5 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -38,6 +38,10 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfloat64 f1, Vfloat64 f2 -> if Float64.(equal (of_float f1) (of_float f2)) then cu else raise NotConvertible + | Varray t1, Varray t2 -> + let len = Parray.length_int t1 in + if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible; + Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV lvl v1 v2 cu) cu t1 t2 | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -51,7 +55,7 @@ let rec conv_val env pb lvl v1 v2 cu = aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu - | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible + | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Varray _ | Vblock _), _ -> raise NotConvertible and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 3819cfd8ee..b00b96018f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -40,6 +40,7 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) + | Lparray of lambda array * lambda | Lmakeblock of prefix * inductive * int * lambda array (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) @@ -187,6 +188,10 @@ let map_lam_with_binders g f n lam = | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') + | Lparray (p,def) -> + let p' = Array.Smart.map (f n) p in + let def' = f n def in + if def' == def && p == p' then lam else Lparray (p', def') (*s Lift and substitution *) @@ -377,6 +382,12 @@ let makeblock env ind tag nparams arity args = let prefix = get_mind_prefix env (fst ind) in Lmakeblock(prefix, ind, tag, args) +let makearray args def = + try + let p = Array.map get_value args in + Lval (Nativevalues.parray_of_array p (get_value def)) + with Not_found -> Lparray (args, def) + (* Translation of constants *) let rec get_alias env (kn, u as p) = @@ -400,8 +411,13 @@ let expand_prim env kn op arity = let lambda_of_prim env kn op args = let arity = CPrimitives.arity op in - if Array.length args >= arity then prim env kn op args - else mkLapp (expand_prim env kn op arity) args + match Int.compare (Array.length args) arity with + | 0 -> prim env kn op args + | x when x > 0 -> + let prim_args = Array.sub args 0 arity in + let extra_args = Array.sub args arity (Array.length args - arity) in + mkLapp(prim env kn op prim_args) extra_args + | _ -> mkLapp (expand_prim env kn op arity) args (*i Global environment *) @@ -589,6 +605,10 @@ let rec lambda_of_constr cache env sigma c = | Float f -> Lfloat f + | Array (_u, t, def, _ty) -> + let def = lambda_of_constr cache env sigma def in + makearray (lambda_of_args cache env sigma 0 t) def + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index e339286329..619d362f35 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -34,6 +34,7 @@ type lambda = | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl | Lint of int (* a constant constructor *) + | Lparray of lambda array * lambda | Lmakeblock of prefix * inductive * int * lambda array (* prefix, inductive name, constructor tag, arguments *) (* A fully applied non-constant constructor *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index a5fcfae1fc..9e17f97a56 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -244,6 +244,7 @@ type kind_of_value = | Vconst of int | Vint64 of int64 | Vfloat64 of float + | Varray of t Parray.t | Vblock of block let kind_of_value (v:t) = @@ -253,7 +254,8 @@ let kind_of_value (v:t) = else let tag = Obj.tag o in if Int.equal tag accumulate_tag then - Vaccu (Obj.magic v) + if Int.equal (Obj.size o) 1 then Varray (Obj.magic v) + else Vaccu (Obj.magic v) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) @@ -686,6 +688,84 @@ let next_down accu x = if is_float x then no_check_next_down x else accu x +let is_parray t = + let t = Obj.magic t in + Obj.is_block t && Obj.size t = 1 + +let to_parray t = Obj.magic t +let of_parray t = Obj.magic t + +let no_check_arraymake n def = + of_parray (Parray.make (to_uint n) def) + +let arraymake accu vA n def = + if is_int n then + no_check_arraymake n def + else accu vA n def + +let no_check_arrayget t n = + Parray.get (to_parray t) (to_uint n) +[@@ocaml.inline always] + +let arrayget accu vA t n = + if is_parray t && is_int n then + no_check_arrayget t n + else accu vA t n + +let no_check_arraydefault t = + Parray.default (to_parray t) +[@@ocaml.inline always] + +let arraydefault accu vA t = + if is_parray t then + no_check_arraydefault t + else accu vA t + +let no_check_arrayset t n v = + of_parray (Parray.set (to_parray t) (to_uint n) v) +[@@ocaml.inline always] + +let arrayset accu vA t n v = + if is_parray t && is_int n then + no_check_arrayset t n v + else accu vA t n v + +let no_check_arraycopy t = + of_parray (Parray.copy (to_parray t)) +[@@ocaml.inline always] + +let arraycopy accu vA t = + if is_parray t then + no_check_arraycopy t + else accu vA t + +let no_check_arrayreroot t = + of_parray (Parray.reroot (to_parray t)) +[@@ocaml.inline always] + +let arrayreroot accu vA t = + if is_parray t then + no_check_arrayreroot t + else accu vA t + +let no_check_arraylength t = + mk_uint (Parray.length (to_parray t)) +[@@ocaml.inline always] + +let arraylength accu vA t = + if is_parray t then + no_check_arraylength t + else accu vA t + +let parray_of_array t def = + (Obj.magic (Parray.unsafe_of_array t def) : t) + +let arrayinit n (f:t->t) def = + of_parray (Parray.init (to_uint n) (Obj.magic f) def) + +let arraymap f t = + of_parray (Parray.map f (to_parray t)) + let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%02x" i) let bohcnv = Array.init 256 (fun i -> i - (if 0x30 <= i then 0x30 else 0) - diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 78a9b2ea13..08c5bd7126 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -134,6 +134,7 @@ type kind_of_value = | Vconst of int | Vint64 of int64 | Vfloat64 of float + | Varray of t Parray.t | Vblock of block val kind_of_value : t -> kind_of_value @@ -332,3 +333,39 @@ val no_check_next_up : t -> t val no_check_next_down : t -> t [@@ocaml.inline always] + +(** Support for arrays *) + +val parray_of_array : t array -> t -> t +val is_parray : t -> bool + +val arraymake : t -> t -> t -> t -> t (* accu A n def *) +val arrayget : t -> t -> t -> t -> t (* accu A t n *) +val arraydefault : t -> t -> t (* accu A t *) +val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *) +val arraycopy : t -> t -> t -> t (* accu A t *) +val arrayreroot : t -> t -> t -> t (* accu A t *) +val arraylength : t -> t -> t -> t (* accu A t *) +val arrayinit : t -> t -> t -> t (* accu A n f def *) +val arraymap : t -> t -> t (* accu A B f t *) + +val no_check_arraymake : t -> t -> t +[@@ocaml.inline always] + +val no_check_arrayget : t -> t -> t -> t +[@@ocaml.inline always] + +val no_check_arraydefault : t -> t +[@@ocaml.inline always] + +val no_check_arrayset : t -> t -> t -> t +[@@ocaml.inline always] + +val no_check_arraycopy : t -> t +[@@ocaml.inline always] + +val no_check_arrayreroot : t -> t +[@@ocaml.inline always] + +val no_check_arraylength : t -> t +[@@ocaml.inline always] diff --git a/kernel/parray.ml b/kernel/parray.ml new file mode 100644 index 0000000000..ea314c1883 --- /dev/null +++ b/kernel/parray.ml @@ -0,0 +1,124 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq 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) *) +(************************************************************************) + +let max_array_length32 = 4194303 + +let max_length = Uint63.of_int max_array_length32 + +let length_to_int i = snd (Uint63.to_int2 i) + +let trunc_size n = + if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int max_array_length32) then + length_to_int n + else max_array_length32 + +type 'a t = ('a kind) ref +and 'a kind = + | Array of 'a array * 'a + | Updated of int * 'a * 'a t + +let unsafe_of_array t def = ref (Array (t,def)) +let of_array t def = unsafe_of_array (Array.copy t) def + +let rec length_int p = + match !p with + | Array (t,_) -> Array.length t + | Updated (_, _, p) -> length_int p + +let length p = Uint63.of_int @@ length_int p + +let rec get p n = + match !p with + | Array (t,def) -> + let l = Array.length t in + if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then + Array.unsafe_get t (length_to_int n) + else def + | Updated (k,e,p) -> + if Uint63.equal n (Uint63.of_int k) then e + else get p n + +let set p n e = + let kind = !p in + match kind with + | Array (t,_) -> + let l = Uint63.of_int @@ Array.length t in + if Uint63.le Uint63.zero n && Uint63.lt n l then + let res = ref kind in + let n = length_to_int n in + p := Updated (n, Array.unsafe_get t n, res); + Array.unsafe_set t n e; + res + else p + | Updated _ -> + if Uint63.le Uint63.zero n && Uint63.lt n (length p) then + ref (Updated((length_to_int n), e, p)) + else p + +let rec default p = + match !p with + | Array (_,def) -> def + | Updated (_,_,p) -> default p + +let make n def = + ref (Array (Array.make (trunc_size n) def, def)) + +let init n f def = + let n = trunc_size n in + let t = Array.init n f in + ref (Array (t, def)) + +let rec to_array p = + match !p with + | Array (t,def) -> Array.copy t, def + | Updated (n,e,p) -> + let (t,_) as r = to_array p in + Array.unsafe_set t n e; r + +let copy p = + let (t,def) = to_array p in + ref (Array (t,def)) + +let rec rerootk t k = + match !t with + | Array _ -> k () + | Updated (i, v, t') -> + let k' () = + begin match !t' with + | Array (a,_def) as n -> + let v' = a.(i) in + Array.unsafe_set a i v; + t := n; + t' := Updated (i, v', t) + | Updated _ -> assert false + end; k() in + rerootk t' k' + +let reroot t = rerootk t (fun () -> t) + +let map f p = + let p = reroot p in + match !p with + | Array (t,def) -> ref (Array (Array.map f t, f def)) + | Updated _ -> assert false + +let fold_left f x p = + let p = reroot p in + match !p with + | Array (t,def) -> f (Array.fold_left f x t) def + | Updated _ -> assert false + +let fold_left2 f a p1 p2 = + let p1 = reroot p1 in + let p2 = reroot p2 in + match !p1, !p2 with + | Array (t1, def1), Array (t2, def2) -> + f (CArray.fold_left2 f a t1 t2) def1 def2 + | _ -> assert false diff --git a/kernel/parray.mli b/kernel/parray.mli new file mode 100644 index 0000000000..0276278bd0 --- /dev/null +++ b/kernel/parray.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq 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) *) +(************************************************************************) + +val max_length : Uint63.t + +type 'a t +val length : 'a t -> Uint63.t +val length_int : 'a t -> int +val get : 'a t -> Uint63.t -> 'a +val set : 'a t -> Uint63.t -> 'a -> 'a t +val default : 'a t -> 'a +val make : Uint63.t -> 'a -> 'a t +val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t +val copy : 'a t -> 'a t +val reroot : 'a t -> 'a t + +val map : ('a -> 'b) -> 'a t -> 'b t + +val to_array : 'a t -> 'a array * 'a (* default *) + +val of_array : 'a array -> 'a (* default *) -> 'a t + +val unsafe_of_array : 'a array -> 'a -> 'a t +(* [unsafe_of_array] injects a mutable array into a persistent one, but does + not perform a copy. This means that if the persistent array is mutated, the + original one will be too. *) + +val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a +val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a diff --git a/kernel/primred.ml b/kernel/primred.ml index c475828cb3..10a8da8813 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -21,6 +21,13 @@ let add_retroknowledge env action = | None -> { retro with retro_float64 = Some c } | Some c' -> assert (Constant.equal c c'); retro in set_retroknowledge env retro + | Register_type(PT_array,c) -> + let retro = env.retroknowledge in + let retro = + match retro.retro_array with + | None -> { retro with retro_array = Some c } + | Some c' -> assert (Constant.equal c c'); retro in + set_retroknowledge env retro | Register_ind(pit,ind) -> let retro = env.retroknowledge in let retro = @@ -120,10 +127,12 @@ module type RedNativeEntries = type elem type args type evd (* will be unit in kernel, evar_map outside *) + type uinstance val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t val get_float : evd -> elem -> Float64.t + val get_parray : evd -> elem -> elem Parray.t val mkInt : env -> Uint63.t -> elem val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem @@ -146,6 +155,7 @@ module type RedNativeEntries = val mkPInf : env -> elem val mkNInf : env -> elem val mkNaN : env -> elem + val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem end module type RedNative = @@ -153,17 +163,20 @@ module type RedNative = type elem type args type evd - val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + type uinstance + val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option end module RedNative (E:RedNativeEntries) : RedNative with type elem = E.elem with type args = E.args - with type evd = E.evd = + with type evd = E.evd + with type uinstance = E.uinstance = struct type elem = E.elem type args = E.args type evd = E.evd + type uinstance = E.uinstance let get_int evd args i = E.get_int evd (E.get args i) @@ -180,7 +193,9 @@ struct let get_float2 evd args = get_float evd args 0, get_float evd args 1 - let red_prim_aux env evd op args = + let get_parray evd args i = E.get_parray evd (E.get args i) + + let red_prim_aux env evd op u args = let open CPrimitives in match op with | Int63head0 -> @@ -315,11 +330,43 @@ struct let f = get_float1 evd args in E.mkFloat env (Float64.next_up f) | Float64next_down -> let f = get_float1 evd args in E.mkFloat env (Float64.next_down f) + | Arraymake -> + let ty = E.get args 0 in + let i = get_int evd args 1 in + let d = E.get args 2 in + E.mkArray env u (Parray.make i d) ty + | Arrayget -> + let t = get_parray evd args 1 in + let i = get_int evd args 2 in + Parray.get t i + | Arraydefault -> + let t = get_parray evd args 1 in + Parray.default t + | Arrayset -> + let ty = E.get args 0 in + let t = get_parray evd args 1 in + let i = get_int evd args 2 in + let a = E.get args 3 in + let t' = Parray.set t i a in + E.mkArray env u t' ty + | Arraycopy -> + let ty = E.get args 0 in + let t = get_parray evd args 1 in + let t' = Parray.copy t in + E.mkArray env u t' ty + | Arrayreroot -> + let ar = E.get args 1 in + let t = E.get_parray evd ar in + let _ = Parray.reroot t in + ar + | Arraylength -> + let t = get_parray evd args 1 in + E.mkInt env (Parray.length t) - let red_prim env evd p args = + let red_prim env evd p u args = try let r = - red_prim_aux env evd p args + red_prim_aux env evd p u args in Some r with NativeDestKO -> None diff --git a/kernel/primred.mli b/kernel/primred.mli index bbe564d8e7..1bfaffaa44 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -24,10 +24,12 @@ module type RedNativeEntries = type elem type args type evd (* will be unit in kernel, evar_map outside *) + type uinstance val get : args -> int -> elem val get_int : evd -> elem -> Uint63.t val get_float : evd -> elem -> Float64.t + val get_parray : evd -> elem -> elem Parray.t val mkInt : env -> Uint63.t -> elem val mkFloat : env -> Float64.t -> elem val mkBool : env -> bool -> elem @@ -50,6 +52,7 @@ module type RedNativeEntries = val mkPInf : env -> elem val mkNInf : env -> elem val mkNaN : env -> elem + val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem end module type RedNative = @@ -57,7 +60,8 @@ module type RedNative = type elem type args type evd - val red_prim : env -> evd -> CPrimitives.t -> args -> elem option + type uinstance + val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option end module RedNative : @@ -65,3 +69,4 @@ module RedNative : RedNative with type elem = E.elem with type args = E.args with type evd = E.evd + with type uinstance = E.uinstance diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e4b0bb17d4..0754e9d4cc 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -138,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 _|Int _|Float _) -> x + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> x | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ -> x + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | Int _ | Float _ | Array _ -> x | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x) @@ -152,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 _|Int _|Float _) -> t + Prod _|Lambda _|Fix _|CoFix _|Int _|Float _|Array _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | Int _ | Float _ | Array _ -> 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) @@ -166,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 _|Int _|Float _) -> t + Prod _|Lambda _|Fix _|CoFix _|LetIn _|Int _|Float _|Array _) -> t | App (c, _) -> begin match kind c with - | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ -> t + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ | Int _ | Float _ | Array _ -> t | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t) @@ -644,13 +644,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv) br1 br2 cuniv + | FArray (u1,t1,ty1), FArray (u2,t2,ty2) -> + let len = Parray.length_int t1 in + if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible; + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in + let cuniv = Parray.fold_left2 (fun u v1 v2 -> ccnv CONV l2r infos el1 el2 v1 v2 u) cuniv t1 t2 in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + (* 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 _ | FCaseInvert _ - | FProd _ | FEvar _ | FInt _ | FFloat _), _ -> raise NotConvertible + | FProd _ | FEvar _ | FInt _ | FFloat _ | FArray _), _ -> 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 diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml index 3dd965aca4..f12b8cba37 100644 --- a/kernel/relevanceops.ml +++ b/kernel/relevanceops.ml @@ -54,7 +54,7 @@ let rec relevance_of_fterm env extra lft f = | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1) | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c | FFlex key -> relevance_of_flex env key - | FInt _ | FFloat _ -> Sorts.Relevant + | FInt _ | FFloat _ | FArray _ -> Sorts.Relevant | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) | FConstruct (c,_) -> relevance_of_constructor env c | FApp (f, _) -> relevance_of_fterm env extra lft f @@ -102,6 +102,7 @@ and relevance_of_term_extra env extra lft subs c = | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> relevance_of_projection env p | Int _ | Float _ -> Sorts.Relevant + | Array _ -> Sorts.Relevant | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 4e642ca11d..f7c4b62d1f 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -19,6 +19,7 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; retro_float64 : Constant.t option; + retro_array : Constant.t option; retro_bool : (constructor * constructor) option; (* true, false *) retro_carry : (constructor * constructor) option; (* C0, C1 *) retro_pair : constructor option; @@ -40,6 +41,7 @@ type retroknowledge = { let empty = { retro_int63 = None; retro_float64 = None; + retro_array = None; retro_bool = None; retro_carry = None; retro_pair = None; @@ -51,4 +53,4 @@ let empty = { type action = | Register_ind : 'a CPrimitives.prim_ind * inductive -> action - | Register_type : CPrimitives.prim_type * Constant.t -> action + | Register_type : 'a CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index bf8ec8badb..fd412cdd0a 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -13,6 +13,7 @@ open Names type retroknowledge = { retro_int63 : Constant.t option; retro_float64 : Constant.t option; + retro_array : Constant.t option; retro_bool : (constructor * constructor) option; (* true, false *) retro_carry : (constructor * constructor) option; (* C0, C1 *) retro_pair : constructor option; @@ -35,4 +36,4 @@ val empty : retroknowledge type action = | Register_ind : 'a CPrimitives.prim_ind * inductive -> action - | Register_type : CPrimitives.prim_type * Constant.t -> action + | Register_type : 'a CPrimitives.prim_type * Constant.t -> action diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c8c2301171..04e7a81697 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -21,13 +21,14 @@ open Constr open Declarations open Environ open Entries +open Univ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) type 'a effect_handler = - env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) + env -> Constr.t -> 'a -> (Constr.t * ContextSet.t * int) let skip_trusted_seff sl b e = let rec aux sl b e acc = @@ -62,55 +63,91 @@ let feedback_completion_typecheck = type typing_context = | MonoTyCtx of Environ.env * unsafe_type_judgment * Id.Set.t * Stateid.t option -| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option +| PolyTyCtx of Environ.env * unsafe_type_judgment * universe_level_subst * AUContext.t * Id.Set.t * Stateid.t option -let infer_declaration env (dcl : constant_entry) = - match dcl with - | ParameterEntry (ctx,(t,uctx),nl) -> - let env = match uctx with - | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env +let check_primitive_type env op_t u t = + let inft = Typeops.type_of_prim_or_type env u op_t in + try Reduction.default_conv ~l2r:false Reduction.CONV env inft t + with Reduction.NotConvertible -> + Type_errors.error_incorrect_primitive env (make_judge op_t inft) t + +let merge_unames = + Array.map2 (fun base user -> match user with Anonymous -> base | Name _ -> user) + +let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = + let open CPrimitives in + let auctx = CPrimitives.op_or_type_univs p in + let univs, typ = + match utyp with + | None -> + let u = UContext.instance (AUContext.repr auctx) in + let typ = Typeops.type_of_prim_or_type env u p in + let univs = if AUContext.is_empty auctx then Monomorphic ContextSet.empty + else Polymorphic auctx in - let j = Typeops.infer env t in - let usubst, univs = Declareops.abstract_universes uctx in - let r = Typeops.assumption_of_judgment env j in - let t = Vars.subst_univs_level_constr usubst j.uj_val in - { - Cooking.cook_body = Undef nl; - cook_type = t; - cook_universes = univs; - cook_relevance = r; - cook_inline = false; - cook_context = ctx; - } + univs, typ - (** Primitives cannot be universe polymorphic *) - | PrimitiveEntry ({ prim_entry_type = otyp; - prim_entry_univs = uctxt; - prim_entry_content = op_t; - }) -> - let env = push_context_set ~strict:true uctxt env in - let ty = match otyp with - | Some typ -> + | Some (typ,Monomorphic_entry uctx) -> + assert (AUContext.is_empty auctx); + let env = push_context_set ~strict:true uctx env in + let u = Instance.empty in + let typ = let typ = Typeops.infer_type env typ in - Typeops.check_primitive_type env op_t typ.utj_val; + check_primitive_type env p u typ.utj_val; typ.utj_val - | None -> - match op_t with - | CPrimitives.OT_op op -> Typeops.type_of_prim env op - | CPrimitives.OT_type _ -> mkSet in - let cd = - match op_t with - | CPrimitives.OT_op op -> Declarations.Primitive op - | CPrimitives.OT_type _ -> Undef None in - { Cooking.cook_body = cd; - cook_type = ty; - cook_universes = Monomorphic uctxt; - cook_inline = false; - cook_context = None; - cook_relevance = Sorts.Relevant; - } + Monomorphic uctx, typ + + | Some (typ,Polymorphic_entry (unames,uctx)) -> + assert (not (AUContext.is_empty auctx)); + (* push_context will check that the universes aren't repeated in the instance + so comparing the sizes works *) + assert (AUContext.size auctx = UContext.size uctx); + (* No polymorphic primitive uses constraints currently *) + assert (Constraint.is_empty (UContext.constraints uctx)); + let env = push_context ~strict:false uctx env in + (* Now we know that uctx matches the auctx *) + let typ = (Typeops.infer_type env typ).utj_val in + let () = check_primitive_type env p (UContext.instance uctx) typ in + let unames = merge_unames (AUContext.names auctx) unames in + let u, auctx = abstract_universes unames uctx in + let typ = Vars.subst_univs_level_constr (make_instance_subst u) typ in + Polymorphic auctx, typ + in + let body = match p with + | OT_op op -> Declarations.Primitive op + | OT_type _ -> Undef None + | OT_const c -> Def (Mod_subst.from_val (CPrimitives.body_of_prim_const c)) + in + { Cooking.cook_body = body; + cook_type = typ; + cook_universes = univs; + cook_inline = false; + cook_context = None; + cook_relevance = Sorts.Relevant; + } + +let infer_declaration env (dcl : constant_entry) = + match dcl with + | ParameterEntry (ctx,(t,uctx),nl) -> + let env = match uctx with + | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env + in + let j = Typeops.infer env t in + let usubst, univs = Declareops.abstract_universes uctx in + let r = Typeops.assumption_of_judgment env j in + let t = Vars.subst_univs_level_constr usubst j.uj_val in + { + Cooking.cook_body = Undef nl; + cook_type = t; + cook_universes = univs; + cook_relevance = r; + cook_inline = false; + cook_context = ctx; + } + + | PrimitiveEntry entry -> infer_primitive env entry | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in @@ -118,13 +155,13 @@ let infer_declaration env (dcl : constant_entry) = let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic ctx + env, empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in - let sbst, auctx = Univ.abstract_universes nas uctx in - let sbst = Univ.make_instance_subst sbst in + let sbst, auctx = abstract_universes nas uctx in + let sbst = make_instance_subst sbst in env, sbst, Polymorphic auctx in let j = Typeops.infer env body in @@ -171,8 +208,8 @@ let infer_opaque env = function let { opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in - let sbst, auctx = Univ.abstract_universes nas uctx in - let usubst = Univ.make_instance_subst sbst in + let sbst, auctx = abstract_universes nas uctx in + let usubst = make_instance_subst sbst in let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in let def = OpaqueDef () in let typ = Vars.subst_univs_level_constr usubst tj.utj_val in @@ -260,7 +297,7 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out | MonoTyCtx (env, tyj, declared, feedback_id) -> let ((body, uctx), side_eff) = body in let (body, uctx', valid_signatures) = handle env body side_eff in - let uctx = Univ.ContextSet.union uctx uctx' in + let uctx = ContextSet.union uctx uctx' in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = Typeops.infer env body in @@ -273,17 +310,17 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out | PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) -> let ((body, ctx), side_eff) = body in let body, ctx', _ = handle env body side_eff in - let ctx = Univ.ContextSet.union ctx ctx' in + let ctx = ContextSet.union ctx ctx' in (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_subgraph ctx env in - let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let private_univs = on_snd (subst_univs_level_constraints usubst) ctx in let j = Typeops.infer env body in let _ = Typeops.judge_of_cast env j DEFAULTcast tj in let () = check_section_variables env declared tj.utj_val body in let def = Vars.subst_univs_level_constr usubst j.uj_val in let () = feedback_completion_typecheck feedback_id in - def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + def, Opaqueproof.PrivatePolymorphic (AUContext.size auctx, private_univs) (*s Global and local constant declaration. *) @@ -325,13 +362,13 @@ let translate_local_def env _id centry = const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; - const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; + const_entry_universes = Monomorphic_entry ContextSet.empty; const_entry_inline_code = false; } in let decl = infer_declaration env (DefinitionEntry centry) in let typ = decl.cook_type in let () = match decl.cook_universes with - | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Monomorphic ctx -> assert (ContextSet.is_empty ctx) | Polymorphic _ -> assert false in let c = match decl.cook_body with diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 58a099f7f6..f86c12e1f1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -213,9 +213,20 @@ let type_of_apply env func funt argsv argstv = apply_rec 0 (inject funt) (* Type of primitive constructs *) -let type_of_prim_type _env = function - | CPrimitives.PT_int63 -> Constr.mkSet - | CPrimitives.PT_float64 -> Constr.mkSet +let type_of_prim_type _env u (type a) (prim : a CPrimitives.prim_type) = match prim with + | CPrimitives.PT_int63 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_float64 -> + assert (Univ.Instance.is_empty u); + Constr.mkSet + | CPrimitives.PT_array -> + begin match Univ.Instance.to_array u with + | [|u|] -> + let ty = Constr.mkType (Univ.Universe.make u) in + Constr.mkProd(Context.anonR, ty , ty) + | _ -> anomaly Pp.(str"universe instance for array type should have length 1") + end let type_of_int env = match env.retroknowledge.Retroknowledge.retro_int63 with @@ -228,71 +239,11 @@ let type_of_float env = | None -> raise (Invalid_argument "Typeops.type_of_float: float64 not_defined") -let type_of_prim env t = - let int_ty () = type_of_int env in - let float_ty () = type_of_float env in - let bool_ty () = - match env.retroknowledge.Retroknowledge.retro_bool with - | Some ((ind,_),_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") - in - let compare_ty () = - match env.retroknowledge.Retroknowledge.retro_cmp with - | Some ((ind,_),_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") - in - let f_compare_ty () = - match env.retroknowledge.Retroknowledge.retro_f_cmp with - | Some ((ind,_),_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") - in - let f_class_ty () = - match env.retroknowledge.Retroknowledge.retro_f_class with - | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind - | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") - in - let pair_ty fst_ty snd_ty = - match env.retroknowledge.Retroknowledge.retro_pair with - | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) - | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") - in - let carry_ty int_ty = - match env.retroknowledge.Retroknowledge.retro_carry with - | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) - | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") - in - let open CPrimitives in - let tr_prim_type = function - | PT_int63 -> int_ty () - | PT_float64 -> float_ty () in - let tr_ind (type t) (i : t prim_ind) (a : t) = match i, a with - | PIT_bool, () -> bool_ty () - | PIT_carry, t -> carry_ty (tr_prim_type t) - | PIT_pair, (t1, t2) -> pair_ty (tr_prim_type t1) (tr_prim_type t2) - | PIT_cmp, () -> compare_ty () - | PIT_f_cmp, () -> f_compare_ty () - | PIT_f_class, () -> f_class_ty () in - let tr_type = function - | PITT_ind (i, a) -> tr_ind i a - | PITT_type t -> tr_prim_type t in - let rec nary_op = function - | [] -> assert false - | [ret_ty] -> tr_type ret_ty - | arg_ty :: r -> - let arg_ty = tr_type arg_ty in - Constr.mkProd(Context.nameR (Id.of_string "x"), arg_ty, nary_op r) in - nary_op (types t) - -let type_of_prim_or_type env = let open CPrimitives in - function - | OT_type t -> type_of_prim_type env t - | OT_op op -> type_of_prim env op - -let judge_of_int env i = - make_judge (Constr.mkInt i) (type_of_int env) - -let judge_of_float env f = - make_judge (Constr.mkFloat f) (type_of_float env) +let type_of_array env u = + assert (Univ.Instance.length u = 1); + match env.retroknowledge.Retroknowledge.retro_array with + | Some c -> mkConstU (c,u) + | None -> CErrors.user_err Pp.(str"The type array must be registered before this construction can be typechecked.") (* Type of product *) @@ -354,6 +305,18 @@ let check_cast env c ct k expected_type = with NotConvertible -> error_actual_type env (make_judge c ct) expected_type +let judge_of_int env i = + make_judge (Constr.mkInt i) (type_of_int env) + +let judge_of_float env f = + make_judge (Constr.mkFloat f) (type_of_float env) + +let judge_of_array env u tj defj = + let def = defj.uj_val in + let ty = defj.uj_type in + Array.iter (fun j -> check_cast env j.uj_val j.uj_type DEFAULTcast ty) tj; + make_judge (mkArray(u, Array.map j_val tj, def, ty)) (mkApp (type_of_array env u, [|ty|])) + (* Inductive types. *) (* The type is parametric over the uniform parameters whose conclusion @@ -621,6 +584,23 @@ let rec execute env cstr = (* Primitive types *) | Int _ -> cstr, type_of_int env | Float _ -> cstr, type_of_float env + | Array(u,t,def,ty) -> + (* ty : Type@{u} and all of t,def : ty *) + let ulev = match Univ.Instance.to_array u with + | [|u|] -> u + | _ -> assert false + in + let ty',tyty = execute env ty in + check_cast env ty' tyty DEFAULTcast (mkType (Universe.make ulev)); + let def', def_ty = execute env def in + check_cast env def' def_ty DEFAULTcast ty'; + let ta = type_of_array env u in + let t' = Array.Smart.map (fun x -> + let x', xt = execute env x in + check_cast env x' xt DEFAULTcast ty'; + x') t in + let cstr = if def'==def && t'==t && ty'==ty then cstr else mkArray(u, t',def',ty') in + cstr, mkApp(ta, [|ty'|]) (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -747,7 +727,77 @@ let judge_of_case env ci pj iv cj lfj = (* Building type of primitive operators and type *) -let check_primitive_type env op_t t = - let inft = type_of_prim_or_type env op_t in - try default_conv ~l2r:false CUMUL env inft t - with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t +let type_of_prim_const env _u c = + let int_ty () = type_of_int env in + match c with + | CPrimitives.Arraymaxlength -> + int_ty () + +let type_of_prim env u t = + let int_ty () = type_of_int env in + let float_ty () = type_of_float env in + let array_ty u a = mkApp(type_of_array env u, [|a|]) in + let bool_ty () = + match env.retroknowledge.Retroknowledge.retro_bool with + | Some ((ind,_),_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type bool must be registered before this primitive.") + in + let compare_ty () = + match env.retroknowledge.Retroknowledge.retro_cmp with + | Some ((ind,_),_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type compare must be registered before this primitive.") + in + let f_compare_ty () = + match env.retroknowledge.Retroknowledge.retro_f_cmp with + | Some ((ind,_),_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_comparison must be registered before this primitive.") + in + let f_class_ty () = + match env.retroknowledge.Retroknowledge.retro_f_class with + | Some ((ind,_),_,_,_,_,_,_,_,_) -> Constr.mkInd ind + | None -> CErrors.user_err Pp.(str"The type float_class must be registered before this primitive.") + in + let pair_ty fst_ty snd_ty = + match env.retroknowledge.Retroknowledge.retro_pair with + | Some (ind,_) -> Constr.mkApp(Constr.mkInd ind, [|fst_ty;snd_ty|]) + | None -> CErrors.user_err Pp.(str"The type pair must be registered before this primitive.") + in + let carry_ty int_ty = + match env.retroknowledge.Retroknowledge.retro_carry with + | Some ((ind,_),_) -> Constr.mkApp(Constr.mkInd ind, [|int_ty|]) + | None -> CErrors.user_err Pp.(str"The type carry must be registered before this primitive.") + in + let open CPrimitives in + let tr_prim_type (tr_type : ind_or_type -> constr) (type a) (ty : a prim_type) (t : a) = match ty with + | PT_int63 -> int_ty t + | PT_float64 -> float_ty t + | PT_array -> array_ty (fst t) (tr_type (snd t)) + in + let tr_ind (tr_type : ind_or_type -> constr) (type t) (i : t prim_ind) (a : t) = match i, a with + | PIT_bool, () -> bool_ty () + | PIT_carry, t -> carry_ty (tr_type t) + | PIT_pair, (t1, t2) -> pair_ty (tr_type t1) (tr_type t2) + | PIT_cmp, () -> compare_ty () + | PIT_f_cmp, () -> f_compare_ty () + | PIT_f_class, () -> f_class_ty () + in + let rec tr_type n = function + | PITT_ind (i, a) -> tr_ind (tr_type n) i a + | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t + | PITT_param i -> Constr.mkRel (n+i) + in + let rec nary_op n = function + | [] -> assert false + | [ret_ty] -> tr_type n ret_ty + | arg_ty :: r -> + Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r) + in + let params, sign = types t in + assert (AUContext.size (univs t) = Instance.length u); + Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params) + +let type_of_prim_or_type env u = let open CPrimitives in + function + | OT_type t -> type_of_prim_type env u t + | OT_op op -> type_of_prim env u op + | OT_const c -> type_of_prim_const env u c diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 65531ed38a..87a5666fcc 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -114,8 +114,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> GlobRef.t -> Constr.named_context -> unit -val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit - (** Types for primitives *) val type_of_int : env -> types @@ -124,8 +122,12 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment val type_of_float : env -> types val judge_of_float : env -> Float64.t -> unsafe_judgment -val type_of_prim_type : env -> CPrimitives.prim_type -> types -val type_of_prim : env -> CPrimitives.t -> types +val type_of_array : env -> Univ.Instance.t -> types +val judge_of_array : env -> Univ.Instance.t -> unsafe_judgment array -> unsafe_judgment -> unsafe_judgment + +val type_of_prim_type : env -> Univ.Instance.t -> 'a CPrimitives.prim_type -> types +val type_of_prim : env -> Univ.Instance.t -> CPrimitives.t -> types +val type_of_prim_or_type : env -> Univ.Instance.t -> CPrimitives.op_or_type -> types val warn_bad_relevance_name : string (** Allow the checker to make this warning into an error. *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 0aca4b41ad..6d8aa02dff 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -985,6 +985,8 @@ module AUContext = struct type t = Names.Name.t array constrained + let make names csts : t = names, csts + let repr (inst, cst) = (Array.init (Array.length inst) (fun i -> Level.var i), cst) diff --git a/kernel/univ.mli b/kernel/univ.mli index 7651e34b12..7286fc84cb 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -353,6 +353,10 @@ module AUContext : sig type t + val make : Names.Name.t array -> Constraint.t -> t + (** Build an abstract context. Constraints may be between universe + variables. *) + val repr : t -> UContext.t (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of the context and [cstr] the abstracted Constraint.t. *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 63d88c659a..f7e28b0cfe 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -252,12 +252,22 @@ let subst_univs_level_constr subst c = let u' = Univ.subst_univs_level_universe subst u in if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) + | Case (ci,p,CaseInvert {univs;args},c,br) -> if Univ.Instance.is_empty univs then Constr.map aux t else let univs' = f univs in if univs' == univs then Constr.map aux t else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) + + | Array (u,elems,def,ty) -> + let u' = f u in + let elems' = CArray.Smart.map aux elems in + let def' = aux def in + let ty' = aux ty in + if u == u' && elems == elems' && def == def' && ty == ty' then t + else (changed := true; mkArray (u',elems',def',ty')) + | _ -> Constr.map aux t in let c' = aux c in @@ -294,10 +304,20 @@ let subst_instance_constr subst c = let u' = Univ.subst_instance_universe subst u in if u' == u then t else (mkSort (Sorts.sort_of_univ u')) + | Case (ci,p,CaseInvert {univs;args},c,br) -> let univs' = f univs in if univs' == univs then Constr.map aux t else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) + + | Array (u,elems,def,ty) -> + let u' = f u in + let elems' = CArray.Smart.map aux elems in + let def' = aux def in + let ty' = aux ty in + if u == u' && elems == elems' && def == def' && ty == ty' then t + else mkArray (u',elems',def',ty') + | _ -> Constr.map aux t in aux c @@ -319,11 +339,14 @@ let universes_of_constr c = let rec aux s c = match kind c with | Const (_c, u) -> - LSet.fold LSet.add (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> - LSet.fold LSet.add (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s + | Array (u,_,_,_) -> + let s = LSet.fold LSet.add (Instance.levels u) s in + Constr.fold aux s c | _ -> Constr.fold aux s c in aux LSet.empty c diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3563407f7e..f78f0d4d1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -76,6 +76,11 @@ and conv_whd env pb k whd1 whd2 cu = | Vfloat64 f1, Vfloat64 f2 -> if Float64.(equal (of_float f1) (of_float f2)) then cu else raise NotConvertible + | Varray t1, Varray t2 -> + if t1 == t2 then cu else + let n = Parray.length_int t1 in + if not (Int.equal n (Parray.length_int t2)) then raise NotConvertible; + Parray.fold_left2 (fun cu v1 v2 -> conv_val env CONV k v1 v2 cu) cu t1 t2 | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> @@ -83,7 +88,7 @@ and conv_whd env pb k whd1 whd2 cu = conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vint64 _, _ - | Vfloat64 _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + | Vfloat64 _, _ | Varray _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible and conv_atom env pb k a1 stk1 a2 stk2 cu = diff --git a/kernel/vm.ml b/kernel/vm.ml index f2d033f89b..d8c66bebd2 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -169,7 +169,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ -> + | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ | Varray _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index f4ce953d4a..ec429d5f9e 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -292,6 +292,7 @@ type whd = | Vconstr_block of vblock | Vint64 of int64 | Vfloat64 of float + | Varray of values Parray.t | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -324,6 +325,7 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vconstr_block _b -> str "Vconstr_block" | Vint64 _ -> str "Vint64" | Vfloat64 _ -> str "Vfloat64" + | Varray _ -> str "Varray" | Vatom_stk (_a,_stk) -> str "Vatom_stk" | Vuniv_level _ -> assert false in @@ -403,7 +405,9 @@ let whd_val : values -> whd = else let tag = Obj.tag o in if tag = accu_tag then - if is_accumulate (fun_code o) then whd_accu o [] + if Int.equal (Obj.size o) 1 then + Varray(Obj.obj o) + else if is_accumulate (fun_code o) then whd_accu o [] else Vprod(Obj.obj o) else if tag = Obj.closure_tag || tag = Obj.infix_tag then @@ -456,7 +460,9 @@ let val_of_atom a = val_of_obj (obj_of_atom a) let val_of_int i = (Obj.magic i : values) -let val_of_uint i = (Obj.magic i : values) +let val_of_uint i = (Obj.magic i : structured_values) + +let val_of_parray p = (Obj.magic p : structured_values) let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in @@ -689,6 +695,7 @@ and pr_whd w = | Vconstr_block _b -> str "Vconstr_block" | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")" + | Varray _ -> str "Varray" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = @@ -701,3 +708,13 @@ and pr_zipper z = | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch _s -> str "Zswitch(...)" | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") + +(** Primitives implemented in OCaml *) + +let parray_make = Obj.magic Parray.make +let parray_get = Obj.magic Parray.get +let parray_get_default = Obj.magic Parray.default +let parray_set = Obj.magic Parray.set +let parray_copy = Obj.magic Parray.copy +let parray_reroot = Obj.magic Parray.reroot +let parray_length = Obj.magic Parray.length diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index cd85440fed..f4070a02a3 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -129,6 +129,7 @@ type whd = | Vconstr_block of vblock | Vint64 of int64 | Vfloat64 of float + | Varray of values Parray.t | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -150,6 +151,7 @@ val val_of_atom : atom -> values val val_of_int : int -> structured_values val val_of_block : tag -> structured_values array -> structured_values val val_of_uint : Uint63.t -> structured_values +val val_of_parray : structured_values Parray.t -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" @@ -199,3 +201,12 @@ val bfield : vblock -> int -> values val check_switch : vswitch -> vswitch -> bool val branch_arg : int -> tag * int -> values + +(** Primitives implemented in OCaml, seen as values (to be used as globals) *) +val parray_make : values +val parray_get : values +val parray_get_default : values +val parray_set : values +val parray_copy : values +val parray_reroot : values +val parray_length : values diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 429e740403..61317f3ef2 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -65,6 +65,18 @@ let test_name_colon = let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None +let test_array_opening = + let open Pcoq.Lookahead in + to_entry "test_array_opening" begin + lk_kw "[" >> lk_kw "|" >> check_no_space + end + +let test_array_closing = + let open Pcoq.Lookahead in + to_entry "test_array_closing" begin + lk_kw "|" >> lk_kw "]" >> check_no_space + end + } GRAMMAR EXTEND Gram @@ -172,9 +184,17 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } + | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance -> + { let t = Array.make (List.length ls) def in + List.iteri (fun i e -> t.(i) <- e) ls; + CAst.make ~loc @@ CArray(u, t, def, ty) + } | "`("; c = operconstr LEVEL "200"; ")" -> { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ] ; + array_elems: + [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]] + ; record_declaration: [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ] ; diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0dbc0513b4..4a41f4c890 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -63,6 +63,11 @@ let pp_boxed_tuple f = function | [x] -> f x | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l)) +let pp_array f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (prlist_with_sep (fun () -> str ";" ++ spc ()) f l) + (** By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the blocks is less that a line length. To avoid this awkward situation, diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e77d37fb81..0bd9efd255 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -30,6 +30,7 @@ val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t +val pp_array : ('a -> Pp.t) -> 'a list -> Pp.t val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t val pr_binding : Id.t list -> Pp.t diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a7c926f50c..2dca1d5e49 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -351,7 +351,7 @@ let rec extract_type env sg db j c args = | (Info, TypeScheme) -> extract_type_app env sg db (r, type_sign env sg ty) args | (Info, Default) -> Tunknown)) - | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false + | Cast _ | LetIn _ | Construct _ | Int _ | Float _ | Array _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -693,6 +693,12 @@ let rec extract_term env sg mle mlt c args = extract_app env sg mle mlt extract_var args | Int i -> assert (args = []); MLuint i | Float f -> assert (args = []); MLfloat f + | Array (_u,t,def,_ty) -> + assert (args = []); + let a = new_meta () in + let ml_arr = Array.map (fun c -> extract_term env sg mle a c []) t in + let def = extract_term env sg mle a def [] in + MLparray(ml_arr, def) | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 97fe8a5776..c25285c987 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -218,6 +218,8 @@ let rec pp_expr par env args = pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") | MLfloat _ -> pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"") + | MLparray _ -> + pp_par par (str "Prelude.error \"EXTRACTION OF ARRAY NOT IMPLEMENTED\"") and pp_cons_pat par r ppl = pp_par par diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 81b3e1bcdc..974d254d9c 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -165,6 +165,11 @@ let rec json_expr env = function ("what", json_str "expr:float"); ("float", json_str (Float64.to_string f)) ] + | MLparray(t,def) -> json_dict [ + ("what", json_str "expr:array"); + ("elems", json_listarr (Array.map (json_expr env) t)); + ("default", json_expr env def) + ] and json_one_pat env (ids,p,t) = let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index 451272d554..a5a6564873 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -128,6 +128,7 @@ and ml_ast = | MLmagic of ml_ast | MLuint of Uint63.t | MLfloat of Float64.t + | MLparray of ml_ast array * ml_ast and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 451272d554..a5a6564873 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -128,6 +128,7 @@ and ml_ast = | MLmagic of ml_ast | MLuint of Uint63.t | MLfloat of Float64.t + | MLparray of ml_ast array * ml_ast and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 465ad50e9b..b1ce10985a 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -431,6 +431,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a + | MLparray (t,def) -> Array.iter (iter n) t; iter n def | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> () in iter 0 @@ -450,6 +451,7 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) + | MLparray (t,def) -> MLparray (Array.map f t, f def) | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ as a -> a @@ -469,6 +471,7 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) + | MLparray (t,def) -> MLparray (Array.map (f n) t, f n def) | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ as a -> a @@ -484,6 +487,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a + | MLparray (t,def) -> Array.iter f t; f def | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> () @@ -521,6 +525,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a + | MLparray (t,def) -> Array.fold_left (fun r a -> r+(nb k a)) 0 t + nb k def | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0 in nb 1 @@ -573,6 +578,11 @@ let dump_unused_vars a = let b' = ren env b in if b' == b then a else MLmagic b' + | MLparray(t,def) -> + let t' = Array.Smart.map (ren env) t in + let def' = ren env def in + if def' == def && t' == t then a else MLparray(t',def') + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a and ren_branch env ((ids,p,b) as tr) = @@ -1406,6 +1416,7 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t + | MLparray(t,def) -> ml_size_array t + ml_size def | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0 diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index d051602844..3a481039bf 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> () + | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ | MLparray _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index a2ce47b11f..088405da5d 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -311,6 +311,11 @@ let rec pp_expr par env args = | MLfloat f -> assert (args=[]); str "(" ++ str (Float64.compile f) ++ str ")" + | MLparray(t,def) -> + assert (args=[]); + let tuple = pp_array (pp_expr true env []) (Array.to_list t) in + let def = pp_expr true env [] def in + str "(ExtrNative.of_array [|" ++ tuple ++ str "|]" ++ spc () ++ def ++ str")" and pp_record_proj par env typ t pv args = diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 1fb605fc9a..ee50476b10 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -133,6 +133,8 @@ let rec pp_expr env args = paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") | MLfloat _ -> paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"") + | MLparray _ -> + paren (str "Prelude.error \"EXTRACTION OF PARRAY NOT IMPLEMENTED\"") and pp_cons_args env = function | MLcons (_,r,args) when is_coinductive r -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f2658a395f..14d0c04212 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -645,6 +645,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos match EConstr.kind sigma f with | Int _ -> user_err Pp.(str "integer cannot be applied") | Float _ -> user_err Pp.(str "float cannot be applied") + | Array _ -> user_err Pp.(str "array cannot be applied") | App _ -> assert false (* we have collected all the app in decompose_app *) | Proj _ -> assert false (*FIXME*) @@ -696,6 +697,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos ; build_proof do_finalize new_infos ] g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") + | Array _ -> CErrors.user_err Pp.(str "Arrays not handled yet") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) Indfun_common.observe_tac diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index f773157c52..ffce2f8c85 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -103,6 +103,8 @@ let is_rec names = names nal) b | GApp (f, args) -> List.exists (lookup names) (f :: args) + | GArray (_u, t, def, ty) -> + Array.exists (lookup names) t || lookup names def || lookup names ty | GCases (_, _, el, brl) -> List.exists (fun (e, _) -> lookup names e) el || List.exists (lookup_br names) brl @@ -2047,7 +2049,8 @@ let rec add_args id new_args = | CGeneralization _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CGeneralization.") | CDelimiters _ -> - CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.")) + CErrors.anomaly ~label:"add_args " (Pp.str "CDelimiters.") + | CArray _ -> CErrors.anomaly ~label:"add_args " (Pp.str "CArray.")) let rec get_args b t : Constrexpr.local_binder_expr list diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 11e4fa0ac7..6ed61043f9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -568,6 +568,7 @@ let rec build_entry_lc env sigma funnames avoid rt : | GProd _ -> user_err Pp.(str "Cannot apply a type") | GInt _ -> user_err Pp.(str "Cannot apply an integer") | GFloat _ -> user_err Pp.(str "Cannot apply a float") + | GArray _ -> user_err Pp.(str "Cannot apply an array") (* end of the application treatement *) ) | GLambda (n, _, t, b) -> (* we first compute the list of constructor @@ -672,6 +673,7 @@ let rec build_entry_lc env sigma funnames avoid rt : build_entry_lc env sigma funnames avoid match_expr | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast (b, _) -> build_entry_lc env sigma funnames avoid b + | GArray _ -> user_err Pp.(str "Not handled GArray") and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples) (brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return = @@ -1196,7 +1198,7 @@ let rec compute_cst_params relnames params gt = discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GArray _ -> CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case")) gt diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5026120849..8e1331ace9 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -109,7 +109,13 @@ let change_vars = | GCast (b, c) -> GCast ( change_vars mapping b - , Glob_ops.map_cast_type (change_vars mapping) c )) + , Glob_ops.map_cast_type (change_vars mapping) c ) + | GArray (u, t, def, ty) -> + GArray + ( u + , Array.map (change_vars mapping) t + , change_vars mapping def + , change_vars mapping ty )) rt and change_vars_br mapping ({CAst.loc; v = idl, patl, res} as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -282,6 +288,12 @@ let rec alpha_rt excluded rt = GCast (alpha_rt excluded b, Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp (f, args) -> GApp (alpha_rt excluded f, List.map (alpha_rt excluded) args) + | GArray (u, t, def, ty) -> + GArray + ( u + , Array.map (alpha_rt excluded) t + , alpha_rt excluded def + , alpha_rt excluded ty ) in new_rt @@ -331,7 +343,9 @@ let is_free_in id = | GHole _ -> false | GCast (b, (CastConv t | CastVM t | CastNative t)) -> is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b - | GInt _ | GFloat _ -> false) + | GInt _ | GFloat _ -> false + | GArray (_u, t, def, ty) -> + Array.exists is_free_in t || is_free_in def || is_free_in ty) x and is_free_in_br {CAst.v = ids, _, rt} = (not (Id.List.mem id ids)) && is_free_in rt @@ -404,6 +418,12 @@ let replace_var_by_term x_id term = | (GSort _ | GHole _) as rt -> rt | GInt _ as rt -> rt | GFloat _ as rt -> rt + | GArray (u, t, def, ty) -> + GArray + ( u + , Array.map replace_var_by_pattern t + , replace_var_by_pattern def + , replace_var_by_pattern ty ) | GCast (b, c) -> GCast ( replace_var_by_pattern b @@ -510,7 +530,10 @@ let expand_as = ( sty , Option.map (expand_as map) po , List.map (fun (rt, t) -> (expand_as map rt, t)) el - , List.map (expand_as_br map) brl )) + , List.map (expand_as_br map) brl ) + | GArray (u, t, def, ty) -> + GArray + (u, Array.map (expand_as map) t, expand_as map def, expand_as map ty)) and expand_as_br map {CAst.loc; v = idl, cpl, rt} = CAst.make ?loc (idl, cpl, expand_as (List.fold_left add_as map cpl) rt) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 701ea56c2a..64f62ba1fb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,9 +305,11 @@ let check_not_nested env sigma forbidden e = | Lambda (_, t, b) -> check_not_nested t; check_not_nested b | LetIn (_, v, t, b) -> check_not_nested t; check_not_nested b; check_not_nested v - | App (f, l) -> - check_not_nested f; - Array.iter check_not_nested l + | App (f, l) -> check_not_nested f + | Array (_u, t, def, ty) -> + Array.iter check_not_nested t; + check_not_nested def; + check_not_nested ty | Proj (p, c) -> check_not_nested c | Const _ -> () | Ind _ -> () @@ -447,6 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Array _ -> user_err Pp.(str "Function cannot treat arrays") | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn (na, b, t, e) -> let new_continuation_tac = diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1ed632f03f..5dedae6388 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -312,6 +312,7 @@ let iter_constr_LR f c = match kind c with | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a + | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> () 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..6880383a31 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) 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/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..30e1dc0611 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 @@ -442,6 +443,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/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/reductionops.ml b/pretyping/reductionops.ml index 18a0637efa..6f02d76f3a 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) @@ -588,6 +588,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 +602,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 +617,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 +705,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 +778,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 +852,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 +869,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 +954,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 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 58fff49faa..b316b3c213 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 diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb518bc2f9..ebf9d4ed1c 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 @@ -301,8 +304,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/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..b3f577b684 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) -> @@ -399,6 +400,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."); diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b285c0abcc..af105f4d63 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -655,6 +655,14 @@ let tag_var = tag Tag.variable return (pr_prim_token p, prec_of_prim_token p) | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) + | CArray(u, t,def,ty) -> + let pp = ref (str " |"++ spc () ++ pr mt ltop def + ++ pr_opt_type_spc (pr mt) ty ++ str " |]" ++ pr_universe_instance u) in + for i = Array.length t - 1 downto 1 do + pp := str ";" ++ pr mt ltop t.(i) ++ !pp + done; + pp := pr mt ltop t.(0) ++ !pp; + hov 0 (str "[|" ++ !pp), 0 in let loc = constr_loc a in pr_with_comments ?loc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index a957f7354f..f89fb9f52d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -127,7 +127,7 @@ let classify_vernac e = | VernacAssumption (_,_,l) -> let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in VtSideff (ids, VtLater) - | VernacPrimitive (id,_,_) -> + | VernacPrimitive ((id,_),_,_) -> VtSideff ([id.CAst.v], VtLater) | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) | VernacInductive (_,l) -> diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 3bed329d31..bb062bfc11 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -86,7 +86,7 @@ let constr_val_discr_st sigma ts t = | Sort _ -> Label(SortLabel, []) | Evar _ -> Everything | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ - | Proj _ | Int _ | Float _ -> Nothing + | Proj _ | Int _ | Float _ | Array _ -> Nothing let constr_pat_discr_st ts t = let open GlobRef in diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 74f793cdfb..dfbcc9fbce 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -620,7 +620,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = end end 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] *) @@ -759,9 +759,9 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |_ -> fold () else fold () - | Int _ | Float _ -> + | Int _ | Float _ | Array _ -> begin match Stack.strip_app stack with - | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) -> + | (_, Stack.Primitive(p,(_,u as kn),rargs,kargs,cst_l')::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 @@ -775,8 +775,9 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = try List.chop n args with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *) in + let s = extra_args @ s 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 + begin match CredNative.red_prim env sigma p u args with | Some t -> whrec cst_l' (t,s) | None -> ((mkApp (mkConstU kn, args), s), cst_l) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index d5358faf59..ec770e2473 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -417,7 +417,7 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = | RelDecl.LocalAssum _ :: c, recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with - | Norec | Imbr _ -> true :: rest + | Norec | Nested _ -> true :: rest | Mrec (_,j) -> if rec_flag && Int.equal j k then true :: true :: rest else true :: rest diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 0f76fdda79..3bcd235b41 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -46,6 +46,7 @@ struct | DCoFix of int * 't array * 't array | DInt of Uint63.t | DFloat of Float64.t + | DArray of 't array * 't * 't (* special constructors only inside the left-hand side of DCtx or DApp. Used to encode lists of foralls/letins/apps as contexts *) @@ -69,6 +70,7 @@ struct Some t' -> str ":=" ++ f t' | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl | DNil -> str "[]" + | DArray _ -> str "ARRAY" (* * Functional iterators for the t datatype @@ -86,6 +88,7 @@ struct | DCoFix(i,ta,ca) -> DCoFix (i,Array.map f ta,Array.map f ca) | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u) + | DArray (t,def,ty) -> DArray(Array.map f t, f def, f ty) let compare_ci ci1 ci2 = let c = ind_ord ci1.ci_ind ci2.ci_ind in @@ -157,6 +160,17 @@ struct | DFloat _, _ -> -1 | _, DFloat _ -> 1 + | DArray(t1,def1,ty1), DArray(t2,def2,ty2) -> + let c = Array.compare cmp t1 t2 in + if c = 0 then + let c = cmp def1 def2 in + if c = 0 then + cmp ty1 ty2 + else c + else c + + | DArray _, _ -> -1 | _, DArray _ -> 1 + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> let c = cmp t1 t2 in if Int.equal c 0 then @@ -178,6 +192,7 @@ struct Array.fold_left f (Array.fold_left f acc ta) ca | DCoFix(i,ta,ca) -> Array.fold_left f (Array.fold_left f acc ta) ca + | DArray(t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u let choose f = function @@ -189,6 +204,7 @@ struct | DFix (ia,i,ta,ca) -> f ta.(0) | DCoFix (i,ta,ca) -> f ta.(0) | DCons ((t,topt),u) -> f u + | DArray(t,def,ty) -> f t.(0) let dummy_cmp () () = 0 @@ -208,10 +224,12 @@ struct Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) -> Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 + | DArray(t1,def1,ty1), DArray(t2,def2,ty2) -> + f (f (Array.fold_left2 f acc t1 t2) def1 def2) ty1 ty2 | 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 _ | DInt _ | DFloat _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _| DArray _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in @@ -230,14 +248,16 @@ struct DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) + | DArray(t1,def1,ty1), DArray(t2,def2,ty2) -> + DArray(Array.map2 f t1 t2, f def1 def2, f ty1 ty2) | 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 _ | DInt _ | DFloat _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _ | DArray _), _ -> assert false let terminal = function | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> true - | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> + | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ | DArray _ -> false let compare t1 t2 = compare dummy_cmp t1 t2 @@ -332,6 +352,8 @@ struct Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) | Int i -> Term (DInt i) | Float f -> Term (DFloat f) + | Array (_u,t,def,ty) -> + Term (DArray (Array.map pat_of_constr t, pat_of_constr def, pat_of_constr ty)) 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 diff --git a/test-suite/Makefile b/test-suite/Makefile index 59cc3e5a38..0935617fbf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -112,7 +112,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr primitive/uint63 primitive/float ltac2 + coqdoc ssr $(wildcard primitive/*) ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS) diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v index 018596ed95..8c06bff056 100644 --- a/test-suite/ltac2/constr.v +++ b/test-suite/ltac2/constr.v @@ -10,3 +10,9 @@ Axiom something : SProp. Ltac2 Eval match (kind '(forall x : something, bool)) with | Prod a c => a | _ => throw Match_failure end. + +From Coq Require Import Int63 PArray. +Open Scope array_scope. +Ltac2 Eval match (kind '([|true|true|])) with + | Array _ _ _ ty => ty + | _ => throw Match_failure end. diff --git a/test-suite/primitive/arrays/copy.v b/test-suite/primitive/arrays/copy.v new file mode 100644 index 0000000000..bc8e733334 --- /dev/null +++ b/test-suite/primitive/arrays/copy.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 5; 2 | 4 |]. +Definition t' : array nat := PArray.copy t. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 5). +Definition foo7 := (eq_refl 5 <: t.[1] = 5). +Definition foo8 := (eq_refl 5 <<: t.[1] = 5). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 5). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 5). diff --git a/test-suite/primitive/arrays/default.v b/test-suite/primitive/arrays/default.v new file mode 100644 index 0000000000..3b89787faf --- /dev/null +++ b/test-suite/primitive/arrays/default.v @@ -0,0 +1,10 @@ +From Coq Require Import Int63 PArray. + +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition foo1 := (eq_refl : default t = 4). +Definition foo2 := (eq_refl 4 <: default t = 4). +Definition foo3 := (eq_refl 4 <<: default t = 4). +Definition x1 := Eval compute in default t. +Definition foo4 := (eq_refl : x1 = 4). +Definition x2 := Eval cbn in default t. +Definition foo5 := (eq_refl : x2 = 4). diff --git a/test-suite/primitive/arrays/get.v b/test-suite/primitive/arrays/get.v new file mode 100644 index 0000000000..9a6f09a83b --- /dev/null +++ b/test-suite/primitive/arrays/get.v @@ -0,0 +1,86 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +(* Test reduction of primitives on array with kernel conversion, vm_compute, +native_compute, cbv, cbn *) + +(* Immediate values *) +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition foo1 := (eq_refl : t.[0] = 1). +Definition foo2 := (eq_refl 1 <: t.[0] = 1). +Definition foo3 := (eq_refl 1 <<: t.[0] = 1). +Definition x1 := Eval compute in t.[0]. +Definition foo4 := (eq_refl : x1 = 1). +Definition x2 := Eval cbn in t.[0]. +Definition foo5 := (eq_refl : x2 = 1). + +Definition foo6 := (eq_refl : t.[2] = 2). +Definition foo7 := (eq_refl 2 <: t.[2] = 2). +Definition foo8 := (eq_refl 2 <<: t.[2] = 2). +Definition x3 := Eval compute in t.[2]. +Definition foo9 := (eq_refl : x3 = 2). +Definition x4 := Eval cbn in t.[2]. +Definition foo10 := (eq_refl : x4 = 2). + +Definition foo11 := (eq_refl : t.[99] = 4). +Definition foo12 := (eq_refl 4 <: t.[99] = 4). +Definition foo13 := (eq_refl 4 <<: t.[99] = 4). +Definition x5 := Eval compute in t.[4]. +Definition foo14 := (eq_refl : x5 = 4). +Definition x6 := Eval cbn in t.[4]. +Definition foo15 := (eq_refl : x6 = 4). + +(* Computations inside the array *) +Definition t2 : array nat := [| 1 + 3 | 5 |]. +Definition foo16 := (eq_refl : t2.[0] = 4). +Definition foo17 := (eq_refl 4 <: t2.[0] = 4). +Definition foo18 := (eq_refl 4 <<: t2.[0] = 4). +Definition x7 := Eval compute in t2.[0]. +Definition foo19 := (eq_refl : x7 = 4). +Definition x8 := Eval cbn in t2.[0]. +Definition foo20 := (eq_refl : x8 = 4). + +(* Functions inside the array *) +Definition t3 : array (nat -> nat) := [| fun x => x | fun x => O |]. +Definition foo21 := (eq_refl : t3.[0] 2 = 2). +Definition foo22 := (eq_refl 2 <: t3.[0] 2 = 2). +Definition foo23 := (eq_refl 2 <<: t3.[0] 2 = 2). +Definition x9 := Eval compute in t3.[0] 2. +Definition foo24 := (eq_refl : x9 = 2). +Definition x10 := Eval cbn in t3.[0] 2. +Definition foo25 := (eq_refl : x10 = 2). + +Ltac check_const_eq name constr := + let v := (eval cbv delta [name] in name) in + tryif constr_eq v constr + then idtac + else fail 0 "Not syntactically equal:" name ":=" v "<>" constr. + +Notation check_const_eq name constr := (ltac:(check_const_eq name constr; exact constr)) (only parsing). + +(* Stuck primitive *) +Definition lazy_stuck_get := Eval lazy in (fun A (t : array A) => t.[0]). +Definition vm_stuck_get := Eval vm_compute in (fun A (t : array A) => t.[0]). +Definition native_stuck_get := Eval native_compute in (fun A (t : array A) => t.[0]). +Definition compute_stuck_get := Eval compute in (fun A (t : array A) => t.[0]). +Definition cbn_stuck_get := Eval cbn in (fun A (t : array A) => t.[0]). + +Check check_const_eq lazy_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq vm_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq native_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq compute_stuck_get (fun A (t : array A) => t.[0]). +Check check_const_eq cbn_stuck_get (fun A (t : array A) => t.[0]). + +(* Under-application *) +Definition lazy_get := Eval lazy in @PArray.get. +Definition vm_get := Eval vm_compute in @PArray.get. +Definition native_get := Eval native_compute in @PArray.get. +Definition compute_get := Eval compute in @PArray.get. +Definition cbn_get := Eval cbn in @PArray.get. + +Check check_const_eq lazy_get (@PArray.get). +Check check_const_eq vm_get (fun A (t : array A) i => t.[i]). +Check check_const_eq native_get (fun A (t : array A) i => t.[i]). +Check check_const_eq compute_get (@PArray.get). +Check check_const_eq cbn_get (@PArray.get). diff --git a/test-suite/primitive/arrays/length.v b/test-suite/primitive/arrays/length.v new file mode 100644 index 0000000000..67f686f2fb --- /dev/null +++ b/test-suite/primitive/arrays/length.v @@ -0,0 +1,12 @@ +From Coq Require Import Int63 PArray. + +Open Scope int63_scope. + +Definition t : array nat := [| 1; 3; 2 | 4 |]%nat. +Definition foo1 := (eq_refl : PArray.length t = 3). +Definition foo2 := (eq_refl 3 <: PArray.length t = 3). +Definition foo3 := (eq_refl 3 <<: PArray.length t = 3). +Definition x1 := Eval compute in PArray.length t. +Definition foo4 := (eq_refl : x1 = 3). +Definition x2 := Eval cbn in PArray.length t. +Definition foo5 := (eq_refl : x2 = 3). diff --git a/test-suite/primitive/arrays/literal.v b/test-suite/primitive/arrays/literal.v new file mode 100644 index 0000000000..13e57adbbe --- /dev/null +++ b/test-suite/primitive/arrays/literal.v @@ -0,0 +1,6 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |]. +Definition t2 := [|Type|Type|]. diff --git a/test-suite/primitive/arrays/make.v b/test-suite/primitive/arrays/make.v new file mode 100644 index 0000000000..a3a39470ed --- /dev/null +++ b/test-suite/primitive/arrays/make.v @@ -0,0 +1,18 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +(* Immediate values *) +Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |]. +Definition t2 := PArray.make 4 3. +Definition foo1 := (eq_refl : t1 = t2). +Definition foo2 := (eq_refl t1 <: t1 = t2). +Definition foo3 := (eq_refl t1 <<: t1 = t2). +Definition x1 := Eval compute in t2. +Definition foo4 := (eq_refl : x1 = t1). +Definition x2 := Eval cbn in t2. +Definition foo5 := (eq_refl : x2 = t1). + +Definition partial1 := Eval lazy in @PArray.make. +Definition partial2 := Eval vm_compute in @PArray.make. +Definition partial3 := Eval native_compute in @PArray.make. diff --git a/test-suite/primitive/arrays/max_length.v b/test-suite/primitive/arrays/max_length.v new file mode 100644 index 0000000000..54a6af7a19 --- /dev/null +++ b/test-suite/primitive/arrays/max_length.v @@ -0,0 +1,13 @@ +From Coq Require Import Int63 PArray. + +Open Scope int63_scope. + +Definition max_length := 4194303. + +Definition foo1 := (eq_refl max_length : PArray.max_length = max_length). +Definition foo2 := (eq_refl max_length <: PArray.max_length = max_length). +Definition foo3 := (eq_refl max_length <<: PArray.max_length = max_length). +Definition max_length2 := Eval compute in PArray.max_length. +Definition foo4 := (eq_refl : max_length = max_length2). +Definition max_length3 := Eval cbn in PArray.max_length. +Definition foo5 := (eq_refl : max_length = max_length3). diff --git a/test-suite/primitive/arrays/nested.v b/test-suite/primitive/arrays/nested.v new file mode 100644 index 0000000000..841cee4463 --- /dev/null +++ b/test-suite/primitive/arrays/nested.v @@ -0,0 +1,47 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Module OneLevel. + +Inductive foo : Set := + C : array foo -> foo. + +Fixpoint f1 (x : foo) {struct x} : False := + match x with + | C t => f1 (t.[0]) + end. + +Fixpoint f2 (x : foo) {struct x} : False := + f2 match x with + | C t => t.[0] + end. + +Fixpoint f3 (x : foo) {struct x} : False := + match x with + | C t => f3 (PArray.default t) + end. + +End OneLevel. + +Module TwoLevels. + +Inductive foo : Set := + C : array (array foo) -> foo. + +Fixpoint f1 (x : foo) {struct x} : False := + match x with + | C t => f1 (t.[0].[0]) + end. + +Fixpoint f2 (x : foo) {struct x} : False := + f2 match x with + | C t => t.[0].[0] + end. + +Fixpoint f3 (x : foo) {struct x} : False := + match x with + | C t => f3 (PArray.default (PArray.default t)) + end. + +End TwoLevels. diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v new file mode 100644 index 0000000000..172a118cc7 --- /dev/null +++ b/test-suite/primitive/arrays/reroot.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 5; 2 | 4 |]. +Definition t' : array nat := PArray.reroot t. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 5). +Definition foo7 := (eq_refl 5 <: t.[1] = 5). +Definition foo8 := (eq_refl 5 <<: t.[1] = 5). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 5). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 5). diff --git a/test-suite/primitive/arrays/set.v b/test-suite/primitive/arrays/set.v new file mode 100644 index 0000000000..f265c37ea8 --- /dev/null +++ b/test-suite/primitive/arrays/set.v @@ -0,0 +1,22 @@ +From Coq Require Import Int63 PArray. + +Open Scope array_scope. + +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition t' : array nat := t.[1 <- 5]. + +Definition foo1 := (eq_refl : t'.[1] = 5). +Definition foo2 := (eq_refl 5 <: t'.[1] = 5). +Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). +Definition x1 := Eval compute in t'.[1]. +Definition foo4 := (eq_refl : x1 = 5). +Definition x2 := Eval cbn in t'.[1]. +Definition foo5 := (eq_refl : x2 = 5). + +Definition foo6 := (eq_refl : t.[1] = 3). +Definition foo7 := (eq_refl 3 <: t.[1] = 3). +Definition foo8 := (eq_refl 3 <<: t.[1] = 3). +Definition x3 := Eval compute in t.[1]. +Definition foo9 := (eq_refl : x3 = 3). +Definition x4 := Eval cbn in t.[1]. +Definition foo10 := (eq_refl : x4 = 3). diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v new file mode 100644 index 0000000000..282f56267c --- /dev/null +++ b/theories/Array/PArray.v @@ -0,0 +1,122 @@ +Require Import Int63. + +Set Universe Polymorphism. + +Primitive array := #array_type. + +Primitive make : forall A, int -> A -> array A := #array_make. +Arguments make {_} _ _. + +Primitive get : forall A, array A -> int -> A := #array_get. +Arguments get {_} _ _. + +Primitive default : forall A, array A -> A:= #array_default. +Arguments default {_} _. + +Primitive set : forall A, array A -> int -> A -> array A := #array_set. +Arguments set {_} _ _ _. + +Primitive length : forall A, array A -> int := #array_length. +Arguments length {_} _. + +Primitive copy : forall A, array A -> array A := #array_copy. +Arguments copy {_} _. + +(* [reroot t] produces an array that is extensionaly equal to [t], but whose + history has been squashed. Useful when performing multiple accesses in an old + copy of an array that has been updated. *) +Primitive reroot : forall A, array A -> array A := #array_reroot. +Arguments reroot {_} _. + +Module Export PArrayNotations. + +Declare Scope array_scope. +Delimit Scope array_scope with array. +Notation "t .[ i ]" := (get t i) + (at level 2, left associativity, format "t .[ i ]"). +Notation "t .[ i <- a ]" := (set t i a) + (at level 2, left associativity, format "t .[ i <- a ]"). + +End PArrayNotations. + +Local Open Scope int63_scope. +Local Open Scope array_scope. + +Primitive max_length := #array_max_length. + +(** Axioms *) +Axiom get_out_of_bounds : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t. + +Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a. +Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j]. +Axiom default_set : forall A t i (a:A), default t.[i<-a] = default t. + + +Axiom get_make : forall A (a:A) size i, (make size a).[i] = a. + +Axiom leb_length : forall A (t:array A), length t <= max_length = true. + +Axiom length_make : forall A size (a:A), + length (make size a) = if size <= max_length then size else max_length. +Axiom length_set : forall A t i (a:A), + length t.[i<-a] = length t. + +Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i]. +Axiom length_copy : forall A (t:array A), length (copy t) = length t. + +Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i]. +Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. + +Axiom array_ext : forall A (t1 t2:array A), + length t1 = length t2 -> + (forall i, i < length t1 = true -> t1.[i] = t2.[i]) -> + default t1 = default t2 -> + t1 = t2. + +(* Lemmas *) + +Lemma default_copy A (t:array A) : default (copy t) = default t. +Proof. + assert (irr_lt : length t < length t = false). + destruct (Int63.ltbP (length t) (length t)); try reflexivity. + exfalso; eapply BinInt.Z.lt_irrefl; eassumption. + assert (get_copy := get_copy A t (length t)). + rewrite !get_out_of_bounds in get_copy; try assumption. + rewrite length_copy; assumption. +Qed. + +Lemma default_make A (a : A) size : default (make size a) = a. +Proof. + assert (irr_lt : length (make size a) < length (make size a) = false). + destruct (Int63.ltbP (length (make size a)) (length (make size a))); try reflexivity. + exfalso; eapply BinInt.Z.lt_irrefl; eassumption. + assert (get_make := get_make A a size (length (make size a))). + rewrite !get_out_of_bounds in get_make; assumption. +Qed. + +Lemma default_reroot A (t:array A) : default (reroot t) = default t. +Proof. + assert (irr_lt : length t < length t = false). + destruct (Int63.ltbP (length t) (length t)); try reflexivity. + exfalso; eapply BinInt.Z.lt_irrefl; eassumption. + assert (get_reroot := get_reroot A t (length t)). + rewrite !get_out_of_bounds in get_reroot; try assumption. + rewrite length_reroot; assumption. +Qed. + +Lemma get_set_same_default A (t : array A) (i : int) : + t.[i <- default t].[i] = default t. +Proof. + case_eq (i < length t); intros. + rewrite get_set_same; trivial. + rewrite get_out_of_bounds, default_set; trivial. + rewrite length_set; trivial. +Qed. + +Lemma get_not_default_lt A (t:array A) x : + t.[x] <> default t -> (x < length t) = true. +Proof. + intros Hd. + case_eq (x < length t); intros Heq; [trivial | ]. + elim Hd; rewrite get_out_of_bounds; trivial. +Qed. diff --git a/theories/extraction/ExtrOCamlPArray.v b/theories/extraction/ExtrOCamlPArray.v new file mode 100644 index 0000000000..67646bdb53 --- /dev/null +++ b/theories/extraction/ExtrOCamlPArray.v @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** Extraction to OCaml of persistent arrays. *) + +From Coq Require PArray Extraction. + +(** Primitive types and operators. *) +Extract Constant PArray.array "'a" => "'a Parray.t". +Extraction Inline PArray.array. +(* Otherwise, the name conflicts with the primitive OCaml type [array] *) + +Extract Constant PArray.make => "Parray.make". +Extract Constant PArray.get => "Parray.get". +Extract Constant PArray.default => "Parray.default". +Extract Constant PArray.set => "Parray.set". +Extract Constant PArray.length => "Parray.length". +Extract Constant PArray.copy => "Parray.copy". +Extract Constant PArray.reroot => "Parray.reroot". diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 4023b5a277..4cc9d99c64 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -47,6 +47,7 @@ Ltac2 Type kind := [ | Proj (projection, constr) | Uint63 (uint63) | Float (float) +| Array (instance, constr array, constr, constr) ]. Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind". diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index ef666ba9e3..cdbcc24484 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -466,6 +466,8 @@ let () = define1 "constr_kind" constr begin fun c -> v_blk 17 [|Value.of_uint63 n|] | Float f -> v_blk 18 [|Value.of_float f|] + | Array(u,t,def,ty) -> + v_blk 19 [|of_instance u; Value.of_array Value.of_constr t; Value.of_constr def; Value.of_constr ty|] end end @@ -547,6 +549,12 @@ let () = define1 "constr_make" valexpr begin fun knd -> | (18, [|f|]) -> let f = Value.to_float f in EConstr.mkFloat f + | (19, [|u;t;def;ty|]) -> + let t = Value.to_array Value.to_constr t in + let def = Value.to_constr def in + let ty = Value.to_constr ty in + let u = to_instance u in + EConstr.mkArray(u,t,def,ty) | _ -> assert false in return (Value.of_constr c) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index ef6f8652e9..f47cdd8bf0 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -155,7 +155,7 @@ let build_beq_scheme_deps kn = | None -> accu) | Rel _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | Proj _ | Construct _ | Case _ | CoFix _ | Fix _ | Meta _ | Evar _ | Int _ - | Float _ -> accu + | Float _ | Array _ -> accu in let u = Univ.Instance.empty in let constrs n = get_constructors env (make_ind_family (((kn, i), u), @@ -293,6 +293,7 @@ let build_beq_scheme mode kn = | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") | Float _ -> raise (EqUnknown "float") + | Array _ -> raise (EqUnknown "array") in aux t in diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index bcfbc049fa..110dcdc98a 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -8,30 +8,45 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let do_primitive id prim typopt = +open Names + +let declare id entry = + let _ : Constant.t = + Declare.declare_constant ~name:id ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) + in + Flags.if_verbose Feedback.msg_info Pp.(Id.print id ++ str " is declared") + +let do_primitive id udecl prim typopt = if Global.sections_are_opened () then CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; - let env = Global.env () in - let evd = Evd.from_env env in - let evd, typopt = Option.fold_left_map - Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env env) - evd typopt - in - let evd = Evd.minimize_universes evd in - let uvars, impls, typopt = match typopt with - | None -> Univ.LSet.empty, [], None - | Some (ty,impls) -> - EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in - let entry = Entries.{ - prim_entry_type = typopt; - prim_entry_univs = uctx; + let loc = id.CAst.loc in + let id = id.CAst.v in + match typopt with + | None -> + if Option.has_some udecl then + CErrors.user_err ?loc + Pp.(strbrk "Cannot use a universe declaration without a type when declaring primitives."); + declare id {Entries.prim_entry_type = None; prim_entry_content = prim} + | Some typ -> + let env = Global.env () in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in + let auctx = CPrimitives.op_or_type_univs prim in + let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in + let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in + let evd, (typ,impls) = + Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) + env evd typ + in + let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = Evd.minimize_universes evd in + let uvars = EConstr.universes_of_constr evd typ in + let evd = Evd.restrict_universe_context evd uvars in + let typ = EConstr.to_constr evd typ in + let univs = Evd.check_univ_decl ~poly:(not (Univ.AUContext.is_empty auctx)) evd udecl in + let entry = { + Entries.prim_entry_type = Some (typ,univs); prim_entry_content = prim; } - in - let _kn : Names.Constant.t = - Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in - Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared") + in + declare id entry diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli index 588eb7fdea..4d468f97b1 100644 --- a/vernac/comPrimitive.mli +++ b/vernac/comPrimitive.mli @@ -8,4 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val do_primitive : Names.lident -> CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit +val do_primitive + : Names.lident + -> Constrexpr.universe_decl_expr option + -> CPrimitives.op_or_type + -> Constrexpr.constr_expr option + -> unit diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index e1f1affb2f..e0550fd744 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -234,7 +234,7 @@ GRAMMAR EXTEND Gram { VernacRegister(g, RegisterCoqlib quid) } | IDENT "Register"; IDENT "Inline"; g = global -> { VernacRegister(g, RegisterInline) } - | IDENT "Primitive"; id = identref; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token -> + | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token -> { VernacPrimitive(id, r, typopt) } | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l } | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 7af6a6a405..cb108b68ae 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1262,7 +1262,7 @@ open Pputils ) | VernacPrimitive(id,r,typopt) -> hov 2 - (keyword "Primitive" ++ spc() ++ pr_lident id ++ + (keyword "Primitive" ++ spc() ++ pr_ident_decl id ++ (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++ str ":=" ++ spc() ++ str (CPrimitives.op_or_type_to_string r)) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b0e483ee74..6ed8c59f9f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2221,10 +2221,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtNoProof(fun () -> unsupported_attributes atts; vernac_register qid r) - | VernacPrimitive (id, prim, typopt) -> + | VernacPrimitive ((id, udecl), prim, typopt) -> VtDefault(fun () -> unsupported_attributes atts; - ComPrimitive.do_primitive id prim typopt) + ComPrimitive.do_primitive id udecl prim typopt) | VernacComments l -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 06ac7f8d48..d8e17d00e3 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -438,7 +438,7 @@ type nonrec vernac_expr = | VernacSearch of searchable * Goal_select.t option * search_restriction | VernacLocate of locatable | VernacRegister of qualid * register_kind - | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option + | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option | VernacComments of comment list (* Proof management *) |