diff options
Diffstat (limited to 'plugins')
25 files changed, 132 insertions, 52 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 52c6c5d0f9..23f8fe04a3 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -112,7 +112,7 @@ module Bool = struct else if head === negb && Array.length args = 1 then Negb (aux args.(0)) else Var (Env.add env c) - | Case (info, r, arg, pats) -> + | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in Names.eq_ind i (Lazy.force ind) 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 0f96b9bbe8..2dca1d5e49 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -291,7 +291,7 @@ let rec extract_type env sg db j c args = let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop + | _ when info_of_family (sort_of env sg (applistc c args)) == Logic -> Tdummy Kprop | Rel n -> (match EConstr.lookup_rel n env with | LocalDef (_,t,_) -> @@ -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], @@ -672,8 +672,9 @@ let rec extract_term env sg mle mlt c args = (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) in extract_app env sg mle mlt extract_rel args - | Case ({ci_ind=ip},_,c0,br) -> - extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args + | Case ({ci_ind=ip},_,iv,c0,br) -> + (* If invert_case then this is a match that will get erased later, but right now we don't care. *) + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> @@ -692,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] *) @@ -852,8 +859,8 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = end else (* [c] has an inductive type, and is not a type scheme type. *) let t = type_of env sg c in - (* The only non-informative case: [c] is of sort [Prop] *) - if (sort_of env sg t) == InProp then + (* The only non-informative case: [c] is of sort [Prop]/[SProp] *) + if info_of_family (sort_of env sg t) == Logic then begin add_recursors env kn; (* May have passed unseen if logical ... *) (* Logical singleton case: *) @@ -1016,7 +1023,7 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) let sub = List.rev_map EConstr.mkConst kns in for i = 0 to n-1 do - if sort_of env sg ti.(i) != InProp then + if info_of_family (sort_of env sg ti.(i)) != Logic then try let e,t = extract_std_constant env sg vkn.(i) (EConstr.Vars.substl sub ci.(i)) ti.(i) in @@ -1073,7 +1080,7 @@ let fake_match_projection env p = else let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in - let body = mkCase (ci, p, mkRel 1, [|branch|]) in + let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt | LocalDef (_,c,t) :: rem -> let c = liftn 1 j c in 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/firstorder/unify.ml b/plugins/firstorder/unify.ml index 9c3debe48f..c62bc73e41 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -67,10 +67,10 @@ let unif env evd t1 t2= | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige - | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> - Queue.add (pa,pb) bige; - Queue.add (ca,cb) bige; - let l=Array.length va in + | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)-> + Queue.add (pa,pb) bige; + Queue.add (ca,cb) bige; + let l=Array.length va in if not (Int.equal l (Array.length vb)) then raise (UFAIL (nt1,nt2)) else diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9b578d4697..14d0c04212 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos let sigma = project g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with - | Case (ci, ct, t, cb) -> + | Case (ci, ct, iv, t, cb) -> let do_finalize_t dyn_info' g = let t = dyn_info'.info in - let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in + let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in let g_nb_prod = nb_prod (project g) (pf_concl g) in let g, type_of_term = tac_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -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 167cf37026..ffce2f8c85 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -70,7 +70,7 @@ let build_newrecursive lnameargsardef = CErrors.user_err ~hdr:"Function" (Pp.str "Body of Function must be given") in - States.with_state_protection (List.map f) lnameargsardef + Vernacstate.System.protect (List.map f) lnameargsardef in (recdef, rec_impls) @@ -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 @@ -987,7 +989,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = ( UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type" )) -> Proofview.V82.of_tactic tauto g - | Case (_, _, v, _) -> + | Case (_, _, _, v, _) -> tclTHENLIST [Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite] g @@ -1026,7 +1028,7 @@ let rec reflexivity_with_destruct_cases g = match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with - | Case (_, _, v, _) -> + | Case (_, _, _, v, _) -> tclTHENLIST [ Proofview.V82.of_tactic (simplest_case v) ; Proofview.V82.of_tactic intros @@ -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 884792cc15..64f62ba1fb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,14 +305,16 @@ 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 _ -> () | Construct _ -> () - | Case (_, t, e, a) -> + | Case (_, t, _, e, a) -> check_not_nested t; check_not_nested e; Array.iter check_not_nested a @@ -374,7 +376,13 @@ type journey_info = ; lambdA : (Name.t * types * constr, constr) journey_info_tac ; casE : ((constr infos -> tactic) -> constr infos -> tactic) - -> (case_info * constr * constr * constr array, constr) journey_info_tac + -> ( case_info + * constr + * (constr, EInstance.t) case_invert + * constr + * constr array + , constr ) + journey_info_tac ; otherS : (unit, constr) journey_info_tac ; apP : (constr * constr list, constr) journey_info_tac ; app_reC : (constr * constr list, constr) journey_info_tac @@ -441,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 = @@ -474,9 +483,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id ) ) - | Case (ci, t, a, l) -> + | Case (ci, t, iv, a, l) -> let continuation_tac_a = - jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac + jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac in travel jinfo continuation_tac_a {expr_info with info = a; is_main_branch = false; is_final = false} @@ -767,7 +776,8 @@ let mkDestructEq not_on_hyp expr g = in (g, tac, to_revert) -let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g = +let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos + g = let sigma = project g in let env = pf_env g in let f_is_present = @@ -779,7 +789,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g = let a' = infos.info in let new_info = { infos with - info = mkCase (ci, t, a', l) + info = mkCase (ci, t, iv, a', l) ; is_main_branch = expr_info.is_main_branch ; is_final = expr_info.is_final } in @@ -916,10 +926,10 @@ let prove_terminate = travel terminate_info (* Equation proof *) -let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos = +let equation_case next_step case expr_info continuation_tac infos = observe_tac (fun _ _ -> str "equation case") - (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos) + (terminate_case next_step case expr_info continuation_tac infos) let rec prove_le g = let sigma = project g in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 40c64a1c26..66c72a30a2 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -776,7 +776,7 @@ let rec find_a_destructable_match sigma t = let cl = [cl, (None, None), None], None in let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in match EConstr.kind sigma t with - | Case (_,_,x,_) when closed0 sigma x -> + | Case (_,_,_,x,_) when closed0 sigma x -> if isVar sigma x then (* TODO check there is no rel n. *) raise (Found (Tacinterp.eval_tactic dest)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 40dea90c00..fb149071c9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -923,8 +923,8 @@ let reset_env env = let env' = Global.env_of_context (Environ.named_context_val env) in Environ.push_rel_context (Environ.rel_context env) env' -let fold_match env sigma c = - let (ci, p, c, brs) = destCase sigma c in +let fold_match ?(force=false) env sigma c = + let (ci, p, iv, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in let dep, pred, exists, sk = let env', ctx, body = @@ -1184,7 +1184,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> b' in state, res - | Case (ci, p, c, brs) -> + | Case (ci, p, iv, c, brs) -> let cty = Retyping.get_type_of env (goalevars evars) c in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in @@ -1194,7 +1194,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let state, res = match c' with | Success r -> - let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in + let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in state, Success (coerce env unfresh (prop,cstr) res) | Fail | Identity -> @@ -1216,7 +1216,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in match found with | Some r -> - let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' c'))) in + let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in state, Success (make_leibniz_proof env ctxc ty r) | None -> state, c' else diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index e6c59f446d..f8c25d5dd0 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -489,7 +489,7 @@ let register_ltac local ?deprecation tacl = in (* STATE XXX: Review what is going on here. Why does this needs protection? Why is not the STM level protection enough? Fishy *) - let defs = States.with_state_protection defs () in + let defs = Vernacstate.System.protect defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac ?deprecation; diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 878f7a834e..95faede7d0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -77,7 +77,7 @@ let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in let c = EConstr.Unsafe.to_constr c0 in let tab = create_tab () in - let infos = create_clos_infos ~evars all env in + let infos = create_clos_infos ~univs:(Evd.universes sigma) ~evars all env in let map = lookup_map map sigma c0 in let rec eval n c = match Constr.kind c with | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5f463f8de4..65204b7868 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1351,9 +1351,8 @@ let unsafe_intro env decl b = let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in let ninst = EConstr.mkRel 1 :: inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in - let sigma, ev = - Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in - sigma, EConstr.mkNamedLambda_or_LetIn decl ev + let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in + sigma, EConstr.mkNamedLambda_or_LetIn decl (EConstr.mkEvar (ev, ninst)) end let set_decl_id id = let open Context in function diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5d6e7c51d0..5dedae6388 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -308,10 +308,11 @@ let iter_constr_LR f c = match kind c with | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b | LetIn (_, v, t, b) -> f v; f t; f b | App (cf, a) -> f cf; Array.iter f a - | Case (_, p, v, b) -> f v; f p; Array.iter f b + | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b | 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 _) -> () @@ -859,7 +860,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -867,11 +868,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg index f5cbf2005b..5e002e09cc 100644 --- a/plugins/ssrsearch/g_search.mlg +++ b/plugins/ssrsearch/g_search.mlg @@ -59,7 +59,7 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let trim_ntn (pntn, m) = (InConstrEntry,Bytes.sub_string pntn 1 (max 0 m)) in let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x |