diff options
109 files changed, 774 insertions, 913 deletions
diff --git a/.gitignore b/.gitignore index 8a0c54f8f..d91a674e1 100644 --- a/.gitignore +++ b/.gitignore @@ -49,6 +49,7 @@ config/Makefile config/coq_config.ml config/Info-*.plist dev/ocamldebug-coq +dev/camlp4.dbg plugins/micromega/csdpcert kernel/byterun/dllcoqrun.so coqdoc.sty @@ -156,5 +157,6 @@ dev/myinclude /doc/refman/Reference-Manual.hoptind /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind + user-contrib .*.sw* @@ -227,7 +227,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -delete cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist distclean: clean cleanconfig cacheclean diff --git a/Makefile.build b/Makefile.build index 95df69c2d..228b2e736 100644 --- a/Makefile.build +++ b/Makefile.build @@ -220,7 +220,7 @@ CINCLUDES= -I $(CAMLHLIB) $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ - $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) + $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ @@ -505,6 +505,12 @@ test-suite: world $(ALLSTDLIB).v # but the -include mechanism should already ensure that we have # up-to-date dependencies. +# Specific rule for kernel.cma, with $(VMBYTEFLAGS). +# This helps loading dllcoqrun.so during an ocamldebug +kernel/kernel.cma: kernel/kernel.mllib + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) + %.cma: %.mllib $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) diff --git a/Makefile.dev b/Makefile.dev index 501a7744a..d9db7055f 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,21 +15,18 @@ .PHONY: devel printers -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers -printers: $(DEBUGPRINTERS) - -dev/printers.cma: dev/printers.mllib - $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer - @rm -f test-printer - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ - -dev/%.mllib.d: dev/%.mllib | $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) +printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg + +ifeq ($(CAMLP4),camlp5) +dev/camlp4.dbg: + echo "load_printer gramlib.cma" > $@ +else +dev/camlp4.dbg: + echo "load_printer camlp4lib.cma" > $@ +endif ############ # revision diff --git a/checker/Makefile b/checker/Makefile deleted file mode 100644 index 2bcc9d365..000000000 --- a/checker/Makefile +++ /dev/null @@ -1,88 +0,0 @@ -OCAMLC=ocamlc -OCAMLOPT=ocamlopt - -COQSRC=.. - -MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4 -BYTEFLAGS=$(MLDIRS) -OPTFLAGS=$(MLDIRS) - -CHECKERNAME=coqchk - -BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE) -MCHECKERLOCAL :=\ - declarations.cmo environ.cmo \ - closure.cmo reduction.cmo \ - type_errors.cmo \ - modops.cmo \ - inductive.cmo typeops.cmo \ - indtypes.cmo subtyping.cmo mod_checking.cmo \ -validate.cmo \ - safe_typing.cmo check.cmo \ - check_stat.cmo checker.cmo - -MCHECKER:=\ - $(COQSRC)/config/coq_config.cmo \ - $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \ - $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \ - $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \ - $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \ - $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \ - $(COQSRC)/kernel/esubst.cmo term.cmo \ - $(MCHECKERLOCAL) - -all: $(BINARIES) - -byte : ../bin/$(CHECKERNAME)$(EXE) -opt : ../bin/$(CHECKERNAME).opt$(EXE) - -check.cma: $(MCHECKERLOCAL) - ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER) - -check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx) - ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx) - -../bin/$(CHECKERNAME)$(EXE): check.cma - ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml - -../bin/$(CHECKERNAME).opt$(EXE): check.cmxa - ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml - -stats: - @echo STRUCTURE - @wc names.ml term.ml declarations.ml environ.ml type_errors.ml - @echo - @echo REDUCTION - @-wc esubst.ml closure.ml reduction.ml - @echo - @echo TYPAGE - @wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml - @echo - @echo MODULES - @wc modops.ml subtyping.ml - @echo - @echo INTERFACE - @wc check*.ml main.ml - @echo - @echo TOTAL - @wc *.ml | tail -1 - -.SUFFIXES:.ml .mli .cmi .cmo .cmx - -.ml.cmo: - $(OCAMLC) -c $(BYTEFLAGS) $< - -.ml.cmx: - $(OCAMLOPT) -c $(OPTFLAGS) $< - -.mli.cmi: - $(OCAMLC) -c $(BYTEFLAGS) $< - - -depend:: - ocamldep *.ml* > .depend - -clean:: - rm -f *.cm* *.o *.a *~ $(BINARIES) - --include .depend diff --git a/configure.ml b/configure.ml index 2c1d531ea..efba6f59b 100644 --- a/configure.ml +++ b/configure.ml @@ -1092,6 +1092,7 @@ let write_makefile f = pr "LOCAL=%B\n\n" !Prefs.local; pr "# Bytecode link flags : should we use -custom or not ?\n"; pr "CUSTOM=%s\n" custom_flag; + pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); pr "%s\n\n" !build_loadpath; pr "# Paths for true installation\n"; List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs; diff --git a/dev/base_db b/dev/base_db index b540aed6c..e18ac534a 100644 --- a/dev/base_db +++ b/dev/base_db @@ -1,6 +1,6 @@ -load_printer "gramlib.cma" -load_printer "top_printers.cmo" -install_printer Top_printers.prid -install_printer Top_printers.prsp -install_printer Top_printers.print_pure_constr +source core.dbg +load_printer top_printers.cmo +install_printer Top_printers.ppid +install_printer Top_printers.ppsp +install_printer Top_printers.ppconstr diff --git a/dev/core.dbg b/dev/core.dbg new file mode 100644 index 000000000..a43aac89a --- /dev/null +++ b/dev/core.dbg @@ -0,0 +1,16 @@ +source camlp4.dbg +load_printer threads.cma +load_printer str.cma +load_printer clib.cma +load_printer lib.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer stm.cma +load_printer toplevel.cma @@ -1,4 +1,5 @@ -load_printer "printers.cma" +source core.dbg +load_printer top_printers.cmo install_printer Top_printers.ppfuture diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index fcee79e07..5933649da 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,17 @@ ========================================= += CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = +========================================= + +We renamed the following functions: + + Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr + Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr + +The following type aliases where removed + + Context.section_context ... it was just an alias for "Context.Named.t" which is still available + +========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index f0df2fc37..79cde4884 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -51,8 +51,8 @@ Debugging from Caml debugger failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle of each of error* functions or anomaly* functions in lib/util.ml - - If "source db" fails, recompile printers.cma with - "make dev/printers.cma" and try again + - If "source db" fails, do a "make printers" and try again (it should build + top_printers.cmo and the core cma files). Global gprof-based profiling ============================ diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f9310e076..46caca8d6 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -12,11 +12,13 @@ [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` +export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH + exec $OCAMLDEBUG \ - -I $CAMLP4LIB \ + -I $CAMLP4LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ + -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ diff --git a/dev/printers.mllib b/dev/printers.mllib deleted file mode 100644 index 316549548..000000000 --- a/dev/printers.mllib +++ /dev/null @@ -1,219 +0,0 @@ -Coq_config - -Terminal -Hook -Canary -Hashset -Hashcons -CSet -CMap -Int -Dyn -HMap -Option -Store -Exninfo -Backtrace -IStream -Pp_control -Loc -CList -CString -Tok -Compat -Flags -Control -Loc -Serialize -Stateid -CObj -CArray -CStack -Util -Pp -Ppstyle -Richpp -Feedback -Segmenttree -Unicodetable -Unicode -CErrors -CWarnings -Bigint -CUnix -Minisys -System -Envars -Aux_file -Profile -Explore -Predicate -Rtree -Heap -Genarg -Stateid -CEphemeron -Future -RemoteCounter -Monad - -Names -Univ -UGraph -Esubst -Uint31 -Sorts -Evar -Constr -Context -Vars -Term -Mod_subst -Cbytecodes -Copcodes -Cemitcodes -Nativevalues -Primitives -Nativeinstr -Future -Opaqueproof -Declareops -Retroknowledge -Conv_oracle -Pre_env -Nativelambda -Nativecode -Nativelib -Cbytegen -Environ -CClosure -Reduction -Nativeconv -Type_errors -Modops -Inductive -Typeops -Fast_typeops -Indtypes -Cooking -Term_typing -Subtyping -Mod_typing -Nativelibrary -Safe_typing -Unionfind - -Summary -Nameops -Libnames -Globnames -Global -Nametab -Libobject -Lib -Loadpath -Goptions -Decls -Heads -Keys -Locusops -Miscops -Universes -Termops -Namegen -UState -Evd -Sigma -Glob_ops -Redops -Pretype_errors -Evarutil -Reductionops -Inductiveops -Arguments_renaming -Nativenorm -Retyping -Cbv - -Evardefine -Evarsolve -Recordops -Evarconv -Typing -Patternops -Constr_matching -Find_subterm -Tacred -Classops -Typeclasses_errors -Logic_monad -Proofview_monad -Proofview -Ftactic -Geninterp -Typeclasses -Detyping -Indrec -Program -Coercion -Cases -Pretyping -Unification -Declaremods -Library -States - -Genprint -CLexer -Ppextend -Pputils -Ppannotation -Stdarg -Constrarg -Constrexpr_ops -Genintern -Notation_ops -Notation -Dumpglob -Syntax_def -Smartlocate -Topconstr -Reserve -Impargs -Implicit_quantifiers -Constrintern -Modintern -Constrextern -Goal -Miscprint -Logic -Refiner -Clenv -Evar_refiner -Refine -Proof -Proof_global -Pfedit -Decl_mode -Ppconstr -Pcoq -Printer -Pptactic -Ppdecl_proof -Egramml -Egramcoq -Tacsubst -Trie -Dn -Btermdn -Hints -Himsg -ExplainErr -Locality -Assumptions -Vernacinterp -Dischargedhypsmap -Discharge -Declare -Ind_tables -Top_printers diff --git a/engine/evarutil.ml b/engine/evarutil.ml index bd86f4bd2..326cd25fc 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -18,6 +18,9 @@ open Environ open Evd open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None @@ -161,11 +164,11 @@ let is_ground_term evd t = not (has_undefined_evars evd t) let is_ground_env evd env = - let open Context.Rel.Declaration in + let open RelDecl in let is_ground_rel_decl = function | LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in - let open Context.Named.Declaration in + let open NamedDecl in let is_ground_named_decl = function | LocalDef (_,b,_) -> is_ground_term evd b | _ -> true in @@ -249,11 +252,10 @@ let non_instantiated sigma = (************************) let make_pure_subst evi args = - let open Context.Named.Declaration in snd (List.fold_right (fun decl (args,l) -> match args with - | a::rest -> (rest, (get_id decl, a)::l) + | a::rest -> (rest, (NamedDecl.get_id decl, a)::l) | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) @@ -327,10 +329,10 @@ let push_var id (n, s) = let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = let open Context.Named.Declaration in let replace_var_named_declaration id0 id decl = - let id' = get_id decl in + let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) + decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None @@ -551,8 +553,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let () = Id.Map.iter check ri in (* No dependency at all, we can keep this ev's context hyp *) (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) + with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter)) ctxt (Array.to_list l) (Id.Map.empty,[]) in (* Check if some rid to clear in the context of ev has dependencies in the type of ev and adjust the source of the dependency *) @@ -591,10 +592,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in let nhyps = - let open Context.Named.Declaration in let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids global) decl + let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in + NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl in let check_value vk = match force_lazy_val vk with | None -> vk @@ -633,8 +633,8 @@ let process_dependent_evar q acc evm is_dependent e = hypotheses), they are all dependent. *) queue_term q true evi.evar_concl; List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); + let open NamedDecl in + queue_term q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b @@ -688,9 +688,8 @@ let undefined_evars_of_term evd t = evrec Evar.Set.empty t let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) + (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) nc ~init:Evar.Set.empty diff --git a/engine/evd.ml b/engine/evd.ml index 6ba8a5112..d573a9f05 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -18,6 +18,9 @@ open Environ open Globnames open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Generic filters *) module Filter : sig @@ -226,7 +229,7 @@ let evar_instance_array test_id info args = if i < len then let c = Array.unsafe_get args i in if test_id d c then instrec filter ctxt (succ i) - else (get_id d, c) :: instrec filter ctxt (succ i) + else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in @@ -235,7 +238,7 @@ let evar_instance_array test_id info args = let map i d = if (i < len) then let c = Array.unsafe_get args i in - if test_id d c then None else Some (get_id d, c) + if test_id d c then None else Some (NamedDecl.get_id d, c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -243,7 +246,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array (isVarId % get_id) info args + evar_instance_array (isVarId % NamedDecl.get_id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in @@ -284,7 +287,7 @@ let metavars_of c = let rec collrec acc c = match kind_of_term c with | Meta mv -> Int.Set.add mv acc - | _ -> fold_constr collrec acc c + | _ -> Term.fold_constr collrec acc c in collrec Int.Set.empty c @@ -681,7 +684,7 @@ let restrict evk filter ?candidates evd = evar_extra = Store.empty } in let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (mkVar % get_id) ctxt in + let id_inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in let body = mkEvar(evk',id_inst) in let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; @@ -731,23 +734,22 @@ let evar_list c = let rec evrec acc c = match kind_of_term c with | Evar (evk, _ as ev) -> ev :: acc - | _ -> fold_constr evrec acc c in + | _ -> Term.fold_constr evrec acc c in evrec [] c let evars_of_term c = let rec evrec acc c = match kind_of_term c with | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> fold_constr evrec acc c + | _ -> Term.fold_constr evrec acc c in evrec Evar.Set.empty c let evars_of_named_context nc = - List.fold_right (fun decl s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl)) - nc Evar.Set.empty + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) + nc + ~init:Evar.Set.empty let evars_of_filtered_evar_info evi = Evar.Set.union (evars_of_term evi.evar_concl) @@ -1283,11 +1285,10 @@ let pr_meta_map mmap = prlist pr_meta_binding (metamap_to_list mmap) let pr_decl (decl,ok) = - let id = get_id decl in - match get_value decl with - | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") + match decl with + | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" @@ -1398,12 +1399,11 @@ let pr_evar_universe_context ctx = h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) let print_env_short env = - let pr_body n = function - | None -> pr_name n - | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in - let pr_rel_decl decl = let open Context.Rel.Declaration in - pr_body (get_name decl) (get_value decl) in + let pr_rel_decl = function + | RelDecl.LocalAssum (n,_) -> pr_name n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + in + let pr_named_decl = pr_rel_decl % NamedDecl.to_rel in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ diff --git a/engine/namegen.ml b/engine/namegen.ml index 84eb98684..1497dbda8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -24,6 +24,8 @@ open Environ open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -114,9 +116,9 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match Environ.lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in @@ -295,11 +297,10 @@ let make_all_name_different env = let avoid = ref (ids_of_named_context (named_context env)) in process_rel_context (fun decl newenv -> - let (na,_,t) = to_tuple decl in - let na = named_hd newenv t na in + let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) + push_rel (RelDecl.set_name (Name id) decl) newenv) env (* 5- Looks for next fresh name outside a list; avoids also to use names that diff --git a/engine/termops.ml b/engine/termops.ml index a047bf53c..3f36059dd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -17,6 +17,7 @@ open Environ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration +module NamedListDecl = Context.NamedList.Declaration (* Sorts and sort family *) @@ -983,14 +984,25 @@ let rec mem_named_context id ctxt = let compact_named_context_reverse sign = let compact l decl = - let (i1,c1,t1) = NamedDecl.to_tuple decl in - match l with - | [] -> [[i1],c1,t1] - | (l2,c2,t2)::q -> - if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - then (i1::l2,c2,t2)::q - else ([i1],c1,t1)::l - in Context.Named.fold_inside compact ~init:[] sign + match decl, l with + | NamedDecl.LocalAssum (i,t), [] -> + [NamedListDecl.LocalAssum ([i],t)] + | NamedDecl.LocalDef (i,c,t), [] -> + [NamedListDecl.LocalDef ([i],c,t)] + | NamedDecl.LocalAssum (i1,t1), NamedListDecl.LocalAssum (li,t2) :: q -> + if Constr.equal t1 t2 + then NamedListDecl.LocalAssum (i1::li, t2) :: q + else NamedListDecl.LocalAssum ([i1],t1) :: NamedListDecl.LocalAssum (li,t2) :: q + | NamedDecl.LocalDef (i1,c1,t1), NamedListDecl.LocalDef (li,c2,t2) :: q -> + if Constr.equal c1 c2 && Constr.equal t1 t2 + then NamedListDecl.LocalDef (i1::li, c2, t2) :: q + else NamedListDecl.LocalDef ([i1],c1,t1) :: NamedListDecl.LocalDef (li,c2,t2) :: q + | NamedDecl.LocalAssum (i,t), q -> + NamedListDecl.LocalAssum ([i],t) :: q + | NamedDecl.LocalDef (i,c,t), q -> + NamedListDecl.LocalDef ([i],c,t) :: q + in + Context.Named.fold_inside compact ~init:[] sign let compact_named_context sign = List.rev (compact_named_context_reverse sign) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7ae..36d676f5d 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,6 +13,9 @@ open Util open Pp open Printer +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered when the -ideslave option is passed to Coqtop. Currently CoqIDE is @@ -133,7 +136,8 @@ let annotate phrase = (** Goal display *) let hyp_next_tac sigma env decl = - let (id,_,ast) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in + let ast = NamedDecl.get_type decl in let id_s = Names.Id.to_string id in let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ @@ -191,11 +195,7 @@ let process_goal sigma g = in let process_hyp d (env,l) = let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in - let d' = List.map (fun name -> let open Context.Named.Declaration in - match pi2 d with - | None -> LocalAssum (name, pi3 d) - | Some value -> LocalDef (name, value, pi3 d)) - (pi1 d) in + let d' = Context.NamedList.Declaration.to_named_context d in (List.fold_right Environ.push_named d' env, (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58f..4d9386b9d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -21,6 +21,8 @@ open Libobject open Nameops open Misctypes open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" @@ -198,7 +200,7 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, decl) = match get_name decl with + let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -242,7 +244,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> - let id' = next_name_away_from (get_name decl) avoid in + let id' = next_name_away_from (RelDecl.get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..6279622bf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,6 +20,9 @@ open Notation_term open Glob_term open Glob_ops open Ppextend +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*i*) (*s A scope is a set of notations; it includes @@ -686,7 +689,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = let n = try let vars = Lib.variable_section_segment_of_reference r in - List.length (List.filter (fun (_,_,b,_) -> b = None) vars) + vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in Some (req,Lib.discharge_global r,n,l,[]) diff --git a/kernel/context.ml b/kernel/context.ml index 4e53b73a2..fed6a5feb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -138,7 +138,7 @@ struct | LocalDef (_,v,ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = + let fold_constr f decl acc = match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) @@ -147,9 +147,6 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) end (** Rel-context is represented as a list of declarations. @@ -336,7 +333,7 @@ struct | LocalDef (_, v, ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = + let fold_constr f decl a = match decl with | LocalAssum (_, ty) -> f ty a | LocalDef (_, v, ty) -> a |> f v |> f ty @@ -348,6 +345,18 @@ struct let of_tuple = function | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + + let of_rel f = function + | Rel.Declaration.LocalAssum (na,t) -> + LocalAssum (f na, t) + | Rel.Declaration.LocalDef (na,v,t) -> + LocalDef (f na, v, t) + + let to_rel = function + | LocalAssum (id,t) -> + Rel.Declaration.LocalAssum (Name id, t) + | LocalDef (id,v,t) -> + Rel.Declaration.LocalDef (Name id,v,t) end (** Named-context is represented as a list of declarations. @@ -401,23 +410,33 @@ struct | _ -> None in List.map_filter filter - end +end module NamedList = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t - - let map_constr f (ids, copt, ty as decl) = - let copt' = Option.map f copt in - let ty' = f ty in - if copt == copt' && ty == ty' then decl else (ids, copt', ty') + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + + let map_constr f = function + | LocalAssum (ids, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (ids, ty') + | LocalDef (ids, c, ty) as decl -> + let ty' = f ty in + let c' = f c in + if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') + + let to_named_context = function + | LocalAssum (ids, t) -> + List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids + | LocalDef (ids, v, t) -> + List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end type t = Declaration.t list let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index b5f3904d2..72fbfb540 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -79,10 +79,9 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Name.t * Constr.t option * Constr.t - val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -193,10 +192,18 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Id.t * Constr.t option * Constr.t val of_tuple : Id.t * Constr.t option * Constr.t -> t + + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. + The function provided as the first parameter determines how to translate "names" to "ids". *) + val of_rel : (Name.t -> Id.t) -> Rel.Declaration.t -> t + + (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *) + (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *) + val to_rel : t -> Rel.Declaration.t end (** Rel-context is represented as a list of declarations. @@ -248,13 +255,15 @@ module NamedList : sig module Declaration : sig - type t = Id.t list * Constr.t option * Constr.t + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + val map_constr : (Constr.t -> Constr.t) -> t -> t + val to_named_context : t -> Named.t end type t = Declaration.t list val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a end - -type section_context = Named.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 134599150..f5059cd75 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,8 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with @@ -152,7 +154,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } = in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 327e697d2..eb4073096 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,7 +19,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option val cook_constant : env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index acd73d97d..3177b5fae 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let open Context.Named in - let open Declaration in - env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env.env_named_context |> Context.Named.lookup id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let open Context.Rel in - let open Declaration in - env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f89773fcc..fe2fa6d7f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -78,7 +78,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { - const_hyps : Context.section_context; (** New: younger hyp at top *) + const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; @@ -177,7 +177,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e062..8943de404 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,7 +9,8 @@ open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -146,7 +147,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + RelDecl.map_type Term.hcons_types % RelDecl.map_value Term.hcons_constr % RelDecl.map_name Names.Name.hcons let hcons_rel_context l = List.smartmap hcons_rel_decl l diff --git a/kernel/entries.mli b/kernel/entries.mli index df2c4653f..b736b2113 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.section_context option; + const_entry_secctx : Context.Named.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -73,7 +73,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.section_context option * bool * types Univ.in_universe_context * inline + Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { proj_entry_ind : mutual_inductive; diff --git a/kernel/environ.ml b/kernel/environ.ml index 7351a87d4..8a147a659 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -416,7 +416,7 @@ let global_vars_set env constr = Id.Set.union (vars_of_global env c) acc | _ -> acc in - fold_constr filtrec acc c + Term.fold_constr filtrec acc c in filtrec Id.Set.empty constr diff --git a/kernel/environ.mli b/kernel/environ.mli index b5e576435..77451d8ea 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -232,7 +232,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index bd91c689d..dce4e9307 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -18,6 +18,9 @@ open Reduction open Inductive open Type_errors +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = @@ -73,8 +76,7 @@ let judge_of_type u = let judge_of_relative env n = try - let open Context.Rel.Declaration in - env |> lookup_rel n |> get_type |> lift n + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n @@ -92,9 +94,8 @@ let judge_of_variable env id = let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun decl () -> - let open Context.Named.Declaration in - let id = get_id decl in - let ty1 = get_type decl in + let id = NamedDecl.get_id decl in + let ty1 = NamedDecl.get_type decl in try let ty2 = named_type id env in if not (eq_constr ty2 ty1) then raise Exit diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d6..d673c91e8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -82,6 +82,9 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775..0af1cde8f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -82,6 +82,9 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + (** constructor *) + val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e2f43b93e..3864df6c9 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1832,10 +1832,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let open Context.Rel in - let n = length env.env_rel_context - n in - let open Declaration in - match lookup n env.env_rel_context with + let n = Context.Rel.length env.env_rel_context - n in + let open Context.Rel.Declaration in + match Context.Rel.lookup n env.env_rel_context with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e..366f9a0a6 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,6 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr +module RelDecl = Context.Rel.Declaration + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -727,8 +729,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let open Context.Rel.Declaration in - let ids = List.rev_map get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 5afefeebd..fefc3222d 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -17,7 +17,8 @@ open Util open Names open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -127,7 +128,7 @@ let env_of_rel n env = let push_named_context_val d (ctxt,vals) = let rval = ref VKnone in - Context.Named.add d ctxt, (get_id d,rval)::vals + Context.Named.add d ctxt, (NamedDecl.get_id d,rval)::vals let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); @@ -135,7 +136,7 @@ let push_named d env = let rval = ref VKnone in { env_globals = env.env_globals; env_named_context = Context.Named.add d env.env_named_context; - env_named_vals = (get_id d, rval) :: env.env_named_vals; + env_named_vals = (NamedDecl.get_id d, rval) :: env.env_named_vals; env_rel_context = env.env_rel_context; env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75c..f176ca579 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -361,7 +363,7 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 749b5dbaf..8db65e33c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,6 +22,9 @@ open Entries open Typeops open Fast_typeops +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let constrain_type env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) @@ -249,18 +252,17 @@ let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> Context.Rel.fold_outside - (Context.Rel.Declaration.fold + (RelDecl.fold_constr (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty let record_aux env s_ty s_bo suggested_expr = - let open Context.Named.Declaration in let in_ty = keep_hyps env s_ty in let v = String.concat " " (CList.map_filter (fun decl -> - let id = get_id decl in - if List.exists (Id.equal id % get_id) in_ty then None + let id = NamedDecl.get_id decl in + if List.exists (Id.equal id % NamedDecl.get_id) in_ty then None else Some (Id.to_string id)) (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) @@ -269,9 +271,8 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = - let open Context.Named.Declaration in let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in + let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in @@ -283,12 +284,12 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in let sort evn l = List.filter (fun decl -> - let id = get_id decl in - List.exists (Names.Id.equal id % get_id) l) + let id = NamedDecl.get_id decl in + List.exists (Names.Id.equal id % NamedDecl.get_id) l) (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in match ctx with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: @@ -482,8 +483,7 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let open Context.Named.Declaration in - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Opaqueproof.force_proof (opaque_tables env) lc) in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0059111c0..24018ab31 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -20,6 +20,9 @@ open Inductive open Type_errors open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y let conv_leq_vecti env v1 v2 = @@ -79,7 +82,7 @@ let judge_of_type u = let judge_of_relative env n = try - let typ = get_type (lookup_rel n env) in + let typ = RelDecl.get_type (lookup_rel n env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -102,7 +105,7 @@ let check_hyps_inclusion env c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in - let id = get_id d1 in + let id = NamedDecl.get_id d1 in try let d2 = lookup_named id env in conv env (get_type d2) (get_type d1); diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2112284ea..81fd1427d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -127,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.section_context -> unit +val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d50..b27e27fda 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,8 @@ open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -160,14 +161,15 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> diff --git a/library/decls.ml b/library/decls.ml index 6e21880f1..2952c258a 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -14,6 +14,8 @@ open Names open Decl_kinds open Libnames +module NamedDecl = Context.Named.Declaration + (** Datas associated to section variables and local definitions *) type variable_data = @@ -46,20 +48,18 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) -open Context.Named.Declaration - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right (fun d signv -> - let id = get_id d in - let d = if variable_opacity id then LocalAssum (id, get_type d) else d in + let id = NamedDecl.get_id d in + let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = Context.Named.fold_outside (fun d sec_ids -> - let id = get_id d in + let id = NamedDecl.get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/impargs.ml b/library/impargs.ml index bce7a15cb..e922ab773 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -22,6 +22,9 @@ open Constrexpr open Termops open Namegen open Decl_kinds +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*s Flags governing the computation of implicit arguments *) @@ -164,7 +167,6 @@ let update pos rig (na,st) = (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env bound depth f = - let open Context.Named.Declaration in match kind_of_term f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true @@ -449,8 +451,7 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let open Context.Named.Declaration in - compute_semi_auto_implicits env flags manual (get_type (lookup_named id env)) + compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) @@ -515,15 +516,11 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,List.smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - let map (id, impl, _, _) = match impl with - | Implicit -> Some (id, Manual, (true, true)) + let map (decl, impl) = match impl with + | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) | _ -> None in - let is_set (_, _, b, _) = match b with - | None -> true - | Some _ -> false - in - List.rev_map map (List.filter is_set ctx) + List.rev_map map (List.filter (is_local_assum % fst) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) diff --git a/library/lib.ml b/library/lib.ml index 8880a8b15..412772e8a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,6 +13,9 @@ open Libnames open Globnames open Nameops open Libobject +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) @@ -388,7 +391,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t @@ -428,12 +431,10 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = - let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> - let (id',b,t) = to_tuple decl in + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r + (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r @@ -443,17 +444,11 @@ let extract_hyps (secs,ohyps) = | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) -let instance_from_variable_context sign = - let rec inst_rec = function - | (id,b,None,_) :: sign -> id :: inst_rec sign - | _ :: sign -> inst_rec sign - | [] -> [] in - Array.of_list (inst_rec sign) - -let named_of_variable_context ctx = let open Context.Named.Declaration in - List.map (function id,_,None,t -> LocalAssum (id,t) - | id,_,Some b,t -> LocalDef (id,b,t)) - ctx +let instance_from_variable_context = + Array.of_list % List.map NamedDecl.get_id % List.filter is_local_assum % List.map fst + +let named_of_variable_context = + List.map fst let add_section_replacement f g poly hyps = match !sectab with diff --git a/library/lib.mli b/library/lib.mli index 7080b5dba..092643c2d 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -162,8 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * - Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 30aeba3bb..c5b26e6d5 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -18,6 +18,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (* The instantiate tactic *) let instantiate_evar evk (ist,rawc) sigma = @@ -48,7 +50,7 @@ let instantiate_tac n c ido = | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> - evar_list (get_type decl) + evar_list (NamedDecl.get_type decl) | InHypValueOnly -> (match decl with | LocalDef (_,body,_) -> evar_list body diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 7acad20d2..ad052cdd1 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -36,6 +36,9 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration + (** Typeclass-based generalized rewriting. *) (** Constants used by the tactic. *) @@ -1527,7 +1530,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let rec insert_dependent env decl accu hyps = match hyps with | [] -> List.rev_append accu [decl] | ndecl :: rem -> - if occur_var_in_decl env (get_id ndecl) decl then + if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then List.rev_append accu (decl :: hyps) else insert_dependent env decl (ndecl :: accu) rem @@ -1537,17 +1540,17 @@ let assert_replacing id newt tac = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ctx = Environ.named_context env in - let after, before = List.split_when (Id.equal id % get_id) ctx in + let after, before = List.split_when (Id.equal id % NamedDecl.get_id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in let map d = - let n = get_id d in + let n = NamedDecl.get_id d in if Id.equal n id then ev' else mkVar n in let (e, _) = destEvar ev in @@ -2088,9 +2091,8 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let open Context.Rel.Declaration in let (sigma, t) = Typing.type_of env sigma rel in - let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in + let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 397cd988d..aa7e096a9 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -388,8 +388,6 @@ let interp_ident ist env sigma id = try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id) with Not_found -> id -let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl) - (* Interprets an optional identifier, bound or fresh *) let interp_name ist env sigma = function | Anonymous -> Anonymous @@ -696,9 +694,6 @@ let interp_typed_pattern ist env sigma (_,c,_) = pattern_of_constr env sigma c (* Interprets a constr expression *) -let pf_interp_constr ist gl = - interp_constr ist (pf_env gl) (project gl) - let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with @@ -720,10 +715,6 @@ let interp_constr_list ist env sigma c = let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr -(* Interprets a type expression *) -let pf_interp_type ist env sigma = - interp_type ist env sigma - (* Interprets a reduction expression *) let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid) @@ -1220,7 +1211,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | TacAbstract (tac,ido) -> Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT - (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) + (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) end } | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) @@ -1706,7 +1697,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = - let (sigma,c_interp) = pf_interp_type ist env sigma c in + let (sigma,c_interp) = interp_type ist env sigma c in sigma , (interp_ident ist env sigma id,n,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) @@ -1721,7 +1712,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let env = pf_env gl in let f sigma (id,c) = - let (sigma,c_interp) = pf_interp_type ist env sigma c in + let (sigma,c_interp) = interp_type ist env sigma c in sigma , (interp_ident ist env sigma id,c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) @@ -1763,7 +1754,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = pf_interp_constr ist gl c in + let (sigma,c_interp) = interp_constr ist env sigma c in let let_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in @@ -1914,7 +1905,7 @@ and interp_atomic ist tac : unit Proofview.tactic = match c with | None -> sigma , None | Some c -> - let (sigma,c_interp) = pf_interp_constr ist gl c in + let (sigma,c_interp) = interp_constr ist env sigma c in sigma , Some c_interp in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fd46d8069..930ab333a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,7 +23,9 @@ open Pp open CErrors open Util open Proofview.Notations -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -155,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -170,7 +172,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -192,10 +194,10 @@ let make_prb gls depth additionnal_terms = ignore (add_term state t)) additionnal_terms; List.iter (fun decl -> - let (id,_,e) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in begin let cid=mkVar id in - match litteral_of_constr env sigma e with + match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97c9d5f4a..8e6c7a70d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -32,6 +32,9 @@ open Misctypes open Sigma.Notations open Context.Named.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Strictness option *) let clear ids { it = goal; sigma } = @@ -247,7 +250,7 @@ let close_previous_case pts = let filter_hyps f gls = let filter_aux id = - let id = get_id id in + let id = NamedDecl.get_id id in if f id then tclIDTAC else @@ -357,8 +360,7 @@ let enstack_subsubgoals env se stack gls= let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in - let open Context.Rel.Declaration in - (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in + (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in @@ -821,9 +823,8 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with - This id -> - let body = pf_get_hyp gls id |> get_value in - Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls + | This id -> + Proofview.V82.of_tactic (pf_get_hyp gls id |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 58744b575..b34a36492 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,8 @@ open Tacmach open Util open Declarations open Globnames -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration let qflag=ref true @@ -141,7 +142,7 @@ let build_atoms gl metagen side cciterm = end; let v = ind_hyps 0 i l gl in let g i _ decl = - build_rec env polarity (lift i (get_type decl)) in + build_rec env polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -152,7 +153,7 @@ let build_atoms gl metagen side cciterm = let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in let g i _ decl = - build_rec (var::env) polarity (lift i (get_type decl)) in + build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -225,7 +226,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in + let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index ffb63af07..7ffc78928 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -19,7 +19,8 @@ open Formula open Sequent open Globnames open Locus -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -36,12 +37,12 @@ let wrap n b continue seq gls= match nc with []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> - let id = get_id nd in + let id = NamedDecl.get_id nd in if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b0ffc775b..f47ab2616 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -16,6 +16,8 @@ open Libnames open Globnames open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* let msgnl = Pp.msgnl *) (* @@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) + (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -938,7 +940,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl decl = Nameops.out_name (get_name decl) +let id_of_decl decl = Nameops.out_name (RelDecl.get_name decl) let var_of_decl decl = mkVar (id_of_decl decl) let revert idl = tclTHEN @@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = map_name fresh_id in + let fresh_decl = RelDecl.map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl))) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let pte_to_fix,rev_info = List.fold_left_i (fun i (acc_map,acc_info) decl -> - let pte = get_name decl in + let pte = RelDecl.get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1277,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) + (args_id@(List.map (fun decl -> Nameops.out_name (RelDecl.get_name decl)) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 5e72b8672..234c3e75e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,8 @@ open Functional_principles_proofs open Misctypes open Sigma.Notations +module RelDecl = Context.Rel.Declaration + exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -38,7 +40,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Name x -> let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; - set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) in let avoid = (Termops.ids_of_context env_with_params ) in @@ -51,7 +53,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod (get_type decl) in + let args,_ = decompose_prod (RelDecl.get_type decl) in let real_args = if princ_type_info.indarg_in_concl then List.tl args diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 52179ae50..4d02c77c8 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -12,6 +12,9 @@ open Util open Glob_termops open Misctypes +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + let observe strm = if do_observe () then Feedback.msg_debug strm @@ -333,19 +336,20 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in - let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in - let open Context.Named.Declaration in - Environ.push_named (of_tuple (id,value,typ)) env + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + (match raw_value with + | None -> + Environ.push_named (NamedDecl.LocalAssum (id,typ)) env + | Some value -> + Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env) let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - let open Context.Rel.Declaration in observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env + | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) typ @@ -353,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = in let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in let new_env = add_pat_variables env pat typ in @@ -361,20 +365,28 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let _,v,t = Context.Rel.Declaration.to_tuple decl in - match Context.Rel.Declaration.get_name decl with - | Anonymous -> assert false - | Name id -> + let open Context.Rel.Declaration in + match decl with + | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false + | LocalAssum (Name id, t) -> + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> let new_t = substl ctxt t in - let new_v = Option.map (substl ctxt) v in + let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -402,8 +414,7 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let open Context.Rel.Declaration in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -602,10 +613,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = - let open Context.Named.Declaration in match n with Anonymous -> env - | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env + | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res @@ -976,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let open Context.Rel.Declaration in - let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in + let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 18817f504..51cf7f4f4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open Context.Rel.Declaration open CErrors open Util open Names @@ -13,11 +12,13 @@ open Misctypes open Decl_kinds open Sigma.Notations +module RelDecl = Context.Rel.Declaration + let is_rec_info scheme_info = let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 26fc88a60..0178c44d0 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,6 +23,8 @@ open Misctypes open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* Some pretty printing function for debugging purpose *) let pr_binding prc = @@ -137,7 +139,7 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | decl :: fun_ctxt -> fun_ctxt, get_type decl + | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function | [] -> accu @@ -148,7 +150,7 @@ let generate_type evd g_to_f f graph i = args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = fun decl -> match get_name decl with + let filter = fun decl -> match RelDecl.get_name decl with | Name id -> Some id | Anonymous -> None in @@ -269,7 +271,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl))))) ) branches in @@ -399,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (get_name decl, get_type decl) :: ctxt) + (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) in res ) @@ -415,7 +417,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -425,7 +427,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -682,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index de4210af5..d9933cf41 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -26,6 +26,8 @@ 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} *) @@ -137,7 +139,7 @@ let showind (id:Id.t) = let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in List.iter (fun decl -> print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); - prconstr (get_type decl); print_string "\n") + prconstr (RelDecl.get_type decl); print_string "\n") ib1.mind_arity_ctxt; Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri @@ -460,12 +462,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array 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 (get_name decl) ^ " : "); - prconstr (get_type decl); prstr "\n") + 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 (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n") + List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n") otherprms2 in { ident=id; @@ -827,7 +829,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = List.fold_left (fun (acc,env) decl -> let nm = Context.Rel.Declaration.get_name decl in - let c = get_type decl in + let c = RelDecl.get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in let newenv = Environ.push_rel (LocalAssum (nm,c)) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f307115..65f96c831 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -377,7 +377,7 @@ type journey_info = let rec add_vars forbidden e = match kind_of_term e with | Var x -> x::forbidden - | _ -> fold_constr add_vars forbidden e + | _ -> Term.fold_constr add_vars forbidden e let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076..1afc6500b 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -30,6 +30,7 @@ open Misctypes open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1697,8 +1698,8 @@ let destructure_hyps = let rec loop = function | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega) | decl::lit -> - let (i,_,t) = to_tuple decl in - begin try match destructurate_prop t with + let i = NamedDecl.get_id decl in + begin try match destructurate_prop (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit | Kapp(Or,[t1;t2]) -> @@ -1808,13 +1809,13 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + decl)) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) - decl)) + (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + decl)) (loop lit)) | _ -> loop lit end diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ca1d0b7fb..ff6b33c49 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -13,6 +13,8 @@ open Term open Environ open Util open Libobject + +module NamedDecl = Context.Named.Declaration (*i*) let name_table = @@ -48,7 +50,7 @@ let discharge_rename_args = function (try let vars,_,_ = section_segment_of_reference c in let c' = pop_global_reference c in - let var_names = List.map (fun (id, _,_,_) -> Name id) vars in + let var_names = List.map (Name.mk_name % NamedDecl.get_id % fst) vars in let names' = List.map (fun l -> var_names @ l) names in Some (ReqGlobal (c', names), (c', names')) with Not_found -> Some req) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fe2b0a5a1..2d8173f94 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -32,6 +32,9 @@ open Evd open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Pattern-matching errors *) type pattern_matching_error = @@ -605,7 +608,7 @@ let relocate_index_tomatch n1 n2 = NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i, map_constr (relocate_index n1 n2 depth) d) + Abstract (i, RelDecl.map_constr (relocate_index n1 n2 depth) d) :: genrec (depth+1) rest in genrec 0 @@ -638,7 +641,7 @@ let replace_tomatch n c = | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i, map_constr (replace_term n c depth) d) + Abstract (i, RelDecl.map_constr (replace_term n c depth) d) :: replrec (depth+1) rest in replrec 0 @@ -663,7 +666,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i, map_constr (liftn n depth) d) + Abstract (i, RelDecl.map_constr (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -731,7 +734,7 @@ let get_names env sign eqns = (* We now replace the names y1 .. yn y by the actual names *) (* xi1 .. xin xi to be found in the i-th clause of the matrix *) -let recover_initial_subpattern_names = List.map2 set_name +let recover_initial_subpattern_names = List.map2 RelDecl.set_name let recover_and_adjust_alias_names names sign = let rec aux = function @@ -756,11 +759,11 @@ let push_rels_eqn_with_names sign eqn = push_rels_eqn sign eqn let push_generalized_decl_eqn env n decl eqn = - match get_name decl with + match RelDecl.get_name decl with | Anonymous -> push_rels_eqn [decl] eqn | Name _ -> - push_rels_eqn [set_name (get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn + push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn let drop_alias_eqn eqn = { eqn with alias_stack = List.tl eqn.alias_stack } @@ -768,7 +771,7 @@ let drop_alias_eqn eqn = let push_alias_eqn alias eqn = let aliasname = List.hd eqn.alias_stack in let eqn = drop_alias_eqn eqn in - let alias = set_name aliasname alias in + let alias = RelDecl.set_name aliasname alias in push_rels_eqn [alias] eqn (**********************************************************************) @@ -1195,7 +1198,7 @@ let rec generalize_problem names pb = function | LocalDef (Anonymous,_,_) -> pb', deps | _ -> (* for better rendering *) - let d = map_type (whd_betaiota !(pb.evdref)) d in + let d = RelDecl.map_type (whd_betaiota !(pb.evdref)) d in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = relocate_index_tomatch (i+1) 1 tomatch in { pb' with @@ -1223,7 +1226,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* that had matched constructor C *) let cs_args = const_info.cs_args in let names,aliasname = get_names pb.env cs_args eqns in - let typs = List.map2 set_name names cs_args + let typs = List.map2 RelDecl.set_name names cs_args in (* We build the matrix obtained by expanding the matching on *) @@ -1273,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs' = List.map2 (fun (tm, (tmtyp,_), decl) deps -> - let na = get_name decl in + let na = RelDecl.get_name decl in let na = match curname, na with | Name _, Anonymous -> curname | Name _, Name _ -> na @@ -1658,8 +1661,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = List.map (fun a -> not (isRel a) || dependent a u || Int.Set.mem (destRel a) depvl) inst in let named_filter = - let open Context.Named.Declaration in - List.map (fun d -> dependent (mkVar (get_id d)) u) + List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u) (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in @@ -1755,7 +1757,7 @@ let build_inversion_problem loc env sigma tms t = let sub_tms = List.map2 (fun deps (tm, (tmtyp,_), decl) -> - let na = if List.is_empty deps then Anonymous else force_name (get_name decl) in + let na = if List.is_empty deps then Anonymous else force_name (RelDecl.get_name decl) in Pushed (true,((tm,tmtyp),deps,na))) dep_sign decls in let subst = List.map (fun (na,t) -> (na,lift n t)) subst in @@ -1818,7 +1820,7 @@ let build_initial_predicate arsign pred = let rec buildrec n pred tmnames = function | [] -> List.rev tmnames,pred | (decl::realdecls)::lnames -> - let na = get_name decl in + let na = RelDecl.get_name decl in let n' = n + List.length realdecls in buildrec (n'+1) pred (force_name na::tmnames) lnames | _ -> assert false @@ -1851,7 +1853,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in LocalAssum (na, build_dependent_inductive env0 indf') - ::(List.map2 set_name realnal arsign) in + ::(List.map2 RelDecl.set_name realnal arsign) in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> @@ -2048,7 +2050,7 @@ let constr_of_pat env evdref arsign pat avoid = let patargs, args, sign, env, n, m, avoid = List.fold_right2 (fun decl ua (patargs, args, sign, env, n, m, avoid) -> - let t = get_type decl in + let t = RelDecl.get_type decl in let pat', sign', arg', typ', argtypargs, n', avoid = let liftt = liftn (List.length sign) (succ (List.length args)) t in typ env (substl args liftt, []) ua avoid @@ -2088,8 +2090,8 @@ let constr_of_pat env evdref arsign pat avoid = (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in - let pat', sign, patc, patty, args, z, avoid = typ env (get_type (List.hd arsign), List.tl arsign) pat avoid in - pat', (sign, patc, (get_type (List.hd arsign), args), pat'), avoid + let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in + pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid (* shadows functional version *) @@ -2120,7 +2122,7 @@ let vars_of_ctx ctx = (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), [hole; GVar (Loc.ghost, prev)])) :: vars | _ -> - match get_name decl with + match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" | Name n -> n, GVar (Loc.ghost, n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) @@ -2297,7 +2299,7 @@ let abstract_tomatch env tomatchs tycon = let build_dependent_signature env evdref avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in - let allnames = List.rev_map (List.map get_name) arsign in + let allnames = List.rev_map (List.map RelDecl.get_name) arsign in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let eqs, neqs, refls, slift, arsign' = List.fold_left2 @@ -2314,14 +2316,14 @@ let build_dependent_signature env evdref avoid tomatchs arsign = as much as possible *) let argsign = List.tl arsign in (* arguments in inverse application order *) let app_decl = List.hd arsign in (* The matched argument *) - let appn = get_name app_decl in - let appt = get_type app_decl in + let appn = RelDecl.get_name app_decl in + let appt = RelDecl.get_type app_decl in let argsign = List.rev argsign in (* arguments in application order *) let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl -> - let name = get_name decl in - let t = get_type decl in + let name = RelDecl.get_name decl in + let t = RelDecl.get_type decl in let argt = Retyping.get_type_of env !evdref arg in let eq, refl_arg = if Reductionops.is_conv env !evdref argt t then @@ -2339,7 +2341,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = let previd, id = let name = match kind_of_term arg with - Rel n -> get_name (lookup_rel n env) + Rel n -> RelDecl.get_name (lookup_rel n env) | _ -> name in make_prime avoid name @@ -2348,7 +2350,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, refl_arg :: refl_args, pred slift, - set_name (Name id) decl :: argsign')) + RelDecl.set_name (Name id) decl :: argsign')) (env, neqs, [], [], slift, []) args argsign in let eq = mk_JMeq evdref @@ -2363,13 +2365,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign = succ nargeqs, refl_eq :: refl_args, pred slift, - ((set_name (Name id) app_decl :: argsign') :: arsigns)) + ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) | _ -> (* Non dependent inductive or not inductive, just use a regular equality *) let decl = match arsign with [x] -> x | _ -> assert(false) in - let name = get_name decl in + let name = RelDecl.get_name decl in let previd, id = make_prime avoid name in - let arsign' = set_name (Name id) decl in + let arsign' = RelDecl.set_name (Name id) decl in let tomatch_ty = type_of_tomatch ty in let eq = mk_eq evdref (lift nar tomatch_ty) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f39..553786f58 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -153,7 +153,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env evdref x y in let dest_prod c = - let open Context.Rel.Declaration in match Reductionops.splay_prod_n env ( !evdref) 1 c with | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c | _ -> raise NoSubtacCoercion diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0fea2ba22..e745824b8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -24,7 +24,10 @@ open Globnames open Evd open Pretype_errors open Sigma.Notations -open Context.Rel.Declaration +open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -58,14 +61,13 @@ let eval_flexible_term ts env evd c = else None | Rel n -> (try match lookup_rel n env with - | LocalAssum _ -> None - | LocalDef (_,v,_) -> Some (lift n v) + | RelDecl.LocalAssum _ -> None + | RelDecl.LocalDef (_,v,_) -> Some (lift n v) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -394,7 +396,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty assert (match sk with [] -> true | _ -> false); let (na,c1,c'1) = destLambda term in let c = nf_evar evd c1 in - let env' = push_rel (LocalAssum (na,c)) env in + let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd @@ -600,7 +602,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let b = nf_evar i b1 in let t = nf_evar i t1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2); + evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) @@ -715,7 +717,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -774,7 +776,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let c = nf_evar i c1 in let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)] + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -951,7 +953,6 @@ let choose_less_dependent_instance evk evd term args = | [] -> None | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) -open Context.Named.Declaration let apply_on_subterm env evdref f c t = let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) @@ -982,14 +983,16 @@ let filter_possible_projections c ty ctxt args = List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in - (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) || + (match decl with + | NamedDecl.LocalAssum _ -> false + | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) (* in u *) isRel a && Int.Set.mem (destRel a) fv1 || isVar a && Id.Set.mem (destVar a) fv2 || - Id.Set.mem (get_id decl) tyvars) + Id.Set.mem (NamedDecl.get_id decl) tyvars) 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") @@ -1020,10 +1023,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map get_id ctxt) in + let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c -> + | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> error "Cannot force abstraction on identity instance." @@ -1031,7 +1034,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = make_subst (ctxt',l,occsl) end | decl'::ctxt', c::l, occs::occsl -> - let (id,_,t) = to_tuple decl' in + let id = NamedDecl.get_id decl' in + let t = NamedDecl.get_type decl' in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections c ty ctxt args in diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f9ab75cea..29eb00c61 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -19,21 +19,21 @@ open Evarutil open Pretype_errors open Sigma.Notations +module RelDecl = Context.Rel.Declaration + let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in (Sigma.to_evar_map evd, evk) let env_nf_evar sigma env = - let open Context.Rel.Declaration in process_rel_context - (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env + (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env let env_nf_betaiotaevar sigma env = - let open Context.Rel.Declaration in process_rel_context (fun d e -> - push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env + push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6c8677855..c0a42ae7d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -632,13 +632,13 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in - let evd,b_in_sign = match d with - | LocalAssum _ -> evd,None + let evd,d' = match d with + | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign) | LocalDef (_,b,_) -> let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in - evd,Some b in - (push_named_context_val (Context.Named.Declaration.of_tuple (id,b_in_sign,t_in_sign)) sign, Filter.extend 1 filter, + evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in + (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), push_rel d env,evd,id::avoid)) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e992..1f9573862 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -16,6 +16,8 @@ open Nameops open Termops open Pretype_errors +module NamedDecl = Context.Named.Declaration + (** Processing occurrences *) type occurrence_error = @@ -61,7 +63,7 @@ let proceed_with_occurrences f occs x = let map_named_declaration_with_hyploc f hyploc acc decl = let open Context.Named.Declaration in - let f = f (Some (get_id decl, hyploc)) in + let f = f (Some (NamedDecl.get_id decl, hyploc)) in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> error_occurrences_error (IncorrectInValueOccurrence id) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0dd64697c..ffb9f8940 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -20,6 +20,8 @@ open Nativecode open Nativevalues open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (** This module implements normalization by evaluation to OCaml code *) exception Find_at of int @@ -122,7 +124,7 @@ let build_case_type dep p realargs c = (* TODO move this function *) let type_of_rel env n = - lookup_rel n env |> get_type |> lift n + lookup_rel n env |> RelDecl.get_type |> lift n let type_of_prop = mkSort type1_sort diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f46674003..0f85dc629 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -44,7 +44,8 @@ open Evarconv open Pattern open Misctypes open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t @@ -461,7 +462,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -506,7 +507,7 @@ let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (get_type (lookup_named id env)) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -1044,8 +1045,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = - let id = get_id decl in - let t = replace_vars subst (get_type decl) in + let id = NamedDecl.get_id decl in + let t = replace_vars subst (NamedDecl.get_type decl) in let c, update = try let c = List.assoc id update in @@ -1057,7 +1058,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try - let t' = lookup_named id env |> get_type in + let t' = lookup_named id env |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 98b36fb92..5b67af3e7 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -20,6 +20,9 @@ open Termops open Arguments_renaming open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type retype_error = | NotASort | NotAnArity @@ -78,8 +81,7 @@ let sort_of_atomic_type env sigma ft args = in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = - let open Context.Named.Declaration in - try get_type (lookup_named id env) + try NamedDecl.get_type (lookup_named id env) with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = @@ -94,7 +96,7 @@ let retype ?(polyprop=true) sigma = (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus with Not_found -> retype_error (BadMeta n)) | Rel n -> - let ty = get_type (lookup_rel n env) in + let ty = RelDecl.get_type (lookup_rel n env) in lift n ty | Var id -> type_of_var env id | Const cst -> rename_type_of_constant env cst @@ -239,7 +241,7 @@ let sorts_of_context env evc ctxt = | [] -> env,[] | d :: ctxt -> let env,sorts = aux ctxt in - let s = get_sort_of env evc (get_type d) in + let s = get_sort_of env evc (RelDecl.get_type d) in (push_rel d env,s::sorts) in snd (aux ctxt) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 820a81b5d..c1d4a3403 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -25,6 +25,9 @@ open Patternops open Locus open Sigma.Notations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Errors *) type reduction_tactic_error = @@ -54,13 +57,12 @@ let is_evaluable env = function | EvalVarRef id -> is_evaluable_var env id let value_of_evaluable_ref env evref u = - let open Context.Named.Declaration in match evref with | EvalConstRef con -> (try constant_value_in env (con,u) with NotEvaluableConst IsProj -> raise (Invalid_argument "value_of_evaluable_ref")) - | EvalVarRef id -> lookup_named id env |> get_value |> Option.get + | EvalVarRef id -> lookup_named id env |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst @@ -112,22 +114,18 @@ let unsafe_reference_opt_value env sigma eval = | Declarations.Def c -> Some (Mod_subst.force_constr c) | _ -> None) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev let reference_opt_value env sigma eval u = match eval with | EvalConst cst -> constant_opt_value_in env (cst,u) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable @@ -541,11 +539,9 @@ let match_eval_ref_value env sigma constr = | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> Some (constant_value_in env (sp, u)) | Var id when is_evaluable env (EvalVarRef id) -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + lookup_named id env |> NamedDecl.get_value | Rel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value + lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value | Evar ev -> Evd.existential_opt_value sigma ev | _ -> None diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2c675b9ea..c3cdb361b 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -17,6 +17,9 @@ open Util open Typeclasses_errors open Libobject open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (*i*) let typeclasses_unique_solutions = ref false @@ -181,7 +184,7 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (map_constr do_subst) in + let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, do_subst_ctx ctx in @@ -197,19 +200,16 @@ let subst_class (subst,cl) = let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right - ( fun (n,_,b,t) (ctx', subst) -> - let decl = match b with - | None -> LocalAssum (Name n, substn_vars 1 subst t) - | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t) - in - (decl :: ctx', n :: subst) + ( fun (decl,_) (ctx', subst) -> + let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in + (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right (fun decl (ctx, k) -> - map_constr (substn_vars k subst) decl :: ctx, succ k + RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k ) rel ([], n) in ctx @@ -222,7 +222,7 @@ let discharge_class (_,cl) = let discharge_context ctx' subst (grs, ctx) = let grs' = let newgrs = List.map (fun decl -> - match decl |> get_type |> class_of_constr with + match decl |> RelDecl.get_type |> class_of_constr with | None -> None | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) ctx' diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6d80db645..213eecc6b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -29,7 +29,9 @@ open Locus open Locusops open Find_subterm open Sigma.Notations -open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { @@ -78,9 +80,8 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = List.fold_left2 (fun (t,evd) (locc,a) decl -> - let open Context.Rel.Declaration in - let na = get_name decl in - let ta = get_type decl in + let na = RelDecl.get_name decl in + let ta = RelDecl.get_type decl in let na = match kind_of_term a with Var id -> Name id | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... @@ -1473,10 +1474,10 @@ let indirectly_dependent c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl (mkVar (get_id d')) d) decls + List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls let indirect_dependency d decls = - decls |> List.filter (fun d' -> dependent_in_decl (mkVar (get_id d')) d) |> List.hd |> get_id + decls |> List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let current_sigma = Sigma.to_evar_map current_sigma in @@ -1595,7 +1596,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let likefirst = clause_with_generic_occurrences occs in let mkvarid () = mkVar id in let compute_dependency _ d (sign,depdecls) = - let hyp = get_id d in + let hyp = NamedDecl.get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> if indirectly_dependent c d depdecls then @@ -1632,7 +1633,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = - if List.is_empty depdecls then None else Some (get_id (List.last depdecls)) in + if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in let res = match out test with | None -> None | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma)) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c396f593b..331ad0912 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -17,6 +17,9 @@ open Reduction open Vm open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (*******************************************) (* Calcul de la forme normal d'un terme *) (*******************************************) @@ -203,12 +206,11 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk = in nf_univ_args ~nb_univs mk env stk | VarKey id -> - let open Context.Named.Declaration in - let ty = get_type (lookup_named id env) in + let ty = NamedDecl.get_type (lookup_named id env) in nf_stk env (mkVar id) ty stk | RelKey i -> let n = (nb_rel env - i) in - let ty = get_type (lookup_rel n env) in + let ty = RelDecl.get_type (lookup_rel n env) in nf_stk env (mkRel n) (lift n ty) stk and nf_stk ?from:(from=0) env c t stk = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9..37098e504 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -27,6 +27,10 @@ open Recordops open Misctypes open Printer open Printmod +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; @@ -132,7 +136,6 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let open Context.Rel.Declaration in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in @@ -170,9 +173,8 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = - let open Context.Named.Declaration in function - | VarRef v when is_local_def (Environ.lookup_named v env) -> + | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -733,8 +735,7 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let open Context.Named.Declaration in - str |> Global.lookup_named |> set_id str |> print_named_decl + str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -762,8 +763,7 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let open Context.Named.Declaration in - lookup_named id env |> set_id id |> print_named_decl + lookup_named id env |> NamedDecl.set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/printing/printer.ml b/printing/printer.ml index 28fd92659..5c62c2af0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,6 +22,10 @@ open Constrextern open Ppconstr open Declarations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module NamedListDecl = Context.NamedList.Declaration + let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = @@ -248,31 +252,36 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl_skel pr_id env sigma (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str" := " ++ pb ++ cut () ) in +let pr_var_list_decl env sigma decl = + let ids, pbody, typ = match decl with + | NamedListDecl.LocalAssum (ids, typ) -> + ids, mt (), typ + | NamedListDecl.LocalDef (ids,c,typ) -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + ids, (str" := " ++ pb ++ cut ()), typ + in + let pids = prlist_with_sep pr_comma pr_id ids in let pt = pr_ltype_env env sigma typ in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) - -let pr_var_decl env sigma d = - pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) - -let pr_var_list_decl env sigma (l,c,typ) = - hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) + hov 0 (pids ++ pbody ++ ptyp) + +let pr_var_decl env sigma decl = + let decl = match decl with + | NamedDecl.LocalAssum (id, t) -> + NamedListDecl.LocalAssum ([id], t) + | NamedDecl.LocalDef (id,c,t) -> + NamedListDecl.LocalDef ([id],c,t) + in + pr_var_list_decl env sigma decl let pr_rel_decl env sigma decl = - let open Context.Rel.Declaration in - let na = get_name decl in - let typ = get_type decl in + let na = RelDecl.get_name decl in + let typ = RelDecl.get_type decl in let pbody = match decl with - | LocalAssum _ -> mt () - | LocalDef (_,c,_) -> + | RelDecl.LocalAssum _ -> mt () + | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -417,8 +426,7 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let open Context.Named.Declaration in - let ids = List.rev_map get_id l in + let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") diff --git a/proofs/goal.ml b/proofs/goal.ml index 111a947a9..75f56c6b9 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -10,7 +10,8 @@ open Util open Pp open Term open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated @@ -77,7 +78,7 @@ module V82 = struct let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (mkVar % get_id) ctxt in + let inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in let ev = Term.mkEvar (evk,inst) in (evk, ev, evars) @@ -148,7 +149,7 @@ module V82 = struct let env = env sigma gl in let genv = Global.env () in let is_proof_var decl = - try ignore (Environ.lookup_named (get_id decl) genv); false + try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then diff --git a/proofs/logic.ml b/proofs/logic.ml index aa0b9bac6..e12fe5d70 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -24,6 +24,8 @@ open Retyping open Misctypes open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + type refiner_error = (* Errors raised by the refiner *) @@ -162,7 +164,7 @@ let reorder_context env sign ord = (match ctxt_head with | [] -> error_no_such_hypothesis (List.hd ord) | d :: ctxt -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x expected then step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail @@ -178,7 +180,7 @@ let reorder_val_context env sign ord = let check_decl_position env sign d = - let x = get_id d in + let x = NamedDecl.get_id d in let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then @@ -204,8 +206,8 @@ let move_location_eq m1 m2 = match m1, m2 with let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | d :: right -> - if Id.equal (get_id d) h then - match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst + if Id.equal (NamedDecl.get_id d) h then + match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst else get_hyp_after h right @@ -213,7 +215,7 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | d :: right -> - let hyp,_,typ = to_tuple d in + let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -235,24 +237,24 @@ let move_hyp toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (get_id d2) d - else occur_var_in_decl env (get_id d) d2 + then occur_var_in_decl env (NamedDecl.get_id d2) d + else occur_var_in_decl env (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) -> + | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right | d :: right -> - let hyp = get_id d in + let hyp = NamedDecl.get_id d in let (first',middle') = if List.exists (test_dep d) middle then if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ + errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -295,9 +297,9 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind_of_term c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | (App _| Case _) -> fold_constr (collrec deep) acc c + | (App _| Case _) -> Term.fold_constr (collrec deep) acc c | Proj (_, c) -> collrec deep acc c - | _ -> fold_constr (collrec true) acc c + | _ -> Term.fold_constr (collrec true) acc c in List.rev (collrec false [] c) @@ -489,15 +491,16 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp check sign sigma d = - let id,b,bt = to_tuple d in + let id = NamedDecl.get_id d in + let b = NamedDecl.get_value d in let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp check sign id (fun _ d' _ -> - let _,c,ct = to_tuple d' in + let c = NamedDecl.get_value d' in let env = Global.env_of_context sign in - if check && not (is_conv env sigma bt ct) then + if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then errorlabstrm "Logic.convert_hyp" (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1a..9b0200039 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -130,8 +130,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** [set_used_variables l] declares that section variables [l] will be used in the proof *) val set_used_variables : - Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list -val get_used_variables : unit -> Context.section_context option + Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list +val get_used_variables : unit -> Context.Named.t option (** {6 Universe binders } *) val get_universe_binders : unit -> universe_binders option diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7605f6387..17cc92803 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -18,6 +18,8 @@ open Util open Pp open Names +module NamedDecl = Context.Named.Declaration + (*** Proof Modes ***) (* Type of proof modes : @@ -89,7 +91,7 @@ type pstate = { pid : Id.t; terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; - section_vars : Context.section_context option; + section_vars : Context.Named.t option; proof : Proof.proof; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; @@ -276,7 +278,7 @@ let set_used_variables l = let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 59daa2968..86fc1deff 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -143,8 +143,8 @@ val set_interp_tac : * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list -val get_used_variables : unit -> Context.section_context option + Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list +val get_used_variables : unit -> Context.Named.t option val get_universe_binders : unit -> universe_binders option diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index caa9b328a..a125fb10d 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -12,6 +12,8 @@ open Util open Vernacexpr open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let to_string e = let rec aux = function | SsEmpty -> "()" @@ -35,12 +37,14 @@ let in_nameset = let rec close_fwd e s = let s' = List.fold_left (fun s decl -> - let (id,b,ty) = Context.Named.Declaration.to_tuple decl in - let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in - let vty = global_vars_set e ty in + let vb = match decl with + | LocalAssum _ -> Id.Set.empty + | LocalDef (_,b,_) -> global_vars_set e b + in + let vty = global_vars_set e (NamedDecl.get_type decl) in let vbty = Id.Set.union vb vty in if Id.Set.exists (fun v -> Id.Set.mem v s) vbty - then Id.Set.add id (Id.Set.union s vbty) else s) + then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s) s (named_context e) in if Id.Set.equal s s' then s else close_fwd e s' @@ -63,13 +67,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id and full_set env = - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in diff --git a/proofs/refine.ml b/proofs/refine.ml index 76e2d7dc5..139862b8f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -11,6 +11,8 @@ open Sigma.Notations open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let extract_prefix env info = let ctx1 = List.rev (Environ.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in @@ -26,7 +28,7 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = get_type decl in + let t = NamedDecl.get_type decl in let evdref = ref sigma in let _ = Typing.e_sort_of env evdref t in let () = match decl with diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ea8543b02..fdd0df445 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,7 +13,8 @@ open Evd open Environ open Proof_type open Logic -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -202,7 +203,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) let { it = gls; sigma = sigma; } = rslt in let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,7 +216,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in Feedback.msg_notice diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 50984c48e..957843bc9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -21,6 +21,8 @@ open Refiner open Sigma.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let re_sig it gc = { it = it; sigma = gc; } (**************************************************************) @@ -46,7 +48,7 @@ let pf_hyps_types gls = | LocalDef (id,_,x) -> id, x) sign -let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) @@ -57,7 +59,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - pf_get_hyp gls id |> get_type + pf_get_hyp gls id |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -199,7 +201,7 @@ module New = struct sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> get_type + pf_get_hyp id gl |> NamedDecl.get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb2f0351d..5e4e34114 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -33,6 +33,9 @@ open Constrintern open Impargs open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = @@ -45,8 +48,7 @@ let call_hook fix_exn hook l c = let retrieve_first_recthm = function | VarRef id -> - let open Context.Named.Declaration in - (get_value (Global.lookup_named id),variable_opacity id) + (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -110,7 +112,7 @@ let find_mutually_recursive_statements thms = (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> - let t = get_type decl in + let t = RelDecl.get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in @@ -456,7 +458,7 @@ let start_proof_com kind thms hook = let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); - let ids = List.map get_name ctx in + let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6e01a676a..8c43ac8b5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -32,6 +32,8 @@ open Misctypes open Proofview.Notations open Hints +module NamedDecl = Context.Named.Declaration + (** Hint database named "typeclass_instances", now created directly in Auto *) (** Options handling *) @@ -523,9 +525,8 @@ let evars_to_goals p evm = (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = - let open Context.Named.Declaration in - let id = get_id decl in - let cty = Evarutil.nf_evar sigma (get_type decl) in + let id = NamedDecl.get_id decl in + let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in let rec iscl env ty = let ctx, ar = decompose_prod_assum ty in match kind_of_term (fst (decompose_app ar)) with @@ -564,10 +565,9 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = - let open Context.Named.Declaration in - try let t = Global.lookup_named (get_id hyp) |> get_type in + try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (get_type hyp)) + not (Term.eq_constr t (NamedDecl.get_type hyp)) with Not_found -> true in if consider then diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c3796b484..c81705c1a 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -13,7 +13,8 @@ open Coqlib open Reductionops open Misctypes open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Absurd *) @@ -46,7 +47,7 @@ let absurd c = absurd c let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (get_type d) -> tac (get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -60,8 +61,8 @@ let contradiction_context = let rec seek_neg l = match l with | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> - let id = get_id d in - let typ = nf_evar sigma (get_type d) in + let id = NamedDecl.get_id d in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in if is_empty_type typ then simplest_elim (mkVar id) diff --git a/tactics/elim.ml b/tactics/elim.ml index f2b9eec4b..3f0c01a29 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -16,7 +16,8 @@ open Tacmach.New open Tacticals.New open Tactics open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = @@ -139,7 +140,7 @@ let induction_trailer abs_i abs_j bargs = let (hyps,_) = List.fold_left (fun (bring_ids,leave_ids) d -> - let cid = get_id d in + let cid = NamedDecl.get_id d in if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4..c94dcfa9d 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -60,6 +60,8 @@ open Indrec open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InProp | InSet -> hid | InType -> xid @@ -600,9 +602,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') = | hp :: p :: ind :: indargs -> let c' = my_it_mkLambda_or_LetIn indargs - (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p) - (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp) - (mkLambda_or_LetIn (map_constr (lift 2) ind) + (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) + (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) + (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) (Reductionops.whd_beta Evd.empty (applist (c, Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) @@ -741,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind = if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in - let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in + let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then diff --git a/tactics/equality.ml b/tactics/equality.ml index 3e5b7b65f..d078532b5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -45,6 +45,8 @@ open Proofview.Notations open Unification open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (* Options *) let discriminate_introduction = ref true @@ -1662,13 +1664,13 @@ exception FoundHyp of (Id.t * constr * bool) (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) let is_eq_x gl x d = - let id = get_id d in + let id = NamedDecl.get_id d in try let is_var id c = match kind_of_term c with | Var id' -> Id.equal id id' | _ -> false in - let c = pf_nf_evar gl (get_type d) in + let c = pf_nf_evar gl (NamedDecl.get_type d) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false)) @@ -1686,7 +1688,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = (* The set of hypotheses using x *) let dephyps = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> - let id = get_id dcl in + let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then @@ -1715,9 +1717,9 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in - let xval = pf_get_hyp x gl |> get_value in + let decl = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) - if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else + if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else (* Find a non-recursive definition for x *) let res = try @@ -1763,12 +1765,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = find_eq_data_decompose gl in let test decl = try - let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in + let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (get_id decl) + Some (NamedDecl.get_id decl) | _ -> None with Constr_matching.PatternMatchingFailure -> None @@ -1782,7 +1784,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> get_type in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else @@ -1851,10 +1853,10 @@ let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with | [] -> error "No such assumption." | hyp ::rest -> - let id = get_id hyp in + let id = NamedDecl.get_id hyp in begin try - let dir = cond_eq_term (get_type hyp) gl in + let dir = cond_eq_term (NamedDecl.get_type hyp) gl in general_rewrite_clause dir false (mkVar id,NoBindings) cl with | Failure _ | UserError _ -> arec rest gl end diff --git a/tactics/hints.ml b/tactics/hints.ml index 8f3eb5eb5..a74fceb8f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -34,7 +34,8 @@ open Tacred open Printer open Vernacexpr open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (****************************************) (* General functions *) @@ -782,11 +783,11 @@ let make_resolves env sigma flags pri poly ?name cr = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma decl = - let hname = get_id decl in + let hname = NamedDecl.get_id decl in try [make_apply_entry env sigma (true, true, false) None false ~name:(PathHints [VarRef hname]) - (mkVar hname, get_type decl, Univ.ContextSet.empty)] + (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc469..36770925f 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -19,6 +19,8 @@ open Declarations open Tacmach.New open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjuction, a general disjunction, or a type with no constructors. @@ -100,7 +102,7 @@ let match_with_one_constructor style onlybinary allow_rec t = (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in if List.for_all - (fun decl -> let c = get_type decl in + (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && isRel c && Int.equal (destRel c) mib.mind_nparams) ctx @@ -109,7 +111,7 @@ let match_with_one_constructor style onlybinary allow_rec t = else None else let ctyp = prod_applist mip.mind_nf_lc.(0) args in - let cargs = List.map get_type (prod_assum ctyp) in + let cargs = List.map RelDecl.get_type (prod_assum ctyp) in if not (is_lax_conjunction style) || has_nodep_prod ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) diff --git a/tactics/inv.ml b/tactics/inv.ml index bda16b01c..575710ecc 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -28,7 +28,8 @@ open Misctypes open Tacexpr open Sigma.Notations open Proofview.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in @@ -182,7 +183,7 @@ let dependent_hyps env id idlist gl = | [] -> [] | d::l -> (* Update the type of id1: it may have been subject to rewriting *) - let d = pf_get_hyp (get_id d) gl in + let d = pf_get_hyp (NamedDecl.get_id d) gl in if occur_var_in_decl env id d then d :: dep_rec l else dep_rec l @@ -192,7 +193,7 @@ let dependent_hyps env id idlist gl = let split_dep_and_nodep hyps gl = List.fold_right (fun d (l1,l2) -> - if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2)) + if var_occurs_in_pf gl (NamedDecl.get_id d) then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) (* Computation of dids is late; must have been done in rewrite_equations*) @@ -383,7 +384,7 @@ let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.nf_enter { enter = begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in - let avoid = if as_mode then List.map get_id nodepids else [] in + let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in match othin with | Some thin -> tclTHENLIST @@ -399,10 +400,10 @@ let rewrite_equations as_mode othin neqns names ba = tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) - let idopt = if as_mode then Some (get_id d) else None in + let idopt = if as_mode then Some (NamedDecl.get_id d) else None in intro_move idopt (if thin then MoveLast else !first_eq)) nodepids; - (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)] + (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 642bf520b..1639ec54c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -29,6 +29,8 @@ open Decl_kinds open Proofview.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ pr_lconstr_env env sigma constr ++ @@ -156,7 +158,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env d (revargs,hyps) -> - let id = get_id d in + let id = NamedDecl.get_id d in if Id.List.mem id ivars then ((mkVar id)::revargs, Context.Named.add d hyps) else @@ -206,7 +208,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context (get_id d) global_named_context then sign + if mem_named_context (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml index 004492e78..a5ccd500c 100644 --- a/tactics/tactic_matching.ml +++ b/tactics/tactic_matching.ml @@ -13,6 +13,8 @@ open Names open Tacexpr open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** [t] is the type of matching successes. It ultimately contains a {!Tacexpr.glob_tactic_expr} representing the left-hand side of the corresponding matching rule, a matching substitution to be @@ -280,9 +282,9 @@ module PatternMatching (E:StaticEnvironment) = struct the name of the matched hypothesis. *) let hyp_match_type hypname pat hyps = pick hyps >>= fun decl -> - let id = get_id decl in + let id = NamedDecl.get_id decl in let refresh = is_local_def decl in - pattern_match_term refresh pat (get_type decl) () <*> + pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> return id @@ -319,7 +321,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* spiwack: alternatively it is possible to return the list with the matched hypothesis removed directly in [hyp_match]. *) - let select_matched_hyp decl = Id.equal (get_id decl) matched_hyp in + let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in let hyps = CList.remove_first select_matched_hyp hyps in hyp_pattern_list_match pats hyps lhs | [] -> return lhs diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d..664629f34 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,7 +16,8 @@ open Declarations open Tacmach open Clenv open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -70,7 +71,7 @@ let nthDecl m gl = try List.nth (pf_hyps gl) (m-1) with Failure _ -> error "No such assumption." -let nthHypId m gl = nthDecl m gl |> get_id +let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) let lastDecl gl = nthDecl 1 gl @@ -81,7 +82,7 @@ let nLastDecls n gl = try List.firstn n (pf_hyps gl) with Failure _ -> error "Not enough hypotheses in the goal." -let nLastHypsId n gl = List.map get_id (nLastDecls n gl) +let nLastHypsId n gl = List.map NamedDecl.get_id (nLastDecls n gl) let nLastHyps n gl = List.map mkVar (nLastHypsId n gl) let onNthDecl m tac gl = tac (nthDecl m gl) gl @@ -99,7 +100,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac let onNLastHyps n tac = onHyps (nLastHyps n) tac let afterHyp id gl = - fst (List.split_when (Id.equal id % get_id) (pf_hyps gl)) + fst (List.split_when (Id.equal id % NamedDecl.get_id) (pf_hyps gl)) (***************************************) (* Clause Tacticals *) @@ -560,7 +561,7 @@ module New = struct let nthHypId m gl = (** We only use [id] *) let gl = Proofview.Goal.assume gl in - nthDecl m gl |> get_id + nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -592,7 +593,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let rem, _ = List.split_when (Id.equal id % get_id) hyps in + let rem, _ = List.split_when (Id.equal id % NamedDecl.get_id) hyps in tac rem end } diff --git a/tactics/tactics.ml b/tactics/tactics.ml index acc0fa1ca..7ee45523f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,6 +43,10 @@ open Locusops open Misctypes open Proofview.Notations open Sigma.Notations +open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let inj_with_occurrences e = (AllOccurrences,e) @@ -162,19 +166,17 @@ let _ = (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env store decl b = - let open Context.Named.Declaration in Refine.refine ~unsafe:true { run = begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in - let inst = List.map (mkVar % get_id) (named_context env) in + let inst = List.map (mkVar % NamedDecl.get_id) (named_context env) in let ninst = mkRel 1 :: inst in - let nb = subst1 (mkVar (get_id decl)) b in + let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) end } let introduction ?(check=true) id = - let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in @@ -186,6 +188,7 @@ let introduction ?(check=true) id = errorlabstrm "Tactics.introduction" (str "Variable " ++ pr_id id ++ str " is already declared.") in + let open Context.Named.Declaration in match kind_of_term (whd_evar sigma concl) with | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b @@ -317,7 +320,6 @@ let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest) (* Renaming hypotheses *) let rename_hyp repl = - let open Context.Named.Declaration in let fold accu (src, dst) = match accu with | None -> None | Some (srcs, dsts) -> @@ -339,7 +341,7 @@ let rename_hyp repl = let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in (** Check that we do not mess variables *) - let fold accu decl = Id.Set.add (get_id decl) accu in + let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in let vars = List.fold_left fold Id.Set.empty hyps in let () = if not (Id.Set.subset src vars) then @@ -358,13 +360,13 @@ let rename_hyp repl = let subst = List.map make_subst repl in let subst c = Vars.replace_vars subst c in let map decl = - decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) - |> map_constr subst + decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id) + |> NamedDecl.map_constr subst in let nhyps = List.map map hyps in let nconcl = subst concl in let nctx = Environ.val_of_named_context nhyps in - let instance = List.map (mkVar % get_id) hyps in + let instance = List.map (mkVar % NamedDecl.get_id) hyps in Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar_instance nctx sigma nconcl ~store instance end } @@ -982,23 +984,21 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = aux n [] let get_next_hyp_position id gl = - let open Context.Named.Declaration in let rec aux = function | [] -> raise (RefinerError (NoSuchHyp id)) | decl :: right -> - if Id.equal (get_id decl) id then - match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast + if Id.equal (NamedDecl.get_id decl) id then + match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast else aux right in aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) let get_previous_hyp_position id gl = - let open Context.Named.Declaration in let rec aux dest = function | [] -> raise (RefinerError (NoSuchHyp id)) | decl :: right -> - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) @@ -1559,7 +1559,7 @@ let make_projection env sigma params cstr sign elim i n c u = | NotADefinedRecordUseScheme elim -> (* bugs: goes from right to left when i increases! *) let decl = List.nth cstr.cs_args i in - let t = get_type decl in + let t = RelDecl.get_type decl in let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in if @@ -1943,7 +1943,6 @@ let exact_proof c = end } let assumption = - let open Context.Named.Declaration in let rec arec gl only_eq = function | [] -> if only_eq then @@ -1951,7 +1950,7 @@ let assumption = arec gl false hyps else Tacticals.New.tclZEROMSG (str "No such assumption.") | decl::rest -> - let t = get_type decl in + let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let (sigma, is_same_type) = @@ -1962,7 +1961,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (NamedDecl.get_id decl)) h } else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> @@ -1992,7 +1991,7 @@ let check_is_type env sigma ty = let check_decl env sigma decl = let open Context.Named.Declaration in - let ty = get_type decl in + let ty = NamedDecl.get_type decl in let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in @@ -2002,7 +2001,7 @@ let check_decl env sigma decl = in !evdref with e when CErrors.noncritical e -> - let id = get_id decl in + let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) let clear_body ids = @@ -2034,7 +2033,7 @@ let clear_body ids = check_decl env sigma decl else sigma in - let seen = seen || List.mem_f Id.equal (get_id decl) ids in + let seen = seen || List.mem_f Id.equal (NamedDecl.get_id decl) ids in (push_named decl env, sigma, seen) in let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in @@ -2074,13 +2073,12 @@ let rec intros_clearing = function (* Keeping only a few hypotheses *) let keep hyps = - let open Context.Named.Declaration in Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) decl -> - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env hyp) keep || occur_var env hyp ccl @@ -2618,13 +2616,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = end } let insert_before decls lasthyp env = - let open Context.Named.Declaration in match lasthyp with | None -> push_named_context decls env | Some id -> Environ.fold_named_context (fun _ d env -> - let env = if Id.equal id (get_id d) then push_named_context decls env else env in + let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in push_named d env) ~init:(reset_context env) env @@ -2763,19 +2760,18 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = generalize_goal_gen env sigma ids i o t cl let old_generalize_dep ?(with_let=false) c gl = - let open Context.Named.Declaration in let env = pf_env gl in let sign = pf_hyps gl in let init_ids = ids_of_named_context (Global.named_context()) in let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) = - if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant + if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.get_id d') d) toquant || dependent_in_decl c d then d::toquant else toquant in let to_quantify = Context.Named.fold_outside seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in - let qhyps = List.map get_id to_quantify_rev in + let qhyps = List.map NamedDecl.get_id to_quantify_rev in let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with @@ -2787,7 +2783,7 @@ let old_generalize_dep ?(with_let=false) c gl = let body = if with_let then match kind_of_term c with - | Var id -> Tacmach.pf_get_hyp gl id |> get_value + | Var id -> Tacmach.pf_get_hyp gl id |> NamedDecl.get_value | _ -> None else None in @@ -2936,7 +2932,7 @@ let unfold_body x = | LocalDef (_,xval,_) -> xval in Tacticals.New.afterHyp x begin fun aft -> - let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in + let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in let rfun _ _ c = replace_vars [x, xval] c in let reducth h = reduct_in_hyp rfun h in let reductc = reduct_in_concl (rfun, DEFAULTcast) in @@ -3255,7 +3251,6 @@ exception Shunt of Id.t move_location let cook_sign hyp0_opt inhyps indvars env = (* First phase from L to R: get [toclear], [decldep] and [statuslist] for the hypotheses before (= more ancient than) hyp0 (see above) *) - let open Context.Named.Declaration in let toclear = ref [] in let avoid = ref [] in let decldeps = ref [] in @@ -3265,7 +3260,7 @@ let cook_sign hyp0_opt inhyps indvars env = let before = ref true in let maindep = ref false in let seek_deps env decl rhyp = - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then begin before:=false; @@ -3284,7 +3279,7 @@ let cook_sign hyp0_opt inhyps indvars env = in let depother = List.is_empty inhyps && (List.exists (fun id -> occur_var_in_decl env id decl) indvars || - List.exists (fun decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps) + List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother @@ -3307,7 +3302,7 @@ let cook_sign hyp0_opt inhyps indvars env = let _ = fold_named_context seek_deps env ~init:MoveFirst in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp decl = - let hyp = get_id decl in + let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then raise (Shunt lhyp); if Id.List.mem hyp !ldeps then begin @@ -3475,8 +3470,8 @@ let ids_of_constr ?(all=false) vars c = Array.fold_left_from (if all then 0 else mib.Declarations.mind_nparams) aux vars args - | _ -> fold_constr aux vars c) - | _ -> fold_constr aux vars c + | _ -> Term.fold_constr aux vars c) + | _ -> Term.fold_constr aux vars c in aux vars c let decompose_indapp f args = @@ -3531,13 +3526,12 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = end } let hyps_of_vars env sign nogen hyps = - let open Context.Named.Declaration in if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside (fun (hs,hl) d -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) else @@ -3567,7 +3561,6 @@ let linear vars args = with Seen -> false let is_defined_variable env id = - let open Context.Named.Declaration in lookup_named id env |> is_local_def let abstract_args gl generalize_vars dep id defined f args = @@ -3591,7 +3584,7 @@ let abstract_args gl generalize_vars dep id defined f args = let name, ty, arity = let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in let decl = List.hd rel in - get_name decl, get_type decl, c + RelDecl.get_name decl, RelDecl.get_type decl, c in let argty = Tacmach.pf_unsafe_type_of gl arg in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in @@ -4026,14 +4019,15 @@ let is_functional_induction elimc gl = need a dependent one or not *) let get_eliminator elim dep s gl = - let open Context.Rel.Declaration in match elim with | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in + let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.get_type d))) + (List.rev s.branches) + in evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts @@ -4095,7 +4089,6 @@ let induction_tac with_evars params indvars elim = induction applies with the induction hypotheses *) let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac = - let open Context.Named.Declaration in Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -4108,7 +4101,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let s = Retyping.get_sort_family_of env sigma tmpcl in let deps_cstr = List.fold_left - (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in + (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in @@ -4190,7 +4183,6 @@ let induction_without_atomization isrec with_evars elim names lid = (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = Proofview.Goal.nf_enter { enter = begin fun gl -> - let open Context.Named.Declaration in if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then errorlabstrm "" @@ -4199,7 +4191,7 @@ let clear_unselected_context id inhyps cls = match cls.onhyps with | Some hyps -> let to_erase d = - let id' = get_id d in + let id' = NamedDecl.get_id d in if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) @@ -4766,7 +4758,7 @@ let interpretable_as_section_decl evd d1 d2 = | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2) + | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) let rec decompose len c t accu = let open Context.Rel.Declaration in @@ -4779,7 +4771,6 @@ let rec decompose len c t accu = | _ -> assert false let rec shrink ctx sign c t accu = - let open Context.Rel.Declaration in match ctx, sign with | [], [] -> (c, t, accu) | p :: ctx, decl :: sign -> @@ -4790,9 +4781,9 @@ let rec shrink ctx sign c t accu = else let c = mkLambda_or_LetIn p c in let t = mkProd_or_LetIn p t in - let accu = if is_local_assum p then let open Context.Named.Declaration in - mkVar (get_id decl) :: accu - else accu + let accu = if RelDecl.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu in shrink ctx sign c t accu | _ -> assert false @@ -4818,7 +4809,6 @@ let abstract_subproof id gk tac = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in - let open Context.Named.Declaration in Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context() @@ -4828,7 +4818,7 @@ let abstract_subproof id gk tac = let sign,secsign = List.fold_right (fun d (s1,s2) -> - let id = get_id d in + let id = NamedDecl.get_id d in if mem_named_context id current_sign && interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d then (s1,push_named_context_val d s2) diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out new file mode 100644 index 000000000..2d4be8bce --- /dev/null +++ b/test-suite/output/ShowProof.out @@ -0,0 +1 @@ +(fun x : Type => conj I ?Goal) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 000000000..73ecaf220 --- /dev/null +++ b/test-suite/output/ShowProof.v @@ -0,0 +1,6 @@ +(* Was #4524 *) +Definition foo (x : Type) : True /\ True. +Proof. +split. +- exact I. + Show Proof. (* Was not finding an evar name at some time *) diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 45c539e22..49a815dc1 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -25,6 +25,8 @@ open Globnames open Printer open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** For a constant c in a module sealed by an interface (M:T and not M<:T), [Global.lookup_constant] may return a [constant_body] without body. We fix this by looking in the implementation @@ -144,7 +146,7 @@ let label_of = function let rec traverse current ctx accu t = match kind_of_term t with | Var id -> - let body () = Global.lookup_named id |> get_value in + let body () = Global.lookup_named id |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> let body () = Global.body_of_constant_body (lookup_constant kn) in diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 180b836ea..81e17ffb5 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -25,7 +25,8 @@ open Tactics open Ind_tables open Misctypes open Proofview.Notations -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration let out_punivs = Univ.out_punivs @@ -150,14 +151,14 @@ let build_beq_scheme mode kn = ( fun a b decl -> (* mkLambda(n,b,a) ) *) (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (eqName (get_name decl)) b a ) + mkNamedLambda (eqName (RelDecl.get_name decl)) b a ) c (List.rev eqs_typ) lnamesparrec in List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) (* Same here , hoping the auto renaming will do something good ;) *) mkNamedLambda - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let make_one_eq cur = let u = Univ.Instance.empty in @@ -249,7 +250,7 @@ let build_beq_scheme mode kn = | 0 -> Lazy.force tt | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in for ndx = 0 to nb_cstr_args-1 do - let cc = get_type (List.nth constrsi.(i).cs_args ndx) in + let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in let eqA, eff' = compute_A_equality rel_list nparrec (nparrec+3+2*nb_cstr_args) @@ -268,14 +269,14 @@ let build_beq_scheme mode kn = (Array.sub eqs 1 (nb_cstr_args - 1)) ) in - (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc + (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc (constrsj.(j).cs_args) ) else ar2.(j) <- (List.fold_left (fun a decl -> - mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) done; - ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) + ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (mkCase (ci,do_predicate rel_list nb_cstr_args, mkVar (Id.of_string "Y") ,ar2)) (constrsi.(i).cs_args)) @@ -489,7 +490,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] *) let list_id l = List.fold_left ( fun a decl -> let s' = - match get_name decl with + match RelDecl.get_name decl with Name s -> Id.to_string s | Anonymous -> "A" in (Id.of_string s',Id.of_string ("eq_"^s'), @@ -537,8 +538,8 @@ let compute_bl_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -680,8 +681,8 @@ let compute_lb_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) lb_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match (get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match (RelDecl.get_name decl) with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in @@ -821,8 +822,8 @@ let compute_dec_goal ind lnamesparrec nparrec = mkNamedProd seq b a ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a decl -> mkNamedProd - (match get_name decl with Name s -> s | Anonymous -> Id.of_string "A") - (get_type decl) a) eq_input lnamesparrec + (match RelDecl.get_name decl with Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_type decl) a) eq_input lnamesparrec in let n = Id.of_string "x" and m = Id.of_string "y" in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..a6fb48749 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -22,6 +22,8 @@ open Constrintern open Constrexpr open Sigma.Notations open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) open Decl_kinds @@ -77,13 +79,13 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function decl :: ctx -> - let t' = substl subst (get_type decl) in + let t' = substl subst (RelDecl.get_type decl) in let c', l = match decl with | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l | LocalDef (_,b,_) -> substl subst b, l in - let d = get_name decl, Some c', t' in + let d = RelDecl.get_name decl, Some c', t' in aux (c' :: subst, d :: instctx) l ctx | [] -> subst in aux (subst, []) inst (List.rev ctx) @@ -156,7 +158,6 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let cl, u = Typeclasses.typeclass_univ_instance k in let _, args = List.fold_right (fun decl (args, args') -> - let open Context.Rel.Declaration in match decl with | LocalAssum _ -> (List.tl args, List.hd args :: args') | LocalDef (_,b,_) -> (args, substl args' b :: args')) @@ -229,7 +230,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (fun (props, rest) decl -> if is_local_assum decl then try - let is_id (id', _) = match get_name decl, get_id id' with + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with | Name id, (_, id') -> Id.equal id id' | Anonymous, _ -> false in @@ -347,7 +348,7 @@ let named_of_rel_context l = let acc, ctx = List.fold_right (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in + let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = match decl with | LocalAssum (_,t) -> id, None, substl subst t | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648..7274ac170 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -39,6 +39,8 @@ open Sigma.Notations open Context.Rel.Declaration open Entries +module RelDecl = Context.Rel.Declaration + let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l @@ -457,7 +459,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (Retyping.get_type_of env evd (get_type d)))) + (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d)))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -576,7 +578,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (fun decl -> out_name (get_name decl)) assums in + let params = List.map (fun decl -> out_name (RelDecl.get_name decl)) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in @@ -909,8 +911,8 @@ let rec telescope = function let ty, tys, (k, constr) = List.fold_left (fun (ty, tys, (k, constr)) decl -> - let t = get_type decl in - let pred = mkLambda (get_name decl, t, ty) in + let t = RelDecl.get_type decl in + let pred = mkLambda (RelDecl.get_name decl, t, ty) in let ty = Universes.constr_of_global (Lazy.force sigT).typ in let intro = Universes.constr_of_global (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in @@ -920,7 +922,7 @@ let rec telescope = function in let (last, subst) = List.fold_right2 (fun pred decl (prev, subst) -> - let t = get_type decl in + let t = RelDecl.get_type decl in let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in let proj1 = applistc p1 [t; pred; prev] in @@ -1133,7 +1135,7 @@ let interp_recursive isfix fixl notations = let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in - let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in + let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff4c18ad2..c5ddf7186 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -25,6 +25,8 @@ open Printer open Evd open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (* This simplifies the typing context of Cases clauses *) (* hope it does not disturb other typing contexts *) let contract env lc = @@ -35,13 +37,10 @@ let contract env lc = l := (Vars.substl !l c') :: !l; env | _ -> - let t' = Vars.substl !l (get_type decl) in - let c' = Option.map (Vars.substl !l) (get_value decl) in - let na' = named_hd env t' (get_name decl) in + let t = Vars.substl !l (RelDecl.get_type decl) in + let decl = decl |> RelDecl.map_name (named_hd env t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in l := (mkRel 1) :: List.map (Vars.lift 1) !l; - match c' with - | None -> push_rel (LocalAssum (na',t')) env - | Some c' -> push_rel (LocalDef (na',c',t')) env + push_rel decl env in let env = process_rel_context contract_context env in (env, List.map (Vars.substl !l) lc) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 29d745732..b3c1623e0 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -20,6 +20,8 @@ open Pp open CErrors open Util +module NamedDecl = Context.Named.Declaration + let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) @@ -51,7 +53,6 @@ type oblinfo = where n binders were passed through. *) let subst_evar_constr evs n idf t = - let open Context.Named.Declaration in let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in @@ -74,6 +75,7 @@ let subst_evar_constr evs n idf t = in let args = let rec aux hyps args acc = + let open Context.Named.Declaration in match hyps, args with (LocalAssum _ :: tlh), (c :: tla) -> aux tlh tla ((substrec (depth, fixrels) c) :: acc) @@ -116,9 +118,9 @@ let etype_of_evar evs hyps concl = let open Context.Named.Declaration in let rec aux acc n = function decl :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in + let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in + let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in (match decl with @@ -598,7 +600,6 @@ let decompose_lam_prod c ty = in aux Context.Rel.empty c ty let shrink_body c ty = - let open Context.Rel.Declaration in let ctx, b, ty = match ty with | None -> @@ -613,6 +614,7 @@ let shrink_body c ty = if noccurn 1 b && Option.cata (noccurn 1) true ty then subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args else + let open Context.Rel.Declaration in let args = if is_local_assum decl then mkRel i :: args else args in mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, succ i, args) diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776..9d14bdf4c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -27,6 +27,8 @@ open Goptions open Sigma.Notations open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (********** definition d'un record (structure) **************) (** Flag governing use of primitive projections. Disabled by default. *) @@ -82,7 +84,7 @@ let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> let univ = if is_local_assum d then - let s = Retyping.get_sort_of env evars (get_type d) in + let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in Univ.sup (univ_of_sort s) univ else univ in (push_rel d env, univ)) @@ -167,7 +169,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs let degenerate_decl decl = - let id = match get_name decl with + let id = match RelDecl.get_name decl with | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match decl with @@ -288,8 +290,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (_,_,kinds,sp_projs,_) = List.fold_left3 (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> - let fi = get_name decl in - let ti = get_type decl in + let fi = RelDecl.get_name decl in + let ti = RelDecl.get_type decl in let (sp_projs,i,subst) = match fi with | Anonymous -> @@ -362,17 +364,17 @@ let structure_signature ctx = | [decl] -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in let evm = Sigma.to_evar_map evm in evm | decl::tl -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in + let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in let evm = Sigma.to_evar_map evm in let new_tl = Util.List.map_i (fun pos decl -> - map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in + RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in deps_to_evar evm new_tl in deps_to_evar Evd.empty (List.rev ctx) @@ -422,7 +424,7 @@ let implicits_of_context ctx = | Name n -> Some n | Anonymous -> None in ExplByPos (i, explname), (true, true, true)) - 1 (List.rev (Anonymous :: (List.map get_name ctx))) + 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = @@ -476,13 +478,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun decl b y -> get_name decl, b, y) + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) (List.rev fields) coers (Recordops.lookup_projections ind) in IndRef ind, l in let ctx_context = List.map (fun decl -> - match Typeclasses.class_of_constr (get_type decl) with + match Typeclasses.class_of_constr (RelDecl.get_type decl) with | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) | None -> None) params, params diff --git a/toplevel/search.ml b/toplevel/search.ml index e670b59b7..d1c108c37 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -20,6 +20,8 @@ open Globnames open Nametab open Goptions +module NamedDecl = Context.Named.Declaration + type filter_function = global_reference -> env -> constr -> bool type display_function = global_reference -> env -> constr -> unit @@ -68,8 +70,7 @@ let iter_constructors indsp u fn env nconstr = done let iter_named_context_name_type f = - let open Context.Named.Declaration in - List.iter (fun decl -> f (get_id decl) (get_type decl)) + List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = @@ -81,13 +82,12 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = (* General search over declarations *) let iter_declarations (fn : global_reference -> env -> constr -> unit) = - let open Context.Named.Declaration in let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> begin try let decl = Global.lookup_named (basename sp) in - fn (VarRef (get_id decl)) env (get_type decl) + fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl) with Not_found -> (* we are in a section *) () end | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc098f1f0..eeb4e26af 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -33,6 +33,8 @@ open Misctypes open Locality open Sigma.Notations +module NamedDecl = Context.Named.Declaration + (** TODO: make this function independent of Ltac *) let (f_interp_redexp, interp_redexp_hook) = Hook.make () @@ -848,14 +850,13 @@ let vernac_set_end_tac tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = - let open Context.Named.Declaration in let env = Global.env () in let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in List.iter (fun id -> - if not (List.exists (Id.equal id % get_id) vars) then + if not (List.exists (Id.equal id % NamedDecl.get_id) vars) then errorlabstrm "vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; @@ -1507,7 +1508,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl() + v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not |