diff options
Diffstat (limited to 'plugins')
40 files changed, 324 insertions, 1435 deletions
diff --git a/plugins/.merlin b/plugins/.merlin index dd6678ba09..2ba6169622 100644 --- a/plugins/.merlin +++ b/plugins/.merlin @@ -1,2 +1 @@ REC -FLG -open API diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index fb65a8639a..c8c4c2dad9 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -38,9 +38,8 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> + let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4ae875cd70..c169b7b50b 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -431,7 +431,7 @@ and extract_really_ind env kn mib = let ip = (kn, 0) in let r = IndRef ip in if is_custom r then raise (I Standard); - if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive); + if mib.mind_finite == CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); let p,u = packets.(0) in if p.ip_logical then raise (I Standard); diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 23452febdc..24c70bccfb 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id END let pr_language = function - | Ocaml -> str "Ocaml" + | Ocaml -> str "OCaml" | Haskell -> str "Haskell" | Scheme -> str "Scheme" | JSON -> str "JSON" +let warn_deprecated_ocaml_spelling = + CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" + (fun () -> + strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) + VERNAC ARGUMENT EXTEND language PRINTED BY pr_language -| [ "Ocaml" ] -> [ Ocaml ] +| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] +| [ "OCaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] | [ "JSON" ] -> [ JSON ] diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index c55040df03..4c59996aa7 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -55,7 +55,8 @@ let ind_hyps env sigma nevar ind largs = let types= Inductiveops.arities_of_constructors env ind in let myhyps t = let t = EConstr.of_constr t in - let t1=Termops.prod_applist sigma t largs in + let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in + let t1=Termops.prod_applist_assum sigma nparam_decls t largs in let t2=snd (decompose_prod_n_assum sigma nevar t1) in fst (decompose_prod_assum sigma t2) in Array.map myhyps types diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b9..b81010c7bd 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 62ca706264..d04887a489 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -324,7 +324,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = context in let new_type_of_hyp = - Reductionops.nf_betaiota sigma new_type_of_hyp in + Reductionops.nf_betaiota env sigma new_type_of_hyp in let new_ctxt,new_end_of_type = decompose_prod_n_assum sigma ctxt_size new_type_of_hyp in @@ -698,6 +698,7 @@ let build_proof : tactic = let rec build_proof_aux do_finalize dyn_infos : tactic = fun g -> + let env = pf_env g in 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 @@ -794,7 +795,7 @@ let build_proof do_finalize dyn_infos g | Lambda _ -> let new_term = - Reductionops.nf_beta sigma dyn_infos.info in + Reductionops.nf_beta env sigma dyn_infos.info in build_proof do_finalize {dyn_infos with info = new_term} g | LetIn _ -> @@ -1153,7 +1154,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let bodies_with_all_params = Array.map (fun body -> - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body, List.rev_map var_of_decl princ_params)) ) @@ -1191,12 +1192,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let body_with_param,num = let body = get_body fnames.(i) in let body_with_full_params = - Reductionops.nf_betaiota (project g) ( + Reductionops.nf_betaiota (pf_env g) (project g) ( applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with | Fix((_,num),(_,_,bs)) -> - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) ( (applist (substl @@ -1279,7 +1280,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) (applist(fix_body,List.rev_map mkVar args_id)); eq_hyps = [] } @@ -1339,7 +1340,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota Evd.empty + Reductionops.nf_betaiota (pf_env g) Evd.empty (applist(fbody_with_full_params, (List.rev_map var_of_decl princ_params)@ (List.rev_map mkVar args_id) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index a3315f22cf..ad396a2cbb 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -29,10 +29,6 @@ val generate_functional_principle : (EConstr.constr array -> int -> Tacmach.tactic) -> unit -val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> - types -> types - - exception No_graph_found val make_scheme : Evd.evar_map ref -> diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 87609296bc..4b828a7022 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) + (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa43536304..f7639d22d6 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProj _ -> user_err Pp.(str "Funind does not support primitive projections") | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) @@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b + | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections") and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : @@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GProj _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = @@ -1497,8 +1499,8 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) - Decl_kinds.Finite + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1509,7 +1511,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1526,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0666ab4f1f..b4ca1073ca 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -17,69 +17,12 @@ let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = DAst.make @@ GSort(s) let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = DAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -let glob_decompose_prod = - let rec glob_decompose_prod args c = match DAst.get c with - | GProd(n,k,t,b) -> - glob_decompose_prod ((n,t)::args) b - | _ -> args,c - in - glob_decompose_prod [] - -let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args rt = match DAst.get rt with - | GProd(n,k,t,b) -> - glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(n,b,t,c) -> - glob_decompose_prod ((n,Some b,t)::args) c - | _ -> args,rt - in - glob_decompose_prod [] - -let glob_compose_prod = - List.fold_left (fun b (n,t) -> mkGProd(n,t,b)) - -let glob_compose_prod_or_letin = - List.fold_left ( - fun concl decl -> - match decl with - | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) - | _ -> assert false) - -let glob_decompose_prod_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match DAst.get c with - | GProd(n,_,t,b) -> - glob_decompose_prod (i-1) ((n,t)::args) b - | _ -> args,c - in - glob_decompose_prod n [] - - -let glob_decompose_prod_or_letin_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match DAst.get c with - | GProd(n,_,t,b) -> - glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(n,b,t,c) -> - glob_decompose_prod (i-1) ((n,Some b,t)::args) c - | _ -> args,c - in - glob_decompose_prod n [] - - let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) @@ -101,18 +44,6 @@ let glob_make_eq ?(typ= mkGHole ()) t1 t2 = let glob_make_neq t1 t2 = mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -let rec glob_make_or_list = function - | [] -> invalid_arg "mk_or" - | [e] -> e - | e::l -> glob_make_or e (glob_make_or_list l) - - let remove_name_from_mapping mapping na = match na with | Anonymous -> mapping @@ -178,6 +109,7 @@ let change_vars = | GCast(b,c) -> GCast(change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) + | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ((loc,(idl,patl,res)) as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -362,6 +294,7 @@ let rec alpha_rt excluded rt = GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) + | GProj(p,c) -> GProj(p, alpha_rt excluded c) in new_rt @@ -413,6 +346,7 @@ 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 + | GProj (_,c) -> is_free_in c ) x and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt @@ -506,6 +440,8 @@ let replace_var_by_term x_id term = | GCast(b,c) -> GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) + | GProj(p,c) -> + GProj(p,replace_var_by_pattern c) ) x and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -575,97 +511,6 @@ let ids_of_pat = in ids_of_pat Id.Set.empty -let id_of_name = function - | Anonymous -> Id.of_string "x" - | Name x -> x - -(* TODO: finish Rec caes *) -let ids_of_glob_constr c = - let rec ids_of_glob_constr acc c = - let idof = id_of_name in - match DAst.get c with - | GVar id -> id::acc - | GApp (g,args) -> - ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc - | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc - | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc - | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc - | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc - | GLetTuple (nal,(na,po),b,c) -> - List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCases (sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl) - | GRec _ -> failwith "Fix inside a constructor branch" - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] - in - (* build the set *) - List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c) - - - - - -let zeta_normalize = - let rec zeta_normalize_term x = DAst.map (function - | GRef _ - | GVar _ - | GEvar _ - | GPatVar _ as rt -> rt - | GApp(rt',rtl) -> - GApp(zeta_normalize_term rt', - List.map zeta_normalize_term rtl - ) - | GLambda(name,k,t,b) -> - GLambda(name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GProd(name,k,t,b) -> - GProd(name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GLetIn(Name id,def,typ,b) -> - DAst.get (zeta_normalize_term (replace_var_by_term id def b)) - | GLetIn(Anonymous,def,typ,b) -> - DAst.get (zeta_normalize_term b) - | GLetTuple(nal,(na,rto),def,b) -> - GLetTuple(nal, - (na,Option.map zeta_normalize_term rto), - zeta_normalize_term def, - zeta_normalize_term b - ) - | GCases(sty,infos,el,brl) -> - GCases(sty, - infos, - List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, - List.map zeta_normalize_br brl - ) - | GIf(b,(na,e_option),lhs,rhs) -> - GIf(zeta_normalize_term b, - (na,Option.map zeta_normalize_term e_option), - zeta_normalize_term lhs, - zeta_normalize_term rhs - ) - | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ - | GHole _ as rt -> rt - | GCast(b,c) -> - GCast(zeta_normalize_term b, - Miscops.map_cast_type zeta_normalize_term c) - ) x - and zeta_normalize_br (loc,(idl,patl,res)) = - (loc,(idl,patl,zeta_normalize_term res)) - in - zeta_normalize_term - - - - let expand_as = let rec add_as map rt = @@ -700,6 +545,7 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(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) + | GProj(p,c) -> GProj(p, expand_as map c) ) and expand_as_br map (loc,(idl,cpl,rt)) = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 99a258de98..7088ae596b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,6 +1,5 @@ open Names open Glob_term -open Misctypes (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) val get_pattern_id : cases_pattern -> Id.t list @@ -21,22 +20,11 @@ val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr -val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) -val mkGCast : glob_constr* glob_constr -> glob_constr (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin : - glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr -val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin_n : int -> glob_constr -> - (Name.t*glob_constr option*glob_constr option) list * glob_constr -val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list -> glob_constr -val glob_compose_prod_or_letin: glob_constr -> - (Name.t*glob_constr option*glob_constr option) list -> glob_constr val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) @@ -44,14 +32,6 @@ val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) val glob_make_neq : glob_constr -> glob_constr -> glob_constr -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -val glob_make_or : glob_constr -> glob_constr -> glob_constr - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -val glob_make_or_list : glob_constr list -> glob_constr - (* alpha_conversion functions *) @@ -109,18 +89,8 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool *) val ids_of_pat : cases_pattern -> Id.Set.t -(* TODO: finish this function (Fix not treated) *) -val ids_of_glob_constr: glob_constr -> Id.Set.t - -(* - removing let_in construction in a glob_constr -*) -val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr - - val expand_as : glob_constr -> glob_constr - (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution *) val resolve_and_replace_implicits : diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad3063..58154d3106 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in - let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -215,6 +215,7 @@ let is_rec names = | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl + | GProj(_,c) -> lookup names c and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -282,7 +283,6 @@ let derive_inversion fix_names = in Invfun.derive_correctness Functional_principles_types.make_scheme - functional_induction fix_names_as_constant lind; with e when CErrors.noncritical e -> @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = @@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") + | CProj _ -> user_err Pp.(str "Funind does not support primitive projections") ) exception Stop of Constrexpr.constr_expr diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8bf6e48fdb..d6fd2f2a0f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -183,12 +183,13 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; - Impargs.make_contextual_implicit_args false; Dumpglob.pause (); try let res = f a in @@ -197,6 +198,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +208,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 694c800514..4acf82d000 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -56,12 +56,6 @@ let do_observe_tac s tac g = CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; - -let observe_tac_strm s tac g = - if do_observe () - then do_observe_tac s tac g - else tac g - let observe_tac s tac g = if do_observe () then do_observe_tac (str s) tac g @@ -87,10 +81,6 @@ let make_eq () = try EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) with _ -> assert false -let make_eq_refl () = - try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) - with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -194,10 +184,9 @@ let rec generate_fresh_id x avoid i = id::(generate_fresh_id x (id::avoid) (pred i)) -(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] +(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. - [functional_induction] is the tactic defined in [indfun] (dependency problem) [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. graphs of the functions and principles and correctness lemma types) to prove correct. @@ -218,7 +207,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = +let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -752,14 +741,13 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti g -(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness +(* [derive_correctness make_scheme funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and - [functional_induction] is Indfun.functional_induction (same pb) *) -let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) = +let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) = assert (funs <> []); assert (graphs <> []); let funs = Array.of_list funs and graphs = Array.of_list graphs in @@ -809,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( ) in let proving_tac = - prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos + prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli new file mode 100644 index 0000000000..e07138596c --- /dev/null +++ b/plugins/funind/invfun.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val invfun : + Misctypes.quantified_hypothesis -> + Globnames.global_reference option -> + Evar.t Evd.sigma -> Evar.t list Evd.sigma +val derive_correctness : + (Evd.evar_map ref -> + (Constr.pconstant * Sorts.family) list -> + 'a Entries.definition_entry list) -> + Constr.pconstant list -> Names.inductive list -> unit diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml deleted file mode 100644 index 9e2774ff32..0000000000 --- a/plugins/funind/merge.ml +++ /dev/null @@ -1,1013 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Merging of induction principles. *) - -open Globnames -open Tactics -open Indfun_common -open CErrors -open Util -open Constrexpr -open Vernacexpr -open Pp -open Names -open Term -open Constr -open Vars -open Declarations -open Glob_term -open Glob_termops -open Decl_kinds -open Context.Rel.Declaration - -module RelDecl = Context.Rel.Declaration - -(** {1 Utilities} *) - -(** {2 Useful operations on constr and glob_constr} *) - -let pop c = Vars.lift (-1) c -let rec popn i c = if i<=0 then c else pop (popn (i-1) c) - -(** Substitutions in constr *) -let compare_constr_nosub t1 t2 = - if Constr.compare_head (fun _ _ -> false) t1 t2 - then true - else false - -let rec compare_constr' t1 t2 = - if compare_constr_nosub t1 t2 - then true - else (Constr.compare_head (compare_constr') t1 t2) - -let rec substitterm prof t by_t in_u = - if (compare_constr' (lift prof t) in_u) - then (lift prof by_t) - else Constr.map_with_binders succ - (fun i -> substitterm i t by_t) prof in_u - -let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl - -let understand = Pretyping.understand (Global.env()) Evd.empty - -(** Operations on names and identifiers *) -let id_of_name = function - Anonymous -> Id.of_string "H" - | Name id -> id;; -let name_of_string = Id.of_string %> Name.mk_name -let string_of_name = id_of_name %> Id.to_string - -(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) -let isVarf f x = - match DAst.get x with - | GVar x -> Id.equal x f - | _ -> false - -(** [ident_global_exist id] returns true if identifier [id] is linked - in global environment. *) -let ident_global_exist id = - try - let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in - let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in - true - with e when CErrors.noncritical e -> false - -(** [next_ident_fresh id] returns a fresh identifier (ie not linked in - global env) with base [id]. *) -let next_ident_fresh (id:Id.t) = - let res = ref id in - while ident_global_exist !res do res := Nameops.increment_subscript !res done; - !res - - -(** {2 Debugging} *) -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" -(* uncomment this to see debugging *) -let prconstr c = - let sigma, env = Pfedit.get_current_context () in - msg (str" " ++ Printer.pr_lconstr_env env sigma c) - -let prconstrnl c = - let sigma, env = Pfedit.get_current_context () in - msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") - -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - let sigma, env = Pfedit.get_current_context () in - begin - msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); - msg(str ""); - end -let prNamedRConstr s c = - let sigma, env = Pfedit.get_current_context () in - begin - msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); - msg(str ""); - end -let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc -let prNamedLConstr s lc = - begin - prstr "[§§§ "; - prstr s; - prNamedLConstr_aux lc; - prstr " §§§]\n"; - end -let prNamedLDecl s lc = - begin - prstr s; prstr "\n"; - List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc; - prstr "\n"; - end -let prNamedRLDecl s lc = - begin - prstr s; prstr "\n"; prstr "{§§ "; - List.iter - (fun x -> - match x with - | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp - | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy - | _ -> assert false - ) lc; - prstr " §§}\n"; - prstr "\n"; - end - -(** {2 Misc} *) - -exception Found of int - -(* Array scanning *) - -let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int = -match Array.findi pred arr with -| None -> Array.length arr (* all elt are positive *) -| Some i -> i - -(* Like List.chop but except that [i] is the size of the suffix of [l]. *) -let list_chop_end i l = - let size_prefix = List.length l -i in - if size_prefix < 0 then failwith "list_chop_end" - else List.chop size_prefix l - -let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = - let i = ref 0 in - List.fold_left - (fun acc x -> - let res = f !i acc x in i := !i + 1; res) - acc arr - -let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = - let i = ref 0 in - List.filter (fun x -> let res = f !i x in i := !i + 1; res) l - - -(** Iteration module *) -module For = -struct - let rec map i j (f: int -> 'a) = if i>j then [] else f i :: (map (i+1) j f) - let rec foldup i j (f: 'a -> int -> 'a) acc = - if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc - let rec folddown i j (f: 'a -> int -> 'a) acc = - if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc - let fold i j = if i<j then foldup i j else folddown i j -end - - -(** {1 Parameters shifting and linking information} *) - -(** This type is used to deal with debruijn linked indices. When a - variable is linked to a previous one, we will ignore it and refer - to previous one. *) -type linked_var = - | Linked of int - | Unlinked - | Funres - -(** When merging two graphs, parameters may become regular arguments, - and thus be shifted. This type describes the result of computing - the changes. *) -type 'a shifted_params = - { - nprm1:'a; - nprm2:'a; - prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *) - nuprm1:'a; - nuprm2:'a; - nargs1:'a; - nargs2:'a; - } - - -let prlinked x = - match x with - | Linked i -> Printf.sprintf "Linked %d" i - | Unlinked -> Printf.sprintf "Unlinked" - | Funres -> Printf.sprintf "Funres" - -let linkmonad f lnkvar = - match lnkvar with - | Linked i -> Linked (f i) - | Unlinked -> Unlinked - | Funres -> Funres - -let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar - -(* This map is used to deal with debruijn linked indices. *) -module Link = Map.Make (Int) - -let pr_links l = - Printf.printf "links:\n"; - Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l; - Printf.printf "_____________\n" - -type 'a merged_arg = - | Prm_stable of 'a - | Prm_linked of 'a - | Prm_arg of 'a - | Arg_stable of 'a - | Arg_linked of 'a - | Arg_funres - -(** Information about graph merging of two inductives. - All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *) - -type merge_infos = - { - ident:Id.t; (** new inductive name *) - mib1: mutual_inductive_body; - oib1: one_inductive_body; - mib2: mutual_inductive_body; - oib2: one_inductive_body; - - (** Array of links of the first inductive (should be all stable) *) - lnk1: int merged_arg array; - - (** Array of links of the second inductive (point to the first ind param/args) *) - lnk2: int merged_arg array; - - (** rec params which remain rec param (ie not linked) *) - recprms1: Context.Rel.Declaration.t list; - recprms2: Context.Rel.Declaration.t list; - nrecprms1: int; - nrecprms2: int; - - (** rec parms which became non parm (either linked to something - or because after a rec parm that became non parm) *) - otherprms1: Context.Rel.Declaration.t list; - otherprms2: Context.Rel.Declaration.t list; - notherprms1:int; - notherprms2:int; - - (** args which remain args in merge *) - args1:Context.Rel.Declaration.t list; - args2:Context.Rel.Declaration.t list; - nargs1:int; - nargs2:int; - - (** functional result args *) - funresprms1: Context.Rel.Declaration.t list; - funresprms2: Context.Rel.Declaration.t list; - nfunresprms1:int; - nfunresprms2:int; - } - - -let pr_merginfo x = - let i,s= - match x with - | Prm_linked i -> Some i,"Prm_linked" - | Arg_linked i -> Some i,"Arg_linked" - | Prm_stable i -> Some i,"Prm_stable" - | Prm_arg i -> Some i,"Prm_arg" - | Arg_stable i -> Some i,"Arg_stable" - | Arg_funres -> None , "Arg_funres" in - match i with - | Some i -> Printf.sprintf "%s(%d)" s i - | None -> Printf.sprintf "%s" s - -let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false - -(* ?? prm_linked?? *) -let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false - -let is_stable x = - match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false - -let isArg_funres x = match x with Arg_funres -> true | _ -> false - -let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list = - let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in - let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in - let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in - prms@args@fres - -(** Reverse the link map, keeping only linked vars, elements are list - of int as several vars may be linked to the same var. *) -let revlinked lnk = - For.fold 0 (Array.length lnk - 1) - (fun acc k -> - match lnk.(k) with - | Unlinked | Funres -> acc - | Linked i -> - let old = try Link.find i acc with Not_found -> [] in - Link.add i (k::old) acc) - Link.empty - -let array_switch arr i j = - let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux - -let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = - let larr = Array.of_list l in - let _ = - Array.iteri - (fun j x -> - match x with - | Prm_linked i -> array_switch larr i j - | Arg_linked i -> array_switch larr i j - | Prm_stable i -> () - | Prm_arg i -> () - | Arg_stable i -> () - | Arg_funres -> () - ) lnk in - filter_shift_stable lnk (Array.to_list larr) - - -let error msg = user_err Pp.(str msg) - -(** {1 Utilities for merging} *) - -let ind1name = Id.of_string "__ind1" -let ind2name = Id.of_string "__ind2" - -(** Performs verifications on two graphs before merging: they must not - be co-inductive, and for the moment they must not be mutual - either. *) -let verify_inds mib1 mib2 = - if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; - if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; - if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; - if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; - () - -(* -(** [build_raw_params prms_decl avoid] returns a list of variables - attributed to the list of decl [prms_decl], avoiding names in - [avoid]. *) -let build_raw_params prms_decl avoid = - let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in - let _ = prNamedConstr "DUMMY" dummy_constr in - let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in - let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in - let res,_ = glob_decompose_prod dummy_glob_constr in - let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr))) -*) - -let ids_of_rawlist avoid rawl = - List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl) - - - -(** {1 Merging function graphs} *) - -(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec - uniform and ordinary ones) of mutual inductives [mib1] and [mib2] - remain uniform when linked by [lnk]. All parameters are - considered, ie we take parameters of the first inductive body of - [mib1] and [mib2]. - - Explanation: The two inductives have parameters, some of the first - are recursively uniform, some of the last are functional result of - the functional graph. - - (I x1 x2 ... xk ... xk' ... xn) - (J y1 y2 ... xl ... yl' ... ym) - - Problem is, if some rec unif params are linked to non rec unif - ones, they become non rec (and the following too). And functinal - argument have to be shifted at the end *) -let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id = - let _ = prstr "\nYOUHOU shift\n" in - let linked_targets = revlinked lnk2 in - let is_param_of_mib1 x = x < mib1.mind_nparams_rec in - let is_param_of_mib2 x = x < mib2.mind_nparams_rec in - let is_targetted_by_non_recparam_lnk1 i = - try - let targets = Link.find i linked_targets in - List.exists (fun x -> not (is_param_of_mib2 x)) targets - with Not_found -> false in - let mlnk1 = - Array.mapi - (fun i lkv -> - let isprm = is_param_of_mib1 i in - let prmlost = is_targetted_by_non_recparam_lnk1 i in - match isprm , prmlost, lnk1.(i) with - | true , true , _ -> Prm_arg i (* recparam becoming ordinary *) - | true , false , _-> Prm_stable i (* recparam remains recparam*) - | false , false , Funres -> Arg_funres - | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *) - | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *) - lnk1 in - let mlnk2 = - Array.mapi - (fun i lkv -> - (* Is this correct if some param of ind2 is lost? *) - let isprm = is_param_of_mib2 i in - match isprm , lnk2.(i) with - | true , Linked j when not (is_param_of_mib1 j) -> - Prm_arg j (* recparam becoming ordinary *) - | true , Linked j -> Prm_linked j (*recparam linked to recparam*) - | true , Unlinked -> Prm_stable i (* recparam remains recparam*) - | false , Linked j -> Arg_linked j (* Args of lnk2 lost *) - | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *) - | false , Funres -> Arg_funres - | true , Funres -> assert false (* fun res cannot be a rec param *) - ) - lnk2 in - let oib1 = mib1.mind_packets.(0) in - let oib2 = mib2.mind_packets.(0) in - (* count params remaining params *) - let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in - let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in - let bldprms arity_ctxt mlnk = - list_fold_lefti - (fun i (acc1,acc2,acc3,acc4) x -> - prstr (pr_merginfo mlnk.(i));prstr "\n"; - match mlnk.(i) with - | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4 - | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4 - | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4 - | Arg_funres -> acc1 , acc2 , acc3, x::acc4 - | _ -> acc1 , acc2 , acc3, acc4) - ([],[],[],[]) arity_ctxt in -(* let arity_ctxt2 = - build_raw_params oib2.mind_arity_ctxt - (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) - let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in - let _ = prstr "\n\n\n" in - let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in - let _ = prstr "\notherprms1:\n" in - let _ = - List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); - prconstr (RelDecl.get_type decl); prstr "\n") - otherprms1 in - let _ = prstr "\notherprms2:\n" in - let _ = - List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n") - otherprms2 in - { - ident=id; - mib1=mib1; - oib1 = oib1; - mib2=mib2; - oib2 = oib2; - lnk1 = mlnk1; - lnk2 = mlnk2; - nrecprms1 = n_params1; - recprms1 = recprms1; - otherprms1 = otherprms1; - args1 = args1; - funresprms1 = funresprms1; - notherprms1 = Array.length mlnk1 - n_params1; - nfunresprms1 = List.length funresprms1; - nargs1 = List.length args1; - nrecprms2 = n_params2; - recprms2 = recprms2; - otherprms2 = otherprms2; - args2 = args2; - funresprms2 = funresprms2; - notherprms2 = Array.length mlnk2 - n_params2; - nargs2 = List.length args2; - nfunresprms2 = List.length funresprms2; - } - - - - -(** {1 Merging functions} *) - -exception NoMerge - -let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = - let lnk = Array.append shift.lnk1 shift.lnk2 in - match DAst.get c1, DAst.get c2 with - | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> - let _ = prstr "\nICI1!\n" in - let args = filter_shift_stable lnk (arr1 @ arr2) in - DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args) - | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge - | GLetIn(nme,bdy,typ,trm) , _ -> - let _ = prstr "\nICI2!\n" in - let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _, GLetIn(nme,bdy,typ,trm) -> - let _ = prstr "\nICI3!\n" in - let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _ -> let _ = prstr "\nICI4!\n" in - raise NoMerge - -let rec merge_app_unsafe c1 c2 shift filter_shift_stable = - let lnk = Array.append shift.lnk1 shift.lnk2 in - match DAst.get c1, DAst.get c2 with - | GApp(f1, arr1), GApp(f2,arr2) -> - let args = filter_shift_stable lnk (arr1 @ arr2) in - DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args) - (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(nme,bdy,typ,trm) , _ -> - let _ = prstr "\nICI2 '!\n" in - let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _, GLetIn(nme,bdy,typ,trm) -> - let _ = prstr "\nICI3 '!\n" in - let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge - - - -(* Heuristic when merging two lists of hypothesis: merge every rec - calls of branch 1 with all rec calls of branch 2. *) -(* TODO: reecrire cette heuristique (jusqu'a merge_types) *) -let rec merge_rec_hyps shift accrec - (ltyp:(Name.t * glob_constr option * glob_constr option) list) - filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = - let is_app c = match DAst.get c with GApp _ -> true | _ -> false in - let mergeonehyp t reldecl = - match reldecl with - | (nme,x,Some ind) when is_app ind - -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) - | (nme,Some _,None) -> error "letins with recursive calls not treated yet" - | (nme,None,Some _) -> assert false - | (nme,None,None) | (nme,Some _,Some _) -> assert false in - let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in - match ltyp with - | [] -> [] - | (nme,None,Some t) :: lt when is_app t -> - let rechyps = List.map (mergeonehyp t) accrec in - rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable - | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable - - -let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = - List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec - - -let find_app (nme:Id.t) ltyp = - let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in - try - ignore - (List.map - (fun x -> - match x with - | _,None,Some c when is_app c -> raise (Found 0) - | _ -> ()) - ltyp); - false - with Found _ -> true - -let prnt_prod_or_letin nm letbdy typ = - match letbdy , typ with - | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy - | None , Some tp -> prNamedRConstr (string_of_name nm) tp - | _ , _ -> assert false - - -let rec merge_types shift accrec1 - (ltyp1:(Name.t * glob_constr option * glob_constr option) list) - (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2 - : (Name.t * glob_constr option * glob_constr option) list * glob_constr = - let _ = prstr "MERGE_TYPES\n" in - let _ = prstr "ltyp 1 : " in - let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in - let _ = prstr "\nltyp 2 : " in - let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in - let _ = prstr "\n" in - let res = - match ltyp1 with - | [] -> - let isrec1 = not (List.is_empty accrec1) in - let isrec2 = find_app ind2name ltyp2 in - let rechyps = - if isrec1 && isrec2 - then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *) - merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 - filter_shift_stable_right - @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2] - filter_shift_stable - else if isrec1 - (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *) - then - merge_rec_hyps shift accrec1 - (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable - else if isrec2 - then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 - filter_shift_stable_right - else ltyp2 in - let _ = prstr"\nrechyps : " in - let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in - let _ = prstr "MERGE CONCL : " in - let _ = prNamedRConstr "concl1" concl1 in - let _ = prstr " with " in - let _ = prNamedRConstr "concl2" concl2 in - let _ = prstr "\n" in - let concl = - merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in - let _ = prstr "FIN " in - let _ = prNamedRConstr "concl" concl in - let _ = prstr "\n" in - - rechyps , concl - | (nme,None, Some t1)as e ::lt1 -> - (match DAst.get t1 with - | GApp(f,carr) when isVarf ind1name f -> - merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 - | _ -> - let recres, recconcl2 = - merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,None,Some t1) :: recres) , recconcl2) - | (nme,Some bd, None) ::lt1 -> - (* FIXME: what if ind1name appears in bd? *) - let recres, recconcl2 = - merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,Some bd,None) :: recres) , recconcl2 - | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false - in - res - - -(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of - linked args [allargs2] to target args of [allargs1] as specified - in [shift]. [allargs1] and [allargs2] are in reverse order. Also - returns the list of unlinked vars of [allargs2]. *) -let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array) - (lnk:int merged_arg array) = - Array.fold_left_i - (fun i acc e -> - if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *) - else - match e with - | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc - | _ -> acc) - Id.Map.empty lnk - -let build_link_map allargs1 allargs2 lnk = - let allargs1 = - Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in - let allargs2 = - Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs2) in - build_link_map_aux allargs1 allargs2 lnk - - -(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two - constructor rawtypes [typcstr1] and [typcstr2]. [typcstr1] and - [typcstr2] contain all parameters (including rec. unif. ones) of - their inductive. - - if [typcstr1] and [typcstr2] are of the form: - - forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1) - forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2) - - we build: - - forall recparams1 (recparams2 without linked params), - forall ordparams1 (ordparams2 without linked params), - H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... - -> (newI x1 ... z1 x2 y2 ...z2 without linked params) - - where Hix' have been adapted, ie: - - linked vars have been changed, - - rec calls to I1 and I2 have been replaced by rec calls to - newI. More precisely calls to I1 and I2 have been merge by an - experimental heuristic (in particular if n o rec calls for I1 - or I2 is found, we use the conclusion as a rec call). See - [merge_types] above. - - Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint. - - TODO: return nothing if equalities (after linking) are contradictory. *) -let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr) - (typcstr2:glob_constr) : glob_constr = - (* FIXME: les noms des parametres corerspondent en principe au - parametres du niveau mib, mais il faudrait s'en assurer *) - (* shift.nfunresprmsx last args are functional result *) - let nargs1 = - shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in - let nargs2 = - shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in - let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in - let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in - (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) - let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in - let rest2 = change_vars linked_map rest2 in - let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in - let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in - let ltyp,concl2 = - merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in - let _ = prNamedRLDecl "ltyp result:" ltyp in - let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in - let revargs1 = - list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in - let _ = prNamedRLDecl "ltyp allargs1" allargs1 in - let _ = prNamedRLDecl "ltyp revargs1" revargs1 in - let revargs2 = - list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in - let _ = prNamedRLDecl "ltyp allargs2" allargs2 in - let _ = prNamedRLDecl "ltyp revargs2" revargs2 in - let typwithprms = - glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in - typwithprms - - -(** constructor numbering *) -let fresh_cstror_suffix , cstror_suffix_init = - let cstror_num = ref 0 in - (fun () -> - let res = string_of_int !cstror_num in - cstror_num := !cstror_num + 1; - res) , - (fun () -> cstror_num := 0) - -(** [merge_constructor_id id1 id2 shift] returns the identifier of the - new constructor from the id of the two merged constructor and - the merging info. *) -let merge_constructor_id id1 id2 shift:Id.t = - let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in - next_ident_fresh (Id.of_string id) - - - -(** [merge_constructors lnk shift avoid] merges the two list of - constructor [(name*type)]. These are translated to glob_constr - first, each of them having distinct var names. *) -let merge_constructors (shift:merge_infos) (avoid:Id.Set.t) - (typcstr1:(Id.t * glob_constr) list) - (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list = - List.flatten - (List.map - (fun (id1,rawtyp1) -> - List.map - (fun (id2,rawtyp2) -> - let typ = merge_one_constructor shift rawtyp1 rawtyp2 in - let newcstror_id = merge_constructor_id id1 id2 shift in - let _ = prstr "\n**************\n" in - newcstror_id , typ) - typcstr2) - typcstr1) - -(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two - inductive bodies [oib1] and [oib2], linking with [lnk], params - info in [shift], avoiding identifiers in [avoid]. *) -let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) - (oib2:one_inductive_body) = - (* building glob_constr type of constructors *) - let mkrawcor nme avoid typ = - (* first replace rel 1 by a varname *) - let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in - let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in - let lcstr1: glob_constr list = - Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in - (* add to avoid all indentifiers of lcstr1 *) - let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in - let lcstr2 = - Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in - let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in - - let params1 = - try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with e when CErrors.noncritical e -> [] in - let params2 = - try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with e when CErrors.noncritical e -> [] in - - let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in - let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in - - cstror_suffix_init(); - params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2 - - -(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual - inductive bodies [mib1] and [mib2] linking vars with - [lnk]. [shift] information on parameters of the new inductive. - For the moment, inductives are supposed to be non mutual. -*) -let merge_mutual_inductive_body - (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = - (* Mutual not treated, we take first ind body of each. *) - merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0) - - -let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *) - Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x - -let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = - let params = prms2 @ prms1 in - let resparams = - List.fold_left - (fun acc (nme,tp) -> - let _ = prstr "param :" in - let _ = prNamedRConstr (string_of_name nme) tp in - let _ = prstr " ; " in - let typ = glob_constr_to_constr_expr tp in - CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) - [] params in - let concl = Constrextern.extern_constr false (Global.env()) Evd.empty (EConstr.of_constr concl) in - let arity,_ = - List.fold_left - (fun (acc,env) decl -> - let nm = Context.Rel.Declaration.get_name decl in - let c = RelDecl.get_type decl in - let typ = Constrextern.extern_constr false env Evd.empty (EConstr.of_constr c) in - let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) - (concl,Global.env()) - (shift.funresprms2 @ shift.funresprms1 - @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in - resparams,arity - - - -(** [glob_constr_list_to_inductive_expr ident rawlist] returns the - induct_expr corresponding to the the list of constructor types - [rawlist], named ident. - FIXME: params et cstr_expr (arity) *) -let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(Id.t * glob_constr) list) = - let lident = (Loc.tag shift.ident), None in - let bindlist , cstr_expr = (* params , arities *) - merge_rec_params_and_arity prms1 prms2 shift mkSet in - let lcstor_expr : (bool * (lident * constr_expr)) list = - List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t)) - rawlist in - lident , bindlist , Some cstr_expr , lcstor_expr - - -let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = - match rdecl with - | LocalAssum (nme,t) -> - let t = EConstr.of_constr t in - let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in - DAst.make @@ GProd (nme,Explicit,traw,t2) - | LocalDef _ -> assert false - - -(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking - variables specified in [lnk]. Graphs are not supposed to be mutual - inductives for the moment. *) -let merge_inductive (ind1: inductive) (ind2: inductive) - (lnk1: linked_var array) (lnk2: linked_var array) id = - let env = Global.env() in - let mib1,_ = Inductive.lookup_mind_specif env ind1 in - let mib2,_ = Inductive.lookup_mind_specif env ind2 in - let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *) - (* compute params that become ordinary args (because linked to ord. args) *) - let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in - let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in - let _ = prstr "\nrawlist : " in - let _ = - List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in - let _ = prstr "\nend rawlist\n" in -(* FIX: retransformer en constr ici - let shift_prm = - { shift_prm with - recprms1=prms1; - recprms1=prms1; - } in *) - let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in - (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] - false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in - (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) - - -(* Find infos on identifier id. *) -let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = - let kn_of_id x = - let f_ref = Libnames.Ident (Loc.tag x) in - locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) - locate_constant f_ref in - try find_Function_infos (kn_of_id id) - with Not_found -> - user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme") - -(** [merge id1 id2 args1 args2 id] builds and declares a new inductive - type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occurring in both arrays [args1] and - [args2] are considered linked (i.e. are the same variable) in the - new graph. - - Warning: For the moment, repetitions of an id in [args1] or - [args2] are not supported. *) -let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array) - (args2:Id.t array) id : unit = - let finfo1 = find_Function_infos_safe id1 in - let finfo2 = find_Function_infos_safe id2 in - (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *) - (* We add one arg (functional arg of the graph) *) - let lnk1 = Array.make (Array.length args1 + 1) Unlinked in - let lnk2' = (* args2 may be linked to args1 members. FIXME: same - as above: vars may be linked inside args2?? *) - Array.mapi - (fun i c -> - match Array.findi (fun i x -> Id.equal x c) args1 with - | Some j -> Linked j - | None -> Unlinked) - args2 in - (* We add one arg (functional arg of the graph) *) - let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in - (* setting functional results *) - let _ = lnk1.(Array.length lnk1 - 1) <- Funres in - let _ = lnk2.(Array.length lnk2 - 1) <- Funres in - merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id - - -let remove_last_arg c = - let (x,y) = decompose_prod c in - let xnolast = List.rev (List.tl (List.rev x)) in - compose_prod xnolast y - -let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l) -let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l)) - -let remove_last_n_arg n c = - let (x,y) = decompose_prod c in - let xnolast = remove_n_last_list n x in - compose_prod xnolast y - -(* [funify_branches relinfo nfuns branch] returns the branch [branch] - of the relinfo [relinfo] modified to fit in a functional principle. - Things to do: - - remove indargs from rel applications - - replace *variables only* corresponding to function (recursive) - results by the actual function application. *) -let funify_branches relinfo nfuns branch = - let mut_induct, induct = - match relinfo.indref with - | None -> assert false - | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind - | _ -> assert false in - let is_dom c = - match Constr.kind c with - | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct - | _ -> false in - let _dom_i c = - assert (is_dom c); - match Constr.kind c with - | Ind((u,i)) | Construct((u,_),i) -> i - | _ -> assert false in - let _is_pred c shift = - match Constr.kind c with - | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) - | _ -> false in - (* FIXME: *) - LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp) - - -let relprinctype_to_funprinctype relprinctype nfuns = - let relprinctype = EConstr.of_constr relprinctype in - let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in - assert (not relinfo.farg_in_concl); - assert (relinfo.indarg_in_concl); - (* first remove indarg and indarg_in_concl *) - let relinfo_noindarg = { relinfo with - indarg_in_concl = false; indarg = None; - concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in - (* the nfuns last induction arguments are functional ones: remove them *) - let relinfo_argsok = { relinfo_noindarg with - nargs = relinfo_noindarg.nargs - nfuns; - (* args is in reverse order, so remove fst *) - args = remove_n_fst_list nfuns relinfo_noindarg.args; - concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl)); - } in - let new_branches = - List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in - let relinfo_branches = { relinfo_argsok with branches = new_branches } in - relinfo_branches - -(* @article{ bundy93rippling, - author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill", - title = "Rippling: A Heuristic for Guiding Inductive Proofs", - journal = "Artificial Intelligence", - volume = "62", - number = "2", - pages = "185-253", - year = "1993", - url = "citeseer.ist.psu.edu/bundy93rippling.html" } - - *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 766adfc63a..8fe05b4978 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -861,7 +861,7 @@ let rec prove_le g = | App (c, [| x0 ; _ |]) -> EConstr.isVar sigma x0 && Id.equal (destVar sigma x0) (destVar sigma x) && - is_global sigma (le ()) c + EConstr.is_global sigma (le ()) c | _ -> false in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) @@ -1427,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evmap, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evmap, env = Pfedit.get_current_context () in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - evmap + evd (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open Constr in let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let ty = EConstr.Unsafe.to_constr ty in - let evm, nf = Evarutil.nf_evars_and_universes !evd in + let evd, nf = Evarutil.nf_evars_and_universes evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in @@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 50b84731b5..b95d64ce9e 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,6 +1,5 @@ open Constr -(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : Tacmach.tactic -> bool -> diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack index 2b443f2a1b..755fa4f879 100644 --- a/plugins/funind/recdef_plugin.mlpack +++ b/plugins/funind/recdef_plugin.mlpack @@ -6,5 +6,4 @@ Functional_principles_proofs Functional_principles_types Invfun Indfun -Merge G_indfun diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 982fc7cc3c..3e3965b94a 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -25,6 +25,7 @@ open Termops open Equality open Misctypes open Proofview.Notations +open Vernacinterp DECLARE PLUGIN "ltac_plugin" @@ -249,11 +250,10 @@ TACTIC EXTEND rewrite_star (**********************************************************************) (* Hint Rewrite *) -let add_rewrite_hint bases ort t lcsr = +let add_rewrite_hint ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in - let poly = Flags.use_polymorphic_flag () in - let f ce = + let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = let ctx = UState.context_set ctx in @@ -270,16 +270,16 @@ let add_rewrite_hint bases ort t lcsr = let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater -VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint +VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - [ add_rewrite_hint bl o None l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - [ add_rewrite_hint bl o (Some t) l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ add_rewrite_hint ["core"] o None l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ add_rewrite_hint ["core"] o (Some t) l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ] END (**********************************************************************) @@ -290,7 +290,7 @@ open EConstr open Vars open Coqlib -let project_hint pri l2r r = +let project_hint ~poly pri l2r r = let gr = Smartlocate.global_with_alias r in let env = Global.env() in let sigma = Evd.from_env env in @@ -313,30 +313,28 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let poly = Flags.use_polymorphic_flag () in let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff ?locality l2r lc n bl = - Hints.add_hints (Locality.make_module_locality locality) bl - (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) +let add_hints_iff ~atts l2r lc n bl = + let open Vernacinterp in + Hints.add_hints (Locality.make_module_locality atts.locality) bl + (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality true lc n bl; + add_hints_iff ~atts true lc n bl; st end ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality true lc n ["core"]; + add_hints_iff ~atts true lc n ["core"]; st end ] @@ -346,15 +344,13 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality false lc n bl; + add_hints_iff ~atts false lc n bl; st end ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality false lc n ["core"]; + add_hints_iff ~atts false lc n ["core"]; st end ] @@ -430,34 +426,46 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater | [ "Type" ] -> [ InType ] END*) -VERNAC COMMAND EXTEND DeriveInversionClear +VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ] END -VERNAC COMMAND EXTEND DeriveInversion +VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s false inv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ] END -VERNAC COMMAND EXTEND DeriveDependentInversion +VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s true dinv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ] END -VERNAC COMMAND EXTEND DeriveDependentInversionClear +VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ] END (**********************************************************************) @@ -1117,3 +1125,12 @@ VERNAC COMMAND EXTEND OptimizeProof | [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> [ Gc.compact () ] END + +(** tactic analogous to "OPTIMIZE HEAP" *) + +let tclOPTIMIZE_HEAP = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) + +TACTIC EXTEND optimize_heap +| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ] +END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8b9eb39837..cc7ce339b2 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -242,12 +237,7 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: @@ -337,7 +327,8 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g + | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6aa2f6f898..e5ff473568 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9ae8bfe65b..1615465281 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -289,7 +289,7 @@ let rec find_in_stack what acc = function | { name } as x :: rest when String.equal name what -> Some(acc, x, rest) | { name } as x :: rest -> find_in_stack what (x :: acc) rest -let exit_tactic start_time c = +let exit_tactic ~count_call start_time c = let diff = time () -. start_time in match Local.(!stack) with | [] | [_] -> @@ -304,7 +304,7 @@ let exit_tactic start_time c = let node = { node with total = node.total +. diff; local = node.local +. diff; - ncalls = node.ncalls + 1; + ncalls = node.ncalls + (if count_call then 1 else 0); max_total = max node.max_total diff; } in (* updating the stack *) @@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) = (fun v -> finally <*> Proofview.tclUNIT v) (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) -let do_profile s call_trace tac = +let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then @@ -359,7 +359,7 @@ let do_profile s call_trace tac = tac (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> (match call_trace with - | (_, c) :: _ -> exit_tactic start_time c + | (_, c) :: _ -> exit_tactic ~count_call start_time c | [] -> ())))) | None -> tac @@ -397,6 +397,27 @@ let reset_profile () = reset_profile_tmp (); data := SM.empty +(* ****************************** Named timers ****************************** *) + +let timer_data = ref M.empty + +let timer_name = function + | Some v -> v + | None -> "" + +let restart_timer name = + timer_data := M.add (timer_name name) (System.get_time ()) !timer_data + +let get_timer name = + try M.find (timer_name name) !timer_data + with Not_found -> System.get_time () + +let finish_timing ~prefix name = + let tend = System.get_time () in + let tstart = get_timer name in + Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++ + System.fmt_time_difference tstart tend) + (* ******************** *) let print_results_filter ~cutoff ~filter = @@ -408,7 +429,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_notice (to_string ~cutoff ~filter results) + Feedback.msg_info (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 52827cb36b..adedf7ee91 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -9,9 +9,39 @@ (** Ltac profiling primitives *) +(* Note(JasonGross): Ltac semantics are a bit insane. There isn't + really a good notion of how many times a tactic has been "called", + because tactics can be partially evaluated, and it's unclear + whether the number of "calls" should be the number of times the + body is fetched and unfolded, or the number of times the code is + executed to a value, etc. The logic in [Tacinterp.eval_tactic] + gives a decent approximation, which I believe roughly corresponds + to the number of times that the engine runs the tactic value which + results from evaluating the tactic expression bound to the name + we're considering. However, this is a poor approximation of the + time spent in the tactic; we want to consider time spent evaluating + a tactic expression to a tactic value to be time spent in the + expression, not just time spent in the caller of the expression. + So we need to wrap some nodes in additional profiling calls which + don't count towards to total call count. Whether or not a call + "counts" is indicated by the [count_call] boolean argument. + + Unfortunately, at present, we can get very strange call graphs when + a named tactic expression never runs as a tactic value: if we have + [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to + run 0(!) times. It evaluates to [t] during tactic expression + evaluation, and although the call trace records the fact that it + was called by [t0] which was called by [t1], the tactic running + phase never sees this. Thus we get one call tree (from expression + evaluation) that has [t1] calls [t0] calls [t], and another call + tree which says that the caller of [t1] calls [t] directly; the + expression evaluation time goes in the first tree, and the call + count and tactic running time goes in the second tree. Alas, I + suspect that fixing this requires a redesign of how the profiler + hooks into the tactic engine. *) val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> - 'b Proofview.tactic -> 'b Proofview.tactic + ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit @@ -22,6 +52,10 @@ val print_results_tactic : string -> unit val reset_profile : unit -> unit +val restart_timer : string option -> unit + +val finish_timing : prefix:string -> string option -> unit + val do_print_results_at_close : unit -> unit (* The collected statistics for a tactic. The timing data is collected over all @@ -46,4 +80,3 @@ type treenode = { (* Returns the profiling results known by the current process *) val get_local_profiling_results : unit -> treenode val feedback_results : treenode -> unit - diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 2b1106ee21..9864ffeb65 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -13,21 +13,55 @@ open Profile_ltac open Stdarg -DECLARE PLUGIN "profile_ltac_plugin" +DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) +let tclRESET_PROFILE = + Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) + +let tclSHOW_PROFILE ~cutoff = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) + +let tclSHOW_PROFILE_TACTIC s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) + +let tclRESTART_TIMER s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) + +let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) + TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END -TACTIC EXTEND stop_profiling +TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END +TACTIC EXTEND reset_ltac_profile +| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ] +END + +TACTIC EXTEND show_ltac_profile +| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ] +| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ] +| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] +END + +TACTIC EXTEND restart_timer +| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] +END + +TACTIC EXTEND finish_timing +| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] +END + VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7c..acd7a30c43 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -210,9 +210,9 @@ end) = struct let t = Reductionops.whd_all env (goalevars evars) ty in match EConstr.kind (goalevars evars) t, l with | Prod (na, ty, b), obj :: cstrs -> - let b = Reductionops.nf_betaiota (goalevars evars) b in + let b = Reductionops.nf_betaiota env (goalevars evars) b in if noccurn (goalevars evars) 1 b (* non-dependent product *) then - let ty = Reductionops.nf_betaiota (goalevars evars) ty in + let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in let evars, relty = mk_relty evars env ty obj in let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in @@ -221,7 +221,7 @@ end) = struct let (evars, b, arg, cstrs) = aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in - let ty = Reductionops.nf_betaiota (goalevars evars) ty in + let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in @@ -231,7 +231,7 @@ end) = struct | _, [] -> (match finalcstr with | None | Some (_, None) -> - let t = Reductionops.nf_betaiota (fst evars) ty in + let t = Reductionops.nf_betaiota env (fst evars) ty in let evars, rel = mk_relty evars env t None in evars, t, rel, [t, Some rel] | Some (t, Some rel) -> evars, t, rel, [t, Some rel]) @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -1557,9 +1557,8 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in (** For compatibility *) - let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in - let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in + let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in + let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") @@ -1781,7 +1780,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -1979,8 +1980,7 @@ let add_morphism_infer glob m n = Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob - poly (ConstRef cst)); + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, poly, @@ -1991,7 +1991,7 @@ let add_morphism_infer glob m n = | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info - glob poly (ConstRef cst)); + glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false in @@ -2012,23 +2012,26 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2066,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in @@ -2084,8 +2087,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9ae112d371..e5933de2a6 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -61,12 +61,9 @@ struct type t = Val.t -let normalize v = v - let of_constr c = in_gen (topwit wit_constr) c let to_constr v = - let v = normalize v in if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in Some c @@ -78,7 +75,6 @@ let to_constr v = let of_uconstr c = in_gen (topwit wit_uconstr) c let to_uconstr v = - let v = normalize v in if has_type v (topwit wit_uconstr) then Some (out_gen (topwit wit_uconstr) v) else None @@ -86,7 +82,6 @@ let to_uconstr v = let of_int i = in_gen (topwit wit_int) i let to_int v = - let v = normalize v in if has_type v (topwit wit_int) then Some (out_gen (topwit wit_int) v) else None @@ -108,14 +103,12 @@ let constr_of_id env id = (* Gives the constr corresponding to a Constr_context tactic_arg *) let coerce_to_constr_context v = - let v = Value.normalize v in if has_type v (topwit wit_constr_context) then out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -140,7 +133,6 @@ let g = sigma in let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -179,7 +171,6 @@ let id_of_name = function let coerce_to_intro_pattern env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then snd (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_var) then @@ -198,7 +189,6 @@ let coerce_to_intro_pattern_naming env sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) -> Id.to_string id @@ -206,13 +196,11 @@ let coerce_to_hint_base v = else raise (CannotCoerceTo "a hint base name") let coerce_to_int v = - let v = Value.normalize v in if has_type v (topwit wit_int) then out_gen (topwit wit_int) v else raise (CannotCoerceTo "an integer") let coerce_to_constr env v = - let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a term") in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -230,7 +218,6 @@ let coerce_to_constr env v = else fail () let coerce_to_uconstr env v = - let v = Value.normalize v in if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -243,7 +230,6 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with @@ -284,7 +270,6 @@ let coerce_to_intro_pattern_list ?loc env sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id @@ -306,7 +291,6 @@ let coerce_to_hyp_list env sigma v = (* Interprets a qualified name *) let coerce_to_reference env sigma v = - let v = Value.normalize v in match Value.to_constr v with | Some c -> begin @@ -318,7 +302,6 @@ let coerce_to_reference env sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -336,7 +319,6 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_decl_or_quant_hyp env sigma v = - let v = Value.normalize v in if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index d7b253a687..dce16b7333 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -31,9 +31,6 @@ module Value : sig type t = Val.t - val normalize : t -> t - (** Eliminated the leading dynamic type casts. *) - val of_constr : constr -> t val to_constr : t -> constr option val of_uconstr : Ltac_pretype.closed_glob_constr -> t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9bd3efc6b7..ccd555b615 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index b16b0a7bae..ebffde441d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f8..f2720954d0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -136,7 +136,6 @@ let to_tacvalue v = out_gen (topwit wit_tacvalue) v (** More naming applications *) let name_vfun appl vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) @@ -235,7 +234,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = - let v = Value.normalize v in let pr_with_env pr = match env with | Some (env,sigma) -> pr env sigma @@ -285,7 +283,6 @@ let push_trace call ist = match TacStore.get ist.extra f_trace with | Some trace -> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -298,7 +295,6 @@ let propagate_trace ist loc id v = else Proofview.tclUNIT v let append_trace trace v = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) @@ -307,11 +303,9 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = - let v = Value.normalize v in let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with @@ -420,7 +414,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -514,7 +508,6 @@ let rec intropattern_ids accu (loc,pat) = match pat with let extract_ids ids lfun accu = let fold id v accu = - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu @@ -816,7 +809,6 @@ let interp_constr_may_eval ist env sigma c = (** TODO: should use dedicated printers *) let message_of_value v = - let v = Value.normalize v in let pr_with_env pr = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in @@ -890,7 +882,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar (loc,id)) -> - (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with + (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) @@ -986,7 +978,6 @@ let interp_destruction_arg ist gl arg = try (** FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in - let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in match v with @@ -1040,7 +1031,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) @@ -1158,10 +1149,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end - | TacAbstract (tac,ido) -> + | TacAbstract (t,ido) -> + let call = LtacMLCall tac in + push_trace(None,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:TacAbstract" trace + (catch_error_tac trace begin Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end + (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) + end end) | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1244,7 +1239,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in match v with @@ -1272,7 +1266,8 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in - val_interp ~appl ist (Tacenv.interp_ltac r) + Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false + (val_interp ~appl ist (Tacenv.interp_ltac r)) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1319,7 +1314,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in - let fv = Value.normalize fv in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1338,7 +1332,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error_tac trace (val_interp ist body) >>= fun v -> + Profile_ltac.do_profile "interp_app" trace ~count_call:false + (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1371,7 +1366,6 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = - let vle = Value.normalize vle in if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> @@ -1598,7 +1592,6 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let result = Value.normalize result in try let cresult = coerce_to_closed_constr env result in Proofview.tclLIFT begin diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faebe..79bf3685e2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e5907..e87951dd7f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index e5b5854f0a..362cc3a597 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -49,16 +49,13 @@ Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -(** We now extract to stdout, see comment in Makefile.build *) - -(*Extraction "plugins/micromega/micromega.ml" *) -Recursive Extraction - List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add - n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. - - - +(** In order to avoid annoying build dependencies the actual + extraction is only performed as a test in the test suite. *) +(* Extraction "plugins/micromega/micromega.ml" *) +(* Recursive Extraction *) +(* List.map simpl_cone (*map_cone indexes*) *) +(* denorm Qpower vm_add *) +(* n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *) (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 8692842468..4271c80cd1 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -652,7 +652,7 @@ let decompile af = (** Backward compat to emulate the old Refine: normalize the goal conclusion *) let new_hole env sigma c = - let c = Reductionops.nf_betaiota sigma c in + let c = Reductionops.nf_betaiota env sigma c in Evarutil.new_evar env sigma c let clever_rewrite_base_poly typ p result theorem = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 047ca509be..7cdf051176 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> Evar.print k) evlist)); let evplist = @@ -894,7 +894,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ let sigma = create_evar_defs sigma in let (sigma, x) = Evarutil.new_evar env sigma - (if bi_types then Reductionops.nf_betaiota sigma src else src) in + (if bi_types then Reductionops.nf_betaiota env sigma src else src) in loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1) | CastType (t, _) -> loop t args sigma n | LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n @@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afbd..6032ed2af8 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 3efb7b9147..d74ad06b34 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d ))) + ((Loc.tag (Name s)),None), d) ]]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e63a05b781..d6dbad7a95 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1228,7 +1228,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1 + | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1236,8 +1236,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in let concl = find_T env0 concl0 1 ~k:do_subst in - let _ = end_T () in - concl + let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> let p = fs sigma p in let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in @@ -1252,8 +1252,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env _ -> do_subst env e_body))) in - let _ = end_X () in let _ = end_T () in - concl + let _ = end_X () in let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, E_In_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1268,8 +1268,9 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> find_E env e_body h ~k:do_subst))) in - let _ = end_E () in let _ = end_X () in let _ = end_T () in - concl + let _,_,(_,us,_) = end_E () in + let _ = end_X () in let _ = end_T () in + concl, us | Some (sigma, E_As_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1287,8 +1288,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in - let _ = end_X () in let _ = end_TE () in - concl + let _ = end_X () in let _,_,(_,us,_) = end_TE () in + concl, us ;; let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = @@ -1306,12 +1307,14 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in (fun env c _ h' -> - do_once r (fun () -> c, Evd.empty_evar_universe_context); + do_once r (fun () -> c); if do_make_rel then mkRel (h'+h-1) else c), - (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in - let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + (fun _ -> if !r = None then fst(redex_of_pattern env pat) + else assert_done r) in + let cl, us = + eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in let e = conclude cl in - e, cl + (e, us), cl ;; (* clenup interface for external use *) @@ -1319,6 +1322,10 @@ let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + fst (eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst) +;; + let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let p = EConstr.Unsafe.to_constr p in let concl = EConstr.Unsafe.to_constr concl in |