diff options
31 files changed, 771 insertions, 1880 deletions
diff --git a/.travis.yml b/.travis.yml index 57f61caa5..19e7075f2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,10 +20,19 @@ addons: apt: sources: - avsm - packages: - - opam - - aspcud - - gcc-multilib +## Due to issues like +## https://github.com/travis-ci/travis-ci/issues/8507 , +## https://github.com/travis-ci/travis-ci/issues/9000 , +## https://github.com/travis-ci/travis-ci/issues/9081 , and +## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent +## failures with using `packages`. Therefore, for most targets, we +## instead invoke `apt-get update` manually with `travis_retry` before +## invoking `apt-get install`, manually, below in the `install:` +## target. +# packages: +# - opam +# - aspcud +# - gcc-multilib env: global: @@ -247,6 +256,8 @@ before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi install: +- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi +- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib; fi - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list @@ -4,6 +4,7 @@ [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://circleci.com/gh/coq/workflows/coq/tree/master) [](https://gitter.im/coq/coq) +[](https://doi.org/10.5281/zenodo.1003420) Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an diff --git a/checker/checker.ml b/checker/checker.ml index fee31b667..b8b4d5dc2 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -208,8 +208,7 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report" ++ - strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") +let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".") let guill s = str "\"" ++ str s ++ str "\"" diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh new file mode 100755 index 000000000..f8bf6bed4 --- /dev/null +++ b/dev/tools/sudo-apt-get-update.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err +! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $? diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 8e43bf6ed..f819d2e6a 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -3,7 +3,7 @@ open Term open Names open Cbytecodes open Cemitcodes -open Vm +open Vmvalues let ppripos (ri,pos) = (match ri with diff --git a/kernel/constr.ml b/kernel/constr.ml index 5930cfadc..1ff1fcc4c 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1178,8 +1178,3 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) - -(*******) -(* Type of abstract machine values *) -(** FIXME: nothing to do there *) -type values diff --git a/kernel/constr.mli b/kernel/constr.mli index 98bf71308..19ffa8fe3 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -459,7 +459,3 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr - -(**************************************) - -type values diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 712c66f11..2bbb867cd 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -15,7 +15,7 @@ open Util open Names open Constr -open Vm +open Vmvalues open Cemitcodes open Cbytecodes open Declarations diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 91bb30e7e..fc935f6ee 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,7 +12,7 @@ open Names open Constr open Pre_env -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 917e4f6f1..749854b8c 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -16,6 +16,7 @@ Cemitcodes Opaqueproof Declarations Entries +Vmvalues Nativevalues CPrimitives Declareops diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 3ef15105a..6c5e1cde5 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Constr open Declarations module NamedDecl = Context.Named.Declaration @@ -50,7 +49,7 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) CEphemeron.key + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 335ca1057..a6b57bd1b 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -36,9 +36,9 @@ type stratification = { type lazy_val -val force_lazy_val : lazy_val -> (values * Id.Set.t) option +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit type named_context_val = private { env_named_ctx : Context.Named.t; diff --git a/kernel/term.ml b/kernel/term.ml index aa8805952..fae990d45 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of projection * 'constr -type values = Constr.values +type values = Vmvalues.values (**********************************************************************) (** Redeclaration of functions from module Constr *) diff --git a/kernel/term.mli b/kernel/term.mli index f5cb72f4e..c9a8cf6e1 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -572,8 +572,8 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Proj of projection * 'constr [@@ocaml.deprecated "Alias for Constr.kind_of_term"] -type values = Constr.values -[@@ocaml.deprecated "Alias for Constr.values"] +type values = Vmvalues.values +[@@ocaml.deprecated "Alias for Vmvalues.values"] val hash_constr : Constr.constr -> int [@@ocaml.deprecated "Alias for Constr.hash"] diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3ef297b1f..8c7658147 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -3,6 +3,7 @@ open Names open Environ open Reduction open Vm +open Vmvalues open Csymtable let val_of_constr env c = diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 7f727df47..c3c9636e8 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,4 +19,4 @@ val vm_conv : conv_pb -> types kernel_conversion_function val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function (** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/vm.ml b/kernel/vm.ml index 51101f88e..352ea74a4 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,47 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Sorts -open Constr open Cbytecodes +open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" -(******************************************) -(* Utility Functions about Obj ************) -(******************************************) - -external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" -external offset : Obj.t -> int = "coq_offset" - -(*******************************************) -(* Initalization of the abstract machine ***) -(*******************************************) - -external init_vm : unit -> unit = "init_coq_vm" - -let _ = init_vm () - -(*******************************************) -(* Machine code *** ************************) -(*******************************************) - -type tcode -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) - -external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" -external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -external int_tcode : tcode -> int -> int = "coq_int_tcode" - -external accumulate : unit -> tcode = "accumulate_code" -let accumulate = accumulate () - -external is_accumulate : tcode -> bool = "coq_is_accumulate_code" - let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = @@ -62,106 +28,6 @@ let popstop_code i = let stop = popstop_code 0 -(******************************************************) -(* Abstract data types and utility functions **********) -(******************************************************) - -(* Values of the abstract machine *) -let val_of_obj v = ((Obj.obj v):values) -let crazy_val = (val_of_obj (Obj.repr 0)) - -(* Abstract data *) -type vprod -type vfun -type vfix -type vcofix -type vblock -type arguments - -type vm_env -type vstack = values array - -type vswitch = { - sw_type_code : tcode; - sw_code : tcode; - sw_annot : annot_switch; - sw_stk : vstack; - sw_env : vm_env - } - -(* Representation of values *) -(* + Products : *) -(* - vprod = 0_[ dom | codom] *) -(* dom : values, codom : vfun *) -(* *) -(* + Functions have two representations : *) -(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) -(* C:tcode, fvi : values *) -(* Remark : a function and its environment is the same value. *) -(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) -(* *) -(* + Fixpoints : *) -(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) -(* One single block to represent all of the fixpoints, each fixpoint *) -(* is the pointer to the field holding the pointer to its code, and *) -(* the infix tag is used to know where the block starts. *) -(* - Partial application follows the scheme of partially applied *) -(* functions. Note: only fixpoints not having been applied to its *) -(* recursive argument are coded this way. When the rec. arg. is *) -(* applied, either it's a constructor and the fix reduces, or it's *) -(* and the fix is coded as an accumulator. *) -(* *) -(* + Cofixpoints : see cbytegen.ml *) -(* *) -(* + vblock's encode (non constant) constructors as in Ocaml, but *) -(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) -(* accumulators. *) -(* *) -(* + vm_env is the type of the machine environments (i.e. a function or *) -(* a fixpoint) *) -(* *) -(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) -(* - representation of [accu] : tag_[....] *) -(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) -(* -- 10_[accu|proj name] : a projection blocked by an accu *) -(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 12_[accu|vswitch] : a match blocked by an accu *) -(* -- 13_[fcofix] : a cofix function *) -(* -- 14_[fcofix|val] : a cofix function, val represent the value *) -(* of the function applied to arg1 ... argn *) -(* The [arguments] type, which is abstracted as an array, represents : *) -(* tag[ _ | _ |v1|... | vn] *) -(* Generally the first field is a code pointer. *) - -(* Do not edit this type without editing C code, especially "coq_values.h" *) - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(* Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix*arguments (* Possibly empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up = values - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t (************************************************) (* Abstract machine *****************************) @@ -178,389 +44,72 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" - - (* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) (* Apply a value to arguments contained in [vargs] *) let apply_arguments vf vargs = let n = nargs vargs in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end (* Apply value [vf] to an array of argument values [varray] *) let apply_varray vf varray = let n = Array.length varray in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; (* The fun code of [vf] will make sure we have enough stack, so we put 0 here. *) push_vstack varray 0; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(*************************************************) -(* Destructors ***********************************) -(*************************************************) - -let uni_lvl_val (v : values) : Univ.Level.t = - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - CErrors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr ++ str ".") - -let rec whd_accu a stk = - let stk = - if Int.equal (Obj.size a) 2 then stk - else Zapp (Obj.obj a) :: stk in - let at = Obj.field a 1 in - match Obj.tag at with - | i when Int.equal i type_atom_tag -> - begin match stk with - | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) - | _ -> assert false - end - | i when i <= max_atom_tag -> - Vatom_stk(Obj.magic at, stk) - | i when Int.equal i proj_tag -> - let zproj = Zproj (Obj.obj (Obj.field at 0)) in - whd_accu (Obj.field at 1) (zproj :: stk) - | i when Int.equal i fix_app_tag -> - let fa = Obj.field at 1 in - let zfix = - Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in - whd_accu (Obj.field at 0) (zfix :: stk) - | i when Int.equal i switch_tag -> - let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in - whd_accu (Obj.field at 0) (zswitch :: stk) - | i when Int.equal i cofix_tag -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcfx, to_up, None) - | [Zapp args] -> Vcofix(vcfx, to_up, Some args) - | _ -> assert false - end - | i when Int.equal i cofix_evaluated_tag -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcofix, res, None) - | [Zapp args] -> Vcofix(vcofix, res, Some args) - | _ -> assert false - end - | tg -> - CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") - -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" - -let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in - if Obj.is_int o then Vconstr_const (Obj.obj o) - else - let tag = Obj.tag o in - if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) - else - if tag = Obj.closure_tag || tag = Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) - else - Vconstr_block(Obj.obj o) - -(**********************************************) -(* Constructors *******************************) -(**********************************************) - -let obj_of_atom : atom -> Obj.t = - fun a -> - let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); - Obj.set_field res 1 (Obj.repr a); - res - -(* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> Obj.repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p - | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res - | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) - -let val_of_obj o = ((Obj.obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let atom_of_proj kn v = - let r = Obj.new_block proj_tag 2 in - Obj.set_field r 0 (Obj.repr kn); - Obj.set_field r 1 (Obj.repr v); - ((Obj.obj r) : atom) - -let val_of_proj kn v = - val_of_atom (atom_of_proj kn v) - -module IdKeyHash = -struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal - open Hashset.Combine - let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) - | VarKey id -> combinesmall 2 (Id.hash id) - | RelKey i -> combinesmall 3 (Int.hash i) -end - -module KeyTable = Hashtbl.Make(IdKeyHash) - -let idkey_tbl = KeyTable.create 31 - -let val_of_idkey key = - try KeyTable.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - KeyTable.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) - -let val_of_named id = val_of_idkey (VarKey id) - -let val_of_constant c = val_of_idkey (ConstKey c) - -external val_of_annot_switch : annot_switch -> values = "%identity" - +(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) - -(*************************************************) -(** Operations manipulating data types ***********) -(*************************************************) - -(* Functions over products *) - -let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) -let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) - -(* Functions over vfun *) - -external closure_arity : vfun -> int = "coq_closure_arity" - -let body_of_vfun k vf = +let reduce_fun k vf = let vargs = mkrel_vstack k 1 in - apply_varray (Obj.magic vf) vargs + apply_varray vf vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_varray (Obj.magic vf1) vargs in - let v2 = apply_varray (Obj.magic vf2) vargs in + let v1 = apply_varray vf1 vargs in + let v2 = apply_varray vf2 vargs in arity, v1, v2 -(* Functions over fixpoint *) - -let first o = (offset_closure o (offset o)) -let last o = (Obj.field o (Obj.size o - 1)) - -let current_fix vf = - (offset (Obj.repr vf) / 2) - -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = first (Obj.repr vf) in - let size = Obj.size (last fb) in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = current_fix f1, current_fix f2 in - (* Checking starting point *) - if i1 = i2 then - let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in - let n = Obj.size (last fb1) in - (* Checking number of definitions *) - if n = Obj.size (last fb2) then - (* Checking recursive arguments *) - try - for i = 0 to n - 1 do - if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i - then raise FALSE - done; - true - with FALSE -> false - else false - else false - (* Functions over vfix *) -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" - -let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; - ref (Array.init len mkAccuCode) - -let relaccu_code i = - let len = Array.length !relaccu_tbl in - if i < len then !relaccu_tbl.(i) - else - begin - realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; - relaccu_tbl := - Array.init nl - (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); - !relaccu_tbl.(i) - end let reduce_fix k vf = - let fb = first (Obj.repr vf) in + let fb = first_fix vf in (* computing types *) - let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let fc_typ = fix_types fb in let ndef = Array.length fc_typ in - let et = offset_closure fb (2*(ndef - 1)) in + let et = offset_closure_fix fb (2*(ndef - 1)) in let ftyp = Array.map - (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in + (fun c -> interprete c crazy_val et 0) fc_typ in (* Construction of the environment of fix bodies *) - let e = Obj.dup fb in - for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) - done; - let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); - Obj.set_field res 1 (offset_closure e (2*i)); - ((Obj.obj res) : vfun) in - (Array.init ndef fix_body, ftyp) - -(* Functions over vcofix *) - -let get_fcofix vcf i = - match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with - | Vcofix(vcfi, _, _) -> vcfi - | _ -> assert false - -let current_cofix vcf = - let ndef = Obj.size (last (Obj.repr vcf)) in - let rec find_cofix pos = - if pos < ndef then - if get_fcofix vcf pos == vcf then pos - else find_cofix (pos+1) - else raise Not_found in - try find_cofix 0 - with Not_found -> assert false - -let check_cofix vcf1 vcf2 = - (current_cofix vcf1 = current_cofix vcf2) && - (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + (mk_fix_body k ndef fb, ftyp) let reduce_cofix k vcf = - let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let fc_typ = cofix_types vcf in let ndef = Array.length fc_typ in let ftyp = (* Evaluate types *) - Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in + Array.map (fun c -> interprete c crazy_val (cofix_env vcf) 0) fc_typ in (* Construction of the environment of cofix bodies *) - let e = Obj.dup (Obj.repr vcf) in - for i = 0 to ndef - 1 do - Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) - done; - - let cofix_body i = - let vcfi = get_fcofix vcf i in - let c = Obj.field (Obj.repr vcfi) 0 in - Obj.set_field e 0 c; - let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); - Obj.set_field self 1 (Obj.repr atom); - apply_varray (Obj.obj e) [|Obj.obj self|] in - (Array.init ndef cofix_body, ftyp) - - -(* Functions over vblock *) - -let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) -let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) - else invalid_arg "Vm.bfield" - - -(* Functions over vswitch *) - -let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl - -let case_info sw = sw.sw_annot.ci + (mk_cofix_body apply_varray k ndef vcf, ftyp) let type_of_switch sw = (* The fun code of types will make sure we have enough stack, so we put 0 @@ -568,20 +117,6 @@ let type_of_switch sw = push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 -let branch_arg k (tag,arity) = - if Int.equal arity 0 then ((Obj.magic tag):values) - else - let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 - else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); - b,1 in - for i = ofs to ofs + arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; - val_of_obj b - let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then @@ -603,8 +138,8 @@ let branch_of_switch k sw = (* t = a stk --> t v *) let rec apply_stack a stk v = match stk with - | [] -> apply_varray a [|v|] - | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v + | [] -> apply_varray (fun_of_val a) [|v|] + | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v | Zfix(f,args) :: stk -> let a,stk = @@ -615,7 +150,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args+ nargs args') in a, stk | _ -> @@ -623,7 +158,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) in a, stk in apply_stack a stk v @@ -634,50 +169,21 @@ let apply_whd k whd = let v = val_of_rel k in match whd with | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false - | Vfun f -> body_of_vfun k f + | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; push_val v; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0 + interprete (fix_code f) (fix_val f) (fix_env f) 0 | Vfix(f, Some args) -> push_ra stop; push_val v; push_arguments args; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) | Vcofix(_,to_up,_) -> push_ra stop; push_val v; - interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 + interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let rec pr_atom a = - Pp.(match a with - | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Constant.print c - | RelKey i -> str "#" ++ int i - | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") -and pr_whd w = - Pp.(match w with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" - | Vuniv_level _ -> assert false) -and pr_stack stk = - Pp.(match stk with - | [] -> str "[]" - | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) -and pr_zipper z = - Pp.(match z with - | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index bc38452d4..c6d92ba26 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -6,118 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Constr -open Cbytecodes +open Vmvalues (** Debug printing *) val set_drawinstr : unit -> unit -(** Machine code *) - -type tcode - -(** Values *) - -type vprod -type vfun -type vfix -type vcofix -type vblock -type vswitch -type arguments - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(** Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix * arguments (** might be empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t - -(** For debugging purposes only *) - -val pr_atom : atom -> Pp.t -val pr_whd : whd -> Pp.t -val pr_stack : stack -> Pp.t - -(** Constructors *) - -val val_of_str_const : structured_constant -> values -val val_of_rel : int -> values -val val_of_named : Id.t -> values -val val_of_constant : Constant.t -> values - -external val_of_annot_switch : annot_switch -> values = "%identity" - -(** Destructors *) - -val whd_val : values -> whd -val uni_lvl_val : values -> Univ.Level.t - -(** Arguments *) - -val nargs : arguments -> int -val arg : arguments -> int -> values - -(** Product *) - -val dom : vprod -> values -val codom : vprod -> vfun - -(** Function *) - -val body_of_vfun : int -> vfun -> values -val decompose_vfun2 : int -> vfun -> vfun -> int * values * values - -(** Fix *) - -val current_fix : vfix -> int -val check_fix : vfix -> vfix -> bool -val rec_args : vfix -> int array val reduce_fix : int -> vfix -> vfun array * values array (** bodies , types *) -(** CoFix *) - -val current_cofix : vcofix -> int -val check_cofix : vcofix -> vcofix -> bool val reduce_cofix : int -> vcofix -> values array * values array (** bodies , types *) -(** Block *) +val type_of_switch : vswitch -> values -val btag : vblock -> int -val bsize : vblock -> int -val bfield : vblock -> int -> values +val branch_of_switch : int -> vswitch -> (int * values) array -(** Switch *) +val reduce_fun : int -> vfun -> values -val check_switch : vswitch -> vswitch -> bool -val case_info : vswitch -> case_info -val type_of_switch : vswitch -> values -val branch_of_switch : int -> vswitch -> (int * values) array +(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current + DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced + bodies under those lambdas. *) +val decompose_vfun2 : int -> vfun -> vfun -> int * values * values (** Apply a value *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml new file mode 100644 index 000000000..1102cdec1 --- /dev/null +++ b/kernel/vmvalues.ml @@ -0,0 +1,525 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Sorts +open Cbytecodes + +(*******************************************) +(* Initalization of the abstract machine ***) +(* Necessary for [relaccu_tbl] *) +(*******************************************) + +external init_vm : unit -> unit = "init_coq_vm" + +let _ = init_vm () + +(******************************************************) +(* Abstract data types and utility functions **********) +(******************************************************) + +(* Values of the abstract machine *) +type values +let val_of_obj v = ((Obj.obj v):values) +let crazy_val = (val_of_obj (Obj.repr 0)) + +(* Abstract data *) +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments + +let fun_val v = (Obj.magic v : values) +let fix_val v = (Obj.magic v : values) +let cofix_upd_val v = (Obj.magic v : values) + +type vm_env +let fun_env v = (Obj.magic v : vm_env) +let fix_env v = (Obj.magic v : vm_env) +let cofix_env v = (Obj.magic v : vm_env) +let cofix_upd_env v = (Obj.magic v : vm_env) +type vstack = values array + +let fun_of_val v = (Obj.magic v : vfun) + +(*******************************************) +(* Machine code *** ************************) +(*******************************************) + +type tcode + +external mkAccuCode : int -> tcode = "coq_makeaccu" +external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" + +let tcode_of_obj v = ((Obj.obj v):tcode) +let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) +let fix_code v = fun_code v +let cofix_upd_code v = fun_code v + + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +(* Representation of values *) +(* + Products : *) +(* - vprod = 0_[ dom | codom] *) +(* dom : values, codom : vfun *) +(* *) +(* + Functions have two representations : *) +(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) +(* C:tcode, fvi : values *) +(* Remark : a function and its environment is the same value. *) +(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* *) +(* + Fixpoints : *) +(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* One single block to represent all of the fixpoints, each fixpoint *) +(* is the pointer to the field holding the pointer to its code, and *) +(* the infix tag is used to know where the block starts. *) +(* - Partial application follows the scheme of partially applied *) +(* functions. Note: only fixpoints not having been applied to its *) +(* recursive argument are coded this way. When the rec. arg. is *) +(* applied, either it's a constructor and the fix reduces, or it's *) +(* and the fix is coded as an accumulator. *) +(* *) +(* + Cofixpoints : see cbytegen.ml *) +(* *) +(* + vblock's encode (non constant) constructors as in Ocaml, but *) +(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) +(* accumulators. *) +(* *) +(* + vm_env is the type of the machine environments (i.e. a function or *) +(* a fixpoint) *) +(* *) +(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation of [accu] : tag_[....] *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[fcofix|val] : a cofix function, val represent the value *) +(* of the function applied to arg1 ... argn *) +(* The [arguments] type, which is abstracted as an array, represents : *) +(* tag[ _ | _ |v1|... | vn] *) +(* Generally the first field is a code pointer. *) + +(* Do not edit this type without editing C code, especially "coq_values.h" *) + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(* Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix*arguments (* Possibly empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type to_update = values + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i)) + +(*************************************************) +(* Destructors ***********************************) +(*************************************************) + +let uni_lvl_val (v : values) : Univ.Level.t = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + CErrors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr ++ str ".") + +let rec whd_accu a stk = + let stk = + if Int.equal (Obj.size a) 2 then stk + else Zapp (Obj.obj a) :: stk in + let at = Obj.field a 1 in + match Obj.tag at with + | i when Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end + | i when i <= max_atom_tag -> + Vatom_stk(Obj.magic at, stk) + | i when Int.equal i proj_tag -> + let zproj = Zproj (Obj.obj (Obj.field at 0)) in + whd_accu (Obj.field at 1) (zproj :: stk) + | i when Int.equal i fix_app_tag -> + let fa = Obj.field at 1 in + let zfix = + Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + whd_accu (Obj.field at 0) (zfix :: stk) + | i when Int.equal i switch_tag -> + let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in + whd_accu (Obj.field at 0) (zswitch :: stk) + | i when Int.equal i cofix_tag -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcfx, to_up, None) + | [Zapp args] -> Vcofix(vcfx, to_up, Some args) + | _ -> assert false + end + | i when Int.equal i cofix_evaluated_tag -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcofix, res, None) + | [Zapp args] -> Vcofix(vcofix, res, Some args) + | _ -> assert false + end + | tg -> + CErrors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") + +external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" +external is_accumulate : tcode -> bool = "coq_is_accumulate_code" +external int_tcode : tcode -> int -> int = "coq_int_tcode" +external accumulate : unit -> tcode = "accumulate_code" +let accumulate = accumulate () + +let whd_val : values -> whd = + fun v -> + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) + else + let tag = Obj.tag o in + if tag = accu_tag then + ( + if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) + else + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o)) + else + if tag = Obj.closure_tag || tag = Obj.infix_tag then + (match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + else + Vconstr_block(Obj.obj o) + +(**********************************************) +(* Constructors *******************************) +(**********************************************) + +let obj_of_atom : atom -> Obj.t = + fun a -> + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr accumulate); + Obj.set_field res 1 (Obj.repr a); + res + +(* obj_of_str_const : structured_constant -> Obj.t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> Obj.repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_proj p -> Obj.repr p + | Const_b0 tag -> Obj.repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = Obj.new_block tag len in + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) + done; + res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) + +let val_of_obj o = ((Obj.obj o) : values) + +let val_of_str_const str = val_of_obj (obj_of_str_const str) + +let val_of_atom a = val_of_obj (obj_of_atom a) + +let atom_of_proj kn v = + let r = Obj.new_block proj_tag 2 in + Obj.set_field r 0 (Obj.repr kn); + Obj.set_field r 1 (Obj.repr v); + ((Obj.obj r) : atom) + +let val_of_proj kn v = + val_of_atom (atom_of_proj kn v) + +module IdKeyHash = +struct + type t = Constant.t tableKey + let equal = Names.eq_table_key Constant.equal + open Hashset.Combine + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +end + +module KeyTable = Hashtbl.Make(IdKeyHash) + +let idkey_tbl = KeyTable.create 31 + +let val_of_idkey key = + try KeyTable.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + KeyTable.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) + +let val_of_named id = val_of_idkey (VarKey id) + +let val_of_constant c = val_of_idkey (ConstKey c) + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(*************************************************) +(** Operations manipulating data types ***********) +(*************************************************) + +(* Functions over products *) + +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) + +(* Functions over vfun *) + +external closure_arity : vfun -> int = "coq_closure_arity" + +(* Functions over fixpoint *) + +external offset : Obj.t -> int = "coq_offset" +external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" + +let first o = (offset_closure o (offset o)) +let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) + +let last o = (Obj.field o (Obj.size o - 1)) +let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) + +let current_fix vf = - (offset (Obj.repr vf) / 2) + +let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 + +let rec_args vf = + let fb = first (Obj.repr vf) in + let size = Obj.size (last fb) in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = current_fix f1, current_fix f2 in + (* Checking starting point *) + if i1 = i2 then + let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in + let n = Obj.size (last fb1) in + (* Checking number of definitions *) + if n = Obj.size (last fb2) then + (* Checking recursive arguments *) + try + for i = 0 to n - 1 do + if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i + then raise FALSE + done; + true + with FALSE -> false + else false + else false + +external atom_rel : unit -> atom array = "get_coq_atom_tbl" +external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" + +let relaccu_tbl = + let atom_rel = atom_rel() in + let len = Array.length atom_rel in + for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + ref (Array.init len mkAccuCode) + +let relaccu_code i = + let len = Array.length !relaccu_tbl in + if i < len then !relaccu_tbl.(i) + else + begin + realloc_atom_rel i; + let atom_rel = atom_rel () in + let nl = Array.length atom_rel in + for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + relaccu_tbl := + Array.init nl + (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); + !relaccu_tbl.(i) + end + +let mk_fix_body k ndef fb = + let e = Obj.dup (Obj.repr fb) in + for i = 0 to ndef - 1 do + Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + done; + let fix_body i = + let jump_grabrec c = offset_tcode c 2 in + let c = jump_grabrec (unsafe_fb_code fb i) in + let res = Obj.new_block Obj.closure_tag 2 in + Obj.set_field res 0 (Obj.repr c); + Obj.set_field res 1 (offset_closure e (2*i)); + ((Obj.obj res) : vfun) in + Array.init ndef fix_body + +(* Functions over vcofix *) + +let get_fcofix vcf i = + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + | Vcofix(vcfi, _, _) -> vcfi + | _ -> assert false + +let current_cofix vcf = + let ndef = Obj.size (last (Obj.repr vcf)) in + let rec find_cofix pos = + if pos < ndef then + if get_fcofix vcf pos == vcf then pos + else find_cofix (pos+1) + else raise Not_found in + try find_cofix 0 + with Not_found -> assert false + +let check_cofix vcf1 vcf2 = + (current_cofix vcf1 = current_cofix vcf2) && + (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + +let mk_cofix_body apply_varray k ndef vcf = + let e = Obj.dup (Obj.repr vcf) in + for i = 0 to ndef - 1 do + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) + done; + + let cofix_body i = + let vcfi = get_fcofix vcf i in + let c = Obj.field (Obj.repr vcfi) 0 in + Obj.set_field e 0 c; + let atom = Obj.new_block cofix_tag 1 in + let self = Obj.new_block accu_tag 2 in + Obj.set_field self 0 (Obj.repr accumulate); + Obj.set_field self 1 (Obj.repr atom); + apply_varray (Obj.obj e) [|Obj.obj self|] in + Array.init ndef cofix_body + +(* Functions over vblock *) + +let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) +let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) + else invalid_arg "Vm.bfield" + + +(* Functions over vswitch *) + +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + +let branch_arg k (tag,arity) = + if Int.equal arity 0 then ((Obj.magic tag):values) + else + let b, ofs = + if tag < last_variant_tag then Obj.new_block tag arity, 0 + else + let b = Obj.new_block last_variant_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + b,1 in + for i = ofs to ofs + arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done; + val_of_obj b + +(* Printing *) + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Constant.print c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli new file mode 100644 index 000000000..350f71372 --- /dev/null +++ b/kernel/vmvalues.mli @@ -0,0 +1,144 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Cbytecodes + +(** Values *) + +type values +type vm_env +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments +type vstack = values array +type to_update + +val fun_val : vfun -> values +val fix_val : vfix -> values +val cofix_upd_val : to_update -> values + +val fun_env : vfun -> vm_env +val fix_env : vfix -> vm_env +val cofix_env : vcofix -> vm_env +val cofix_upd_env : to_update -> vm_env + +(** Cast a value known to be a function, unsafe in general *) +val fun_of_val : values -> vfun + +val crazy_val : values + +(** Machine code *) + +type tcode + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +external mkAccuCode : int -> tcode = "coq_makeaccu" + +val fun_code : vfun -> tcode +val fix_code : vfix -> tcode +val cofix_upd_code : to_update -> tcode + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(** Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix * arguments (** might be empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(** For debugging purposes only *) + +val pr_atom : atom -> Pp.t +val pr_whd : whd -> Pp.t +val pr_stack : stack -> Pp.t + +(** Constructors *) + +val val_of_str_const : structured_constant -> values +val val_of_rel : int -> values +val val_of_named : Id.t -> values +val val_of_constant : Constant.t -> values +val val_of_proj : Constant.t -> values -> values +val val_of_atom : atom -> values + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(** Destructors *) + +val whd_val : values -> whd +val uni_lvl_val : values -> Univ.Level.t + +(** Arguments *) + +val nargs : arguments -> int +val arg : arguments -> int -> values + +(** Product *) + +val dom : vprod -> values +val codom : vprod -> vfun + +(** Fun *) +external closure_arity : vfun -> int = "coq_closure_arity" + +(** Fix *) + +val current_fix : vfix -> int +val check_fix : vfix -> vfix -> bool +val rec_args : vfix -> int array +val first_fix : vfix -> vfix +val fix_types : vfix -> tcode array +val cofix_types : vcofix -> tcode array +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +val mk_fix_body : int -> int -> vfix -> vfun array + +(** CoFix *) + +val current_cofix : vcofix -> int +val check_cofix : vcofix -> vcofix -> bool +val mk_cofix_body : (vfun -> vstack -> values) -> int -> int -> vcofix -> values array + +(** Block *) + +val btag : vblock -> int +val bsize : vblock -> int +val bfield : vblock -> int -> values + +(** Switch *) + +val check_switch : vswitch -> vswitch -> bool +val branch_arg : int -> Cbytecodes.tag * int -> values diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index a3315f22c..ad396a2cb 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -29,10 +29,6 @@ val generate_functional_principle : (EConstr.constr array -> int -> Tacmach.tactic) -> unit -val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> - types -> types - - exception No_graph_found val make_scheme : Evd.evar_map ref -> diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 0666ab4f1..be8abb92e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -17,69 +17,12 @@ let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = DAst.make @@ GSort(s) let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = DAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -let glob_decompose_prod = - let rec glob_decompose_prod args c = match DAst.get c with - | GProd(n,k,t,b) -> - glob_decompose_prod ((n,t)::args) b - | _ -> args,c - in - glob_decompose_prod [] - -let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args rt = match DAst.get rt with - | GProd(n,k,t,b) -> - glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(n,b,t,c) -> - glob_decompose_prod ((n,Some b,t)::args) c - | _ -> args,rt - in - glob_decompose_prod [] - -let glob_compose_prod = - List.fold_left (fun b (n,t) -> mkGProd(n,t,b)) - -let glob_compose_prod_or_letin = - List.fold_left ( - fun concl decl -> - match decl with - | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) - | _ -> assert false) - -let glob_decompose_prod_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match DAst.get c with - | GProd(n,_,t,b) -> - glob_decompose_prod (i-1) ((n,t)::args) b - | _ -> args,c - in - glob_decompose_prod n [] - - -let glob_decompose_prod_or_letin_n n = - let rec glob_decompose_prod i args c = - if i<=0 then args,c - else - match DAst.get c with - | GProd(n,_,t,b) -> - glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(n,b,t,c) -> - glob_decompose_prod (i-1) ((n,Some b,t)::args) c - | _ -> args,c - in - glob_decompose_prod n [] - - let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) @@ -101,18 +44,6 @@ let glob_make_eq ?(typ= mkGHole ()) t1 t2 = let glob_make_neq t1 t2 = mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -let glob_make_or t1 t2 = mkGApp (mkGRef(Lazy.force Coqlib.coq_or_ref),[t1;t2]) - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -let rec glob_make_or_list = function - | [] -> invalid_arg "mk_or" - | [e] -> e - | e::l -> glob_make_or e (glob_make_or_list l) - - let remove_name_from_mapping mapping na = match na with | Anonymous -> mapping @@ -575,97 +506,6 @@ let ids_of_pat = in ids_of_pat Id.Set.empty -let id_of_name = function - | Anonymous -> Id.of_string "x" - | Name x -> x - -(* TODO: finish Rec caes *) -let ids_of_glob_constr c = - let rec ids_of_glob_constr acc c = - let idof = id_of_name in - match DAst.get c with - | GVar id -> id::acc - | GApp (g,args) -> - ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc - | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc - | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc - | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc - | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc - | GLetTuple (nal,(na,po),b,c) -> - List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCases (sty,rtntypopt,tml,brchl) -> - List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl) - | GRec _ -> failwith "Fix inside a constructor branch" - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] - in - (* build the set *) - List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c) - - - - - -let zeta_normalize = - let rec zeta_normalize_term x = DAst.map (function - | GRef _ - | GVar _ - | GEvar _ - | GPatVar _ as rt -> rt - | GApp(rt',rtl) -> - GApp(zeta_normalize_term rt', - List.map zeta_normalize_term rtl - ) - | GLambda(name,k,t,b) -> - GLambda(name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GProd(name,k,t,b) -> - GProd(name, - k, - zeta_normalize_term t, - zeta_normalize_term b - ) - | GLetIn(Name id,def,typ,b) -> - DAst.get (zeta_normalize_term (replace_var_by_term id def b)) - | GLetIn(Anonymous,def,typ,b) -> - DAst.get (zeta_normalize_term b) - | GLetTuple(nal,(na,rto),def,b) -> - GLetTuple(nal, - (na,Option.map zeta_normalize_term rto), - zeta_normalize_term def, - zeta_normalize_term b - ) - | GCases(sty,infos,el,brl) -> - GCases(sty, - infos, - List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, - List.map zeta_normalize_br brl - ) - | GIf(b,(na,e_option),lhs,rhs) -> - GIf(zeta_normalize_term b, - (na,Option.map zeta_normalize_term e_option), - zeta_normalize_term lhs, - zeta_normalize_term rhs - ) - | GRec _ -> raise (UserError(None,str "Not handled GRec")) - | GSort _ - | GHole _ as rt -> rt - | GCast(b,c) -> - GCast(zeta_normalize_term b, - Miscops.map_cast_type zeta_normalize_term c) - ) x - and zeta_normalize_br (loc,(idl,patl,res)) = - (loc,(idl,patl,zeta_normalize_term res)) - in - zeta_normalize_term - - - - let expand_as = let rec add_as map rt = diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 99a258de9..7088ae596 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,6 +1,5 @@ open Names open Glob_term -open Misctypes (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *) val get_pattern_id : cases_pattern -> Id.t list @@ -21,22 +20,11 @@ val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr -val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) -val mkGCast : glob_constr* glob_constr -> glob_constr (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) -val glob_decompose_prod : glob_constr -> (Name.t*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin : - glob_constr -> (Name.t*glob_constr option*glob_constr option) list * glob_constr -val glob_decompose_prod_n : int -> glob_constr -> (Name.t*glob_constr) list * glob_constr -val glob_decompose_prod_or_letin_n : int -> glob_constr -> - (Name.t*glob_constr option*glob_constr option) list * glob_constr -val glob_compose_prod : glob_constr -> (Name.t*glob_constr) list -> glob_constr -val glob_compose_prod_or_letin: glob_constr -> - (Name.t*glob_constr option*glob_constr option) list -> glob_constr val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) @@ -44,14 +32,6 @@ val glob_decompose_app : glob_constr -> glob_constr*(glob_constr list) val glob_make_eq : ?typ:glob_constr -> glob_constr -> glob_constr -> glob_constr (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) val glob_make_neq : glob_constr -> glob_constr -> glob_constr -(* [glob_make_or P1 P2] build the glob_constr corresponding to [P1 \/ P2] *) -val glob_make_or : glob_constr -> glob_constr -> glob_constr - -(* [glob_make_or_list [P1;...;Pn]] build the glob_constr corresponding - to [P1 \/ ( .... \/ Pn)] -*) -val glob_make_or_list : glob_constr list -> glob_constr - (* alpha_conversion functions *) @@ -109,18 +89,8 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool *) val ids_of_pat : cases_pattern -> Id.Set.t -(* TODO: finish this function (Fix not treated) *) -val ids_of_glob_constr: glob_constr -> Id.Set.t - -(* - removing let_in construction in a glob_constr -*) -val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr - - val expand_as : glob_constr -> glob_constr - (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution *) val resolve_and_replace_implicits : diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 071599d9c..071bab2f3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -282,7 +282,6 @@ let derive_inversion fix_names = in Invfun.derive_correctness Functional_principles_types.make_scheme - functional_induction fix_names_as_constant lind; with e when CErrors.noncritical e -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 694c80051..4acf82d00 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -56,12 +56,6 @@ let do_observe_tac s tac g = CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; - -let observe_tac_strm s tac g = - if do_observe () - then do_observe_tac s tac g - else tac g - let observe_tac s tac g = if do_observe () then do_observe_tac (str s) tac g @@ -87,10 +81,6 @@ let make_eq () = try EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) with _ -> assert false -let make_eq_refl () = - try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) - with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -194,10 +184,9 @@ let rec generate_fresh_id x avoid i = id::(generate_fresh_id x (id::avoid) (pred i)) -(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] +(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. - [functional_induction] is the tactic defined in [indfun] (dependency problem) [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. graphs of the functions and principles and correctness lemma types) to prove correct. @@ -218,7 +207,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = +let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -752,14 +741,13 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti g -(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness +(* [derive_correctness make_scheme funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and - [functional_induction] is Indfun.functional_induction (same pb) *) -let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) = +let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) = assert (funs <> []); assert (graphs <> []); let funs = Array.of_list funs and graphs = Array.of_list graphs in @@ -809,7 +797,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( ) in let proving_tac = - prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos + prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli new file mode 100644 index 000000000..e07138596 --- /dev/null +++ b/plugins/funind/invfun.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val invfun : + Misctypes.quantified_hypothesis -> + Globnames.global_reference option -> + Evar.t Evd.sigma -> Evar.t list Evd.sigma +val derive_correctness : + (Evd.evar_map ref -> + (Constr.pconstant * Sorts.family) list -> + 'a Entries.definition_entry list) -> + Constr.pconstant list -> Names.inductive list -> unit diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml deleted file mode 100644 index 8f5d3f22f..000000000 --- a/plugins/funind/merge.ml +++ /dev/null @@ -1,1013 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Merging of induction principles. *) - -open Globnames -open Tactics -open Indfun_common -open CErrors -open Util -open Constrexpr -open Vernacexpr -open Pp -open Names -open Term -open Constr -open Vars -open Glob_term -open Glob_termops -open Decl_kinds -open Declarations -open Context.Rel.Declaration - -module RelDecl = Context.Rel.Declaration - -(** {1 Utilities} *) - -(** {2 Useful operations on constr and glob_constr} *) - -let pop c = Vars.lift (-1) c -let rec popn i c = if i<=0 then c else pop (popn (i-1) c) - -(** Substitutions in constr *) -let compare_constr_nosub t1 t2 = - if Constr.compare_head (fun _ _ -> false) t1 t2 - then true - else false - -let rec compare_constr' t1 t2 = - if compare_constr_nosub t1 t2 - then true - else (Constr.compare_head (compare_constr') t1 t2) - -let rec substitterm prof t by_t in_u = - if (compare_constr' (lift prof t) in_u) - then (lift prof by_t) - else Constr.map_with_binders succ - (fun i -> substitterm i t by_t) prof in_u - -let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl - -let understand = Pretyping.understand (Global.env()) Evd.empty - -(** Operations on names and identifiers *) -let id_of_name = function - Anonymous -> Id.of_string "H" - | Name id -> id;; -let name_of_string = Id.of_string %> Name.mk_name -let string_of_name = id_of_name %> Id.to_string - -(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) -let isVarf f x = - match DAst.get x with - | GVar x -> Id.equal x f - | _ -> false - -(** [ident_global_exist id] returns true if identifier [id] is linked - in global environment. *) -let ident_global_exist id = - try - let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in - let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in - true - with e when CErrors.noncritical e -> false - -(** [next_ident_fresh id] returns a fresh identifier (ie not linked in - global env) with base [id]. *) -let next_ident_fresh (id:Id.t) = - let res = ref id in - while ident_global_exist !res do res := Nameops.increment_subscript !res done; - !res - - -(** {2 Debugging} *) -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" -(* uncomment this to see debugging *) -let prconstr c = - let sigma, env = Pfedit.get_current_context () in - msg (str" " ++ Printer.pr_lconstr_env env sigma c) - -let prconstrnl c = - let sigma, env = Pfedit.get_current_context () in - msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") - -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - let sigma, env = Pfedit.get_current_context () in - begin - msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); - msg(str ""); - end -let prNamedRConstr s c = - let sigma, env = Pfedit.get_current_context () in - begin - msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); - msg(str ""); - end -let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc -let prNamedLConstr s lc = - begin - prstr "[§§§ "; - prstr s; - prNamedLConstr_aux lc; - prstr " §§§]\n"; - end -let prNamedLDecl s lc = - begin - prstr s; prstr "\n"; - List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc; - prstr "\n"; - end -let prNamedRLDecl s lc = - begin - prstr s; prstr "\n"; prstr "{§§ "; - List.iter - (fun x -> - match x with - | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp - | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy - | _ -> assert false - ) lc; - prstr " §§}\n"; - prstr "\n"; - end - -(** {2 Misc} *) - -exception Found of int - -(* Array scanning *) - -let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int = -match Array.findi pred arr with -| None -> Array.length arr (* all elt are positive *) -| Some i -> i - -(* Like List.chop but except that [i] is the size of the suffix of [l]. *) -let list_chop_end i l = - let size_prefix = List.length l -i in - if size_prefix < 0 then failwith "list_chop_end" - else List.chop size_prefix l - -let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = - let i = ref 0 in - List.fold_left - (fun acc x -> - let res = f !i acc x in i := !i + 1; res) - acc arr - -let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list = - let i = ref 0 in - List.filter (fun x -> let res = f !i x in i := !i + 1; res) l - - -(** Iteration module *) -module For = -struct - let rec map i j (f: int -> 'a) = if i>j then [] else f i :: (map (i+1) j f) - let rec foldup i j (f: 'a -> int -> 'a) acc = - if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc - let rec folddown i j (f: 'a -> int -> 'a) acc = - if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc - let fold i j = if i<j then foldup i j else folddown i j -end - - -(** {1 Parameters shifting and linking information} *) - -(** This type is used to deal with debruijn linked indices. When a - variable is linked to a previous one, we will ignore it and refer - to previous one. *) -type linked_var = - | Linked of int - | Unlinked - | Funres - -(** When merging two graphs, parameters may become regular arguments, - and thus be shifted. This type describes the result of computing - the changes. *) -type 'a shifted_params = - { - nprm1:'a; - nprm2:'a; - prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *) - nuprm1:'a; - nuprm2:'a; - nargs1:'a; - nargs2:'a; - } - - -let prlinked x = - match x with - | Linked i -> Printf.sprintf "Linked %d" i - | Unlinked -> Printf.sprintf "Unlinked" - | Funres -> Printf.sprintf "Funres" - -let linkmonad f lnkvar = - match lnkvar with - | Linked i -> Linked (f i) - | Unlinked -> Unlinked - | Funres -> Funres - -let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar - -(* This map is used to deal with debruijn linked indices. *) -module Link = Map.Make (Int) - -let pr_links l = - Printf.printf "links:\n"; - Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l; - Printf.printf "_____________\n" - -type 'a merged_arg = - | Prm_stable of 'a - | Prm_linked of 'a - | Prm_arg of 'a - | Arg_stable of 'a - | Arg_linked of 'a - | Arg_funres - -(** Information about graph merging of two inductives. - All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *) - -type merge_infos = - { - ident:Id.t; (** new inductive name *) - mib1: mutual_inductive_body; - oib1: one_inductive_body; - mib2: mutual_inductive_body; - oib2: one_inductive_body; - - (** Array of links of the first inductive (should be all stable) *) - lnk1: int merged_arg array; - - (** Array of links of the second inductive (point to the first ind param/args) *) - lnk2: int merged_arg array; - - (** rec params which remain rec param (ie not linked) *) - recprms1: Context.Rel.Declaration.t list; - recprms2: Context.Rel.Declaration.t list; - nrecprms1: int; - nrecprms2: int; - - (** rec parms which became non parm (either linked to something - or because after a rec parm that became non parm) *) - otherprms1: Context.Rel.Declaration.t list; - otherprms2: Context.Rel.Declaration.t list; - notherprms1:int; - notherprms2:int; - - (** args which remain args in merge *) - args1:Context.Rel.Declaration.t list; - args2:Context.Rel.Declaration.t list; - nargs1:int; - nargs2:int; - - (** functional result args *) - funresprms1: Context.Rel.Declaration.t list; - funresprms2: Context.Rel.Declaration.t list; - nfunresprms1:int; - nfunresprms2:int; - } - - -let pr_merginfo x = - let i,s= - match x with - | Prm_linked i -> Some i,"Prm_linked" - | Arg_linked i -> Some i,"Arg_linked" - | Prm_stable i -> Some i,"Prm_stable" - | Prm_arg i -> Some i,"Prm_arg" - | Arg_stable i -> Some i,"Arg_stable" - | Arg_funres -> None , "Arg_funres" in - match i with - | Some i -> Printf.sprintf "%s(%d)" s i - | None -> Printf.sprintf "%s" s - -let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false - -(* ?? prm_linked?? *) -let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false - -let is_stable x = - match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false - -let isArg_funres x = match x with Arg_funres -> true | _ -> false - -let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list = - let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in - let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in - let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in - prms@args@fres - -(** Reverse the link map, keeping only linked vars, elements are list - of int as several vars may be linked to the same var. *) -let revlinked lnk = - For.fold 0 (Array.length lnk - 1) - (fun acc k -> - match lnk.(k) with - | Unlinked | Funres -> acc - | Linked i -> - let old = try Link.find i acc with Not_found -> [] in - Link.add i (k::old) acc) - Link.empty - -let array_switch arr i j = - let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux - -let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list = - let larr = Array.of_list l in - let _ = - Array.iteri - (fun j x -> - match x with - | Prm_linked i -> array_switch larr i j - | Arg_linked i -> array_switch larr i j - | Prm_stable i -> () - | Prm_arg i -> () - | Arg_stable i -> () - | Arg_funres -> () - ) lnk in - filter_shift_stable lnk (Array.to_list larr) - - -let error msg = user_err Pp.(str msg) - -(** {1 Utilities for merging} *) - -let ind1name = Id.of_string "__ind1" -let ind2name = Id.of_string "__ind2" - -(** Performs verifications on two graphs before merging: they must not - be co-inductive, and for the moment they must not be mutual - either. *) -let verify_inds mib1 mib2 = - if mib1.mind_finite == CoFinite then error "First argument is coinductive"; - if mib2.mind_finite == CoFinite then error "Second argument is coinductive"; - if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; - if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; - () - -(* -(** [build_raw_params prms_decl avoid] returns a list of variables - attributed to the list of decl [prms_decl], avoiding names in - [avoid]. *) -let build_raw_params prms_decl avoid = - let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in - let _ = prNamedConstr "DUMMY" dummy_constr in - let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in - let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in - let res,_ = glob_decompose_prod dummy_glob_constr in - let comblist = List.combine prms_decl res in - comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr))) -*) - -let ids_of_rawlist avoid rawl = - List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl) - - - -(** {1 Merging function graphs} *) - -(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec - uniform and ordinary ones) of mutual inductives [mib1] and [mib2] - remain uniform when linked by [lnk]. All parameters are - considered, ie we take parameters of the first inductive body of - [mib1] and [mib2]. - - Explanation: The two inductives have parameters, some of the first - are recursively uniform, some of the last are functional result of - the functional graph. - - (I x1 x2 ... xk ... xk' ... xn) - (J y1 y2 ... xl ... yl' ... ym) - - Problem is, if some rec unif params are linked to non rec unif - ones, they become non rec (and the following too). And functinal - argument have to be shifted at the end *) -let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id = - let _ = prstr "\nYOUHOU shift\n" in - let linked_targets = revlinked lnk2 in - let is_param_of_mib1 x = x < mib1.mind_nparams_rec in - let is_param_of_mib2 x = x < mib2.mind_nparams_rec in - let is_targetted_by_non_recparam_lnk1 i = - try - let targets = Link.find i linked_targets in - List.exists (fun x -> not (is_param_of_mib2 x)) targets - with Not_found -> false in - let mlnk1 = - Array.mapi - (fun i lkv -> - let isprm = is_param_of_mib1 i in - let prmlost = is_targetted_by_non_recparam_lnk1 i in - match isprm , prmlost, lnk1.(i) with - | true , true , _ -> Prm_arg i (* recparam becoming ordinary *) - | true , false , _-> Prm_stable i (* recparam remains recparam*) - | false , false , Funres -> Arg_funres - | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *) - | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *) - lnk1 in - let mlnk2 = - Array.mapi - (fun i lkv -> - (* Is this correct if some param of ind2 is lost? *) - let isprm = is_param_of_mib2 i in - match isprm , lnk2.(i) with - | true , Linked j when not (is_param_of_mib1 j) -> - Prm_arg j (* recparam becoming ordinary *) - | true , Linked j -> Prm_linked j (*recparam linked to recparam*) - | true , Unlinked -> Prm_stable i (* recparam remains recparam*) - | false , Linked j -> Arg_linked j (* Args of lnk2 lost *) - | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *) - | false , Funres -> Arg_funres - | true , Funres -> assert false (* fun res cannot be a rec param *) - ) - lnk2 in - let oib1 = mib1.mind_packets.(0) in - let oib2 = mib2.mind_packets.(0) in - (* count params remaining params *) - let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in - let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in - let bldprms arity_ctxt mlnk = - list_fold_lefti - (fun i (acc1,acc2,acc3,acc4) x -> - prstr (pr_merginfo mlnk.(i));prstr "\n"; - match mlnk.(i) with - | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4 - | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4 - | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4 - | Arg_funres -> acc1 , acc2 , acc3, x::acc4 - | _ -> acc1 , acc2 , acc3, acc4) - ([],[],[],[]) arity_ctxt in -(* let arity_ctxt2 = - build_raw_params oib2.mind_arity_ctxt - (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*) - let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in - let _ = prstr "\n\n\n" in - let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in - let _ = prstr "\notherprms1:\n" in - let _ = - List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); - prconstr (RelDecl.get_type decl); prstr "\n") - otherprms1 in - let _ = prstr "\notherprms2:\n" in - let _ = - List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n") - otherprms2 in - { - ident=id; - mib1=mib1; - oib1 = oib1; - mib2=mib2; - oib2 = oib2; - lnk1 = mlnk1; - lnk2 = mlnk2; - nrecprms1 = n_params1; - recprms1 = recprms1; - otherprms1 = otherprms1; - args1 = args1; - funresprms1 = funresprms1; - notherprms1 = Array.length mlnk1 - n_params1; - nfunresprms1 = List.length funresprms1; - nargs1 = List.length args1; - nrecprms2 = n_params2; - recprms2 = recprms2; - otherprms2 = otherprms2; - args2 = args2; - funresprms2 = funresprms2; - notherprms2 = Array.length mlnk2 - n_params2; - nargs2 = List.length args2; - nfunresprms2 = List.length funresprms2; - } - - - - -(** {1 Merging functions} *) - -exception NoMerge - -let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = - let lnk = Array.append shift.lnk1 shift.lnk2 in - match DAst.get c1, DAst.get c2 with - | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> - let _ = prstr "\nICI1!\n" in - let args = filter_shift_stable lnk (arr1 @ arr2) in - DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args) - | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge - | GLetIn(nme,bdy,typ,trm) , _ -> - let _ = prstr "\nICI2!\n" in - let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _, GLetIn(nme,bdy,typ,trm) -> - let _ = prstr "\nICI3!\n" in - let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _ -> let _ = prstr "\nICI4!\n" in - raise NoMerge - -let rec merge_app_unsafe c1 c2 shift filter_shift_stable = - let lnk = Array.append shift.lnk1 shift.lnk2 in - match DAst.get c1, DAst.get c2 with - | GApp(f1, arr1), GApp(f2,arr2) -> - let args = filter_shift_stable lnk (arr1 @ arr2) in - DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args) - (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(nme,bdy,typ,trm) , _ -> - let _ = prstr "\nICI2 '!\n" in - let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _, GLetIn(nme,bdy,typ,trm) -> - let _ = prstr "\nICI3 '!\n" in - let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - DAst.make @@ GLetIn(nme,bdy,typ,newtrm) - | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge - - - -(* Heuristic when merging two lists of hypothesis: merge every rec - calls of branch 1 with all rec calls of branch 2. *) -(* TODO: reecrire cette heuristique (jusqu'a merge_types) *) -let rec merge_rec_hyps shift accrec - (ltyp:(Name.t * glob_constr option * glob_constr option) list) - filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = - let is_app c = match DAst.get c with GApp _ -> true | _ -> false in - let mergeonehyp t reldecl = - match reldecl with - | (nme,x,Some ind) when is_app ind - -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) - | (nme,Some _,None) -> error "letins with recursive calls not treated yet" - | (nme,None,Some _) -> assert false - | (nme,None,None) | (nme,Some _,Some _) -> assert false in - let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in - match ltyp with - | [] -> [] - | (nme,None,Some t) :: lt when is_app t -> - let rechyps = List.map (mergeonehyp t) accrec in - rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable - | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable - - -let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = - List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec - - -let find_app (nme:Id.t) ltyp = - let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in - try - ignore - (List.map - (fun x -> - match x with - | _,None,Some c when is_app c -> raise (Found 0) - | _ -> ()) - ltyp); - false - with Found _ -> true - -let prnt_prod_or_letin nm letbdy typ = - match letbdy , typ with - | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy - | None , Some tp -> prNamedRConstr (string_of_name nm) tp - | _ , _ -> assert false - - -let rec merge_types shift accrec1 - (ltyp1:(Name.t * glob_constr option * glob_constr option) list) - (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2 - : (Name.t * glob_constr option * glob_constr option) list * glob_constr = - let _ = prstr "MERGE_TYPES\n" in - let _ = prstr "ltyp 1 : " in - let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in - let _ = prstr "\nltyp 2 : " in - let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in - let _ = prstr "\n" in - let res = - match ltyp1 with - | [] -> - let isrec1 = not (List.is_empty accrec1) in - let isrec2 = find_app ind2name ltyp2 in - let rechyps = - if isrec1 && isrec2 - then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *) - merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 - filter_shift_stable_right - @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2] - filter_shift_stable - else if isrec1 - (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *) - then - merge_rec_hyps shift accrec1 - (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable - else if isrec2 - then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 - filter_shift_stable_right - else ltyp2 in - let _ = prstr"\nrechyps : " in - let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in - let _ = prstr "MERGE CONCL : " in - let _ = prNamedRConstr "concl1" concl1 in - let _ = prstr " with " in - let _ = prNamedRConstr "concl2" concl2 in - let _ = prstr "\n" in - let concl = - merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in - let _ = prstr "FIN " in - let _ = prNamedRConstr "concl" concl in - let _ = prstr "\n" in - - rechyps , concl - | (nme,None, Some t1)as e ::lt1 -> - (match DAst.get t1 with - | GApp(f,carr) when isVarf ind1name f -> - merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 - | _ -> - let recres, recconcl2 = - merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,None,Some t1) :: recres) , recconcl2) - | (nme,Some bd, None) ::lt1 -> - (* FIXME: what if ind1name appears in bd? *) - let recres, recconcl2 = - merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,Some bd,None) :: recres) , recconcl2 - | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false - in - res - - -(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of - linked args [allargs2] to target args of [allargs1] as specified - in [shift]. [allargs1] and [allargs2] are in reverse order. Also - returns the list of unlinked vars of [allargs2]. *) -let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array) - (lnk:int merged_arg array) = - Array.fold_left_i - (fun i acc e -> - if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *) - else - match e with - | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc - | _ -> acc) - Id.Map.empty lnk - -let build_link_map allargs1 allargs2 lnk = - let allargs1 = - Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in - let allargs2 = - Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs2) in - build_link_map_aux allargs1 allargs2 lnk - - -(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two - constructor rawtypes [typcstr1] and [typcstr2]. [typcstr1] and - [typcstr2] contain all parameters (including rec. unif. ones) of - their inductive. - - if [typcstr1] and [typcstr2] are of the form: - - forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1) - forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2) - - we build: - - forall recparams1 (recparams2 without linked params), - forall ordparams1 (ordparams2 without linked params), - H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... - -> (newI x1 ... z1 x2 y2 ...z2 without linked params) - - where Hix' have been adapted, ie: - - linked vars have been changed, - - rec calls to I1 and I2 have been replaced by rec calls to - newI. More precisely calls to I1 and I2 have been merge by an - experimental heuristic (in particular if n o rec calls for I1 - or I2 is found, we use the conclusion as a rec call). See - [merge_types] above. - - Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint. - - TODO: return nothing if equalities (after linking) are contradictory. *) -let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr) - (typcstr2:glob_constr) : glob_constr = - (* FIXME: les noms des parametres corerspondent en principe au - parametres du niveau mib, mais il faudrait s'en assurer *) - (* shift.nfunresprmsx last args are functional result *) - let nargs1 = - shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in - let nargs2 = - shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in - let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in - let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in - (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) - let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in - let rest2 = change_vars linked_map rest2 in - let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in - let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in - let ltyp,concl2 = - merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in - let _ = prNamedRLDecl "ltyp result:" ltyp in - let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in - let revargs1 = - list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in - let _ = prNamedRLDecl "ltyp allargs1" allargs1 in - let _ = prNamedRLDecl "ltyp revargs1" revargs1 in - let revargs2 = - list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in - let _ = prNamedRLDecl "ltyp allargs2" allargs2 in - let _ = prNamedRLDecl "ltyp revargs2" revargs2 in - let typwithprms = - glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in - typwithprms - - -(** constructor numbering *) -let fresh_cstror_suffix , cstror_suffix_init = - let cstror_num = ref 0 in - (fun () -> - let res = string_of_int !cstror_num in - cstror_num := !cstror_num + 1; - res) , - (fun () -> cstror_num := 0) - -(** [merge_constructor_id id1 id2 shift] returns the identifier of the - new constructor from the id of the two merged constructor and - the merging info. *) -let merge_constructor_id id1 id2 shift:Id.t = - let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in - next_ident_fresh (Id.of_string id) - - - -(** [merge_constructors lnk shift avoid] merges the two list of - constructor [(name*type)]. These are translated to glob_constr - first, each of them having distinct var names. *) -let merge_constructors (shift:merge_infos) (avoid:Id.Set.t) - (typcstr1:(Id.t * glob_constr) list) - (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list = - List.flatten - (List.map - (fun (id1,rawtyp1) -> - List.map - (fun (id2,rawtyp2) -> - let typ = merge_one_constructor shift rawtyp1 rawtyp2 in - let newcstror_id = merge_constructor_id id1 id2 shift in - let _ = prstr "\n**************\n" in - newcstror_id , typ) - typcstr2) - typcstr1) - -(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two - inductive bodies [oib1] and [oib2], linking with [lnk], params - info in [shift], avoiding identifiers in [avoid]. *) -let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) - (oib2:one_inductive_body) = - (* building glob_constr type of constructors *) - let mkrawcor nme avoid typ = - (* first replace rel 1 by a varname *) - let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in - let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in - let lcstr1: glob_constr list = - Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in - (* add to avoid all indentifiers of lcstr1 *) - let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in - let lcstr2 = - Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in - let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in - - let params1 = - try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) - with e when CErrors.noncritical e -> [] in - let params2 = - try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) - with e when CErrors.noncritical e -> [] in - - let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in - let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in - - cstror_suffix_init(); - params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2 - - -(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual - inductive bodies [mib1] and [mib2] linking vars with - [lnk]. [shift] information on parameters of the new inductive. - For the moment, inductives are supposed to be non mutual. -*) -let merge_mutual_inductive_body - (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = - (* Mutual not treated, we take first ind body of each. *) - merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0) - - -let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *) - Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x - -let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = - let params = prms2 @ prms1 in - let resparams = - List.fold_left - (fun acc (nme,tp) -> - let _ = prstr "param :" in - let _ = prNamedRConstr (string_of_name nme) tp in - let _ = prstr " ; " in - let typ = glob_constr_to_constr_expr tp in - CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) - [] params in - let concl = Constrextern.extern_constr false (Global.env()) Evd.empty (EConstr.of_constr concl) in - let arity,_ = - List.fold_left - (fun (acc,env) decl -> - let nm = Context.Rel.Declaration.get_name decl in - let c = RelDecl.get_type decl in - let typ = Constrextern.extern_constr false env Evd.empty (EConstr.of_constr c) in - let newenv = Environ.push_rel (LocalAssum (nm,c)) env in - CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) - (concl,Global.env()) - (shift.funresprms2 @ shift.funresprms1 - @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in - resparams,arity - - - -(** [glob_constr_list_to_inductive_expr ident rawlist] returns the - induct_expr corresponding to the the list of constructor types - [rawlist], named ident. - FIXME: params et cstr_expr (arity) *) -let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift - (rawlist:(Id.t * glob_constr) list) = - let lident = (Loc.tag shift.ident), None in - let bindlist , cstr_expr = (* params , arities *) - merge_rec_params_and_arity prms1 prms2 shift mkSet in - let lcstor_expr : (bool * (lident * constr_expr)) list = - List.map (* zeta_normalize t ? *) - (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t)) - rawlist in - lident , bindlist , Some cstr_expr , lcstor_expr - - -let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = - match rdecl with - | LocalAssum (nme,t) -> - let t = EConstr.of_constr t in - let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in - DAst.make @@ GProd (nme,Explicit,traw,t2) - | LocalDef _ -> assert false - - -(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking - variables specified in [lnk]. Graphs are not supposed to be mutual - inductives for the moment. *) -let merge_inductive (ind1: inductive) (ind2: inductive) - (lnk1: linked_var array) (lnk2: linked_var array) id = - let env = Global.env() in - let mib1,_ = Inductive.lookup_mind_specif env ind1 in - let mib2,_ = Inductive.lookup_mind_specif env ind2 in - let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *) - (* compute params that become ordinary args (because linked to ord. args) *) - let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in - let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in - let _ = prstr "\nrawlist : " in - let _ = - List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in - let _ = prstr "\nend rawlist\n" in -(* FIX: retransformer en constr ici - let shift_prm = - { shift_prm with - recprms1=prms1; - recprms1=prms1; - } in *) - let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in - (* Declare inductive *) - let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] - false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in - (* Declare the mutual inductive block with its associated schemes *) - ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) - - -(* Find infos on identifier id. *) -let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = - let kn_of_id x = - let f_ref = Libnames.Ident (Loc.tag x) in - locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) - locate_constant f_ref in - try find_Function_infos (kn_of_id id) - with Not_found -> - user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme") - -(** [merge id1 id2 args1 args2 id] builds and declares a new inductive - type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occurring in both arrays [args1] and - [args2] are considered linked (i.e. are the same variable) in the - new graph. - - Warning: For the moment, repetitions of an id in [args1] or - [args2] are not supported. *) -let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array) - (args2:Id.t array) id : unit = - let finfo1 = find_Function_infos_safe id1 in - let finfo2 = find_Function_infos_safe id2 in - (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *) - (* We add one arg (functional arg of the graph) *) - let lnk1 = Array.make (Array.length args1 + 1) Unlinked in - let lnk2' = (* args2 may be linked to args1 members. FIXME: same - as above: vars may be linked inside args2?? *) - Array.mapi - (fun i c -> - match Array.findi (fun i x -> Id.equal x c) args1 with - | Some j -> Linked j - | None -> Unlinked) - args2 in - (* We add one arg (functional arg of the graph) *) - let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in - (* setting functional results *) - let _ = lnk1.(Array.length lnk1 - 1) <- Funres in - let _ = lnk2.(Array.length lnk2 - 1) <- Funres in - merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id - - -let remove_last_arg c = - let (x,y) = decompose_prod c in - let xnolast = List.rev (List.tl (List.rev x)) in - compose_prod xnolast y - -let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l) -let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l)) - -let remove_last_n_arg n c = - let (x,y) = decompose_prod c in - let xnolast = remove_n_last_list n x in - compose_prod xnolast y - -(* [funify_branches relinfo nfuns branch] returns the branch [branch] - of the relinfo [relinfo] modified to fit in a functional principle. - Things to do: - - remove indargs from rel applications - - replace *variables only* corresponding to function (recursive) - results by the actual function application. *) -let funify_branches relinfo nfuns branch = - let mut_induct, induct = - match relinfo.indref with - | None -> assert false - | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind - | _ -> assert false in - let is_dom c = - match Constr.kind c with - | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct - | _ -> false in - let _dom_i c = - assert (is_dom c); - match Constr.kind c with - | Ind((u,i)) | Construct((u,_),i) -> i - | _ -> assert false in - let _is_pred c shift = - match Constr.kind c with - | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches) - | _ -> false in - (* FIXME: *) - LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp) - - -let relprinctype_to_funprinctype relprinctype nfuns = - let relprinctype = EConstr.of_constr relprinctype in - let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in - assert (not relinfo.farg_in_concl); - assert (relinfo.indarg_in_concl); - (* first remove indarg and indarg_in_concl *) - let relinfo_noindarg = { relinfo with - indarg_in_concl = false; indarg = None; - concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in - (* the nfuns last induction arguments are functional ones: remove them *) - let relinfo_argsok = { relinfo_noindarg with - nargs = relinfo_noindarg.nargs - nfuns; - (* args is in reverse order, so remove fst *) - args = remove_n_fst_list nfuns relinfo_noindarg.args; - concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl)); - } in - let new_branches = - List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in - let relinfo_branches = { relinfo_argsok with branches = new_branches } in - relinfo_branches - -(* @article{ bundy93rippling, - author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill", - title = "Rippling: A Heuristic for Guiding Inductive Proofs", - journal = "Artificial Intelligence", - volume = "62", - number = "2", - pages = "185-253", - year = "1993", - url = "citeseer.ist.psu.edu/bundy93rippling.html" } - - *) diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 50b84731b..b95d64ce9 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,6 +1,5 @@ open Constr -(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : Tacmach.tactic -> bool -> diff --git a/plugins/funind/recdef_plugin.mlpack b/plugins/funind/recdef_plugin.mlpack index 2b443f2a1..755fa4f87 100644 --- a/plugins/funind/recdef_plugin.mlpack +++ b/plugins/funind/recdef_plugin.mlpack @@ -6,5 +6,4 @@ Functional_principles_proofs Functional_principles_types Invfun Indfun -Merge G_indfun diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index e395bdbc6..b21fbf0eb 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -15,6 +15,7 @@ open Vars open Environ open Inductive open Reduction +open Vmvalues open Vm open Context.Rel.Declaration @@ -134,7 +135,7 @@ let build_case_type dep p realargs c = (* La fonction de normalisation *) -let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t +let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t and nf_vtype env sigma v = nf_val env sigma v crazy_type @@ -144,7 +145,7 @@ and nf_whd env sigma whd typ = | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in + let vc = reduce_fun (nb_rel env) (codom p) in let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env sigma f typ @@ -191,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = else match stk with | Zapp args :: _ -> let inst = - Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i)) + Array.init nb_univs (fun i -> uni_lvl_val (arg args i)) in Univ.Instance.of_array inst | _ -> assert false @@ -254,7 +255,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in - let ci = case_info sw in + let ci = sw.sw_annot.Cbytecodes.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -266,14 +267,14 @@ and nf_predicate env sigma ind mip params v pT = match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) | Vfun f, _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in @@ -307,7 +308,7 @@ and nf_bargs env sigma b ofs t = and nf_fun env sigma f typ = let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = try decompose_prod env typ with DestKO -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d04bdb652..fc94a1013 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -485,7 +485,10 @@ let update_global_env () = (* XXX: Bullet hook, should be really moved elsewhere *) let _ = let hook n = - let prf = give_me_the_proof () in - (Proof_bullet.suggest prf) in + try + let prf = give_me_the_proof () in + (Proof_bullet.suggest prf) + with NoCurrentProof -> mt () + in Proofview.set_nosuchgoals_hook hook |