From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- toplevel/auto_ind_decl.ml | 812 ++++++++++++++++++++++++++++++++++++++++ toplevel/auto_ind_decl.mli | 27 ++ toplevel/cerrors.ml | 29 +- toplevel/class.ml | 52 +-- toplevel/class.mli | 12 +- toplevel/classes.ml | 737 ++++++++++++++++++++++++++++++++++++ toplevel/classes.mli | 103 +++++ toplevel/command.ml | 884 ++++++++++++++++++++++++++++++++----------- toplevel/command.mli | 79 +++- toplevel/coqinit.ml | 78 ++-- toplevel/coqtop.ml | 65 ++-- toplevel/discharge.ml | 4 +- toplevel/himsg.ml | 907 ++++++++++++++++++++++++--------------------- toplevel/himsg.mli | 5 +- toplevel/ind_tables.ml | 102 +++++ toplevel/ind_tables.mli | 40 ++ toplevel/metasyntax.ml | 28 +- toplevel/metasyntax.mli | 4 +- toplevel/minicoq.ml | 4 +- toplevel/mltop.ml4 | 13 +- toplevel/record.ml | 55 +-- toplevel/record.mli | 12 +- toplevel/toplevel.ml | 18 +- toplevel/vernac.ml | 29 +- toplevel/vernacentries.ml | 419 ++++++++++++++------- toplevel/vernacentries.mli | 9 +- toplevel/vernacexpr.ml | 65 +++- toplevel/vernacinterp.ml | 4 +- toplevel/whelp.ml4 | 22 +- 29 files changed, 3632 insertions(+), 986 deletions(-) create mode 100644 toplevel/auto_ind_decl.ml create mode 100644 toplevel/auto_ind_decl.mli create mode 100644 toplevel/classes.ml create mode 100644 toplevel/classes.mli create mode 100644 toplevel/ind_tables.ml create mode 100644 toplevel/ind_tables.mli (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml new file mode 100644 index 00000000..094a77ff --- /dev/null +++ b/toplevel/auto_ind_decl.ml @@ -0,0 +1,812 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [] + | 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 (* 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 -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = msg_with Format.str_formatter + (str "Leibniz->boolean:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr type_of_pq ++ + str " first."); + Format.flush_str_formatter () + in + error err_msg + 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 (* 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 -> + (* spiwack: the format of this error message should probably + be improved. *) + let err_msg = msg_with Format.str_formatter + (str "boolean->Leibniz:" ++ + str "You have to declare the" ++ + str "decidability over " ++ + Printer.pr_constr tt1 ++ + str " first."); + Format.flush_str_formatter () + in + error err_msg + 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 + None; + intro_using freshm; + new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm), + Rawterm.NoBindings))] + None + Genarg.IntroAnonymous + None; + intro_using freshz; + intros; + tclTRY ( + tclORELSE reflexivity (Equality.discr_tac false None) + ); + simpl_in_hyp + ((Rawterm.all_occurrences_expr,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]]) None) 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)))@[Auto.default_auto]) 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 + None; + intro_using freshm; + new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshm),Rawterm.NoBindings)] + None + Genarg.IntroAnonymous + None; + intro_using freshz; + intros; + tclTRY ( + tclORELSE reflexivity (Equality.discr_tac false None) + ); + Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); + 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 + None) + 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]]) None + ); + 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 + all_occurrences + (List.hd !avoid) + ((mkVar (List.hd (List.tl !avoid))), + Rawterm.NoBindings + ) + true); + Pfedit.by (Equality.discr_tac false None) + + diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli new file mode 100644 index 00000000..b8fa1710 --- /dev/null +++ b/toplevel/auto_ind_decl.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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/cerrors.ml b/toplevel/cerrors.ml index f6c5c3af..40d74256 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 9306 2006-10-28 18:28:19Z herbelin $ *) +(* $Id: cerrors.ml 10410 2007-12-31 13:11:55Z msozeau $ *) open Pp open Util @@ -26,11 +26,7 @@ let print_loc loc = let guill s = "\""^s^"\"" let where s = - if !Options.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) - -let anomaly_string () = str "Anomaly: " - -let report () = (str "." ++ spc () ++ str "Please report.") + if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) @@ -68,12 +64,21 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") - | Univ.UniverseInconsistency -> - hov 0 (str "Error: Universe inconsistency.") + | Univ.UniverseInconsistency (o,u,v) -> + let msg = + if !Constrextern.print_universes then + spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++ + str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") + ++ spc() ++ Univ.pr_uni v ++ str")" + else + mt() in + hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te) | PretypeError(ctx,te) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te) + | Typeclasses_errors.TypeClassError(env, te) -> + hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te) | InductiveError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) | RecursionSchemeError e -> @@ -127,11 +132,15 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise) ++ report_fn ()) +let anomaly_string () = str "Anomaly: " + +let report () = (str "." ++ spc () ++ str "Please report.") + let explain_exn_default = - explain_exn_default_aux (fun () -> str "Anomaly: ") report + explain_exn_default_aux anomaly_string report let raise_if_debug e = - if !Options.debug then raise e + if !Flags.debug then raise e let _ = Tactic_debug.explain_logic_error := explain_exn_default diff --git a/toplevel/class.ml b/toplevel/class.ml index 5f385934..92fd2d4c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *) +(* $Id: class.ml 11085 2008-06-10 08:54:43Z herbelin $ *) open Util open Pp @@ -27,28 +27,12 @@ open Nametab open Decl_kinds open Safe_typing -let strength_min4 stre1 stre2 stre3 stre4 = - strength_min ((strength_min (stre1,stre2)),(strength_min (stre3,stre4))) +let strength_min l = if List.mem Local l then Local else Global let id_of_varid c = match kind_of_term c with | Var id -> id | _ -> anomaly "class__id_of_varid" -(* lf liste des variable dont depend la coercion f - lc liste des variable dont depend la classe source *) - -let rec stre_unif_cond = function - | ([],[]) -> Global - | (v::l,[]) -> variable_strength v - | ([],v::l) -> variable_strength v - | (v1::l1,v2::l2) -> - if v1=v2 then - stre_unif_cond (l1,l2) - else - let stre1 = (variable_strength v1) - and stre2 = (variable_strength v2) in - strength_min (stre1,stre2) - (* Errors *) type coercion_error_kind = @@ -98,9 +82,9 @@ let check_reference_arity ref = let check_arity = function | CL_FUN | CL_SORT -> () - | CL_CONST sp -> check_reference_arity (ConstRef sp) - | CL_SECVAR sp -> check_reference_arity (VarRef sp) - | CL_IND sp -> check_reference_arity (IndRef sp) + | CL_CONST cst -> check_reference_arity (ConstRef cst) + | CL_SECVAR id -> check_reference_arity (VarRef id) + | CL_IND kn -> check_reference_arity (IndRef kn) (* Coercions *) @@ -184,20 +168,22 @@ let prods_of t = aux [] t let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp + | CL_CONST kn -> Global + | CL_SECVAR id -> Local | _ -> Global let get_strength stre ref cls clt = let stres = strength_of_cl cls in let stret = strength_of_cl clt in let stref = strength_of_global ref in -(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? - let streunif = stre_unif_cond (s_vardep,f_vardep) in - *) - let streunif = Global in - let stre' = strength_min4 stres stret stref streunif in - strength_min (stre,stre') + strength_min [stre;stres;stret;stref] + +let ident_key_of_class = function + | CL_FUN -> "Funclass" + | CL_SORT -> "Sortclass" + | CL_CONST sp -> string_of_label (con_label sp) + | CL_IND (sp,_) -> string_of_label (label sp) + | CL_SECVAR id -> string_of_id id (* coercion identité *) @@ -239,15 +225,15 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> - id_of_string ("Id_"^(string_of_class source)^"_"^ - (string_of_class (fst (find_class_type t)))) + id_of_string ("Id_"^(ident_key_of_class source)^"_"^ + (ident_key_of_class (fst (find_class_type t)))) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()} in + const_entry_boxed = Flags.boxed_definitions()} in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn @@ -318,7 +304,7 @@ let try_add_new_coercion_with_source ref stre ~source = let add_coercion_hook stre ref = try_add_new_coercion ref stre; - Options.if_verbose message + Flags.if_verbose message (string_of_qualid (shortest_qualid_of_global Idset.empty ref) ^ " is now a coercion") diff --git a/toplevel/class.mli b/toplevel/class.mli index 7717d754..98ed6a0d 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: class.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: class.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) (*i*) open Names @@ -22,28 +22,28 @@ open Nametab (* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : global_reference -> strength -> +val try_add_new_coercion_with_target : global_reference -> locality -> source:cl_typ -> target:cl_typ -> unit (* [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : global_reference -> strength -> unit +val try_add_new_coercion : global_reference -> locality -> unit (* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a transparent constant which unfolds to some class [tg]; it declares an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) -val try_add_new_coercion_subclass : cl_typ -> strength -> unit +val try_add_new_coercion_subclass : cl_typ -> locality -> unit (* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : global_reference -> strength -> +val try_add_new_coercion_with_source : global_reference -> locality -> source:cl_typ -> unit (* [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an identity coercion from [src] to [tg] *) -val try_add_new_identity_coercion : identifier -> strength -> +val try_add_new_identity_coercion : identifier -> locality -> source:cl_typ -> target:cl_typ -> unit val add_coercion_hook : Tacexpr.declaration_hook diff --git a/toplevel/classes.ml b/toplevel/classes.ml new file mode 100644 index 00000000..8ed99cbd --- /dev/null +++ b/toplevel/classes.ml @@ -0,0 +1,737 @@ +(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Flags.silently (fun () -> + Auto.add_hints false [hint_db] + (Vernacexpr.HintsResolve + [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ()) + +let declare_instance_cst glob con = + let instance = Typeops.type_of_constant (Global.env ()) con in + let _, r = decompose_prod_assum instance in + match class_of_constr r with + | Some tc -> add_instance (new_instance tc None glob con) + | None -> error "Constant does not build instances of a declared type class" + +let declare_instance glob idl = + let con = + try (match global (Ident idl) with + | ConstRef x -> x + | _ -> raise Not_found) + with _ -> error "Instance definition not found" + in declare_instance_cst glob con + +let mismatched_params env n m = mismatched_ctx_inst env Parameters n m +(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) +let mismatched_props env n m = mismatched_ctx_inst env Properties n m + +type binder_list = (identifier located * bool * constr_expr) list + +let interp_binders_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) ((loc, i), t) -> + let n = Name i in + let t' = interp_binder_evars isevars env n t in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_typeclass_context_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) (iid, bk, l) -> + let t' = interp_binder_evars isevars env (snd iid) l in + let i = match snd iid with + | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids + | Name id -> id + in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_constrs_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) t -> + let t' = interp_binder_evars isevars env Anonymous t in + let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in + let d = (id,None,t') in + (push_named d env, id :: ids, d::params)) + (env, avoid, []) l + +let raw_assum_of_binders k = + List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t)) + +let raw_assum_of_constrs k = + List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t)) + +let raw_assum_of_anonymous_constrs k = + List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t)) + +let decl_expr_of_binders = + List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t)) + +let rec unfold n f acc = + match n with + | 0 -> f 0 acc + | n -> unfold (n - 1) f (f n acc) + +(* Declare everything in the parameters as implicit, and the class instance as well *) +open Topconstr + +let declare_implicit_proj c proj imps sub = + let len = List.length c.cl_context in + let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in + let expls = + let rec aux i expls = function + [] -> expls + | (Name n, _) :: tl -> + let impl = ExplByPos (i, Some n), (true, true) in + aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl + | (Anonymous,_) :: _ -> assert(false) + in + aux 1 [] (List.rev ctx) + in + let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in + if sub then + declare_instance_cst true (snd proj); + Impargs.declare_manual_implicits false (ConstRef (snd proj)) true expls + +let declare_implicits impls subs cl = + Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub) + cl.cl_projs impls subs; + let len = List.length cl.cl_context in + let indimps = + list_fold_left_i + (fun i acc (is, (na, b, t)) -> + if len - i <= cl.cl_params then acc + else + match is with + None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc + | _ -> acc) + 1 [] (List.rev cl.cl_context) + in + Impargs.declare_manual_implicits false cl.cl_impl false indimps + +let rel_of_named_context subst l = + List.fold_right + (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc) + l ([], subst) + +let ids_of_rel_context subst l = + List.fold_right + (fun (id, _, t) acc -> Nameops.out_name id :: acc) + l subst + +let degenerate_decl (na,b,t) = + let id = match na with + | Name id -> id + | Anonymous -> anomaly "Unnamed record variable" in + match b with + | None -> (id, Entries.LocalAssum t) + | Some b -> (id, Entries.LocalDef b) + + +let declare_structure env id idbuild params arity fields = + let nparams = List.length params and nfields = List.length fields in + let args = extended_rel_list nfields params in + let ind = applist (mkRel (1+nparams+nfields), args) in + let type_constructor = it_mkProd_or_LetIn ind fields in + let mie_ind = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } in + let mie = + { mind_entry_params = List.map degenerate_decl params; + mind_entry_record = true; + mind_entry_finite = true; + mind_entry_inds = [mie_ind] } in + let kn = Command.declare_mutual_with_eliminations true mie [] in + let rsp = (kn,0) in (* This is ind path of idstruc *) + let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in + let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in + let _build = ConstructRef (rsp,1) in + Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); + rsp + +let interp_type_evars evdref env ?(impls=([],[])) typ = + let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in + let imps = Implicit_quantifiers.implicits_of_rawterm typ' in + imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' + +let mk_interning_data env na impls typ = + let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls + in (na, ([], impl, Notation.compute_arguments_scope typ)) + +let interp_fields_evars isevars env avoid l = + List.fold_left + (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> + let impl, t' = interp_type_evars isevars env ~impls t in + let data = mk_interning_data env i impl t' in + let d = (i,None,t') in + (push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) + (env, [], avoid, [], ([], [])) l + +let interp_fields_rel_evars isevars env avoid l = + List.fold_left + (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> + let impl, t' = interp_type_evars isevars env ~impls t in + let data = mk_interning_data env i impl t' in + let d = (Name i,None,t') in + (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls))) + (env, [], avoid, [], ([], [])) l + +let name_typeclass_binder avoid = function + | LocalRawAssum ([loc, Anonymous], bk, c) -> + let name = + let id = + match c with + CApp (_, (_, CRef (Ident (loc,id))), _) -> id + | _ -> id_of_string "assum" + in Implicit_quantifiers.make_fresh avoid (Global.env ()) id + in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid + | x -> x, avoid + +let name_typeclass_binders avoid l = + let l', avoid = + List.fold_left + (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in + b' :: binders, avoid) + ([], avoid) l + in List.rev l', avoid + +let decompose_named_assum = + let rec prodec_rec subst l c = + match kind_of_term c with + | Prod (Name na,t,c) -> + let decl = (na,None,substl subst t) in + let subst' = mkVar na :: subst in + prodec_rec subst' (add_named_decl decl l) (substl subst' c) + | LetIn (Name na, b, t, c) -> + let decl = (na,Some (substl subst b),substl subst t) in + let subst' = mkVar na :: subst in + prodec_rec subst' (add_named_decl decl l) (substl subst' c) + | Cast (c,_,_) -> prodec_rec subst l c + | _ -> l,c + in prodec_rec [] [] + +let push_named_context = + List.fold_right push_named + +let named_of_rel_context (subst, ids, env as init) ctx = + Sign.fold_rel_context + (fun (na,c,t) (subst, avoid, env) -> + let id = Nameops.next_name_away na avoid in + let d = (id,Option.map (substl subst) c,substl subst t) in + (mkVar id :: subst, id::avoid, d::env)) + ctx ~init + +let new_class id par ar sup props = + let env0 = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in + let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in + let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in + let sup, bound = name_typeclass_binders bound sup in + let supnames = + List.fold_left (fun acc b -> + match b with + LocalRawAssum (nl, _, _) -> nl @ acc + | LocalRawDef _ -> assert(false)) + [] sup + in + + (* Interpret the arity *) + let arity_imps, fullarity = + let ar = + match ar with + Some ar -> ar | None -> (dummy_loc, Rawterm.RType None) + in + let arity = CSort (fst ar, snd ar) in + let term = prod_constr_expr (prod_constr_expr arity par) sup in + interp_type_evars isevars env0 term + in + let ctx_params, arity = decompose_prod_assum fullarity in + let env_params = push_rel_context ctx_params env0 in + + (* Interpret the definitions and propositions *) + let env_props, prop_impls, bound, ctx_props, _ = + interp_fields_rel_evars isevars env_params bound props + in + let subs = List.map (fun ((loc, id), b, _) -> b) props in + (* Instantiate evars and check all are resolved *) + let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in + let isevars = Typeclasses.resolve_typeclasses env_props isevars in + let sigma = Evd.evars_of isevars in + let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in + let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in + let arity = Reductionops.nf_evar sigma arity in + let ce t = Evarutil.check_evars env0 Evd.empty isevars t in + let impl, projs = + let params = ctx_params and fields = ctx_props in + List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields); + match fields with + [(Name proj_name, _, field)] -> + let class_body = it_mkLambda_or_LetIn field params in + let class_type = + match ar with + Some _ -> Some (it_mkProd_or_LetIn arity params) + | None -> None + in + let class_entry = + { const_entry_body = class_body; + const_entry_type = class_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in + let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in + let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in + let proj_entry = + { const_entry_body = proj_body; + const_entry_type = Some proj_type; + const_entry_opaque = false; + const_entry_boxed = false } + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + ConstRef cst, [proj_name, proj_cst] + | _ -> + let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in + let kn = declare_structure env0 (snd id) idb params arity fields in + IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) + fields (Recordops.lookup_projections kn)) + in + let ids = List.map pi1 (named_context env0) in + let (subst, ids, named_ctx_params) = named_of_rel_context ([], ids, []) ctx_params in + let (_, _, named_ctx_props) = named_of_rel_context (subst, ids, []) ctx_props in + let ctx_context = + List.map (fun ((na, b, t) as d) -> + match Typeclasses.class_of_constr t with + | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = Name na) supnames), d) + | None -> (None, d)) + named_ctx_params + in + let k = + { cl_impl = impl; + cl_params = List.length par; + cl_context = ctx_context; + cl_props = named_ctx_props; + cl_projs = projs } + in + declare_implicits (List.rev prop_impls) subs k; + add_class k + +type binder_def_list = (identifier located * identifier located list * constr_expr) list + +let binders_of_lidents l = + List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l + +let subst_ids_in_named_context subst l = + let x, _ = + List.fold_right + (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k) + l ([], 1) + in x + +let subst_one_named inst ids t = + substnl inst 0 (substn_vars 1 ids t) + +let subst_named inst subst ctx = + let ids = List.map (fun (id, _, _) -> id) subst in + let ctx' = subst_ids_in_named_context ids ctx in + let ctx', _ = + List.fold_right + (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k) + ctx' ([], 0) + in ctx' +(* +let infer_super_instances env params params_ctx super = + let super = subst_named params params_ctx super in + List.fold_right + (fun (na, _, t) (sups, ids, supctx) -> + let t = subst_one_named sups ids t in + let inst = + try resolve_one_typeclass env t + with Not_found -> + let cl, args = destClass t in + no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args) + in + let d = (na, Some inst, t) in + inst :: sups, na :: ids, d :: supctx) + super ([], [], [])*) + +(* let evars_of_context ctx id n env = *) +(* List.fold_right (fun (na, _, t) (n, env, nc) -> *) +(* let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *) +(* let d = (na, Some b, t) in *) +(* (succ n, push_named d env, d :: nc)) *) +(* ctx (n, env, []) *) + +let type_ctx_instance isevars env ctx inst subst = + List.fold_left2 + (fun (subst, instctx) (na, _, t) ce -> + let t' = replace_vars subst t in + let c = interp_casted_constr_evars isevars env ce t' in + let d = na, Some c, t' in + (na, c) :: subst, d :: instctx) + (subst, []) (List.rev ctx) inst + +let substitution_of_constrs ctx cstrs = + List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] + +let destClassApp cl = + match cl with + | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l + | _ -> raise Not_found + +let refine_ref = ref (fun _ -> assert(false)) + +let id_of_class cl = + match cl.cl_impl with + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l + | IndRef (kn,i) -> + let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in + mip.(0).Declarations.mind_typename + | _ -> assert false + +open Pp + +let ($$) g f = fun x -> g (f x) + +let default_on_free_vars = + Flags.if_verbose + (fun fvs -> + match fvs with + [] -> () + | l -> msgnl (str"Implicitly generalizing " ++ + prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str".")) + +let fail_on_free_vars = function + [] -> () + | [fv] -> + errorlabstrm "Classes" + (str"Unbound variable " ++ Nameops.pr_id fv ++ str".") + | fvs -> errorlabstrm "Classes" + (str"Unbound variables " ++ + prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".") + +let instance_hook k pri global imps ?hook cst = + let inst = Typeclasses.new_instance k pri global cst in + Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps; + Typeclasses.add_instance inst; + (match hook with Some h -> h cst | None -> ()) + +let declare_instance_constant k pri global imps ?hook id term termtype = + let cdecl = + let kind = IsDefinition Instance in + let entry = + { const_entry_body = term; + const_entry_type = Some termtype; + const_entry_opaque = false; + const_entry_boxed = false } + in DefinitionEntry entry, kind + in + let kn = Declare.declare_constant id cdecl in + Flags.if_verbose Command.definition_message id; + instance_hook k pri global imps ?hook kn; + id + +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) + ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = + let env = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in + let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in + let tclass = + match bk with + | Implicit -> + let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in + let k = class_info (Nametab.global id) in + let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in + let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in + if needlen <> applen then + mismatched_params env (List.map fst par) (List.map snd k.cl_context); + let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) + (fun avoid (clname, (id, _, t)) -> + match clname with + Some (cl, b) -> + let t = + if b then + let _k = class_info cl in + CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None)))) + else CHole (Util.dummy_loc, None) + in t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + par (List.rev k.cl_context) + in Topconstr.CAppExpl (loc, (None, id), pars) + + | Explicit -> cl + in + let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in + let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in + on_free_vars (List.rev fvs @ List.rev gen_ids); + let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in + let bound = Idset.union gen_idset ctx_bound in + let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in + let ctx, avoid = name_typeclass_binders bound ctx in + let ctx = List.append ctx (List.rev gen_ctx) in + let k, ctx', imps, subst = + let c = Command.generalize_constr_expr tclass ctx in + let imps, c' = interp_type_evars isevars env c in + let ctx, c = decompose_named_assum c' in + let cl, args = Typeclasses.dest_class_app c in + cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) + in + let id = + match snd instid with + Name id -> + let sp = Lib.make_path id in + if Nametab.exists_cci sp then + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + id + | Anonymous -> + let i = Nameops.add_suffix (id_of_class k) "_instance_0" in + Termops.next_global_ident_away false i (Termops.ids_of_context env) + in + let env' = push_named_context ctx' env in + isevars := Evarutil.nf_evar_defs !isevars; + isevars := resolve_typeclasses env !isevars; + let sigma = Evd.evars_of !isevars in + let substctx = Typeclasses.nf_substitution sigma subst in + if Lib.is_modtype () then + begin + let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in + let termtype = + let t = it_mkNamedProd_or_LetIn ty_constr ctx' in + Evarutil.nf_isevar !isevars t + in + Evarutil.check_evars env Evd.empty !isevars termtype; + let cst = Declare.declare_internal_constant id + (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical) + in instance_hook k None false imps ?hook cst; id + end + else + begin + let subst, _propsctx = + let props = + List.map (fun (x, l, d) -> + x, Topconstr.abstract_constr_expr d (binders_of_lidents l)) + props + in + if List.length props > List.length k.cl_props then + mismatched_props env' (List.map snd props) k.cl_props; + let props, rest = + List.fold_left + (fun (props, rest) (id,_,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); + c :: props, rest' + with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props substctx + in + let app, ty_constr = instance_constructor k (List.rev_map snd subst) in + let termtype = + let t = it_mkNamedProd_or_LetIn ty_constr ctx' in + Evarutil.nf_isevar !isevars t + in + let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in + isevars := Evarutil.nf_evar_defs !isevars; + let term = Evarutil.nf_isevar !isevars term in + let evm = Evd.evars_of (undefined_evars !isevars) in + Evarutil.check_evars env Evd.empty !isevars termtype; + if evm = Evd.empty then + declare_instance_constant k pri global imps ?hook id term termtype + else begin + isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; + let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in + Flags.silently (fun () -> + Command.start_proof id kind termtype + (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst + | _ -> assert false); + if props <> [] then + Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) + (!refine_ref (evm, term)); + (match tac with Some tac -> Pfedit.by tac | None -> ())) (); + Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); + id + end + end + +let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition + +let solve_by_tac env evd evar evi t = + let goal = {it = evi; sigma = (Evd.evars_of evd) } in + let (res, valid) = t goal in + if res.it = [] then + let prooftree = valid [] in + let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in + if obls = [] then + let evd' = evars_reset_evd res.sigma evd in + let evd' = evar_define evar proofterm evd' in + evd', true + else evd, false + else evd, false + +let context ?(hook=fun _ -> ()) l = + let env = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let avoid = Termops.ids_of_context env in + let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in + let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in + let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in + isevars := Evarutil.nf_evar_defs !isevars; + let sigma = Evd.evars_of !isevars in + let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in + List.iter (function (id,_,t) -> + if Lib.is_modtype () then + let cst = Declare.declare_internal_constant id + (ParameterEntry (t,false), IsAssumption Logical) + in + match class_of_constr t with + | Some tc -> + add_instance (Typeclasses.new_instance tc None false cst); + hook (ConstRef cst) + | None -> () + else + (Command.declare_one_assumption false (Local (* global *), Definitional) t + [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id); + match class_of_constr t with + None -> () + | Some tc -> hook (VarRef id))) + (List.rev fullctx) + +open Libobject + +let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init") +let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation") + +let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid))) +let tactic = lazy (Tacinterp.interp tactic_expr) + +let _ = + Typeclasses.solve_instanciation_problem := + (fun env evd ev evi -> + Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *) + solve_by_tac env evd ev evi (Lazy.force tactic)) + +(* let prod = lazy_fun Coqlib.build_prod *) + +(* let build_conjunction evm = *) +(* List.fold_left *) +(* (fun (acc, evs) (ev, evi) -> *) +(* if class_of_constr evi.evar_concl <> None then *) +(* mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *) +(* else acc, Evd.add evs ev evi) *) +(* (Coqlib.build_coq_True (), Evd.empty) evm *) + +(* let destruct_conjunction evm_list evm evm' term = *) +(* let _, evm = *) +(* List.fold_right *) +(* (fun (ev, evi) (term, evs) -> *) +(* if class_of_constr evi.evar_concl <> None then *) +(* match kind_of_term term with *) +(* | App (x, [| _ ; _ ; proof ; term |]) -> *) +(* let evs' = Evd.define evs ev proof in *) +(* (term, evs') *) +(* | _ -> assert(false) *) +(* else *) +(* match (Evd.find evm' ev).evar_body with *) +(* Evar_empty -> raise Not_found *) +(* | Evar_defined c -> *) +(* let evs' = Evd.define evs ev c in *) +(* (term, evs')) *) +(* evm_list (term, evm) *) +(* in evm *) + +(* let solve_by_tac env evd evar evi t = *) +(* let goal = {it = evi; sigma = (Evd.evars_of evd) } in *) +(* let (res, valid) = t goal in *) +(* if res.it = [] then *) +(* let prooftree = valid [] in *) +(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) +(* if obls = [] then *) +(* let evd' = evars_reset_evd res.sigma evd in *) +(* let evd' = evar_define evar proofterm evd' in *) +(* evd', true *) +(* else evd, false *) +(* else evd, false *) + +(* let resolve_all_typeclasses env evd = *) +(* let evm = Evd.evars_of evd in *) +(* let evm_list = Evd.to_list evm in *) +(* let goal, typesevm = build_conjunction evm_list in *) +(* let evars = ref (Evd.create_evar_defs typesevm) in *) +(* let term = resolve_one_typeclass_evd env evars goal in *) +(* let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *) +(* Evd.create_evar_defs evm' *) + +(* let _ = *) +(* Typeclasses.solve_instanciations_problem := *) +(* (fun env evd -> *) +(* Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *) +(* resolve_all_typeclasses env evd) *) + +let solve_evars_by_tac env evd t = + let ev = make_evar empty_named_context_val mkProp in + let goal = {it = ev; sigma = (Evd.evars_of evd) } in + let (res, valid) = t goal in + let evd' = evars_reset_evd res.sigma evd in + evd' +(* Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *) + +(* let _ = *) +(* Typeclasses.solve_instanciations_problem := *) +(* (fun env evd -> *) +(* Eauto.resolve_all_evars false (true, 15) env *) +(* (fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *) +(* && class_of_constr evi.evar_concl <> None) evd) *) diff --git a/toplevel/classes.mli b/toplevel/classes.mli new file mode 100644 index 00000000..f3cb0c58 --- /dev/null +++ b/toplevel/classes.mli @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* local_binder list + +val declare_implicit_proj : typeclass -> (identifier * constant) -> + Impargs.manual_explicitation list -> bool -> unit +(* +val infer_super_instances : env -> constr list -> + named_context -> named_context -> types list * identifier list * named_context +*) +val new_class : identifier located -> + local_binder list -> + Vernacexpr.sort_expr located option -> + local_binder list -> + binder_list -> unit + +(* By default, print the free variables that are implicitely generalized. *) + +val default_on_free_vars : identifier list -> unit + +val fail_on_free_vars : identifier list -> unit + +val declare_instance_constant : + typeclass -> + int option -> (* priority *) + bool -> (* globality *) + Impargs.manual_explicitation list -> (* implicits *) + ?hook:(Names.constant -> unit) -> + identifier -> (* name *) + Term.constr -> (* body *) + Term.types -> (* type *) + Names.identifier + +val new_instance : + ?global:bool -> (* Not global by default. *) + local_binder list -> + typeclass_constraint -> + binder_def_list -> + ?on_free_vars:(identifier list -> unit) -> + ?tac:Proof_type.tactic -> + ?hook:(constant -> unit) -> + int option -> + identifier + +(* For generation on names based on classes only *) +val id_of_class : typeclass -> identifier + +val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit + +val declare_instance : bool -> identifier located -> unit + +val mismatched_params : env -> constr_expr list -> named_context -> 'a + +val mismatched_props : env -> constr_expr list -> named_context -> 'a + +val solve_by_tac : env -> + Evd.evar_defs -> + Evd.evar -> + evar_info -> + Proof_type.tactic -> + Evd.evar_defs * bool + +val solve_evars_by_tac : env -> + Evd.evar_defs -> + Proof_type.tactic -> + Evd.evar_defs + +val refine_ref : (open_constr -> Proof_type.tactic) ref + +val decompose_named_assum : types -> named_context * types + +val push_named_context : named_context -> env -> env + +val name_typeclass_binders : Idset.t -> + Topconstr.local_binder list -> + Topconstr.local_binder list * Idset.t + diff --git a/toplevel/command.ml b/toplevel/command.ml index a8e0133e..531eadb3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 10067 2007-08-09 17:13:16Z msozeau $ *) +(* $Id: command.ml 11169 2008-06-24 14:37:18Z notin $ *) open Pp open Util -open Options +open Flags open Term open Termops open Declarations @@ -42,22 +42,26 @@ open Pretyping open Evarutil open Evarconv open Notation +open Goptions +open Mod_subst +open Evd +open Decls -let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) -let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) +let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b)) +let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b)) let rec abstract_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + | LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl (abstract_constr_expr c bl) let rec generalize_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],t,b)) idl + | LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl (generalize_constr_expr c bl) let rec under_binders env f n c = @@ -80,7 +84,7 @@ let rec destSubCast c = match kind_of_term c with let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) - | CHole loc -> + | CHole (loc, k) -> let (has_no_args,name,params) = a in if not has_no_args then user_err_loc (loc,"", @@ -98,13 +102,13 @@ let definition_message id = if_verbose message ((string_of_id id) ^ " is defined") let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = - let sigma = Evd.empty in let env = Global.env() in - match comtypopt with + match comtypopt with None -> let b = abstract_constr_expr com bl in - let j = interp_constr_judgment sigma env b in - { const_entry_body = j.uj_val; + let b, imps = interp_constr_evars_impls env b in + imps, + { const_entry_body = b; const_entry_type = None; const_entry_opaque = opacity; const_entry_boxed = boxed } @@ -112,7 +116,9 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in - let (body,typ) = destSubCast (interp_constr sigma env b) in + let b, imps = interp_constr_evars_impls env b in + let (body,typ) = destSubCast b in + imps, { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = opacity; @@ -127,16 +133,23 @@ let red_constant_entry bl ce = function (local_binders_length bl) body } -let declare_global_definition ident ce local = +let declare_global_definition ident ce local imps = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in - if local = Local && Options.is_verbose() then - msg_warning (pr_id ident ++ str" is declared as a global definition"); - definition_message ident; - ConstRef kn + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + if local = Local && Flags.is_verbose() then + msg_warning (pr_id ident ++ str" is declared as a global definition"); + definition_message ident; + gr + +let declare_definition_hook = ref ignore +let set_declare_definition_hook = (:=) declare_definition_hook +let get_declare_definition_hook () = !declare_definition_hook let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = - let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in + let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in let ce' = red_constant_entry bl ce red_option in + !declare_definition_hook ce'; let r = match local with | Local when Lib.sections_are_opened () -> let c = @@ -144,28 +157,29 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; if Pfedit.refining () then - msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ - str" is not visible from current goals"); + Flags.if_verbose msg_warning + (str"Local definition " ++ pr_id ident ++ + str" is not visible from current goals"); VarRef ident | (Global|Local) -> - declare_global_definition ident ce' local in + declare_global_definition ident ce' local imps in hook local r -let syntax_definition ident c local onlyparse = - let c = snd (interp_aconstr [] [] c) in - Syntax_def.declare_syntactic_definition local ident onlyparse c +let syntax_definition ident (vars,c) local onlyparse = + let pat = interp_aconstr [] vars c in + Syntax_def.declare_syntactic_definition local ident onlyparse pat (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c (_,ident) = +let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = declare_variable ident - (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ @@ -173,19 +187,26 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = VarRef ident | (Global|Local) -> let kn = - declare_constant ident (ParameterEntry c, IsAssumption kind) in + declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; assumption_message ident; - if local=Local & Options.is_verbose () then + if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); - ConstRef kn in + gr in if is_coe then Class.try_add_new_coercion r local -let declare_assumption idl is_coe k bl c = +let declare_assumption_hook = ref ignore +let set_declare_assumption_hook = (:=) declare_assumption_hook + +let declare_assumption idl is_coe k bl c impl keep nl = if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in - let c = interp_type Evd.empty (Global.env()) c in - List.iter (declare_one_assumption is_coe k c) idl + let env = Global.env () in + let c', imps = interp_type_evars_impls env c in + !declare_assumption_hook c'; + List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -193,6 +214,8 @@ let declare_assumption idl is_coe k bl c = (* 3a| Elimination schemes for mutual inductive definitions *) open Indrec +open Inductiveops + let non_type_eliminations = [ (InProp,elimination_suffix InProp); @@ -208,7 +231,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() }, + const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Definition) in definition_message id; kn @@ -248,27 +271,189 @@ 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 + try + 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 = Flags.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 + with Not_found -> + error "Your type contains Parameters without a boolean equality" + +(* decidability of eq *) + + +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_hook = ref ignore +let set_start_hook = (:=) start_hook + +let start_proof id kind c ?init_tac hook = + let sign = Global.named_context () in + let sign = clear_proofs sign in + !start_hook c; + Pfedit.start_proof id kind sign c ?init_tac:init_tac hook + +let save id const (locality,kind) hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let k = logical_kind_of_goal_kind kind in + let l,r = match locality with + | Local when Lib.sections_are_opened () -> + let c = SectionLocalDef (pft, tpo, opacity) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local, VarRef id) + | Local | Global -> + 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_hook = ref ignore +let set_save_hook f = save_hook := f + +let save_named opacity = + let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook 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); + try + if (!eq_flag) then (make_eq_decidability (sp,i)) + with _ -> + Pfedit.delete_current_proof(); + message "Error while computing decidability scheme. Please report." + done; + end (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl = - let mk_interning_data na typ = +let compute_interning_datas env l nal typl impll = + let mk_interning_data na typ impls = let idl, impl = - if is_implicit_args() then - let impl = compute_implicits env typ in - let sub_impl,_ = list_chop (List.length l) impl in - let sub_impl' = List.filter is_status_implicit sub_impl in + let impl = + compute_implicits_with_manual env typ (is_implicit_args ()) impls + in + let sub_impl,_ = list_chop (List.length l) impl in + let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) - else - ([],[]) in - (na, (idl, impl, compute_arguments_scope typ)) in - (l, List.map2 mk_interning_data nal typl) + in + (na, (idl, impl, compute_arguments_scope typ)) in + (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = silently (Metasyntax.add_notation_interpretation df impls c) scope @@ -294,34 +479,39 @@ let minductive_message = function spc () ++ str "are defined") let check_all_names_different indl = - let get_names ind = ind.ind_name::List.map fst ind.ind_lc in - if not (list_distinct (List.flatten (List.map get_names indl))) then - error "Two inductive objects have the same name" - -let mk_mltype_data isevars env assums arity indname = - let is_ml_type = is_sort env (Evd.evars_of !isevars) arity in + let ind_names = List.map (fun ind -> ind.ind_name) indl in + let cstr_names = list_map_append (fun ind -> List.map fst ind.ind_lc) indl in + let l = list_duplicates ind_names in + if l <> [] then raise (InductiveError (SameNamesTypes (List.hd l))); + let l = list_duplicates cstr_names in + if l <> [] then raise (InductiveError (SameNamesConstructors (List.hd l))); + let l = list_intersect ind_names cstr_names in + if l <> [] then raise (InductiveError (SameNamesOverlap l)) + +let mk_mltype_data evdref env assums arity indname = + let is_ml_type = is_sort env (evars_of !evdref) arity in (is_ml_type,indname,assums) let prepare_param = function | (na,None,t) -> out_name na, LocalAssum t | (na,Some b,_) -> out_name na, LocalDef b -let interp_ind_arity isevars env ind = - interp_type_evars isevars env ind.ind_arity +let interp_ind_arity evdref env ind = + interp_type_evars evdref env ind.ind_arity -let interp_cstrs isevars env impls mldata arity ind = +let interp_cstrs evdref env impls mldata arity ind = let cnames,ctyps = List.split ind.ind_lc in (* Complete conclusions of constructor types if given in ML-style syntax *) let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in (* Interpret the constructor types *) - let ctyps'' = List.map (interp_type_evars isevars env ~impls) ctyps' in - (cnames, ctyps'') + let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in + (cnames, ctyps'', cimpls) let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let env_params, ctx_params = interp_context_evars isevars env0 paramsl in + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -329,37 +519,38 @@ let interp_mutual paramsl indl notations finite = let params = List.map (fun (na,_,_) -> out_name na) assums in (* Interpret the arities *) - let arities = List.map (interp_ind_arity isevars env_params) indl in + let arities = List.map (interp_ind_arity evdref env_params) indl in let fullarities = List.map (fun c -> it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let impls = compute_interning_datas env0 params indnames fullarities in - let mldatas = List.map2 (mk_mltype_data isevars env_params params) arities indnames in + let indimpls = List.map (fun _ -> userimpls) fullarities in + let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = States.with_heavy_rollback (fun () -> (* Temporary declaration of notations and scopes *) List.iter (declare_interning_data impls) notations; (* Interpret the constructor types *) - list_map3 (interp_cstrs isevars env_ar_params impls) mldatas arities indl) + list_map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl) () in (* Instantiate evars and check all are resolved *) - let isevars,_ = consider_remaining_unif_problems env_params !isevars in - let sigma = Evd.evars_of isevars in - let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in + let evd,_ = consider_remaining_unif_problems env_params !evdref in + let sigma = evars_of evd in + let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in - List.iter (check_evars env_params Evd.empty isevars) arities; - Sign.iter_rel_context (check_evars env0 Evd.empty isevars) ctx_params; - List.iter (fun (_,ctyps) -> - List.iter (check_evars env_ar_params Evd.empty isevars) ctyps) + List.iter (check_evars env_params Evd.empty evd) arities; + Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + List.iter (fun (_,ctyps,_) -> + List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; (* Build the inductive entries *) - let entries = list_map3 (fun ind arity (cnames,ctypes) -> { + let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; mind_entry_consnames = cnames; @@ -370,15 +561,15 @@ let interp_mutual paramsl indl notations finite = { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = false; mind_entry_finite = finite; - mind_entry_inds = entries } + mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors) let eq_constr_expr c1 c2 = try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false (* Very syntactical equality *) let eq_local_binder d1 d2 = match d1,d2 with - | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) -> - List.length nal1 = List.length nal2 && + | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) -> + List.length nal1 = List.length nal2 && k1 = k2 && List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 && eq_constr_expr c1 c2 | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> @@ -410,23 +601,49 @@ let prepare_inductive ntnl indl = ind_arity = ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl in - List.fold_right option_cons ntnl [], indl + List.fold_right Option.List.cons ntnl [], indl + + +let elim_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of eliminations"; + optkey = (SecondaryTable ("Elimination","Schemes")); + optread = (fun () -> !elim_flag) ; + optwrite = (fun b -> elim_flag := b) } + + +let lift_implicits n = + List.map (fun x -> + match fst x with + ExplByPos (k, id) -> ExplByPos (k + n, id), snd x + | _ -> x) -let declare_mutual_with_eliminations isrecord mie = +let declare_mutual_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_,kn) = declare_mind isrecord mie in - if_verbose ppnl (minductive_message names); - declare_eliminations kn; - kn + let params = List.length mie.mind_entry_params in + let (_,kn) = declare_mind isrecord mie in + list_iter_i (fun i (indimpls, constrimpls) -> + let ind = (kn,i) in + list_iter_i + (fun j impls -> + maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) + (is_implicit_args()) (indimpls @ (lift_implicits params impls))) + constrimpls) + impls; + if_verbose ppnl (minductive_message names); + if !elim_flag then declare_eliminations kn; + kn let build_mutual l finite = let indl,ntnl = List.split l in let paramsl = extract_params indl in let coes = extract_coercions indl in let notations,indl = prepare_inductive ntnl indl in - let mie = interp_mutual paramsl indl notations finite in + let mie,impls = interp_mutual paramsl indl notations finite in (* Declare the mutual inductive block with its eliminations *) - ignore (declare_mutual_with_eliminations false mie); + ignore (declare_mutual_with_eliminations false mie impls); (* Declare the possible notations of inductive types *) List.iter (declare_interning_data ([],[])) notations; (* Declare the coercions *) @@ -434,13 +651,27 @@ let build_mutual l finite = (* 3c| Fixpoints and co-fixpoints *) -let recursive_message = function +let pr_rank = function + | 0 -> str "1st" + | 1 -> str "2nd" + | 2 -> str "3rd" + | n -> str ((string_of_int (n+1))^"th") + +let recursive_message indexes = function | [] -> anomaly "no recursive definition" - | [id] -> pr_id id ++ str " is recursively defined" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ - spc () ++ str "are recursively defined") - -let corecursive_message = function + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ()) + +let corecursive_message _ = function | [] -> error "no corecursive definition" | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ @@ -521,7 +752,7 @@ let check_mutuality env kind fixl = | _ -> () type fixpoint_kind = - | IsFixpoint of (int option * recursion_order_expr) list + | IsFixpoint of (identifier located option * recursion_order_expr) list | IsCoFixpoint type fixpoint_expr = { @@ -531,15 +762,20 @@ type fixpoint_expr = { fix_type : constr_expr } -let interp_fix_type isevars env fix = - interp_type_evars isevars env - (generalize_constr_expr fix.fix_type fix.fix_binders) +let interp_fix_context evdref env fix = + interp_context_evars evdref env fix.fix_binders -let interp_fix_body isevars env impls fix fixtype = - interp_casted_constr_evars isevars env ~impls - (abstract_constr_expr fix.fix_body fix.fix_binders) fixtype +let interp_fix_ccl evdref (env,_) fix = + interp_type_evars evdref env fix.fix_type -let declare_fix boxed kind f def t = +let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = + let env = push_rel_context ctx env_rec in + let body = interp_casted_constr_evars evdref env ~impls fix.fix_body ccl in + it_mkLambda_or_LetIn body ctx + +let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx + +let declare_fix boxed kind f def t imps = let ce = { const_entry_body = def; const_entry_type = Some t; @@ -547,26 +783,37 @@ let declare_fix boxed kind f def t = const_entry_boxed = boxed } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in - ConstRef kn - + let gr = ConstRef kn in + maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + gr + let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) -let compute_guardness_evidence (n,_) fixl fixtype = +(* Jump over let-bindings. *) + +let rel_index n ctx = + list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) + +let rec unfold f b = + match f b with + | Some (x, b') -> x :: unfold f b' + | None -> [] + +let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = match n with - | Some n -> n + | Some (loc, n) -> [rel_index n fixctx] | None -> - (* Recursive argument was not given by the user : - We check that there is only one inductive argument *) - let m = local_binders_length fixl.fix_binders in - let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in - let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in - (* This could be more precise (e.g. do some delta) *) - let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in - try (list_unique_index true lb) - 1 - with Not_found -> error "the recursive argument needs to be specified" + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let len = List.length fixctx in + unfold (function x when x = len -> None + | n -> Some (n, succ n)) 0 let interp_recursive fixkind l boxed = let env = Global.env() in @@ -575,70 +822,124 @@ let interp_recursive fixkind l boxed = let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let isevars = ref (Evd.create_evar_defs Evd.empty) in - let fixtypes = List.map (interp_fix_type isevars env) fixl in + let evdref = ref (Evd.create_evar_defs Evd.empty) in + let fixctxs, fiximps = + List.split (List.map (interp_fix_context evdref env) fixl) in + let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes in - let notations = List.fold_right option_cons ntnl [] in + let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = States.with_heavy_rollback (fun () -> List.iter (declare_interning_data impls) notations; - List.map2 (interp_fix_body isevars env_rec impls) fixl fixtypes) + list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in (* Instantiate evars and check all are resolved *) - let isevars,_ = consider_remaining_unif_problems env_rec !isevars in - let fixdefs = List.map (nf_evar (Evd.evars_of isevars)) fixdefs in - let fixtypes = List.map (nf_evar (Evd.evars_of isevars)) fixtypes in - List.iter (check_evars env_rec Evd.empty isevars) fixdefs; - List.iter (check_evars env Evd.empty isevars) fixtypes; + let evd,_ = consider_remaining_unif_problems env_rec !evdref in + let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in + let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in + List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (check_evars env Evd.empty evd) fixtypes; check_mutuality env kind (List.combine fixnames fixdefs); (* Build the fix declaration block *) let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let fixdecls = + let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> - let fixwf = list_map3 compute_guardness_evidence wfl fixl fixtypes in - list_map_i (fun i _ -> mkFix ((Array.of_list fixwf,i),fixdecls)) 0 l + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in + let indexes = search_guard dummy_loc env possible_indexes fixdecls in + Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l | IsCoFixpoint -> - list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l + None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) - ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes); - if_verbose ppnl (recursive_message kind fixnames); + ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps); + if_verbose ppnl (recursive_message kind indexes fixnames); (* Declare notations *) List.iter (declare_interning_data ([],[])) notations let build_recursive l b = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in - let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) l in interp_recursive (IsFixpoint g) fixl b let build_corecursive l b = - let fixl = List.map (fun ((id,bl,typ,def),ntn) -> + let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) l in interp_recursive IsCoFixpoint fixl b (* 3d| Schemes *) - -let build_scheme lnamedepindsort = +let rec split_scheme l = + let env = Global.env() in + match l with + | [] -> [],[] + | (Some id,t)::q -> let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2 + | EqualityScheme x -> l1,(x::l2) + ) +(* + if no name has been provided, we build one from the types of the ind +requested +*) + | (None,t)::q -> + let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> + let ind = mkInd (Nametab.inductive_of_reference y) in + let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) +in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + else ( match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + | _ -> + if x then (match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + else (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + ) in + let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in + let newref = (dummy_loc,id_of_string newid) in + ((newref,x,y,z)::l1),l2 + | EqualityScheme x -> l1,(x::l2) + ) + + +let build_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and sigma = Evd.empty and env0 = Global.env() in let lrecspec = List.map (fun (_,dep,indid,sort) -> - let ind = Nametab.global_inductive indid in + let ind = Nametab.inductive_of_reference indid in let (mib,mip) = Global.lookup_inductive ind in (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort @@ -650,114 +951,259 @@ let build_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in - if_verbose ppnl (recursive_message Fixpoint lrecnames) - -let rec get_concl n t = - if n = 0 then t - else - match kind_of_term t with - Prod (_,_,t) -> get_concl (pred n) t - | _ -> raise (Invalid_argument "get_concl") - -let cut_last l = - let rec aux acc = function - hd :: [] -> List.rev acc, hd - | hd :: tl -> aux (hd :: acc) tl - | [] -> raise (Invalid_argument "cut_last") - in aux [] l + if_verbose ppnl (recursive_message Fixpoint None lrecnames) + +let build_scheme l = + let ischeme,escheme = split_scheme l in +(* we want 1 kind of scheme at a time so we check if the user +tried to declare different schemes at once *) + if (ischeme <> []) && (escheme <> []) + then + error "Do not declare equality and induction scheme at the same time." + else ( + if ischeme <> [] then build_induction_scheme ischeme; + List.iter ( fun indname -> + let ind = Nametab.inductive_of_reference indname + in declare_eq_scheme (fst ind); + try + make_eq_decidability ind + with _ -> + Pfedit.delete_current_proof(); + message "Error while computing decidability scheme. Please report." + ) escheme + ) +let list_split_rev_at index l = + let rec aux i acc = function + hd :: tl when i = index -> acc, tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_at: Invalid argument" + in aux 0 [] l + +let fold_left' f = function + [] -> raise (Invalid_argument "fold_right'") + | hd :: tl -> List.fold_left f hd tl + let build_combined_scheme name schemes = let env = Global.env () in - let defs = +(* let nschemes = List.length schemes in *) + let find_inductive ty = + let (ctx, arity) = decompose_prod ty in + let (_, last) = List.hd ctx in + match kind_of_term last with + | App (ind, args) -> ctx, destInd ind, Array.length args + | _ -> ctx, destInd last, 0 + in + let defs = List.map (fun x -> let refe = Ident x in let qualid = qualid_of_reference refe in - let cst = Nametab.locate_constant (snd qualid) in - qualid, cst, Typeops.type_of_constant env cst) + let cst = try + Nametab.locate_constant (snd qualid) + with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared") + in + let ty = Typeops.type_of_constant env cst in + qualid, cst, ty) schemes in let (qid, c, t) = List.hd defs in - let nargs = - let (_, arity, _) = destProd t in - nb_prod arity - in - let prods = nb_prod t - nargs in - let defs, (qid, c, t) = cut_last defs in - let (args, concl) = decompose_prod_n prods t in - let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in + let ctx, ind, nargs = find_inductive t in + (* Number of clauses, including the predicates quantification *) + let prods = nb_prod t - (nargs + 1) in let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in let relargs = rel_vect 0 prods in - let concl_typ, concl_bod = - List.fold_right - (fun (cst, x) (acct, accb) -> - mkApp (coqand, [| x; acct |]), - mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) - concls (concl, mkApp (mkConst c, relargs)) + let concls = List.rev_map + (fun (_, cst, t) -> + mkApp(mkConst cst, relargs), + snd (decompose_prod_n prods t)) defs in + let concl_bod, concl_typ = + fold_left' + (fun (accb, acct) (cst, x) -> + mkApp (coqconj, [| x; acct; cst; accb |]), + mkApp (coqand, [| x; acct |])) concls in - let ctx = List.map (fun (x, y) -> x, None, y) args in + let ctx, _ = + list_split_rev_at prods + (List.rev_map (fun (x, y) -> x, None, y) ctx) in let typ = it_mkProd_wo_LetIn concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in let ce = { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in - if_verbose ppnl (recursive_message Fixpoint [snd name]) - + 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 -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - errorlabstrm "start_proof" (pr_id id ++ str " already exists"); - id - | None -> - next_global_ident_away false (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let env = Global.env () in - let c = interp_type Evd.empty env (generalize_constr_expr t bl) in - 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 +(* 4.1| Support for mutually proved theorems *) + +let retrieve_first_recthm = function + | VarRef id -> + (pi2 (Global.lookup_named id),variable_opacity id) + | ConstRef cst -> + let {const_body=body;const_opaque=opaq} = + Global.lookup_constant cst in + (Option.map Declarations.force body,opaq) + | _ -> assert false + +let compute_proof_name = function + | Some (loc,id) -> + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + user_err_loc (loc,"",pr_id id ++ str " already exists"); + id + | None -> + next_global_ident_away false (id_of_string "Unnamed_thm") + (Pfedit.get_all_proof_names ()) + +let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = + match body with + | None -> + (match local with + | Local -> + let impl=false and keep=false in (* copy values from Vernacentries *) + let k = IsAssumption Conjectural in + let c = SectionLocalAssum (t_i,impl,keep) in + let _ = declare_variable id (Lib.cwd(),c,k) in + (Local,VarRef id,imps) + | Global -> + let k = IsAssumption Conjectural in + let kn = declare_constant id (ParameterEntry (t_i,false), k) in + (Global,ConstRef kn,imps)) + | Some body -> + let k = logical_kind_of_goal_kind kind in + let body_i = match kind_of_term body with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | _ -> anomaly "Not a proof by induction" in + match local with + | Local -> + let c = SectionLocalDef (body_i, Some t_i, opaq) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local,VarRef id,imps) + | Global -> + let const = + { const_entry_body = body_i; + const_entry_type = Some t_i; + const_entry_opaque = opaq; + const_entry_boxed = false (* copy of what cook_proof does *)} in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global,ConstRef kn,imps) + +let look_for_mutual_statements thms = + if List.tl thms <> [] then + (* More than one statement: we look for a common inductive hyp or a *) + (* common coinductive conclusion *) + let n = List.length thms in + let inds = List.map (fun (id,(t,_) as x) -> + let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in + let whnf_hyp_hds = map_rel_context_with_binders + (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c))) + hyps in + let ind_hyps = + List.filter ((<>) None) (list_map_i (fun i (_,b,t) -> + match kind_of_term t with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_ntypes = n & mind.mind_finite & b = None -> + Some (ind,x,i) + | _ -> + None) 1 whnf_hyp_hds) in + let ind_ccl = + let cclenv = push_rel_context hyps (Global.env()) in + let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in + match kind_of_term whnf_ccl with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_ntypes = n & not mind.mind_finite -> + Some (ind,x,0) + | _ -> + None in + ind_hyps,ind_ccl) thms in + let inds_hyps,ind_ccls = List.split inds in + let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in + let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in + (* Check if all conclusions are coinductive in the same type *) + let same_indccl = + match ind_ccls with + | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest + -> Some (x :: List.map Option.get rest) + | _ -> None in + (* Check if some hypotheses are inductive in the same type *) + let common_same_indhyp = + let rec find_same_ind inds = + match inds with + | []::_ -> + [] + | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms -> + let others' = List.map (List.filter (is_same_ind kn)) other_thms in + (x,others')::find_same_ind (hyps_thms1::other_thms) + | (None::hyps_thm1)::other_thms -> + find_same_ind (hyps_thm1::other_thms) + | [] -> + assert false in + find_same_ind inds_hyps in + let common_inds,finite = + match same_indccl, common_same_indhyp with + | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest -> + (* One occurrence of common inductive hyps and no common coind ccls *) + Option.get x::List.map (fun x -> Option.get (List.hd x)) rest, + false + | Some indccl, [] -> + (* One occurrence of common coind ccls and no common inductive hyps *) + indccl, true + | _ -> + error + ("Cannot find a common mutual inductive premise or coinductive" ^ + " conclusion in the statements") in + let ordered_inds = List.sort compare_kn common_inds in + list_iter_i (fun i' ((kn,i),_,_) -> + if i <> i' then + error + ("Cannot find distinct (co)inductive types of the same family" ^ + "of mutual (co)inductive types")) + ordered_inds; + let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in + let rec_tac = + if finite then + match List.map (fun (id,(t,_)) -> (id,t)) thms with + | (id,_)::l -> Hiddentac.h_mutual_cofix true id l + | _ -> assert false + else + match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l + | _ -> assert false in + Some rec_tac,thms + else + None, thms + +(* 4.2| General support for goals *) + +let start_proof_com kind thms hook = + let thms = List.map (fun (sopt,(bl,t)) -> + (compute_proof_name sopt, + interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl))) + thms in + let rec_tac,thms = look_for_mutual_statements thms in + match thms with + | [] -> anomaly "No proof to start" + | (id,(t,imps))::other_thms -> + let hook strength ref = + let other_thms_data = + if other_thms = [] then [] else + (* there are several theorems defined mutually *) + let body,opaq = retrieve_first_recthm ref in + list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in + let thms_data = (strength,ref,imps)::other_thms_data in + List.iter (fun (strength,ref,imps) -> + maybe_declare_manual_implicits false ref (is_implicit_args ()) imps; + hook strength ref) thms_data in + start_proof id kind t ?init_tac:rec_tac hook let check_anonymity id save_ident = if atompart_of_id id <> "Unnamed_thm" then @@ -767,13 +1213,13 @@ let check_anonymity id save_ident = *) let save_anonymous opacity save_ident = - let id,(const,persistence,hook) = Pfedit.cook_proof () in + let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; save save_ident const persistence hook let save_anonymous_with_strength kind opacity save_ident = - let id,(const,_,hook) = Pfedit.cook_proof () in + let id,(const,_,hook) = Pfedit.cook_proof !save_hook in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) @@ -786,7 +1232,7 @@ let admit () = error "Only statements declared as conjecture can be admitted"; *) let kn = - declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in + declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) @@ -795,3 +1241,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/command.mli b/toplevel/command.mli index d15e90cb..26526a5f 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 10067 2007-08-09 17:13:16Z msozeau $ i*) +(*i $Id: command.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) (*i*) open Util @@ -30,28 +30,74 @@ open Redexpr functions of [Declare]; they return an absolute reference to the defined object *) +val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit) +val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit + +val definition_message : identifier -> unit +val assumption_message : identifier -> unit + val declare_definition : identifier -> definition_kind -> local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> declaration_hook -> unit + constr_expr option -> declaration_hook -> unit -val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit +val syntax_definition : identifier -> identifier list * constr_expr -> + bool -> bool -> unit -val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> - Names.variable located -> unit +val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> + Impargs.manual_explicitation list -> + bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit + +val set_declare_assumption_hook : (types -> unit) -> unit val declare_assumption : identifier located list -> - coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit + coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> + bool -> bool -> bool -> unit + +val declare_interning_data : 'a * Constrintern.implicits_env -> + string * Topconstr.constr_expr * Topconstr.scope_name option -> unit + + +val compute_interning_datas : Environ.env -> + 'a list -> + 'b list -> + Term.types list -> + Impargs.manual_explicitation list list -> + 'a list * + ('b * + (Names.identifier list * Impargs.implicits_list * + Topconstr.scope_name option list)) + list val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : - bool -> Entries.mutual_inductive_entry -> mutual_inductive + bool -> Entries.mutual_inductive_entry -> + (Impargs.manual_explicitation list * + Impargs.manual_explicitation list list) list -> + mutual_inductive -val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit +type fixpoint_kind = + | IsFixpoint of (identifier located option * recursion_order_expr) list + | IsCoFixpoint -val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit +type fixpoint_expr = { + fix_name : identifier; + fix_binders : local_binder list; + fix_body : constr_expr; + fix_type : constr_expr +} -val build_scheme : (identifier located * bool * reference * rawsort) list -> unit +val recursive_message : Decl_kinds.definition_object_kind -> + int array option -> Names.identifier list -> Pp.std_ppcmds + +val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier -> + constr -> types -> Impargs.manual_explicitation list -> global_reference + +val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit + +val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit + +val build_scheme : (identifier located option * scheme ) list -> unit val build_combined_scheme : identifier located -> identifier located list -> unit @@ -59,11 +105,18 @@ val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val start_proof : identifier -> goal_kind -> constr -> +(* A hook start_proof calls on the type of the definition being started *) +val set_start_hook : (types -> unit) -> unit + +val start_proof : identifier -> goal_kind -> types -> + ?init_tac:Proof_type.tactic -> declaration_hook -> unit + +val start_proof_com : goal_kind -> + (lident option * (local_binder list * constr_expr)) list -> declaration_hook -> unit -val start_proof_com : identifier option -> goal_kind -> - (local_binder list * constr_expr) -> declaration_hook -> unit +(* A hook the next three functions pass to cook_proof *) +val set_save_hook : (Refiner.pftreestate -> unit) -> unit (*s [save_named b] saves the current completed proof under the name it was started; boolean [b] tells if the theorem is declared opaque; it diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 44b2e231..884589e7 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: coqinit.ml 10901 2008-05-07 18:53:48Z letouzey $ *) open Pp open System @@ -14,7 +14,7 @@ open Toplevel let (/) = Filename.concat -let set_debug () = Options.debug := true +let set_debug () = Flags.debug := true (* Loading of the ressource file. rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one @@ -41,7 +41,7 @@ let load_rcfile() = Vernac.load_vernac false !rcfile else () (* - Options.if_verbose + Flags.if_verbose mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) @@ -49,13 +49,14 @@ let load_rcfile() = (msgnl (str"Load of rcfile failed."); raise e) else - Options.if_verbose msgnl (str"Skipping rcfile loading.") + Flags.if_verbose msgnl (str"Skipping rcfile loading.") let add_ml_include s = Mltop.add_ml_dir s (* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path s = Mltop.add_path s (Names.make_dirpath [Nameops.coq_root]) +let coq_add_path d s = + Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) let coq_add_rec_path s = Mltop.add_rec_path s (Names.make_dirpath [Nameops.coq_root]) (* By the option -include -I or -R of the command line *) @@ -68,32 +69,61 @@ let hm2 s = let n = String.length s in if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s +(* The list of all theories in the standard library /!\ order does matter *) +let theories_dirs_map = [ + "theories/Unicode", "Unicode" ; + "theories/Classes", "Classes" ; + "theories/Program", "Program" ; + "theories/FSets", "FSets" ; + "theories/Reals", "Reals" ; + "theories/Strings", "Strings" ; + "theories/Sorting", "Sorting" ; + "theories/Setoids", "Setoids" ; + "theories/Sets", "Sets" ; + "theories/Lists", "Lists" ; + "theories/Wellfounded", "Wellfounded" ; + "theories/Relations", "Relations" ; + "theories/Numbers", "Numbers" ; + "theories/QArith", "QArith" ; + "theories/NArith", "NArith" ; + "theories/ZArith", "ZArith" ; + "theories/Arith", "Arith" ; + "theories/Bool", "Bool" ; + "theories/Logic", "Logic" ; + "theories/Init", "Init" + ] + (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = - (* developper specific directories to open *) - let dev = if Coq_config.local then [ "dev" ] else [] in let coqlib = (* variable COQLIB overrides the default library *) getenv_else "COQLIB" - (if Coq_config.local || !Options.boot then Coq_config.coqtop - else Coq_config.coqlib) in - (* first user-contrib *) + (if Coq_config.local || !Flags.boot then Coq_config.coqtop + else Coq_config.coqlib) in let user_contrib = coqlib/"user-contrib" in - if Sys.file_exists user_contrib then - Mltop.add_rec_path user_contrib Nameops.default_root_prefix; - (* then standard library *) - let vdirs = [ "theories"; "contrib" ] in - let dirs = "states" :: dev @ vdirs in - List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; + let dirs = "states" :: ["contrib"] in let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in - add_ml_include camlp4; - (* then current directory *) - Mltop.add_path "." Nameops.default_root_prefix; - (* additional loadpath, given with -I -include -R options *) - List.iter - (fun (s,alias,reci) -> - if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) - (List.rev !includes) + (* first user-contrib *) + if Sys.file_exists user_contrib then + Mltop.add_rec_path user_contrib Nameops.default_root_prefix; + (* then states, contrib and dev *) + List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; + (* developer specific directory to open *) + if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + (* then standard library *) + List.iter + (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) + theories_dirs_map; + (* then camlp4lib *) + add_ml_include camlp4; + (* then current directory *) + Mltop.add_path "." Nameops.default_root_prefix; + (* additional loadpath, given with -I -include -R options *) + List.iter + (fun (s,alias,reci) -> + if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) + (List.rev !includes) + let init_library_roots () = includes := [] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 3374b0ee..e6d2deec 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqtop.ml 9191 2006-09-29 15:45:42Z courtieu $ *) +(* $Id: coqtop.ml 11062 2008-06-06 14:19:50Z notin $ *) open Pp open Util open System -open Options +open Flags open Names open Libnames open Nameops @@ -32,6 +32,8 @@ let print_header () = Printf.printf "Welcome to Coq %s (%s)\n" ver rev; flush stdout +let output_context = ref false + let memory_stat = ref false let print_memory_stat () = @@ -81,7 +83,7 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> - if Options.do_translate () then + if Flags.do_translate () then with_option translate_file (Vernac.load_vernac b) s else Vernac.load_vernac b s) @@ -102,7 +104,7 @@ let require () = let compile_list = ref ([] : (bool * string) list) let add_compile verbose s = set_batch_mode (); - Options.make_silent true; + Flags.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in @@ -111,7 +113,7 @@ let compile_files () = (fun (v,f) -> States.unfreeze init_state; Constrintern.coqdoc_unfreeze coqdoc_init_state; - if Options.do_translate () then + if Flags.do_translate () then with_option translate_file (Vernac.compile v) f else Vernac.compile v f) @@ -129,6 +131,11 @@ let set_opt () = re_exec_version := "opt" let re_exec is_ide = let s = !re_exec_version in let is_native = (Mltop.get()) = Mltop.Native in + (* Unix.readlink is not implemented on Windows architectures :-( + let prog = + try Unix.readlink "/proc/self/exe" + with Unix.Unix_error _ -> Sys.argv.(0) in + *) let prog = Sys.argv.(0) in if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin @@ -151,7 +158,7 @@ let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); - Options.set_boxed_definitions !boxed_def; + Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm (*s Parsing of the command line. @@ -236,7 +243,7 @@ let parse_args is_ide = | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem | "-compile-verbose" :: [] -> usage () - | "-dont-load-proofs" :: rem -> Options.dont_load_proofs := true; parse rem + | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem | "-translate" :: rem -> make_translate true; parse rem @@ -246,13 +253,15 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Options.print_emacs := true; - Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem - + | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> Flags.print_emacs := true; + Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem + + | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem + | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 - | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem + | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -270,13 +279,15 @@ let parse_args is_ide = | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem - | "-xml" :: rem -> Options.xml_export := true; parse rem + | "-xml" :: rem -> Flags.xml_export := true; parse rem + + | "-output-context" :: rem -> output_context := true; parse rem - (* Scanned in Options! *) + (* Scanned in Flags. *) | "-v7" :: rem -> error "This version of Coq does not support v7 syntax" | "-v8" :: rem -> parse rem - | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem + | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem | s :: rem -> if is_ide then begin @@ -297,15 +308,10 @@ let parse_args is_ide = end | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end - -(* To prevent from doing the initialization twice *) -let initialized = ref false - let init is_ide = - if not !initialized then begin - initialized := true; - Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - Lib.init(); + Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + Lib.init(); + begin try parse_args is_ide; re_exec is_ide; @@ -315,21 +321,26 @@ let init is_ide = set_vm_opt (); engage (); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then - option_iter Declaremods.start_library !toplevel_name; + Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); load_rcfile(); load_vernacular (); compile_files (); - outputstate (); + outputstate () with e -> flush_all(); - if not !batch_mode then message "Error during initialization :"; + if not !batch_mode then message "Error during initialization:"; msgnl (Toplevel.print_toplevel_error e); exit 1 end; - if !batch_mode then (flush_all(); Profile.print_profile (); exit 0); + if !batch_mode then + (flush_all(); + if !output_context then + Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); + Profile.print_profile (); + exit 0); Lib.declare_initial_state () let init_ide () = init true; List.rev !ide_args diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 63a6ad07..ae9a243f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: discharge.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: discharge.ml 10861 2008-04-28 08:19:14Z herbelin $ *) open Names open Util @@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (Global.env()) (mib,mip))) in + let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1809baa5..579acffa 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: himsg.ml 11150 2008-06-19 11:38:27Z msozeau $ *) open Pp open Util -open Options +open Flags open Names open Nameops open Term @@ -21,6 +21,7 @@ open Sign open Environ open Pretype_errors open Type_errors +open Typeclasses_errors open Indrec open Reduction open Cases @@ -29,51 +30,45 @@ open Printer open Rawterm open Evd -let quote s = h 0 (str "\"" ++ s ++ str "\"") - let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) -let nth i = - let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in - int i ++ str many - -let pr_db ctx i = +let pr_db env i = try - match lookup_rel i ctx with + match lookup_rel i env with Name id, _, _ -> pr_id id - | Anonymous, _, _ -> str"<>" - with Not_found -> str"UNBOUND_REL_"++int i + | Anonymous, _, _ -> str "<>" + with Not_found -> str "UNBOUND_REL_" ++ int i -let explain_unbound_rel ctx n = - let pe = pr_ne_context_of (str "In environment") ctx in - str"Unbound reference: " ++ pe ++ - str"The reference " ++ int n ++ str " is free" +let explain_unbound_rel env n = + let pe = pr_ne_context_of (str "In environment") env in + str "Unbound reference: " ++ pe ++ + str "The reference " ++ int n ++ str " is free." -let explain_unbound_var ctx v = +let explain_unbound_var env v = let var = pr_id v in - str"No such section variable or assumption : " ++ var - -let explain_not_type ctx j = - let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = pr_ljudge_env ctx j in - pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++ - str"has type" ++ spc () ++ pt ++ spc () ++ - str"which should be Set, Prop or Type." - -let explain_bad_assumption ctx j = - let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = pr_ljudge_env ctx j in - pe ++ str "cannot declare a variable or hypothesis over the term" ++ - brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++ + str "No such section variable or assumption: " ++ var ++ str "." + +let explain_not_type env j = + let pe = pr_ne_context_of (str "In environment") env in + let pc,pt = pr_ljudge_env env j in + pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ spc () ++ pt ++ spc () ++ + str "which should be Set, Prop or Type." + +let explain_bad_assumption env j = + let pe = pr_ne_context_of (str "In environment") env in + let pc,pt = pr_ljudge_env env j in + pe ++ str "Cannot declare a variable or hypothesis over the term" ++ + brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." let explain_reference_variables c = let pc = pr_lconstr c in - str "the constant" ++ spc () ++ pc ++ spc () ++ - str "refers to variables which are not in the context" + str "The constant" ++ spc () ++ pc ++ spc () ++ + str "refers to variables which are not in the context." let rec pr_disjunction pr = function | [a] -> pr a @@ -81,10 +76,10 @@ let rec pr_disjunction pr = function | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l | [] -> assert false -let explain_elim_arity ctx ind sorts c pj okinds = - let ctx = make_all_name_different ctx in - let pi = pr_inductive ctx ind in - let pc = pr_lconstr_env ctx c in +let explain_elim_arity env ind sorts c pj okinds = + let env = make_all_name_different env in + let pi = pr_inductive env ind in + let pc = pr_lconstr_env env c in let msg = match okinds with | Some(kp,ki,explanation) -> let pki = pr_sort_family ki in @@ -93,144 +88,137 @@ let explain_elim_arity ctx ind sorts c pj okinds = | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" | StrongEliminationOnNonSmallType -> - "strong elimination on non-small inductive types leads to paradoxes." + "strong elimination on non-small inductive types leads to paradoxes" | WrongArity -> "wrong arity" in let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in - let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in - hov 0 - (str "the return type has sort" ++ spc() ++ ppt ++ spc() ++ - str "while it" ++ spc() ++ str "should be " ++ ppar ++ str ".") ++ - fnl() ++ + let ppt = pr_lconstr_env env (snd (decompose_prod_assum pj.uj_type)) in + hov 0 + (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++ + str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++ + fnl () ++ hov 0 (str "Elimination of an inductive object of sort " ++ pki ++ brk(1,0) ++ - str "is not allowed on a predicate in sort " ++ pkp ++ fnl() ++ - str "because" ++ spc() ++ str explanation ++ str ".") - | None -> + str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++ + str "because" ++ spc () ++ str explanation ++ str ".") + | None -> str "ill-formed elimination predicate." in hov 0 ( - str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++ - str "in the inductive type" ++ spc() ++ quote pi ++ str":") ++ + str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++ + str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ fnl () ++ msg -let explain_case_not_inductive ctx cj = - let ctx = make_all_name_different ctx in - let pc = pr_lconstr_env ctx cj.uj_val in - let pct = pr_lconstr_env ctx cj.uj_type in +let explain_case_not_inductive env cj = + let env = make_all_name_different env in + let pc = pr_lconstr_env env cj.uj_val in + let pct = pr_lconstr_env env cj.uj_type in match kind_of_term cj.uj_type with - | Evar _ -> - str "Cannot infer a type for this expression" + | Evar _ -> + str "Cannot infer a type for this expression." | _ -> - str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ spc () ++ - str "which is not a (co-)inductive type" - -let explain_number_branches ctx cj expn = - let ctx = make_all_name_different ctx in - let pc = pr_lconstr_env ctx cj.uj_val in - let pct = pr_lconstr_env ctx cj.uj_type in - str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ + str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ brk(1,1) ++ pct ++ spc () ++ + str "which is not a (co-)inductive type." + +let explain_number_branches env cj expn = + let env = make_all_name_different env in + let pc = pr_lconstr_env env cj.uj_val in + let pct = pr_lconstr_env env cj.uj_type in + str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ brk(1,1) ++ pct ++ spc () ++ - str "expects " ++ int expn ++ str " branches" + str "expects " ++ int expn ++ str " branches." -let ordinal n = - let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in - string_of_int n ^ s - -let explain_ill_formed_branch ctx c i actty expty = - let ctx = make_all_name_different ctx in - let pc = pr_lconstr_env ctx c in - let pa = pr_lconstr_env ctx actty in - let pe = pr_lconstr_env ctx expty in +let explain_ill_formed_branch env c i actty expty = + let env = make_all_name_different env in + let pc = pr_lconstr_env env c in + let pa = pr_lconstr_env env actty in + let pe = pr_lconstr_env env expty in str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ - str "which should be" ++ brk(1,1) ++ pe - -let explain_generalization ctx (name,var) j = - let pe = pr_ne_context_of (str "In environment") ctx in - let pv = pr_ltype_env ctx var in - let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in - str"Illegal generalization: " ++ pe ++ - str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ - str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++ - str"it has type" ++ spc () ++ pt ++ - spc () ++ str"which should be Set, Prop or Type." - -let explain_actual_type ctx j pt = - let pe = pr_ne_context_of (str "In environment") ctx in - let (pc,pct) = pr_ljudge_env ctx j in - let pt = pr_lconstr_env ctx pt in + spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ + brk(1,1) ++ pa ++ spc () ++ + str "which should be" ++ brk(1,1) ++ pe ++ str "." + +let explain_generalization env (name,var) j = + let pe = pr_ne_context_of (str "In environment") env in + let pv = pr_ltype_env env var in + let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) j in + pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ + str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++ + str "it has type" ++ spc () ++ pt ++ + spc () ++ str "which should be Set, Prop or Type." + +let explain_actual_type env j pt = + let pe = pr_ne_context_of (str "In environment") env in + let (pc,pct) = pr_ljudge_env env j in + let pt = pr_lconstr_env env pt in pe ++ - str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ - str "while it is expected to have type" ++ brk(1,1) ++ pt - -let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = - let ctx = make_all_name_different ctx in - let randl = Array.to_list randl in -(* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr,prt = pr_ljudge_env ctx rator in - let term_string1,term_string2 = - if List.length randl > 1 then - str "terms", (str"The "++nth n++str" term") - else - str "term", str "This term" in - let appl = prlist_with_sep pr_fnl + str "The term" ++ brk(1,1) ++ pc ++ spc () ++ + str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ + str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." + +let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = + let env = make_all_name_different env in + let nargs = Array.length randl in +(* let pe = pr_ne_context_of (str "in environment") env in*) + let pr,prt = pr_ljudge_env env rator in + let term_string1 = str (plural nargs "term") in + let term_string2 = + if nargs>1 then str "The " ++ nth n ++ str " term" else str "This term" in + let appl = prvect_with_sep pr_fnl (fun c -> - let pc,pct = pr_ljudge_env ctx c in - hov 2 (pc ++ spc () ++ str": " ++ pct)) randl + let pc,pct = pr_ljudge_env env c in + hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in - str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ - str"The term" ++ brk(1,1) ++ pr ++ spc () ++ - str"of type" ++ brk(1,1) ++ prt ++ spc () ++ - str"cannot be applied to the " ++ term_string1 ++ fnl () ++ - str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++ - brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++ - str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp - -let explain_cant_apply_not_functional ctx rator randl = - let ctx = make_all_name_different ctx in - let randl = Array.to_list randl in -(* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr = pr_lconstr_env ctx rator.uj_val in - let prt = pr_lconstr_env ctx rator.uj_type in - let term_string = if List.length randl > 1 then "terms" else "term" in - let appl = prlist_with_sep pr_fnl + str "Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ + str "The term" ++ brk(1,1) ++ pr ++ spc () ++ + str "of type" ++ brk(1,1) ++ prt ++ spc () ++ + str "cannot be applied to the " ++ term_string1 ++ fnl () ++ + str " " ++ v 0 appl ++ fnl () ++ term_string2 ++ str " has type" ++ + brk(1,1) ++ pr_lconstr_env env actualtyp ++ spc () ++ + str "which should be coercible to" ++ brk(1,1) ++ + pr_lconstr_env env exptyp ++ str "." + +let explain_cant_apply_not_functional env rator randl = + let env = make_all_name_different env in + let nargs = Array.length randl in +(* let pe = pr_ne_context_of (str "in environment") env in*) + let pr = pr_lconstr_env env rator.uj_val in + let prt = pr_lconstr_env env rator.uj_type in + let appl = prvect_with_sep pr_fnl (fun c -> - let pc = pr_lconstr_env ctx c.uj_val in - let pct = pr_lconstr_env ctx c.uj_type in - hov 2 (pc ++ spc () ++ str": " ++ pct)) randl + let pc = pr_lconstr_env env c.uj_val in + let pct = pr_lconstr_env env c.uj_type in + hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl in - str"Illegal application (Non-functional construction): " ++ + str "Illegal application (Non-functional construction): " ++ (* pe ++ *) fnl () ++ - str"The expression" ++ brk(1,1) ++ pr ++ spc () ++ - str"of type" ++ brk(1,1) ++ prt ++ spc () ++ - str("cannot be applied to the "^term_string) ++ fnl () ++ - str" " ++ v 0 appl - -let explain_unexpected_type ctx actual_type expected_type = - let pract = pr_lconstr_env ctx actual_type in - let prexp = pr_lconstr_env ctx expected_type in - str"This type is" ++ spc () ++ pract ++ spc () ++ + str "The expression" ++ brk(1,1) ++ pr ++ spc () ++ + str "of type" ++ brk(1,1) ++ prt ++ spc () ++ + str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++ + str " " ++ v 0 appl + +let explain_unexpected_type env actual_type expected_type = + let pract = pr_lconstr_env env actual_type in + let prexp = pr_lconstr_env env expected_type in + str "This type is" ++ spc () ++ pract ++ spc () ++ str "but is expected to be" ++ - spc () ++ prexp + spc () ++ prexp ++ str "." -let explain_not_product ctx c = - let pr = pr_lconstr_env ctx c in - str"The type of this term is a product," ++ spc () ++ - str"while it is expected to be" ++ - if is_Type c then str " a sort" else (brk(1,1) ++ pr) +let explain_not_product env c = + let pr = pr_lconstr_env env c in + str "The type of this term is a product" ++ spc () ++ + str "while it is expected to be" ++ + (if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) -let explain_ill_formed_rec_body ctx err names i = +let explain_ill_formed_rec_body env err names i fixenv vdefj = let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id - | Anonymous -> str"The " ++ nth i ++ str" definition" in + | Anonymous -> str "The " ++ nth i ++ str " definition" in let st = match err with @@ -238,277 +226,359 @@ let explain_ill_formed_rec_body ctx err names i = | NotEnoughAbstractionInFixBody -> str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> - str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++ + str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" | RecursionOnIllegalTerm(j,arg,le,lt) -> let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str"the " ++ nth i ++ str" definition" in + | Anonymous -> str "the " ++ nth i ++ str " definition" in let vars = match (lt,le) with - ([],[]) -> mt() + ([],[]) -> assert false | ([],[x]) -> - str "a subterm of " ++ pr_db ctx x + str "a subterm of " ++ pr_db env x | ([],_) -> str "a subterm of the following variables: " ++ - prlist_with_sep pr_spc (pr_db ctx) le - | ([x],_) -> pr_db ctx x + prlist_with_sep pr_spc (pr_db env) le + | ([x],_) -> pr_db env x | _ -> str "one of the following variables: " ++ - prlist_with_sep pr_spc (pr_db ctx) lt in - str "Recursive call to " ++ called ++ spc() ++ - str "has principal argument equal to" ++ spc() ++ - pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars + prlist_with_sep pr_spc (pr_db env) lt in + str "Recursive call to " ++ called ++ spc () ++ + str "has principal argument equal to" ++ spc () ++ + pr_lconstr_env env arg ++ fnl () ++ str "instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str"the " ++ nth i ++ str" definition" in - str "Recursive call to " ++ called ++ str " had not enough arguments" + | Anonymous -> str "the " ++ nth i ++ str " definition" in + str "Recursive call to " ++ called ++ str " has not enough arguments" (* CoFixpoint guard errors *) | CodomainNotInductiveType c -> - str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++ + str "The codomain is" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be a coinductive type" | NestedRecursiveOccurrences -> - str "nested recursive occurrences" + str "Nested recursive occurrences" | UnguardedRecursiveCall c -> - str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c + str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env c | RecCallInTypeOfAbstraction c -> - str "recursive call forbidden in the domain of an abstraction:" ++ - spc() ++ pr_lconstr_env ctx c + str "Recursive call forbidden in the domain of an abstraction:" ++ + spc () ++ pr_lconstr_env env c | RecCallInNonRecArgOfConstructor c -> - str "recursive call on a non-recursive argument of constructor" ++ - spc() ++ pr_lconstr_env ctx c + str "Recursive call on a non-recursive argument of constructor" ++ + spc () ++ pr_lconstr_env env c | RecCallInTypeOfDef c -> - str "recursive call forbidden in the type of a recursive definition" ++ - spc() ++ pr_lconstr_env ctx c + str "Recursive call forbidden in the type of a recursive definition" ++ + spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c - | RecCallInCaseArg c -> - str "recursive call in the argument of cases in" ++ spc() ++ - pr_lconstr_env ctx c + str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + | RecCallInCaseArg c -> + str "Recursive call in the argument of cases in" ++ spc () ++ + pr_lconstr_env env c | RecCallInCasePred c -> - str "recursive call in the type of cases in" ++ spc() ++ - pr_lconstr_env ctx c + str "Recursive call in the type of cases in" ++ spc () ++ + pr_lconstr_env env c | NotGuardedForm c -> - str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++ - str "not in guarded form" ++ spc()++ - str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)" + str "Sub-expression " ++ pr_lconstr_env env c ++ + strbrk " not in guarded form (should be a constructor," ++ + strbrk " an abstraction, a match, a cofix or a recursive call)" in - prt_name i ++ str" is ill-formed." ++ fnl() ++ - pr_ne_context_of (str "In environment") ctx ++ - st - -let explain_ill_typed_rec_body ctx i names vdefj vargs = - let ctx = make_all_name_different ctx in - let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in - let pv = pr_lconstr_env ctx vargs.(i) in - str"The " ++ - (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++ - str"recursive definition" ++ spc () ++ pvd ++ spc () ++ - str "has type" ++ spc () ++ pvdt ++spc () ++ - str "it should be" ++ spc () ++ pv -(* -let explain_not_inductive ctx c = - let ctx = make_all_name_different ctx in - let pc = pr_lconstr_env ctx c in - str"The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "is not an inductive definition" -*) -let explain_cant_find_case_type ctx c = - let ctx = make_all_name_different ctx in - let pe = pr_lconstr_env ctx c in - hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe) - -let explain_occur_check ctx ev rhs = - let ctx = make_all_name_different ctx in + prt_name i ++ str " is ill-formed." ++ fnl () ++ + pr_ne_context_of (str "In environment") env ++ + st ++ str "." + +let explain_ill_typed_rec_body env i names vdefj vargs = + let env = make_all_name_different env in + let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in + let pv = pr_lconstr_env env vargs.(i) in + str "The " ++ + (if Array.length vdefj = 1 then mt () else nth (i+1) ++ spc ()) ++ + str "recursive definition" ++ spc () ++ pvd ++ spc () ++ + str "has type" ++ spc () ++ pvdt ++ spc () ++ + str "while it should be" ++ spc () ++ pv ++ str "." + +let explain_cant_find_case_type env c = + let env = make_all_name_different env in + let pe = pr_lconstr_env env c in + str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." + +let explain_occur_check env ev rhs = + let env = make_all_name_different env in let id = Evd.string_of_existential ev in - let pt = pr_lconstr_env ctx rhs in - str"Occur check failed: tried to define " ++ str id ++ - str" with term" ++ brk(1,1) ++ pt + let pt = pr_lconstr_env env rhs in + str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++ + pt ++ spc () ++ str "that would depend on itself." let explain_hole_kind env = function - | QuestionMark _ -> str "a term for this placeholder" + | QuestionMark _ -> str "this placeholder" | CasesType -> str "the type of this pattern-matching problem" | BinderType (Name id) -> - str "a type for " ++ Nameops.pr_id id + str "the type of " ++ Nameops.pr_id id | BinderType Anonymous -> - str "a type for this anonymous binder" + str "the type of this anonymous binder" | ImplicitArg (c,(n,ido)) -> - let id = out_some ido in - str "an instance for the implicit parameter " ++ + let id = Option.get ido in + str "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c | InternalHole -> - str "a term for an internal placeholder" + str "an internal placeholder" | TomatchTypeParameter (tyi,n) -> - str "the " ++ pr_ord n ++ + str "the " ++ nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ str ") of this term" + | GoalEvar -> + str "an existential variable" + | ImpossibleCase -> + str "the type of an impossible pattern-matching clause" -let explain_not_clean ctx ev t k = - let ctx = make_all_name_different ctx in +let explain_not_clean env ev t k = + let env = make_all_name_different env in let id = Evd.string_of_existential ev in - let var = pr_lconstr_env ctx t in - str"Tried to define " ++ explain_hole_kind ctx k ++ - str" (" ++ str id ++ str ")" ++ spc() ++ - str"with a term using variable " ++ var ++ spc () ++ - str"which is not in its scope." - -let explain_unsolvable_implicit env k = - str "Cannot infer " ++ explain_hole_kind env k - - -let explain_var_not_found ctx id = - str "The variable" ++ spc () ++ str (string_of_id id) ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment" - -let explain_wrong_case_info ctx ind ci = - let pi = pr_lconstr (mkInd ind) in + let var = pr_lconstr_env env t in + str "Tried to instantiate " ++ explain_hole_kind env k ++ + str " (" ++ str id ++ str ")" ++ spc () ++ + str "with a term using variable " ++ var ++ spc () ++ + str "which is not in its scope." + +let explain_unsolvability = function + | None -> mt() + | Some (SeveralInstancesFound n) -> + strbrk " (several distinct possible instances found)" + +let pr_ne_context_of header footer env = + if Environ.rel_context env = empty_rel_context & + Environ.named_context env = empty_named_context then footer + else pr_ne_context_of header env + +let explain_typeclass_resolution env evi k = + match k with + InternalHole | ImplicitArg _ -> + (match Typeclasses.class_of_constr evi.evar_concl with + | Some c -> + let env = Evd.evar_env evi in + fnl () ++ str "Could not find an instance for " ++ + pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env + | None -> mt()) + | _ -> mt() + +let explain_unsolvable_implicit env evi k explain = + str "Cannot infer " ++ explain_hole_kind env k ++ + explain_unsolvability explain ++ str "." ++ + explain_typeclass_resolution env evi k + +let explain_var_not_found env id = + str "The variable" ++ spc () ++ pr_id id ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "." + +let explain_wrong_case_info env ind ci = + let pi = pr_inductive (Global.env()) ind in if ci.ci_ind = ind then - str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++ - spc () ++ str"has invalid information" + str "Pattern-matching expression on an object of inductive type" ++ + spc () ++ pi ++ spc () ++ str "has invalid information." else - let pc = pr_lconstr (mkInd ci.ci_ind) in - str"A term of inductive type" ++ spc () ++ pi ++ spc () ++ - str"was given to a pattern-matching expression on the inductive type" ++ - spc () ++ pc - - -let explain_cannot_unify ctx m n = - let pm = pr_lconstr_env ctx m in - let pn = pr_lconstr_env ctx n in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn + let pc = pr_inductive (Global.env()) ci.ci_ind in + str "A term of inductive type" ++ spc () ++ pi ++ spc () ++ + str "was given to a pattern-matching expression on the inductive type" ++ + spc () ++ pc ++ str "." + +let explain_cannot_unify env m n = + let pm = pr_lconstr_env env m in + let pn = pr_lconstr_env env n in + str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str "with" ++ brk(1,1) ++ pn let explain_cannot_unify_local env m n subn = - let pm = pr_lconstr_env env m in + let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in let psubn = pr_lconstr_env env subn in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ - psubn ++ str" contains local variables" - -let explain_refiner_cannot_generalize ty = - str "Cannot find a well-typed generalisation of the goal with type : " ++ - pr_lconstr ty - -let explain_no_occurrence_found c = - str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal" - -let explain_cannot_unify_binding_type ctx m n = - let pm = pr_lconstr_env ctx m in - let pn = pr_lconstr_env ctx n in - str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ + str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++ + psubn ++ str " contains local variables" + +let explain_refiner_cannot_generalize env ty = + str "Cannot find a well-typed generalisation of the goal with type: " ++ + pr_lconstr_env env ty + +let explain_no_occurrence_found env c id = + str "Found no subterm matching " ++ pr_lconstr_env env c ++ + str " in " ++ + (match id with + | Some id -> pr_id id + | None -> str"the current goal") + +let explain_cannot_unify_binding_type env m n = + let pm = pr_lconstr_env env m in + let pn = pr_lconstr_env env n in + str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn -let explain_type_error ctx err = - let ctx = make_all_name_different ctx in +let explain_cannot_find_well_typed_abstraction env p l = + let la,lc = list_chop (List.length l - 1) l in + str "Abstracting over the " ++ + str (plural (List.length l) "term") ++ spc () ++ + hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++ + (if la<>[] then str " and" ++ spc () else mt()) ++ + pr_lconstr_env env (List.hd lc)) ++ spc () ++ + str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ + str "which is ill-typed" + +let explain_type_error env err = + let env = make_all_name_different env in match err with - | UnboundRel n -> - explain_unbound_rel ctx n - | UnboundVar v -> - explain_unbound_var ctx v - | NotAType j -> - explain_not_type ctx j - | BadAssumption c -> - explain_bad_assumption ctx c - | ReferenceVariables id -> + | UnboundRel n -> + explain_unbound_rel env n + | UnboundVar v -> + explain_unbound_var env v + | NotAType j -> + explain_not_type env j + | BadAssumption c -> + explain_bad_assumption env c + | ReferenceVariables id -> explain_reference_variables id | ElimArity (ind, aritylst, c, pj, okinds) -> - explain_elim_arity ctx ind aritylst c pj okinds - | CaseNotInductive cj -> - explain_case_not_inductive ctx cj - | NumberBranches (cj, n) -> - explain_number_branches ctx cj n - | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch ctx c i actty expty + explain_elim_arity env ind aritylst c pj okinds + | CaseNotInductive cj -> + explain_case_not_inductive env cj + | NumberBranches (cj, n) -> + explain_number_branches env cj n + | IllFormedBranch (c, i, actty, expty) -> + explain_ill_formed_branch env c i actty expty | Generalization (nvar, c) -> - explain_generalization ctx nvar c - | ActualType (j, pt) -> - explain_actual_type ctx j pt + explain_generalization env nvar c + | ActualType (j, pt) -> + explain_actual_type env j pt | CantApplyBadType (t, rator, randl) -> - explain_cant_apply_bad_type ctx t rator randl + explain_cant_apply_bad_type env t rator randl | CantApplyNonFunctional (rator, randl) -> - explain_cant_apply_not_functional ctx rator randl - | IllFormedRecBody (err, lna, i) -> - explain_ill_formed_rec_body ctx err lna i - | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body ctx i lna vdefj vargs + explain_cant_apply_not_functional env rator randl + | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> + explain_ill_formed_rec_body env err lna i fixenv vdefj + | IllTypedRecBody (i, lna, vdefj, vargs) -> + explain_ill_typed_rec_body env i lna vdefj vargs | WrongCaseInfo (ind,ci) -> - explain_wrong_case_info ctx ind ci -(* - | NotInductive c -> - explain_not_inductive ctx c -*) -let explain_pretype_error ctx err = - let ctx = make_all_name_different ctx in - match err with - | CantFindCaseType c -> - explain_cant_find_case_type ctx c - | OccurCheck (n,c) -> - explain_occur_check ctx n c - | NotClean (n,c,k) -> - explain_not_clean ctx n c k - | UnsolvableImplicit k -> - explain_unsolvable_implicit ctx k - | VarNotFound id -> - explain_var_not_found ctx id - | UnexpectedType (actual,expected) -> - explain_unexpected_type ctx actual expected - | NotProduct c -> - explain_not_product ctx c - | CannotUnify (m,n) -> explain_cannot_unify ctx m n - | CannotUnifyLocal (e,m,n,sn) -> explain_cannot_unify_local e m n sn - | CannotGeneralize ty -> explain_refiner_cannot_generalize ty - | NoOccurrenceFound c -> explain_no_occurrence_found c - | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type ctx m n + explain_wrong_case_info env ind ci +let explain_pretype_error env err = + let env = make_all_name_different env in + match err with + | CantFindCaseType c -> explain_cant_find_case_type env c + | OccurCheck (n,c) -> explain_occur_check env n c + | NotClean (n,c,k) -> explain_not_clean env n c k + | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp + | VarNotFound id -> explain_var_not_found env id + | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect + | NotProduct c -> explain_not_product env c + | CannotUnify (m,n) -> explain_cannot_unify env m n + | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn + | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty + | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id + | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n + | CannotFindWellTypedAbstraction (p,l) -> + explain_cannot_find_well_typed_abstraction env p l + + +(* Typeclass errors *) + +let explain_not_a_class env c = + pr_constr_env env c ++ str" is not a declared type class" + +let explain_unbound_method env cid id = + str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ + pr_global cid + +let pr_constr_exprs exprs = + hv 0 (List.fold_right + (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps) + exprs (mt ())) + +let explain_no_instance env (_,id) l = + str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++ + str "applied to arguments" ++ spc () ++ + prlist_with_sep pr_spc (pr_lconstr_env env) l + +let pr_constraints env evm = + let l = Evd.to_list evm in + let (ev, evi) = List.hd l in + if List.for_all (fun (ev', evi') -> + eq_named_context_val evi.evar_hyps evi'.evar_hyps) l + then + let pe = pr_ne_context_of (str "In environment:") (mt ()) + (reset_with_named_context evi.evar_hyps env) in + pe ++ fnl () ++ + prlist_with_sep (fun () -> fnl ()) + (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l + else + pr_evar_map evm + +let explain_unsatisfiable_constraints env evd constr = + let evm = Evd.evars_of evd in + match constr with + | None -> + str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++ + pr_constraints env evm + | Some (evi, k) -> + explain_unsolvable_implicit env evi k None ++ fnl () ++ + if List.length (Evd.to_list evm) > 1 then + str"With the following meta variables:" ++ + fnl() ++ Evd.pr_evar_map evm + else mt () + +let explain_mismatched_contexts env c i j = + str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ + hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ + hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) + +let explain_typeclass_error env err = + match err with + | NotAClass c -> explain_not_a_class env c + | UnboundMethod (cid, id) -> explain_unbound_method env cid id + | NoInstance (id, l) -> explain_no_instance env id l + | UnsatisfiableConstraints (evd, c) -> explain_unsatisfiable_constraints env evd c + | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j + (* Refiner errors *) let explain_refiner_bad_type arg ty conclty = - str"refiner was given an argument" ++ brk(1,1) ++ + str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr arg ++ spc () ++ - str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str"instead of" ++ brk(1,1) ++ pr_lconstr conclty + str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ + str "instead of" ++ brk(1,1) ++ pr_lconstr conclty -let explain_refiner_occur_meta t = - str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++ - spc () ++ str"because there are metavariables, and it is" ++ - spc () ++ str"neither an application nor a Case" - -let explain_refiner_occur_meta_goal t = - str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++ - spc () ++ str"has metavariables in it" +let explain_refiner_unresolved_bindings l = + let l = map_succeed (function Name id -> id | _ -> failwith "") l in + str "Unable to find an instance for the " ++ + str (plural (List.length l) "variable") ++ spc () ++ + prlist_with_sep pr_coma pr_id l let explain_refiner_cannot_apply t harg = - str"in refiner, a term of type " ++ brk(1,1) ++ - pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ + str "In refiner, a term of type " ++ brk(1,1) ++ + pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ pr_lconstr harg let explain_refiner_not_well_typed c = - str"The term " ++ pr_lconstr c ++ str" is not well-typed" + str "The term " ++ pr_lconstr c ++ str " is not well-typed" let explain_intro_needs_product () = - str "Introduction tactics needs products" + str "Introduction tactics needs products." let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++ - spc () ++ pr_id hyp + str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ + str "does not occur in" ++ spc () ++ pr_id hyp ++ str "." let explain_non_linear_proof c = - str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ - spc () ++ str"because a metavariable has several occurrences" + str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ + spc () ++ str "because a metavariable has several occurrences." let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty - | OccurMeta t -> explain_refiner_occur_meta t - | OccurMetaGoal t -> explain_refiner_occur_meta_goal t + | UnresolvedBindings t -> explain_refiner_unresolved_bindings t | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg | NotWellTyped c -> explain_refiner_not_well_typed c | IntroNeedsProduct -> explain_intro_needs_product () @@ -521,48 +591,52 @@ let error_non_strictly_positive env c v = let pc = pr_lconstr_env env c in let pv = pr_lconstr_env env v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ - brk(1,1) ++ pc + brk(1,1) ++ pc ++ str "." let error_ill_formed_inductive env c v = let pc = pr_lconstr_env env c in let pv = pr_lconstr_env env v in str "Not enough arguments applied to the " ++ pv ++ - str " in" ++ brk(1,1) ++ pc + str " in" ++ brk(1,1) ++ pc ++ str "." -let error_ill_formed_constructor env c v = - let pc = pr_lconstr_env env c in +let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env v in - str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ - str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv - -let str_of_nth n = - (string_of_int n)^ - (match n mod 10 with - | 1 -> "st" - | 2 -> "nd" - | 3 -> "rd" - | _ -> "th") + let atomic = (nb_prod c = 0) in + str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ + str "is not valid;" ++ brk(1,1) ++ + strbrk (if atomic then "it must be " else "its conclusion must be ") ++ + pv ++ + (* warning: because of implicit arguments it is difficult to say which + parameters must be explicitly given *) + (if nparams<>0 then + strbrk " applied to its " ++ str (plural nparams "parameter") + else + mt()) ++ + (if nargs<>0 then + str (if nparams<>0 then " and" else " applied") ++ + strbrk " to some " ++ str (plural nargs "argument") + else + mt()) ++ str "." let error_bad_ind_parameters env c n v1 v2 = let pc = pr_lconstr_env_at_top env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in - str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++ - str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc + str "The " ++ nth n ++ str " argument of " ++ pv2 ++ brk(1,1) ++ + str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = - str "The name" ++ spc () ++ pr_id id ++ spc () ++ - str "is used twice is the inductive types definition." + str "The name" ++ spc () ++ pr_id id ++ spc () ++ + str "is used more than once." -let error_same_names_constructors id cid = - str "The constructor name" ++ spc () ++ pr_id cid ++ spc () ++ - str "is used twice is the definition of type" ++ spc () ++ - pr_id id +let error_same_names_constructors id = + str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++ + str "is used more than once." -let error_same_names_overlap idl = - str "The following names" ++ spc () ++ - str "are used both as type names and constructor names:" ++ spc () ++ - prlist_with_sep pr_coma pr_id idl +let error_same_names_overlap idl = + strbrk "The following names are used both as type names and constructor " ++ + str "names:" ++ spc () ++ + prlist_with_sep pr_coma pr_id idl ++ str "." let error_not_an_arity id = str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." @@ -571,29 +645,36 @@ let error_bad_entry () = str "Bad inductive definition." let error_not_allowed_case_analysis dep kind i = - str (if dep then "Dependent" else "Non Dependent") ++ + str (if dep then "Dependent" else "Non dependent") ++ str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++ str "is not allowed for inductive definition: " ++ - pr_inductive (Global.env()) i + pr_inductive (Global.env()) i ++ str "." let error_bad_induction dep indid kind = str (if dep then "Dependent" else "Non dependent") ++ str " induction for type " ++ pr_id indid ++ str " and sort " ++ pr_sort kind ++ spc () ++ - str "is not allowed" + str "is not allowed." -let error_not_mutual_in_scheme () = - str "Induction schemes are concerned only with distinct mutually inductive types" +let error_not_mutual_in_scheme ind ind' = + if ind = ind' then + str "The inductive type " ++ pr_inductive (Global.env()) ind ++ + str "occurs twice." + else + str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ + str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ + str "are not mutually defined." (* Inductive constructions errors *) let explain_inductive_error = function | NonPos (env,c,v) -> error_non_strictly_positive env c v | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v - | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v + | NotConstructor (env,id,c,v,n,m) -> + error_ill_formed_constructor env id c v n m | NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2 | SameNamesTypes id -> error_same_names_types id - | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid + | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () @@ -604,54 +685,54 @@ let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (dep,k,i) -> error_not_allowed_case_analysis dep k i | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind - | NotMutualInScheme -> error_not_mutual_in_scheme () + | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' (* Pattern-matching errors *) -let explain_bad_pattern ctx cstr ty = - let ctx = make_all_name_different ctx in - let pt = pr_lconstr_env ctx ty in - let pc = pr_constructor ctx cstr in - str "Found the constructor " ++ pc ++ brk(1,1) ++ - str "while matching a term of type " ++ pt ++ brk(1,1) ++ - str "which is not an inductive type" - -let explain_bad_constructor ctx cstr ind = - let pi = pr_inductive ctx ind in -(* let pc = pr_constructor ctx cstr in*) - let pt = pr_inductive ctx (inductive_of_constructor cstr) in - str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++ - str "while a constructor of " ++ pi ++ brk(1,1) ++ - str "is expected" +let explain_bad_pattern env cstr ty = + let env = make_all_name_different env in + let pt = pr_lconstr_env env ty in + let pc = pr_constructor env cstr in + str "Found the constructor " ++ pc ++ brk(1,1) ++ + str "while matching a term of type " ++ pt ++ brk(1,1) ++ + str "which is not an inductive type." + +let explain_bad_constructor env cstr ind = + let pi = pr_inductive env ind in +(* let pc = pr_constructor env cstr in*) + let pt = pr_inductive env (inductive_of_constructor cstr) in + str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++ + str "while a constructor of " ++ pi ++ brk(1,1) ++ + str "is expected." let decline_string n s = if n = 0 then "no "^s else if n = 1 then "1 "^s else (string_of_int n^" "^s^"s") -let explain_wrong_numarg_constructor ctx cstr n = - str "The constructor " ++ pr_constructor ctx cstr ++ - str " expects " ++ str (decline_string n "argument") +let explain_wrong_numarg_constructor env cstr n = + str "The constructor " ++ pr_constructor env cstr ++ + str " expects " ++ str (decline_string n "argument") ++ str "." -let explain_wrong_numarg_inductive ctx ind n = - str "The inductive type " ++ pr_inductive ctx ind ++ - str " expects " ++ str (decline_string n "argument") +let explain_wrong_numarg_inductive env ind n = + str "The inductive type " ++ pr_inductive env ind ++ + str " expects " ++ str (decline_string n "argument") ++ str "." -let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity= - let ctx = make_all_name_different ctx in - let pp = pr_lconstr_env ctx pred in +let explain_wrong_predicate_arity env pred nondep_arity dep_arity= + let env = make_all_name_different env in + let pp = pr_lconstr_env env pred in str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ - str "should be of arity" ++ spc () ++ - pr_lconstr_env ctx nondep_arity ++ spc () ++ - str "(for non dependent case) or" ++ - spc () ++ pr_lconstr_env ctx dep_arity ++ spc () ++ str "(for dependent case)." - -let explain_needs_inversion ctx x t = - let ctx = make_all_name_different ctx in - let px = pr_lconstr_env ctx x in - let pt = pr_lconstr_env ctx t in - str "Sorry, I need inversion to compile pattern matching of term " ++ - px ++ str " of type: " ++ pt + str "should be of arity" ++ spc () ++ + pr_lconstr_env env nondep_arity ++ spc () ++ + str "(for non dependent case) or" ++ + spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ str "(for dependent case)." + +let explain_needs_inversion env x t = + let env = make_all_name_different env in + let px = pr_lconstr_env env x in + let pt = pr_lconstr_env env t in + str "Sorry, I need inversion to compile pattern matching on term " ++ + px ++ str " of type: " ++ pt ++ str "." let explain_unused_clause env pats = (* Without localisation @@ -659,24 +740,24 @@ let explain_unused_clause env pats = (str ("Unused clause with pattern"^s) ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")") *) - str "This clause is redundant" + str "This clause is redundant." let explain_non_exhaustive env pats = - let s = if List.length pats > 1 then "s" else "" in - str ("Non exhaustive pattern-matching: no clause found for pattern"^s) ++ + str "Non exhaustive pattern-matching: no clause found for " ++ + str (plural (List.length pats) "pattern") ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) -let explain_cannot_infer_predicate ctx typs = - let ctx = make_all_name_different ctx in +let explain_cannot_infer_predicate env typs = + let env = make_all_name_different env in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in - str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ + str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ in str "Unable to unify the types found in the branches:" ++ spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) let explain_pattern_matching_error env = function - | BadPattern (c,t) -> + | BadPattern (c,t) -> explain_bad_pattern env c t | BadConstructor (c,ind) -> explain_bad_constructor env c ind @@ -697,6 +778,6 @@ let explain_pattern_matching_error env = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> - str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++ - spc() ++ str "is not well typed." ++ fnl () ++ + str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ + spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' e diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 92fcafb7..1b9e38ce 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: himsg.mli 8003 2006-02-07 22:11:50Z herbelin $ i*) +(*i $Id: himsg.mli 10410 2007-12-31 13:11:55Z msozeau $ i*) (*i*) open Pp @@ -15,6 +15,7 @@ open Indtypes open Environ open Type_errors open Pretype_errors +open Typeclasses_errors open Indrec open Cases open Logic @@ -28,6 +29,8 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds val explain_inductive_error : inductive_error -> std_ppcmds +val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds + val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds val explain_refiner_error : refiner_error -> std_ppcmds diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml new file mode 100644 index 00000000..4b97f8b2 --- /dev/null +++ b/toplevel/ind_tables.ml @@ -0,0 +1,102 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !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 00000000..2edb294f --- /dev/null +++ b/toplevel/ind_tables.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 + + + + diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 13f1f1da..fbeaea34 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 10192 2007-10-08 00:33:39Z letouzey $ *) +(* $Id: metasyntax.ml 11121 2008-06-12 21:15:49Z herbelin $ *) open Pp open Util @@ -74,7 +74,7 @@ let (inTacticGrammar, outTacticGrammar) = let cons_production_parameter l = function | VTerm _ -> l - | VNonTerm (_,_,ido) -> option_cons ido l + | VNonTerm (_,_,ido) -> Option.List.cons ido l let rec tactic_notation_key = function | VTerm id :: _ -> id @@ -97,7 +97,7 @@ let add_tactic_notation (n,prods,e) = (**********************************************************************) (* Printing grammar entries *) -let print_grammar univ = function +let print_grammar = function | "constr" | "operconstr" | "binder_constr" -> msgnl (str "Entry constr is"); Gram.Entry.print Pcoq.Constr.constr; @@ -562,7 +562,7 @@ let is_not_small_constr = function let rec define_keywords_aux = function NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l when is_not_small_constr e -> - prerr_endline ("Defining '"^k^"' as keyword"); + message ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); n1 :: Term("",k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l @@ -570,7 +570,7 @@ let rec define_keywords_aux = function let define_keywords = function Term("IDENT",k)::l -> - prerr_endline ("Defining '"^k^"' as keyword"); + message ("Defining '"^k^"' as keyword"); Lexer.add_token("",k); Term("",k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -755,7 +755,7 @@ let find_precedence lev etyps symbols = error "The level of the leftmost non-terminal cannot be changed" | ETIdent | ETBigint | ETReference -> if lev = None then - Options.if_verbose msgnl (str "Setting notation at level 0") + Flags.if_verbose msgnl (str "Setting notation at level 0") else if lev <> Some 0 then error "A notation starting with an atomic expression must be at level 0"; @@ -763,21 +763,21 @@ let find_precedence lev etyps symbols = | ETPattern | ETOther _ -> (* Give a default ? *) if lev = None then error "Need an explicit level" - else out_some lev + else Option.get lev | ETConstrList _ -> assert false (* internally used in grammar only *) with Not_found -> if lev = None then error "A left-recursive notation must have an explicit level" - else out_some lev) + else Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then - (Options.if_verbose msgnl (str "Setting notation at level 0"); 0) - else out_some lev + (Flags.if_verbose msgnl (str "Setting notation at level 0"); 0) + else Option.get lev | _ -> if lev = None then error "Cannot determine the level"; - out_some lev + Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () @@ -839,7 +839,7 @@ let compute_syntax_data (df,modifiers) = (* Registration of notations interpretation *) let load_notation _ (_,(_,scope,pat,onlyparse,_)) = - option_iter Notation.declare_scope scope + Option.iter Notation.declare_scope scope let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin @@ -854,8 +854,8 @@ let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) = - (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf) +let subst_notation (_,subst,(lc,scope,pat,b,ndf)) = + (lc,scope,subst_interpretation subst pat,b,ndf) let classify_notation (_,(local,_,_,_,_ as o)) = if local then Dispose else Substitute o diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 71522567..c3bdadfa 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: metasyntax.mli 9677 2007-02-24 14:17:54Z herbelin $ i*) (*i*) open Util @@ -51,7 +51,7 @@ val add_syntax_extension : (* Print the Camlp4 state of a grammar *) -val print_grammar : string -> string -> unit +val print_grammar : string -> unit (* Removes quotes in a notation *) diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index a3b51a11..e688d50e 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: minicoq.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: minicoq.ml 10346 2007-12-05 21:11:19Z aspiwack $ *) open Pp open Util @@ -54,7 +54,7 @@ let check c = let definition id ty c = let c = globalize [] c in - let ty = option_map (globalize []) ty in + let ty = Option.map (globalize []) ty in let ce = { const_entry_body = c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce (locals()) !env; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 2185d2a0..30cffa34 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -6,11 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mltop.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) +(*i camlp4use: "pa_macro.cmo" i*) +(* WARNING + * camlp4deps will not work for this file unless Makefile system enhanced. + *) + +(* $Id: mltop.ml4 10348 2007-12-06 17:36:14Z aspiwack $ *) open Util open Pp -open Options +open Flags open System open Libobject open Library @@ -99,6 +104,10 @@ let dir_ml_load s = (* TO DO: .cma loading without toplevel *) | WithoutTop -> IFDEF Byte THEN + (* WARNING + * if this code section starts to use a module not used elsewhere + * in this file, the Makefile dependency logic needs to be updated. + *) let _,gname = where_in_path !coq_mlpath_copy s in try Dynlink.loadfile gname; diff --git a/toplevel/record.ml b/toplevel/record.ml index ab430d0c..5629bb71 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: record.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: record.ml 11024 2008-05-30 12:41:39Z msozeau $ *) open Pp open Util @@ -41,15 +41,17 @@ let interp_decl sigma env = function let j = interp_constr_judgment Evd.empty env c in (id,Some j.uj_val, refresh_universes j.uj_type) -let typecheck_params_and_fields ps fs = +let typecheck_params_and_fields id t ps fs = let env0 = Global.env () in - let env1,newps = interp_context Evd.empty env0 ps in + let (env1,newps), _ = interp_context Evd.empty env0 ps in + let fullarity = it_mkProd_or_LetIn t newps in + let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,newfs = List.fold_left (fun (env,newfs) d -> let decl = interp_decl Evd.empty env d in (push_rel decl env, decl::newfs)) - (env1,[]) fs + (env_ar,[]) fs in newps, newfs @@ -75,20 +77,20 @@ let warning_or_error coe indsp err = | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> - (str (string_of_id fi) ++ + (pr_id fi ++ str" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ str " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> - (str (string_of_id fi) ++ + (pr_id fi ++ str" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ str " is not.") | _ -> - (str " cannot be defined because it is not typable") + (pr_id fi ++ str " cannot be defined because it is not typable") in if coe then errorlabstrm "structure" st; - Options.if_verbose ppnl (hov 0 (str"Warning: " ++ st)) + Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st)) type field_status = | NoProjection of name @@ -124,15 +126,20 @@ let subst_projection fid l c = raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' +let instantiate_possibly_recursive_type indsp paramdecls fields = + let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in + substl_rel_context (subst@[mkInd indsp]) fields + (* We build projections *) -let declare_projections indsp coers fields = +let declare_projections indsp ?(kind=StructureComponent) ?name coers fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let paramdecls = mib.mind_params_ctxt in let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) - let x = Termops.named_hd (Global.env()) r Anonymous in + let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in + let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = List.fold_left2 @@ -152,8 +159,7 @@ let declare_projections indsp coers fields = let ccl' = liftn 1 2 ccl in let p = mkLambda (x, lift 1 rp, ccl') in let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in - let ci = Inductiveops.make_case_info env indsp - LetStyle [| RegularPat |] in + let ci = Inductiveops.make_case_info env indsp LetStyle in mkCase (ci, p, mkRel 1, [|branch|]) in let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in @@ -165,10 +171,10 @@ let declare_projections indsp coers fields = const_entry_body = proj; const_entry_type = Some projtyp; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in - let k = (DefinitionEntry cie,IsDefinition StructureComponent) in + const_entry_boxed = Flags.boxed_definitions() } in + let k = (DefinitionEntry cie,IsDefinition kind) in let kn = declare_internal_constant fid k in - Options.if_verbose message (string_of_id fid ^" is defined"); + Flags.if_verbose message (string_of_id fid ^" is defined"); kn with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in @@ -199,23 +205,28 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; (* Now, younger decl in params and fields is on top *) - let params,fields = typecheck_params_and_fields ps fs in - let args = extended_rel_list (List.length fields) params in - let ind = applist (mkRel (1+List.length params+List.length fields), args) in + let params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in + let nparams = List.length params and nfields = List.length fields in + let args = extended_rel_list nfields params in + let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let mie_ind = { mind_entry_typename = idstruc; mind_entry_arity = mkSort s; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in + let declare_as_coind = + (* CoInd if recursive; otherwise Ind to have compat on _ind schemes *) + dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) in let mie = { mind_entry_params = List.map degenerate_decl params; mind_entry_record = true; - mind_entry_finite = true; + mind_entry_finite = not declare_as_coind; mind_entry_inds = [mie_ind] } in - let sp = declare_mutual_with_eliminations true mie in - let rsp = (sp,0) in (* This is ind path of idstruc *) + let kn = declare_mutual_with_eliminations true mie [] in + let rsp = (kn,0) in (* This is ind path of idstruc *) let kinds,sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) if is_coe then Class.try_add_new_coercion build Global; - Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs) + Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs); + kn diff --git a/toplevel/record.mli b/toplevel/record.mli index 66282c20..9642b351 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: record.mli 6743 2005-02-18 22:14:08Z herbelin $ i*) +(*i $Id: record.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) (*i*) open Names @@ -16,13 +16,13 @@ open Vernacexpr open Topconstr (*i*) -(* [declare_projections ref coers params fields] declare projections of - record [ref] (if allowed), and put them as coercions accordingly to - [coers]; it returns the absolute names of projections *) +(* [declare_projections ref name coers params fields] declare projections of + record [ref] (if allowed) using the given [name] as argument, and put them + as coercions accordingly to [coers]; it returns the absolute names of projections *) val declare_projections : - inductive -> bool list -> rel_context -> bool list * constant option list + inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list val definition_structure : lident with_coercion * local_binder list * - (local_decl_expr with_coercion) list * identifier * sorts -> unit + (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index fdd30711..42f2883a 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 10087 2007-08-24 10:39:30Z herbelin $ *) +(* $Id: toplevel.ml 10916 2008-05-10 15:38:36Z herbelin $ *) open Pp open Util -open Options +open Flags open Cerrors open Vernac open Pcoq @@ -103,7 +103,7 @@ let get_bols_of_loc ibuf (bp,ep) = lines_rec ll nafter fl in let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in - (fl,out_some ll) + (fl,Option.get ll) let dotted_location (b,e) = if e-b < 3 then @@ -134,18 +134,18 @@ let print_highlight_location ib loc = (l1 ++ li ++ ln) in let loc = make_loc (bp,ep) in - (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++ + (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) (* Functions to report located errors in a file. *) let print_location_in_file s inlibrary fname loc = - let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in + let errstrm = (str"Error while reading " ++ str s ++ str":") in if loc = dummy_loc then (errstrm ++ str", unknown location." ++ fnl ()) else if inlibrary then - (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ + (errstrm ++ fnl () ++ str"Module " ++ str ("\""^fname^"\"") ++ str" characters " ++ Cerrors.print_loc loc ++ fnl ()) else let (bp,ep) = unloc loc in @@ -162,7 +162,7 @@ let print_location_in_file s inlibrary fname loc = close_in ic; (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str", line " ++ int line ++ - str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ fnl ()) + str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ str":" ++ fnl ()) with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ())) let print_command_location ib dloc = @@ -221,11 +221,9 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in -(* statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ (emacs_prompt_endstring()) *) - if !Options.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " else "" - (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0bcf55a8..c331c13b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 9397 2006-11-21 21:50:54Z herbelin $ *) +(* $Id: vernac.ml 10836 2008-04-23 11:43:58Z courtieu $ *) (* Parsing of vernacular. *) open Pp open Lexer open Util -open Options +open Flags open System open Vernacexpr open Vernacinterp @@ -127,7 +127,7 @@ let rec vernac_com interpfun (loc,com) = (* end translator state *) (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in - if !Options.translate_file then + if !Flags.translate_file then begin let _,f = find_file_in_path (Library.get_load_paths ()) (make_suffix fname ".v") in @@ -137,13 +137,13 @@ let rec vernac_com interpfun (loc,com) = begin try read_vernac_file verbosely (make_suffix fname ".v"); - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; Constrintern.coqdoc_unfreeze cds with e -> - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; @@ -174,11 +174,12 @@ and vernac interpfun input = vernac_com interpfun (parse_phrase input) and read_vernac_file verbosely s = + Flags.make_warn verbosely; let interpfun = if verbosely then Vernacentries.interp else - Options.silently Vernacentries.interp + Flags.silently Vernacentries.interp in let (in_chan, fname, input) = open_file_twice_if verbosely s in try @@ -195,11 +196,13 @@ and read_vernac_file verbosely s = (* raw_do_vernac : char Stream.t -> unit * parses and executes one command of the vernacular char stream. - * Marks the end of the command in the lib_stk to make vernac undoing - * easier. *) + * Marks the end of the command in the lib_stk with a new label to + * make vernac undoing easier. Also freeze state to speed up + * backtracking. *) let raw_do_vernac po = vernac (States.with_heavy_rollback Vernacentries.interp) (po,None); + Lib.add_frozen_state(); Lib.mark_end_of_command() (* XML output hooks *) @@ -212,22 +215,22 @@ let set_xml_end_library f = xml_end_library := f (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = chan_translate := - if !Options.translate_file then open_out (file^"8") else stdout; + if !Flags.translate_file then open_out (file^"8") else stdout; try read_vernac_file verb file; - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; with e -> - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; raise_with_file file e (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = let ldir,long_f_dot_v = Library.start_library f in if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - if !Options.xml_export then !xml_start_library (); + if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in if Pfedit.get_all_proof_names () <> [] then (message "Error: There are pending proofs"; exit 1); - if !Options.xml_export then !xml_end_library (); + if !Flags.xml_export then !xml_end_library (); Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dd6d7e25..402f3b34 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 10067 2007-08-09 17:13:16Z msozeau $ i*) +(*i $Id: vernacentries.ml 11065 2008-06-06 22:39:43Z msozeau $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp open Util -open Options +open Flags open Names open Entries open Nameops @@ -35,6 +35,7 @@ open Decl_kinds open Topconstr open Pretyping open Redexpr +open Syntax_def (* Pcoq hooks *) @@ -44,8 +45,8 @@ type pcoq_hook = { abort : string -> unit; search : searchable -> dir_path list * bool -> unit; print_name : reference -> unit; - print_check : Environ.unsafe_judgment -> unit; - print_eval : (constr -> constr) -> Environ.env -> constr_expr -> + print_check : Environ.env -> Environ.unsafe_judgment -> unit; + print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> Environ.unsafe_judgment -> unit; show_goal : int option -> unit } @@ -58,7 +59,7 @@ let set_pcoq_hook f = pcoq := Some f let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Nametab.global r) + | RefClass r -> Class.class_of_global (global_with_alias r) (*******************) (* "Show" commands *) @@ -94,7 +95,7 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (print_treescript true evc pf) + msgnl_with !Pp_control.deep_ft (print_treescript true evc pf) let show_thesis () = msgnl (anomaly "TODO" ) @@ -272,6 +273,11 @@ let print_located_module r = str "No module is referred to by name ") ++ pr_qualid qid in msgnl msg +let global_with_alias r = + let gr = global_with_alias r in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + gr + (**********) (* Syntax *) @@ -284,8 +290,8 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope -let vernac_arguments_scope local qid scl = - Notation.declare_arguments_scope local (global qid) scl +let vernac_arguments_scope local r scl = + Notation.declare_arguments_scope local (global_with_alias r) scl let vernac_infix = Metasyntax.add_infix @@ -294,12 +300,31 @@ let vernac_notation = Metasyntax.add_notation (***********) (* Gallina *) -let start_proof_and_print idopt k t hook = - start_proof_com idopt k t hook; +let start_proof_and_print k l hook = + start_proof_com k l hook; print_subgoals (); - if !pcoq <> None then (out_some !pcoq).start_proof () + if !pcoq <> None then (Option.get !pcoq).start_proof () + +let current_dirpath sec = + drop_dirpath_prefix (Lib.library_dp ()) + (if sec then Lib.cwd () + else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())) + +let dump_definition (loc, id) sec s = + Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc)) + (string_of_dirpath (current_dirpath sec)) (string_of_id id)) + +let dump_reference loc modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty) -let vernac_definition (local,_,_ as k) id def hook = +let dump_constraint ((loc, n), _, _) sec ty = + match n with + | Name id -> dump_definition (loc, id) sec ty + | Anonymous -> () + +let vernac_definition (local,_,_ as k) (_,id as lid) def hook = + if !Flags.dump then dump_definition lid false "def"; match def with | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_modtype () then @@ -307,7 +332,8 @@ let vernac_definition (local,_,_ as k) id def hook = (str "Proof editing mode not supported in module types") else let hook _ _ = () in - start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook + start_proof_and_print (local,DefinitionBody Definition) + [Some lid,(bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -316,7 +342,12 @@ let vernac_definition (local,_,_ as k) id def hook = Some (interp_redexp env evc r) in declare_definition id k bl red_option c typ_opt hook -let vernac_start_proof kind sopt (bl,t) lettop hook = +let vernac_start_proof kind l lettop hook = + if !Flags.dump then + List.iter (fun (id, _) -> + match id with + | Some lid -> dump_definition lid false "prf" + | None -> ()) l; if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" @@ -324,12 +355,12 @@ let vernac_start_proof kind sopt (bl,t) lettop hook = if Lib.is_modtype () then errorlabstrm "Vernacentries.StartProof" (str "Proof editing mode not supported in module types"); - start_proof_and_print sopt (Global, Proof kind) (bl,t) hook + start_proof_and_print (Global, Proof kind) l hook let vernac_end_proof = function | Admitted -> admit () | Proved (is_opaque,idopt) -> - if not !Options.print_emacs then if_verbose show_script (); + if not !Flags.print_emacs then if_verbose show_script (); match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id @@ -348,14 +379,31 @@ let vernac_exact_proof c = errorlabstrm "Vernacentries.ExactProof" (str "Command 'Proof ...' can only be used at the beginning of the proof") -let vernac_assumption kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l - -let vernac_inductive f indl = build_mutual indl f - -let vernac_fixpoint = build_recursive - -let vernac_cofixpoint = build_corecursive +let vernac_assumption kind l nl= + let global = fst kind = Global in + List.iter (fun (is_coe,(idl,c)) -> + if !dump then + List.iter (fun lid -> + if global then dump_definition lid false "ax" + else dump_definition lid true "var") idl; + declare_assumption idl is_coe kind [] c false false nl) l + +let vernac_inductive f indl = + if !dump then + List.iter (fun ((lid, _, _, cstrs), _) -> + dump_definition lid false"ind"; + List.iter (fun (_, (lid, _)) -> + dump_definition lid false "constr") cstrs) + indl; + build_mutual indl f + +let vernac_fixpoint l b = + List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l; + build_recursive l b + +let vernac_cofixpoint l b = + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l; + build_corecursive l b let vernac_scheme = build_scheme @@ -369,7 +417,7 @@ let vernac_import export refl = List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export id binders_ast mty_ast_o = +let vernac_declare_module export (loc, id) binders_ast mty_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -381,33 +429,38 @@ let vernac_declare_module export id binders_ast mty_ast_o = "Remove the \"Export\" and \"Import\" keywords from every functor " ^ "argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) None; + id binders_ast (Some mty_ast_o) None + in + Modintern.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = +let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; match mexpr_ast_o with | None -> + check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in - Declaremods.start_module Modintern.interp_modtype export - id binders_ast mty_ast_o; - if_verbose message - ("Interactive Module "^ string_of_id id ^" started") ; - List.iter - (fun (export,id) -> - option_iter - (fun export -> vernac_import export [Ident (dummy_loc,id)]) export - ) argsexport + let mp = Declaremods.start_module Modintern.interp_modtype export + id binders_ast mty_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("Interactive Module "^ string_of_id id ^" started") ; + List.iter + (fun (export,id) -> + Option.iter + (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + ) argsexport | Some _ -> let binders_ast = List.map (fun (export,idl,ty) -> @@ -416,37 +469,42 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = " the definition is interactive. Remove the \"Export\" and " ^ "\"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o; - if_verbose message - ("Module "^ string_of_id id ^" is defined"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) - export - -let vernac_end_module export id = - Declaremods.end_module id; + id binders_ast mty_ast_o mexpr_ast_o + in + Modintern.dump_moddef loc mp "mod"; + if_verbose message + ("Module "^ string_of_id id ^" is defined"); + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + export + +let vernac_end_module export (loc,id) = + let mp = Declaremods.end_module id in + Modintern.dump_modref loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined") ; - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_declare_module_type id binders_ast mty_ast_o = +let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections"; match mty_ast_o with | None -> + check_no_pending_proofs (); let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in - Declaremods.start_modtype Modintern.interp_modtype id binders_ast; + let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport @@ -458,25 +516,35 @@ let vernac_declare_module_type id binders_ast mty_ast_o = " the definition is interactive. Remove the \"Export\" " ^ "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in - Declaremods.declare_modtype Modintern.interp_modtype - id binders_ast base_mty; + let mp = Declaremods.declare_modtype Modintern.interp_modtype + id binders_ast base_mty in + Modintern.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_end_modtype id = - Declaremods.end_modtype id; +let vernac_end_modtype (loc,id) = + let mp = Declaremods.end_modtype id in + Modintern.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") - +let vernac_include = function + | CIMTE mty_ast -> + Declaremods.declare_include Modintern.interp_modtype mty_ast false + | CIME mexpr_ast -> + Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + + + (**********************) (* Gallina extensions *) - + let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) - | Some (_,id) -> id in + | Some (_,id as lid) -> + if !dump then dump_definition lid false "constr"; id in let sigma = Evd.empty in let env = Global.env() in let s = interp_constr sigma env sort in @@ -485,45 +553,48 @@ let vernac_record struc binders sort nameopt cfs = | Sort s -> s | _ -> user_err_loc (constr_loc sort,"definition_structure", str "Sort expected") in - Record.definition_structure (struc,binders,cfs,const,s) + if !dump then ( + dump_definition (snd struc) false "rec"; + List.iter (fun (_, x) -> + match x with + | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj" + | _ -> ()) cfs); + ignore(Record.definition_structure (struc,binders,cfs,const,s)) (* Sections *) -let vernac_begin_section = Lib.open_section -let vernac_end_section = Lib.close_section +let vernac_begin_section (_, id as lid) = + check_no_pending_proofs (); + if !Flags.dump then dump_definition lid true "sec"; + Lib.open_section id + +let vernac_end_section (loc, id) = + if !Flags.dump then + dump_reference loc + (string_of_dirpath (current_dirpath true)) "<>" "sec"; + Lib.close_section id -let vernac_end_segment id = +let vernac_end_segment lid = check_no_pending_proofs (); let o = try Lib.what_is_opened () with Not_found -> error "There is nothing to end." in match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid + | _,Lib.OpenedModtype _ -> vernac_end_modtype lid + | _,Lib.OpenedSection _ -> vernac_end_section lid | _ -> anomaly "No more opened things" let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import -let vernac_canonical locqid = - Recordops.declare_canonical_structure (Nametab.global locqid) - -let locate_reference ref = - let (loc,qid) = qualid_of_reference ref in - try match Nametab.extended_locate qid with - | TrueGlobal ref -> ref - | SyntacticDef kn -> - match Syntax_def.search_syntactic_definition loc kn with - | Rawterm.RRef (_,ref) -> ref - | _ -> raise Not_found - with Not_found -> - error_global_not_found_loc loc qid +let vernac_canonical r = + Recordops.declare_canonical_structure (global_with_alias r) let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - let ref' = locate_reference ref in + let ref' = global_with_alias ref in Class.try_add_new_coercion_with_target ref' stre source target; if_verbose message ((string_of_reference ref) ^ " is now a coercion") @@ -532,6 +603,24 @@ let vernac_identity_coercion stre id qids qidt = let source = cl_of_qualid qids in Class.try_add_new_identity_coercion id stre source target +(* Type classes *) +let vernac_class id par ar sup props = + if !dump then ( + dump_definition id false "class"; + List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props); + Classes.new_class id par ar sup props + +let vernac_instance glob sup inst props pri = + if !dump then dump_constraint inst false "inst"; + ignore(Classes.new_instance ~global:glob sup inst props pri) + +let vernac_context l = + if !dump then List.iter (fun x -> dump_constraint x true "var") l; + Classes.context l + +let vernac_declare_instance id = + if !dump then dump_definition id false "inst"; + Classes.declare_instance false id (***********) (* Solving *) @@ -547,12 +636,12 @@ let vernac_solve n tcom b = (* in case a strict subtree was completed, go back to the top of the prooftree *) if subtree_solved () then begin - Options.if_verbose msgnl (str "Subgoal proved"); + Flags.if_verbose msgnl (str "Subgoal proved"); make_focus 0; reset_top_of_script () end; print_subgoals(); - if !pcoq <> None then (out_some !pcoq).solve n + if !pcoq <> None then (Option.get !pcoq).solve n (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -664,13 +753,16 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef let vernac_hints = Auto.add_hints -let vernac_syntactic_definition = Command.syntax_definition - -let vernac_declare_implicits local locqid = function +let vernac_syntactic_definition lid = + dump_definition lid false "syndef"; + Command.syntax_definition (snd lid) + +let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (Nametab.global locqid) imps + Impargs.declare_manual_implicits local (global_with_alias r) false + (List.map (fun (ex,b,f) -> ex, (b,f)) imps) | None -> - Impargs.declare_implicits local (Nametab.global locqid) + Impargs.declare_implicits local (global_with_alias r) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -706,6 +798,14 @@ let _ = optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } +let _ = + declare_bool_option + { optsync = true; + optname = "strong strict implicit arguments"; + optkey = (TertiaryTable ("Strongly","Strict","Implicit")); + optread = Impargs.is_strongly_strict_implicit_args; + optwrite = Impargs.make_strongly_strict_implicit_args } + let _ = declare_bool_option { optsync = true; @@ -714,6 +814,30 @@ let _ = optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } +(* let _ = *) +(* declare_bool_option *) +(* { optsync = true; *) +(* optname = "forceable implicit arguments"; *) +(* optkey = (SecondaryTable ("Forceable","Implicit")); *) +(* optread = Impargs.is_forceable_implicit_args; *) +(* optwrite = Impargs.make_forceable_implicit_args } *) + +let _ = + declare_bool_option + { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); + optread = Impargs.is_reversible_pattern_implicit_args; + optwrite = Impargs.make_reversible_pattern_implicit_args } + +let _ = + declare_bool_option + { optsync = true; + optname = "maximal insertion of implicit"; + optkey = (TertiaryTable ("Maximal","Implicit","Insertion")); + optread = Impargs.is_maximal_implicit_args; + optwrite = Impargs.make_maximal_implicit_args } + let _ = declare_bool_option { optsync = true; @@ -722,6 +846,13 @@ let _ = optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } +let _ = + declare_bool_option + { optsync = true; + optname = "printing of existential variable instances"; + optkey = (TertiaryTable ("Printing","Existential","Instances")); + optread = (fun () -> !Constrextern.print_evar_arguments); + optwrite = (:=) Constrextern.print_evar_arguments } let _ = declare_bool_option { optsync = true; @@ -730,6 +861,14 @@ let _ = optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } +let _ = + declare_bool_option + { optsync = true; + optname = "implicit arguments defensive printing"; + optkey = (TertiaryTable ("Printing","Implicit","Defensive")); + optread = (fun () -> !Constrextern.print_implicits_defensive); + optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } + let _ = declare_bool_option { optsync = true; @@ -751,8 +890,8 @@ let _ = { optsync = true; optname = "raw printing"; optkey = (SecondaryTable ("Printing","All")); - optread = (fun () -> !Options.raw_print); - optwrite = (fun b -> Options.raw_print := b) } + optread = (fun () -> !Flags.raw_print); + optwrite = (fun b -> Flags.raw_print := b) } let _ = declare_bool_option @@ -767,8 +906,8 @@ let _ = { optsync = true; optname = "use of boxed definitions"; optkey = (SecondaryTable ("Boxed","Definitions")); - optread = Options.boxed_definitions; - optwrite = (fun b -> Options.set_boxed_definitions b) } + optread = Flags.boxed_definitions; + optwrite = (fun b -> Flags.set_boxed_definitions b) } let _ = declare_bool_option @@ -791,8 +930,8 @@ let _ = { optsync=false; optkey=SecondaryTable("Hyps","Limit"); optname="the hypotheses limit"; - optread=Options.print_hyps_limit; - optwrite=Options.set_print_hyps_limit } + optread=Flags.print_hyps_limit; + optwrite=Flags.set_print_hyps_limit } let _ = declare_int_option @@ -814,7 +953,7 @@ let _ = declare_bool_option { optsync=true; optkey=SecondaryTable("Printing","Universes"); - optname="the printing of universes"; + optname="printing of universes"; optread=(fun () -> !Constrextern.print_universes); optwrite=(fun b -> Constrextern.print_universes:=b) } @@ -829,15 +968,15 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -let vernac_set_opacity opaq locqid = - match Nametab.global locqid with - | ConstRef sp -> - if opaq then set_opaque_const sp - else set_transparent_const sp - | VarRef id -> - if opaq then set_opaque_var id - else set_transparent_var id - | _ -> error "cannot set an inductive type or a constructor as transparent" +let vernac_set_opacity local str = + let glob_ref r = + match global_with_alias r with + | ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in + Redexpr.set_strategy local str let vernac_set_option key = function | StringValue s -> set_string_option_value key s @@ -888,13 +1027,13 @@ let vernac_check_may_eval redexp glopt rc = let j = Typeops.typing env c in match redexp with | None -> - if !pcoq <> None then (out_some !pcoq).print_check j + if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in if !pcoq <> None - then (out_some !pcoq).print_eval (redfun env evmap) env rc j - else msg (print_eval redfun env j) + then (Option.get !pcoq).print_eval redfun env evmap rc j + else msg (print_eval redfun env evmap rc j) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -910,7 +1049,7 @@ let vernac_print = function | PrintFullContext -> msg (print_full_context_typ ()) | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) - | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent + | PrintGrammar ent -> Metasyntax.print_grammar ent | PrintLoadPath -> (* For compatibility ? *) print_loadpath () | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid @@ -918,11 +1057,13 @@ let vernac_print = function | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> - if !pcoq <> None then (out_some !pcoq).print_name qid + if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) + | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) + | PrintInstances c -> ppnl (Prettyp.print_instances (global c)) | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid))) | PrintCoercions -> ppnl (Prettyp.print_coercions()) | PrintCoercionPaths (cls,clt) -> @@ -930,7 +1071,7 @@ let vernac_print = function | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) | PrintUniverses (Some s) -> dump_universes s - | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid) + | PrintHint r -> Auto.print_hint_ref (global_with_alias r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s @@ -944,6 +1085,11 @@ let vernac_print = function pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) +(*spiwack: prints all the axioms and section variables used by a term *) + | PrintAssumptions r -> + let cstr = constr_of_global (global_with_alias r) in + let nassumptions = Environ.assumptions cstr (Global.env ()) in + msg (Printer.pr_assumptionset (Global.env ()) nassumptions) let global_module r = let (loc,qid) = qualid_of_reference r in @@ -959,12 +1105,12 @@ let interp_search_restriction = function open Search let interp_search_about_item = function - | SearchRef qid -> GlobSearchRef (Nametab.global qid) + | SearchRef r -> GlobSearchRef (global_with_alias r) | SearchString s -> GlobSearchString s let vernac_search s r = let r = interp_search_restriction r in - if !pcoq <> None then (out_some !pcoq).search s r else + if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in @@ -972,8 +1118,8 @@ let vernac_search s r = | SearchRewrite c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in Search.search_rewrite pat r - | SearchHead locqid -> - Search.search_by_head (Nametab.global locqid) r + | SearchHead ref -> + Search.search_by_head (global_with_alias ref) r | SearchAbout sl -> Search.search_about (List.map interp_search_about_item sl) r @@ -994,7 +1140,7 @@ let vernac_goal = function | Some c -> if not (refining()) then begin let unnamed_kind = Lemma (* Arbitrary *) in - start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->()); + start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); print_subgoals () end else error "repeated Goal not permitted in refining mode" @@ -1003,12 +1149,12 @@ let vernac_abort = function | None -> delete_current_proof (); if_verbose message "Current goal aborted"; - if !pcoq <> None then (out_some !pcoq).abort "" + if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); - if !pcoq <> None then (out_some !pcoq).abort s + if !pcoq <> None then (Option.get !pcoq).abort s let vernac_abort_all () = if refining() then begin @@ -1078,7 +1224,7 @@ let explain_tree occ = let vernac_show = function | ShowGoal nopt -> - if !pcoq <> None then (out_some !pcoq).show_goal nopt + if !pcoq <> None then (Option.get !pcoq).show_goal nopt else msg (match nopt with | None -> pr_open_subgoals () | Some n -> pr_nth_open_subgoal n) @@ -1116,7 +1262,7 @@ let vernac_check_guard () = let interp c = match c with (* Control (done in vernac) *) - | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false + | (VernacTime _ | VernacList _ | VernacLoad _) -> assert false (* Syntax *) | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e) @@ -1129,12 +1275,11 @@ let interp c = match c with | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc (* Gallina *) - | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f - | VernacStartTheoremProof (k,(_,id),t,top,f) -> - vernac_start_proof k (Some id) t top f + | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f + | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,l) -> vernac_assumption stre l + | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,l) -> vernac_inductive finite l | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b @@ -1142,17 +1287,18 @@ let interp c = match c with | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) - | VernacDeclareModule (export,(_,id),bl,mtyo) -> - vernac_declare_module export id bl mtyo - | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> - vernac_define_module export id bl mtyo mexpro - | VernacDeclareModuleType ((_,id),bl,mtyo) -> - vernac_declare_module_type id bl mtyo - + | VernacDeclareModule (export,lid,bl,mtyo) -> + vernac_declare_module export lid bl mtyo + | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> + vernac_define_module export lid bl mtyo mexpro + | VernacDeclareModuleType (lid,bl,mtyo) -> + vernac_declare_module_type lid bl mtyo + | VernacInclude (in_ast) -> + vernac_include in_ast (* Gallina extensions *) - | VernacBeginSection (_,id) -> vernac_begin_section id + | VernacBeginSection lid -> vernac_begin_section lid - | VernacEndSegment (_,id) -> vernac_end_segment id + | VernacEndSegment lid -> vernac_end_segment lid | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl @@ -1161,6 +1307,13 @@ let interp c = match c with | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t + (* Type classes *) + | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props + + | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri + | VernacContext sup -> vernac_context sup + | VernacDeclareInstance id -> vernac_declare_instance id + (* Solving *) | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c @@ -1186,6 +1339,7 @@ let interp c = match c with | VernacRestoreState s -> vernac_restore_state s (* Resetting *) + | VernacRemoveName id -> Lib.remove_name id | VernacResetName id -> vernac_reset_name id | VernacResetInitial -> vernac_reset_initial () | VernacBack n -> vernac_back n @@ -1197,7 +1351,7 @@ let interp c = match c with | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c - | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl + | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl | VernacSetOption (key,v) -> vernac_set_option key v | VernacUnsetOption key -> vernac_unset_option key | VernacRemoveOption (key,v) -> vernac_remove_option key v @@ -1213,13 +1367,14 @@ let interp c = match c with | VernacNop -> () (* Proof management *) - | VernacGoal t -> vernac_start_proof Theorem None ([],t) false (fun _ _ ->()) + | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->()) | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () | VernacSuspend -> vernac_suspend () | VernacResume id -> vernac_resume id | VernacUndo n -> vernac_undo n + | VernacUndoTo n -> undo_todepth n | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index bcd89490..8afb783b 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.mli 8781 2006-05-03 10:15:05Z jforest $ i*) +(*i $Id: vernacentries.mli 10580 2008-02-22 13:39:13Z lmamane $ i*) (*i*) open Names @@ -39,14 +39,15 @@ type pcoq_hook = { abort : string -> unit; search : searchable -> dir_path list * bool -> unit; print_name : Libnames.reference -> unit; - print_check : Environ.unsafe_judgment -> unit; - print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit; + print_check : Environ.env -> Environ.unsafe_judgment -> unit; + print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr -> + Environ.unsafe_judgment -> unit; show_goal : int option -> unit } val set_pcoq_hook : pcoq_hook -> unit -(* This function makes sure that the function given is argument is preceded +(* This function makes sure that the function given in argument is preceded by a command aborting all proofs if necessary. It is used in pcoq. *) val abort_refine : ('a -> unit) -> 'a -> unit;; diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 9f51841d..744c3a6f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 10067 2007-08-09 17:13:16Z msozeau $ i*) +(*i $Id: vernacexpr.ml 11024 2008-05-30 12:41:39Z msozeau $ i*) open Util open Names @@ -37,7 +37,7 @@ type printable = | PrintFullContext | PrintSectionContext of reference | PrintInspect of int - | PrintGrammar of string * string + | PrintGrammar of string | PrintLoadPath | PrintModules | PrintModule of reference @@ -48,6 +48,8 @@ type printable = | PrintOpaqueName of reference | PrintGraph | PrintClasses + | PrintTypeClasses + | PrintInstances of reference | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr @@ -64,6 +66,7 @@ type printable = | PrintVisibility of string option | PrintAbout of reference | PrintImplicit of reference + | PrintAssumptions of reference type search_about_item = | SearchRef of reference @@ -109,7 +112,7 @@ type comment = | CommentInt of int type hints = - | HintsResolve of constr_expr list + | HintsResolve of (int option * constr_expr) list | HintsImmediate of constr_expr list | HintsUnfold of reference list | HintsConstructors of reference list @@ -144,10 +147,12 @@ type sort_expr = Rawterm.rawsort type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a type constructor_expr = (lident * constr_expr) with_coercion type inductive_expr = lident * local_binder list * constr_expr * constructor_expr list + type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr @@ -167,12 +172,15 @@ type proof_end = | Admitted | Proved of opacity_flag * (lident * theorem_kind option) option +type scheme = + | InductionScheme of bool * lreference * sort_expr + | EqualityScheme of lreference + type vernac_expr = (* Control *) | VernacList of located_vernac_expr list | VernacLoad of verbose_flag * lstring | VernacTime of vernac_expr - | VernacVar of lident (* Syntax *) | VernacTacticNotation of int * grammar_production list * raw_tactic_expr @@ -190,15 +198,16 @@ type vernac_expr = (* Gallina *) | VernacDefinition of definition_kind * lident * definition_expr * declaration_hook - | VernacStartTheoremProof of theorem_kind * lident * - (local_binder list * constr_expr) * bool * declaration_hook + | VernacStartTheoremProof of theorem_kind * + (lident option * (local_binder list * constr_expr)) list * + bool * declaration_hook | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of assumption_kind * simple_binder with_coercion list + | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool - | VernacScheme of (lident * bool * lreference * sort_expr) list + | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list (* Gallina extensions *) @@ -211,10 +220,30 @@ type vernac_expr = export_flag option * specif_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of lreference - | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of strength * lident * + | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr + | VernacIdentityCoercion of locality * lident * class_rawexpr * class_rawexpr + (* Type classes *) + | VernacClass of + lident * (* name *) + local_binder list * (* params *) + sort_expr located option * (* arity *) + local_binder list * (* constraints *) + (lident * bool * constr_expr) list (* props, with substructure hints *) + + | VernacInstance of + bool * (* global *) + local_binder list * (* super *) + typeclass_constraint * (* instance name, class name, params *) + (lident * lident list * constr_expr) list * (* props *) + int option (* Priority *) + + | VernacContext of typeclass_context + + | VernacDeclareInstance of + lident (* instance name *) + (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * module_binder list * (module_type_ast * bool) @@ -222,6 +251,7 @@ type vernac_expr = module_binder list * (module_type_ast * bool) option * module_ast option | VernacDeclareModuleType of lident * module_binder list * module_type_ast option + | VernacInclude of include_ast (* Solving *) @@ -248,6 +278,7 @@ type vernac_expr = | VernacRestoreState of lstring (* Resetting *) + | VernacRemoveName of lident | VernacResetName of lident | VernacResetInitial | VernacBack of int @@ -255,14 +286,15 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - rec_flag * (lident * raw_tactic_expr) list + rec_flag * (reference * bool * raw_tactic_expr) list | VernacHints of locality_flag * lstring list * hints - | VernacSyntacticDefinition of identifier * constr_expr * locality_flag * - onlyparsing_flag - | VernacDeclareImplicits of locality_flag * lreference * - explicitation list option + | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * + locality_flag * onlyparsing_flag + | VernacDeclareImplicits of locality_flag * lreference * + (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr - | VernacSetOpacity of opacity_flag * lreference list + | VernacSetOpacity of + locality_flag * (Conv_oracle.level * lreference list) list | VernacUnsetOption of Goptions.option_name | VernacSetOption of Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list @@ -285,6 +317,7 @@ type vernac_expr = | VernacSuspend | VernacResume of lident option | VernacUndo of int + | VernacUndoTo of int | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 98584bac..f43c0c5e 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacinterp.ml 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: vernacinterp.ml 10348 2007-12-06 17:36:14Z aspiwack $ *) open Pp open Util @@ -64,7 +64,7 @@ let call (opn,converted_args) = | Drop -> raise Drop | ProtectedLoop -> raise ProtectedLoop | e -> - if !Options.debug then + if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); raise e diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index b067ba1f..58703c8e 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -8,9 +8,9 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: whelp.ml4 10105 2007-08-30 16:53:32Z herbelin $ *) +(* $Id: whelp.ml4 10904 2008-05-08 16:31:26Z herbelin $ *) -open Options +open Flags open Pp open Util open System @@ -28,6 +28,7 @@ open Command open Pfedit open Refiner open Tacmach +open Syntax_def (* Coq interface to the Whelp query engine developed at the University of Bologna *) @@ -150,12 +151,12 @@ let rec uri_of_constr c = let inst,rest = merge (section_parameters f) args in uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; url_list_with_sep " " uri_of_constr rest - | RLambda (_,na,ty,c) -> + | RLambda (_,na,k,ty,c) -> url_string "\\lambda "; url_of_name na; url_string ":"; uri_of_constr ty; url_string "."; uri_of_constr c - | RProd (_,Anonymous,ty,c) -> + | RProd (_,Anonymous,k,ty,c) -> uri_of_constr ty; url_string "\\to "; uri_of_constr c - | RProd (_,Name id,ty,c) -> + | RProd (_,Name id,k,ty,c) -> url_string "\\forall "; url_id id; url_string ":"; uri_of_constr ty; url_string "."; uri_of_constr c | RLetIn (_,na,b,c) -> @@ -174,7 +175,7 @@ let make_string f x = Buffer.reset b; f x; Buffer.contents b let send_whelp req s = let url = make_whelp_request req s in - let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in + let command = subst_command_placeholder browser_cmd_fmt url in let _ = run_command (fun x -> x) print_string command in () let whelp_constr req c = @@ -192,13 +193,6 @@ let whelp_locate s = let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) -let locate_inductive r = - let (loc,qid) = qualid_of_reference r in - try match Syntax_def.locate_global qid with - | IndRef ind -> ind - | _ -> user_err_loc (loc,"",str "Inductive type expected") - with Not_found -> error_global_not_found_loc loc qid - let on_goal f = let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) @@ -221,7 +215,7 @@ END VERNAC COMMAND EXTEND Whelp | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END -- cgit v1.2.3