summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /toplevel
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml812
-rw-r--r--toplevel/auto_ind_decl.mli27
-rw-r--r--toplevel/cerrors.ml29
-rw-r--r--toplevel/class.ml52
-rw-r--r--toplevel/class.mli12
-rw-r--r--toplevel/classes.ml737
-rw-r--r--toplevel/classes.mli103
-rw-r--r--toplevel/command.ml884
-rw-r--r--toplevel/command.mli79
-rw-r--r--toplevel/coqinit.ml78
-rw-r--r--toplevel/coqtop.ml65
-rw-r--r--toplevel/discharge.ml4
-rw-r--r--toplevel/himsg.ml907
-rw-r--r--toplevel/himsg.mli5
-rw-r--r--toplevel/ind_tables.ml102
-rw-r--r--toplevel/ind_tables.mli40
-rw-r--r--toplevel/metasyntax.ml28
-rw-r--r--toplevel/metasyntax.mli4
-rw-r--r--toplevel/minicoq.ml4
-rw-r--r--toplevel/mltop.ml413
-rw-r--r--toplevel/record.ml55
-rw-r--r--toplevel/record.mli12
-rw-r--r--toplevel/toplevel.ml18
-rw-r--r--toplevel/vernac.ml29
-rw-r--r--toplevel/vernacentries.ml419
-rw-r--r--toplevel/vernacentries.mli9
-rw-r--r--toplevel/vernacexpr.ml65
-rw-r--r--toplevel/vernacinterp.ml4
-rw-r--r--toplevel/whelp.ml422
29 files changed, 3632 insertions, 986 deletions
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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: auto_ind_decl.ml 11166 2008-06-22 13:23:35Z herbelin $ i*)
+
+open Tacmach
+open Util
+open Flags
+open Decl_kinds
+open Pp
+open Entries
+open Termops
+open Declarations
+open Declare
+open Term
+open Names
+open Libnames
+open Goptions
+open Mod_subst
+open Indrec
+open Inductiveops
+open Tactics
+open Tacticals
+open Ind_tables
+
+(* boolean equality *)
+
+let quick_chop n l =
+ let rec kick_last = function
+ | t::[] -> []
+ | t::q -> t::(kick_last q)
+ | [] -> failwith "kick_last"
+and aux = function
+ | (0,l') -> l'
+ | (n,h::t) -> aux (n-1,t)
+ | _ -> failwith "quick_chop"
+ in
+ if n > (List.length l) then failwith "quick_chop args"
+ else kick_last (aux (n,l) )
+
+let rec deconstruct_type t =
+ let l,r = decompose_prod t in
+ (List.map (fun (_,b) -> b) (List.rev l))@[r]
+
+let subst_in_constr (_,subst,(ind,const)) =
+ let ind' = (subst_kn subst (fst ind)),(snd ind)
+ and const' = subst_mps subst const in
+ ind',const'
+
+exception EqNotFound of string
+exception EqUnknown of string
+
+(* Some pre declaration of constant we are going to use *)
+let bb = constr_of_global Coqlib.glob_bool
+
+let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop
+
+let andb_true_intro = fun _ ->
+ (Coqlib.build_bool_type()).Coqlib.andb_true_intro
+
+let tt = constr_of_global Coqlib.glob_true
+
+let ff = constr_of_global Coqlib.glob_false
+
+let eq = constr_of_global Coqlib.glob_eq
+
+let sumbool = Coqlib.build_coq_sumbool
+
+let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
+
+(* reconstruct the inductive with the correct deBruijn indexes *)
+let mkFullInd ind n =
+ let mib = Global.lookup_mind (fst ind) in
+ let nparams = mib.mind_nparams in
+ let nparrec = mib.mind_nparams_rec in
+ (* params context divided *)
+ let lnonparrec,lnamesparrec =
+ context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ if nparrec > 0
+ then mkApp (mkInd ind,
+ Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
+ else mkInd ind
+
+let make_eq_scheme sp =
+ (* fetching global env *)
+ let env = Global.env() in
+ (* fetching the mutual inductive body *)
+ let mib = Global.lookup_mind sp in
+ (* number of inductives in the mutual *)
+ let nb_ind = Array.length mib.mind_packets in
+ (* number of params in the type *)
+ let nparams = mib.mind_nparams in
+ let nparrec = mib.mind_nparams_rec in
+ (* params context divided *)
+ let lnonparrec,lnamesparrec =
+ context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ (* predef coq's boolean type *)
+ (* rec name *)
+ let rec_name i =(string_of_id (Array.get mib.mind_packets i).mind_typename)^
+ "_eqrec"
+ in
+ (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *)
+ let create_input c =
+ let myArrow u v = mkArrow u (lift 1 v)
+ and eqName = function
+ | Name s -> id_of_string ("eq_"^(string_of_id s))
+ | Anonymous -> id_of_string "eq_A"
+ in
+ let ext_rel_list = extended_rel_list 0 lnamesparrec in
+ let lift_cnt = ref 0 in
+ let eqs_typ = List.map (fun aa ->
+ let a = lift !lift_cnt aa in
+ incr lift_cnt;
+ myArrow a (myArrow a bb)
+ ) ext_rel_list in
+
+ let eq_input = List.fold_left2
+ ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *)
+ (* here I leave the Naming thingy so that the type of
+ the function is more readable for the user *)
+ mkNamedLambda (eqName n) b a )
+ c (List.rev eqs_typ) lnamesparrec
+ in
+ List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *)
+ (* Same here , hoping the auto renaming will do something good ;) *)
+ mkNamedLambda
+ (match n with Name s -> s | Anonymous -> id_of_string "A")
+ t a) eq_input lnamesparrec
+ in
+ let make_one_eq cur =
+ let ind = sp,cur in
+ (* current inductive we are working on *)
+ let cur_packet = mib.mind_packets.(snd ind) in
+ (* Inductive toto : [rettyp] := *)
+ let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in
+ (* split rettyp in a list without the non rec params and the last ->
+ e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
+ let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
+ (* give a type A, this function tries to find the equality on A declared
+ previously *)
+ (* nlist = the number of args (A , B , ... )
+ eqA = the deBruijn index of the first eq param
+ ndx = how much to translate due to the 2nd Case
+ *)
+ let compute_A_equality rel_list nlist eqA ndx t =
+ let lifti = ndx in
+ let rec aux c a = match c with
+ | Rel x -> mkRel (x-nlist+ndx)
+ | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x)))
+ | Cast (x,_,_) -> aux (kind_of_term x) a
+ | App (x,newa) -> aux (kind_of_term x) newa
+ | Ind (sp',i) -> if sp=sp' then mkRel(eqA-nlist-i+nb_ind-1)
+ else ( try
+ let eq = find_eq_scheme (sp',i)
+ and eqa = Array.map
+ (fun x -> aux (kind_of_term x) [||] ) a
+ in
+ let args = Array.append
+ (Array.map (fun x->lift lifti x) a) eqa
+ in if args = [||] then eq
+ else mkApp (eq,Array.append
+ (Array.map (fun x->lift lifti x) a) eqa)
+ with Not_found -> raise(EqNotFound (string_of_kn sp'))
+ )
+ | Sort _ -> raise (EqUnknown "Sort" )
+ | Prod _ -> raise (EqUnknown "Prod" )
+ | Lambda _-> raise (EqUnknown "Lambda")
+ | LetIn _ -> raise (EqUnknown "LetIn")
+ | Const kn -> let mp,dir,lbl= repr_con kn in
+ mkConst (make_con mp dir (
+ mk_label ("eq_"^(string_of_label lbl))))
+ | Construct _ -> raise (EqUnknown "Construct")
+ | Case _ -> raise (EqUnknown "Case")
+ | CoFix _ -> raise (EqUnknown "CoFix")
+ | Fix _ -> raise (EqUnknown "Fix")
+ | Meta _ -> raise (EqUnknown "Meta")
+ | Evar _ -> raise (EqUnknown "Evar")
+ in
+ aux t [||]
+ in
+ (* construct the predicate for the Case part*)
+ let do_predicate rel_list n =
+ List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
+ (mkLambda (Anonymous,
+ mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
+ bb))
+ (List.rev rettyp_l) in
+ (* make_one_eq *)
+ (* do the [| C1 ... => match Y with ... end
+ ...
+ Cn => match Y with ... end |] part *)
+ let ci = make_case_info env ind MatchStyle in
+ let constrs n = get_constructors env (make_ind_family (ind,
+ extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+ let constrsi = constrs (3+nparrec) in
+ let n = Array.length constrsi in
+ let ar = Array.create n ff in
+ for i=0 to n-1 do
+ let nb_cstr_args = List.length constrsi.(i).cs_args in
+ let ar2 = Array.create n ff in
+ let constrsj = constrs (3+nparrec+nb_cstr_args) in
+ for j=0 to n-1 do
+ if (i=j) then
+ ar2.(j) <- let cc = (match nb_cstr_args with
+ | 0 -> tt
+ | _ -> let eqs = Array.make nb_cstr_args tt in
+ for ndx = 0 to nb_cstr_args-1 do
+ let _,_,cc = List.nth constrsi.(i).cs_args ndx in
+ let eqA = compute_A_equality rel_list
+ nparrec
+ (nparrec+3+2*nb_cstr_args)
+ (nb_cstr_args+ndx+1)
+ (kind_of_term cc)
+ in
+ Array.set eqs ndx
+ (mkApp (eqA,
+ [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
+ ))
+ done;
+ Array.fold_left
+ (fun a b -> mkApp (andb(),[|b;a|]))
+ (eqs.(0))
+ (Array.sub eqs 1 (nb_cstr_args - 1))
+ )
+ in
+ (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc
+ (constrsj.(j).cs_args)
+ )
+ else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
+ mkLambda (p,r,a)) ff (constrsj.(j).cs_args) )
+ done;
+
+ ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
+ (mkCase (ci,do_predicate rel_list nb_cstr_args,
+ mkVar (id_of_string "Y") ,ar2))
+ (constrsi.(i).cs_args))
+ done;
+ mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1)) (
+ mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2)) (
+ mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar)))
+ in (* make_eq_scheme *)
+ try
+ let names = Array.make nb_ind Anonymous and
+ types = Array.make nb_ind mkSet and
+ cores = Array.make nb_ind mkSet and
+ res = Array.make nb_ind mkSet in
+ for i=0 to (nb_ind-1) do
+ names.(i) <- Name (id_of_string (rec_name i));
+ types.(i) <- mkArrow (mkFullInd (sp,i) 0)
+ (mkArrow (mkFullInd (sp,i) 1) bb);
+ cores.(i) <- make_one_eq i
+ done;
+ if (string_of_mp (modpath sp ))="Coq.Init.Logic"
+ then print_string "Logic time, do nothing.\n"
+ else (
+ for i=0 to (nb_ind-1) do
+ let cpack = Array.get mib.mind_packets i in
+ if check_eq_scheme (sp,i)
+ then message ("Boolean equality is already defined on "^
+ (string_of_id cpack.mind_typename)^".")
+ else (
+ let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
+ res.(i) <- create_input fix
+ )
+ done;
+ );
+ res
+ with
+ | EqUnknown s -> error ("Type unexpected ("^s^
+ ") during boolean eq computation, please report.")
+ | EqNotFound s -> error ("Boolean equality on "^s^
+ " is missing, equality will not be defined.")
+ | _ -> error ("Unknown exception during boolean equality creation,"^
+ " the equality will not be defined.")
+
+(* This function tryies to get the [inductive] between a constr
+ the constr should be Ind i or App(Ind i,[|args|])
+*)
+let destruct_ind c =
+ try let u,v = destApp c in
+ let indc = destInd u in
+ indc,v
+ with _-> let indc = destInd c in
+ indc,[||]
+
+(*
+ In the followind, avoid is the list of names to avoid.
+ If the args of the Inductive type are A1 ... An
+ then avoid should be
+ [| lb_An ... lb _A1 (resp. bl_An ... bl_A1)
+ eq_An .... eq_A1 An ... A1 |]
+so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
+*)
+(* used in the leib -> bool side*)
+let do_replace_lb aavoid narg gls p q =
+ let avoid = Array.of_list aavoid in
+ let do_arg v offset =
+ try
+ let x = narg*offset in
+ let s = destVar v in
+ let n = Array.length avoid in
+ let rec find i =
+ if avoid.(n-i) = s then avoid.(n-i-x)
+ else (if i<n then find (i+1)
+ else error ("Var "^(string_of_id s)^" seems unknown.")
+ )
+ in mkVar (find 1)
+ with _ -> (* if this happen then the args have to be already declared as a
+ Parameter*)
+ (
+ let mp,dir,lbl = repr_con (destConst v) in
+ mkConst (make_con mp dir (mk_label (
+ if offset=1 then ("eq_"^(string_of_label lbl))
+ else ((string_of_label lbl)^"_lb")
+ )))
+ )
+ in
+ let type_of_pq = pf_type_of gls p in
+ let u,v = destruct_ind type_of_pq
+ in let lb_type_of_p =
+ try find_lb_proof u
+ with Not_found ->
+ (* 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<n then find (i+1)
+ else error ("Var "^(string_of_id s)^" seems unknown.")
+ )
+ in mkVar (find 1)
+ with _ -> (* if this happen then the args have to be already declared as a
+ Parameter*)
+ (
+ let mp,dir,lbl = repr_con (destConst v) in
+ mkConst (make_con mp dir (mk_label (
+ if offset=1 then ("eq_"^(string_of_label lbl))
+ else ((string_of_label lbl)^"_bl")
+ )))
+ )
+ in
+
+ let rec aux l1 l2 =
+ match (l1,l2) with
+ | (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in
+ if t1=t2 then aux q1 q2
+ else (
+ let u,v = try destruct_ind tt1
+ (* trick so that the good sequence is returned*)
+ with _ -> ind,[||]
+ in if u = ind
+ then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
+ else (
+ let bl_t1 =
+ try find_bl_proof u
+ with Not_found ->
+ (* 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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Term
+open Names
+open Libnames
+open Mod_subst
+open Sign
+
+
+val subst_in_constr : (object_name*substitution*(inductive*constr))
+ -> (inductive*constr)
+
+val compute_bl_goal : inductive -> rel_context -> int -> types
+val compute_bl_tact : inductive -> rel_context -> int -> unit
+val compute_lb_goal : inductive -> rel_context -> int -> types
+val compute_lb_tact : inductive -> rel_context -> int -> unit
+val compute_dec_goal : inductive -> rel_context -> int -> types
+val compute_dec_tact : inductive -> rel_context -> int -> unit
+
+
+val make_eq_scheme :mutual_inductive -> types array
diff --git a/toplevel/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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: classes.ml 11161 2008-06-21 14:32:47Z msozeau $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Termops
+open Sign
+open Entries
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Typeclasses_errors
+open Typeclasses
+open Libnames
+open Constrintern
+open Rawterm
+open Topconstr
+(*i*)
+
+open Decl_kinds
+open Entries
+
+let hint_db = "typeclass_instances"
+
+let qualid_of_con c =
+ Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+
+let _ =
+ Typeclasses.register_add_instance_hint
+ (fun inst pri ->
+ 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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: classes.mli 11024 2008-05-30 12:41:39Z msozeau $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Topconstr
+open Util
+open Typeclasses
+open Implicit_quantifiers
+(*i*)
+
+type binder_list = (identifier located * bool * constr_expr) list
+type binder_def_list = (identifier located * identifier located list * constr_expr) list
+
+val binders_of_lidents : identifier located list -> 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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: ind_tables.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
+open Names
+open Mod_subst
+
+let eq_scheme_map = ref Indmap.empty
+
+let cache_scheme (_,(ind,const)) =
+ eq_scheme_map := Indmap.add ind const (!eq_scheme_map)
+
+let export_scheme obj =
+ Some obj
+
+
+
+let _ = Summary.declare_summary "eqscheme"
+ { Summary.freeze_function = (fun () -> !eq_scheme_map);
+ Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs);
+ Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = true}
+
+let find_eq_scheme ind =
+ Indmap.find ind !eq_scheme_map
+
+let check_eq_scheme ind =
+ Indmap.mem ind !eq_scheme_map
+
+let bl_map = ref Indmap.empty
+let lb_map = ref Indmap.empty
+let dec_map = ref Indmap.empty
+
+
+let cache_bl (_,(ind,const)) =
+ bl_map := Indmap.add ind const (!bl_map)
+
+let cache_lb (_,(ind,const)) =
+ lb_map := Indmap.add ind const (!lb_map)
+
+let cache_dec (_,(ind,const)) =
+ dec_map := Indmap.add ind const (!dec_map)
+
+let export_bool_leib obj =
+ Some obj
+
+let export_leib_bool obj =
+ Some obj
+
+let export_dec_proof obj =
+ Some obj
+
+
+
+let _ = Summary.declare_summary "bl_proof"
+ { Summary.freeze_function = (fun () -> !bl_map);
+ Summary.unfreeze_function = (fun fs -> bl_map := fs);
+ Summary.init_function = (fun () -> bl_map := Indmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = true}
+
+let find_bl_proof ind =
+ Indmap.find ind !bl_map
+
+let check_bl_proof ind =
+ Indmap.mem ind !bl_map
+
+let _ = Summary.declare_summary "lb_proof"
+ { Summary.freeze_function = (fun () -> !lb_map);
+ Summary.unfreeze_function = (fun fs -> lb_map := fs);
+ Summary.init_function = (fun () -> lb_map := Indmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = true}
+
+let find_lb_proof ind =
+ Indmap.find ind !lb_map
+
+let check_lb_proof ind =
+ Indmap.mem ind !lb_map
+
+let _ = Summary.declare_summary "eq_dec_proof"
+ { Summary.freeze_function = (fun () -> !dec_map);
+ Summary.unfreeze_function = (fun fs -> dec_map := fs);
+ Summary.init_function = (fun () -> dec_map := Indmap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = true}
+
+let find_eq_dec_proof ind =
+ Indmap.find ind !dec_map
+
+let check_dec_proof ind =
+ Indmap.mem ind !dec_map
+
+
+
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
new file mode 100644
index 00000000..2edb294f
--- /dev/null
+++ b/toplevel/ind_tables.mli
@@ -0,0 +1,40 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Term
+open Names
+open Libnames
+open Mod_subst
+open Sign
+
+
+val cache_scheme :(object_name*(Indmap.key*constr)) -> unit
+val export_scheme : (Indmap.key*constr) -> (Indmap.key*constr) option
+
+val find_eq_scheme : Indmap.key -> constr
+val check_eq_scheme : Indmap.key -> bool
+
+val cache_bl: (object_name*(Indmap.key*constr)) -> unit
+val cache_lb: (object_name*(Indmap.key*constr)) -> unit
+val cache_dec : (object_name*(Indmap.key*constr)) -> unit
+
+val export_bool_leib : (Indmap.key*constr) -> (Indmap.key*constr) option
+val export_leib_bool : (Indmap.key*constr) -> (Indmap.key*constr) option
+val export_dec_proof : (Indmap.key*constr) -> (Indmap.key*constr) option
+
+val find_bl_proof : Indmap.key -> constr
+val find_lb_proof : Indmap.key -> constr
+val find_eq_dec_proof : Indmap.key -> constr
+
+val check_bl_proof: Indmap.key -> bool
+val check_lb_proof: Indmap.key -> bool
+val check_dec_proof: Indmap.key -> bool
+
+
+
+
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
@@ -709,11 +801,43 @@ let _ =
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;
optname = "contextual implicit arguments";
optkey = (SecondaryTable ("Contextual","Implicit"));
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;
@@ -725,6 +849,13 @@ let _ =
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;
optname = "implicit arguments printing";
optkey = (SecondaryTable ("Printing","Implicit"));
optread = (fun () -> !Constrextern.print_implicits);
@@ -733,6 +864,14 @@ let _ =
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;
optname = "projection printing using dot notation";
optkey = (SecondaryTable ("Printing","Projections"));
optread = (fun () -> !Constrextern.print_projections);
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:32:52 +0000