diff options
Diffstat (limited to 'toplevel')
43 files changed, 999 insertions, 999 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5ddf2b705..3e025b032 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -30,7 +30,7 @@ open Ind_tables (* boolean equality *) -let quick_chop n l = +let quick_chop n l = let rec kick_last = function | t::[] -> [] | t::q -> t::(kick_last q) @@ -39,20 +39,20 @@ and aux = function | (0,l') -> l' | (n,h::t) -> aux (n-1,t) | _ -> failwith "quick_chop" - in + in if n > (List.length l) then failwith "quick_chop args" else kick_last (aux (n,l) ) -let rec deconstruct_type t = +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 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 EqNotFound of string exception EqUnknown of string let dl = dummy_loc @@ -62,28 +62,28 @@ 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 andb_true_intro = fun _ -> + (Coqlib.build_bool_type()).Coqlib.andb_true_intro -let tt = constr_of_global Coqlib.glob_true +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 eq = constr_of_global Coqlib.glob_eq -let sumbool = Coqlib.build_coq_sumbool +let sumbool = Coqlib.build_coq_sumbool -let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb (* reconstruct the inductive with the correct deBruijn indexes *) -let mkFullInd ind n = +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 = + let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - if nparrec > 0 + if nparrec > 0 then mkApp (mkInd ind, Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) else mkInd ind @@ -99,33 +99,33 @@ let make_eq_scheme sp = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in (* params context divided *) - let lnonparrec,lnamesparrec = + 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" + "_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) + 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" + | 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) + 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 ) + 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 *) @@ -134,83 +134,83 @@ let make_eq_scheme sp = (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 + 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 + 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 -> + (* 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 + ndx = how much to translate due to the 2nd Case *) - let compute_A_equality rel_list nlist eqA ndx t = + 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 + | 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 + 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 + 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") + | Lambda _-> raise (EqUnknown "Lambda") | LetIn _ -> raise (EqUnknown "LetIn") - | Const kn -> let mp,dir,lbl= repr_con kn in + | Const kn -> let mp,dir,lbl= repr_con kn in mkConst (make_con mp dir ( - mk_label ("eq_"^(string_of_label lbl)))) + 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") + | 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)) + 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 + bb)) + (List.rev rettyp_l) in (* make_one_eq *) - (* do the [| C1 ... => match Y with ... end - ... + (* 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 + 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 + if (i=j) then ar2.(j) <- let cc = (match nb_cstr_args with | 0 -> tt - | _ -> let eqs = Array.make nb_cstr_args tt in + | _ -> 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 @@ -218,53 +218,53 @@ let make_eq_scheme sp = (nparrec+3+2*nb_cstr_args) (nb_cstr_args+ndx+1) (kind_of_term cc) - in - Array.set eqs ndx + 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)) + 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) - ) + (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)) + 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)) + (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))) + 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 + 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 + 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) + 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" + 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 + 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)^".") + (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 @@ -272,7 +272,7 @@ let make_eq_scheme sp = done; ); res - with + with | EqUnknown s -> error ("Type unexpected ("^s^ ") during boolean eq computation, please report.") | EqNotFound s -> error ("Boolean equality on "^s^ @@ -283,32 +283,32 @@ let make_eq_scheme sp = (* 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 = +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. +(* + 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 + 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 do_replace_lb aavoid narg gls p q = let avoid = Array.of_list aavoid in - let do_arg v offset = - try + let do_arg v offset = + try let x = narg*offset in - let s = destVar v 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) + 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) @@ -317,47 +317,47 @@ let do_replace_lb aavoid narg gls p q = ( 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)) + 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 -> + 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 + let err_msg = msg_with Format.str_formatter (str "Leibniz->boolean:" ++ - str "You have to declare the" ++ + str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr type_of_pq ++ + Printer.pr_constr type_of_pq ++ str " first."); Format.flush_str_formatter () in error err_msg - in let lb_args = Array.append (Array.append + 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 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 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 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) + 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) @@ -366,60 +366,60 @@ let do_replace_bl ind gls aavoid narg lft rgt = ( 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)) + if offset=1 then ("eq_"^(string_of_label lbl)) else ((string_of_label lbl)^"_bl") ))) ) in - let rec aux l1 l2 = + 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 + let u,v = try destruct_ind tt1 (* trick so that the good sequence is returned*) with _ -> ind,[||] - in if u = 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 -> + 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 + let err_msg = msg_with Format.str_formatter (str "boolean->Leibniz:" ++ - str "You have to declare the" ++ + str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr tt1 ++ + Printer.pr_constr tt1 ++ str " first."); Format.flush_str_formatter () in error err_msg - in let bl_args = - Array.append (Array.append + 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 + 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 + 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 _ -> + _ -> (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 _ -> @@ -427,14 +427,14 @@ let do_replace_bl ind gls aavoid narg lft rgt = 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)) + 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 +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'), @@ -445,61 +445,61 @@ let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = (* build the right eq_I A B.. N eq_A .. eq_N *) -let eqI ind l = +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 + 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 compute_bl_goal ind lnamesparrec nparrec = let eqI = eqI ind lnamesparrec in - let list_id = list_id 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 + mkArrow ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) )) - ) list_id in + ) 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 + ) 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 + ) 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 + 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 + 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 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 = + 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 + ( 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 @@ -526,7 +526,7 @@ let compute_bl_tact ind lnamesparrec nparrec = None; intro_using freshz; intros; - tclTRY ( + tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); simpl_in_hyp (freshz,InHyp); @@ -537,9 +537,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). tclTHENSEQ [ simple_apply_in freshz (andb_prop()); fun gl -> - let fresht = fresh_id (!avoid) (id_of_string "Z") gsig + let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in - avoid := fresht::(!avoid); + avoid := fresht::(!avoid); (new_destruct false [Tacexpr.ElimOnConstr ((mkVar freshz,Rawterm.NoBindings))] None @@ -548,30 +548,30 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). dl,Genarg.IntroIdentifier freshz]])) None) gl ]); (* - Ci a1 ... an = Ci b1 ... bn + 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) -> ( + | App (c,ca) -> ( match (kind_of_term c) with - | Ind (i1,i2) -> + | 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 + 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 compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eqI = eqI ind lnamesparrec in let create_input c = @@ -580,43 +580,43 @@ let compute_lb_goal ind lnamesparrec nparrec = let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) )) - ) list_id in + ) 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 + ) 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 + ) 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 + 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 + 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 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 = + 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 + ( 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 @@ -630,20 +630,20 @@ let compute_lb_tact ind lnamesparrec nparrec = Pfedit.by ( tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; - new_induct false [Tacexpr.ElimOnConstr - ((mkVar freshn),Rawterm.NoBindings)] + new_induct false [Tacexpr.ElimOnConstr + ((mkVar freshn),Rawterm.NoBindings)] None (None,None) None; intro_using freshm; - new_destruct false [Tacexpr.ElimOnConstr + new_destruct false [Tacexpr.ElimOnConstr ((mkVar freshm),Rawterm.NoBindings)] None (None,None) None; intro_using freshz; intros; - tclTRY ( + tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); @@ -657,21 +657,21 @@ let compute_lb_tact ind lnamesparrec nparrec = (* 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') -> + | App(c',ca') -> let n = Array.length ca' in - tclTHENSEQ (do_replace_lb (!avoid) - nparrec gls + 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." ) - | _ -> 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 compute_dec_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let create_input c = let x = id_of_string "x" and @@ -679,37 +679,37 @@ let compute_dec_goal ind lnamesparrec nparrec = let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) )) - ) list_id in + ) list_id in let bl_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) )) - ) list_id in + ) 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 + ) 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 + ) 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 + ) 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 + 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 @@ -721,26 +721,26 @@ let compute_dec_goal ind lnamesparrec nparrec = ) ) -let compute_dec_tact ind lnamesparrec nparrec = +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 = + 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 + ( 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); + 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); @@ -749,9 +749,9 @@ let compute_dec_tact ind lnamesparrec nparrec = intros_using [freshn;freshm]; assert_tac (Name freshH) ( mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) - ) ]); + ) ]); (*we do this so we don't have to prove the same goal twice *) - Pfedit.by ( tclTHEN + Pfedit.by ( tclTHEN (new_destruct false [Tacexpr.ElimOnConstr (eqbnm,Rawterm.NoBindings)] None @@ -762,8 +762,8 @@ let compute_dec_tact ind lnamesparrec nparrec = 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)] + new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshH),Rawterm.NoBindings)] None (None,Some (dl,Genarg.IntroOrAndPattern [ [dl,Genarg.IntroAnonymous]; @@ -782,7 +782,7 @@ let compute_dec_tact ind lnamesparrec nparrec = " equality is required.") in - (* left *) + (* left *) Pfedit.by ( tclTHENSEQ [ simplest_left; apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)); Auto.default_auto @@ -794,20 +794,20 @@ let compute_dec_tact ind lnamesparrec nparrec = unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all; - assert_tac (Name freshH3) + assert_tac (Name freshH3) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) ]); - Pfedit.by + 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) + (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 index b8fa1710e..291ce7bb1 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -14,14 +14,14 @@ open Sign val subst_in_constr : (object_name*substitution*(inductive*constr)) - -> (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_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 compute_dec_tact : inductive -> rel_context -> int -> unit val make_eq_scheme :mutual_inductive -> types array diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 4946ee933..cc174ebac 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -18,7 +18,7 @@ open Sign open Libnames (*i*) -(*s +(*s * Automatic detection of (some) record instances *) @@ -30,25 +30,25 @@ type signature = global_reference * evar list * evar_map type instance_decl_function = global_reference -> rel_context -> constr list -> unit -(* +(* * Search algorithm - *) + *) -let rec subst_evar evar def n c = +let rec subst_evar evar def n c = match kind_of_term c with | Evar (e,_) when e=evar -> lift n def | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c -let subst_evar_in_evm evar def evm = +let subst_evar_in_evm evar def evm = Evd.fold - (fun ev evi acc -> - let evar_body = match evi.evar_body with + (fun ev evi acc -> + let evar_body = match evi.evar_body with | Evd.Evar_empty -> Evd.Evar_empty | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in let evar_concl = subst_evar evar def 0 evi.evar_concl in Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl} ) evm empty - + (* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev : * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated * by this definition. *) @@ -59,7 +59,7 @@ let rec safe_define evm ev c = let evi = (Evd.find evm ev) in let define_subst evm sigma = Util.Intmap.fold - ( fun ev (e,c) evm -> + ( fun ev (e,c) evm -> match kind_of_term c with Evar (i,_) when i=ev -> evm | _ -> safe_define evm ev (lift (-List.length e) c) ) sigma evm in @@ -72,7 +72,7 @@ let rec safe_define evm ev c = let evm = subst_evar_in_evm ev c evm in define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u) -let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = +let add_gen_ctx (cl,gen,evm) ctx : signature * constr list = let rec really_new_evar () = let ev = Evarutil.new_untyped_evar() in if Evd.is_evar evm ev then really_new_evar() else ev in @@ -104,7 +104,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = (* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*) let substs = ref SubstSet.empty in try List.iter - ( fun (gr,(pat,_),s) -> + ( fun (gr,(pat,_),s) -> let (_,genl,_) = Termops.decompose_prod_letin pat in let genl = List.map (fun (_,_,t) -> t) genl in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in @@ -146,7 +146,7 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit ( fun (ctx,ev) -> let tyl = List.map (fun (_,_,t) -> t) ctx in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in - let def = applistc c argl in + let def = applistc c argl in (* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_defs evm);*) try if not (Evd.is_defined evm ev) then @@ -155,8 +155,8 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit with Termops.CannotFilter -> () ) evl in aux evm - -let new_inst_no = + +let new_inst_no = let cnt = ref 0 in fun () -> incr cnt; string_of_int !cnt @@ -172,7 +172,7 @@ let new_instance_message ident typ def = open Entries -let rec deep_refresh_universes c = +let rec deep_refresh_universes c = match kind_of_term c with | Sort (Type _) -> Termops.new_Type() | _ -> map_constr deep_refresh_universes c @@ -182,23 +182,23 @@ let declare_record_instance gr ctx params = let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in let ce = { const_entry_body=def; const_entry_type=None; - const_entry_opaque=false; const_entry_boxed=false } in - let cst = Declare.declare_constant ident + const_entry_opaque=false; const_entry_boxed=false } in + let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def -let declare_class_instance gr ctx params = +let declare_class_instance gr ctx params = let ident = make_instance_ident gr in let cl = Typeclasses.class_info gr in let (def,typ) = Typeclasses.instance_constructor cl params in let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in - let ce = Entries.DefinitionEntry + let ce = Entries.DefinitionEntry { const_entry_type=Some typ; const_entry_body=def; - const_entry_opaque=false; const_entry_boxed=false } in + const_entry_opaque=false; const_entry_boxed=false } in try - let cst = Declare.declare_constant ident + let cst = Declare.declare_constant ident (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst); new_instance_message ident typ def @@ -217,16 +217,16 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature ('a * 'b * Term.constr) list * Evd.evar) Gmapl.t ref) = ref Gmapl.empty in iter_under_prod - ( fun ctx typ -> + ( fun ctx typ -> List.iter - (fun ((cl,ev,evm),_,_) -> + (fun ((cl,ev,evm),_,_) -> (* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_defs evm);*) smap := Gmapl.add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; - Gmapl.iter - ( fun (cl,evm) evl -> - let f = if Typeclasses.is_class cl then + Gmapl.iter + ( fun (cl,evm) evl -> + let f = if Typeclasses.is_class cl then declare_class_instance else declare_record_instance in complete_with_evars_permut (cl,[],evm) evl gr_c (fun sign -> complete_signature (k f) sign) @@ -239,15 +239,15 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature let evar_definition evi = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c - -let gen_sort_topo l evm = + +let gen_sort_topo l evm = let iter_evar f ev = let rec aux c = match kind_of_term c with Evar (e,_) -> f e | _ -> iter_constr aux c in aux (Evd.evar_concl (Evd.find evm ev)); if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in - let r = ref [] in + let r = ref [] in let rec dfs ev = iter_evar dfs ev; if not(List.mem ev !r) then r := ev::!r in List.iter dfs l; List.rev !r @@ -258,15 +258,15 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) let evm = Evarutil.nf_evars evm in let gen = gen_sort_topo gen evm in let (evm,gen) = List.fold_right - (fun ev (evm,gen) -> - if Evd.is_defined evm ev - then Evd.remove evm ev,gen + (fun ev (evm,gen) -> + if Evd.is_defined evm ev + then Evd.remove evm ev,gen else evm,(ev::gen)) gen (evm,[]) in (* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*) let ngen = List.length gen in let (_,ctx,evm) = List.fold_left - ( fun (i,ctx,evm) ev -> + ( fun (i,ctx,evm) ev -> let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in (i-1,ctx,evm) @@ -277,7 +277,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) let autoinstance_opt = ref true let search_declaration gr = - if !autoinstance_opt && + if !autoinstance_opt && not (Lib.is_modtype()) then let deftyp = Global.type_of_global gr in complete_signature_with_def gr deftyp declare_instance @@ -301,7 +301,7 @@ let begin_autoinstance () = if not !autoinstance_opt then ( autoinstance_opt := true; ) - + let end_autoinstance () = if !autoinstance_opt then ( autoinstance_opt := false; diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index f9a336430..dfedc178f 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -17,9 +17,9 @@ open Indrec open Lexer let print_loc loc = - if loc = dummy_loc then + if loc = dummy_loc then (str"<unknown>") - else + else let loc = unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) @@ -31,43 +31,43 @@ let where s = (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) let rec explain_exn_default_aux anomaly_string report_fn = function - | Stream.Failure -> + | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") - | Stream.Error txt -> + | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Token.Error txt -> + | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Sys_error msg -> + | Sys_error msg -> hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ()) - | UserError(s,pps) -> + | UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps) - | Out_of_memory -> + | Out_of_memory -> hov 0 (str "Out of memory.") - | Stack_overflow -> + | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") - | Anomaly (s,pps) -> + | Anomaly (s,pps) -> hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) | Match_failure(filename,pos1,pos2) -> - hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ + hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ if Sys.ocaml_version = "3.06" then - (str " from character " ++ int pos1 ++ + (str " from character " ++ int pos1 ++ str " to " ++ int pos2) else (str " at line " ++ int pos1 ++ str " character " ++ int pos2) ++ report_fn ()) - | Not_found -> + | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ()) - | Failure s -> + | Failure s -> hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ()) - | Invalid_argument s -> + | Invalid_argument s -> hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ()) - | Sys.Break -> + | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> - let msg = + 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 -> "=") @@ -75,60 +75,60 @@ let rec explain_exn_default_aux anomaly_string report_fn = function else mt() in hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") - | TypeError(ctx,te) -> + | 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 -> + | InductiveError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) - | RecursionSchemeError e -> + | RecursionSchemeError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () -> explain_exn_default_aux anomaly_string report_fn exc | Proof_type.LtacLocated (s,exc) -> hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () ++ explain_exn_default_aux anomaly_string report_fn exc) - | Cases.PatternMatchingError (env,e) -> + | Cases.PatternMatchingError (env,e) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) - | Tacred.ReductionTacticError e -> + | Tacred.ReductionTacticError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e) - | Logic.RefinerError e -> + | Logic.RefinerError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> hov 0 (str "Error:" ++ spc () ++ str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ + spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") | Nametab.GlobalizationConstantError q -> hov 0 (str "Error:" ++ spc () ++ - str "No constant of this name:" ++ spc () ++ + str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure" ++ + hov 0 (str "Error: Tactic failure" ++ (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++ if i=0 then str "." else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn_default_aux anomaly_string report_fn exc) - | Lexer.Error Illegal_character -> + | Lexer.Error Illegal_character -> hov 0 (str "Syntax error: Illegal character.") - | Lexer.Error Unterminated_comment -> + | Lexer.Error Unterminated_comment -> hov 0 (str "Syntax error: Unterminated comment.") - | Lexer.Error Unterminated_string -> + | Lexer.Error Unterminated_string -> hov 0 (str "Syntax error: Unterminated string.") - | Lexer.Error Undefined_token -> + | Lexer.Error Undefined_token -> hov 0 (str "Syntax error: Undefined token.") - | Lexer.Error (Bad_token s) -> + | Lexer.Error (Bad_token s) -> hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ - (if s <> "" then + (if s <> "" then if Sys.ocaml_version = "3.06" then - (str ("(file \"" ^ s ^ "\", characters ") ++ + (str ("(file \"" ^ s ^ "\", characters ") ++ int b ++ str "-" ++ int e ++ str ")") else (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ @@ -138,7 +138,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function (mt ())) ++ report_fn ()) | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ + hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise) ++ report_fn ()) let anomaly_string () = str "Anomaly: " diff --git a/toplevel/class.ml b/toplevel/class.ml index 11c5bf398..3a3588743 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -50,7 +50,7 @@ let explain_coercion_error g = function | NotAFunction -> (Printer.pr_global g ++ str" is not a function") | NoSource (Some cl) -> - (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " + (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " ++ Printer.pr_global g) | NoSource None -> (str ": cannot find the source class of " ++ Printer.pr_global g) @@ -91,24 +91,24 @@ let check_target clt = function (* condition d'heritage uniforme *) -let uniform_cond nargs lt = +let uniform_cond nargs lt = let rec aux = function | (0,[]) -> true | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l)) | _ -> false - in + in aux (nargs,lt) let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id - | ConstructRef _ as c -> + | ConstructRef _ as c -> errorlabstrm "class_of_global" - (str "Constructors, such as " ++ Printer.pr_global c ++ + (str "Constructors, such as " ++ Printer.pr_global c ++ str ", cannot be used as a class.") -(* +(* lp est la liste (inverse'e) des arguments de la coercion ids est le nom de la classe source sps_opt est le sp de la classe source dans le cas des structures @@ -127,13 +127,13 @@ let get_source lp source = match lp with | [] -> raise Not_found | t1::_ -> find_class_type (Global.env()) Evd.empty t1 - in + in (cl1,lv1,1) | Some cl -> let rec aux = function | [] -> raise Not_found | t1::lt -> - try + try let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in if cl = cl1 then cl1,lv1,(List.length lt+1) else raise Not_found @@ -141,20 +141,20 @@ let get_source lp source = in aux (List.rev lp) let get_target t ind = - if (ind > 1) then + if (ind > 1) then CL_FUN - else + else fst (find_class_type (Global.env()) Evd.empty t) -let prods_of t = +let prods_of t = let rec aux acc d = match kind_of_term d with | Prod (_,c1,c2) -> aux (c1::acc) c2 | Cast (c,_,_) -> aux acc c | _ -> (d,acc) - in + in aux [] t -let strength_of_cl = function +let strength_of_cl = function | CL_CONST kn -> Global | CL_SECVAR id -> Local | _ -> Global @@ -200,7 +200,7 @@ let build_id_coercion idf_opt source = lams in (* juste pour verification *) - let _ = + let _ = if not (Reductionops.is_conv_leq env Evd.empty (Typing.type_of env Evd.empty val_f) typ_f) @@ -229,7 +229,7 @@ let check_source = function | Some (CL_FUN|CL_SORT as s) -> raise (CoercionError (ForbiddenSourceClass s)) | _ -> () -(* +(* nom de la fonction coercion strength de f nom de la classe source (optionnel) @@ -248,7 +248,7 @@ let add_new_coercion_core coef stre source target isid = let llp = List.length lp in if llp = 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = - try + try get_source lp source with Not_found -> raise (CoercionError (NoSource source)) @@ -258,7 +258,7 @@ let add_new_coercion_core coef stre source target isid = raise (CoercionError NotUniform); let clt = try - get_target tg ind + get_target tg ind with Not_found -> raise (CoercionError NoTarget) in @@ -291,7 +291,7 @@ let try_add_new_identity_coercion id stre ~source ~target = let try_add_new_coercion_with_source ref stre ~source = try_add_new_coercion_core ref stre (Some source) None false -let add_coercion_hook stre ref = +let add_coercion_hook stre ref = try_add_new_coercion ref stre; Flags.if_verbose message (string_of_qualid (shortest_qualid_of_global Idset.empty ref) diff --git a/toplevel/class.mli b/toplevel/class.mli index 3bbc2f043..3398e3fab 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -22,7 +22,7 @@ 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 -> locality -> +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 diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 2eeb8a7de..50bcf589b 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -35,13 +35,13 @@ open Entries let typeclasses_db = "typeclass_instances" let _ = - Typeclasses.register_add_instance_hint + Typeclasses.register_add_instance_hint (fun inst pri -> - Flags.silently (fun () -> - Auto.add_hints false [typeclasses_db] + Flags.silently (fun () -> + Auto.add_hints false [typeclasses_db] (Auto.HintsResolveEntry [pri, false, mkConst inst])) ()) - + let declare_instance_cst glob con = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in @@ -50,13 +50,13 @@ let declare_instance_cst glob con = | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_instance glob idl = - let con = + 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_props env n m = mismatched_ctx_inst env Properties n m @@ -68,18 +68,18 @@ let interp_type_evars evdref env ?(impls=([],[])) typ = let typ' = intern_gen true ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ' - + (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr - + let type_ctx_instance evars env ctx inst subst = - let (s, _) = + let (s, _) = List.fold_left2 (fun (subst, instctx) (na, b, t) ce -> let t' = substl subst t in - let c' = - match b with + let c' = + match b with | None -> interp_casted_constr_evars evars env ce t' | Some b -> substl subst b in @@ -93,25 +93,25 @@ 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) -> + | 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 instance_hook k pri global imps ?hook cst = + +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) ~enriching: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 cdecl = let kind = IsDefinition Instance in - let entry = + let entry = { const_entry_body = term; const_entry_type = Some termtype; const_entry_opaque = false; @@ -127,13 +127,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in let evars = ref Evd.empty in - let tclass = + let tclass = match bk with | Implicit -> Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false - (fun avoid (clname, (id, _, t)) -> - match clname with - | Some (cl, b) -> + (fun avoid (clname, (id, _, t)) -> + match clname with + | Some (cl, b) -> let t = CHole (Util.dummy_loc, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) @@ -141,21 +141,21 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) | Explicit -> cl in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in - let k, ctx', imps, subst = + let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let imps, c' = interp_type_evars evars env c in let ctx, c = decompose_prod_assum c' in let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in cl, ctx, imps, List.rev args in - let id = + let id = match snd instid with - Name id -> + 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 -> + | 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 @@ -167,7 +167,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) if Lib.is_modtype () then begin let _, ty_constr = instance_constructor k (List.rev subst) in - let termtype = + let termtype = let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !evars t in @@ -178,49 +178,49 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) end else begin - let props = + let props = match props with - | CRecord (loc, _, fs) -> - if List.length fs > List.length k.cl_props then + | CRecord (loc, _, fs) -> + if List.length fs > List.length k.cl_props then mismatched_props env' (List.map snd fs) k.cl_props; fs - | _ -> - if List.length k.cl_props <> 1 then + | _ -> + if List.length k.cl_props <> 1 then errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] in - let subst = - match k.cl_props with - | [(na,b,ty)] -> - let term = match props with [] -> CHole (Util.dummy_loc, None) + let subst = + match k.cl_props with + | [(na,b,ty)] -> + let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in let ty' = substl subst ty in let c = interp_casted_constr_evars evars env' term ty' in c :: subst | _ -> - let props, rest = + let props, rest = List.fold_left - (fun (props, rest) (id,b,_) -> - try + (fun (props, rest) (id,b,_) -> + try let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); c :: props, rest' - with Not_found -> + with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) ([], props) k.cl_props in - if rest <> [] then + if rest <> [] then unbound_method env' k.cl_impl (fst (List.hd rest)) else type_ctx_instance evars env' k.cl_props props subst in - let subst = List.fold_left2 + let subst = List.fold_left2 (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') [] subst (k.cl_props @ snd k.cl_context) in let app, ty_constr = instance_constructor k subst in - let termtype = + let termtype = let t = it_mkProd_or_LetIn ty_constr ctx' in Evarutil.nf_isevar !evars t in @@ -235,10 +235,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> - Command.start_proof id kind termtype + Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst | _ -> assert false); - if props <> [] then + if props <> [] then Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS !evars) *) (!refine_ref (evm, term)); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); @@ -248,8 +248,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) end let named_of_rel_context l = - let acc, ctx = - List.fold_right + let acc, ctx = + List.fold_right (fun (na, b, t) (subst, ctx) -> let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in let d = (id, Option.map (substl subst) b, substl subst t) in @@ -272,11 +272,11 @@ let context ?(hook=fun _ -> ()) l = let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; - let ctx = try named_of_rel_context fullctx with _ -> + let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in - List.iter (function (id,_,t) -> - if Lib.is_modtype () then + List.iter (function (id,_,t) -> + if Lib.is_modtype () then let cst = Declare.declare_internal_constant id (ParameterEntry (t,false), IsAssumption Logical) in @@ -286,8 +286,8 @@ let context ?(hook=fun _ -> ()) l = hook (ConstRef cst) | None -> () else ( - let impl = List.exists (fun (x,_) -> - match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls + let impl = List.exists (fun (x,_) -> + match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_one_assumption false (Local (* global *), Definitional) t [] impl (* implicit *) false (* inline *) (dummy_loc, id); diff --git a/toplevel/classes.mli b/toplevel/classes.mli index c79eccab8..7a8e9a923 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -43,8 +43,8 @@ val declare_instance_constant : Term.constr -> (* body *) Term.types -> (* type *) Names.identifier - -val new_instance : + +val new_instance : ?global:bool -> (* Not global by default. *) local_binder list -> typeclass_constraint -> @@ -59,9 +59,9 @@ val new_instance : val id_of_class : typeclass -> identifier -(* Context command *) +(* Context command *) -val context : ?hook:(Libnames.global_reference -> unit) -> +val context : ?hook:(Libnames.global_reference -> unit) -> local_binder list -> unit (* Forward ref for refine *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 1da86712d..735e1ff27 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -94,7 +94,7 @@ let definition_message id = let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = let env = Global.env() in match comtypopt with - None -> + None -> let b = abstract_constr_expr com bl in let b, imps = interp_constr_evars_impls env b in imps, @@ -121,7 +121,7 @@ let red_constant_entry bl ce = function | None -> ce | Some red -> let body = ce.const_entry_body in - { ce with const_entry_body = + { ce with const_entry_body = under_binders (Global.env()) (fst (reduction_of_red_expr red)) (local_binders_length bl) body } @@ -150,9 +150,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; - if Pfedit.refining () then - Flags.if_verbose msg_warning - (str"Local definition " ++ pr_id ident ++ + if Pfedit.refining () then + Flags.if_verbose msg_warning + (str"Local definition " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident | (Global|Local) -> @@ -172,12 +172,12 @@ let assumption_message id = let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> - let _ = - declare_variable ident + let _ = + declare_variable ident (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in assumption_message ident; - if is_verbose () & Pfedit.refining () then - msgerrnl (str"Warning: Variable " ++ pr_id ident ++ + if is_verbose () & Pfedit.refining () then + msgerrnl (str"Warning: Variable " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident | (Global|Local) -> @@ -197,7 +197,7 @@ let declare_assumption_hook = ref ignore let set_declare_assumption_hook = (:=) declare_assumption_hook let declare_assumption idl is_coe k bl c impl nl = - if not (Pfedit.refining ()) then + if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in let env = Global.env () in let c', imps = interp_type_evars_impls env c in @@ -213,12 +213,12 @@ open Indrec open Inductiveops -let non_type_eliminations = +let non_type_eliminations = [ (InProp,elimination_suffix InProp); (InSet,elimination_suffix InSet) ] let declare_one_elimination ind = - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Global.lookup_inductive ind in let mindstr = string_of_id mip.mind_typename in let declare s c t = let id = id_of_string s in @@ -227,7 +227,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Definition) in definition_message id; kn @@ -235,13 +235,13 @@ let declare_one_elimination ind = let env = Global.env () in let sigma = Evd.empty in let elim_scheme = Indrec.build_indrec env sigma ind in - let npars = + let npars = (* if a constructor of [ind] contains a recursive call, the scheme is generalized only wrt recursively uniform parameters *) - if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) - then + if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) + then mib.mind_nparams_rec - else + else mib.mind_nparams in let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in let kelim = elim_sorts (mib,mip) in @@ -253,22 +253,22 @@ let declare_one_elimination ind = let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in let c = mkConst cte in let t = type_of_constant (Global.env()) cte in - List.iter (fun (sort,suff) -> - let (t',c') = + List.iter (fun (sort,suff) -> + let (t',c') = Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) npars c t in let _ = declare (mindstr^suff) c' (Some t') in ()) non_type_eliminations else (* Impredicative or logical inductive definition *) List.iter - (fun (sort,suff) -> + (fun (sort,suff) -> if List.mem sort kelim then let elim = make_elim (new_sort_in_family sort) in let _ = declare (mindstr^suff) elim None in ()) non_type_eliminations (* bool eq declaration flag && eq dec declaration flag *) -let eq_flag = ref false +let eq_flag = ref false let _ = declare_bool_option { optsync = true; @@ -278,14 +278,14 @@ let _ = optwrite = (fun b -> eq_flag := b) } (* boolean equality *) -let (inScheme,_) = - 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 (inScheme,_) = + 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 @@ -297,7 +297,7 @@ let declare_eq_scheme sp = let cst_entry = {const_entry_body = eq_array.(i); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } + const_entry_boxed = Flags.boxed_definitions() } in let cst_decl = (DefinitionEntry cst_entry),(IsDefinition Definition) in @@ -305,7 +305,7 @@ let declare_eq_scheme sp = Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst)); definition_message nam done - with Not_found -> + with Not_found -> error "Your type contains Parameters without a boolean equality." (* decidability of eq *) @@ -349,7 +349,7 @@ let adjust_guardness_conditions const = List.map (fun c -> interval 0 (List.length ((lam_assum c)))) (Array.to_list fixdefs) in - let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in + let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in { const with const_entry_body = mkFix ((indexes,0),fixdecls) } | c -> const @@ -380,12 +380,12 @@ let save_named opacity = let const = { const with const_entry_opaque = opacity } in save id const do_guard persistence hook -let make_eq_decidability ind = +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 = + 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 @@ -399,24 +399,24 @@ let make_eq_decidability ind = else ( start_proof (id_of_string bl_name) (Global,Proof Theorem) - (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec) + (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 + 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 + 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) + (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 + Lib.add_anonymous_leaf (inLeibBool (ind,mkConst (Lib.make_con (id_of_string lb_name)))) (* definition_message (id_of_string lb_name) *) ); @@ -424,12 +424,12 @@ let make_eq_decidability ind = then (message (proof_name^" is already declared.")) else ( start_proof (id_of_string proof_name) - (Global,Proof Theorem) + (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 + Lib.add_anonymous_leaf (inDec (ind,mkConst (Lib.make_con (id_of_string proof_name)))) (* definition_message (id_of_string proof_name) *) ) @@ -444,7 +444,7 @@ let declare_eliminations sp = declare_one_elimination (sp,i); try if (!eq_flag) then (make_eq_decidability (sp,i)) - with _ -> + with _ -> Pfedit.delete_current_proof(); message "Error while computing decidability scheme. Please report." done; @@ -455,9 +455,9 @@ let declare_eliminations sp = let compute_interning_datas env ty l nal typl impll = let mk_interning_data na typ impls = let idl, impl = - let impl = + let impl = compute_implicits_with_manual env typ (is_implicit_args ()) impls - in + 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) @@ -465,15 +465,15 @@ let compute_interning_datas env ty l nal typl impll = (na, (ty, idl, impl, compute_arguments_scope typ)) in (l, list_map3 mk_interning_data nal typl impll) - - (* temporary open scopes during interpretation of mutual families - so that locally defined notations are available + + (* temporary open scopes during interpretation of mutual families + so that locally defined notations are available *) let open_temp_scopes = function | None -> () | Some sc -> if not (Notation.scope_is_open sc) then Notation.open_close_scope (false,true,sc) - + let declare_interning_data (_,impls) (df,c,scope) = silently (Metasyntax.add_notation_interpretation df impls c) scope @@ -512,7 +512,7 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | (na,None,t) -> out_name na, LocalAssum t + | (na,None,t) -> out_name na, LocalAssum t | (na,Some b,_) -> out_name na, LocalDef b let interp_ind_arity evdref env ind = @@ -526,12 +526,12 @@ let interp_cstrs evdref env impls mldata arity ind = 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 = +let interp_mutual paramsl indl notations finite = check_all_names_different indl; let env0 = Global.env() in let evdref = ref Evd.empty in - let (env_params, ctx_params), userimpls = - interp_context_evars ~fail_anonymous:false evdref env0 paramsl + let (env_params, ctx_params), userimpls = + interp_context_evars ~fail_anonymous:false evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -552,7 +552,7 @@ let interp_mutual paramsl indl notations finite = let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = - States.with_state_protection (fun () -> + States.with_state_protection (fun () -> (* Temporary declaration of notations and scopes *) List.iter (fun ((_,_,sc) as x ) -> declare_interning_data impls x; @@ -574,7 +574,7 @@ let interp_mutual paramsl indl notations finite = 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,cimpls) -> { mind_entry_typename = ind.ind_name; @@ -582,17 +582,17 @@ let interp_mutual paramsl indl notations finite = mind_entry_consnames = cnames; mind_entry_lc = ctypes }) indl arities constructors in - let impls = + let impls = let len = List.length ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> - indimpls, List.map (fun impls -> + indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = false; - mind_entry_finite = finite; - mind_entry_inds = entries }, + mind_entry_record = false; + mind_entry_finite = finite; + mind_entry_inds = entries }, impls let eq_constr_expr c1 c2 = @@ -622,13 +622,13 @@ let extract_params indl = match paramsl with | [] -> anomaly "empty list of inductive types" | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then error + if not (List.for_all (eq_local_binders params) paramsl) then error "Parameters should be syntactically the same for each inductive type."; params let prepare_inductive ntnl indl = let indl = - List.map (fun ((_,indname),_,ar,lc) -> { + List.map (fun ((_,indname),_,ar,lc) -> { ind_name = indname; ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc @@ -638,7 +638,7 @@ let prepare_inductive ntnl indl = let elim_flag = ref true let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "automatic declaration of eliminations"; optkey = ["Elimination";"Schemes"]; @@ -647,13 +647,13 @@ let _ = 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 - list_iter_i (fun i (indimpls, constrimpls) -> + let (_,kn) = declare_mind isrecord mie in + list_iter_i (fun i (indimpls, constrimpls) -> let ind = (kn,i) in Autoinstance.search_declaration (IndRef ind); maybe_declare_manual_implicits false (IndRef ind) indimpls; list_iter_i - (fun j impls -> + (fun j impls -> (* Autoinstance.search_declaration (ConstructRef (ind,j));*) maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) constrimpls) @@ -677,7 +677,7 @@ let build_mutual l finite = (* 3c| Fixpoints and co-fixpoints *) -let pr_rank = function +let pr_rank = function | 0 -> str "1st" | 1 -> str "2nd" | 2 -> str "3rd" @@ -686,12 +686,12 @@ let pr_rank = function let recursive_message indexes = function | [] -> anomaly "no recursive definition" | [id] -> pr_id id ++ str " is recursively defined" ++ - (match indexes with + (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" ++ - match indexes with + match indexes with | Some a -> spc () ++ str "(decreasing respectively on " ++ prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ str " arguments)" @@ -703,7 +703,7 @@ let corecursive_message _ = function | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ spc () ++ str "are corecursively defined") -let recursive_message isfix = +let recursive_message isfix = if isfix=Fixpoint then recursive_message else corecursive_message (* An (unoptimized) function that maps preorders to partial orders... @@ -728,11 +728,11 @@ let rec partial_order = function | (z, Inr zge) when List.mem x zge -> (z, Inr (list_union zge xge')) | r -> r) res in (x,Inr xge')::res - | y::xge -> - let rec link y = + | y::xge -> + let rec link y = try match List.assoc y res with | Inl z -> link z - | Inr yge -> + | Inr yge -> if List.mem x yge then let res = List.remove_assoc y res in let res = List.map (function @@ -748,13 +748,13 @@ let rec partial_order = function browse res (list_add_set y (list_union xge' yge)) xge with Not_found -> browse res (list_add_set y xge') xge in link y - in browse (partial_order rest) [] xge + in browse (partial_order rest) [] xge let non_full_mutual_message x xge y yge kind rest = - let reason = - if List.mem x yge then + let reason = + if List.mem x yge then string_of_id y^" depends on "^string_of_id x^" but not conversely" - else if List.mem y xge then + else if List.mem y xge then string_of_id x^" depends on "^string_of_id y^" but not conversely" else string_of_id y^" and "^string_of_id x^" are not mutually dependent" in @@ -768,7 +768,7 @@ let non_full_mutual_message x xge y yge kind rest = let check_mutuality env kind fixl = let names = List.map fst fixl in let preorder = - List.map (fun (id,def) -> + List.map (fun (id,def) -> (id, List.filter (fun id' -> id<>id' & occur_var env id' def) names)) fixl in let po = partial_order preorder in @@ -813,7 +813,7 @@ let declare_fix boxed kind f def t imps = Autoinstance.search_declaration (ConstRef kn); maybe_declare_manual_implicits false gr 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 @@ -821,7 +821,7 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = (* Jump over let-bindings. *) -let rel_index n ctx = +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 = @@ -830,16 +830,16 @@ let rec unfold f b = | None -> [] let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = - match n with + match n with | Some (loc, n) -> [rel_index n fixctx] - | None -> + | None -> (* 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 + 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 + unfold (function x when x = len -> None | n -> Some (n, succ n)) 0 let interp_recursive fixkind l boxed = @@ -862,8 +862,8 @@ let interp_recursive fixkind l boxed = let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - States.with_state_protection (fun () -> + let fixdefs = + States.with_state_protection (fun () -> List.iter (fun ((_,_,sc) as x) -> declare_interning_data impls x; open_temp_scopes sc @@ -882,12 +882,12 @@ let interp_recursive fixkind l boxed = (* Build the fix declaration block *) let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let indexes, fixdecls = + let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> - let possible_indexes = + let possible_indexes = list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in - let indexes = search_guard dummy_loc env possible_indexes fixdecls 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 -> None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l @@ -902,30 +902,30 @@ let interp_recursive fixkind l boxed = 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 rec split_scheme l = +let rec split_scheme l = let env = Global.env() in match l with | [] -> [],[] - | (Some id,t)::q -> let l1,l2 = split_scheme q in + | (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 +requested *) | (None,t)::q -> let l1,l2 = split_scheme q in @@ -963,7 +963,7 @@ in ) -let build_induction_scheme lnamedepindsort = +let build_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and sigma = Evd.empty and env0 = Global.env() in @@ -972,10 +972,10 @@ let build_induction_scheme lnamedepindsort = (fun (_,dep,indid,sort) -> let ind = smart_global_inductive indid in let (mib,mip) = Global.lookup_inductive ind in - (ind,mib,mip,dep,interp_elimination_sort sort)) + (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort in - let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in + let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in let decltype = refresh_universes decltype in @@ -985,41 +985,41 @@ let build_induction_scheme lnamedepindsort = const_entry_boxed = Flags.boxed_definitions() } in let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref - in + in let _ = List.fold_right2 declare listdecl lrecnames [] in if_verbose ppnl (recursive_message Fixpoint None lrecnames) -let build_scheme l = +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 <> []) + 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 -> + List.iter ( fun indname -> let ind = smart_global_inductive indname in declare_eq_scheme (fst ind); try - make_eq_decidability ind - with _ -> + 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 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_when: Invalid argument" in aux 0 [] l -let fold_left' f = function +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 nschemes = List.length schemes in *) @@ -1027,17 +1027,17 @@ let build_combined_scheme name schemes = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in match kind_of_term last with - | App (ind, args) -> + | App (ind, args) -> let ind = destInd ind in let (_,spec) = Inductive.lookup_mind_specif env ind in ctx, ind, spec.mind_nrealargs | _ -> ctx, destInd last, 0 in - let defs = - List.map (fun x -> + let defs = + List.map (fun x -> let refe = Ident x in let qualid = qualid_of_reference refe in - let cst = try Nametab.locate_constant (snd qualid) + 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 @@ -1050,18 +1050,18 @@ let build_combined_scheme name schemes = 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 concls = List.rev_map - (fun (_, cst, t) -> + 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 = + let concl_bod, concl_typ = fold_left' - (fun (accb, acct) (cst, x) -> + (fun (accb, acct) (cst, x) -> mkApp (coqconj, [| x; acct; cst; accb |]), mkApp (coqand, [| x; acct |])) concls in - let ctx, _ = - list_split_rev_at prods + 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 @@ -1076,9 +1076,9 @@ let build_combined_scheme name schemes = (* 4.1| Support for mutually proved theorems *) let retrieve_first_recthm = function - | VarRef id -> + | VarRef id -> (pi2 (Global.lookup_named id),variable_opacity id) - | ConstRef cst -> + | ConstRef cst -> let {const_body=body;const_opaque=opaq} = Global.lookup_constant cst in (Option.map Declarations.force body,opaq) | _ -> assert false @@ -1094,7 +1094,7 @@ let compute_proof_name = function | None -> let rec next avoid id = let id = next_global_ident_away false id avoid in - if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id + if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id else id in next (Pfedit.get_all_proof_names ()) default_thm_id @@ -1124,7 +1124,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = let c = SectionLocalDef (body_i, Some t_i, opaq) in let _ = declare_variable id (Lib.cwd(), c, k) in (Local,VarRef id,imps) - | Global -> + | Global -> let const = { const_entry_body = body_i; const_entry_type = Some t_i; @@ -1138,7 +1138,7 @@ let look_for_mutual_statements thms = (* 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 inds = List.map (fun (id,(t,_) as x) -> let (hyps,ccl) = decompose_prod_assum t in let whnf_hyp_hds = map_rel_context_in_env (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) @@ -1169,7 +1169,7 @@ let look_for_mutual_statements thms = (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = list_cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks + if List.for_all (of_same_mutind hyp) oks then Some (hyp::oks) else None) [] ind_ccls in let ordered_same_indccl = List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in @@ -1183,7 +1183,7 @@ let look_for_mutual_statements thms = | indccl::rest, _ -> assert (rest=[]); (* One occ. of common coind ccls and no common inductive hyps *) - if common_same_indhyp <> [] then + if common_same_indhyp <> [] then if_verbose warning "Assuming mutual coinductive statements."; flush_all (); indccl, true @@ -1271,6 +1271,6 @@ let admit () = let get_current_context () = try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> + with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) diff --git a/toplevel/command.mli b/toplevel/command.mli index d648fc10e..14cfef6b2 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -40,17 +40,17 @@ val declare_definition : identifier -> definition_kind -> local_binder list -> red_expr option -> constr_expr -> constr_expr option -> declaration_hook -> unit -val syntax_definition : identifier -> identifier list * constr_expr -> +val syntax_definition : identifier -> identifier list * constr_expr -> bool -> bool -> unit val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> Impargs.manual_explicitation list -> bool (* implicit *) -> 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 -> + coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool -> bool -> unit val open_temp_scopes : Topconstr.scope_name option -> unit @@ -58,7 +58,7 @@ val open_temp_scopes : Topconstr.scope_name option -> unit val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit -val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> +val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> 'a list -> 'b list -> Term.types list ->Impargs.manual_explicitation list list -> 'a list * @@ -69,11 +69,11 @@ val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_ty val check_mutuality : Environ.env -> definition_object_kind -> (identifier * types) list -> unit -val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * +val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : - bool -> Entries.mutual_inductive_entry -> + bool -> Entries.mutual_inductive_entry -> (Impargs.manual_explicitation list * Impargs.manual_explicitation list list) list -> mutual_inductive @@ -91,7 +91,7 @@ type fixpoint_expr = { val recursive_message : definition_object_kind -> int array option -> identifier list -> Pp.std_ppcmds - + val declare_fix : bool -> definition_object_kind -> identifier -> constr -> types -> Impargs.manual_explicitation list -> global_reference @@ -113,7 +113,7 @@ val set_start_hook : (types -> unit) -> unit val start_proof : identifier -> goal_kind -> types -> ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit -val start_proof_com : goal_kind -> +val start_proof_com : goal_kind -> (lident option * (local_binder list * constr_expr)) list -> declaration_hook -> unit diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 729db2d02..4007a96bb 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -32,7 +32,7 @@ let load_rcfile() = if !load_rc then try if !rcfile_specified then - if file_readable_p !rcfile then + if file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else if file_readable_p (!rcfile^"."^Coq_config.version) then @@ -48,7 +48,7 @@ let load_rcfile() = with e -> (msgnl (str"Load of rcfile failed."); raise e) - else + else Flags.if_verbose msgnl (str"Skipping rcfile loading.") (* Puts dir in the path of ML and in the LoadPath *) @@ -64,24 +64,24 @@ let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes (* 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/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" ] @@ -91,24 +91,24 @@ let init_load_path () = let user_contrib = coqlib/"user-contrib" in let dirs = ["states";"plugins"] in (* first user-contrib *) - if Sys.file_exists user_contrib then + if Sys.file_exists user_contrib then Mltop.add_rec_path user_contrib Nameops.default_root_prefix; (* then states, theories 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])) + 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 current directory *) Mltop.add_path "." Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) - List.iter + 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 := [] @@ -116,11 +116,11 @@ let init_library_roots () = find the "include" file in the *source* directory *) let init_ocaml_path () = let coqsrc = Coq_config.coqsrc in - let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) + let add_subdir dl = + Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) in - Mltop.add_ml_dir (Envars.coqlib ()); + Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir - [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; + [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a699e528b..d66e975fc 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -21,7 +21,7 @@ open Coqinit let get_version_date () = try - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib () in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -37,7 +37,7 @@ let output_context = ref false let memory_stat = ref false -let print_memory_stat () = +let print_memory_stat () = if !memory_stat then Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()) @@ -47,7 +47,7 @@ let engagement = ref None let set_engagement c = engagement := Some c let engage () = match !engagement with Some c -> Global.set_engagement c | None -> () - + let set_batch_mode () = batch_mode := true let toplevel_default_name = make_dirpath [id_of_string "Top"] @@ -76,7 +76,7 @@ let set_include d p = let p = dirpath_of_string p in push_include (d,p) let set_rec_include d p = - let p = dirpath_of_string p in + let p = dirpath_of_string p in push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) @@ -84,7 +84,7 @@ let add_load_vernacular verb s = load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list let load_vernacular () = List.iter - (fun (s,b) -> + (fun (s,b) -> if Flags.do_beautify () then with_option beautify_file (Vernac.load_vernac b) s else @@ -93,7 +93,7 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj -let load_vernac_obj () = +let load_vernac_obj () = List.iter (fun f -> Library.require_library_from_file None f None) (List.rev !load_vernacular_obj) @@ -106,7 +106,7 @@ let require () = let compile_list = ref ([] : (bool * string) list) let add_compile verbose s = set_batch_mode (); - Flags.make_silent true; + Flags.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in @@ -142,11 +142,11 @@ let re_exec is_ide = if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let s = if s = "" then if is_native then "opt" else "byte" else s in - let newprog = + let newprog = let dir = Filename.dirname prog in let coqtop = if is_ide then "coqide." else "coqtop." in let com = coqtop ^ s ^ Coq_config.exec_extension in - if dir <> "." then Filename.concat dir com else com + if dir <> "." then Filename.concat dir com else com in Sys.argv.(0) <- newprog; Unix.handle_unix_error (Unix.execvp newprog) Sys.argv @@ -189,12 +189,12 @@ let parse_args is_ide = let glob_opt = ref false in let rec parse = function | [] -> () - | "-with-geoproof" :: s :: rem -> + | "-with-geoproof" :: s :: rem -> if s = "yes" then Coq_config.with_geoproof := true else if s = "no" then Coq_config.with_geoproof := false else usage (); parse rem - | "-impredicative-set" :: rem -> + | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem @@ -221,13 +221,13 @@ let parse_args is_ide = | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem - | "-boot" :: rem -> boot := true; no_load_rc (); parse rem + | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem | "-outputstate" :: s :: rem -> set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | "-nois" :: rem -> set_inputstate ""; parse rem - + | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem | ("-inputstate"|"-is") :: [] -> usage () @@ -237,11 +237,11 @@ let parse_args is_ide = | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem | "-load-ml-source" :: [] -> usage () - | ("-load-vernac-source"|"-l") :: f :: rem -> + | ("-load-vernac-source"|"-l") :: f :: rem -> add_load_vernacular false f; parse rem | ("-load-vernac-source"|"-l") :: [] -> usage () - | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> + | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> add_load_vernacular true f; parse rem | ("-load-vernac-source-verbose"|"-lv") :: [] -> usage () @@ -278,9 +278,9 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Flags.print_emacs := true; + | "-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 | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem @@ -302,7 +302,7 @@ let parse_args is_ide = | "-user" :: u :: rem -> set_rcuser u; parse rem | "-user" :: [] -> usage () - | "-notactics" :: rem -> + | "-notactics" :: rem -> warning "Obsolete option \"-notactics\"."; remove_top_ml (); parse rem @@ -320,7 +320,7 @@ let parse_args is_ide = | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem - | s :: rem -> + | s :: rem -> if is_ide then begin ide_args := s :: !ide_args; parse rem @@ -330,7 +330,7 @@ let parse_args is_ide = in try parse (List.tl (Array.to_list Sys.argv)) - with + with | UserError(_,s) as e -> begin try Stream.empty s; exit 1 @@ -368,10 +368,10 @@ let init is_ide = exit 1 end; if !batch_mode then - (flush_all(); + (flush_all(); if !output_context then Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); - Profile.print_profile (); + Profile.print_profile (); exit 0); Lib.declare_initial_state () diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 6f3edf57f..87f4bdeb5 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -9,14 +9,14 @@ (*i $Id$ i*) (* The Coq main module. The following function [start] will parse the - command line, print the banner, initialize the load path, load the input + command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch [Toplevel.loop]. *) val start : unit -> unit -(* [init_ide] is to be used by the Coq IDE. - It does everything [start] does, except launching the toplevel loop. +(* [init_ide] is to be used by the Coq IDE. + It does everything [start] does, except launching the toplevel loop. It returns the list of Coq files given on the command line. *) val init_ide : unit -> string list diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index dfed4a3be..4c21e4915 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -36,26 +36,26 @@ let detype_param = function *) let abstract_inductive hyps nparams inds = - let ntyp = List.length inds in + let ntyp = List.length inds in let nhyp = named_context_length hyps in let args = instance_from_named_context (List.rev hyps) in let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in let inds' = List.map - (function (tname,arity,cnames,lc) -> + (function (tname,arity,cnames,lc) -> let lc' = List.map (substl subs) lc in let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in (tname,arity',cnames,lc'')) inds in let nparams' = nparams + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_) = List.hd inds' in +(* To be sure to be the same as before, should probably be moved to process_inductive *) + let params' = let (_,arity,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparams' arity in List.map detype_param params in - let ind'' = - List.map + let ind'' = + List.map (fun (a,arity,c,lc) -> let _, short_arity = decompose_prod_n_assum nparams' arity in let shortlc = @@ -70,7 +70,7 @@ let abstract_inductive hyps nparams inds = let process_inductive sechyps modlist mib = let nparams = mib.mind_nparams in - let inds = + let inds = array_map_to_list (fun mip -> let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index c8af4d1da..c6496cd4b 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -13,5 +13,5 @@ open Cooking open Declarations open Entries -val process_inductive : +val process_inductive : named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b005aedf6..99e228dd4 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -369,17 +369,17 @@ let explain_typeclass_resolution env evi k = match k with | GoalEvar | InternalHole | ImplicitArg _ -> (match Typeclasses.class_of_constr evi.evar_concl with - | Some c -> + | Some c -> let env = Evd.evar_env evi in - fnl () ++ str "Could not find an instance for " ++ - pr_lconstr_env env evi.evar_concl ++ + 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 (Some evi) k ++ - explain_unsolvability explain ++ str "." ++ + str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++ + explain_unsolvability explain ++ str "." ++ explain_typeclass_resolution env evi k let explain_var_not_found env id = @@ -418,7 +418,7 @@ let explain_refiner_cannot_generalize env ty = let explain_no_occurrence_found env c id = str "Found no subterm matching " ++ pr_lconstr_env env c ++ - str " in " ++ + str " in " ++ (match id with | Some id -> pr_id id | None -> str"the current goal") ++ str "." @@ -431,9 +431,9 @@ let explain_cannot_unify_binding_type env m n = let explain_cannot_find_well_typed_abstraction env p l = str "Abstracting over the " ++ - str (plural (List.length l) "term") ++ spc () ++ + str (plural (List.length l) "term") ++ spc () ++ hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++ - str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ + str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ str "which is ill-typed." let explain_type_error env err = @@ -490,24 +490,24 @@ let explain_pretype_error env err = | 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 () ++ + str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." -let pr_constr_exprs exprs = - hv 0 (List.fold_right +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 () ++ + str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l let pr_constraints printenv env evm = @@ -516,14 +516,14 @@ let pr_constraints printenv env evm = 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 ()) + let pe = pr_ne_context_of (str "In environment:") (mt ()) (reset_with_named_context evi.evar_hyps env) in (if printenv then pe ++ fnl () else mt ()) ++ - prlist_with_sep (fun () -> fnl ()) + prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l else pr_evar_defs evm - + let explain_unsatisfiable_constraints env evd constr = let evm = Evarutil.nf_evars evd in let undef = Evd.undefined_evars evm in @@ -531,26 +531,26 @@ let explain_unsatisfiable_constraints env evd constr = | None -> str"Unable to satisfy the following constraints:" ++ fnl() ++ pr_constraints true env evm - | Some (ev, k) -> + | Some (ev, k) -> explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++ if List.length (Evd.to_list undef) > 1 then - str"With the following constraints:" ++ fnl() ++ + str"With the following constraints:" ++ fnl() ++ pr_constraints false env (Evd.remove undef ev) else mt () - -let explain_mismatched_contexts env c i j = + +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_rel_context env j) ++ fnl () ++ brk (1,1) ++ + hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ fnl () ++ brk (1,1) ++ hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) -let explain_typeclass_error env err = +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 = @@ -560,7 +560,7 @@ let explain_refiner_bad_type arg ty conclty = str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "." let explain_refiner_unresolved_bindings l = - str "Unable to find an instance for the " ++ + str "Unable to find an instance for the " ++ str (plural (List.length l) "variable") ++ spc () ++ prlist_with_sep pr_coma pr_name l ++ str"." @@ -584,9 +584,9 @@ let explain_non_linear_proof c = spc () ++ str "because a metavariable has several occurrences." let explain_meta_in_type c = - str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++ str " of another meta" - + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t @@ -615,9 +615,9 @@ let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env v in 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 ++ + 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 @@ -663,7 +663,7 @@ let error_large_non_prop_inductive_not_in_type () = let error_not_allowed_case_analysis isrec kind i = str (if isrec then "Induction" else "Case analysis") ++ - strbrk " on sort " ++ pr_sort kind ++ + strbrk " on sort " ++ pr_sort kind ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str "." @@ -801,7 +801,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = | Proof_type.LtacNotationCall s -> quote (str s) | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) | Proof_type.LtacVarCall (id,t) -> - quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ + quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Proof_type.LtacAtomCall (te,otac) -> quote (Pptactic.pr_glob_tactic (Global.env()) @@ -821,7 +821,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = (if unboundvars <> [] or vars <> [] then strbrk " (with " ++ prlist_with_sep pr_coma - (fun (id,c) -> + (fun (id,c) -> pr_id id ++ str ":=" ++ Printer.pr_lconstr c) (List.rev vars @ unboundvars) ++ str ")" else mt())) ++ @@ -832,7 +832,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = let kind_of_last_call = match list_last calls with | (_,Proof_type.LtacConstrInterp _) -> ", last term evaluation failed." | _ -> ", last call failed." in - hov 0 (str "In nested Ltac calls to " ++ + hov 0 (str "In nested Ltac calls to " ++ pr_enum pr_call calls ++ strbrk kind_of_last_call) else mt () diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 8cc179e81..848fec79c 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -29,7 +29,7 @@ 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_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds @@ -41,6 +41,6 @@ val explain_pattern_matching_error : val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds -val explain_ltac_call_trace : +val explain_ltac_call_trace : int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> std_ppcmds diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 5df33d459..49c8ce715 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -11,9 +11,9 @@ open Names open Mod_subst -let eq_scheme_map = ref Indmap.empty +let eq_scheme_map = ref Indmap.empty -let cache_scheme (_,(ind,const)) = +let cache_scheme (_,(ind,const)) = eq_scheme_map := Indmap.add ind const (!eq_scheme_map) let export_scheme obj = @@ -26,10 +26,10 @@ let _ = Summary.declare_summary "eqscheme" Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs); Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty) } -let find_eq_scheme ind = +let find_eq_scheme ind = Indmap.find ind !eq_scheme_map -let check_eq_scheme ind = +let check_eq_scheme ind = Indmap.mem ind !eq_scheme_map let bl_map = ref Indmap.empty @@ -37,13 +37,13 @@ let lb_map = ref Indmap.empty let dec_map = ref Indmap.empty -let cache_bl (_,(ind,const)) = +let cache_bl (_,(ind,const)) = bl_map := Indmap.add ind const (!bl_map) -let cache_lb (_,(ind,const)) = +let cache_lb (_,(ind,const)) = lb_map := Indmap.add ind const (!lb_map) -let cache_dec (_,(ind,const)) = +let cache_dec (_,(ind,const)) = dec_map := Indmap.add ind const (!dec_map) let export_bool_leib obj = @@ -62,7 +62,7 @@ let _ = Summary.declare_summary "bl_proof" Summary.unfreeze_function = (fun fs -> bl_map := fs); Summary.init_function = (fun () -> bl_map := Indmap.empty) } -let find_bl_proof ind = +let find_bl_proof ind = Indmap.find ind !bl_map let check_bl_proof ind = @@ -73,7 +73,7 @@ let _ = Summary.declare_summary "lb_proof" Summary.unfreeze_function = (fun fs -> lb_map := fs); Summary.init_function = (fun () -> lb_map := Indmap.empty) } -let find_lb_proof ind = +let find_lb_proof ind = Indmap.find ind !lb_map let check_lb_proof ind = @@ -84,7 +84,7 @@ let _ = Summary.declare_summary "eq_dec_proof" Summary.unfreeze_function = (fun fs -> dec_map := fs); Summary.init_function = (fun () -> dec_map := Indmap.empty) } -let find_eq_dec_proof ind = +let find_eq_dec_proof ind = Indmap.find ind !dec_map let check_dec_proof ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 2edb294f9..a97c2daaa 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -19,9 +19,9 @@ 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 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 @@ -31,9 +31,9 @@ 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 +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/libtypes.ml b/toplevel/libtypes.ml index c999c0609..fa636989a 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -10,21 +10,21 @@ open Term open Summary open Libobject -(* +(* * Module construction *) - -let reduce c = Reductionops.head_unfold_under_prod + +let reduce c = Reductionops.head_unfold_under_prod (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) (Global.env()) Evd.empty c -module TypeDnet = Term_dnet.Make(struct +module TypeDnet = Term_dnet.Make(struct type t = Libnames.global_reference let compare = Pervasives.compare let subst s gr = fst (Libnames.subst_global s gr) let constr_of = Global.type_of_global end) - (struct let reduce = reduce + (struct let reduce = reduce let direction = false end) type result = Libnames.global_reference * (constr*existential_key) * Termops.subst @@ -36,18 +36,18 @@ let defined_types = ref TypeDnet.empty * Bookeeping & States *) -let freeze () = +let freeze () = (!all_types,!defined_types) -let unfreeze (lt,dt) = - all_types := lt; +let unfreeze (lt,dt) = + all_types := lt; defined_types := dt -let init () = - all_types := TypeDnet.empty; +let init () = + all_types := TypeDnet.empty; defined_types := TypeDnet.empty -let _ = +let _ = declare_summary "type-library-state" { freeze_function = freeze; unfreeze_function = unfreeze; @@ -56,7 +56,7 @@ let _ = let load (_,d) = (* Profile.print_logical_stats !all_types; Profile.print_logical_stats d;*) - all_types := TypeDnet.union d !all_types + all_types := TypeDnet.union d !all_types let subst s t = TypeDnet.subst s t (* @@ -66,18 +66,18 @@ let subst a b = Profile.profile2 subst_key TypeDnet.subst a b let load_key = Profile.declare_profile "load" let load a = Profile.profile1 load_key load a *) -let (input,output) = +let (input,output) = declare_object { (default_object "LIBTYPES") with load_function = (fun _ -> load); subst_function = (fun (_,s,t) -> subst s t); export_function = (fun x -> Some x); - classify_function = (fun x -> Substitute x) + classify_function = (fun x -> Substitute x) } let update () = Lib.add_anonymous_leaf (input !defined_types) -(* +(* * Search interface *) @@ -93,12 +93,12 @@ let add typ gr = let add_key = Profile.declare_profile "add" let add a b = Profile.profile1 add_key add a b *) - -(* - * Hooks declaration + +(* + * Hooks declaration *) -let _ = Declare.add_cache_hook +let _ = Declare.add_cache_hook ( fun sp -> let gr = Nametab.global_of_path sp in let ty = Global.type_of_global gr in diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index be5e9312a..d57ecb948 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -12,8 +12,8 @@ open Term (*i*) -(* - * Persistent library of all declared object, +(* + * Persistent library of all declared object, * indexed by their types (uses Dnets) *) @@ -24,7 +24,7 @@ type result = Libnames.global_reference * (constr*existential_key) * Termops.sub (* this is the reduction function used in the indexing process *) val reduce : types -> types -(* The different types of search available. +(* The different types of search available. * See term_dnet.mli for more explanations *) val search_pattern : types -> result list val search_concl : types -> result list diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml index 9f5d72c5a..a9dcff3e7 100644 --- a/toplevel/line_oriented_parser.ml +++ b/toplevel/line_oriented_parser.ml @@ -12,7 +12,7 @@ let line_oriented_channel_to_option stop_string input_channel = let count = ref 0 in let buff = ref "" in let current_length = ref 0 in - fun i -> + fun i -> if (i - !count) >= !current_length then begin count := !count + !current_length + 1; buff := input_line input_channel; diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 9912f3281..288f1850e 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -115,14 +115,14 @@ let print_grammar = function Gram.Entry.print Pcoq.Constr.operconstr; | "pattern" -> Gram.Entry.print Pcoq.Constr.pattern - | "tactic" -> + | "tactic" -> msgnl (str "Entry tactic_expr is"); Gram.Entry.print Pcoq.Tactic.tactic_expr; msgnl (str "Entry binder_tactic is"); Gram.Entry.print Pcoq.Tactic.binder_tactic; msgnl (str "Entry simple_tactic is"); Gram.Entry.print Pcoq.Tactic.simple_tactic; - | "vernac" -> + | "vernac" -> msgnl (str "Entry vernac is"); Gram.Entry.print Pcoq.Vernac_.vernac; msgnl (str "Entry command is"); @@ -174,7 +174,7 @@ let parse_format (loc,str) = (* Parse " // " *) | '/' when i <= String.length str & str.[i+1] = '/' -> (* We forget the useless n spaces... *) - push_token (UnpCut PpFnl) + push_token (UnpCut PpFnl) (parse_token (close_quotation (i+2))) (* Parse " .. / .. " *) | '/' when i <= String.length str -> @@ -244,10 +244,10 @@ let split_notation_string str = let push_token beg i l = if beg = i then l else let s = String.sub str beg (i - beg) in - String s :: l + String s :: l in let push_whitespace beg i l = - if beg = i then l else WhiteSpace (i-beg) :: l + if beg = i then l else WhiteSpace (i-beg) :: l in let rec loop beg i = if i < String.length str then @@ -271,9 +271,9 @@ let split_notation_string str = (* Interpret notations with a recursive component *) let rec find_pattern xl = function - | Break n as x :: l, Break n' :: l' when n=n' -> + | Break n as x :: l, Break n' :: l' when n=n' -> find_pattern (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when s = s' -> + | Terminal s as x :: l, Terminal s' :: l' when s = s' -> find_pattern (x::xl) (l,l') | [NonTerminal x], NonTerminal x' :: l' -> (x,x',xl),l' @@ -281,7 +281,7 @@ let rec find_pattern xl = function error ("The token "^s^" occurs on one side of \"..\" but not on the other side.") | [NonTerminal _], Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") - | ((SProdList _ | NonTerminal _) :: _ | []), _ -> + | ((SProdList _ | NonTerminal _) :: _ | []), _ -> error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".") let rec interp_list_parser hd = function @@ -293,7 +293,7 @@ let rec interp_list_parser hd = function (* remove the second copy of it afterwards *) (y,x)::yl, x::xl, SProdList (x,sl) :: tl'' | (Terminal _ | Break _) as s :: tl -> - if hd = [] then + if hd = [] then let yl,xl,tl' = interp_list_parser [] tl in yl, xl, s :: tl' else @@ -328,7 +328,7 @@ let rec raw_analyze_notation_tokens = function | WhiteSpace n :: sl -> Break n :: raw_analyze_notation_tokens sl -let is_numeral symbs = +let is_numeral symbs = match List.filter (function Break _ -> false | _ -> true) symbs with | ([Terminal "-"; Terminal x] | [Terminal x]) -> (try let _ = Bigint.of_string x in true with _ -> false) @@ -363,10 +363,10 @@ let remove_extravars extrarecvars (vars,recvars) = error "Two end variables of a recursive notation are not in the same scope." else - List.remove_assoc x l) + List.remove_assoc x l) extrarecvars (List.remove_assoc ldots_var vars) in (vars,recvars) - + (**********************************************************************) (* Build pretty-printing rules *) @@ -457,7 +457,7 @@ let make_hunks etyps symbols from = else if is_operator s then if ws = CanBreak then UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods) - else + else UnpTerminal s :: add_break 1 (make NoBreak prods) else if is_ident_tail s.[String.length s - 1] then let sep = if is_prod_ident (List.hd prods) then "" else " " in @@ -502,14 +502,14 @@ let error_format () = error "The format does not match the notation." let rec split_format_at_ldots hd = function | UnpTerminal s :: fmt when s = string_of_id ldots_var -> List.rev hd, fmt - | u :: fmt -> + | u :: fmt -> check_no_ldots_in_box u; split_format_at_ldots (u::hd) fmt | [] -> raise Exit and check_no_ldots_in_box = function | UnpBox (_,fmt) -> - (try + (try let _ = split_format_at_ldots [] fmt in error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.") with Exit -> ()) @@ -533,7 +533,7 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let hunks_of_format (from,(vars,typs)) symfmt = +let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when s' = String.make (String.length s') ' ' -> @@ -545,7 +545,7 @@ let hunks_of_format (from,(vars,typs)) symfmt = let i = list_index s vars in let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l - | symbs, UnpBox (a,b) :: fmt -> + | symbs, UnpBox (a,b) :: fmt -> let symbs', b' = aux (symbs,b) in let symbs', l = aux (symbs',fmt) in symbs', UnpBox (a,b') :: l @@ -605,7 +605,7 @@ let make_production etyps symbols = l | SProdList (x,sl) -> let sl = List.flatten - (List.map (function Terminal s -> [terminal s] + (List.map (function Terminal s -> [terminal s] | Break _ -> [] | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in let y = match List.assoc x etyps with @@ -624,7 +624,7 @@ let rec find_symbols c_current c_next c_last = function (id, prec) :: (find_symbols c_next c_next c_last sl) | Terminal s :: sl -> find_symbols c_next c_next c_last sl | Break n :: sl -> find_symbols c_current c_next c_last sl - | SProdList (x,_) :: sl' -> + | SProdList (x,_) :: sl' -> (x,c_next)::(find_symbols c_next c_next c_last sl') let border = function @@ -654,13 +654,13 @@ let pr_level ntn (from,args) = let error_incompatible_level ntn oldprec prec = errorlabstrm "" - (str ("Notation "^ntn^" is already defined") ++ spc() ++ - pr_level ntn oldprec ++ - spc() ++ str "while it is now required to be" ++ spc() ++ + (str ("Notation "^ntn^" is already defined") ++ spc() ++ + pr_level ntn oldprec ++ + spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") let cache_one_syntax_extension (prec,ntn,gr,pp) = - try + try let oldprec = Notation.level_of_notation ntn in if prec <> oldprec then error_incompatible_level ntn oldprec prec with Not_found -> @@ -738,13 +738,13 @@ let check_infix_modifiers modifiers = if t <> [] then error "Explicit entry level or type unexpected in infix notation." -let no_syntax_modifiers modifiers = +let no_syntax_modifiers modifiers = modifiers = [] or modifiers = [SetOnlyParsing] (* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = - let typ = try + let typ = try match List.assoc x etyps, typ with | ETConstr (n,()), (_,BorderProd (left,_)) -> ETConstr (n,BorderProd (left,None)) @@ -754,7 +754,7 @@ let set_entry_type etyps (x,typ) = with Not_found -> ETConstr typ in (x,typ) -let check_rule_productivity l = +let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then error "A notation must include at least one symbol."; if (match l with SProdList _ :: _ -> true | _ -> false) then @@ -770,8 +770,8 @@ let find_precedence lev etyps symbols = (try match List.assoc x etyps with | ETConstr _ -> error "The level of the leftmost non-terminal cannot be changed." - | ETName | ETBigint | ETReference -> - if lev = None then + | ETName | ETBigint | ETReference -> + if lev = None then Flags.if_verbose msgnl (str "Setting notation at level 0.") else if lev <> Some 0 then @@ -782,13 +782,13 @@ let find_precedence lev etyps symbols = error "Need an explicit level." else Option.get lev | ETConstrList _ -> assert false (* internally used in grammar only *) - with Not_found -> + with Not_found -> if lev = None then error "A left-recursive notation must have an explicit level." else Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) - -> + -> if lev = None then (Flags.if_verbose msgnl (str "Setting notation at level 0."); 0) else Option.get lev @@ -798,18 +798,18 @@ let find_precedence lev etyps symbols = let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () - with Not_found -> + with Not_found -> error "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved." (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) -let remove_curly_brackets l = +let remove_curly_brackets l = let rec next = function | Break _ :: l -> next l | l -> l in let rec aux deb = function | [] -> [] - | Terminal "{" as t1 :: l -> + | Terminal "{" as t1 :: l -> (match next l with | NonTerminal _ as x :: l' as l0 -> (match next l' with @@ -898,17 +898,17 @@ let contract_notation ntn = if i <= String.length ntn - 5 then let ntn' = if String.sub ntn i 5 = "{ _ }" then - String.sub ntn 0 i ^ "_" ^ + String.sub ntn 0 i ^ "_" ^ String.sub ntn (i+5) (String.length ntn -i-5) else ntn in - aux ntn' (i+1) + aux ntn' (i+1) else ntn in aux ntn 0 exception NoSyntaxRule let recover_syntax ntn = - try + try let prec = Notation.level_of_notation ntn in let pprule,_ = Notation.find_notation_printing_rule ntn in let gr = Egrammar.recover_notation_grammar ntn prec in @@ -926,7 +926,7 @@ let recover_notation_syntax rawntn = (**********************************************************************) (* Main entry point for building parsing and printing rules *) - + let make_pa_rule (n,typs,symbols,_) ntn = let assoc = recompute_assoc typs in let prod = make_production typs symbols in @@ -1035,12 +1035,12 @@ let cache_scope_command o = open_scope_command 1 o let subst_scope_command (_,subst,(scope,o as x)) = match o with - | ScopeClasses cl -> + | ScopeClasses cl -> let cl' = Classops.subst_cl_typ subst cl in if cl'==cl then x else scope, ScopeClasses cl' | _ -> x -let (inScopeCommand,outScopeCommand) = +let (inScopeCommand,outScopeCommand) = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; @@ -1052,5 +1052,5 @@ let (inScopeCommand,outScopeCommand) = let add_delimiters scope key = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) -let add_class_scope scope cl = +let add_class_scope scope cl = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index d9f70610b..53822b473 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -23,7 +23,7 @@ val add_token_obj : string -> unit (* Adding a tactic notation in the environment *) -val add_tactic_notation : +val add_tactic_notation : int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit (* Adding a (constr) notation in the environment*) @@ -46,7 +46,7 @@ val add_notation_interpretation : string -> Constrintern.implicits_env -> (* Add only the parsing/printing rule of a notation *) -val add_syntax_extension : +val add_syntax_extension : locality_flag -> (string * syntax_modifier list) -> unit (* Print the Camlp4 state of a grammar *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index c390c7c52..e33363f3a 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -25,12 +25,12 @@ open Vernacinterp (* Code to hook Coq into the ML toplevel -- depends on having the objective-caml compiler mostly visible. The functions implemented here are: \begin{itemize} - \item [dir_ml_load name]: Loads the ML module fname from the current ML - path. + \item [dir_ml_load name]: Loads the ML module fname from the current ML + path. \item [dir_ml_use]: Directive #use of Ocaml toplevel \item [add_ml_dir]: Directive #directory of Ocaml toplevel \end{itemize} - + How to build an ML module interface with these functions. The idea is that the ML directory path is like the Coq directory path. So we can maintain the two in parallel. @@ -53,13 +53,13 @@ let keep_copy_mlpath path = coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy (* If there is a toplevel under Coq *) -type toplevel = { +type toplevel = { load_obj : string -> unit; use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } -(* Determines the behaviour of Coq with respect to ML files (compiled +(* Determines the behaviour of Coq with respect to ML files (compiled or not) *) type kind_load = | WithTop of toplevel @@ -93,7 +93,7 @@ let ocaml_toploop () = | _ -> () (* Dynamic loading of .cmo/.cma *) -let dir_ml_load s = +let dir_ml_load s = match !load with | WithTop t -> (try t.load_obj s @@ -133,7 +133,7 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path *) -let add_rec_ml_dir dir = +let add_rec_ml_dir dir = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs dir) (* Adding files to Coq and ML loadpath *) @@ -149,8 +149,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> - if_verbose warning + with _ -> + if_verbose warning ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); flush_all (); failwith "caught" @@ -169,14 +169,14 @@ let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = else msg_warning (str ("Cannot open " ^ dir)) -(* convertit un nom quelconque en nom de fichier ou de module *) +(* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = let base = if Filename.check_suffix name ".cmo" then Filename.chop_suffix name ".cmo" - else + else name - in + in String.capitalize base let get_ml_object_suffix name = @@ -227,7 +227,7 @@ let file_of_name name = let stdlib_use_plugins = Coq_config.has_natdynlink (* [known_loaded_module] contains the names of the loaded ML modules - * (linked or loaded with load_object). It is used not to load a + * (linked or loaded with load_object). It is used not to load a * module twice. It is NOT the list of ML modules Coq knows. *) type ml_module_object = { mnames : string list } @@ -264,13 +264,13 @@ let unfreeze_ml_modules x = if has_dynlink then let fname = file_of_name mname in load_object mname fname - else + else errorlabstrm "Mltop.unfreeze_ml_modules" (str"Loading of ML object file forbidden in a native Coq."); add_loaded_module mname) x -let _ = +let _ = Summary.declare_summary "ML-MODULES" { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); @@ -318,7 +318,7 @@ let print_ml_path () = hv 0 (prlist_with_sep pr_fnl pr_str l)) (* Printing of loaded ML modules *) - + let print_ml_modules () = let l = get_loaded_modules () in pp (str"Loaded ML Modules: " ++ pr_vertical_list pr_str l) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 715355635..2b5de5708 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -8,9 +8,9 @@ (*i $Id$ i*) -(* If there is a toplevel under Coq, it is described by the following +(* If there is a toplevel under Coq, it is described by the following record. *) -type toplevel = { +type toplevel = { load_obj : string -> unit; use_file : string -> unit; add_dir : string -> unit; diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index db5a5c4c5..ad1beb553 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -27,7 +27,7 @@ open Vernacexpr let break_happened = ref false -(* Before outputing any data, output_results makes sure that no interrupt +(* Before outputing any data, output_results makes sure that no interrupt is going to disturb the process. *) let output_results_nl stream = let _ = Sys.signal Sys.sigint @@ -36,7 +36,7 @@ let output_results_nl stream = msgnl stream let rearm_break () = - let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun _ -> raise Sys.Break)) in + let _ = Sys.signal Sys.sigint (Sys.Signal_handle(fun _ -> raise Sys.Break)) in () let check_break () = @@ -52,7 +52,7 @@ let global_request_id = ref 013 let acknowledge_command_ref = ref(fun request_id command_count opt_exn -> (fnl () ++ str "acknowledge command number " ++ - int request_id ++ fnl () ++ + int request_id ++ fnl () ++ str "successfully executed " ++ int command_count ++ fnl () ++ str "error message" ++ fnl () ++ (match opt_exn with @@ -76,7 +76,7 @@ let set_start_marker s = start_marker := s; start_length := String.length s; start_marker_buffer := String.make !start_length ' ' - + let set_end_marker s = end_marker := s @@ -89,7 +89,7 @@ let rec parse_one_command_group input_channel = String.blit this_line 0 !start_marker_buffer 0 !start_length; if !start_marker_buffer = !start_marker then let req_id_line = input_line input_channel in - begin + begin (try global_request_id := int_of_string req_id_line with @@ -114,7 +114,7 @@ let rec parse_one_command_group input_channel = None else let first_cmd_status = - try + try raw_do_vernac (Pcoq.Gram.parsable stream_tail); None @@ -126,17 +126,17 @@ let rec parse_one_command_group input_channel = let r = execute_n_commands 0 in (match r with None -> - output_results_nl + output_results_nl (acknowledge_command !global_request_id !count None) | Some(rank, e) -> - (match e with + (match e with | DuringCommandInterp(a,e1) | Stdpp.Exc_located (a,DuringSyntaxChecking e1) -> output_results_nl (acknowledge_command !global_request_id rank (Some e1)) - | e -> + | e -> output_results_nl (acknowledge_command !global_request_id rank (Some e)))); @@ -158,7 +158,7 @@ let protected_loop input_chan = looprec input_chan; end and looprec input_chan = - try + try while true do parse_one_command_group input_chan done with | Vernacexpr.Drop -> raise Vernacexpr.Drop diff --git a/toplevel/record.ml b/toplevel/record.ml index ef3ee5087..152ae5b70 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -39,13 +39,13 @@ let interp_evars evdref env ?(impls=([],[])) k 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, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) - + let interp_fields_evars evars env nots l = List.fold_left2 (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> let impl, t' = interp_evars evars env ~impls Pretyping.IsType t in let b' = Option.map (fun x -> snd (interp_evars evars env ~impls (Pretyping.OfType (Some t')) x)) b in - let impls = + let impls = match i with | Anonymous -> impls | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls) @@ -87,7 +87,7 @@ let typecheck_params_and_fields id t ps nots fs = let degenerate_decl (na,b,t) = let id = match na with | Name id -> id - | Anonymous -> anomaly "Unnamed record variable" in + | Anonymous -> anomaly "Unnamed record variable" in match b with | None -> (id, Entries.LocalAssum t) | Some b -> (id, Entries.LocalDef b) @@ -102,21 +102,21 @@ let warning_or_error coe indsp err = let s,have = if List.length projs > 1 then "s","were" else "","was" in (str(string_of_id fi) ++ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ - prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ + prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ strbrk " not defined.") | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> - (pr_id fi ++ + (pr_id fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ - strbrk " is not.") + strbrk " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> - (pr_id fi ++ + (pr_id fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") - | _ -> + | _ -> (pr_id fi ++ strbrk " cannot be defined because it is not typable.") in if coe then errorlabstrm "structure" st; @@ -139,20 +139,20 @@ let subst_projection fid l c = let rec substrec depth c = match kind_of_term c with | Rel k -> (* We are in context [[params;fields;x:ind;...depth...]] *) - if k <= depth+1 then + if k <= depth+1 then c else if k-depth-1 <= lv then match List.nth l (k-depth-2) with | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> assert false - else + else mkRel (k-lv) | _ -> map_constr_with_binders succ substrec depth c in let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) let c'' = substrec 0 c' in - if !bad_projs <> [] then + if !bad_projs <> [] then raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' @@ -226,14 +226,14 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls in (kinds,sp_projs) let structure_signature ctx = - let rec deps_to_evar evm l = + let rec deps_to_evar evm l = match l with [] -> Evd.empty - | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) + | [(_,_,typ)] -> Evd.add evm (Evarutil.new_untyped_evar()) (Evd.make_evar Environ.empty_named_context_val typ) - | (_,_,typ)::tl -> + | (_,_,typ)::tl -> let ev = Evarutil.new_untyped_evar() in let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in - let new_tl = Util.list_map_i + let new_tl = Util.list_map_i (fun pos (n,c,t) -> n,c, Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in deps_to_evar evm new_tl in @@ -241,7 +241,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields +let declare_structure finite infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = extended_rel_list nfields params in @@ -257,7 +257,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls but isn't *) (* there is probably a way to push this to "declare_mutual" *) begin match finite with - | BiFinite -> + | BiFinite -> if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." | _ -> () @@ -280,8 +280,8 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls let implicits_of_context ctx = list_map_i (fun i name -> - let explname = - match name with + let explname = + match name with | Name n -> Some n | Anonymous -> None in ExplByPos (i, explname), (true, true, true)) @@ -289,11 +289,11 @@ let implicits_of_context ctx = let typeclasses_db = "typeclass_instances" -let qualid_of_con c = +let qualid_of_con c = Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) -let set_rigid c = - Auto.add_hints false [typeclasses_db] +let set_rigid c = + Auto.add_hints false [typeclasses_db] (Auto.HintsTransparencyEntry ([EvalConstRef c], false)) let declare_instance_cst glob con = @@ -305,7 +305,7 @@ let declare_instance_cst glob con = let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = - let fieldimpls = + let fieldimpls = (* Make the class and all params implicits in the projections *) let ctx_impls = implicits_of_context params in let len = succ (List.length params) in @@ -323,19 +323,19 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls const_entry_boxed = false } in let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) + (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 = + 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) + (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; @@ -354,7 +354,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls (List.rev fields) (Recordops.lookup_projections ind)) in let ctx_context = - List.map (fun (na, b, t) -> + List.map (fun (na, b, t) -> match Typeclasses.class_of_constr t with | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*) | None -> None) @@ -366,7 +366,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls cl_props = fields; cl_projs = projs } in - List.iter2 (fun p sub -> + List.iter2 (fun p sub -> if sub then match snd p with Some p -> declare_instance_cst true p | None -> ()) k.cl_projs coers; add_class k; impl @@ -381,7 +381,7 @@ let interp_and_check_sort sort = open Vernacexpr open Autoinstance -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in @@ -394,13 +394,13 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil if not (list_distinct allnames) then error "Two objects have the same name"; (* Now, younger decl in params and fields is on top *) let sc = interp_and_check_sort s in - let implpars, params, implfs, fields = + let implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields idstruc sc ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + match kind with | Class def -> - let gr = declare_class finite def infer (loc,idstruc) idbuild + let gr = declare_class finite def infer (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers sign in if infer then search_record declare_class_instance gr sign; gr diff --git a/toplevel/record.mli b/toplevel/record.mli index 0e23af5c0..b9864f083 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -24,11 +24,11 @@ open Libnames val declare_projections : inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> - bool list -> manual_explicitation list list -> rel_context -> + bool list -> manual_explicitation list list -> rel_context -> (name * bool) list * constant option list -val declare_structure : Decl_kinds.recursivity_kind -> - bool (*infer?*) -> identifier -> identifier -> +val declare_structure : Decl_kinds.recursivity_kind -> + bool (*infer?*) -> identifier -> identifier -> manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *) Impargs.manual_explicitation list list -> rel_context -> (* fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> @@ -39,5 +39,5 @@ val declare_structure : Decl_kinds.recursivity_kind -> val definition_structure : inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list * - (local_decl_expr with_coercion with_notation) list * + (local_decl_expr with_coercion with_notation) list * identifier * constr_expr option -> global_reference diff --git a/toplevel/search.ml b/toplevel/search.ml index 66dc28e2d..8457ef020 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -49,8 +49,8 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let env = Global.env () in let crible_rec (sp,kn) lobj = match object_tag lobj with | "VARIABLE" -> - (try - let (id,_,typ) = Global.lookup_named (basename sp) in + (try + let (id,_,typ) = Global.lookup_named (basename sp) in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then @@ -63,22 +63,22 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ - | "INDUCTIVE" -> - let mib = Global.lookup_mind kn in - (match refopt with + | "INDUCTIVE" -> + let mib = Global.lookup_mind kn in + (match refopt with | Some (IndRef ((kn',tyi) as ind)) when kn=kn' -> print_constructors ind fn env (Array.length (mib.mind_packets.(tyi).mind_user_lc)) | Some _ -> () | _ -> - Array.iteri + Array.iteri (fun i mip -> print_constructors (kn,i) fn env (Array.length mip.mind_user_lc)) mib.mind_packets) | _ -> () - in - try + in + try Declaremods.iter_all_segments crible_rec - with Not_found -> + with Not_found -> () let crible ref = gen_crible (Some ref) @@ -87,17 +87,17 @@ let crible ref = gen_crible (Some ref) exception No_full_path -let rec head c = +let rec head c = let c = strip_outer_cast c in match kind_of_term c with | Prod (_,_,c) -> head c | LetIn (_,_,_,c) -> head c | _ -> c - + let constr_to_full_path c = match kind_of_term c with | Const sp -> sp | _ -> raise No_full_path - + let xor a b = (a or b) & (not (a & b)) let plain_display ref a c = @@ -105,17 +105,17 @@ let plain_display ref a c = let pr = pr_global ref in msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) -let filter_by_module (module_list:dir_path list) (accept:bool) +let filter_by_module (module_list:dir_path list) (accept:bool) (ref:global_reference) _ _ = try let sp = path_of_global ref in let sl = dirpath sp in let rec filter_aux = function | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) - | [] -> true + | [] -> true in xor accept (filter_aux module_list) - with No_full_path -> + with No_full_path -> false let ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0 @@ -129,18 +129,18 @@ let mk_rewrite_pattern2 eq pattern = PApp (PRef eq, [| PMeta None; PMeta None; pattern |]) let pattern_filter pat _ a c = - try + try try - is_matching pat (head c) - with _ -> + is_matching pat (head c) + with _ -> is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) - with UserError _ -> + with UserError _ -> false let filtered_search filter_function display_function ref = crible ref - (fun s a c -> if filter_function s a c then display_function s a c) + (fun s a c -> if filter_function s a c then display_function s a c) let rec id_from_pattern = function | PRef gr -> gr @@ -149,32 +149,32 @@ let rec id_from_pattern = function *) | PApp (p,_) -> id_from_pattern p | _ -> error "The pattern is not simple enough." - + let raw_pattern_search extra_filter display_function pat = let name = id_from_pattern pat in - filtered_search - (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) + filtered_search + (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c) display_function name let raw_search_rewrite extra_filter display_function pattern = filtered_search (fun s a c -> ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) || - (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) + (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) && extra_filter s a c) display_function gref_eq let raw_search_by_head extra_filter display_function pattern = Util.todo "raw_search_by_head" -(* +(* * functions to use the new Libtypes facility *) let raw_search search_function extra_filter display_function pat = let env = Global.env() in - List.iter - (fun (gr,_,_) -> + List.iter + (fun (gr,_,_) -> let typ = Global.type_of_global gr in if extra_filter gr env typ then display_function gr env typ @@ -193,7 +193,7 @@ let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) | l, outside -> filter_by_module l (not outside) -let search_by_head pat inout = +let search_by_head pat inout = text_search_by_head (filter_by_module_from_list inout) pat let search_rewrite pat inout = @@ -204,7 +204,7 @@ let search_pattern pat inout = let gen_filtered_search filter_function display_function = gen_crible None - (fun s a c -> if filter_function s a c then display_function s a c) + (fun s a c -> if filter_function s a c then display_function s a c) (** SearchAbout *) @@ -221,10 +221,10 @@ let search_about_item (itemref,typ) = function let raw_search_about filter_modules display_function l = let filter ref' env typ = filter_modules ref' env typ && - List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && + List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && not (string_string_contains (name_of_reference ref') "_subproof") in gen_filtered_search filter display_function -let search_about ref inout = +let search_about ref inout = raw_search_about (filter_by_module_from_list inout) plain_display ref diff --git a/toplevel/search.mli b/toplevel/search.mli index 96163f7da..cc764fbde 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -25,7 +25,7 @@ type glob_search_about_item = val search_by_head : constr -> dir_path list * bool -> unit val search_rewrite : constr -> dir_path list * bool -> unit val search_pattern : constr -> dir_path list * bool -> unit -val search_about : +val search_about : (bool * glob_search_about_item) list -> dir_path list * bool -> unit (* The filtering function that is by standard search facilities. @@ -39,14 +39,14 @@ val filter_by_module_from_list : They are also used for pcoq. *) val gen_filtered_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> unit -val filtered_search : (global_reference -> env -> constr -> bool) -> +val filtered_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> global_reference -> unit val raw_pattern_search : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_about : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> + (global_reference -> env -> constr -> unit) -> (bool * glob_search_about_item) list -> unit val raw_search_by_head : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 54e491f90..d14acaab9 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -20,7 +20,7 @@ open Protectedtoplevel (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) -type input_buffer = { +type input_buffer = { mutable prompt : unit -> string; mutable str : string; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) @@ -72,7 +72,7 @@ let prompt_char ic ibuf count = ibuf.str.[ibuf.len] <- c; ibuf.len <- ibuf.len + 1; Some c - with End_of_file -> + with End_of_file -> None (* Reinitialize the char stream (after a Drop) *) @@ -94,22 +94,22 @@ let get_bols_of_loc ibuf (bp,ep) = if b < 0 or e < b then anomaly "Bad location"; match lines with | ([],None) -> ([], Some (b,e)) - | (fl,oe) -> ((b,e)::fl, oe) + | (fl,oe) -> ((b,e)::fl, oe) in let rec lines_rec ba after = function | [] -> add_line (0,ba) after | ll::_ when ll <= bp -> add_line (ll,ba) after | ll::fl -> let nafter = if ll < ep then add_line (ll,ba) after else after in - lines_rec ll nafter fl + lines_rec ll nafter fl in let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in (fl,Option.get ll) let dotted_location (b,e) = - if e-b < 3 then + if e-b < 3 then ("", String.make (e-b) ' ') - else + else (String.make (e-b-1) '.', " ") let blanching_string s i n = @@ -127,11 +127,11 @@ let blanching_string s i n = let print_highlight_location ib loc = let (bp,ep) = unloc loc in - let bp = bp - ib.start + let bp = bp - ib.start and ep = ep - ib.start in let highlight_lines = match get_bols_of_loc ib (bp,ep) with - | ([],(bl,el)) -> + | ([],(bl,el)) -> (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++ str"> " ++ str(blanching_string ib.str bl (bp-bl)) ++ str(String.make (ep-bp) '^')) @@ -144,9 +144,9 @@ let print_highlight_location ib loc = prlist (fun (bi,ei) -> (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++ - str sn ++ str dn) in + str sn ++ str dn) in (l1 ++ li ++ ln) - in + in let loc = make_loc (bp,ep) in (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ str":" ++ fnl () ++ highlight_lines ++ fnl ()) @@ -184,7 +184,7 @@ let print_location_in_file s inlibrary fname loc = with e -> (close_in ic; hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()) - + let print_command_location ib dloc = match dloc with | Some (bp,ep) -> @@ -198,10 +198,10 @@ let valid_loc dloc loc = | Some dloc -> let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed | _ -> true - + let valid_buffer_loc ib dloc loc = - valid_loc dloc loc & - let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e + valid_loc dloc loc & + let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing @@ -209,35 +209,35 @@ let valid_buffer_loc ib dloc loc = let make_prompt () = try (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " - with _ -> + with _ -> "Coq < " -(*let build_pending_list l = +(*let build_pending_list l = let pl = ref ">" in let l' = ref l in - let res = - while List.length !l' > 1 do + let res = + while List.length !l' > 1 do pl := !pl ^ "|" Names.string_of_id x; l':=List.tl !l' done in let last = try List.hd !l' with _ -> in "<"^l' -*) +*) (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof backtracking) plus the list of open (nested) proofs (for proof aborting when backtracking). It looks like: - + "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = let statnum = string_of_int (Lib.current_command_label ()) in let dpth = Pfedit.current_proof_depth() in let pending = Pfedit.get_all_proof_names() in - let pendingprompt = - List.fold_left + let pendingprompt = + List.fold_left (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 @@ -248,9 +248,9 @@ let make_emacs_prompt() = * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = - emacs_prompt_startstring() - ^ make_prompt() + let pr() = + emacs_prompt_startstring() + ^ make_prompt() ^ make_emacs_prompt() ^ emacs_prompt_endstring() in @@ -263,7 +263,7 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> + <- (fun () -> emacs_prompt_startstring() ^ prompt () ^ emacs_prompt_endstring()) @@ -287,31 +287,31 @@ let print_toplevel_error exc = | DuringCommandInterp (loc,ie) | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) - | _ -> (None, exc) + | _ -> (None, exc) in let (locstrm,exc) = match exc with | Stdpp.Exc_located (loc, ie) -> if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) - else + else ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) - | _ -> + | _ -> ((mt ()) (* print_command_location top_buffer dloc *), exc) in match exc with - | End_of_input -> + | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 | Vernacexpr.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise Vernacexpr.Drop; (str"Error: There is no ML toplevel." ++ fnl ()) | Vernacexpr.ProtectedLoop -> raise Vernacexpr.ProtectedLoop - | Vernacexpr.Quit -> + | Vernacexpr.Quit -> raise Vernacexpr.Quit - | _ -> + | _ -> (if is_pervasive_exn exc then (mt ()) else locstrm) ++ Cerrors.explain_exn exc @@ -321,14 +321,14 @@ let parse_to_dot = | ("", ".") -> () | ("EOI", "") -> raise End_of_input | _ -> dot st - in + in Gram.Entry.of_parser "Coqtoplevel.dot" dot - + (* We assume that when a lexer error occurs, at least one char was eaten *) let rec discard_to_dot () = - try + try Gram.Entry.parse parse_to_dot top_buffer.tokens - with Stdpp.Exc_located(_,Token.Error _) -> + with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() @@ -336,14 +336,14 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ + | DuringCommandInterp _ | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e | e -> - if is_pervasive_exn e then + if is_pervasive_exn e then e - else - try - discard_to_dot (); e + else + try + discard_to_dot (); e with | End_of_input -> End_of_input | de -> if is_pervasive_exn de then de else e @@ -357,11 +357,11 @@ let do_vernac () = msgerrnl (mt ()); if !print_emacs then msgerr (str (top_buffer.prompt())); resynch_buffer top_buffer; - begin - try + begin + try raw_do_vernac top_buffer.tokens - with e -> - msgnl (print_toplevel_error (process_error e)) + with e -> + msgnl (print_toplevel_error (process_error e)) end; flush_all() @@ -386,7 +386,7 @@ let rec coq_switch b = protected_loop stdin with | Vernacexpr.Drop -> () - | Vernacexpr.ProtectedLoop -> + | Vernacexpr.ProtectedLoop -> Lib.declare_initial_state(); coq_switch false | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0 diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 63a87201b..3f2fa83ad 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -18,7 +18,7 @@ open Pcoq (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) -type input_buffer = { +type input_buffer = { mutable prompt : unit -> string; mutable str : string; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index fcb14b2c6..257660481 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -23,7 +23,7 @@ let print_usage_channel co command = " -I dir -as coqdir map physical dir to logical coqdir -I dir map directory dir to the empty logical path -include dir (idem) - -R dir -as coqdir recursively map physical dir to logical coqdir + -R dir -as coqdir recursively map physical dir to logical coqdir -R dir coqdir (idem) -top coqdir set the toplevel name to be coqdir instead of Top -notop r set the toplevel name to be the empty logical path @@ -35,10 +35,10 @@ let print_usage_channel co command = -outputstate f write state in file f.coq -compat X.Y provides compatibility support for Coq version X.Y - -load-ml-object f load ML object file f - -load-ml-source f load ML file f + -load-ml-object f load ML object file f + -load-ml-source f load ML file f -load-vernac-source f load Coq file f.v (Load f.) - -l f (idem) + -l f (idem) -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.) -lv f (idem) -load-vernac-object f load Coq object file f.vo @@ -88,7 +88,7 @@ options are: (* Print the configuration information *) -let print_config () = +let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ee962334e..a14e8ad45 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -34,7 +34,7 @@ let raise_with_file file exc = match exc with | DuringCommandInterp(loc,e) | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e) - | e -> (dummy_loc,e) + | e -> (dummy_loc,e) in let (inner,inex) = match re with @@ -43,7 +43,7 @@ let raise_with_file file exc = | Stdpp.Exc_located (loc, e) when loc <> dummy_loc -> ((false,file, loc), e) | _ -> ((false,file,cmdloc), re) - in + in raise (Error_in_file (file, inner, disable_drop inex)) let real_error = function @@ -68,7 +68,7 @@ let open_file_twice_if verbosely fname = (in_chan, longfname, (po, verb_ch)) let close_input in_chan (_,verb) = - try + try close_in in_chan; match verb with | Some verb_ch -> close_in verb_ch @@ -88,7 +88,7 @@ let verbose_phrase verbch loc = | _ -> () exception End_of_input - + let parse_phrase (po, verbch) = match Pcoq.Gram.Entry.parse Pcoq.main_entry po with | Some (loc,_ as com) -> verbose_phrase verbch loc; com @@ -133,7 +133,7 @@ let rec vernac_com interpfun (loc,com) = (* end translator state *) (* coqdoc state *) let cds = Dumpglob.coqdoc_freeze() in - if !Flags.beautify_file then + if !Flags.beautify_file then begin let _,f = find_file_in_path ~warn:(Flags.is_verbose()) (Library.get_load_paths ()) @@ -141,7 +141,7 @@ let rec vernac_com interpfun (loc,com) = chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; - begin + begin try read_vernac_file verbosely (make_suffix fname ".v"); if !Flags.beautify_file then close_out !chan_beautify; @@ -149,7 +149,7 @@ let rec vernac_com interpfun (loc,com) = Lexer.restore_com_state cs; Pp.comments := cl; Dumpglob.coqdoc_unfreeze cds - with e -> + with e -> if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Lexer.restore_com_state cs; @@ -157,7 +157,7 @@ let rec vernac_com interpfun (loc,com) = Dumpglob.coqdoc_unfreeze cds; raise e end - + | VernacList l -> List.iter (fun (_,v) -> interp v) l | VernacTime v -> @@ -185,11 +185,11 @@ let rec vernac_com interpfun (loc,com) = | v -> if not !just_parsing then interpfun v - in + in try if do_beautify () then pr_new_syntax loc (Some com); interp com - with e -> + with e -> Format.set_formatter_out_channel stdout; raise (DuringCommandInterp (loc, e)) @@ -199,10 +199,10 @@ and vernac interpfun input = and read_vernac_file verbosely s = Flags.make_warn verbosely; let interpfun = - if verbosely then + if verbosely then Vernacentries.interp - else - Flags.silently Vernacentries.interp + else + Flags.silently Vernacentries.interp in let (in_chan, fname, input) = open_file_twice_if verbosely s in try @@ -239,17 +239,17 @@ let set_xml_end_library f = xml_end_library := f let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; - try + try read_vernac_file verb file; if !Flags.beautify_file then close_out !chan_beautify; - with e -> + with e -> if !Flags.beautify_file then close_out !chan_beautify; 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 = Flags.verbosely Library.start_library f in - if Dumpglob.multi_dump () then + if Dumpglob.multi_dump () then Dumpglob.open_glob_file (f ^ ".glob"); Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); if !Flags.xml_export then !xml_start_library (); diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index f1ea6fa44..4dff36e53 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -41,6 +41,6 @@ val compile : bool -> string -> unit (* Interpret a vernac AST *) -val vernac_com : +val vernac_com : (Vernacexpr.vernac_expr -> unit) -> Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index be7c29bab..c97c24cd1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -72,7 +72,7 @@ let show_proof () = msgnl (str"LOC: " ++ prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ str"Subgoals" ++ fnl () ++ - prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ + prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ pr_ltype ty ++ fnl ()) meta_types ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) @@ -90,7 +90,7 @@ let show_node () = str" " ++ hov 0 (prlist_with_sep pr_fnl pr_goal (List.map goal_of_proof spfl))))) - + let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts @@ -101,9 +101,9 @@ let show_thesis () = msgnl (anomaly "TODO" ) let show_top_evars () = - let pfts = get_pftreestate () in - let gls = top_goal_of_pftreestate pfts in - let sigma = project gls in + let pfts = get_pftreestate () in + let gls = top_goal_of_pftreestate pfts in + let sigma = project gls in msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) let show_prooftree () = @@ -120,38 +120,38 @@ let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in - if all - then - let lid = Tactics.find_intro_names l gl in + if all + then + let lid = Tactics.find_intro_names l gl in msgnl (hov 0 (prlist_with_sep spc pr_id lid)) - else - try + else + try let n = list_last l in msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl))) with Failure "list_last" -> message "" -let id_of_name = function - | Names.Anonymous -> id_of_string "x" +let id_of_name = function + | Names.Anonymous -> id_of_string "x" | Names.Name x -> x (* Building of match expression *) (* From ide/coq.ml *) -let make_cases s = +let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in match glob_ref with - | Libnames.IndRef i -> + | Libnames.IndRef i -> let {Declarations.mind_nparams = np} - , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } + , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in - Util.array_fold_right2 - (fun n t l -> + Util.array_fold_right2 + (fun n t l -> let (al,_) = Term.decompose_prod t in let al,_ = Util.list_chop (List.length al - np) al in - let rec rename avoid = function + let rec rename avoid = function | [] -> [] - | (n,_)::l -> + | (n,_)::l -> let n' = Termops.next_global_ident_away true (id_of_name n) avoid in string_of_id n' :: rename (n'::avoid) l in let al' = rename [] (List.rev al) in @@ -160,18 +160,18 @@ let make_cases s = | _ -> raise Not_found -let show_match id = +let show_match id = try let s = string_of_id (snd id) in let patterns = make_cases s in - let cases = - List.fold_left - (fun acc x -> + let cases = + List.fold_left + (fun acc x -> match x with | [] -> assert false | [x] -> "| "^ x ^ " => \n" ^ acc - | x::l -> - "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" + | x::l -> + "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")" ^ " => \n" ^ acc) "end" patterns in msg (str ("match # with\n" ^ cases)) @@ -196,7 +196,7 @@ let print_modules () = and loaded = Library.loaded_libraries () in let loaded_opened = list_intersect loaded opened and only_loaded = list_subtract loaded opened in - str"Loaded and imported library files: " ++ + str"Loaded and imported library files: " ++ pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ str"Loaded and not imported library files: " ++ pr_vertical_list pr_dirpath only_loaded @@ -213,7 +213,7 @@ let print_module r = with Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid) -let print_modtype r = +let print_modtype r = let (loc,qid) = qualid_of_reference r in try let kn = Nametab.locate_modtype qid in @@ -226,7 +226,7 @@ let dump_universes s = try Univ.dump_universes output (Global.universes ()); close_out output; - msgnl (str ("Universes written to file \""^s^"\".")) + msgnl (str ("Universes written to file \""^s^"\".")) with e -> close_out output; raise e @@ -237,7 +237,7 @@ let locate_file f = try let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in msgnl (str file) - with Not_found -> + with Not_found -> msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++ str"on loadpath")) @@ -256,7 +256,7 @@ let msg_notfound_library loc qid = function strbrk "Cannot find a physical path bound to logical path " ++ pr_dirpath dir ++ str".") | Library.LibNotFound -> - msgnl (hov 0 + msgnl (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str".")) | e -> assert false @@ -265,18 +265,18 @@ let print_located_library r = try msg_found_library (Library.locate_qualified_library false qid) with e -> msg_notfound_library loc qid e -let print_located_module r = +let print_located_module r = let (loc,qid) = qualid_of_reference r in let msg = - try + try let dir = Nametab.full_name_module qid in str "Module " ++ pr_dirpath dir with Not_found -> (if fst (repr_qualid qid) = empty_dirpath then str "No module is referred to by basename " - else + else str "No module is referred to by name ") ++ pr_qualid qid - in msgnl msg + in msgnl msg let smart_global r = let gr = Smartlocate.smart_global r in @@ -290,7 +290,7 @@ let vernac_syntax_extension = Metasyntax.add_syntax_extension let vernac_delimiters = Metasyntax.add_delimiters -let vernac_bind_scope sc cll = +let vernac_bind_scope sc cll = List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll let vernac_open_close_scope = Notation.open_close_scope @@ -319,19 +319,19 @@ let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = (str "Proof editing mode not supported in module types.") else let hook _ _ = () in - start_proof_and_print (local,DefinitionBody Definition) + 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 - | Some r -> + | Some r -> let (evc,env)= Command.get_current_context () in Some (interp_redexp env evc r) in declare_definition id k bl red_option c typ_opt hook) - + let vernac_start_proof kind l lettop hook = if Dumpglob.dump () then - List.iter (fun (id, _) -> + List.iter (fun (id, _) -> match id with | Some lid -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; @@ -365,18 +365,18 @@ let vernac_exact_proof c = else errorlabstrm "Vernacentries.ExactProof" (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.") - + let vernac_assumption kind l nl= let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> + List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then - List.iter (fun lid -> - if global then Dumpglob.dump_definition lid false "ax" + List.iter (fun lid -> + if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; declare_assumption idl is_coe kind [] c false nl) l - + let vernac_record k finite infer struc binders sort nameopt cfs = - let const = match nameopt with + let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> Dumpglob.dump_definition lid false "constr"; id in @@ -387,11 +387,11 @@ let vernac_record k finite infer struc binders sort nameopt cfs = | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); ignore(Record.definition_structure (k,finite,infer,struc,binders,cfs,const,sort)) - -let vernac_inductive finite infer indl = + +let vernac_inductive finite infer indl = if Dumpglob.dump () then List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> - match cstrs with + match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; List.iter (fun (_, (lid, _)) -> @@ -399,28 +399,28 @@ let vernac_inductive finite infer indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; match indl with - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> + | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> vernac_record (match b with Class true -> Class false | _ -> b) finite infer id bl c oc fs - | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> - let f = + | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> + let f = let (coe, ((loc, id), ce)) = l in ((coe, AssumExpr ((loc, Name id), ce)), None) in vernac_record (Class true) finite infer id bl c None [f] - | [ ( id , bl , c , Class true, _), _ ] -> + | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" | [ ( id , bl , c , Class false, Constructors _), _ ] -> Util.error "Inductive classes not supported" - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> + | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> Util.error "where clause not supported for (co)inductive records" - | _ -> let unpack = function + | _ -> let unpack = function | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn | _ -> Util.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in Command.build_mutual indl (recursivity_flag_of_kind finite) -let vernac_fixpoint l b = +let vernac_fixpoint l b = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_recursive l b @@ -438,13 +438,13 @@ let vernac_combined_scheme = build_combined_scheme (* Modules *) let vernac_import export refl = - let import ref = + let import ref = Library.import_module export (qualid_of_reference ref) in List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export (loc, 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 @@ -456,15 +456,15 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = "Remove the \"Export\" and \"Import\" keywords from every functor " ^ "argument.") else (idl,ty)) binders_ast in - let mp = Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr id binders_ast (Some mty_ast_o) None - in + in Dumpglob.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 -let vernac_define_module export (loc, 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 @@ -478,10 +478,10 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = Declaremods.start_module Modintern.interp_modtype export - id binders_ast mty_ast_o + id binders_ast mty_ast_o in Dumpglob.dump_moddef loc mp "mod"; - if_verbose message + if_verbose message ("Interactive Module "^ string_of_id id ^" started") ; List.iter (fun (export,id) -> @@ -496,12 +496,12 @@ let vernac_define_module export (loc, 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 - let mp = Declaremods.declare_module + let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast mty_ast_o mexpr_ast_o + id binders_ast mty_ast_o mexpr_ast_o in Dumpglob.dump_moddef loc mp "mod"; - if_verbose message + if_verbose message ("Module "^ string_of_id id ^" is defined"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export @@ -515,7 +515,7 @@ let vernac_end_module export (loc,id as lid) = 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 (); @@ -526,14 +526,14 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = ([],[]) in let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose message + if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport - + | Some base_mty -> let binders_ast = List.map (fun (export,idl,ty) -> @@ -542,23 +542,23 @@ let vernac_declare_module_type (loc,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 - let mp = Declaremods.declare_modtype Modintern.interp_modtype + let mp = Declaremods.declare_modtype Modintern.interp_modtype id binders_ast base_mty in Dumpglob.dump_moddef loc mp "modtype"; - if_verbose message + if_verbose message ("Module Type "^ string_of_id id ^" is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.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 *) @@ -570,7 +570,7 @@ let vernac_begin_section (_, id as lid) = Lib.open_section id let vernac_end_section (loc,_) = - Dumpglob.dump_reference loc + Dumpglob.dump_reference loc (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () @@ -611,7 +611,7 @@ let vernac_identity_coercion stre id qids qidt = Class.try_add_new_identity_coercion id stre source target (* Type classes *) - + let vernac_instance glob sup inst props pri = Dumpglob.dump_constraint inst false "inst"; ignore(Classes.new_instance ~global:glob sup inst props pri) @@ -631,12 +631,12 @@ let vernac_solve n tcom b = error "Unknown command of the non proof-editing mode."; Decl_mode.check_not_proof_mode "Unknown proof instruction"; begin - if b then + if b then solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) else solve_nth n (Tacinterp.hide_interp tcom None) end; - (* in case a strict subtree was completed, - go back to the top of the prooftree *) + (* in case a strict subtree was completed, + go back to the top of the prooftree *) if subtree_solved () then begin Flags.if_verbose msgnl (str "Subgoal proved"); make_focus 0; @@ -648,9 +648,9 @@ let vernac_solve n tcom b = (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof machine, and enables to instantiate existential variables when - there are no more goals to solve. It cannot be a tactic since + there are no more goals to solve. It cannot be a tactic since all tactics fail if there are no further goals to prove. *) - + let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = @@ -662,9 +662,9 @@ let vernac_set_end_tac tac = (***********************) (* Proof Language Mode *) -let vernac_decl_proof () = +let vernac_decl_proof () = check_not_proof_mode "Already in Proof Mode"; - if tree_solved () then + if tree_solved () then error "Nothing left to prove here." else begin @@ -672,17 +672,17 @@ let vernac_decl_proof () = print_subgoals () end -let vernac_return () = +let vernac_return () = match get_current_mode () with Mode_tactic -> Decl_proof_instr.return_from_tactic_mode (); print_subgoals () - | Mode_proof -> + | Mode_proof -> error "\"return\" is only used after \"escape\"." - | Mode_none -> - error "There is no proof to end." + | Mode_none -> + error "There is no proof to end." -let vernac_proof_instr instr = +let vernac_proof_instr instr = Decl_proof_instr.proof_instr instr; print_subgoals () @@ -753,7 +753,7 @@ let vernac_backto n = Lib.reset_label n let vernac_declare_tactic_definition = Tacinterp.add_tacdef -let vernac_create_hintdb local id b = +let vernac_create_hintdb local id b = Auto.create_hint_db local id full_transparent_state b let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h) @@ -761,12 +761,12 @@ let vernac_hints local lb h = Auto.add_hints local lb (Auto.interp_hints h) let vernac_syntactic_definition lid = Dumpglob.dump_definition lid false "syndef"; Command.syntax_definition (snd lid) - + let vernac_declare_implicits local r = function | Some imps -> Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (fun (ex,b,f) -> ex, (b,true,f)) imps) - | None -> + | None -> Impargs.declare_implicits local (smart_global r) let vernac_reserve idl c = @@ -775,12 +775,12 @@ let vernac_reserve idl c = List.iter (fun id -> Reserve.declare_reserved_type id t) idl let make_silent_if_not_pcoq b = - if !pcoq <> None then + if !pcoq <> None then error "Turning on/off silent flag is not supported in Pcoq mode." else make_silent b let _ = - declare_bool_option + declare_bool_option { optsync = false; optname = "silent"; optkey = ["Silent"]; @@ -788,7 +788,7 @@ let _ = optwrite = make_silent_if_not_pcoq } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; @@ -796,7 +796,7 @@ let _ = optwrite = Impargs.make_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; @@ -804,7 +804,7 @@ let _ = optwrite = Impargs.make_strict_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; @@ -812,7 +812,7 @@ let _ = optwrite = Impargs.make_strongly_strict_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; @@ -828,7 +828,7 @@ let _ = (* optwrite = Impargs.make_forceable_implicit_args } *) let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; @@ -836,7 +836,7 @@ let _ = optwrite = Impargs.make_reversible_pattern_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; @@ -844,7 +844,7 @@ let _ = optwrite = Impargs.make_maximal_implicit_args } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; @@ -852,14 +852,14 @@ let _ = optwrite = (fun b -> Constrextern.print_coercions := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); optwrite = (:=) Constrextern.print_evar_arguments } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; @@ -867,7 +867,7 @@ let _ = optwrite = (fun b -> Constrextern.print_implicits := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; @@ -875,7 +875,7 @@ let _ = optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; @@ -883,7 +883,7 @@ let _ = optwrite = (fun b -> Constrextern.print_projections := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "notations printing"; optkey = ["Printing";"Notations"]; @@ -891,7 +891,7 @@ let _ = optwrite = (fun b -> Constrextern.print_no_symbol := not b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "raw printing"; optkey = ["Printing";"All"]; @@ -899,7 +899,7 @@ let _ = optwrite = (fun b -> Flags.raw_print := b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of virtual machine inside the kernel"; optkey = ["Virtual";"Machine"]; @@ -907,20 +907,20 @@ let _ = optwrite = (fun b -> Vconv.set_use_vm b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of boxed definitions"; optkey = ["Boxed";"Definitions"]; optread = Flags.boxed_definitions; - optwrite = (fun b -> Flags.set_boxed_definitions b) } + optwrite = (fun b -> Flags.set_boxed_definitions b) } let _ = - declare_bool_option + declare_bool_option { optsync = true; optname = "use of boxed values"; optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); - optwrite = (fun b -> Vm.set_transp_values (not b)) } + optwrite = (fun b -> Vm.set_transp_values (not b)) } let _ = declare_int_option @@ -1061,7 +1061,7 @@ let vernac_print = function | PrintModuleType qid -> print_modtype qid | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () - | PrintName qid -> + | PrintName qid -> if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) @@ -1098,7 +1098,7 @@ let vernac_print = function let global_module r = let (loc,qid) = qualid_of_reference r in try Nametab.full_name_module qid - with Not_found -> + with Not_found -> user_err_loc (loc, "global_module", str "Module/section " ++ pr_qualid qid ++ str " not found.") @@ -1117,12 +1117,12 @@ let interp_search_about_item = function | SearchString (s,None) when is_ident s -> GlobSearchString s | SearchString (s,sc) -> - try + try let ref = Notation.interp_notation_as_global_reference dummy_loc (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) - with UserError _ -> + with UserError _ -> error ("Unable to interp \""^s^"\" either as a reference or as an identifier component") @@ -1162,7 +1162,7 @@ let vernac_goal = function let unnamed_kind = Lemma (* Arbitrary *) in start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->()); print_subgoals () - end else + end else error "repeated Goal not permitted in refining mode." let vernac_abort = function @@ -1207,14 +1207,14 @@ let vernac_backtrack snum pnum naborts = Pp.flush_all(); (* there may be no proof in progress, even if no abort *) (try print_subgoals () with UserError _ -> ()) - + let vernac_focus gln = check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; - match gln with + match gln with | None -> traverse_nth_goal 1; print_subgoals () | Some n -> traverse_nth_goal n; print_subgoals () - + (* Reset the focus to the top of the tree *) let vernac_unfocus () = check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; @@ -1231,7 +1231,7 @@ let apply_subproof f occ = let evc = evc_of_pftreestate pts in let rec aux pts = function | [] -> pts - | (n::l) -> aux (Tacmach.traverse n pts) occ in + | (n::l) -> aux (Tacmach.traverse n pts) occ in let pts = aux pts (occ@[-1]) in let pf = proof_of_pftreestate pts in f evc (Global.named_context()) pf @@ -1270,14 +1270,14 @@ let vernac_check_guard () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts in let (pfterm,_) = extract_open_pftreestate pts in - let message = - try + let message = + try Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) - pfterm; + pfterm; (str "The condition holds up to here") - with UserError(_,s) -> + with UserError(_,s) -> (str ("Condition violated: ") ++s) - in + in msgnl message let interp c = match c with @@ -1308,11 +1308,11 @@ let interp c = match c with | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) - | VernacDeclareModule (export,lid,bl,mtyo) -> + | VernacDeclareModule (export,lid,bl,mtyo) -> vernac_declare_module export lid bl mtyo - | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> + | VernacDefineModule (export,lid,bl,mtyo,mexpro) -> vernac_define_module export lid bl mtyo mexpro - | VernacDeclareModuleType (lid,bl,mtyo) -> + | VernacDeclareModuleType (lid,bl,mtyo) -> vernac_declare_module_type lid bl mtyo | VernacInclude (in_ast) -> vernac_include in_ast @@ -1340,7 +1340,7 @@ let interp c = match c with | VernacDeclProof -> vernac_decl_proof () | VernacReturn -> vernac_return () - | VernacProofInstr stp -> vernac_proof_instr stp + | VernacProofInstr stp -> vernac_proof_instr stp (* /MMode *) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 300ff44f8..44e8b7ab4 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -54,4 +54,4 @@ val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit -val vernac_reset_name : identifier Util.located -> unit +val vernac_reset_name : identifier Util.located -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 080acc7fc..56fbd192b 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -31,7 +31,7 @@ type lstring = string type lreference = reference type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation - + type printable = | PrintTables | PrintFullContext @@ -164,7 +164,7 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_coercion with_notation list type inductive_expr = - lident with_coercion * local_binder list * constr_expr option * inductive_kind * + lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type module_binder = bool option * lident list * module_type_ast @@ -196,13 +196,13 @@ type vernac_expr = | VernacTime of vernac_expr | VernacTimeout of int * vernac_expr - (* Syntax *) + (* Syntax *) | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list) | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * lstring | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of locality_flag * reference or_by_notation * + | VernacArgumentsScope of locality_flag * reference or_by_notation * scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * constr_expr * scope_name option @@ -211,9 +211,9 @@ type vernac_expr = scope_name option (* Gallina *) - | VernacDefinition of definition_kind * lident * definition_expr * + | VernacDefinition of definition_kind * lident * definition_expr * declaration_hook - | VernacStartTheoremProof of theorem_kind * + | VernacStartTheoremProof of theorem_kind * (lident option * (local_binder list * constr_expr)) list * bool * declaration_hook | VernacEndProof of proof_end @@ -232,12 +232,12 @@ type vernac_expr = export_flag option * specif_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of reference or_by_notation - | VernacCoercion of locality * reference or_by_notation * + | VernacCoercion of locality * reference or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of locality * lident * + | VernacIdentityCoercion of locality * lident * class_rawexpr * class_rawexpr - (* Type classes *) + (* Type classes *) | VernacInstance of bool * (* global *) local_binder list * (* super *) @@ -246,16 +246,16 @@ type vernac_expr = int option (* Priority *) | VernacContext of local_binder list - + | VernacDeclareInstance of lident (* instance name *) (* Modules and Module Types *) - | VernacDeclareModule of bool option * lident * + | VernacDeclareModule of bool option * lident * module_binder list * (module_type_ast * bool) - | VernacDefineModule of bool option * lident * + | VernacDefineModule of bool option * lident * module_binder list * (module_type_ast * bool) option * module_ast option - | VernacDeclareModuleType of lident * + | VernacDeclareModuleType of lident * module_binder list * module_type_ast option | VernacInclude of include_ast @@ -297,7 +297,7 @@ type vernac_expr = | VernacHints of locality_flag * lstring list * hints_expr | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) * locality_flag * onlyparsing_flag - | VernacDeclareImplicits of locality_flag * reference or_by_notation * + | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr | VernacSetOpacity of @@ -345,7 +345,7 @@ and located_vernac_expr = loc * vernac_expr exception DuringSyntaxChecking of exn -let syntax_checking_error s = +let syntax_checking_error s = raise (DuringSyntaxChecking (UserError ("",Pp.str s))) (* Managing locality *) @@ -366,7 +366,7 @@ let use_locality_full () = r let use_locality () = - match use_locality_full () with Some true -> true | _ -> false + match use_locality_full () with Some true -> true | _ -> false let use_locality_exp () = local_of_bool (use_locality ()) @@ -374,16 +374,16 @@ let use_section_locality () = match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened () let use_non_locality () = - match use_locality_full () with Some false -> false | _ -> true + match use_locality_full () with Some false -> false | _ -> true let enforce_locality () = let local = - match !locality_flag with + match !locality_flag with | Some false -> error "Cannot be simultaneously Local and Global." - | _ -> + | _ -> Flags.if_verbose - Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; + Pp.warning "Obsolete syntax: use \"Local\" as a prefix."; true in locality_flag := None; local @@ -391,8 +391,8 @@ let enforce_locality () = let enforce_locality_exp () = local_of_bool (enforce_locality ()) let enforce_locality_of local = - let local = - match !locality_flag with + let local = + match !locality_flag with | Some false when local -> error "Cannot be simultaneously Local and Global." | Some true when local -> diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 8520686d6..211d20d39 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -27,24 +27,24 @@ let vernac_tab = (string, Tacexpr.raw_generic_argument list -> unit -> unit) Hashtbl.t) let vinterp_add s f = - try + try Hashtbl.add vernac_tab s f with Failure _ -> errorlabstrm "vinterp_add" (str"Cannot add the vernac command " ++ str s ++ str" twice.") let overwriting_vinterp_add s f = - begin - try - let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s + begin + try + let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s with Not_found -> () end; Hashtbl.add vernac_tab s f let vinterp_map s = - try + try Hashtbl.find vernac_tab s - with Not_found -> + with Not_found -> errorlabstrm "Vernac Interpreter" (str"Cannot find vernac command " ++ str s ++ str".") diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 95c2f45d6..7adc74930 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -13,11 +13,11 @@ open Tacexpr (*i*) (* Interpretation of extended vernac phrases. *) - + val disable_drop : exn -> exn val vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit -val overwriting_vinterp_add : +val overwriting_vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit val vinterp_init : unit -> unit diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index b7db4b431..dac56e7d6 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -30,7 +30,7 @@ open Refiner open Tacmach open Syntax_def -(* Coq interface to the Whelp query engine developed at +(* Coq interface to the Whelp query engine developed at the University of Bologna *) let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080" @@ -39,7 +39,7 @@ let getter_server_name = ref "http://mowgli.cs.unibo.it:58081" open Goptions let _ = - declare_string_option + declare_string_option { optsync = false; optname = "Whelp server"; optkey = ["Whelp";"Server"]; @@ -47,7 +47,7 @@ let _ = optwrite = (fun s -> whelp_server_name := s) } let _ = - declare_string_option + declare_string_option { optsync = false; optname = "Whelp getter"; optkey = ["Whelp";"Getter"]; @@ -61,7 +61,7 @@ let make_whelp_request req c = let b = Buffer.create 16 let url_char c = - if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or + if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or '0' <= c & c <= '9' or c ='.' then Buffer.add_char b c else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) @@ -71,7 +71,7 @@ let url_string s = String.iter url_char s let rec url_list_with_sep sep f = function | [] -> () | [a] -> f a - | a::l -> f a; url_string sep; url_list_with_sep sep f l + | a::l -> f a; url_string sep; url_list_with_sep sep f l let url_id id = url_string (string_of_id id) @@ -81,10 +81,10 @@ let uri_of_dirpath dir = let error_whelp_unknown_reference ref = let qid = Nametab.shortest_qualid_of_global Idset.empty ref in errorlabstrm "" - (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ + (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ strbrk ", are not supported in Whelp.") -let uri_of_repr_kn ref (mp,dir,l) = +let uri_of_repr_kn ref (mp,dir,l) = match mp with | MPfile sl -> uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl) @@ -109,7 +109,7 @@ let uri_of_global ref = | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".") | ConstRef cst -> uri_of_repr_kn ref (repr_con cst); url_string ".con" - | IndRef (kn,i) -> + | IndRef (kn,i) -> uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1] | ConstructRef ((kn,i),j) -> uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j] @@ -124,7 +124,7 @@ let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c let uri_params f = function | [] -> () - | l -> url_string "\\subst"; + | l -> url_string "\\subst"; url_bracket (url_list_with_sep ";" (uri_of_binding f)) l let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) @@ -151,7 +151,7 @@ let rec uri_of_constr c = | _ -> url_paren (fun () -> match c with | RApp (_,f,args) -> let inst,rest = merge (section_parameters f) args in - uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; + uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; url_list_with_sep " " uri_of_constr rest | RLambda (_,na,k,ty,c) -> url_string "\\lambda "; url_of_name na; url_string ":"; @@ -170,7 +170,7 @@ let rec uri_of_constr c = error "Whelp does not support pattern-matching and (co-)fixpoint." | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) -> anomaly "Written w/o parenthesis" - | RPatVar _ | RDynamic _ -> + | RPatVar _ | RDynamic _ -> anomaly "Found constructors not supported in constr") () let make_string f x = Buffer.reset b; f x; Buffer.contents b @@ -192,7 +192,7 @@ let whelp_constr_expr req c = let whelp_locate s = send_whelp "locate" s -let whelp_elim ind = +let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) let on_goal f = @@ -215,13 +215,13 @@ VERNAC ARGUMENT EXTEND whelp_constr_request 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 (Smartlocate.global_inductive_with_alias r) ] +| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] +| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END VERNAC COMMAND EXTEND WhelpHint -| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] +| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] +| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index 4ad615a62..2f1621a7a 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -8,7 +8,7 @@ (*i $Id$ i*) -(* Coq interface to the Whelp query engine developed at +(* Coq interface to the Whelp query engine developed at the University of Bologna *) open Names |