diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 21 | ||||
| -rw-r--r-- | kernel/closure.mli | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 5 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 74 | ||||
| -rw-r--r-- | kernel/names.ml | 19 | ||||
| -rw-r--r-- | kernel/names.mli | 7 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 11 | ||||
| -rw-r--r-- | kernel/reduction.ml | 25 |
8 files changed, 99 insertions, 65 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index ea9b2755f2..bc414d9715 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -346,7 +346,6 @@ and fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -376,7 +375,6 @@ let update v1 no t = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * constant | Zfix of fconstr * stack @@ -569,10 +567,6 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op - | FCase (ci,p,c,ve) -> - mkCase (ci, constr_fun lfts p, - constr_fun lfts c, - CArray.Fun1.map constr_fun lfts ve) | FCaseT (ci,p,c,ve,env) -> mkCase (ci, constr_fun lfts (mk_clos env p), constr_fun lfts c, @@ -646,9 +640,6 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -731,7 +722,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -842,7 +833,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -904,10 +894,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (depth, args, Zcase(ci,_,br)::s) -> - assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - kni info br.(c-1) (rargs@s) | (depth, args, ZcaseT(ci,_,br,e)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -924,7 +910,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) -> + (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) @@ -953,9 +939,6 @@ let rec zip_term zfun m stk = | [] -> m | Zapp args :: s -> zip_term zfun (mkApp(m, Array.map zfun args)) s - | Zcase(ci,p,br)::s -> - let t = mkCase(ci, zfun p, m, Array.map zfun br) in - zip_term zfun t s | ZcaseT(ci,p,br,e)::s -> let t = mkCase(ci, zfun (mk_clos e p), m, Array.map (fun b -> zfun (mk_clos e b)) br) in diff --git a/kernel/closure.mli b/kernel/closure.mli index a3b0e0f301..c6f212aa55 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -119,7 +119,6 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -136,7 +135,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * constant | Zfix of fconstr * stack diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c2..bf12d6c6dc 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -584,7 +584,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8c89abe940..e3457006d0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -30,8 +30,13 @@ let indices_matter = ref false let enforce_indices_matter () = indices_matter := true let is_indices_matter () = !indices_matter -(* Same as noccur_between but may perform reductions. - Could be refined more... *) +(* [weaker_noccur_between env n nvars t] (defined above), checks that + no de Bruijn indices between [n] and [n+nvars] occur in [t]. If + some such occurrences are found, then reduction is performed + (lazily for efficiency purposes) in order to determine whether + these occurrences are occurrences in the normal form. If the + occurrences are eliminated a witness reduct [Some t'] of [t] is + returned otherwise [None] is returned. *) let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else @@ -451,17 +456,30 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a -(* The recursive function that checks positivity and builds the list - of recursive arguments *) +(** [check_positivity_one ienv hyps (mind,i) nargs lcnames indlc] + checks the positivity of the [i]-th member of the mutually + inductive definition [mind]. It returns an [Rtree.t] which + represents the position of the recursive calls of inductive in [i] + for use by the guard condition (terms at these positions are + considered sub-terms) as well as the number of of non-uniform + arguments (used to generate induction schemes, so a priori less + relevant to the kernel). *) let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in - (* Checking the (strict) positivity of a constructor argument type [c] *) + (** Positivity of one argument [c] of a constructor (i.e. the + constructor [cn] has a type of the shape [… -> c … -> P], where, + more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in + (** If one of the inductives of the mutually inductive + block occurs in the left-hand side of a product, then + such an occurrence is a non-strictly-positive + recursive call. Occurrences in the right-hand side of + the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with None -> failwith_non_pos_list n ntypes [b] | Some b -> @@ -474,21 +492,35 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname Mrec _ -> compute_rec_par ienv hyps nmr largs | _ -> nmr) in + (** The case where one of the inductives of the mutually + inductive block occurs as an argument of another is not + known to be safe. So Coq rejects it. *) if not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) | Ind ind_kn -> - (* If the inductive type being defined appears in a - parameter, then we have a nested indtype *) + (** If one of the inductives of the mutually inductive + block being defined appears in a parameter, then we + have a nested inductive type. The positivity is then + discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) | err -> + (** If an inductive of the mutually inductive block + appears in any other way, then the positivy check gives + up. *) if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) + (** [check_positive_nested] handles the case of nested inductive + calls, that is, when an inductive types from the mutually + inductive block is called as an argument of an inductive types + (for the moment, this inductive type must be a previously + defined types, not one of the types of the mutually inductive + block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in @@ -497,12 +529,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let (lpar,auxlargs) = try List.chop auxnpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in - (* If the inductive appears in the args (non params) then the - definition is not positive. *) + (** Inductives of the inductive block being defined are only + allowed to appear nested in the parameters of another inductive + type. Not in the proper indices. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then failwith_non_pos_list n ntypes auxlargs; - (* We do not deal with imbricated mutual inductive types *) + (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) @@ -513,8 +546,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in let irecargs_nmr = - (* fails if the inductive type occurs non positively *) - (* with recursive parameters substituted *) + (** Checks that the "nesting" inductive type is covariant in + the relevant parameters. In other words, that the + (nested) parameters which are instantiated with + inductives of the mutually inductive block occur + positively in the types of the nested constructors. *) Array.map (function c -> let c' = hnf_prod_applist env' c lpar' in @@ -528,10 +564,14 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname in (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) - (* check the inductive types occur positively in the products of C, if - check_head=true, also check the head corresponds to a constructor of - the ith type *) - + (** [check_constructors ienv check_head nmr c] checks the positivity + condition in the type [c] of a constructor (i.e. that recursive + calls to the inductives of the mutually inductive definition + appear strictly positively in each of the arguments of the + constructor, see also [check_pos]). If [check_head] is [true], + then the type of the fully applied constructor (the "head" of + the type [c]) is checked to be the right (properly applied) + inductive type. *) and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_betadeltaiota env c) in @@ -571,6 +611,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) +(** [check_positivity kn env_ar params] checks that the mutually + inductive block [inds] is strictly positive. *) let check_positivity kn env_ar params inds = let ntypes = Array.length inds in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b6389..9e4e8cd61d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -204,7 +204,7 @@ struct DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = - "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" + "<"^DirPath.to_string p ^"#" ^ s ^"#"^ string_of_int i^">" let compare (x : t) (y : t) = if x == y then 0 @@ -282,6 +282,11 @@ module ModPath = struct | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l + let rec debug_to_string = function + | MPfile sl -> DirPath.to_string sl + | MPbound uid -> MBId.debug_to_string uid + | MPdot (mp,l) -> debug_to_string mp ^ "." ^ Label.to_string l + (** we compare labels first if both are MPdots *) let rec compare mp1 mp2 = if mp1 == mp2 then 0 @@ -375,12 +380,16 @@ module KerName = struct let modpath kn = kn.modpath let label kn = kn.knlabel - let to_string kn = + let to_string_gen mp_to_string kn = let dp = if DirPath.is_empty kn.dirpath then "." else "#" ^ DirPath.to_string kn.dirpath ^ "#" in - ModPath.to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel + + let to_string kn = to_string_gen ModPath.to_string kn + + let debug_to_string kn = to_string_gen ModPath.debug_to_string kn let print kn = str (to_string kn) @@ -500,9 +509,9 @@ module KerPair = struct let print kp = str (to_string kp) let debug_to_string = function - | Same kn -> "(" ^ KerName.to_string kn ^ ")" + | Same kn -> "(" ^ KerName.debug_to_string kn ^ ")" | Dual (knu,knc) -> - "(" ^ KerName.to_string knu ^ "," ^ KerName.to_string knc ^ ")" + "(" ^ KerName.debug_to_string knu ^ "," ^ KerName.debug_to_string knc ^ ")" let debug_print kp = str (debug_to_string kp) diff --git a/kernel/names.mli b/kernel/names.mli index 7cc4443752..77139f1c31 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -217,6 +217,9 @@ sig val to_string : t -> string + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) @@ -244,6 +247,10 @@ sig (** Display *) val to_string : t -> string + + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val print : t -> Pp.std_ppcmds (** Comparisons *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index b2142b43c7..331598d85a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -30,10 +30,6 @@ let output_dir = ".coq-native" (* Extension of genereted ml files, stored for debugging purposes *) let source_ext = ".native" -(* Global settings and utilies for interface with OCaml *) -let compiler_name = - if Dynlink.is_native then ocamlopt () else ocamlc () - let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed @@ -70,14 +66,15 @@ let call_compiler ml_filename = remove link_filename; remove (f ^ ".cmi"); let args = - (if Dynlink.is_native then "-shared" else "-c") + (if Dynlink.is_native then "opt" else "ocamlc") + ::(if Dynlink.is_native then "-shared" else "-c") ::"-o"::link_filename ::"-rectypes" ::"-w"::"a" ::include_dirs @ ["-impl"; ml_filename] in - if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args))); - try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename + if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); + try CUnix.sys_command (ocamlfind ()) args = Unix.WEXITED 0, link_filename with Unix.Unix_error (e,_,_) -> Pp.(msg_warning (str (Unix.error_message e))); false, link_filename diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b09367dd92..2cf3f88735 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -56,8 +56,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -91,9 +90,8 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + in snd (pure_rec lfts stk) (****************************************************************************) @@ -237,7 +235,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -250,7 +247,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -260,13 +256,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,p) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk @@ -532,8 +527,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) @@ -735,8 +730,8 @@ let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb false (fun _->None) env t1 t2 + Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + fconv cv_pb false (fun _->None) env t1 t2 let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None)) @@ -747,8 +742,8 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = try !default_conv ~l2r cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb false (fun _->None) env t1 t2 + Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion"); + fconv cv_pb false (fun _->None) env t1 t2 let default_conv_leq = default_conv CUMUL (* |