diff options
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | interp/coqlib.ml | 11 | ||||
| -rw-r--r-- | interp/coqlib.mli | 7 | ||||
| -rw-r--r-- | tactics/equality.ml | 39 | ||||
| -rw-r--r-- | theories/Bool/Bool.v | 14 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 17 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 793 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 27 | ||||
| -rw-r--r-- | toplevel/command.ml | 218 | ||||
| -rw-r--r-- | toplevel/ind_tables.ml | 100 | ||||
| -rw-r--r-- | toplevel/ind_tables.mli | 40 |
11 files changed, 1211 insertions, 57 deletions
diff --git a/Makefile.common b/Makefile.common index 08feab44b..ba911adb0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -147,6 +147,7 @@ TACTICS:=\ tactics/evar_tactics.cmo \ tactics/hiddentac.cmo tactics/elim.cmo \ tactics/dhyp.cmo tactics/auto.cmo \ + toplevel/ind_tables.cmo \ tactics/setoid_replace.cmo tactics/equality.cmo \ tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ tactics/tacinterp.cmo tactics/autorewrite.cmo \ @@ -155,6 +156,7 @@ TACTICS:=\ TOPLEVEL:=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ + toplevel/auto_ind_decl.cmo \ toplevel/command.cmo toplevel/record.cmo \ parsing/ppvernac.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 0cf9c934d..5fe0329f6 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -143,8 +143,19 @@ type coq_sigma_data = { intro : constr; typ : constr } +type coq_bool_data = { + andb : constr; + andb_prop : constr; + andb_true_intro : constr} + type 'a delayed = unit -> 'a +let build_bool_type () = + { andb = init_constant ["Datatypes"] "andb"; + andb_prop = init_constant ["Datatypes"] "andb_prop"; + andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } + + let build_sigma_set () = anomaly "Use build_sigma_type" let build_sigma_type () = diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 0a37eefbd..038cf94ff 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -73,6 +73,7 @@ val path_of_false : constructor val glob_true : global_reference val glob_false : global_reference + (* Equality *) val glob_eq : global_reference @@ -84,6 +85,12 @@ val glob_eq : global_reference type 'a delayed = unit -> 'a +type coq_bool_data = { + andb : constr; + andb_prop : constr; + andb_true_intro : constr} +val build_bool_type : coq_bool_data delayed + (*s For Equality tactics *) type coq_sigma_data = { proj1 : constr; diff --git a/tactics/equality.ml b/tactics/equality.ml index 066bf88d4..677039015 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -801,7 +801,7 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = let injfun = mkNamedLambda e t injbody in let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in let ty = simplify_args env sigma (get_type_of env sigma pf) in - (pf,ty)) + (pf,ty)) posns in if injectors = [] then errorlabstrm "Equality.inj" (str "Failed to decompose the equality"); @@ -809,6 +809,9 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) injectors +exception Not_dep_pair + + let injEq ipats (eq,(t,t1,t2)) id gls = let sigma = project gls in let env = pf_env gls in @@ -825,10 +828,44 @@ let injEq ipats (eq,(t,t1,t2)) id gls = let t1 = try_delta_expand env sigma t1 in let t2 = try_delta_expand env sigma t2 in *) + try ( +(* fetch the informations of the pair *) + let ceq = constr_of_global Coqlib.glob_eq in + let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in + let eqTypeDest = fst (destApp t) in + let _,ar1 = destApp t1 and + _,ar2 = destApp t2 in + let ind = destInd ar1.(0) in + let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" + ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in +(* check whether the equality deals with dep pairs or not *) +(* if yes, check if the user has declared the dec principle *) +(* and compare the fst arguments of the dep pair *) + let new_eq_args = [|type_of env sigma (ar1.(3));ar1.(3);ar2.(3)|] in + if ( (eqTypeDest = sigTconstr()) && + (Ind_tables.check_dec_proof ind=true) && + (is_conv env sigma (ar1.(2)) (ar2.(2)) = true)) + then ( +(* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*) + let qidl = qualid_of_reference + (Ident (dummy_loc,id_of_string "Eqdep_dec")) in + Library.require_library [qidl] (Some false); +(* cut with the good equality and prove the requested goal *) + tclTHENS (cut (mkApp (ceq,new_eq_args)) ) + [tclIDTAC; tclTHEN (apply ( + mkApp(inj2, + [|ar1.(0);Ind_tables.find_eq_dec_proof ind; + ar1.(1);ar1.(2);ar1.(3);ar2.(3)|]) + )) (Auto.trivial [] []) + ] gls +(* not a dep eq or no decidable type found *) + ) else (raise Not_dep_pair) + ) with _ -> ( tclTHEN (inject_at_positions env sigma (eq,(t,t1,t2)) id posns) (intros_pattern None ipats) gls + ) let inj ipats = onEquality (injEq ipats) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 8f739e0da..0d674ebf9 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -308,26 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62. (** * Properties of [andb] *) (*******************************) -Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true. -Proof. - destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. -Qed. -Hint Resolve andb_prop: bool v62. - Lemma andb_true_eq : forall a b:bool, true = a && b -> true = a /\ true = b. Proof. destruct a; destruct b; auto. Defined. -Lemma andb_true_intro : - forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. -Proof. - destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. -Qed. -Hint Resolve andb_true_intro: bool v62. - Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false. Proof. destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 912192b26..3525908ab 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -51,6 +51,23 @@ Definition negb (b:bool) := if b then false else true. Infix "||" := orb (at level 50, left associativity) : bool_scope. Infix "&&" := andb (at level 40, left associativity) : bool_scope. +(*******************************) +(** * Properties of [andb] *) +(*******************************) + +Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. +Proof. + destruct a; destruct b; intros; split; try (reflexivity || discriminate). +Qed. +Hint Resolve andb_prop: bool v62. + +Lemma andb_true_intro : + forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. +Proof. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. +Qed. +Hint Resolve andb_true_intro: bool v62. + (** Interpretation of booleans as propositions *) Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml new file mode 100644 index 000000000..b4b951f5f --- /dev/null +++ b/toplevel/auto_ind_decl.ml @@ -0,0 +1,793 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Tacmach +open Util +open Options +open Decl_kinds +open Pp +open Entries +open Termops +open Declarations +open Declare +open Term +open Names +open Libnames +open Goptions +open Mod_subst +open Indrec +open Inductiveops +open Tactics +open Tacticals +open Ind_tables + +(* boolean equality *) +(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k + variables *) +let context_chop k ctx = + let rec chop_aux acc = function + | (0, l2) -> (List.rev acc, l2) + | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) + | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) + | (_, []) -> failwith "context_chop" + in chop_aux [] (k,ctx) + +let quick_chop n l = + let rec kick_last = function + | t::[] -> [] + | t::q -> t::(kick_last q) + | [] -> failwith "kick_last" +and aux = function + | (0,l') -> l' + | (n,h::t) -> aux (n-1,t) + | _ -> failwith "quick_chop" + in + if n > (List.length l) then failwith "quick_chop args" + else kick_last (aux (n,l) ) + +let rec deconstruct_type t = + let l,r = decompose_prod t in + (List.map (fun (_,b) -> b) (List.rev l))@[r] + +let subst_in_constr (_,subst,(ind,const)) = + let ind' = (subst_kn subst (fst ind)),(snd ind) + and const' = subst_mps subst const in + ind',const' + +exception EqNotFound of string +exception EqUnknown of string + +(* Some pre declaration of constant we are going to use *) +let bb = constr_of_global Coqlib.glob_bool + +let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop + +let andb_true_intro = fun _ -> + (Coqlib.build_bool_type()).Coqlib.andb_true_intro + +let tt = constr_of_global Coqlib.glob_true + +let ff = constr_of_global Coqlib.glob_false + +let eq = constr_of_global Coqlib.glob_eq + +let sumbool = Coqlib.build_coq_sumbool + +let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb + +(* reconstruct the inductive with the correct deBruijn indexes *) +let mkFullInd ind n = + let mib = Global.lookup_mind (fst ind) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + (* params context divided *) + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + if nparrec > 0 + then mkApp (mkInd ind, + Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) + else mkInd ind + +let make_eq_scheme sp = + (* fetching global env *) + let env = Global.env() in + (* fetching the mutual inductive body *) + let mib = Global.lookup_mind sp in + (* number of inductives in the mutual *) + let nb_ind = Array.length mib.mind_packets in + (* number of params in the type *) + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + (* params context divided *) + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + (* predef coq's boolean type *) + (* rec name *) + let rec_name i =(string_of_id (Array.get mib.mind_packets i).mind_typename)^ + "_eqrec" + in + (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *) + let create_input c = + let myArrow u v = mkArrow u (lift 1 v) + and eqName = function + | Name s -> id_of_string ("eq_"^(string_of_id s)) + | Anonymous -> id_of_string "eq_A" + in + let ext_rel_list = extended_rel_list 0 lnamesparrec in + let lift_cnt = ref 0 in + let eqs_typ = List.map (fun aa -> + let a = lift !lift_cnt aa in + incr lift_cnt; + myArrow a (myArrow a bb) + ) ext_rel_list in + + let eq_input = List.fold_left2 + ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *) + (* here I leave the Naming thingy so that the type of + the function is more readable for the user *) + mkNamedLambda (eqName n) b a ) + c (List.rev eqs_typ) lnamesparrec + in + List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *) + (* Same here , hoping the auto renaming will do something good ;) *) + mkNamedLambda + (match n with Name s -> s | Anonymous -> id_of_string "A") + t a) eq_input lnamesparrec + in + let make_one_eq cur = + let ind = sp,cur in + (* current inductive we are working on *) + let cur_packet = mib.mind_packets.(snd ind) in + (* Inductive toto : [rettyp] := *) + let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in + (* split rettyp in a list without the non rec params and the last -> + e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) + let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in + (* give a type A, this function tries to find the equality on A declared + previously *) + (* nlist = the number of args (A , B , ... ) + eqA = the deBruijn index of the first eq param + ndx = how much to translate due to the 2nd Case + *) + let compute_A_equality rel_list nlist eqA ndx t = + let lifti = ndx in + let rec aux c a = match c with + | Rel x -> mkRel (x-nlist+ndx) + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))) + | Cast (x,_,_) -> aux (kind_of_term x) a + | App (x,newa) -> aux (kind_of_term x) newa + | Ind (sp',i) -> if sp=sp' then mkRel(eqA-nlist-i+nb_ind-1) + else ( try + let eq = find_eq_scheme (sp',i) + and eqa = Array.map + (fun x -> aux (kind_of_term x) [||] ) a + in + let args = Array.append + (Array.map (fun x->lift lifti x) a) eqa + in if args = [||] then eq + else mkApp (eq,Array.append + (Array.map (fun x->lift lifti x) a) eqa) + with Not_found -> raise(EqNotFound (string_of_kn sp')) + ) + | Sort _ -> raise (EqUnknown "Sort" ) + | Prod _ -> raise (EqUnknown "Prod" ) + | Lambda _-> raise (EqUnknown "Lambda") + | LetIn _ -> raise (EqUnknown "LetIn") + | Const kn -> let mp,dir,lbl= repr_con kn in + mkConst (make_con mp dir ( + mk_label ("eq_"^(string_of_label lbl)))) + | Construct _ -> raise (EqUnknown "Construct") + | Case _ -> raise (EqUnknown "Case") + | CoFix _ -> raise (EqUnknown "CoFix") + | Fix _ -> raise (EqUnknown "Fix") + | Meta _ -> raise (EqUnknown "Meta") + | Evar _ -> raise (EqUnknown "Evar") + in + aux t [||] + in + (* construct the predicate for the Case part*) + let do_predicate rel_list n = + List.fold_left (fun a b -> mkLambda(Anonymous,b,a)) + (mkLambda (Anonymous, + mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), + bb)) + (List.rev rettyp_l) in + (* make_one_eq *) + (* do the [| C1 ... => match Y with ... end + ... + Cn => match Y with ... end |] part *) + let ci = make_case_info env ind MatchStyle in + let constrs n = get_constructors env (make_ind_family (ind, + extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in + let constrsi = constrs (3+nparrec) in + let n = Array.length constrsi in + let ar = Array.create n ff in + for i=0 to n-1 do + let nb_cstr_args = List.length constrsi.(i).cs_args in + let ar2 = Array.create n ff in + let constrsj = constrs (3+nparrec+nb_cstr_args) in + for j=0 to n-1 do + if (i=j) then + ar2.(j) <- let cc = (match nb_cstr_args with + | 0 -> tt + | _ -> let eqs = Array.make nb_cstr_args tt in + for ndx = 0 to nb_cstr_args-1 do + let _,_,cc = List.nth constrsi.(i).cs_args ndx in + let eqA = compute_A_equality rel_list + nparrec + (nparrec+3+2*nb_cstr_args) + (nb_cstr_args+ndx+1) + (kind_of_term cc) + in + Array.set eqs ndx + (mkApp (eqA, + [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] + )) + done; + Array.fold_left + (fun a b -> mkApp (andb(),[|b;a|])) + (eqs.(0)) + (Array.sub eqs 1 (nb_cstr_args - 1)) + ) + in + (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc + (constrsj.(j).cs_args) + ) + else ar2.(j) <- (List.fold_left (fun a (p,q,r) -> + mkLambda (p,r,a)) ff (constrsj.(j).cs_args) ) + done; + + ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) + (mkCase (ci,do_predicate rel_list nb_cstr_args, + mkVar (id_of_string "Y") ,ar2)) + (constrsi.(i).cs_args)) + done; + mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1)) ( + mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2)) ( + mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar))) + in (* make_eq_scheme *) + try + let names = Array.make nb_ind Anonymous and + types = Array.make nb_ind mkSet and + cores = Array.make nb_ind mkSet and + res = Array.make nb_ind mkSet in + for i=0 to (nb_ind-1) do + names.(i) <- Name (id_of_string (rec_name i)); + types.(i) <- mkArrow (mkFullInd (sp,i) 0) + (mkArrow (mkFullInd (sp,i) 1) bb); + cores.(i) <- make_one_eq i + done; + if (string_of_mp (modpath sp ))="Coq.Init.Logic" + then print_string "Logic time, do nothing.\n" + else ( + for i=0 to (nb_ind-1) do + let cpack = Array.get mib.mind_packets i in + if check_eq_scheme (sp,i) + then message ("Boolean equality is already defined on "^ + (string_of_id cpack.mind_typename)^".") + else ( + let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in + res.(i) <- create_input fix + ) + done; + ); + res + with + | EqUnknown s -> error ("Type unexpected ("^s^ + ") during boolean eq computation, please report.") + | EqNotFound s -> error ("Boolean equality on "^s^ + " is missing, equality will not be defined.") + | _ -> error ("Unknown exception during boolean equality creation,"^ + " the equality will not be defined.") + +(* This function tryies to get the [inductive] between a constr + the constr should be Ind i or App(Ind i,[|args|]) +*) +let destruct_ind c = + try let u,v = destApp c in + let indc = destInd u in + indc,v + with _-> let indc = destInd c in + indc,[||] + +(* + In the followind, avoid is the list of names to avoid. + If the args of the Inductive type are A1 ... An + then avoid should be + [| lb_An ... lb _A1 (resp. bl_An ... bl_A1) + eq_An .... eq_A1 An ... A1 |] +so from Ai we can find the the correct eq_Ai bl_ai or lb_ai +*) +(* used in the leib -> bool side*) +let do_replace_lb aavoid narg gls p q = + let avoid = Array.of_list aavoid in + let do_arg v offset = + try + let x = narg*offset in + let s = destVar v in + let n = Array.length avoid in + let rec find i = + if avoid.(n-i) = s then avoid.(n-i-x) + else (if i<n then find (i+1) + else error ("Var "^(string_of_id s)^" seems unknown.") + ) + in mkVar (find 1) + with _ -> (* if this happen then the args have to be already declared as a + Parameter*) + ( + let mp,dir,lbl = repr_con (destConst v) in + mkConst (make_con mp dir (mk_label ( + if offset=1 then ("eq_"^(string_of_label lbl)) + else ((string_of_label lbl)^"_lb") + ))) + ) + in + let type_of_pq = pf_type_of gls p in + let u,v = destruct_ind type_of_pq + in let lb_type_of_p = + try find_lb_proof u + with Not_found -> error + ("Leibniz->boolean:You have to declare the decidability over "^ + (string_of_constr type_of_pq)^" first.") + in let lb_args = Array.append (Array.append + (Array.map (fun x -> x) v) + (Array.map (fun x -> do_arg x 1) v)) + (Array.map (fun x -> do_arg x 2) v) + in let app = if lb_args = [||] + then lb_type_of_p else mkApp (lb_type_of_p,lb_args) + in [Equality.replace p q ; apply app ; Auto.default_auto] + + +(* used in the bool -> leib side *) +let do_replace_bl ind gls aavoid narg lft rgt = + let avoid = Array.of_list aavoid in + let do_arg v offset = + try + let x = narg*offset in + let s = destVar v in + let n = Array.length avoid in + let rec find i = + if avoid.(n-i) = s then avoid.(n-i-x) + else (if i<n then find (i+1) + else error ("Var "^(string_of_id s)^" seems unknown.") + ) + in mkVar (find 1) + with _ -> (* if this happen then the args have to be already declared as a + Parameter*) + ( + let mp,dir,lbl = repr_con (destConst v) in + mkConst (make_con mp dir (mk_label ( + if offset=1 then ("eq_"^(string_of_label lbl)) + else ((string_of_label lbl)^"_bl") + ))) + ) + in + + let rec aux l1 l2 = + match (l1,l2) with + | (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in + if t1=t2 then aux q1 q2 + else ( + let u,v = try destruct_ind tt1 + (* trick so that the good sequence is returned*) + with _ -> ind,[||] + in if u = ind + then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2) + else ( + let bl_t1 = + try find_bl_proof u + with Not_found -> error + ("boolean->Leibniz:You have to declare the decidability over "^ + (string_of_constr tt1)^" first.") + in let bl_args = + Array.append (Array.append + (Array.map (fun x -> x) v) + (Array.map (fun x -> do_arg x 1) v)) + (Array.map (fun x -> do_arg x 2) v ) + in + let app = if bl_args = [||] + then bl_t1 else mkApp (bl_t1,bl_args) + in + (Equality.replace_by t1 t2 + (tclTHEN (apply app) (Auto.default_auto)))::(aux q1 q2) + ) + ) + | ([],[]) -> [] + | _ -> error "Both side of the equality must have the same arity." + in + let (ind1,ca1) = try destApp lft with + _ -> error "replace failed." + and (ind2,ca2) = try destApp rgt with + _ -> error "replace failed." + in + let (sp1,i1) = try destInd ind1 with + _ -> (try fst (destConstruct ind1) with _ -> + error "The expected type is an inductive one.") + and (sp2,i2) = try destInd ind2 with + _ -> (try fst (destConstruct ind2) with _ -> + error "The expected type is an inductive one.") + in + if (sp1 <> sp2) || (i1 <> i2) + then (error "Eq should be on the same type") + else (aux (Array.to_list ca1) (Array.to_list ca2)) + +(* + create, from a list of ids [i1,i2,...,in] the list + [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] +*) +let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = + match n with + Name s -> string_of_id s + | Anonymous -> "A" in + (id_of_string s',id_of_string ("eq_"^s'), + id_of_string (s'^"_bl"), + id_of_string (s'^"_lb")) + ::a + ) [] l +(* + build the right eq_I A B.. N eq_A .. eq_N +*) +let eqI ind l = + let list_id = list_id l in + let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ + (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) + and e = try find_eq_scheme ind with + Not_found -> error + ("The boolean equality on "^(string_of_kn (fst ind))^" is needed."); + in (if eA = [||] then e else mkApp(e,eA)) + +let compute_bl_goal ind lnamesparrec nparrec = + let eqI = eqI ind lnamesparrec in + let list_id = list_id lnamesparrec in + let create_input c = + let x = id_of_string "x" and + y = id_of_string "y" in + let bl_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + )) + ) list_id in + let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> + mkNamedProd sbl b a + ) c (List.rev list_id) (List.rev bl_typ) in + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) bl_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a (n,_,t) -> mkNamedProd + (match n with Name s -> s | Anonymous -> id_of_string "A") + t a) eq_input lnamesparrec + in + let n = id_of_string "n" and + m = id_of_string "m" in + create_input ( + mkNamedProd n (mkFullInd ind nparrec) ( + mkNamedProd m (mkFullInd ind (nparrec+1)) ( + mkArrow + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) + (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|])) + ))) + +let compute_bl_tact ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let avoid = ref [] in + let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ + ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) + in + let fresh_first_intros = List.map ( fun s -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh ) first_intros in + let freshn = fresh_id (!avoid) (id_of_string "n") gsig in + let freshm = avoid := freshn::(!avoid); + fresh_id (!avoid) (id_of_string "m") gsig in + let freshz = avoid := freshm::(!avoid); + fresh_id (!avoid) (id_of_string "Z") gsig in + (* try with *) + avoid := freshz::(!avoid); + Pfedit.by ( + tclTHENSEQ [ intros_using fresh_first_intros; + intro_using freshn ; + new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn), + Rawterm.NoBindings))] + None + Genarg.IntroAnonymous; + intro_using freshm; + new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm), + Rawterm.NoBindings))] + None + Genarg.IntroAnonymous; + intro_using freshz; + intros; + tclTRY ( + tclORELSE reflexivity (Equality.discr_tac None) + ); + simpl_in_hyp (([],freshz),Tacexpr.InHyp); +(* +repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). +*) + tclREPEAT ( + tclTHENSEQ [ + apply_in false freshz [(andb_prop()),Rawterm.NoBindings]; + fun gl -> + let fresht = fresh_id (!avoid) (id_of_string "Z") gsig + in + avoid := fresht::(!avoid); + (new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshz,Rawterm.NoBindings))] + None + ( Genarg.IntroOrAndPattern [[ + Genarg.IntroIdentifier fresht; + Genarg.IntroIdentifier freshz]])) gl + ]); +(* + Ci a1 ... an = Ci b1 ... bn + replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto +*) + fun gls-> let gl = (gls.Evd.it).Evd.evar_concl in + match (kind_of_term gl) with + | App (c,ca) -> ( + match (kind_of_term c) with + | Ind (i1,i2) -> + if(string_of_label (label i1) = "eq") + then ( + tclTHENSEQ (do_replace_bl ind gls (!avoid) + nparrec (ca.(2)) + (ca.(1))) gls + ) + else + (error "Failure while solving Boolean->Leibniz.") + | _ -> error "Failure while solving Boolean->Leibniz." + ) + | _ -> error "Failure while solving Boolean->Leibniz." + + ] + ) + +let compute_lb_goal ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let eqI = eqI ind lnamesparrec in + let create_input c = + let x = id_of_string "x" and + y = id_of_string "y" in + let lb_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + )) + ) list_id in + let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> + mkNamedProd slb b a + ) c (List.rev list_id) (List.rev lb_typ) in + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) lb_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a (n,_,t) -> mkNamedProd + (match n with Name s -> s | Anonymous -> id_of_string "A") + t a) eq_input lnamesparrec + in + let n = id_of_string "n" and + m = id_of_string "m" in + create_input ( + mkNamedProd n (mkFullInd ind nparrec) ( + mkNamedProd m (mkFullInd ind (nparrec+1)) ( + mkArrow + (mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|])) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) + ))) + +let compute_lb_tact ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let avoid = ref [] in + let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + let fresh_first_intros = List.map ( fun s -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh ) first_intros in + let freshn = fresh_id (!avoid) (id_of_string "n") gsig in + let freshm = avoid := freshn::(!avoid); + fresh_id (!avoid) (id_of_string "m") gsig in + let freshz = avoid := freshm::(!avoid); + fresh_id (!avoid) (id_of_string "Z") gsig in + (* try with *) + avoid := freshz::(!avoid); + Pfedit.by ( + tclTHENSEQ [ intros_using fresh_first_intros; + intro_using freshn ; + new_induct false [Tacexpr.ElimOnConstr + ((mkVar freshn),Rawterm.NoBindings)] + None + Genarg.IntroAnonymous; + intro_using freshm; + new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshm),Rawterm.NoBindings)] + None + Genarg.IntroAnonymous; + intro_using freshz; + intros; + tclTRY ( + tclORELSE reflexivity (Equality.discr_tac None) + ); + Equality.inj [] freshz; intros; simpl_in_concl; + Auto.default_auto; + tclREPEAT ( + tclTHENSEQ [apply (andb_true_intro()); + simplest_split ;Auto.default_auto ] + ); + fun gls -> let gl = (gls.Evd.it).Evd.evar_concl in + (* assume the goal to be eq (eq_type ...) = true *) + match (kind_of_term gl) with + | App(c,ca) -> (match (kind_of_term ca.(1)) with + | App(c',ca') -> + let n = Array.length ca' in + tclTHENSEQ (do_replace_lb (!avoid) + nparrec gls + ca'.(n-2) ca'.(n-1)) gls + | _ -> error + "Failure while solving Leibniz->Boolean." + ) + | _ -> error + "Failure while solving Leibniz->Boolean." + ] + ) + +(* {n=m}+{n<>m} part *) +let compute_dec_goal ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let create_input c = + let x = id_of_string "x" and + y = id_of_string "y" in + let lb_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + )) + ) list_id in + let bl_typ = List.map (fun (s,seq,_,_) -> + mkNamedProd x (mkVar s) ( + mkNamedProd y (mkVar s) ( + mkArrow + ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) + ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) + )) + ) list_id in + + let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> + mkNamedProd slb b a + ) c (List.rev list_id) (List.rev lb_typ) in + let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> + mkNamedProd sbl b a + ) lb_input (List.rev list_id) (List.rev bl_typ) in + + let eqs_typ = List.map (fun (s,_,_,_) -> + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) + ) list_id in + let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> + mkNamedProd seq b a + ) bl_input (List.rev list_id) (List.rev eqs_typ) in + List.fold_left (fun a (n,_,t) -> mkNamedProd + (match n with Name s -> s | Anonymous -> id_of_string "A") + t a) eq_input lnamesparrec + in + let n = id_of_string "n" and + m = id_of_string "m" in + let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in + create_input ( + mkNamedProd n (mkFullInd ind (2*nparrec)) ( + mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( + mkApp(sumbool(),[|eqnm;mkApp (Coqlib.build_coq_not(),[|eqnm|])|]) + ) + ) + ) + +let compute_dec_tact ind lnamesparrec nparrec = + let list_id = list_id lnamesparrec in + let eqI = eqI ind lnamesparrec in + let avoid = ref [] in + let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in + let eqtrue x = mkApp(eq,[|bb;x;tt|]) in + let eqfalse x = mkApp(eq,[|bb;x;ff|]) in + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) @ + ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ + ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + let fresh_first_intros = List.map ( fun s -> + let fresh = fresh_id (!avoid) s gsig in + avoid := fresh::(!avoid); fresh ) first_intros in + let freshn = fresh_id (!avoid) (id_of_string "n") gsig in + let freshm = avoid := freshn::(!avoid); + fresh_id (!avoid) (id_of_string "m") gsig in + let freshH = avoid := freshm::(!avoid); + fresh_id (!avoid) (id_of_string "H") gsig in + let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in + avoid := freshH::(!avoid); + Pfedit.by ( tclTHENSEQ [ + intros_using fresh_first_intros; + intros_using [freshn;freshm]; + assert_as true (Genarg.IntroIdentifier freshH) ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + ) ]); +(*we do this so we don't have to prove the same goal twice *) + Pfedit.by ( tclTHEN + (new_destruct false [Tacexpr.ElimOnConstr + (eqbnm,Rawterm.NoBindings)] + None + Genarg.IntroAnonymous) + Auto.default_auto + ); + Pfedit.by ( + let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in + avoid := freshH2::(!avoid); + new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshH),Rawterm.NoBindings)] + None + (Genarg.IntroOrAndPattern [ + [Genarg.IntroAnonymous]; + [Genarg.IntroIdentifier freshH2]]) + ); + let arfresh = Array.of_list fresh_first_intros in + let xargs = Array.sub arfresh 0 (2*nparrec) in + let blI = try find_bl_proof ind with + Not_found -> error ( + "Error during the decidability part, boolean to leibniz"^ + " equality is required.") + in + let lbI = try find_lb_proof ind with + Not_found -> error ( + "Error during the decidability part, leibniz to boolean"^ + " equality is required.") + in + + (* left *) + Pfedit.by ( tclTHENSEQ [ simplest_left; + apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)); + Auto.default_auto + ]); + (*right *) + let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in + avoid := freshH3::(!avoid); + Pfedit.by (tclTHENSEQ [ simplest_right ; + unfold_constr (Lazy.force Coqlib.coq_not_ref); + intro; + Equality.subst_all; + assert_as true (Genarg.IntroIdentifier freshH3) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) + ]); + Pfedit.by + (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)); + Auto.default_auto + ]); + Pfedit.by (Equality.general_rewrite_bindings_in true + (List.hd !avoid) + ((mkVar (List.hd (List.tl !avoid))), + Rawterm.NoBindings + ) + true); + Pfedit.by (Equality.discr_tac None) + + diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli new file mode 100644 index 000000000..b8fa1710e --- /dev/null +++ b/toplevel/auto_ind_decl.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Names +open Libnames +open Mod_subst +open Sign + + +val subst_in_constr : (object_name*substitution*(inductive*constr)) + -> (inductive*constr) + +val compute_bl_goal : inductive -> rel_context -> int -> types +val compute_bl_tact : inductive -> rel_context -> int -> unit +val compute_lb_goal : inductive -> rel_context -> int -> types +val compute_lb_tact : inductive -> rel_context -> int -> unit +val compute_dec_goal : inductive -> rel_context -> int -> types +val compute_dec_tact : inductive -> rel_context -> int -> unit + + +val make_eq_scheme :mutual_inductive -> types array diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b8c537b4..0b9f76d95 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -42,6 +42,8 @@ open Pretyping open Evarutil open Evarconv open Notation +open Goptions +open Mod_subst open Evd let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) @@ -195,6 +197,8 @@ let declare_assumption idl is_coe k bl c nl= (* 3a| Elimination schemes for mutual inductive definitions *) open Indrec +open Inductiveops + let non_type_eliminations = [ (InProp,elimination_suffix InProp); @@ -250,12 +254,174 @@ let declare_one_elimination ind = let _ = declare (mindstr^suff) elim None in ()) non_type_eliminations +(* bool eq declaration flag && eq dec declaration flag *) +let eq_flag = ref false +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of boolean equality"; + optkey = (SecondaryTable ("Equality","Scheme")); + optread = (fun () -> !eq_flag) ; + optwrite = (fun b -> eq_flag := b) } + +(* boolean equality *) +let (inScheme,outScheme) = + declare_object {(default_object "EQSCHEME") with + cache_function = Ind_tables.cache_scheme; + load_function = (fun _ -> Ind_tables.cache_scheme); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_scheme } + +let declare_eq_scheme sp = + let mib = Global.lookup_mind sp in + let nb_ind = Array.length mib.mind_packets in + let eq_array = Auto_ind_decl.make_eq_scheme sp in + for i=0 to (nb_ind-1) do + let cpack = Array.get mib.mind_packets i in + let nam = id_of_string ((string_of_id cpack.mind_typename)^"_beq") + in + let cst_entry = {const_entry_body = eq_array.(i); + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() } + in + let cst_decl = (DefinitionEntry cst_entry),(IsDefinition Definition) + in + let cst = Declare.declare_constant nam cst_decl in + Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst)); + definition_message nam + done +(* decidability of eq *) + +(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k + variables *) +let context_chop k ctx = + let rec chop_aux acc = function + | (0, l2) -> (List.rev acc, l2) + | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) + | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) + | (_, []) -> failwith "context_chop" + in chop_aux [] (k,ctx) + + +let (inBoolLeib,outBoolLeib) = + declare_object {(default_object "BOOLLIEB") with + cache_function = Ind_tables.cache_bl; + load_function = (fun _ -> Ind_tables.cache_bl); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_bool_leib } + +let (inLeibBool,outLeibBool) = + declare_object {(default_object "LIEBBOOL") with + cache_function = Ind_tables.cache_lb; + load_function = (fun _ -> Ind_tables.cache_lb); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_leib_bool } + +let (inDec,outDec) = + declare_object {(default_object "EQDEC") with + cache_function = Ind_tables.cache_dec; + load_function = (fun _ -> Ind_tables.cache_dec); + subst_function = Auto_ind_decl.subst_in_constr; + export_function = Ind_tables.export_dec_proof } + +let start_proof id kind c hook = + let sign = Global.named_context () in + let sign = clear_proofs sign in + Pfedit.start_proof id kind sign c hook + +let save id const (locality,kind) hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let l,r = match locality with + | Local when Lib.sections_are_opened () -> + let k = logical_kind_of_goal_kind kind in + let c = SectionLocalDef (pft, tpo, opacity) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local, VarRef id) + | Local -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) + | Global -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) in + Pfedit.delete_current_proof (); + definition_message id; + hook l r + +let save_named opacity = + let id,(const,persistence,hook) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in + save id const persistence hook + +let make_eq_decidability ind = + (* fetching data *) + let mib = Global.lookup_mind (fst ind) in + let nparams = mib.mind_nparams in + let nparrec = mib.mind_nparams_rec in + let lnonparrec,lnamesparrec = + context_chop (nparams-nparrec) mib.mind_params_ctxt in + let proof_name = (string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_eq_dec" in + let bl_name =(string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_bl" in + let lb_name =(string_of_id( + Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_lb" in + (* main calls*) + if Ind_tables.check_bl_proof ind + then (message (bl_name^" is already declared.")) + else ( + start_proof (id_of_string bl_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec) + (fun _ _ -> ()); + Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inBoolLeib (ind,mkConst (Lib.make_con (id_of_string bl_name)))) +(* definition_message (id_of_string bl_name) *) + ); + if Ind_tables.check_lb_proof ind + then (message (lb_name^" is already declared.")) + else ( + start_proof (id_of_string lb_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_lb_goal ind lnamesparrec nparrec) + ( fun _ _ -> ()); + Auto_ind_decl.compute_lb_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inLeibBool (ind,mkConst (Lib.make_con (id_of_string lb_name)))) +(* definition_message (id_of_string lb_name) *) + ); + if Ind_tables.check_dec_proof ind + then (message (proof_name^" is already declared.")) + else ( + start_proof (id_of_string proof_name) + (Global,Proof Theorem) + (Auto_ind_decl.compute_dec_goal ind lnamesparrec nparrec) + ( fun _ _ -> ()); + Auto_ind_decl.compute_dec_tact ind lnamesparrec nparrec; + save_named true; + Lib.add_anonymous_leaf + (inDec (ind,mkConst (Lib.make_con (id_of_string proof_name)))) +(* definition_message (id_of_string proof_name) *) + ) + +(* end of automated definition on ind*) + let declare_eliminations sp = let mib = Global.lookup_mind sp in - if mib.mind_finite then + if mib.mind_finite then begin + if (!eq_flag) then (declare_eq_scheme sp); for i = 0 to Array.length mib.mind_packets - 1 do - declare_one_elimination (sp,i) - done + declare_one_elimination (sp,i); + if (!eq_flag) then (make_eq_decidability (sp,i)); + done; + end (* 3b| Mutual inductive definitions *) @@ -419,7 +585,6 @@ let prepare_inductive ntnl indl = }) indl in List.fold_right option_cons ntnl [], indl -open Goptions let elim_flag = ref true let _ = @@ -755,12 +920,12 @@ tried to declare different schemes at once *) error "Do not declare equality and induction scheme at the same time." else ( if ischeme <> [] then build_induction_scheme ischeme; - List.iter ( fun indname -> + List.iter ( fun indname -> let ind = Nametab.global_inductive indname -(* vsiles :This will be replace with the boolean eq when it will be commited *) - in Pp.msgnl (print_constr (mkInd ind)) - ) escheme - ) + in declare_eq_scheme (fst ind); + make_eq_decidability ind + ) escheme + ) let rec get_concl n t = if n = 0 then t @@ -815,12 +980,6 @@ let build_combined_scheme name schemes = if_verbose ppnl (recursive_message Fixpoint None [snd name]) (* 4| Goal declaration *) - -let start_proof id kind c hook = - let sign = Global.named_context () in - let sign = clear_proofs sign in - Pfedit.start_proof id kind sign c hook - let start_proof_com sopt kind (bl,t) hook = let id = match sopt with | Some id -> @@ -837,33 +996,6 @@ let start_proof_com sopt kind (bl,t) hook = let _ = Typeops.infer_type env c in start_proof id kind c hook -let save id const (locality,kind) hook = - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let l,r = match locality with - | Local when Lib.sections_are_opened () -> - let k = logical_kind_of_goal_kind kind in - let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in - Pfedit.delete_current_proof (); - definition_message id; - hook l r - -let save_named opacity = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - save id const persistence hook - let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then error "This command can only be used for unnamed theorem" @@ -900,3 +1032,5 @@ let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) + + diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml new file mode 100644 index 000000000..fe3bddf37 --- /dev/null +++ b/toplevel/ind_tables.ml @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Mod_subst + +let eq_scheme_map = ref Indmap.empty + +let cache_scheme (_,(ind,const)) = + eq_scheme_map := Indmap.add ind const (!eq_scheme_map) + +let export_scheme obj = + Some obj + + + +let _ = Summary.declare_summary "eqscheme" + { Summary.freeze_function = (fun () -> !eq_scheme_map); + Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs); + Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty); + Summary.survive_module = false; + Summary.survive_section = true} + +let find_eq_scheme ind = + Indmap.find ind !eq_scheme_map + +let check_eq_scheme ind = + Indmap.mem ind !eq_scheme_map + +let bl_map = ref Indmap.empty +let lb_map = ref Indmap.empty +let dec_map = ref Indmap.empty + + +let cache_bl (_,(ind,const)) = + bl_map := Indmap.add ind const (!bl_map) + +let cache_lb (_,(ind,const)) = + lb_map := Indmap.add ind const (!lb_map) + +let cache_dec (_,(ind,const)) = + dec_map := Indmap.add ind const (!dec_map) + +let export_bool_leib obj = + Some obj + +let export_leib_bool obj = + Some obj + +let export_dec_proof obj = + Some obj + + + +let _ = Summary.declare_summary "bl_proof" + { Summary.freeze_function = (fun () -> !bl_map); + Summary.unfreeze_function = (fun fs -> bl_map := fs); + Summary.init_function = (fun () -> bl_map := Indmap.empty); + Summary.survive_module = false; + Summary.survive_section = true} + +let find_bl_proof ind = + Indmap.find ind !bl_map + +let check_bl_proof ind = + Indmap.mem ind !bl_map + +let _ = Summary.declare_summary "lb_proof" + { Summary.freeze_function = (fun () -> !lb_map); + Summary.unfreeze_function = (fun fs -> lb_map := fs); + Summary.init_function = (fun () -> lb_map := Indmap.empty); + Summary.survive_module = false; + Summary.survive_section = true} + +let find_lb_proof ind = + Indmap.find ind !lb_map + +let check_lb_proof ind = + Indmap.mem ind !lb_map + +let _ = Summary.declare_summary "eq_dec_proof" + { Summary.freeze_function = (fun () -> !dec_map); + Summary.unfreeze_function = (fun fs -> dec_map := fs); + Summary.init_function = (fun () -> dec_map := Indmap.empty); + Summary.survive_module = false; + Summary.survive_section = true} + +let find_eq_dec_proof ind = + Indmap.find ind !dec_map + +let check_dec_proof ind = + Indmap.mem ind !dec_map + + + diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli new file mode 100644 index 000000000..2edb294f9 --- /dev/null +++ b/toplevel/ind_tables.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Names +open Libnames +open Mod_subst +open Sign + + +val cache_scheme :(object_name*(Indmap.key*constr)) -> unit +val export_scheme : (Indmap.key*constr) -> (Indmap.key*constr) option + +val find_eq_scheme : Indmap.key -> constr +val check_eq_scheme : Indmap.key -> bool + +val cache_bl: (object_name*(Indmap.key*constr)) -> unit +val cache_lb: (object_name*(Indmap.key*constr)) -> unit +val cache_dec : (object_name*(Indmap.key*constr)) -> unit + +val export_bool_leib : (Indmap.key*constr) -> (Indmap.key*constr) option +val export_leib_bool : (Indmap.key*constr) -> (Indmap.key*constr) option +val export_dec_proof : (Indmap.key*constr) -> (Indmap.key*constr) option + +val find_bl_proof : Indmap.key -> constr +val find_lb_proof : Indmap.key -> constr +val find_eq_dec_proof : Indmap.key -> constr + +val check_bl_proof: Indmap.key -> bool +val check_lb_proof: Indmap.key -> bool +val check_dec_proof: Indmap.key -> bool + + + + |