From de5bd6a09e2323faf4ac4b7576d55c3d2cb94ba7 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 25 Nov 2012 17:39:12 +0000 Subject: Monomorphization (proof) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/clenv.ml | 10 +++++----- proofs/clenvtac.ml | 2 +- proofs/evar_refiner.ml | 4 ++-- proofs/goal.ml | 9 +++++---- proofs/logic.ml | 42 ++++++++++++++++++++++++++---------------- proofs/pfedit.ml | 2 +- proofs/proof.ml | 6 ++++-- proofs/proof_global.ml | 17 ++++++++++++----- proofs/proofview.ml | 6 ++++-- proofs/redexpr.ml | 4 ++-- proofs/refiner.ml | 9 +++++---- proofs/tacmach.ml | 4 ++-- proofs/tactic_debug.ml | 40 +++++++++++++++++++++++----------------- 13 files changed, 92 insertions(+), 63 deletions(-) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0dbaccc33..ebb1cbcd4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -150,7 +150,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) let mentions clenv mv0 = let rec menrec mv1 = - mv0 = mv1 || + Int.equal mv0 mv1 || let mlist = try match meta_opt_fvalue clenv.evd mv1 with | Some (b,_) -> b.freemetas @@ -445,7 +445,7 @@ let clenv_assign_binding clenv k c = { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = - if bl = [] then + if List.is_empty bl then clenv else let mvs = clenv_independent clenv in @@ -473,17 +473,17 @@ let error_not_right_number_missing_arguments n = int n ++ str ").") let clenv_constrain_dep_args hyps_only bl clenv = - if bl = [] then + if List.is_empty bl then clenv else let occlist = clenv_dependent_gen hyps_only clenv in - if List.length occlist = List.length bl then + if Int.equal (List.length occlist) (List.length bl) then List.fold_left2 clenv_assign_binding clenv occlist bl else if hyps_only then (* Tolerance for compatibility <= 8.3 *) let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in - if List.length occlist' = List.length bl then + if Int.equal (List.length occlist') (List.length bl) then List.fold_left2 clenv_assign_binding clenv occlist' bl else error_not_right_number_missing_arguments (List.length occlist) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ff13cd46a..2c1b9d21f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -52,7 +52,7 @@ let clenv_value_cast_meta clenv = let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent clenv in - if dep_mvs <> [] & not with_evars then + if not (List.is_empty dep_mvs) && not with_evars then raise (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fb8e6b16e..8f7513371 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -17,9 +17,9 @@ open Evarutil (******************************************) let depends_on_evar evk _ (pbty,_,t1,t2) = - try head_evar t1 = evk + try Int.equal (head_evar t1) evk with NoHeadEvar -> - try head_evar t2 = evk + try Int.equal (head_evar t2) evk with NoHeadEvar -> false let define_and_solve_constraints evk c evd = diff --git a/proofs/goal.ml b/proofs/goal.ml index b7be860b5..c076cd676 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp open Term @@ -180,8 +181,8 @@ module Refinable = struct let rec fusion l1 l2 = match l1 , l2 with | [] , _ -> l2 | _ , [] -> l1 - | a::l1 , b::_ when a>b -> a::(fusion l1 l2) - | a::l1 , b::l2 when a=b -> a::(fusion l1 l2) + | a::l1 , b::_ when a > b -> a::(fusion l1 l2) + | a::l1 , b::l2 when Int.equal a b -> a::(fusion l1 l2) | _ , b::l2 -> b::(fusion l1 l2) let update_handle handle init_defs post_defs = @@ -353,7 +354,7 @@ let plus s1 s2 env rdefs goal info = with UndefinedHere -> s2 env rdefs goal info (* Equality of two goals *) -let equal { content = e1 } { content = e2 } = e1 = e2 +let equal { content = e1 } { content = e2 } = Int.equal e1 e2 let here goal value _ _ goal' _ = if equal goal goal' then @@ -426,7 +427,7 @@ let rename_hyp_sign id1 id2 sign = (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) let rename_hyp id1 id2 env rdefs gl info = let hyps = hyps env rdefs gl info in - if id1 <> id2 && + if not (Names.id_eq id1 id2) && List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then Errors.error ((Names.string_of_id id2)^" is already used."); let new_hyps = rename_hyp_sign id1 id2 hyps in diff --git a/proofs/logic.ml b/proofs/logic.ml index 5437d2ba1..725f16b8e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -147,10 +147,10 @@ let find_q x (m,q) = let rec find accs acc = function [] -> raise Not_found | [(x',l)] -> - if x=x' then ((v,Idset.union accs l),(m',List.rev acc)) + if id_eq x x' then ((v,Idset.union accs l),(m',List.rev acc)) else raise Not_found | (x',l as i)::((x'',l'')::q as itl) -> - if x=x' then + if id_eq x x' then ((v,Idset.union accs l), (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q)) else find (Idset.union l accs) (i::acc) itl in @@ -163,7 +163,7 @@ let occur_vars_in_decl env hyps d = let reorder_context env sign ord = let ords = List.fold_right Idset.add ord Idset.empty in - if List.length ord <> Idset.cardinal ords then + if not (Int.equal (List.length ord) (Idset.cardinal ords)) then error "Order list has duplicates"; let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with @@ -211,10 +211,17 @@ let check_decl_position env sign (x,_,_ as d) = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +let move_location_eq m1 m2 = match m1, m2 with +| MoveAfter id1, MoveAfter id2 -> id_eq id1 id2 +| MoveBefore id1, MoveBefore id2 -> id_eq id1 id2 +| MoveLast, MoveLast -> true +| MoveFirst, MoveFirst -> true +| _ -> false + let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | (hyp,_,_) :: right -> - if hyp = h then + if id_eq hyp h then match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst else get_hyp_after h right @@ -223,11 +230,14 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | (hyp,c,typ) as d :: right -> - if hyp = hfrom then - (left,right,d, toleft or hto = MoveLast) + if id_eq hyp hfrom then + (left,right,d, toleft || move_location_eq hto MoveLast) else - splitrec (d::left) - (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) + let is_toleft = match hto with + | MoveAfter h' | MoveBefore h' -> id_eq hyp h' + | _ -> false + in + splitrec (d::left) (toleft || is_toleft) right in splitrec [] false l @@ -249,12 +259,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | (hyp,_,_) :: _ as right when hto = MoveBefore hyp -> + | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) -> List.rev first @ List.rev middle @ right | (hyp,_,_) as d :: right -> let (first',middle') = if List.exists (test_dep d) middle then - if with_dep & hto <> MoveAfter hyp then + if with_dep && not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ @@ -264,7 +274,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = else (d::first, middle) in - if hto = MoveAfter hyp then + if move_location_eq hto (MoveAfter hyp) then List.rev first' @ List.rev middle' @ right else moverec first' middle' right @@ -340,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (** we keep the casts (in particular VMcast) except when they are annotating metas *) if isMeta t then begin - assert (k <> VMcast); + assert (k != VMcast); res end else let (gls,cty,sigma,trm) = res in @@ -526,7 +536,7 @@ let prim_refiner r sigma goal = let rec check_ind env k cl = match kind_of_term (strip_outer_cast cl) with | Prod (na,c1,b) -> - if k = 1 then + if Int.equal k 1 then try fst (find_inductive env sigma c1) with Not_found -> @@ -541,7 +551,7 @@ let prim_refiner r sigma goal = let rec mk_sign sign = function | (f,n,ar)::oth -> let (sp',_) = check_ind env n ar in - if not (sp=sp') then + if not (eq_mind sp sp') then error ("Fixpoints should be on the same " ^ "mutual inductive declaration."); if !check && mem_named_context f (named_context_of_val sign) then @@ -622,7 +632,7 @@ let prim_refiner r sigma goal = check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let (sg,ev,sigma) = mk_goal sign cl' in - let ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev in + let ev = if k != DEFAULTcast then mkCast(ev,k,cl) else ev in let sigma = Goal.V82.partial_solution sigma goal ev in ([sg], sigma) else @@ -669,7 +679,7 @@ let prim_refiner r sigma goal = ([gl], sigma) | Rename (id1,id2) -> - if !check & id1 <> id2 && + if !check && not (id_eq id1 id2) && List.mem id2 (ids_of_named_context (named_context_of_val sign)) then error ((string_of_id id2)^" is already used."); let sign' = rename_hyp id1 id2 sign in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 962061f34..44c5d7f30 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -45,7 +45,7 @@ let current_proof_depth () = let undo_todepth n = try undo ((current_proof_depth ()) - n ) - with Proof_global.NoCurrentProof when n=0 -> () + with Proof_global.NoCurrentProof when Int.equal n 0 -> () let start_proof id str hyps c ?init_tac ?compute_guard hook = let goals = [ (Global.env_of_context hyps , c) ] in diff --git a/proofs/proof.ml b/proofs/proof.ml index bae5f1157..479ccabcc 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -29,6 +29,8 @@ Therefore the undo stack stores action to be ran to undo. *) +open Util + type _focus_kind = int type 'a focus_kind = _focus_kind type focus_info = Obj.t @@ -48,7 +50,7 @@ let new_focus_kind () = r (* Auxiliary function to define conditions. *) -let check kind1 kind2 = kind1=kind2 +let check kind1 kind2 = Int.equal kind1 kind2 (* To be authorized to unfocus one must meet the condition prescribed by the action which focused.*) @@ -85,7 +87,7 @@ module Cond = struct | _ , Cannot e -> Cannot e | Strict, Strict -> Strict | _ , _ -> Loose - let kind e k0 k p = bool e (k0=k) k p + let kind e k0 k p = bool e (Int.equal k0 k) k p let pdone e k p = bool e (Proofview.finished p) k p end diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 25ed1f3e8..9cc726beb 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -14,6 +14,7 @@ (* *) (***********************************************************************) +open Util open Pp open Names @@ -102,7 +103,7 @@ let _ = Errors.register_handler begin function end let extract id l = let rec aux = function - | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l) + | ((id',_) as np)::l when id_eq id id' -> (np,l) | np::l -> let (np', l) = aux l in (np' , np::l) | [] -> raise NoSuchProof in @@ -154,7 +155,7 @@ let msg_proofs () = | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ (pr_sequence Nameops.pr_id l) ++ str".") -let there_is_a_proof () = !current_proof <> [] +let there_is_a_proof () = not (List.is_empty !current_proof) let there_are_pending_proofs () = there_is_a_proof () let check_no_pending_proof () = if not (there_are_pending_proofs ()) then @@ -222,7 +223,7 @@ end let start_proof id str goals ?(compute_guard=[]) hook = begin List.iter begin fun (id_ex,_) -> - if Names.id_ord id id_ex = 0 then raise AlreadyExists + if Names.id_eq id id_ex then raise AlreadyExists end !current_proof end; let p = Proof.start goals in @@ -307,6 +308,12 @@ module Bullet = struct type t = Vernacexpr.bullet + let bullet_eq b1 b2 = match b1, b2 with + | Vernacexpr.Dash, Vernacexpr.Dash -> true + | Vernacexpr.Star, Vernacexpr.Star -> true + | Vernacexpr.Plus, Vernacexpr.Plus -> true + | _ -> false + type behavior = { name : string; put : Proof.proof -> t -> unit @@ -338,7 +345,7 @@ module Bullet = struct let has_bullet bul pr = let rec has_bullet = function - | b'::_ when bul=b' -> true + | b'::_ when bullet_eq bul b' -> true | _::l -> has_bullet l | [] -> false in @@ -358,7 +365,7 @@ module Bullet = struct let put p bul = if has_bullet bul p then Proof.transaction p begin fun () -> - while bul <> pop p do () done; + while not (bullet_eq bul (pop p)) do () done; push bul p end else diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 98e1acc42..a4b914525 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -20,6 +20,8 @@ There is also need of a list of the evars which initialised the proofview to be able to return information about the proofview. *) +open Util + (* Type of proofviews. *) type proofview = { initial : (Term.constr * Term.types) list; @@ -81,7 +83,7 @@ exception IndexOutOfRange Raises [IndexOutOfRange] if [i > length l]*) let list_goto = let rec aux acc index = function - | l when index = 0-> (acc,l) + | l when Int.equal index 0-> (acc,l) | [] -> raise IndexOutOfRange | a::q -> aux (a::acc) (index-1) q in @@ -313,7 +315,7 @@ let tclDISPATCHS tacs = let extend_to_list = let rec copy n x l = if n < 0 then raise SizeMismatch - else if n = 0 then l + else if Int.equal n 0 then l else copy (n-1) x (x::l) in fun startxs rx endxs l -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c16e02b3f..aa3d13f8a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -71,8 +71,8 @@ let map_strategy f l = match f q with Some q' -> q' :: ql | None -> ql) ql [] in - if ql'=[] then str else (lev,ql')::str) l [] in - if l'=[] then None else Some (false,l') + if List.is_empty ql' then str else (lev,ql')::str) l [] in + if List.is_empty l' then None else Some (false,l') let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 78bdc194f..704dd9887 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -355,7 +355,7 @@ let tclIDTAC_list gls = gls let first_goal gls = let gl = gls.it and sig_0 = gls.sigma in - if gl = [] then error "first_goal"; + if List.is_empty gl then error "first_goal"; { it = List.hd gl; sigma = sig_0 } (* goal_goal_list : goal sigma -> goal list sigma *) @@ -398,14 +398,15 @@ let check_evars env sigma extsigma gl = let origsigma = gl.sigma in let rest = Evd.fold_undefined (fun evk evi acc -> - if Evd.is_undefined extsigma evk & not (Evd.mem origsigma evk) then + if Evd.is_undefined extsigma evk && not (Evd.mem origsigma evk) then evi::acc else acc) sigma [] in - if rest <> [] then - let evi = List.hd rest in + match rest with + | [] -> () + | evi :: _ -> let (loc,k) = evi.evar_source in let evi = Evarutil.nf_evar_info sigma evi in Pretype_errors.error_unsolvable_implicit loc env sigma evi k None diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0352d5624..66a9a9962 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -147,11 +147,11 @@ let convert_hyp_no_check d gl = (* This does not check dependencies *) let thin_no_check ids gl = - if ids = [] then tclIDTAC gl else refiner (Thin ids) gl + if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl (* This does not check dependencies *) let thin_body_no_check ids gl = - if ids = [] then tclIDTAC gl else refiner (ThinBody ids) gl + if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl let move_hyp_no_check with_dep id1 id2 gl = refiner (Move (with_dep,id1,id2)) gl diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 10ce0e76b..6f93ab725 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Names open Pp open Tacexpr @@ -69,11 +70,11 @@ let skip = ref 0 let breakpoint = ref None let rec drop_spaces inst i = - if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1) + if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) else i let possibly_unquote s = - if String.length s >= 2 & s.[0] = '"' & s.[String.length s - 1] = '"' then + if String.length s >= 2 & s.[0] == '"' & s.[String.length s - 1] == '"' then String.sub s 1 (String.length s - 2) else s @@ -84,7 +85,7 @@ let db_initialize () = (* Gives the number of steps or next breakpoint of a run command *) let run_com inst = - if (String.get inst 0)='r' then + if (String.get inst 0) == 'r' then let i = drop_spaces inst 1 in if String.length inst > i then let s = String.sub inst i (String.length inst - i) in @@ -135,10 +136,10 @@ let rec prompt level = let debug_prompt lev g tac f = (* What to print and to do next *) let newlevel = - if !skip = 0 then - if !breakpoint = None then (goal_com g tac; prompt lev) + if Int.equal !skip 0 then + if Option.is_empty !breakpoint then (goal_com g tac; prompt lev) else (run false; DebugOn (lev+1)) - else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in + else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in (* What to execute *) try f newlevel with e -> @@ -147,14 +148,19 @@ let debug_prompt lev g tac f = msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); raise e +let is_debug db = match db, !breakpoint with +| DebugOff, _ -> false +| _, Some _ -> false +| _ -> Int.equal !skip 0 + (* Prints a constr *) let db_constr debug env c = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c) (* Prints the pattern rule *) let db_pattern_rule debug num r = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then begin msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++ str "|" ++ spc () ++ !prmatchrl r) @@ -167,38 +173,38 @@ let hyp_bound = function (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str "Hypothesis " ++ str ((Names.string_of_id id)^(hyp_bound ido)^ " has been matched: ") ++ print_constr_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c) (* Prints a success message when the goal has been matched *) let db_mc_pattern_success debug = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++ str "Let us execute the right-hand side part..." ++ fnl()) (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ " cannot match: ") ++ !prmatchpatt env hyp) (* Prints a matching failure message for a rule *) let db_matching_failure debug = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++ str "Let us try the next one...") (* Prints an evaluation failure message for a rule *) let db_eval_failure debug s = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then let s = str "message \"" ++ s ++ str "\"" in msg_tac_debug (str "This rule has failed due to \"Fail\" tactic (" ++ @@ -206,7 +212,7 @@ let db_eval_failure debug s = (* Prints a logic failure message for a rule *) let db_logic_failure debug err = - if debug <> DebugOff & !skip = 0 & !breakpoint = None then + if is_debug debug then begin msg_tac_debug (!explain_logic_error err); msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++ @@ -214,12 +220,12 @@ let db_logic_failure debug err = end let is_breakpoint brkname s = match brkname, s with - | Some s, MsgString s'::_ -> s = s' + | Some s, MsgString s'::_ -> String.equal s s' | _ -> false let db_breakpoint debug s = match debug with - | DebugOn lev when s <> [] & is_breakpoint !breakpoint s -> + | DebugOn lev when not (List.is_empty s) && is_breakpoint !breakpoint s -> breakpoint:=None | _ -> () -- cgit v1.2.3