From d65eaaaa8cb311a0344a584df7a4b405034780b9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 15:56:51 +0100 Subject: Revert "Useless check when loading notations through import." This reverts commit 124734fd2c523909802d095abb37350519856864. --- interp/notation.ml | 8 ++++++++ interp/notation.mli | 4 ++++ toplevel/metasyntax.ml | 2 +- 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/interp/notation.ml b/interp/notation.ml index aeec4b6153..6040c33a5e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -516,6 +516,14 @@ let availability_of_prim_token n printer_scope local_scopes = (* Miscellaneous *) +let exists_notation_in_scope scopt ntn r = + let scope = match scopt with Some s -> s | None -> default_scope in + try + let sc = String.Map.find scope !scope_map in + let (r',_) = String.Map.find ntn sc.notations in + Pervasives.(=) r' r (** FIXME *) + with Not_found -> false + let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) diff --git a/interp/notation.mli b/interp/notation.mli index c66115cbdd..854c52b2c7 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *) val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) -> notation -> delimiters option -> global_reference +(** Checks for already existing notations *) +val exists_notation_in_scope : scope_name option -> notation -> + interpretation -> bool + (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> global_reference -> scope_name option list -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index cdbff17149..c8eff59b15 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1118,7 +1118,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) -- cgit v1.2.3 From 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 16:01:03 +0100 Subject: Fixing equality of notation_constrs. Fixes bug #4136. --- interp/notation.ml | 20 +++++++++++++++- interp/notation_ops.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++++ interp/notation_ops.mli | 2 ++ pretyping/glob_ops.mli | 3 +++ 4 files changed, 87 insertions(+), 1 deletion(-) diff --git a/interp/notation.ml b/interp/notation.ml index 6040c33a5e..f498761344 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -516,12 +516,30 @@ let availability_of_prim_token n printer_scope local_scopes = (* Miscellaneous *) +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + +let ntpe_eq t1 t2 = match t1, t2 with +| NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeConstrList, NtnTypeConstrList -> true +| NtnTypeBinderList, NtnTypeBinderList -> true +| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false + + +let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = + Id.equal id1 id2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + ntpe_eq tp1 tp2 + +let interpretation_eq (vars1, t1) (vars2, t2) = + List.equal vars_eq vars1 vars2 && + Notation_ops.eq_notation_constr t1 t2 + let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in let (r',_) = String.Map.find ntn sc.notations in - Pervasives.(=) r' r (** FIXME *) + interpretation_eq r' r with Not_found -> false let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c91c781591..2762dc0b8d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -170,6 +170,69 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 +let rec eq_notation_constr t1 t2 = match t1, t2 with +| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NVar id1, NVar id2 -> Id.equal id1 id2 +| NApp (t1, a1), NApp (t2, a2) -> + eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 +| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 && b1 == b2 +| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NProd (na1, t1, u1), NProd (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) + let eqpat (p1, t1) (p2, t2) = + List.equal cases_pattern_eq p1 p2 && + eq_notation_constr t1 t2 + in + let eqf (t1, (na1, o1)) (t2, (na2, o2)) = + let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in + eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + in + Option.equal eq_notation_constr o1 o2 && + List.equal eqf r1 r2 && + List.equal eqpat p1 p2 +| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + List.equal Name.equal nas1 nas2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + eq_notation_constr t1 t2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr u1 u2 && + eq_notation_constr r1 r2 +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) + let eq (na1, o1, t1) (na2, o2, t2) = + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 + in + Array.equal Id.equal ids1 ids2 && + Array.equal (List.equal eq) ts1 ts2 && + Array.equal eq_notation_constr us1 us2 && + Array.equal eq_notation_constr rs1 rs2 +| NSort s1, NSort s2 -> + Miscops.glob_sort_eq s1 s2 +| NPatVar p1, NPatVar p2 -> + Id.equal p1 p2 +| NCast (t1, c1), NCast (t2, c2) -> + eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 +| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false + + let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 7283ed6f12..c6770deea2 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -25,6 +25,8 @@ val ldots_var : Id.t (** FIXME: nothing to do here *) val eq_glob_constr : glob_constr -> glob_constr -> bool +val eq_notation_constr : notation_constr -> notation_constr -> bool + (** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 67f3cb4169..e514fd529e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,9 @@ open Glob_term val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cast_type_eq : ('a -> 'a -> bool) -> + 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) -- cgit v1.2.3 From b9048e5347c207b832d2bf2af022322025e59c08 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 19:43:24 +0100 Subject: Fixing representation of dynamics in votour (again). --- checker/values.ml | 12 ++++++------ checker/votour.ml | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/checker/values.ml b/checker/values.ml index c986415070..2b375651b1 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -332,19 +332,19 @@ let v_univopaques = (** Registering dynamic values *) -module StringOrd = +module IntOrd = struct - type t = string + type t = int let compare (x : t) (y : t) = compare x y end -module StringMap = Map.Make(StringOrd) +module IntMap = Map.Make(IntOrd) -let dyn_table : value StringMap.t ref = ref StringMap.empty +let dyn_table : value IntMap.t ref = ref IntMap.empty let register_dyn name t = - dyn_table := StringMap.add name t !dyn_table + dyn_table := IntMap.add name t !dyn_table let find_dyn name = - try StringMap.find name !dyn_table + try IntMap.find name !dyn_table with Not_found -> Any diff --git a/checker/votour.ml b/checker/votour.ml index d016b45632..f8d8f392ac 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -12,7 +12,7 @@ open Values (** Name of a value *) -type dyn = { dyn_tag : string; dyn_obj : Obj.t; } +type dyn = { dyn_tag : int; dyn_obj : Obj.t; } let to_dyn obj = (Obj.magic obj : dyn) -- cgit v1.2.3 From 2e8e5cc85bfb7f2339fc38babd2dec0026ff5aa4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 19:58:18 +0100 Subject: Functorized interface over object representation in votour. This gives more safety in object manipulation, as we delimit the uses of Obj functions, and allows for an alternative implementation of the representation of OCaml structures. --- checker/votour.ml | 152 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 108 insertions(+), 44 deletions(-) diff --git a/checker/votour.ml b/checker/votour.ml index f8d8f392ac..2db92853ab 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,11 +10,44 @@ open Values (** {6 Interactive visit of a vo} *) -(** Name of a value *) - -type dyn = { dyn_tag : int; dyn_obj : Obj.t; } +type 'a repr = +| INT of int +| STRING of string +| BLOCK of int * 'a array +| OTHER + +module type S = +sig + type obj + val input : in_channel -> obj + val repr : obj -> obj repr + val size : int list -> int +end + +module Repr : S = +struct + type obj = Obj.t + + let input chan = + let obj = input_value chan in + let () = CObj.register_shared_size obj in + obj + + let repr obj = + if Obj.is_block obj then + let tag = Obj.tag obj in + if tag = Obj.string_tag then STRING (Obj.magic obj) + else if tag < Obj.no_scan_tag then + let data = Obj.dup obj in + let () = Obj.set_tag data 0 in + BLOCK (tag, Obj.magic data) + else OTHER + else INT (Obj.magic obj) + + let size p = CObj.shared_size_of_pos p +end -let to_dyn obj = (Obj.magic obj : dyn) +(** Name of a value *) let rec get_name ?(extra=false) = function |Any -> "?" @@ -32,69 +65,101 @@ let rec get_name ?(extra=false) = function (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) -let get_string_in_tuple v o = +let get_string_in_tuple o = try - for i = 0 to Array.length v - 1 do - if v.(i) = String then - failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]"); + for i = 0 to Array.length o - 1 do + match Repr.repr o.(i) with + | STRING s -> + failwith (Printf.sprintf " [..%s..]" s) + | _ -> () done; "" with Failure s -> s (** Some details : tags, integer value for non-block, etc etc *) -let rec get_details v o = match v with - |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) -> - " [" ^ String.escaped (Obj.magic o : string) ^"]" - |Tuple (_,v) -> get_string_in_tuple v o - |(Sum _|Any) when Obj.is_block o -> - " [tag=" ^ string_of_int (Obj.tag o) ^"]" - |(Sum _|Any) -> - " [imm=" ^ string_of_int (Obj.magic o : int) ^"]" - |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]" - |Annot (s,v) -> get_details v o +let rec get_details v o = match v, Repr.repr o with + | (String | Any), STRING s -> + Printf.sprintf " [%s]" (String.escaped s) + |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o + |(Sum _|Any), BLOCK (tag, _) -> + Printf.sprintf " [tag=%i]" tag + |(Sum _|Any), INT i -> + Printf.sprintf " [imm=%i]" i + |Int, INT i -> Printf.sprintf " [imm=%i]" i + |Annot (s,v), _ -> get_details v o |_ -> "" let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)" + " (size "^ string_of_int (Repr.size p)^"w)" (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) -let access_children vs o pos = - Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs - +let access_children vs os pos = + if Array.length os = Array.length vs then + Array.mapi (fun i v -> v, os.(i), i::pos) vs + else raise Exit + +let access_list v o pos = + let rec loop o pos = match Repr.repr o with + | INT 0 -> [] + | BLOCK (0, [|hd; tl|]) -> + (v, hd, 0 :: pos) :: loop tl (1 :: pos) + | _ -> raise Exit + in + Array.of_list (loop o pos) + +let access_block o = match Repr.repr o with +| BLOCK (tag, os) -> (tag, os) +| _ -> raise Exit +let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit + +(** raises Exit if the object has not the expected structure *) let rec get_children v o pos = match v with - |Tuple (_,v) -> access_children v o pos - |Sum (_,_,vv) -> - if Obj.is_block o then access_children vv.(Obj.tag o) o pos - else [||] - |Array v -> access_children (Array.make (Obj.size o) v) o pos - |List v -> - let rec loop pos = function - | [] -> [] - | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol - in - Array.of_list (loop pos (Obj.magic o : Obj.t list)) + |Tuple (_, v) -> + let (_, os) = access_block o in + access_children v os pos + |Sum (_, _, vv) -> + begin match Repr.repr o with + | BLOCK (tag, os) -> access_children vv.(tag) os pos + | INT _ -> [||] + | _ -> raise Exit + end + |Array v -> + let (_, os) = access_block o in + access_children (Array.make (Array.length os) v) os pos + |List v -> access_list v o pos |Opt v -> - if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||] + begin match Repr.repr o with + | INT 0 -> [||] + | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] + | _ -> raise Exit + end |String | Int -> [||] |Annot (s,v) -> get_children v o pos - |Any -> - if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then - Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos)) - else [||] + |Any -> raise Exit |Dyn -> - let t = to_dyn o in - let tpe = find_dyn t.dyn_tag in - [|(Int, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|] + begin match Repr.repr o with + | BLOCK (0, [|id; o|]) -> + let n = access_int id in + let tpe = find_dyn n in + [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] + | _ -> raise Exit + end |Fail s -> failwith "forbidden" +let get_children v o pos = + try get_children v o pos + with Exit -> match Repr.repr o with + | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os + | _ -> [||] + type info = { nam : string; typ : value; - obj : Obj.t; + obj : Repr.obj; pos : int list } @@ -176,8 +241,7 @@ let visit_vo f = let l = read_line () in let seg = int_of_string l in seek_in ch segments.(seg).pos; - let o = (input_value ch : Obj.t) in - let () = CObj.register_shared_size o in + let o = Repr.input ch in let () = init () in visit segments.(seg).typ o [] done -- cgit v1.2.3 From 7061f479eaf148779d216ad6779cf153076fb005 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:40:29 +0100 Subject: Fixing wrong rel_context in checking positivity condition. Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. --- kernel/indtypes.ml | 9 ++++----- test-suite/success/Inductive.v | 9 +++++++++ 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 799471c68a..49bf3281fe 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -346,7 +346,7 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds - in (env_arities, params, inds) + in (env_arities, env_ar_par, params, inds) (************************************************************************) (************************************************************************) @@ -366,9 +366,8 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env0 nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c nargs err = let (lpar,c') = mind_extract_params nbpar c in - let env = push_rel_context lpar env0 in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) @@ -822,9 +821,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, params, inds) = typecheck_inductive env mie in + let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar params inds in + let (nmr,recargs) = check_positivity kn env_ar_par params inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 3d4257543a..04d92daad9 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -121,3 +121,12 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0. (* Check cross inference of evars from constructors *) Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. + +(* An example with reduction removing an occurrence of the inductive type in one of its argument *) + +Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). + +(* This type was considered as ill-formed before March 2015, while it + could be accepted considering that the type IND1 above was accepted *) + +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). -- cgit v1.2.3 From 72b5c9d35dddf774c1d517889cb8f48a932d7095 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:29:38 +0100 Subject: Fixing computation of non-recursively uniform arguments in the presence of let-ins. This fixes #3491. --- kernel/indtypes.ml | 1 + test-suite/bugs/closed/3491.v | 4 ++++ test-suite/success/Inductive.v | 16 +++++++++++++++- 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/3491.v diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 49bf3281fe..6b909824ba 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -485,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in + let largs = List.map (whd_betadeltaiota env) largs in let nmr1 = (match ra with Mrec _ -> compute_rec_par ienv hyps nmr largs diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v new file mode 100644 index 0000000000..fd394ddbc3 --- /dev/null +++ b/test-suite/bugs/closed/3491.v @@ -0,0 +1,4 @@ +(* Was failing while building the _rect scheme, due to wrong computation of *) +(* the number of non recursively uniform parameters in the presence of let-ins*) +Inductive list (A : Type) (T := A) : Type := + nil : list A | cons : T -> list T -> list A. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 04d92daad9..de18ed96ef 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -126,7 +126,21 @@ Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0. Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1). -(* This type was considered as ill-formed before March 2015, while it +(* These types were considered as ill-formed before March 2015, while they could be accepted considering that the type IND1 above was accepted *) Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). + +Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A. + +Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A. + +(* This type was ok before March 2015 *) + +Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A. + +(* This type was raising an anomaly when building the _rect scheme, + because of a wrong computation of the number of non-recursively + uniform parameters in the presence of let-ins (see #3491) *) + +Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. -- cgit v1.2.3 From c801b004bcb71f4f1db5d4cf260ef5a01fc8dde0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 24 Mar 2015 22:52:10 +0100 Subject: Updating test-suite (see previous commit). --- test-suite/bugs/opened/3491.v | 2 -- 1 file changed, 2 deletions(-) delete mode 100644 test-suite/bugs/opened/3491.v diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v deleted file mode 100644 index 9837b0ecb2..0000000000 --- a/test-suite/bugs/opened/3491.v +++ /dev/null @@ -1,2 +0,0 @@ -Fail Inductive list (A : Type) (T := A) : Type := - nil : list A | cons : T -> list T -> list A. -- cgit v1.2.3 From 810454922d4eeffaf9f92ccd7d8e10a1433de947 Mon Sep 17 00:00:00 2001 From: forest Date: Mon, 23 Mar 2015 14:54:18 +0100 Subject: correcting a bug with aliased when using Functional Scheme --- plugins/funind/functional_principles_types.ml | 36 +++++++++++++-------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 80167686aa..d4f49af4de 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -447,7 +447,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let first_fun = List.hd funs in - let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical first_fun) in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind @@ -498,27 +498,27 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis 0 (prove_princ_for_struct false 0 (Array.of_list funs)) (fun _ _ _ -> ()) - with e when Errors.noncritical e -> - begin - begin - try - let id = Pfedit.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Pfedit.delete_current_proof () - else () - else () - with e when Errors.noncritical e -> () - end; - raise (Defining_principle e) - end + with e when Errors.noncritical e -> + begin + begin + try + let id = Pfedit.get_current_proof_name () in + let s = Id.to_string id in + let n = String.length "___________princ_________" in + if String.length s >= n + then if String.equal (String.sub s 0 n) "___________princ_________" + then Pfedit.delete_current_proof () + else () + else () + with e when Errors.noncritical e -> () + end; + raise (Defining_principle e) + end in incr i; let opacity = - let finfos = find_Function_infos this_block_funs.(0) in + let finfos = find_Function_infos first_fun in try let equation = Option.get finfos.equation_lemma in Declareops.is_opaque (Global.lookup_constant equation) -- cgit v1.2.3 From f54d0b3158bc69a11fe579289f06f164ff5ccb94 Mon Sep 17 00:00:00 2001 From: jforest Date: Wed, 25 Mar 2015 10:27:13 +0100 Subject: Correcting a bug introduced by universes polymorphism --- plugins/funind/functional_principles_types.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d4f49af4de..deaf603ef0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,10 +274,11 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro in let hook = Lemmas.mk_hook (hook new_principle_type) in begin + let evd,_ = Typing.e_type_of ~refresh:true (Global.env ()) Evd.empty new_principle_type in Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (*FIXME*) Evd.empty + evd new_principle_type hook ; @@ -323,7 +324,7 @@ let generate_functional_principle let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry value in (*FIXME, no poly, nothing *) + let ce = Declare.definition_entry value in ignore( Declare.declare_constant name -- cgit v1.2.3 From 57109109a53c4bbbd7c8fa0acc142e47c80c5df7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Mar 2015 11:09:56 +0100 Subject: coqc: fix --help --- toplevel/usage.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6909d89440..4ee3bc4745 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -48,6 +48,10 @@ let print_usage_channel co command = \n -compile f compile Coq file f.v (implies -batch)\ \n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\ \n -quick quickly compile .v files to .vio files (skip proofs)\ +\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ +\n into fi.vo\ +\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ +\n proofs in each fi.vio\ \n\ \n -where print Coq's standard library location and exit\ \n -config print Coq's configuration information and exit\ -- cgit v1.2.3 From 12a77d49db68f88fc5886d6527217a761045865b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 25 Mar 2015 11:15:51 +0100 Subject: Use kernel names instead of user names when looking for coercions. (Fix for bug #4133) Note that, if someone was purposely modifying the user name of a type in order to disable a coercion, it no longer works. Hopefully, no one did. --- pretyping/classops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 559f5fe66a..055996de55 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2 - | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2 + | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) module ClTyp = struct -- cgit v1.2.3 From 1a519fc37e703b014e3bcc77de01edd82aabea5f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Mar 2015 09:44:12 +0100 Subject: Another example about the consequence of a wrong computation of the number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). --- test-suite/success/Inductive.v | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index de18ed96ef..0a4ae68733 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -144,3 +144,14 @@ Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IN uniform parameters in the presence of let-ins (see #3491) *) Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. + +(* An example of nested positivity which was rejected by the kernel + before 24 March 2015 (even with Unset Elimination Schemes to avoid + the _rect bug) due to the wrong computation of non-recursively + uniform parameters in list' *) + +Inductive list' (A:Type) (B:=A) := +| nil' : list' A +| cons' : A -> list' B -> list' A. + +Inductive tree := node : list' tree -> tree. -- cgit v1.2.3 From c1729637d4fe32ebe0268eb338fcf4d032bb5df7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Mar 2015 11:26:21 +0100 Subject: Fully fixing bug #3491 (anomaly when building _rect scheme in the presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. --- kernel/declarations.mli | 4 ++-- pretyping/inductiveops.ml | 16 +++++++++------- pretyping/inductiveops.mli | 10 ++++++++-- test-suite/success/Inductive.v | 19 +++++++++++++------ 4 files changed, 32 insertions(+), 17 deletions(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index cef920c6a5..c68e39ce33 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -139,7 +139,7 @@ type one_inductive_body = { mind_kelim : sorts_family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *) + mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) @@ -172,7 +172,7 @@ type mutual_inductive_body = { mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) - mind_nparams : int; (** Number of expected parameters *) + mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7f6a4a6442..dfdc24d480 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -365,14 +365,16 @@ let get_arity env ((ind,u),params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in let parsign = (* Dynamically detect if called with an instance of recursively - uniform parameter only or also of non recursively uniform + uniform parameter only or also of recursively non-uniform parameters *) - let parsign = mib.mind_params_ctxt in - let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in - if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then - snd (List.chop nnonrecparams mib.mind_params_ctxt) - else - parsign in + let nparams = List.length params in + if Int.equal nparams mib.mind_nparams then + mib.mind_params_ctxt + else begin + assert (Int.equal nparams mib.mind_nparams_rec); + let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in + snd (List.chop nnonrecparamdecls mib.mind_params_ctxt) + end in let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index af1783b705..7959759a3f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array (** Return constructor types in normal form *) val arities_of_constructors : env -> pinductive -> types array -(** An inductive type with its parameters *) +(** An inductive type with its parameters (transparently supports + reasoning either with only recursively uniform parameters or with all + parameters including the recursively non-uniform ones *) type inductive_family val make_ind_family : inductive puniverses * constr list -> inductive_family val dest_ind_family : inductive_family -> inductive puniverses * constr list @@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary -val get_arity : env -> inductive_family -> rel_context * sorts_family val get_constructors : env -> inductive_family -> constructor_summary array val get_projections : env -> inductive_family -> constant array option +(** [get_arity] returns the arity of the inductive family instantiated + with the parameters; if recursively non-uniform parameters are not + part of the inductive family, they appears in the arity *) +val get_arity : env -> inductive_family -> rel_context * sorts_family + val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : env -> bool -> inductive_family -> rel_context diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 0a4ae68733..9661b3bfac 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -139,12 +139,6 @@ Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A. Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A. -(* This type was raising an anomaly when building the _rect scheme, - because of a wrong computation of the number of non-recursively - uniform parameters in the presence of let-ins (see #3491) *) - -Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. - (* An example of nested positivity which was rejected by the kernel before 24 March 2015 (even with Unset Elimination Schemes to avoid the _rect bug) due to the wrong computation of non-recursively @@ -155,3 +149,16 @@ Inductive list' (A:Type) (B:=A) := | cons' : A -> list' B -> list' A. Inductive tree := node : list' tree -> tree. + +(* This type was raising an anomaly when building the _rect scheme, + because of a bug in Inductiveops.get_arity in the presence of + let-ins and recursively non-uniform parameters. *) + +Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. + +(* This type was raising an anomaly when building the _rect scheme, + because of a wrong computation of the number of non-recursively + uniform parameters when conversion is needed, leading the example to + hit the Inductiveops.get_arity bug mentioned above (see #3491) *) + +Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. -- cgit v1.2.3 From 578d73a8b8eb6623bfa688c1e3ed9d1442bd435f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 Mar 2015 09:24:00 +0100 Subject: Exporting memory representation of STM tasks for votour. --- checker/values.ml | 27 +++++++++++++++++++++++++++ checker/votour.ml | 2 +- 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/checker/values.ml b/checker/values.ml index 2b375651b1..cf93466b00 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -321,6 +321,33 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) +(** STM objects *) + +let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|]) +let v_states = v_pair Any v_frozen +let v_state = Tuple ("state", [|v_states; Any; v_bool|]) + +let v_vcs = + let data = Opt Any in + let vcs = + Tuple ("vcs", + [|Any; Any; + Tuple ("dag", + [|Any; Any; v_map Any (Tuple ("state_info", + [|Any; Any; Opt v_state; v_pair data Any|])) + |]) + |]) + in + let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in + vcs + +let v_uuid = Any +let v_request id doc = + Tuple ("request", [|Any; Any; doc; Any; id; String|]) +let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool) +let v_counters = Any +let v_stm_seg = v_pair v_tasks v_counters + (** Toplevel structures in a vo (see Cic.mli) *) let v_lib = diff --git a/checker/votour.ml b/checker/votour.ml index 2db92853ab..7c954d6f98 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -219,7 +219,7 @@ let visit_vo f = {name="library"; pos=0; typ=Values.v_lib}; {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Any}; + {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg}; {name="opaque proofs"; pos=0; typ=Values.v_opaques}; |] in while true do -- cgit v1.2.3 From 99ed6c907c3b2c4901ba51446e0b67696929e02e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Mar 2015 16:57:31 +0100 Subject: STM: avoid processing asynchronously empty proofs (Close: #4134) --- stm/stm.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index d9ecc8bcce..267f08ed5f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1638,6 +1638,7 @@ let collect_proof keep cur hd brkind id = | { expr = VernacPrint (PrintName _) } -> true | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in + let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with @@ -1687,7 +1688,8 @@ let collect_proof keep cur hd brkind id = else if keep == VtDrop then `Sync (no_name,None,`Aborted) else let rc = collect (Some cur) [] id in - if (keep == VtKeep || keep == VtKeepAsAxiom) && + if is_empty rc then make_sync `AlreadyEvaluated rc + else if (keep == VtKeep || keep == VtKeepAsAxiom) && (not(State.is_cached id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc -- cgit v1.2.3 From 7c7ceb48c12cad0bcfd59e1e8ae944d7c6137cbe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Mar 2015 16:57:55 +0100 Subject: Summary: fix code to detect functional values in summary --- library/summary.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/library/summary.ml b/library/summary.ml index 7e7628a1b7..8e2abbf15b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -66,6 +66,7 @@ let freeze_summaries ~marshallable : frozen = let fold id (_, decl) accu = (* to debug missing Lazy.force if marshallable <> `No then begin + let id, _ = Int.Map.find id !summaries in prerr_endline ("begin marshalling " ^ id); ignore(Marshal.to_string (decl.freeze_function marshallable) []); prerr_endline ("end marshalling " ^ id); -- cgit v1.2.3 From 5047734648d83890eb4fc4e5cff7ab77d46b48eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 25 Mar 2015 17:04:38 +0100 Subject: More clever representation of substituted Cemitcode. Module substitution is made nodewise, allowing to drop it for opaque terms in the VM. This saves a few useless substitutions. --- kernel/cemitcodes.ml | 44 ++++++++++++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 14 deletions(-) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 9ecae2b36f..c5f88f6f5d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -333,25 +333,41 @@ let subst_patch s (ri,pos) = let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv +let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) + type body_code = | BCdefined of to_patch | BCallias of pconstant | BCconstant -let subst_body_code s = function - | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u) - | BCconstant -> BCconstant - -type to_patch_substituted = body_code substituted - -let from_val = from_val - -let force = force subst_body_code - -let subst_to_patch_subst = subst_substituted - -let repr_body_code = repr_substituted +type to_patch_substituted = +| PBCdefined of to_patch substituted +| PBCallias of pconstant substituted +| PBCconstant + +let from_val = function +| BCdefined tp -> PBCdefined (from_val tp) +| BCallias cu -> PBCallias (from_val cu) +| BCconstant -> PBCconstant + +let force = function +| PBCdefined tp -> BCdefined (force subst_to_patch tp) +| PBCallias cu -> BCallias (force subst_pconstant cu) +| PBCconstant -> BCconstant + +let subst_to_patch_subst s = function +| PBCdefined tp -> PBCdefined (subst_substituted s tp) +| PBCallias cu -> PBCallias (subst_substituted s cu) +| PBCconstant -> PBCconstant + +let repr_body_code = function +| PBCdefined tp -> + let (s, tp) = repr_substituted tp in + (s, BCdefined tp) +| PBCallias cu -> + let (s, cu) = repr_substituted cu in + (s, BCallias cu) +| PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = init(); -- cgit v1.2.3 From 1bafb18f64ab1c929abfaf9c1b75f691914d9a46 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 Mar 2015 19:06:16 +0100 Subject: Fix vm compiler to refuse to compile code making use of inductives with more than 245 constructors (unsupported by OCaml's runtime). --- kernel/cbytegen.ml | 49 +++++++++++++++++++++++++++++++++++-------------- kernel/cbytegen.mli | 8 +++++--- kernel/csymtable.ml | 23 ++++++++++++++--------- kernel/declarations.mli | 2 +- kernel/declareops.ml | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 2 +- kernel/mod_typing.ml | 2 +- kernel/modops.ml | 2 +- kernel/nativelambda.ml | 9 ++++++--- kernel/term_typing.ml | 12 +++++++----- 11 files changed, 73 insertions(+), 40 deletions(-) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3b0c93b322..83f0a37214 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -329,6 +329,15 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) +(* Limitation due to OCaml's representation of non-constant + constructors: limited to 245 cases. *) + +exception TooLargeInductive of Id.t + +let check_compilable ib = + if ib.mind_nb_args < 245 then () + else raise (TooLargeInductive ib.mind_typename) + (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = let f_cont = @@ -357,6 +366,7 @@ let rec str_const c = begin let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in + let () = check_compilable oip in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) (Array.length args) then @@ -435,6 +445,7 @@ let rec str_const c = with Not_found -> let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in + let () = check_compilable oip in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num) @@ -489,9 +500,12 @@ let rec compile_fv reloc l sz cont = let rec get_allias env (kn,u as p) = let cb = lookup_constant kn env in let tps = cb.const_body_code in - (match Cemitcodes.force tps with - | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u') - | _ -> p) + match tps with + | None -> p + | Some tps -> + (match Cemitcodes.force tps with + | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u') + | _ -> p) (* Compiling expressions *) @@ -607,6 +621,7 @@ let rec compile_constr reloc c sz cont = let ind = ci.ci_ind in let mib = lookup_mind (fst ind) !global_env in let oib = mib.mind_packets.(snd ind) in + let () = check_compilable oib in let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in @@ -706,13 +721,14 @@ and compile_const = Kgetglobal (get_allias !global_env (kn,u)) :: cont) compile_constr reloc () args sz cont -let compile env c = +let compile fail_on_error env c = set_global_env env; init_fun_code (); Label.reset_label_counter (); let reloc = empty_comp_env () in - let init_code = compile_constr reloc c 0 [Kstop] in - let fv = List.rev (!(reloc.in_env).fv_rev) in + try + let init_code = compile_constr reloc c 0 [Kstop] in + let fv = List.rev (!(reloc.in_env).fv_rev) in (* draw_instr init_code; draw_instr !fun_code; Format.print_string "fv = "; @@ -722,21 +738,26 @@ let compile env c = | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format .print_string "\n"; Format.print_flush(); *) - init_code,!fun_code, Array.of_list fv - -let compile_constant_body env = function - | Undef _ | OpaqueDef _ -> BCconstant + Some (init_code,!fun_code, Array.of_list fv) + with TooLargeInductive tname -> + let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in + (Pp.(fn + (str "Cannot compile code for virtual machine as it uses inductive " ++ + Id.print tname ++ str " which has more than 245 constructors")); + None) + +let compile_constant_body fail_on_error env = function + | Undef _ | OpaqueDef _ -> Some BCconstant | Def sb -> let body = Mod_subst.force_constr sb in match kind_of_term body with | Const (kn',u) -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in - BCallias (get_allias env (con,u)) + Some (BCallias (get_allias env (con,u))) | _ -> - let res = compile env body in - let to_patch = to_memory res in - BCdefined to_patch + let res = compile fail_on_error env body in + Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 8fb6601a93..1128f0d0b7 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -5,10 +5,12 @@ open Declarations open Pre_env -val compile : env -> constr -> bytecodes * bytecodes * fv - (** init, fun, fv *) +val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *) + env -> constr -> (bytecodes * bytecodes * fv) option +(** init, fun, fv *) -val compile_constant_body : env -> constant_def -> body_code +val compile_constant_body : bool -> + env -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index ed8b0a6d1d..b29f06c652 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) = with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = - match Cemitcodes.force cb.const_body_code with - | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) - | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + match cb.const_body_code with + | None -> set_global (val_of_constant (kn,u)) + | Some code -> + match Cemitcodes.force code with + | BCdefined(code,pl,fv) -> + if Univ.Instance.is_empty u then + let v = eval_to_patch env (code,pl,fv) in + set_global v + else set_global (val_of_constant (kn,u)) + | BCallias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant (kn,u)) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = - try compile env c + try match compile true env c with + | Some v -> v + | None -> assert false with reraise -> let reraise = Errors.push reraise in let () = print_string "can not compile \n" in diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c68e39ce33..27c1c3f3f0 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -70,7 +70,7 @@ type constant_body = { const_hyps : Context.section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; - const_body_code : Cemitcodes.to_patch_substituted; + const_body_code : Cemitcodes.to_patch_substituted option; const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 48a6098eee..a7051d5c13 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -129,7 +129,7 @@ let subst_const_body sub cb = const_type = type'; const_proj = proj'; const_body_code = - Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code } diff --git a/kernel/environ.ml b/kernel/environ.ml index 0ebff440a1..a79abbb7e8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -473,7 +473,7 @@ type unsafe_type_judgment = { (*s Compilation of global declaration *) -let compile_constant_body = Cbytegen.compile_constant_body +let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found diff --git a/kernel/environ.mli b/kernel/environ.mli index de960ecccf..ede356e699 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -253,7 +253,7 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_def -> Cemitcodes.body_code +val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 99d353aae6..26dd45f5f3 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -97,7 +97,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let cb' = { cb with const_body = def; - const_body_code = Cemitcodes.from_val (compile_constant_body env' def); + const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def); const_universes = ctx' } in before@(lab,SFBconst(cb'))::after, c', ctx' diff --git a/kernel/modops.ml b/kernel/modops.ml index d8f319fa79..d52fe611c0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } + const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 543397df53..383f810295 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -375,9 +375,12 @@ let makeblock env cn u tag args = let rec get_allias env (kn, u as p) = let tps = (lookup_constant kn env).const_body_code in - match Cemitcodes.force tps with - | Cemitcodes.BCallias kn' -> get_allias env kn' - | _ -> p + match tps with + | None -> p + | Some tps -> + match Cemitcodes.force tps with + | Cemitcodes.BCallias kn' -> get_allias env kn' + | _ -> p (*i Global environment *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b54511e402..a316b4492b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -245,12 +245,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) let tps = (* FIXME: incompleteness of the bytecode vm: we compile polymorphic constants like opaque definitions. *) - if poly then Cemitcodes.from_val Cemitcodes.BCconstant + if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant) else - match proj with - | None -> Cemitcodes.from_val (compile_constant_body env def) - | Some pb -> - Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))) + let res = + match proj with + | None -> compile_constant_body env def + | Some pb -> + compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)) + in Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; -- cgit v1.2.3 From 2ef5fa7910e644d7eb39ee01024878a67086bd42 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Mar 2015 10:45:38 +0100 Subject: STM: change how proof mode switching commands are handled (decl_mode) This is likely to make nested proofs containing proof modes switch broken, but fixes the problems Arnaud has in his branch. It is possible that the classification function we have today is not fine grained enough. If a command that changes the proof mode has as the only global effect changing the proof mode, then the current code is fine. If it has a more global effect that persists after the proof is over but has no impact on the proof itself, then the old code is fine. As far as I can get, the proof mode switching commands have a global effect (changing parser) but also a proof effect (un/focusing). We don't have a classification for these. Today a command having a global effect is played twice: on the proof branch an on master. Of course if such command cannot work on master (where there is no finished proof for example) we need a special treatment for it. --- stm/stm.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 267f08ed5f..9e30cbbcd9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2126,9 +2126,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); - VCS.propagate_sideff (Some x); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () -- cgit v1.2.3 From c9074aa238e73bb932be67c67479b11bc95cd47a Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 14:21:13 +0100 Subject: add coqdep in distributed_exec, else make does not work. --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 45912615e2..9ff483603c 100644 --- a/configure.ml +++ b/configure.ml @@ -17,7 +17,7 @@ three non-negative, period-separed integers [...]" *) let vo_magic = 8591 let state_magic = 58501 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; -"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert"] +"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) -- cgit v1.2.3 From 5c6a50d6ec1d04bacd3e41ffbb88453fef92cd5d Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 14:24:54 +0100 Subject: Fix bug 4157, change the representation of inductive constructor when there is too many non constant constructors in the inductive type Conflicts: kernel/cbytegen.ml --- kernel/cbytecodes.ml | 1 + kernel/cbytecodes.mli | 1 + kernel/cbytegen.ml | 78 +++++++++++++++++++++++++++++++++++++-------------- kernel/vconv.ml | 4 +-- kernel/vm.ml | 32 ++++++++++++++++----- kernel/vm.mli | 3 +- pretyping/vnorm.ml | 4 +-- 7 files changed, 89 insertions(+), 34 deletions(-) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ae679027d6..91b701e0e6 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -24,6 +24,7 @@ let fix_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 +let max_tag = Obj.lazy_tag - 1 type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index b65268f722..4277b47710 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -20,6 +20,7 @@ val fix_tag : tag val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag +val max_tag : tag type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 83f0a37214..95ce2da344 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -329,14 +329,32 @@ let init_fun_code () = fun_code := [] (* Compilation of constructors and inductive types *) + (* Limitation due to OCaml's representation of non-constant constructors: limited to 245 cases. *) exception TooLargeInductive of Id.t let check_compilable ib = - if ib.mind_nb_args < 245 then () - else raise (TooLargeInductive ib.mind_typename) + if not (ib.mind_nb_args <= 0xFFFF && ib.mind_nb_constant <= 0xFFFF) then + raise (TooLargeInductive ib.mind_typename) + +(* Inv: arity > 0 *) + +let const_bn tag args = + if tag < max_tag then Const_bn(tag, args) + else + Const_bn(max_tag, + [|Const_b0 (tag - max_tag); + Const_bn (0, args) |]) + +let code_makeblock arity tag cont = + if tag < max_tag then + Kmakeblock(arity, tag) :: cont + else + Kmakeblock(arity, 0) :: Kpush :: (* Const_bn (0, args) *) + Kconst (Const_b0 (tag - max_tag)) :: (* Const_b0 (tag - max_tag)) *) + Kmakeblock(2, max_tag) :: cont (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = @@ -344,7 +362,8 @@ let code_construct tag nparams arity cont = add_pop nparams (if Int.equal arity 0 then [Kconst (Const_b0 tag); Kreturn 0] - else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]) + else + Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0]) in let lbl = Label.create() in fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; @@ -354,7 +373,6 @@ let get_strcst = function | Bstrconst sc -> sc | _ -> raise Not_found - let rec str_const c = match kind_of_term c with | Sort s -> Bstrconst (Const_sorts s) @@ -367,7 +385,7 @@ let rec str_const c = let oib = lookup_mind kn !global_env in let oip = oib.mind_packets.(j) in let () = check_compilable oip in - let num,arity = oip.mind_reloc_tbl.(i-1) in + let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if Int.equal (nparams + arity) (Array.length args) then (* spiwack: *) @@ -409,15 +427,15 @@ let rec str_const c = with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) - if Int.equal arity 0 then Bstrconst(Const_b0 num) + if Int.equal arity 0 then Bstrconst(Const_b0 tag) else let rargs = Array.sub args nparams arity in let b_args = Array.map str_const rargs in try let sc_args = Array.map get_strcst b_args in - Bstrconst(Const_bn(num, sc_args)) + Bstrconst(const_bn tag sc_args) with Not_found -> - Bmakeblock(num,b_args) + Bmakeblock(tag,b_args) else let b_args = Array.map str_const args in (* spiwack: tries first to apply the run-time compilation @@ -428,7 +446,7 @@ let rec str_const c = f), b_args) with Not_found -> - Bconstruct_app(num, nparams, arity, b_args) + Bconstruct_app(tag, nparams, arity, b_args) end | _ -> Bconstr c end @@ -624,7 +642,11 @@ let rec compile_constr reloc c sz cont = let () = check_compilable oib in let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in - let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in + let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) + let nblock = min nallblock (max_tag + 1) in + let lbl_blocks = Array.make nblock Label.no in + let neblock = max 0 (nallblock - max_tag) in + let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) let lbl_typ,fcode = @@ -644,6 +666,15 @@ let rec compile_constr reloc c sz cont = in lbl_blocks.(0) <- lbl_accu; let c = ref code_accu in + (* perform the extra match if needed (to many block constructor) *) + if neblock <> 0 then begin + let lbl_b, code_b = + label_code ( + Kpushfields 2 :: Kacc 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(max_tag) <- lbl_b; + c := code_b + end; + (* Compiling regular constructor branches *) for i = 0 to Array.length tbl - 1 do let tag, arity = tbl.(i) in @@ -655,19 +686,22 @@ let rec compile_constr reloc c sz cont = else let args, body = decompose_lam branchs.(i) in let nargs = List.length args in - let lbl_b,code_b = - label_code( - if Int.equal nargs arity then + let code_b = + if Int.equal nargs arity then Kpushfields arity :: - compile_constr (push_param arity sz_b reloc) + compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in Kpushfields arity :: - compile_constr reloc branchs.(i) (sz_b+arity) - (Kappterm(arity,sz_appterm) :: !c)) - in - lbl_blocks.(tag) <- lbl_b; + compile_constr reloc branchs.(i) (sz_b+arity) + (Kappterm(arity,sz_appterm) :: !c) in + let code_b = + if tag < max_tag then code_b + else Kacc 1::Kpop 2::code_b in + let lbl_b,code_b = label_code code_b in + if tag < max_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - max_tag) <- lbl_b; c := code_b done; c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; @@ -692,9 +726,10 @@ and compile_str_cst reloc sc sz cont = | Bstrconst sc -> Kconst sc :: cont | Bmakeblock(tag,args) -> let nargs = Array.length args in - comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont) + comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont) | Bconstruct_app(tag,nparams,arity,args) -> - if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont + if Int.equal (Array.length args) 0 then + code_construct tag nparams arity cont else comp_app (fun _ _ _ cont -> code_construct tag nparams arity cont) @@ -743,7 +778,8 @@ let compile fail_on_error env c = let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str " which has more than 245 constructors")); + Id.print tname ++ str + " which has more than 65535 constant constructors or more than 65535 non-constant constructors")); None) let compile_constant_body fail_on_error env = function diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 29315b0a90..6044e1846b 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -63,9 +63,9 @@ and conv_whd env pb k whd1 whd2 cu = else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Vconstr_block b1, Vconstr_block b2 -> + | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) -> let sz = bsize b1 in - if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then + if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then let rcu = ref cu in for i = 0 to sz - 1 do rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu diff --git a/kernel/vm.ml b/kernel/vm.ml index 2cc1efe431..65d84e882d 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -79,7 +79,7 @@ type vprod type vfun type vfix type vcofix -type vblock +type vblock type arguments type vm_env @@ -161,7 +161,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of vblock + | Vconstr_block of int * vblock | Vatom_stk of atom * stack (*************************************************) @@ -224,7 +224,13 @@ let whd_val : values -> whd = | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) - else Vconstr_block(Obj.obj o) + else + if tag = max_tag then + let tag = Obj.obj (Obj.field o 0) + max_tag in + let block = Obj.obj (Obj.field o 1) in + Vconstr_block(tag, block) + else + Vconstr_block(tag, Obj.obj o) @@ -518,10 +524,22 @@ let type_of_switch sw = let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else - let b = Obj.new_block tag arity in - for i = 0 to arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; + let init b = + for i = 0 to arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done in + let b = + if tag < max_tag then + let b = Obj.new_block tag arity in + init b; + b + else + let b0 = Obj.new_block 0 arity in + init b0; + let b = Obj.new_block max_tag 2 in + Obj.set_field b 0 (Obj.repr (tag - max_tag)); + Obj.set_field b 1 (Obj.repr b0); + b in val_of_obj b let apply_switch sw arg = diff --git a/kernel/vm.mli b/kernel/vm.mli index 295ea83c49..139202f090 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -46,7 +46,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of vblock + | Vconstr_block of int * vblock | Vatom_stk of atom * stack (** Constructors *) @@ -94,7 +94,6 @@ val reduce_cofix : int -> vcofix -> values array * values array (** Block *) -val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 19613c4e06..3c302f8da3 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -165,8 +165,8 @@ and nf_whd env whd typ = let _, args = nf_args env vargs t in mkApp(cfd,args) | Vconstr_const n -> construct_of_constr_const env n typ - | Vconstr_block b -> - let capp,ctyp = construct_of_constr_block env (btag b) typ in + | Vconstr_block (tag,b) -> + let capp,ctyp = construct_of_constr_block env tag typ in let args = nf_bargs env b ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> -- cgit v1.2.3 From f920ae56ffacf80f85dcf33d3f1ccf0acb4375b1 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 16:48:32 +0100 Subject: fix compilation --- dev/vm_printers.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 4578a3b33d..a583e2e54e 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -74,14 +74,14 @@ and ppwhd whd = | Vfix _ -> print_vfix() | Vcofix _ -> print_string "cofix" | Vconstr_const i -> print_string "C(";print_int i;print_string")" - | Vconstr_block b -> ppvblock b + | Vconstr_block (tag,b) -> ppvblock tag b | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s -and ppvblock b = +and ppvblock tag b = open_hbox(); - print_string "Cb(";print_int (btag b); + print_string "Cb(";print_int tag; let n = bsize b in for i = 0 to n -1 do print_string ",";ppvalues (bfield b i) -- cgit v1.2.3 From 00894adf6fc11f4336a3ece0c347676bbf0b4c11 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Thu, 26 Mar 2015 19:00:00 +0100 Subject: allows the vm to deal with inductive type with 8388607 constant constructors and 8388851 non-constant constructor. --- kernel/byterun/coq_fix_code.c | 4 ++-- kernel/byterun/coq_interp.c | 4 ++-- kernel/cbytegen.ml | 13 ++++++++++--- kernel/cemitcodes.ml | 2 +- 4 files changed, 15 insertions(+), 8 deletions(-) diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 52dc49bf8e..f1f9c92153 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) { uint32_t i, sizes, const_size, block_size; COPY32(q,p); p++; sizes=*q++; - const_size = sizes & 0xFFFF; - block_size = sizes >> 16; + const_size = sizes & 0x7FFFFF; + block_size = sizes >> 23; sizes = const_size + block_size; for(i=0; i 0 *) @@ -778,8 +786,7 @@ let compile fail_on_error env c = let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ - Id.print tname ++ str - " which has more than 65535 constant constructors or more than 65535 non-constant constructors")); + Id.print tname ++ str str_max_constructors)); None) let compile_constant_body fail_on_error env = function diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index c5f88f6f5d..aa1bba02d7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -223,7 +223,7 @@ let emit_instr = function slot_for_annot annot;out_int sz | Kswitch (tbl_const, tbl_block) -> out opSWITCH; - out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); + out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block -- cgit v1.2.3 From 924a6e99f85aa0d70d42e753d6901b067ebf8f1d Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 27 Mar 2015 06:44:02 +0100 Subject: use a more compact representation of non-constant constructors for which there corresponding tag are greater than max_variant_tag. The code is a merge with the patch proposed by Bruno on github barras/coq commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c --- dev/vm_printers.ml | 6 +++--- kernel/cbytecodes.ml | 4 +++- kernel/cbytecodes.mli | 2 +- kernel/cbytegen.ml | 52 +++++++++++++++++++++++++-------------------------- kernel/vconv.ml | 3 ++- kernel/vm.ml | 36 +++++++++++------------------------ kernel/vm.mli | 3 ++- pretyping/vnorm.ml | 17 ++++++++++++----- 8 files changed, 60 insertions(+), 63 deletions(-) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index a583e2e54e..4578a3b33d 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -74,14 +74,14 @@ and ppwhd whd = | Vfix _ -> print_vfix() | Vcofix _ -> print_string "cofix" | Vconstr_const i -> print_string "C(";print_int i;print_string")" - | Vconstr_block (tag,b) -> ppvblock tag b + | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s -and ppvblock tag b = +and ppvblock b = open_hbox(); - print_string "Cb(";print_int tag; + print_string "Cb(";print_int (btag b); let n = bsize b in for i = 0 to n -1 do print_string ",";ppvalues (bfield b i) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 91b701e0e6..700de50200 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -24,7 +24,9 @@ let fix_tag = 3 let switch_tag = 4 let cofix_tag = 5 let cofix_evaluated_tag = 6 -let max_tag = Obj.lazy_tag - 1 +(* It could be greate if OCaml export this value, + So fixme if this occur in a new version of OCaml *) +let last_variant_tag = 245 type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 4277b47710..fbb40ffd1f 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -20,7 +20,7 @@ val fix_tag : tag val switch_tag : tag val cofix_tag : tag val cofix_evaluated_tag : tag -val max_tag : tag +val last_variant_tag : tag type structured_constant = | Const_sorts of sorts diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0cd250113d..45808b0729 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -331,12 +331,12 @@ let init_fun_code () = fun_code := [] (* Limitation due to OCaml's representation of non-constant - constructors: limited to 245 cases. *) + constructors: limited to 245 + 1 (0 tag) cases. *) exception TooLargeInductive of Id.t let max_nb_const = 0x7FFFFF -let max_nb_block = 0x7FFFFF + max_tag - 1 +let max_nb_block = 0x7FFFFF + last_variant_tag - 1 let str_max_constructors = Format.sprintf @@ -350,19 +350,17 @@ let check_compilable ib = (* Inv: arity > 0 *) let const_bn tag args = - if tag < max_tag then Const_bn(tag, args) + if tag < last_variant_tag then Const_bn(tag, args) else - Const_bn(max_tag, - [|Const_b0 (tag - max_tag); - Const_bn (0, args) |]) + Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) + let code_makeblock arity tag cont = - if tag < max_tag then + if tag < last_variant_tag then Kmakeblock(arity, tag) :: cont else - Kmakeblock(arity, 0) :: Kpush :: (* Const_bn (0, args) *) - Kconst (Const_b0 (tag - max_tag)) :: (* Const_b0 (tag - max_tag)) *) - Kmakeblock(2, max_tag) :: cont + Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) :: + Kmakeblock(arity+1, last_variant_tag) :: cont (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = @@ -370,8 +368,11 @@ let code_construct tag nparams arity cont = add_pop nparams (if Int.equal arity 0 then [Kconst (Const_b0 tag); Kreturn 0] + else if tag < last_variant_tag then + [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] else - Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0]) + [Kconst (Const_b0 (tag - last_variant_tag)); + Kmakeblock(arity+1, last_variant_tag); Kreturn 0]) in let lbl = Label.create() in fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; @@ -651,9 +652,9 @@ let rec compile_constr reloc c sz cont = let tbl = oib.mind_reloc_tbl in let lbl_consts = Array.make oib.mind_nb_constant Label.no in let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) - let nblock = min nallblock (max_tag + 1) in + let nblock = min nallblock (last_variant_tag + 1) in let lbl_blocks = Array.make nblock Label.no in - let neblock = max 0 (nallblock - max_tag) in + let neblock = max 0 (nallblock - last_variant_tag) in let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) @@ -674,12 +675,12 @@ let rec compile_constr reloc c sz cont = in lbl_blocks.(0) <- lbl_accu; let c = ref code_accu in - (* perform the extra match if needed (to many block constructor) *) + (* perform the extra match if needed (to many block constructors) *) if neblock <> 0 then begin let lbl_b, code_b = label_code ( - Kpushfields 2 :: Kacc 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in - lbl_blocks.(max_tag) <- lbl_b; + Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in + lbl_blocks.(last_variant_tag) <- lbl_b; c := code_b end; @@ -694,25 +695,24 @@ let rec compile_constr reloc c sz cont = else let args, body = decompose_lam branchs.(i) in let nargs = List.length args in + let code_b = if Int.equal nargs arity then - Kpushfields arity :: - compile_constr (push_param arity sz_b reloc) + compile_constr (push_param arity sz_b reloc) body (sz_b+arity) (add_pop arity (branch :: !c)) else let sz_appterm = if is_tailcall then sz_b + arity else arity in - Kpushfields arity :: - compile_constr reloc branchs.(i) (sz_b+arity) + compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c) in let code_b = - if tag < max_tag then code_b - else Kacc 1::Kpop 2::code_b in - let lbl_b,code_b = label_code code_b in - if tag < max_tag then lbl_blocks.(tag) <- lbl_b - else lbl_eblocks.(tag - max_tag) <- lbl_b; + if tag < last_variant_tag then Kpushfields arity :: code_b + else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in + let lbl_b,code_b = label_code code_b in + if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; c := code_b done; - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; let code_sw = match branch1 with (* spiwack : branch1 can't be a lbl anymore it's a Branch instead diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 6044e1846b..1c31cc0414 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -63,7 +63,8 @@ and conv_whd env pb k whd1 whd2 cu = else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if Int.equal i1 i2 then cu else raise NotConvertible - | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) -> + | Vconstr_block b1, Vconstr_block b2 -> + let tag1 = btag b1 and tag2 = btag b2 in let sz = bsize b1 in if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then let rcu = ref cu in diff --git a/kernel/vm.ml b/kernel/vm.ml index 65d84e882d..d4bf461b39 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -161,7 +161,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of int * vblock + | Vconstr_block of vblock | Vatom_stk of atom * stack (*************************************************) @@ -225,15 +225,8 @@ let whd_val : values -> whd = | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else - if tag = max_tag then - let tag = Obj.obj (Obj.field o 0) + max_tag in - let block = Obj.obj (Obj.field o 1) in - Vconstr_block(tag, block) - else - Vconstr_block(tag, Obj.obj o) - - - + Vconstr_block(Obj.obj o) + (************************************************) (* Abstrct machine ******************************) (************************************************) @@ -524,22 +517,15 @@ let type_of_switch sw = let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else - let init b = - for i = 0 to arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done in - let b = - if tag < max_tag then - let b = Obj.new_block tag arity in - init b; - b + let b, ofs = + if tag < last_variant_tag then Obj.new_block tag arity, 0 else - let b0 = Obj.new_block 0 arity in - init b0; - let b = Obj.new_block max_tag 2 in - Obj.set_field b 0 (Obj.repr (tag - max_tag)); - Obj.set_field b 1 (Obj.repr b0); - b in + 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 = diff --git a/kernel/vm.mli b/kernel/vm.mli index 139202f090..5190356828 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -46,7 +46,7 @@ type whd = | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option | Vconstr_const of int - | Vconstr_block of int * vblock + | Vconstr_block of vblock | Vatom_stk of atom * stack (** Constructors *) @@ -94,6 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array (** Block *) +val btag : vblock -> int val bsize : vblock -> int val bfield : vblock -> int -> values diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 3c302f8da3..8198db1b8a 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -165,9 +165,16 @@ and nf_whd env whd typ = let _, args = nf_args env vargs t in mkApp(cfd,args) | Vconstr_const n -> construct_of_constr_const env n typ - | Vconstr_block (tag,b) -> + | Vconstr_block b -> + let tag = btag b in + let (tag,ofs) = + if tag = Cbytecodes.last_variant_tag then + match whd_val (bfield b 0) with + | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1) + | _ -> assert false + else (tag, 0) in let capp,ctyp = construct_of_constr_block env tag typ in - let args = nf_bargs env b ctyp in + let args = nf_bargs env b ofs ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> let c,typ = constr_type_of_idkey env idkey in @@ -242,14 +249,14 @@ and nf_args env vargs t = t := subst1 c codom; c) in !t,args -and nf_bargs env b t = +and nf_bargs env b ofs t = let t = ref t in - let len = bsize b in + let len = bsize b - ofs in let args = Array.init len (fun i -> let _,dom,codom = decompose_prod env !t in - let c = nf_val env (bfield b i) dom in + let c = nf_val env (bfield b (i+ofs)) dom in t := subst1 c codom; c) in args -- cgit v1.2.3 From 0da60299fa3abd4a84c7c673fa8f9ed202c84188 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 27 Mar 2015 09:29:00 +0100 Subject: Properly handle extra "clean" targets with coq_makefile. --- tools/coq_makefile.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index e2bca2acfb..72735e900f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -536,9 +536,13 @@ let include_dirs (inc_ml,inc_i,inc_r) = List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n"; end +let double_colon = ["clean"; "cleanall"; "archclean"] + let custom sps = let pr_path (file,dependencies,is_phony,com) = - print file; print ": "; print dependencies; print "\n"; + print file; + print (if List.mem file double_colon then ":: " else ": "); + print dependencies; print "\n"; if com <> "" then (print "\t"; print com; print "\n"); print "\n" in -- cgit v1.2.3 From a5a333ddbf5c27320e767ca0611caf8a821449aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Mar 2015 12:02:30 +0100 Subject: STM: refine the notion of "simply a tactic" When a worker sends back a system state to master, it tries to just send a delta. If the command is a simple tactic, then only the proof state changes. Now, what is a simple tactic? 1. a tactic 2. that does not change the environment Check 1. was surely incomplete. Now it is: VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ Is it complete? --- stm/stm.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 9e30cbbcd9..477ca1f0dc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1093,6 +1093,9 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else + let is_tac = function + | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true + | _ -> false in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next @@ -1110,8 +1113,8 @@ end = struct (* {{{ *) if State.is_cached id then Some (State.get_cached id) else None in match prev, this with | _, None -> None - | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n - when State.same_env o n -> (* A pure tactic *) + | Some (prev, o, `Cmd { cast = { expr }}), Some n + when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> msg_warning (str "Sending back a fat state"); -- cgit v1.2.3 From e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Mar 2015 18:17:03 +0100 Subject: Putting the From parameter of the Require command into the AST. --- intf/vernacexpr.mli | 2 +- parsing/g_vernac.ml4 | 5 ++--- printing/ppvernac.ml | 8 ++++++-- stm/texmacspp.ml | 19 +++++++++++-------- toplevel/vernacentries.ml | 8 ++++++-- 5 files changed, 26 insertions(+), 16 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 07891d0b48..450b1af0f9 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -316,7 +316,7 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - export_flag option * lreference list + lreference option * export_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of reference or_by_notation | VernacCoercion of obsolete_locality * reference or_by_notation * diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 70a8ec5522..cf7f6af28b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -465,11 +465,10 @@ GEXTEND Gram (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> - VernacRequire (export, qidl) + VernacRequire (None, export, qidl) | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token ; qidl = LIST1 global -> - let qidl = List.map (Libnames.join_reference ns) qidl in - VernacRequire (export, qidl) + VernacRequire (Some ns, export, qidl) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e0b94669c2..89ffae4b3e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -863,10 +863,14 @@ module Make | VernacNameSectionHypSet (id,set) -> return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ str ":="++spc()++pr_using set)) - | VernacRequire (exp, l) -> + | VernacRequire (from, exp, l) -> + let from = match from with + | None -> mt () + | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc () + in return ( hov 2 - (keyword "Require" ++ spc() ++ pr_require_token exp ++ + (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++ prlist_with_sep sep pr_module l) ) | VernacImport (f,l) -> diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index a0979f8b15..083fd54bfa 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -617,14 +617,17 @@ let rec tmpp v loc = | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id) | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id) | VernacNameSectionHypSet _ as x -> xmlTODO loc x - | VernacRequire (None,l) -> - xmlRequire loc (List.map (fun ref -> - xmlReference ref) l) - | VernacRequire (Some true,l) -> - xmlRequire loc ~attr:["export","true"] (List.map (fun ref -> - xmlReference ref) l) - | VernacRequire (Some false,l) -> - xmlRequire loc ~attr:["import","true"] (List.map (fun ref -> + | VernacRequire (from, import, l) -> + let import = match import with + | None -> [] + | Some true -> ["export","true"] + | Some false -> ["import","true"] + in + let from = match from with + | None -> [] + | Some r -> ["from", Libnames.string_of_reference r] + in + xmlRequire loc ~attr:(from @ import) (List.map (fun ref -> xmlReference ref) l) | VernacImport (true,l) -> xmlImport loc ~attr:["export","true"] (List.map (fun ref -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a4ffae0fff..62e5f0a324 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -749,7 +749,11 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) -let vernac_require import qidl = +let vernac_require from import qidl = + let qidl = match from with + | None -> qidl + | Some ns -> List.map (Libnames.join_reference ns) qidl + in let qidl = List.map qualid_of_reference qidl in let modrefl = List.map Library.try_locate_qualified_library qidl in if Dumpglob.dump () then @@ -1884,7 +1888,7 @@ let interp ?proof locality poly c = | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set - | VernacRequire (export, qidl) -> vernac_require export qidl + | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (local,r,s,t) -> vernac_coercion locality poly local r s t -- cgit v1.2.3 From f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 27 Mar 2015 19:46:40 +0100 Subject: Normalize scope names before storing them in vo files. (Fix for bug #4162) Note that I do not understand why the delimiter map is incomplete on loading and thus was causing a failure. So, while the patch is the proper way to deal with notation scopes, there might be another bug lurking in this file. --- interp/notation.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/interp/notation.ml b/interp/notation.ml index f498761344..80db2cb396 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -136,10 +136,6 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = if Int.equal i 1 then - let sc = match sc with - | Scope sc -> Scope (normalize_scope sc) - | _ -> sc - in scope_stack := if op then sc :: !scope_stack else List.except scope_eq sc !scope_stack @@ -166,7 +162,7 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope sc)) + Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) let empty_scope_stack = [] -- cgit v1.2.3 From 2c7d80e8234797da38d54326b914ded7f343d062 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2015 15:03:19 +0200 Subject: Fixing bug #4165. The context matching function was dropping the surrounding context in let-ins. --- pretyping/constr_matching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index cf6ac619dd..f05812979d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -373,7 +373,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = authorized_occ env sigma partial_app closed pat c mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function - | [c1;c2] -> mkLetIn (x,c1,t,c2) + | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2)) | _ -> assert false in let next () = -- cgit v1.2.3 From 598ac5ca1ac87fbd9152c7da1812a6ae7aa1e7bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2015 15:16:09 +0200 Subject: Adding test for bug #4165. --- test-suite/bugs/closed/4165.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4165.v diff --git a/test-suite/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v new file mode 100644 index 0000000000..8e0a62d35c --- /dev/null +++ b/test-suite/bugs/closed/4165.v @@ -0,0 +1,7 @@ +Lemma foo : True. +Proof. +pose (fun x : nat => (let H:=true in x)) as s. +match eval cbv delta [s] in s with +| context C[true] => + let C':=context C[false] in pose C' as s' +end. -- cgit v1.2.3 From ab299ba2d7d9ff18d65cc999dca127d2ce5e9c5d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 Mar 2015 14:56:33 +0200 Subject: Ensuring more invariants in Constr_matching. --- pretyping/constr_matching.ml | 70 +++++++++++++++++++++++++------------------- 1 file changed, 40 insertions(+), 30 deletions(-) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index f05812979d..161cffa865 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -351,25 +351,36 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next = else mkresult subst (mk_ctx (mkMeta special_meta)) next with PatternMatchingFailure -> next () +let subargs env v = Array.map_to_list (fun c -> (env, c)) v + (* Tries to match a subterm of [c] with [pat] *) let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let rec aux env c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in - let next () = try_aux [env] [c1] next_mk_ctx next in + let next_mk_ctx = function + | [c1] -> mk_ctx (mkCast (c1, k, c2)) + | _ -> assert false + in + let next () = try_aux [env, c1] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Lambda (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + let next_mk_ctx = function + | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2)) + | _ -> assert false + in let next () = let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1; c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Prod (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + let next_mk_ctx = function + | [c1; c2] -> mk_ctx (mkProd (x, c1, c2)) + | _ -> assert false + in let next () = let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | LetIn (x,c1,t,c2) -> let next_mk_ctx = function @@ -378,7 +389,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = in let next () = let env' = Environ.push_rel (x,Some c1,t) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in + try_aux [(env, c1); (env', c2)] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | App (c1,lc) -> let next () = @@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let mk_ctx = function | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in - try_aux [env] [app;Array.last lc] mk_ctx next + try_aux [(env, app); (env, Array.last lc)] mk_ctx next else let rec aux2 app args next = match args with | [] -> let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux [env] (c1::Array.to_list lc) mk_ctx next + let sub = (env, c1) :: subargs env lc in + try_aux sub mk_ctx next | arg :: args -> let app = mkApp (app,[|arg|]) in let next () = aux2 app args next in @@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = else let mk_ctx le = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - try_aux [env] (c1::Array.to_list lc) mk_ctx next + let sub = (env, c1) :: subargs env lc in + try_aux sub mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Case (ci,hd,c1,lc) -> @@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in + let sub = (env, c1) :: subargs env lc in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux - [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + let sub = subargs env types @ subargs env bodies in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | CoFix (i,(names,types,bodies)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + let sub = subargs env types @ subargs env bodies in + let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Proj (p,c') -> let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in @@ -443,25 +456,22 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = aux env term mk_ctx next with Retyping.RetypeError _ -> next () else - try_aux [env] [c'] next_mk_ctx next in + try_aux [env, c'] next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> authorized_occ env sigma partial_app closed pat c mk_ctx next (* Tries [sub_match] for all terms in the list *) - and try_aux lenv lc mk_ctx next = - let rec try_sub_match_rec lacc lenv lc = - match lenv, lc with - | _, [] -> next () - | env :: tlenv, c::tl -> - let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in - let next () = - let env' = match tlenv with [] -> lenv | _ -> tlenv in - try_sub_match_rec (c::lacc) env' tl - in - aux env c mk_ctx next - | _ -> assert false in - try_sub_match_rec [] lenv lc in + and try_aux lc mk_ctx next = + let rec try_sub_match_rec lacc lc = + match lc with + | [] -> next () + | (env, c) :: tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in + let next () = try_sub_match_rec (c :: lacc) tl in + aux env c mk_ctx next + in + try_sub_match_rec [] lc in let lempty () = IStream.Nil in let result () = aux env c (fun x -> x) lempty in IStream.thunk result -- cgit v1.2.3 From 596a4a5251cc50f50bd6d25e36c81341bf65cfed Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 30 Mar 2015 10:47:12 +0200 Subject: fix code and bound for SWITCH instruction. --- kernel/byterun/coq_fix_code.c | 4 ++-- kernel/byterun/coq_interp.c | 4 ++-- kernel/cbytegen.ml | 4 ++-- kernel/cemitcodes.ml | 45 ++++++++++++++++--------------------------- 4 files changed, 23 insertions(+), 34 deletions(-) diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index f1f9c92153..1be3e65113 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -150,8 +150,8 @@ value coq_tcode_of_code (value code, value size) { uint32_t i, sizes, const_size, block_size; COPY32(q,p); p++; sizes=*q++; - const_size = sizes & 0x7FFFFF; - block_size = sizes >> 23; + const_size = sizes & 0xFFFFFF; + block_size = sizes >> 24; sizes = const_size + block_size; for(i=0; i= String.length !out_buffer then begin - let len = String.length !out_buffer in - let new_buffer = String.create (2 * len) in - String.blit !out_buffer 0 new_buffer 0 len; - out_buffer := new_buffer - end; - String.unsafe_set !out_buffer p (Char.unsafe_chr b1); - String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); - String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); - String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); - out_position := p + 4 -*) - let out_word b1 b2 b3 b4 = let p = !out_position in if p >= String.length !out_buffer then begin @@ -66,13 +54,10 @@ let out_word b1 b2 b3 b4 = String.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; - String.unsafe_set !out_buffer p (Char.unsafe_chr b1); - String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2); - String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3); - String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4); + patch_char4 !out_buffer p (Char.unsafe_chr b1) + (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); out_position := p + 4 - let out opcode = out_word opcode 0 0 0 @@ -101,7 +86,7 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; + !out_buffer.[pos] <- Char.unsafe_chr displ; !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) @@ -222,8 +207,12 @@ let emit_instr = function out_label typlbl; out_label swlbl; slot_for_annot annot;out_int sz | Kswitch (tbl_const, tbl_block) -> + let lenb = Array.length tbl_block in + let lenc = Array.length tbl_const in + assert (lenb < 0x100 && lenc < 0x1000000); out opSWITCH; - out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); + out_word lenc (lenc asr 8) (lenc asr 16) (lenb); +(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block -- cgit v1.2.3 From c8c545713fa1e248a62fbd9905be56a5449b96a0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 10:41:32 +0200 Subject: coq_makefile: fix compilation with camlp4 --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 72735e900f..0931fd5506 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -463,7 +463,7 @@ let variables is_install opt (args,defs) = print "ifeq ($(CAMLP4),camlp5) CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma else -CAMLP4EXTEND= +CAMLP4EXTEND=threads.cma endif\n"; print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; -- cgit v1.2.3 From d58900ce20a6a7144db386a02093d3fc1c54c894 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:14:01 +0200 Subject: camlp4: grep away warnings in output/* tests --- test-suite/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/test-suite/Makefile b/test-suite/Makefile index 4a3a287c08..cffbe48196 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -273,6 +273,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ + | grep -v "^" \ > $$tmpoutput; \ diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ -- cgit v1.2.3 From b4f2e48b9e128a62d63668621844b571d3449cbf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:13:41 +0200 Subject: grammar: export hypident This is necessary to make ssr compile with both camlp4/5 --- interp/constrarg.ml | 3 +++ interp/constrarg.mli | 2 ++ parsing/g_tactic.ml4 | 2 +- parsing/pcoq.ml4 | 1 + parsing/pcoq.mli | 1 + 5 files changed, 8 insertions(+), 1 deletion(-) diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 3f232c3612..a7241399e0 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType let wit_bindings = unsafe_of_type BindingsArgType +let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = + Genarg.make0 None "hyp_location_flag" + let wit_red_expr = unsafe_of_type RedExprArgType let wit_clause_dft_concl = diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 74c6bd310c..fdeddd66a1 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -64,6 +64,8 @@ val wit_bindings : glob_constr_and_expr bindings, constr bindings Evd.sigma) genarg_type +val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type + val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b42b2c6dd3..69593f993c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -202,7 +202,7 @@ let merge_occurrences loc cl = function GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr - simple_intropattern clause_dft_concl; + simple_intropattern clause_dft_concl hypident; int_or_var: [ [ n = integer -> ArgArg n diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index cf6435fec4..6a9848c1ca 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -375,6 +375,7 @@ module Tactic = make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" let bindings = make_gen_entry utactic (rawwit wit_bindings) "bindings" + let hypident = Gram.entry_create "hypident" let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" let uconstr = make_gen_entry utactic (rawwit wit_uconstr) "uconstr" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index dbd2aadf9d..e23b65e12c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -215,6 +215,7 @@ module Tactic : val open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry + val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry -- cgit v1.2.3 From 41e4725805588b3fffdfdc0cd5ee6859de1612b5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:26:58 +0200 Subject: grammar: export constr_eval --- parsing/g_ltac.ml4 | 2 +- parsing/pcoq.ml4 | 1 + parsing/pcoq.mli | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 3cd7dbc9be..a4dba506d2 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -33,7 +33,7 @@ let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - constr_may_eval; + constr_may_eval constr_eval; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6a9848c1ca..54edbb2c88 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -377,6 +377,7 @@ module Tactic = make_gen_entry utactic (rawwit wit_bindings) "bindings" let hypident = Gram.entry_create "hypident" let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" let uconstr = make_gen_entry utactic (rawwit wit_uconstr) "uconstr" let quantified_hypothesis = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e23b65e12c..2146ad964f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -217,6 +217,7 @@ module Tactic : val bindings : constr_expr bindings Gram.entry val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry + val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val int_or_var : int or_var Gram.entry -- cgit v1.2.3