From: Claudio Sacerdoti Coen Date: Thu, 27 Dec 2018 00:19:15 +0000 (+0100) Subject: Most warnings turned into errors and avoided X-Git-Tag: make_still_working~229^2~1^2~12 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3df31c02806eca83c63c14e6a89844f764c3e2cb Most warnings turned into errors and avoided --- diff --git a/matita/components/Makefile.common b/matita/components/Makefile.common index 7a4727c76..922a0e132 100644 --- a/matita/components/Makefile.common +++ b/matita/components/Makefile.common @@ -20,7 +20,7 @@ endif PREPROCOPTIONS = -pp camlp5o SYNTAXOPTIONS = -syntax camlp5o PREREQ = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7 OCAMLDEBUGOPTIONS = -g #OCAML_PROF=p -p a OCAMLARCHIVEOPTIONS = diff --git a/matita/components/content/notationEnv.ml b/matita/components/content/notationEnv.ml index be9171a8d..164fec0e8 100644 --- a/matita/components/content/notationEnv.ml +++ b/matita/components/content/notationEnv.ml @@ -93,7 +93,7 @@ let lookup_list env name = | ty, _ -> raise (Type_mismatch (name, ty)) let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) -let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) +let opt_binding_none (n, (ty, _v)) = (n, (OptType ty, OptValue None)) let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None)) let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) let opt_declaration (n, ty) = (n, OptType ty) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index 369a0fa28..038d75d9c 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -110,7 +110,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t = (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) (pp_patterns status patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) - | Ast.LetIn ((var,t2), t1, t3) -> + | Ast.LetIn ((var,_t2), t1, t3) -> (* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) sprintf "let %s \\def %s in %s" (pp_term var) (* (pp_term ~pp_parens:true t2) *) @@ -251,8 +251,8 @@ and pp_variable = function | Ast.NumVar s -> "number " ^ s | Ast.IdentVar s -> "ident " ^ s | Ast.TermVar (s,Ast.Self _) -> s - | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l - | Ast.Ascription (t, n) -> assert false + | Ast.TermVar (_s,Ast.Level l) -> "term " ^string_of_int l + | Ast.Ascription (_t, _n) -> assert false | Ast.FreshVar n -> "fresh " ^ n let _pp_term = ref (pp_term ~pp_parens:false) diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 82096f80b..02530eff5 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -111,7 +111,7 @@ let visit_variable k = function | Ast.Ascription (t, s) -> Ast.Ascription (k t, s) let variables_of_term t = - let rec vars = ref [] in + let vars = ref [] in let add_variable v = if List.mem v !vars then () else vars := v :: !vars @@ -145,7 +145,7 @@ let names_of_term t = List.map aux (variables_of_term t) let keywords_of_term t = - let rec keywords = ref [] in + let keywords = ref [] in let add_keyword k = keywords := k :: !keywords in let rec aux = function | Ast.AttributedTerm (_, t) -> aux t @@ -166,7 +166,7 @@ let rec strip_attributes t = | Ast.AttributedTerm (_, term) -> strip_attributes term | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m) | Ast.Variable _ as t -> t - | t -> assert false + | _t -> assert false in visit_ast ~special_k strip_attributes t @@ -177,7 +177,7 @@ let rec get_idrefs = | _ -> [] let meta_names_of_term term = - let rec names = ref [] in + let names = ref [] in let add_name n = if List.mem n !names then () else names := n :: !names @@ -186,7 +186,7 @@ let meta_names_of_term term = | Ast.AttributedTerm (_, term) -> aux term | Ast.Appl terms -> List.iter aux terms | Ast.Binder (_, _, body) -> aux body - | Ast.Case (term, indty, outty_opt, patterns) -> + | Ast.Case (term, _indty, outty_opt, patterns) -> aux term ; aux_opt outty_opt ; List.iter aux_branch patterns @@ -218,7 +218,7 @@ let meta_names_of_term term = aux term and aux_pattern = function - Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars + Ast.Pattern (_head, _, vars) -> List.iter aux_capture_var vars | Ast.Wildcard -> () and aux_substs substs = List.iter (fun (_, term) -> aux term) substs and aux_meta_substs meta_substs = List.iter aux_opt meta_substs @@ -350,8 +350,8 @@ let rec freshen_term ?(index = ref 0) term = | _ -> assert false in match term with - | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ()) - | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ()) + | Ast.Symbol (s, _instance) -> Ast.Symbol (s, fresh_instance ()) + | Ast.Num (s, _instance) -> Ast.Num (s, fresh_instance ()) | t -> visit_ast ~special_k freshen_term t let freshen_obj obj = diff --git a/matita/components/content_pres/Makefile b/matita/components/content_pres/Makefile index 1f4ede959..28d403a70 100644 --- a/matita/components/content_pres/Makefile +++ b/matita/components/content_pres/Makefile @@ -16,19 +16,15 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) -cicNotationPres.cmi: OCAMLOPTIONS += -rectypes -cicNotationPres.cmo: OCAMLOPTIONS += -rectypes -cicNotationPres.cmx: OCAMLOPTIONS += -rectypes - all: clean: LOCAL_LINKOPTS = -package helm-content_pres -linkpkg cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) -cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) +cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) -w -27 cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) -cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) +cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) -w -27 cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) diff --git a/matita/components/content_pres/boxPp.ml b/matita/components/content_pres/boxPp.ml index 45c8b6c20..1d99a8bb0 100644 --- a/matita/components/content_pres/boxPp.ml +++ b/matita/components/content_pres/boxPp.ml @@ -136,15 +136,15 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let spacing = want_spacing attrs in let children' = List.map aux_box children in (fun size -> - let (size', renderings) as res = + let (size', _renderings) as res = render_row max_size spacing children' in if size' <= size then (* children fit in a row *) res else (* break needed, re-render using a Box.V *) aux_box (Box.V (attrs, children)) size) - | Box.V (attrs, []) -> assert false - | Box.V (attrs, [child]) -> aux_box child + | Box.V (_attrs, []) -> assert false + | Box.V (_attrs, [child]) -> aux_box child | Box.V (attrs, hd :: tl) -> let indent = want_indent attrs in let hd_f = aux_box hd in @@ -163,8 +163,8 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = in let rows = hd_rendering @ List.concat tl_renderings in max_len rows, rows) - | Box.HOV (attrs, []) -> assert false - | Box.HOV (attrs, [child]) -> aux_box child + | Box.HOV (_attrs, []) -> assert false + | Box.HOV (_attrs, [child]) -> aux_box child | Box.HOV (attrs, children) -> let spacing = want_spacing attrs in let indent = want_indent attrs in @@ -216,7 +216,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = let href = try let _,_,href = - List.find (fun (ns,na,value) -> ns = Some "xlink" && na = "href") attrs + List.find (fun (ns,na,_value) -> ns = Some "xlink" && na = "href") attrs in Some href with Not_found -> None in @@ -240,7 +240,7 @@ let render_to_strings ~map_unicode_to_tex choose_action size markup = in fixed_rendering href s | Pres.Mspace _ -> fixed_rendering href string_space - | Pres.Mrow (attrs, children) -> + | Pres.Mrow (_attrs, children) -> let children' = List.map aux_mpres children in (fun size -> render_row size false children') | Pres.Mfrac (_, m, n) -> diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 1e6860281..8c7460346 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -189,8 +189,8 @@ let extract_term_production status pattern = and aux_magic magic = match magic with | Ast.Opt p -> - let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : NotationEnv.t option) (loc : Ast.location) = + let _p_bindings, p_atoms, p_names, p_action = inner_pattern p in + let action (env_opt : NotationEnv.t option) (_loc : Ast.location) = match env_opt with | Some env -> List.map Env.opt_binding_some env | None -> List.map Env.opt_binding_of_name p_names diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml index 04440ffe7..fe9b5f869 100644 --- a/matita/components/content_pres/cicNotationPres.ml +++ b/matita/components/content_pres/cicNotationPres.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - module Ast = NotationPt module Mpres = Mpresentation @@ -194,7 +192,7 @@ let add_parens child_prec curr_prec t = match t with | Mpresentation.Mobject (_, box) -> mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ])) - | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren]) + | _mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren]) end else ((*prerr_endline ("NOT adding parens around: "^ BoxPp.render_to_string (function x::_->x|_->assert false) @@ -311,7 +309,7 @@ let render status ~lookup_uri ?(prec=(-1)) = | t -> prerr_endline ("unexpected ast: " ^ NotationPp.pp_term status t); assert false - and aux_attributes xmlattrs mathonly xref prec t = + and aux_attributes _xmlattrs mathonly _xref prec t = let reset = ref false in let inferred_level = ref None in let expected_level = ref None in @@ -352,7 +350,7 @@ let render status ~lookup_uri ?(prec=(-1)) = in (* prerr_endline (NotationPp.pp_term t); *) aux_attribute t - and aux_literal xmlattrs xref prec l = + and aux_literal xmlattrs xref _prec l = let attrs = make_href xmlattrs xref in (match l with | `Symbol s -> Mpres.Mo (attrs, to_unicode s) diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index 880024ad9..7918772f4 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -85,7 +85,7 @@ let make_args_for_apply term2pres args = let make_arg_for_apply is_first arg row = let res = match arg with - Con.Aux n -> assert false + Con.Aux _n -> assert false | Con.Premise prem -> let name = (match prem.Con.premise_binder with @@ -404,16 +404,16 @@ and conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude = (match p.Con.premise_binder with | None -> assert false; (* unnamed hypothesis ??? *) | Some s -> B.Text([],s)) - | err -> assert false) in + | _err -> assert false) in (match conclude.Con.conclude_conclusion with None -> B.b_h [] [B.b_kw "by"; B.b_space; arg] - | Some c -> + | Some _c -> B.b_h [] [B.b_kw "by"; B.b_space; arg] ) else if conclude.Con.conclude_method = "Intros+LetTac" then (match conclude.Con.conclude_args with - [Con.ArgProof p] -> + [Con.ArgProof _p] -> (match conclude.Con.conclude_args with [Con.ArgProof p] -> proof2pres0 term2pres ?skip_initial_lambdas_internal true p false @@ -538,11 +538,11 @@ and args2pres term2pres l = List.map (arg2pres term2pres) l and arg2pres term2pres = function Con.Aux n -> B.b_kw ("aux " ^ n) - | Con.Premise prem -> B.b_kw "premise" - | Con.Lemma lemma -> B.b_kw "lemma" + | Con.Premise _prem -> B.b_kw "premise" + | Con.Lemma _lemma -> B.b_kw "lemma" | Con.Term (_,t) -> term2pres t | Con.ArgProof p -> proof2pres0 term2pres true p false - | Con.ArgMethod s -> B.b_kw "method" + | Con.ArgMethod _s -> B.b_kw "method" and case term2pres conclude = let proof_conclusion = @@ -557,7 +557,7 @@ and case term2pres conclude = let case_on = let case_arg = (match arg with - Con.Aux n -> B.b_kw "an aux???" + Con.Aux _n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with None -> B.b_kw "previous" @@ -565,8 +565,8 @@ and case term2pres conclude = | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> term2pres t - | Con.ArgProof p -> B.b_kw "a proof???" - | Con.ArgMethod s -> B.b_kw "a method???") + | Con.ArgProof _p -> B.b_kw "a proof???" + | Con.ArgMethod _s -> B.b_kw "a method???") in (make_concl "we proceed by cases on" case_arg) in let to_prove = @@ -588,7 +588,7 @@ and byinduction term2pres conclude = let induction_on = let arg = (match inductive_arg with - Con.Aux n -> B.b_kw "an aux???" + Con.Aux _n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with None -> B.b_kw "previous" @@ -596,8 +596,8 @@ and byinduction term2pres conclude = | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term (_,t) -> term2pres t - | Con.ArgProof p -> B.b_kw "a proof???" - | Con.ArgMethod s -> B.b_kw "a method???") in + | Con.ArgProof _p -> B.b_kw "a proof???" + | Con.ArgMethod _s -> B.b_kw "a method???") in (make_concl "we proceed by induction on" arg) in let to_prove = B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in @@ -690,14 +690,14 @@ and falseind term2pres conclude = | Some t -> term2pres t) in let case_arg = (match conclude.Con.conclude_args with - [Con.Aux(n);_;case_arg] -> case_arg + [Con.Aux(_n);_;case_arg] -> case_arg | _ -> assert false; (* List.map (ContentPp.parg 0) conclude.Con.conclude_args; assert false *)) in let arg = (match case_arg with - Con.Aux n -> assert false + Con.Aux _n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with None -> [B.b_kw "Contradiction, hence"] @@ -713,14 +713,14 @@ and falseind term2pres conclude = and andind term2pres conclude = let proof,case_arg = (match conclude.Con.conclude_args with - [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg + [Con.Aux(_n);_;Con.ArgProof proof;case_arg] -> proof,case_arg | _ -> assert false; (* List.map (ContentPp.parg 0) conclude.Con.conclude_args; assert false *)) in let arg = (match case_arg with - Con.Aux n -> assert false + Con.Aux _n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with None -> [] @@ -730,7 +730,7 @@ and andind term2pres conclude = B.Object([], P.Mi([],lemma.Con.lemma_name))] | _ -> assert false) in match proof.Con.proof_context with - `Hypothesis hyp1::`Hypothesis hyp2::tl -> + `Hypothesis hyp1::`Hypothesis hyp2::_tl -> let preshyp1 = B.H ([], [B.Text([],"("); @@ -763,14 +763,14 @@ and andind term2pres conclude = and exists term2pres conclude = let proof = (match conclude.Con.conclude_args with - [Con.Aux(n);_;Con.ArgProof proof;_] -> proof + [Con.Aux(_n);_;Con.ArgProof proof;_] -> proof | _ -> assert false; (* List.map (ContentPp.parg 0) conclude.Con.conclude_args; assert false *)) in match proof.Con.proof_context with - `Declaration decl::`Hypothesis hyp::tl - | `Hypothesis decl::`Hypothesis hyp::tl -> + `Declaration decl::`Hypothesis hyp::_tl + | `Hypothesis decl::`Hypothesis hyp::_tl -> let presdecl = B.H ([], [(B.b_kw "let"); @@ -982,7 +982,7 @@ let njoint_def2pres term2pres joint_kind defs = let nobj2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres - (id,metasenv,obj : NotationPt.term Content.cobj) + (_id,metasenv,obj : NotationPt.term Content.cobj) = match obj with | `Def (Content.Const, thesis, `Proof p) -> diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml index ee62e06e6..f6319c735 100644 --- a/matita/components/content_pres/content2presMatcher.ml +++ b/matita/components/content_pres/content2presMatcher.ml @@ -25,11 +25,8 @@ (* $Id$ *) -open Printf - module Ast = NotationPt module Env = NotationEnv -module Pp = NotationPp module Util = NotationUtil let get_tag term0 = @@ -84,7 +81,7 @@ struct Ast.Variable (Ast.TermVar (name,Ast.Level 0)) in let rec aux = function - | Ast.AttributedTerm (_, t) -> assert false + | Ast.AttributedTerm (_, _t) -> assert false | Ast.Literal _ | Ast.Layout _ -> assert false | Ast.Variable v -> Ast.Variable v @@ -169,7 +166,7 @@ input *) and compile_magic = function - | Ast.Fold (kind, p_base, names, p_rec) -> + | Ast.Fold (_kind, p_base, names, p_rec) -> let p_rec_decls = Env.declarations_of_term p_rec in (* LUCA: p_rec_decls should not contain "names" *) let acc_name = try List.hd names with Failure _ -> assert false in @@ -184,7 +181,7 @@ input let rec aux term = match compiled_rec term with | None -> aux_base term - | Some (env', ctors', _) -> + | Some (env', _ctors', _) -> begin let acc = Env.lookup_term env' acc_name in let env'' = Env.remove_name env' acc_name in @@ -220,7 +217,7 @@ input | Some (env', ctors', 0) -> let env' = List.map - (fun (name, (ty, v)) as binding -> + (fun (name, (_ty, _v)) as binding -> if List.exists (fun (name', _) -> name = name') p_opt_decls then Env.opt_binding_some binding else binding) diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 49d9241b9..84f4a2f72 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -44,7 +44,7 @@ let resolve_binder = function let add_level_info prec t = Ast.AttributedTerm (`Level prec, t) -let rec top_pos t = add_level_info ~-1 t +let top_pos t = add_level_info ~-1 t let rec remove_level_info = function @@ -347,7 +347,7 @@ let instantiate21 idrefs env l1 = Ast.AttributedTerm (attr, subst_singleton pos env t) | t -> NotationUtil.group (subst pos env t) and subst pos env = function - | Ast.AttributedTerm (attr, t) -> + | Ast.AttributedTerm (_attr, t) -> (* prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *) subst pos env t | Ast.Variable var -> @@ -378,7 +378,7 @@ let instantiate21 idrefs env l1 = | Ast.Literal l as t -> let t = add_idrefs idrefs t in (match l with - | `Keyword k -> [ add_keyword_attrs t ] + | `Keyword _k -> [ add_keyword_attrs t ] | _ -> [ t ]) | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ] | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ] @@ -587,7 +587,7 @@ let instantiate_level2 status env term = in let rec aux env term = match term with - | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term + | Ast.AttributedTerm (_a, term) -> (*Ast.AttributedTerm (a, *)aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) | Ast.Binder (binder, var, body) -> Ast.Binder (binder, aux_capture_var env var, aux env body) @@ -632,8 +632,8 @@ let instantiate_level2 status env term = Ast.Pattern (head, hrefs, vars) -> Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars) | Ast.Wildcard -> Ast.Wildcard - and aux_definition env (params, var, term, i) = - (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i) + (*and aux_definition env (params, var, term, i) = + (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)*) and aux_substs env substs = List.map (fun (name, term) -> (name, aux env term)) substs and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs @@ -646,7 +646,7 @@ let instantiate_level2 status env term = | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> Ast.AttributedTerm (`Level l,Env.lookup_term env name) | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None) - | Ast.Ascription (term, name) -> assert false + | Ast.Ascription (_term, _name) -> assert false and aux_magic env = function | Ast.Default (some_pattern, none_pattern) -> let some_pattern_names = NotationUtil.names_of_term some_pattern in @@ -714,7 +714,7 @@ let instantiate_level2 status env term = | _ -> assert false in instantiate_fold_right env) - | Ast.If (_, p_true, p_false) as t -> + | Ast.If (_, _p_true, _p_false) as t -> aux env (NotationUtil.find_branch (Ast.Magic t)) | Ast.Fail -> assert false | _ -> assert false diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index f27c723b0..8bd266370 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -51,8 +51,8 @@ type 'a disambiguator_input = string * int * 'a type domain = domain_tree list and domain_tree = Node of Stdpp.location list * domain_item * domain -let mono_uris_callback ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id = +let mono_uris_callback ~selection_mode:_ ?ok:(_) + ?enable_button_for_non_vars:(_ = true) ~title:(_) ~msg:(_) ~id:(_) = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation" then @@ -69,7 +69,7 @@ let set_choose_interp_callback f = _choose_interp_callback := f let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp -let input_or_locate_uri ~(title:string) ?id () = None +let input_or_locate_uri ~title:(_:string) ?id:(_) () = None (* Zack: I try to avoid using this callback. I therefore assume that * the presence of an identifier that can't be resolved via "locate" * query is a syntax error *) @@ -139,7 +139,7 @@ let resolve ~env ~mk_choice (item: domain_item) arg = match snd (mk_choice (Environment.find item env)), arg with `Num_interp f, `Num_arg n -> f n | `Sym_interp f, `Args l -> f l - | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f [] + | `Sym_interp f, `Num_arg _n -> (* Implicit number! *) f [] | _,_ -> assert false with Not_found -> failwith ("Domain item not found: " ^ @@ -149,7 +149,7 @@ let resolve ~env ~mk_choice (item: domain_item) arg = let find_in_context name context = let rec aux acc = function | [] -> raise Not_found - | Some hd :: tl when hd = name -> acc + | Some hd :: _tl when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context @@ -231,7 +231,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | _ :: tl -> get_first_constructor tl in let do_branch = function - Ast.Pattern (head, _, args), term -> + Ast.Pattern (_head, _, args), term -> let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> @@ -284,8 +284,8 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.NRef _ -> [] | Ast.NCic _ -> [] | Ast.Implicit _ -> [] - | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] - | Ast.Meta (index, local_context) -> + | Ast.Num (_num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Meta (_index, local_context) -> List.fold_left (fun dom term -> dom @ domain_of_term_option ~loc ~context term) [] local_context @@ -352,7 +352,7 @@ let domain_of_obj ~context ast = (fun (context,res) (name,ty,_,_) -> Some name::context, res @ domain_of_term context ty ) (context_w_types,[]) fields) - | Ast.LetRec (kind, defs, _) -> + | Ast.LetRec (_kind, defs, _) -> let add_defs context = List.fold_left (fun acc (_, (var, _), _, _) -> string_of_name var :: acc @@ -393,7 +393,7 @@ let domain_diff dom1 dom2 = (match elt with Symbol (symb',_) when symb = symb' -> true | _ -> false) - | Num i -> + | Num _i -> (match elt with Num _ -> true | _ -> false) @@ -449,7 +449,7 @@ let disambiguate_thing let aliases, todo_dom = let rec aux (aliases,acc) = function | [] -> aliases, acc - | (Node (locs, item,extra) as node) :: tl -> + | Node (locs, item,extra) :: tl -> let choices = lookup_choices item in if List.length choices = 0 then (* Quick failure *) diff --git a/matita/components/disambiguation/disambiguateTypes.ml b/matita/components/disambiguation/disambiguateTypes.ml index 50d1d59da..19c16d130 100644 --- a/matita/components/disambiguation/disambiguateTypes.ml +++ b/matita/components/disambiguation/disambiguateTypes.ml @@ -53,10 +53,10 @@ struct let find k env = match k with - Symbol (sym,n) -> + Symbol (sym,_n) -> (try find k env with Not_found -> find (Symbol (sym,0)) env) - | Num n -> + | Num _n -> (try find k env with Not_found -> find (Num 0) env) | _ -> find k env diff --git a/matita/components/disambiguation/multiPassDisambiguator.ml b/matita/components/disambiguation/multiPassDisambiguator.ml index b1cf9aed0..1ee9df14e 100644 --- a/matita/components/disambiguation/multiPassDisambiguator.ml +++ b/matita/components/disambiguation/multiPassDisambiguator.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - let debug = ref false;; let debug_print s = if !debug then prerr_endline (Lazy.force s) else ();; @@ -119,7 +117,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing let try_pass (fresh_instances, (_, aliases, universe), use_coercions) = f ~fresh_instances ~aliases ~universe ~use_coercions thing in - let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = + let set_aliases (_instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = if use_mono_aliases then drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else if user_asked then diff --git a/matita/components/extlib/discrimination_tree.ml b/matita/components/extlib/discrimination_tree.ml index cdc498e9c..1a8147f7d 100644 --- a/matita/components/extlib/discrimination_tree.ml +++ b/matita/components/extlib/discrimination_tree.ml @@ -157,8 +157,8 @@ and type data = A.elt and type dataset = A.t = (* the equivalent of skip, but on the index, thus the list of trees that are rooted just after the term represented by the tree root are returned (we are skipping the root) *) - let skip_root = function DiscriminationTree.Node (value, map) -> - let rec get n = function DiscriminationTree.Node (v, m) as tree -> + let skip_root = function DiscriminationTree.Node (_value, map) -> + let rec get n = function DiscriminationTree.Node (_v, m) as tree -> if n = 0 then [tree] else PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m [] in @@ -171,7 +171,7 @@ and type data = A.elt and type dataset = A.t = match tree, path with | DiscriminationTree.Node (Some s, _), [] -> s | DiscriminationTree.Node (None, _), [] -> A.empty - | DiscriminationTree.Node (_, map), Variable::path when unif -> + | DiscriminationTree.Node (_, _map), Variable::path when unif -> List.fold_left A.union A.empty (List.map (retrieve path) (skip_root tree)) | DiscriminationTree.Node (_, map), node::path -> @@ -239,7 +239,7 @@ and type data = A.elt and type dataset = A.t = (List.map (fun s, w -> HExtlib.filter_map (fun x -> - try Some (x, w + snd (List.find (fun (s,w) -> A.mem x s) l2)) + try Some (x, w + snd (List.find (fun (s,_w) -> A.mem x s) l2)) with Not_found -> None) (A.elements s)) l1) @@ -254,7 +254,7 @@ and type data = A.elt and type dataset = A.t = match tree, path with | DiscriminationTree.Node (Some s, _), [] -> S.singleton (s, n) | DiscriminationTree.Node (None, _), [] -> S.empty - | DiscriminationTree.Node (_, map), Variable::path when unif -> + | DiscriminationTree.Node (_, _map), Variable::path when unif -> List.fold_left S.union S.empty (List.map (retrieve n path) (skip_root tree)) | DiscriminationTree.Node (_, map), node::path -> diff --git a/matita/components/extlib/hExtlib.ml b/matita/components/extlib/hExtlib.ml index 576101053..b7b664ff2 100644 --- a/matita/components/extlib/hExtlib.ml +++ b/matita/components/extlib/hExtlib.ml @@ -302,7 +302,7 @@ let list_iter_sep ~sep f = in aux -let rec list_findopt f l = +let list_findopt f l = let rec aux k = function | [] -> None | x::tl -> @@ -316,13 +316,13 @@ let split_nth n l = let rec aux acc n l = match n, l with | 0, _ -> List.rev acc, l - | n, [] -> raise (Failure "HExtlib.split_nth") + | _, [] -> raise (Failure "HExtlib.split_nth") | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in aux [] n l let list_last l = let l = List.rev l in - try List.hd l with exn -> raise (Failure "HExtlib.list_last") + try List.hd l with _ -> raise (Failure "HExtlib.list_last") ;; let rec list_assoc_all a = function diff --git a/matita/components/extlib/hLog.ml b/matita/components/extlib/hLog.ml index 4ad2b5ba4..74cacb408 100644 --- a/matita/components/extlib/hLog.ml +++ b/matita/components/extlib/hLog.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - type log_tag = [ `Debug | `Error | `Message | `Warning ] type log_callback = log_tag -> string -> unit diff --git a/matita/components/extlib/patternMatcher.ml b/matita/components/extlib/patternMatcher.ml index f57c3ea6c..fa8c6061e 100644 --- a/matita/components/extlib/patternMatcher.ml +++ b/matita/components/extlib/patternMatcher.ml @@ -25,8 +25,6 @@ (* $Id$ *) -open Printf - type pattern_kind = Variable | Constructor type tag_t = int @@ -121,7 +119,7 @@ struct | _ -> kfail () (*CSC: was assert false, but it did happen*)) let success_closure ksucc = - (fun matched_terms constructors terms -> + (fun matched_terms constructors _terms -> (* prerr_endline "success_closure"; *) ksucc matched_terms constructors) diff --git a/matita/components/extlib/trie.ml b/matita/components/extlib/trie.ml index f60b2d45c..e9e7e3f7b 100644 --- a/matita/components/extlib/trie.ml +++ b/matita/components/extlib/trie.ml @@ -113,7 +113,7 @@ module Make (M : Map.S) = struct in traverse [] t - let rec fold f t acc = + let fold f t acc = let rec traverse revp t acc = match t with | Node (None,m) -> M.fold (fun x -> traverse (x::revp)) m acc diff --git a/matita/components/getter/http_getter.ml b/matita/components/getter/http_getter.ml index 4e431ee81..4de03eab2 100644 --- a/matita/components/getter/http_getter.ml +++ b/matita/components/getter/http_getter.ml @@ -89,18 +89,18 @@ let getter_url () = Helm_registry.get "getter.url" (* Remote interface: getter methods implemented using a remote getter *) (* *) -let getxml_remote uri = not_implemented "getxml_remote" -let getxslt_remote uri = not_implemented "getxslt_remote" -let getdtd_remote uri = not_implemented "getdtd_remote" +let getxml_remote _uri = not_implemented "getxml_remote" +let getxslt_remote _uri = not_implemented "getxslt_remote" +let getdtd_remote _uri = not_implemented "getdtd_remote" let clean_cache_remote () = not_implemented "clean_cache_remote" let list_servers_remote () = not_implemented "list_servers_remote" -let add_server_remote ~logger ~position name = +let add_server_remote ~logger:_ ~position:_ _name = not_implemented "add_server_remote" -let remove_server_remote ~logger position = +let remove_server_remote ~logger:_ _position = not_implemented "remove_server_remote" let getalluris_remote () = not_implemented "getalluris_remote" -let ls_remote lsuri = not_implemented "ls_remote" -let exists_remote uri = not_implemented "exists_remote" +let ls_remote _lsuri = not_implemented "ls_remote" +let exists_remote _uri = not_implemented "exists_remote" (* *) let resolve_remote ~writable uri = @@ -132,7 +132,7 @@ let resolve_remote ~writable uri = | Exception e -> raise e | Resolved url -> url -let deref_index_theory ~local uri = +let deref_index_theory ~local:_ uri = (* if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *) if is_theory_uri uri && Filename.basename uri = "index.theory" then strip_trailing_slash (Filename.dirname uri) ^ theory_suffix @@ -229,7 +229,7 @@ let store_obj tbl o = | s when Pcre.pmatch ~rex:body_ann_RE s -> (true, No, Ann, No) | s when Pcre.pmatch ~rex:proof_tree_RE s -> (false, No, No, Yes) | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true, No, No, Ann) - | s -> no_flags + | _s -> no_flags in Hashtbl.replace tbl basepart (oldflags ++ newflags) end diff --git a/matita/components/getter/http_getter_common.ml b/matita/components/getter/http_getter_common.ml index ddce33f5d..4c817d8f0 100644 --- a/matita/components/getter/http_getter_common.ml +++ b/matita/components/getter/http_getter_common.ml @@ -60,7 +60,7 @@ let rec uri_of_string = function Cic_uri (Theory (Pcre.replace ~pat:"^theory:" uri)) | uri -> raise (Invalid_URI uri) -let patch_xsl ?(via_http = true) () = +let patch_xsl ?via_http:(_ = true) () = fun line -> let mk_patch_fun tag line = Pcre.replace @@ -125,7 +125,7 @@ let return_file | (None, None) -> [] in Http_daemon.send_basic_headers ~code:(`Code 200) outchan; - Http_daemon.send_headers headers outchan; + Http_daemon.send_headers ~headers outchan; Http_daemon.send_CRLF outchan end; match gunzip, patch_fun with diff --git a/matita/components/getter/http_getter_logger.ml b/matita/components/getter/http_getter_logger.ml index 1d774c102..91e7c8a93 100644 --- a/matita/components/getter/http_getter_logger.ml +++ b/matita/components/getter/http_getter_logger.ml @@ -55,7 +55,7 @@ let log ?(level = 1) s = let msg = "[HTTP-Getter] " ^ s in match (!logfile, !logchan) with | None, _ -> prerr_endline msg - | Some fname, Some oc -> + | Some _fname, Some oc -> output_string oc msg; output_string oc "\n"; flush oc diff --git a/matita/components/getter/http_getter_misc.ml b/matita/components/getter/http_getter_misc.ml index d67dceff1..38a943bc5 100644 --- a/matita/components/getter/http_getter_misc.ml +++ b/matita/components/getter/http_getter_misc.ml @@ -33,7 +33,7 @@ open Printf let file_scheme_prefix = "file://" let trailing_dot_gz_RE = Pcre.regexp "\\.gz$" (* for g{,un}zip *) -let url_RE = Pcre.regexp "^([\\w.-]+)(:(\\d+))?(/.*)?$" +(*let url_RE = Pcre.regexp "^([\\w.-]+)(:(\\d+))?(/.*)?$"*) let http_scheme_RE = Pcre.regexp ~flags:[`CASELESS] "^http://" let file_scheme_RE = Pcre.regexp ~flags:[`CASELESS] ("^" ^ file_scheme_prefix) let dir_sep_RE = Pcre.regexp "/" @@ -47,7 +47,7 @@ let local_url = with Not_found -> None let bufsiz = 16384 (* for file system I/O *) -let tcp_bufsiz = 4096 (* for TCP I/O *) +(*let tcp_bufsiz = 4096 (* for TCP I/O *)*) let fold_file f init fname = let ic = open_in fname in diff --git a/matita/components/getter/http_getter_storage.ml b/matita/components/getter/http_getter_storage.ml index c17435f6a..4ff552a4b 100644 --- a/matita/components/getter/http_getter_storage.ml +++ b/matita/components/getter/http_getter_storage.ml @@ -37,7 +37,7 @@ let index_fname = "INDEX" (******************************* HELPERS **************************************) -let trailing_slash_RE = Pcre.regexp "/$" +(*let trailing_slash_RE = Pcre.regexp "/$"*) let relative_RE_raw = "(^[^/]+(/[^/]+)*/?$)" let relative_RE = Pcre.regexp relative_RE_raw let file_scheme_RE_raw = "(^file://)" @@ -115,7 +115,7 @@ let keep_first l = let lookup uri = let matches = HExtlib.filter_map - (fun (rex, _, l, _ as entry) -> + (fun (rex, _, _l, _ as entry) -> try let got = Pcre.extract ~full_match:true ~rex uri in Some (entry, String.length got.(0)) diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 92944aaeb..2e088bd77 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -55,7 +55,7 @@ let rec pp_ntactic status ~map_unicode_to_tex = let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function | NApply (_,t) -> "@" ^ NotationPp.pp_term status t - | NSmartApply (_,t) -> "fixme" + | NSmartApply (_,_t) -> "fixme" | NAuto (_,(None,flgs)) -> "nautobatch" ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) @@ -63,26 +63,26 @@ let rec pp_ntactic status ~map_unicode_to_tex = "nautobatch" ^ " by " ^ (String.concat "," (List.map (NotationPp.pp_term status) l)) ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) - | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term status what ^ + | NCases (_,what,_where) -> "ncases " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NConstructor (_,None,l) -> "@ " ^ String.concat " " (List.map (NotationPp.pp_term status) l) | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ String.concat " " (List.map (NotationPp.pp_term status) l) | NCase1 (_,n) -> "*" ^ n ^ ":" - | NChange (_,what,wwhat) -> "nchange " ^ "...to be implemented..." ^ + | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ " with " ^ NotationPp.pp_term status wwhat | NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *) | NClear (_,l) -> "nclear " ^ String.concat " " l - | NDestruct (_,dom,skip) -> "ndestruct ..." - | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^ + | NDestruct (_,_dom,_skip) -> "ndestruct ..." + | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n | NIntros (_,l) -> "#" ^ String.concat " " l - | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term status what ^ + | NInversion (_,what,_where) -> "ninversion " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t | NRewrite (_,dir,n,where) -> "nrewrite " ^ @@ -112,6 +112,8 @@ let rec pp_ntactic status ~map_unicode_to_tex = let pp_nmacro status = function | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term status term) | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name + | NAutoInteractive _ + | NIntroGuess _ -> assert false (* TODO *) ;; let pp_l1_pattern = NotationPp.pp_term @@ -137,7 +139,7 @@ let pp_precedence i = sprintf "with precedence %d" i let pp_argument_pattern = function | NotationPt.IdentArg (eta_depth, name) -> let eta_buf = Buffer.create 5 in - for i = 1 to eta_depth do + for _i = 1 to eta_depth do Buffer.add_string eta_buf "\\eta." done; sprintf "%s%s" (Buffer.contents eta_buf) name diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 387a09fe7..bd9e76ff2 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -40,7 +40,7 @@ let basic_eval_unification_hint (t,n) status = let inject_unification_hint = let basic_eval_unification_hint (t,n) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then @@ -88,7 +88,7 @@ let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern let inject_interpretation = let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only = let rec refresh = @@ -117,8 +117,8 @@ let basic_eval_alias (mode,diff) status = ;; let inject_alias = - let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term - ~refresh_uri_in_reference ~alias_only = + let basic_eval_alias (mode,diff) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ + ~refresh_uri_in_reference:_ ~alias_only:_ = basic_eval_alias (mode,diff) in GrafiteTypes.Serializer.register#run "alias" basic_eval_alias @@ -138,7 +138,7 @@ let basic_eval_input_notation (l1,l2) status = let inject_input_notation = let basic_eval_input_notation (l1,l2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = if not alias_only then @@ -169,7 +169,7 @@ let basic_eval_output_notation (l1,l2) status = let inject_output_notation = let basic_eval_output_notation (l1,l2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status = if not alias_only then @@ -195,8 +195,8 @@ let eval_output_notation status data= ;; let record_index_obj = - let aux l ~refresh_uri_in_universe - ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status + let aux l ~refresh_uri_in_universe:_ + ~refresh_uri_in_term ~refresh_uri_in_reference:_ ~alias_only status = let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in if not alias_only then @@ -297,8 +297,8 @@ let basic_extract_ocaml_obj obj status = let inject_extract_obj = let basic_extract_obj info - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference - ~alias_only status + ~refresh_uri_in_universe:__ ~refresh_uri_in_term:_ ~refresh_uri_in_reference + ~alias_only:_ status = let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in status#set_extraction_db @@ -309,8 +309,8 @@ let inject_extract_obj = let inject_extract_ocaml_obj = let basic_extract_ocaml_obj info - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference - ~alias_only status + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference + ~alias_only:_ status = let info= OcamlExtractionTable.refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri:NCicLibrary.refresh_uri info in status#set_ocaml_extraction_db @@ -358,7 +358,7 @@ let index_eq print uri (status:#NCic.status) = let record_index_eq = let basic_index_eq uri - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status else @@ -381,7 +381,7 @@ let index_eq_for_auto status uri = let inject_constraint = let basic_eval_add_constraint (acyclic,u1,u2) - ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference + ~refresh_uri_in_universe ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then @@ -560,7 +560,7 @@ let extract_uris status uris = let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = match cmd with - | GrafiteAst.Include (loc, mode, fname) -> + | GrafiteAst.Include (_loc, mode, fname) -> let _root, baseuri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let baseuri = NUri.uri_of_string baseuri in @@ -571,7 +571,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = ~alias_only ~baseuri ~fname:fullpath status in OcamlExtraction.print_open status (NCicLibrary.get_transitively_included status) - | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n + | GrafiteAst.UnificationHint (_loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, compose, None) -> let status, t, ty, source, target = let o_t = NotationPt.Ident (name,None) in @@ -602,7 +602,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) in eval_ncommand ~include_paths opts status (text,prefix_len,cmd) - | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) -> + | GrafiteAst.NCoercion (_loc, name, compose, Some (t, ty, source, target)) -> let status, composites = NCicCoercDeclaration.eval_ncoercion status name compose t ty source target in @@ -610,11 +610,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) let aliases = GrafiteDisambiguate.aliases_for_objs status composites in eval_alias status (mode,aliases) - | GrafiteAst.NQed (loc,index) -> + | GrafiteAst.NQed (_loc,index) -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") else - let uri,height,menv,subst,obj_kind = status#obj in + let uri,_height,menv,subst,obj_kind = status#obj in if menv <> [] then raise (GrafiteTypes.Command_error"You can't Qed an incomplete theorem") @@ -717,7 +717,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = match nobj with NCic.Inductive (is_ind,leftno,itl,_) -> List.fold_left (fun status it -> - (let _,ind_name,ty,cl = it in + (let _,ind_name,_ty,_cl = it in List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in @@ -743,11 +743,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = | _ -> status in let status = match nobj with - NCic.Inductive (is_ind,leftno,itl,_) -> + NCic.Inductive (_is_ind,leftno,itl,_) -> (* first leibniz *) let status' = List.fold_left (fun status it -> - let _,ind_name,ty,cl = it in + let _,ind_name,_ty,_cl = it in let status = status#set_ng_mode `ProofMode in try (let status,invobj = @@ -774,7 +774,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (* then JMeq *) List.fold_left (fun status it -> - let _,ind_name,ty,cl = it in + let _,ind_name,_ty,_cl = it in let status = status#set_ng_mode `ProofMode in try (let status,invobj = @@ -829,7 +829,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = exn -> NCicLibrary.time_travel old_status; raise exn) - | GrafiteAst.NCopy (log,tgt,src_uri, map) -> + | GrafiteAst.NCopy (_loc,tgt,src_uri, map) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@ -860,14 +860,14 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) - | GrafiteAst.NObj (loc,obj,index) -> + | GrafiteAst.NObj (_loc,obj,index) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status,obj = GrafiteDisambiguate.disambiguate_nobj status ~baseuri:status#baseuri (text,prefix_len,obj) in - let uri,height,nmenv,nsubst,nobj = obj in + let _uri,_height,nmenv,_nsubst,_nobj = obj in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj obj in let status = status#set_stack ninitial_stack in @@ -878,12 +878,12 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index)) | _ -> status) - | GrafiteAst.NDiscriminator (loc, indty) -> + | GrafiteAst.NDiscriminator (_loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status = status#set_ng_mode `ProofMode in - let metasenv,subst,status,indty = + let _metasenv,_subst,status,indty = GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] (text,prefix_len,indty) in let indtyno, (_,_,tys,_,_),leftno = match indty with NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> @@ -898,7 +898,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> prerr_endline ("Discriminator: non empty metasenv"); status) - | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> + | GrafiteAst.NInverter (_loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else @@ -918,7 +918,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = "ninverter: found target %s, which is not a sort" (status#ppterm ~metasenv ~subst ~context:[] sort))) in let status = status#set_ng_mode `ProofMode in - let metasenv,subst,status,indty = + let _metasenv,_subst,status,indty = GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst (text,prefix_len,indty) in let indtyno,(_,leftno,tys,_,_) = @@ -939,16 +939,16 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false)) | _ -> assert false) - | GrafiteAst.NUnivConstraint (loc,acyclic,u1,u2) -> + | GrafiteAst.NUnivConstraint (_loc,acyclic,u1,u2) -> eval_add_constraint status acyclic [`Type,u1] [`Type,u2] (* ex lexicon commands *) - | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> + | GrafiteAst.Interpretation (_loc, dsc, (symbol, args), cic_appl_pattern) -> let cic_appl_pattern = GrafiteDisambiguate.disambiguate_cic_appl_pattern status args cic_appl_pattern in eval_interpretation status (dsc,(symbol, args),cic_appl_pattern) - | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> + | GrafiteAst.Notation (_loc, dir, l1, associativity, precedence, l2) -> let l1 = CicNotationParser.check_l1_pattern l1 (dir = Some `RightToLeft) precedence associativity @@ -959,23 +959,23 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = in if dir <> Some `LeftToRight then eval_output_notation status (l1,l2) else status - | GrafiteAst.Alias (loc, spec) -> + | GrafiteAst.Alias (_loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with - | GrafiteAst.Ident_alias (id,uri) -> + | GrafiteAst.Ident_alias (id,_uri) -> [DisambiguateTypes.Id id,spec] - | GrafiteAst.Symbol_alias (symb, instance, desc) -> + | GrafiteAst.Symbol_alias (symb, instance, _desc) -> [DisambiguateTypes.Symbol (symb,instance),spec] - | GrafiteAst.Number_alias (instance,desc) -> + | GrafiteAst.Number_alias (instance,_desc) -> [DisambiguateTypes.Num instance,spec] in let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*) eval_alias status (mode,diff) ;; -let eval_comment opts status (text,prefix_len,c) = status +let eval_comment _opts status (_text,_prefix_len,_c) = status let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = match ex with diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index 74a7eb6a4..a2ed8044a 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -152,7 +152,7 @@ disambiguation error"))) aux 0 [] ty in let status, tgt, arity = - let metasenv,subst,status,tgt = + let _metasenv,subst,status,tgt = GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,tgt) in let tgt = NCicUntrusted.apply_subst status subst [] tgt in @@ -182,7 +182,7 @@ let fresh_uri status prefix suffix = exception Stop;; -let close_graph name t s d to_s from_d p a status = +let close_graph _name t s d to_s from_d _p a status = let c = List.find (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false) @@ -228,7 +228,7 @@ let close_graph name t s d to_s from_d p a status = let pos = match p with | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv) - | t -> raise Stop + | _t -> raise Stop in let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in @@ -292,8 +292,8 @@ let record_ncoercion = let d = refresh_uri_in_term d in basic_index_ncoercion (name,compose,t,s,d,p,a) in - let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term - ~refresh_uri_in_reference ~alias_only status + let aux_l l ~refresh_uri_in_universe:_ ~refresh_uri_in_term + ~refresh_uri_in_reference:_ ~alias_only status = if not alias_only then List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 3bf2dfa62..b5b20bb60 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -22,8 +22,8 @@ depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) # # -grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) -grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) +grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) -w -27 +grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) -w -27 include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml index 738ceb4da..9fea12e40 100644 --- a/matita/components/grafite_parser/print_grammar.ml +++ b/matita/components/grafite_parser/print_grammar.ml @@ -105,7 +105,7 @@ let needs_brackets t = count_brothers t > 1 let visit_description desc fmt self = - let skip s = true in + let skip _s = true in let inline s = List.mem s [ "int" ] in let rec visit_entry e ?level todo is_son = @@ -140,7 +140,7 @@ let visit_description desc fmt self = (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref) todo is_son - and visit_tree name t todo is_son = + and visit_tree name t todo _is_son = if List.for_all (List.for_all is_symbol_dummy) t then todo else ( Format.fprintf fmt "@["; (match name with diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml index 13fccbfa2..bcb84fd67 100644 --- a/matita/components/library/librarian.ml +++ b/matita/components/library/librarian.ml @@ -41,7 +41,7 @@ let find_root path = let path = absolutize path in let paths = List.rev (Str.split (Str.regexp "/") path) in let rec build = function - | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl + | _he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl | [] -> ["/"] in let paths = List.map HExtlib.normalize_path (build paths) in @@ -78,7 +78,7 @@ let load_root_file rootpath = let find_root_for ~include_paths file = let include_paths = "" :: Sys.getcwd () :: include_paths in - let rec find_path_for file = + let find_path_for file = try HExtlib.find_in include_paths file with Failure "find_in" -> HLog.error ("We are in: " ^ Sys.getcwd ()); diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 8d7818992..1b3df75f8 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -25,16 +25,14 @@ (* $Id$ *) -open Printf - let debug = false let debug_prerr = if debug then prerr_endline else ignore -module HGT = Http_getter_types;; -module HG = Http_getter;; +(*module HGT = Http_getter_types;;*) +(*module HG = Http_getter;;*) (*module UM = UriManager;;*) -let decompile = ref (fun ~baseuri -> assert false);; +let decompile = ref (fun ~baseuri:_ -> assert false);; let set_decompile_cb f = decompile := f;; (* @@ -219,11 +217,11 @@ let moo_root_dir = lazy ( ;; *) -let rec close_db cache_of_processed_baseuri uris next = +let close_db _cache_of_processed_baseuri uris _next = uris (* MATITA 1.0 *) ;; -let clean_baseuris ?(verbose=true) buris = +let clean_baseuris ?verbose:(_=true) _buris = (* MATITA 1.0 *) () (* let cache_of_processed_baseuri = Hashtbl.create 1024 in let buris = List.map Http_getter_misc.strip_trailing_slash buris in diff --git a/matita/components/logger/helmLogger.ml b/matita/components/logger/helmLogger.ml index c41674754..467c05464 100644 --- a/matita/components/logger/helmLogger.ml +++ b/matita/components/logger/helmLogger.ml @@ -15,7 +15,7 @@ type html_msg = [ `Error of html_tag | `Msg of html_tag ] type logger_fun = ?append_NL:bool -> html_msg -> unit -let rec string_of_html_tag = +let string_of_html_tag = let rec aux indent = let indent_str = String.make indent ' ' in function diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index 47b1ac063..794859369 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -107,7 +107,7 @@ let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) let instantiate32 idrefs env symbol args = - let rec instantiate_arg = function + let instantiate_arg = function | Ast.IdentArg (n, name) -> let t = try List.assoc name env @@ -267,7 +267,7 @@ let nast_of_cic0 status | NCic.Lambda (n,s,t) -> idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), k ~context:((n,NCic.Decl s)::context) t)) - | NCic.LetIn (n,s,ty,NCic.Rel 1) -> + | NCic.LetIn (_n,s,ty,NCic.Rel 1) -> idref (Ast.Cast (k ~context ty, k ~context s)) | NCic.LetIn (n,s,ty,t) -> idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context @@ -324,7 +324,7 @@ let nast_of_cic0 status in let rec eat_branch n ctx ty pat = match (ty, pat) with - | NCic.Prod (name, s, t), _ when n > 0 -> + | NCic.Prod (_name, _s, t), _ when n > 0 -> eat_branch (pred n) ctx t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in @@ -431,7 +431,7 @@ let nmap_context0 status ~idref ~metasenv ~subst context = ) context ([],[])) ;; -let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = +let nmap_sequent0 status ~idref ~metasenv ~subst (i,(_n,context,ty)) = let module K = Content in let nast_of_cic = nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in @@ -457,7 +457,7 @@ let gen_id prefix seed = res ;; -let build_def_item seed context metasenv id n t ty = +let build_def_item seed _context _metasenv id n t ty = let module K = Content in (* try @@ -543,7 +543,7 @@ let build_inductive b seed = K.inductive_constructors = build_constructors seed cl } in -let build_fixpoint b seed = +let build_fixpoint _b seed = fun (_,n,_,ty,t) -> let t = nast_of_cic ~context:[] t in let ty = nast_of_cic ~context:[] ty in diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml index 7b1e2c508..3ada62287 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -122,7 +122,7 @@ let ncic_mk_choice status = function let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in desc, `Num_interp (fun num -> match f with `Num_interp f -> f num | _ -> assert false) - | GrafiteAst.Ident_alias (name, uri) -> + | GrafiteAst.Ident_alias (_name, uri) -> uri, `Sym_interp (fun l->assert(l = []); let nref = NReference.reference_of_string uri in @@ -139,7 +139,7 @@ let mk_implicit b = ;; let nlookup_in_library - interactive_user_uri_choice input_or_locate_uri item + _interactive_user_uri_choice _input_or_locate_uri item = match item with | DisambiguateTypes.Id id -> @@ -206,8 +206,8 @@ let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_pat (wanted, hyp_paths, goal_path) ;; -let disambiguate_reduction_kind text prefix_len = function - | `Unfold (Some t) -> assert false (* MATITA 1.0 *) +let disambiguate_reduction_kind _text _prefix_len = function + | `Unfold (Some _t) -> assert false (* MATITA 1.0 *) | `Normalize | `Simpl | `Unfold None diff --git a/matita/components/ng_extraction/Makefile b/matita/components/ng_extraction/Makefile index 8bbda655e..46f6f14de 100644 --- a/matita/components/ng_extraction/Makefile +++ b/matita/components/ng_extraction/Makefile @@ -16,9 +16,6 @@ IMPLEMENTATION_FILES = \ miniml.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/ng_extraction/common.ml b/matita/components/ng_extraction/common.ml index fffc09974..be8f3d968 100644 --- a/matita/components/ng_extraction/common.ml +++ b/matita/components/ng_extraction/common.ml @@ -10,7 +10,7 @@ open Coq open OcamlExtractionTable -open Miniml +(*open Miniml*) open Mlutil (*s Some pretty-print utility functions. *) @@ -41,13 +41,13 @@ let rec lowercase_id id = if id = "" then "x" else if id.[0] = '_' then lowercase_id (String.sub id 1 (String.length id - 1)) else if is_invalid_id id then lowercase_id ("x" ^ id) else - String.uncapitalize id + String.uncapitalize_ascii id let rec uppercase_id id = if id = "" then "T" else if id.[0] = '_' then uppercase_id (String.sub id 1 (String.length id - 1)) else if is_invalid_id id then uppercase_id ("x" ^ id) else - String.capitalize id + String.capitalize_ascii id type kind = Term | Type | Cons @@ -108,7 +108,7 @@ let safe_name_of_reference status r = NUri.name_of_uri uri | _ -> NCicPp.r2s status true r -let maybe_capitalize b n = if b then String.capitalize n else n +let maybe_capitalize b n = if b then String.capitalize_ascii n else n let modname_of_filename status capitalize name = try @@ -116,7 +116,7 @@ let modname_of_filename status capitalize name = status, maybe_capitalize capitalize name with Not_found -> let globs = Idset.elements (get_modnames status) in - let s = next_ident_away (String.uncapitalize name) globs in + let s = next_ident_away (String.uncapitalize_ascii name) globs in let status = add_modname status s in let status = add_modname_for_filename status name s in status, maybe_capitalize capitalize s diff --git a/matita/components/ng_extraction/common.mli b/matita/components/ng_extraction/common.mli index 2cf44e003..96550bd4d 100644 --- a/matita/components/ng_extraction/common.mli +++ b/matita/components/ng_extraction/common.mli @@ -9,8 +9,8 @@ (*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Coq -open Miniml -open Mlutil +(**open Miniml +open Mlutil*) open OcamlExtractionTable (** By default, in module Format, you can do horizontal placing of blocks diff --git a/matita/components/ng_extraction/coq.ml b/matita/components/ng_extraction/coq.ml index 130f7ebdf..7e0ff35c6 100644 --- a/matita/components/ng_extraction/coq.ml +++ b/matita/components/ng_extraction/coq.ml @@ -187,7 +187,7 @@ let array_map2 f v1 v2 = if Array.length v1 == 0 then [| |] else begin - let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in + let res = Array.make (Array.length v1) (f v1.(0) v2.(0)) in for i = 1 to pred (Array.length v1) do res.(i) <- f v1.(i) v2.(i) done; @@ -324,7 +324,7 @@ let rec pr_com ft s = let n = String.index s '\n' in String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1)) with Not_found -> s,None in - com_if ft (Lazy.lazy_from_val()); + com_if ft (Lazy.from_val()); (* let s1 = if String.length s1 <> 0 && s1.[0] = ' ' then (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1)) @@ -347,26 +347,26 @@ let pp_dirs ft = in let rec pp_cmd = function | Ppcmd_print(n,s) -> - com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s + com_if ft (Lazy.from_val()); Format.pp_print_as ft n s | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - com_if ft (Lazy.lazy_from_val()); + com_if ft (Lazy.from_val()); pp_open_box bty ; if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss; Format.pp_close_box ft () - | Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty + | Ppcmd_open_box bty -> com_if ft (Lazy.from_val()); pp_open_box bty | Ppcmd_close_box -> Format.pp_close_box ft () | Ppcmd_close_tbox -> Format.pp_close_tbox ft () | Ppcmd_white_space n -> - com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0)) + com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0)) | Ppcmd_print_break(m,n) -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n)) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n)) | Ppcmd_set_tab -> Format.pp_set_tab ft () | Ppcmd_print_tbreak(m,n) -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n)) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n)) | Ppcmd_force_newline -> com_brk ft; Format.pp_force_newline ft () | Ppcmd_print_if_broken -> - com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ())) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ())) | Ppcmd_comment i -> let coms = split_com [] [] i !comments in (* Format.pp_open_hvbox ft 0;*) diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml index 382801b61..be8099598 100644 --- a/matita/components/ng_extraction/extraction.ml +++ b/matita/components/ng_extraction/extraction.ml @@ -207,7 +207,7 @@ let sign_with_implicits _r s = (* Enriching a exception message *) -let rec handle_exn _r _n _fn_name = function x -> x +let handle_exn _r _n _fn_name = function x -> x (*CSC: only for pretty printing | MLexn s -> (try Scanf.sscanf s "UNBOUND %d" @@ -1014,7 +1014,7 @@ and extract_case context mle (ip,c,br) status mlt = (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) -let rec decomp_lams_eta_n n m status context c t = +let decomp_lams_eta_n n m status context c t = let rels = fst (splay_prod_n status context n t) in let rels',c = decompose_lam c in let d = n - m in diff --git a/matita/components/ng_extraction/extraction.mli b/matita/components/ng_extraction/extraction.mli index a5ab1b055..a45dff55c 100644 --- a/matita/components/ng_extraction/extraction.mli +++ b/matita/components/ng_extraction/extraction.mli @@ -10,9 +10,7 @@ (*s Extraction from Coq terms to Miniml. *) -open Coq open Miniml -open OcamlExtractionTable val extract: #OcamlExtractionTable.status as 'status -> NCic.obj -> diff --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml index 0d5e89f6e..01a0cd85d 100644 --- a/matita/components/ng_extraction/mlutil.ml +++ b/matita/components/ng_extraction/mlutil.ml @@ -168,7 +168,7 @@ module Mlenv = struct let clean_free mle = let rem = ref Metaset.empty and add = ref Metaset.empty in - let clean m = match m.contents with + let clean m = match m.Miniml.contents with | None -> () | Some u -> rem := Metaset.add m !rem; add := find_free !add u in @@ -238,18 +238,18 @@ let type_maxvar t = (*s What are the type variables occurring in [t]. *) -let intset_union_map_list f l = - List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l +(*let intset_union_map_list f l = + List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l*) -let intset_union_map_array f a = - Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a +(*let intset_union_map_array f a = + Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a*) -let rec type_listvar = function +(*let rec type_listvar = function | Tmeta {contents = Some t} -> type_listvar t | Tvar i | Tvar' i -> Intset.singleton i | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b) | Tglob (_,l) -> intset_union_map_list type_listvar l - | _ -> Intset.empty + | _ -> Intset.empty*) (*s From [a -> b -> c] to [[a;b],c]. *) @@ -467,12 +467,12 @@ let ast_occurs_itvl k k' t = (*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *) -let nb_occur_k k t = +(*let nb_occur_k k t = let cpt = ref 0 in ast_iter_rel (fun i -> if i = k then incr cpt) t; - !cpt + !cpt*) -let nb_occur t = nb_occur_k 1 t +(*let nb_occur t = nb_occur_k 1 t*) (* Number of occurences of [Rel 1] in [t], with special treatment of match: occurences in different branches aren't added, but we rather use max. *) @@ -596,7 +596,7 @@ let rec many_lams id a = function | 0 -> a | n -> many_lams id (MLlam (id,a)) (pred n) -let anonym_lams a n = many_lams anonymous a n +(*let anonym_lams a n = many_lams anonymous a n*) let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n let dummy_lams a n = many_lams Dummy a n @@ -629,7 +629,7 @@ let rec test_eta_args_lift k n = function (*s Computes an eta-reduction. *) -let eta_red e = +(*let eta_red e = let ids,t = collect_lams e in let n = List.length ids in if n = 0 then e @@ -649,12 +649,12 @@ let eta_red e = if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body) then named_lams ids (ast_lift (-p) body) else e - | _ -> e + | _ -> e*) (*s Computes all head linear beta-reductions possible in [(t a)]. Non-linear head beta-redex become let-in. *) -let rec linear_beta_red a t = match a,t with +(*let rec linear_beta_red a t = match a,t with | [], _ -> t | a0::a, MLlam (id,t) -> (match nb_occur_match t with @@ -663,11 +663,11 @@ let rec linear_beta_red a t = match a,t with | _ -> let a = List.map (ast_lift 1) a in MLletin (id, a0, linear_beta_red a t)) - | _ -> MLapp (t, a) + | _ -> MLapp (t, a)*) -let rec tmp_head_lams = function +(*let rec tmp_head_lams = function | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t) - | e -> e + | e -> e*) (*s Applies a substitution [s] of constants by their body, plus linear beta reductions at modified positions. @@ -675,7 +675,7 @@ let rec tmp_head_lams = function reduction (this helps the inlining of recursors). *) -let rec ast_glob_subst _s _t = assert false (*CSC: reimplement match t with +let ast_glob_subst _s _t = assert false (*CSC: reimplement match t with | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap'.find refe s) @@ -789,7 +789,7 @@ let rec merge_ids ids ids' = match ids,ids' with let is_exn = function MLexn _ -> true | _ -> false -let rec permut_case_fun br _acc = +let permut_case_fun br _acc = let nb = ref max_int in Array.iter (fun (_,_,t) -> let ids, c = collect_lams t in @@ -1168,7 +1168,7 @@ let optimize_fix a = (* Utility functions used in the decision of inlining. *) -let rec ml_size = function +(*let rec ml_size = function | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l | MLlam(_,t) -> 1 + ml_size t | MLcons(_,_,l) -> ml_size_list l @@ -1181,14 +1181,14 @@ let rec ml_size = function and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l -and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l +and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l*) -let is_fix = function MLfix _ -> true | _ -> false +(*let is_fix = function MLfix _ -> true | _ -> false*) -let rec is_constr = function +(*let rec is_constr = function | MLcons _ -> true | MLlam(_,t) -> is_constr t - | _ -> false + | _ -> false*) (*s Strictness *) @@ -1198,11 +1198,11 @@ let rec is_constr = function it begins by at least one non-strict lambda, since the corresponding argument to [t] might be unevaluated in the expanded code. *) -exception Toplevel +(*exception Toplevel*) -let lift n l = List.map ((+) n) l +(*let lift n l = List.map ((+) n) l*) -let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l +(*let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l*) (* This function returns a list of de Bruijn indices of non-strict variables, or raises [Toplevel] if it has an internal non-strict variable. @@ -1212,7 +1212,7 @@ let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l variable to the candidates? We use this flag to check only the external lambdas, those that will correspond to arguments. *) -let rec non_stricts add cand = function +(*let rec non_stricts add cand = function | MLlam (_id,t) -> let cand = lift 1 cand in let cand = if add then 1::cand else cand in @@ -1242,20 +1242,20 @@ let rec non_stricts add cand = function let n = List.length i in let cand = lift n cand in let cand = pop n (non_stricts add cand t) in - Sort.merge (<=) cand c) [] v + List.merge (compare) cand c) [] v (* [merge] may duplicates some indices, but I don't mind. *) | MLmagic t -> non_stricts add cand t | _ -> - cand + cand*) (* The real test: we are looking for internal non-strict variables, so we start with no candidates, and the only positive answer is via the [Toplevel] exception. *) -let is_not_strict t = +(*let is_not_strict t = try let _ = non_stricts true [] t in false - with Toplevel -> true + with Toplevel -> true*) (*s Inlining decision *) @@ -1278,7 +1278,7 @@ let is_not_strict t = restriction for the moment. *) -let inline_test _r _t = +(*let inline_test _r _t = (*CSC:if not (auto_inline ()) then*) false (* else @@ -1289,7 +1289,7 @@ let inline_test _r _t = let t1 = eta_red t in let t2 = snd (collect_lams t1) in not (is_fix t2) && ml_size t < 12 && is_not_strict t -*) +*)*) (*CSC: (not) reimplemented let con_of_string s = @@ -1313,9 +1313,9 @@ let manual_inline_set = ] Cset_env.empty*) -let manual_inline = function (*CSC: +(*let manual_inline = function (*CSC: | ConstRef c -> Cset_env.mem c manual_inline_set - |*) _ -> false + |*) _ -> false*) (* If the user doesn't say he wants to keep [t], we inline in two cases: \begin{itemize} diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml index 2ef1afaa0..213db1eb2 100644 --- a/matita/components/ng_extraction/ocaml.ml +++ b/matita/components/ng_extraction/ocaml.ml @@ -115,7 +115,7 @@ let pp_fields status r fields = (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) -let rec pp_type status par vl t = +let pp_type status par vl t = let rec pp_rec status par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try status,pp_tvar (List.nth vl (pred i)) diff --git a/matita/components/ng_kernel/Makefile b/matita/components/ng_kernel/Makefile index 35b89f3b1..31dd1e9c4 100644 --- a/matita/components/ng_kernel/Makefile +++ b/matita/components/ng_kernel/Makefile @@ -16,9 +16,6 @@ IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml index 52cdb3840..7542a52e0 100644 --- a/matita/components/ng_kernel/nCicReduction.ml +++ b/matita/components/ng_kernel/nCicReduction.ml @@ -18,7 +18,7 @@ module E = NCicEnvironment exception AssertFailure of string Lazy.t;; let debug = ref false;; -let pp m = if !debug then prerr_endline (Lazy.force m) else ();; +(*let pp m = if !debug then prerr_endline (Lazy.force m) else ();;*) module type Strategy = sig type stack_term diff --git a/matita/components/ng_kernel/nCicSubstitution.ml b/matita/components/ng_kernel/nCicSubstitution.ml index 2e382f434..603be63da 100644 --- a/matita/components/ng_kernel/nCicSubstitution.ml +++ b/matita/components/ng_kernel/nCicSubstitution.ml @@ -12,7 +12,6 @@ (* $Id$ *) module C = NCic -module Ref = NReference let lift_from status ?(no_implicit=true) k n = let rec liftaux k = function diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml index b60734508..24217d6ae 100644 --- a/matita/components/ng_kernel/nCicTypeChecker.ml +++ b/matita/components/ng_kernel/nCicTypeChecker.ml @@ -1376,7 +1376,7 @@ let _ = NCicReduction.set_get_relevance get_relevance;; let indent = ref 0;; let debug = true;; -let logger = +let _logger = let do_indent () = String.make !indent ' ' in (function | `Start_type_checking s -> diff --git a/matita/components/ng_library/Makefile b/matita/components/ng_library/Makefile index 861f19acd..20157a09e 100644 --- a/matita/components/ng_library/Makefile +++ b/matita/components/ng_library/Makefile @@ -8,9 +8,6 @@ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae all: %: %.ml $(PACKAGE).cma diff --git a/matita/components/ng_paramodulation/.depend b/matita/components/ng_paramodulation/.depend index 1ee59514d..be0690e45 100644 --- a/matita/components/ng_paramodulation/.depend +++ b/matita/components/ng_paramodulation/.depend @@ -7,8 +7,8 @@ foUnif.cmi : terms.cmi orderings.cmi foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi foUtils.cmi : terms.cmi orderings.cmi -index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +index.cmo : terms.cmi orderings.cmi foUtils.cmi index.cmi +index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi index.cmi : terms.cmi orderings.cmi nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi @@ -21,13 +21,13 @@ nCicParamod.cmi : terms.cmi nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicProof.cmi : terms.cmi -orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi +orderings.cmo : terms.cmi foSubst.cmi orderings.cmi +orderings.cmx : terms.cmx foSubst.cmx orderings.cmi orderings.cmi : terms.cmi paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi + foUtils.cmi paramod.cmi paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi + foUtils.cmx paramod.cmi paramod.cmi : terms.cmi orderings.cmi pp.cmo : terms.cmi pp.cmi pp.cmx : terms.cmx pp.cmi diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 5f4f1cc56..9593d8958 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,45 +1,29 @@ -terms.cmi : -pp.cmi : terms.cmi +foSubst.cmx : terms.cmx foSubst.cmi foSubst.cmi : terms.cmi -orderings.cmi : terms.cmi -foUtils.cmi : terms.cmi orderings.cmi +foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi foUnif.cmi : terms.cmi orderings.cmi +foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUtils.cmi : terms.cmi orderings.cmi +index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi index.cmi : terms.cmi orderings.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -stats.cmi : terms.cmi orderings.cmi -paramod.cmi : terms.cmi orderings.cmi +nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi nCicBlob.cmi : terms.cmi -nCicProof.cmi : terms.cmi +nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ + nCicBlob.cmx nCicParamod.cmi nCicParamod.cmi : terms.cmi -terms.cmo : terms.cmi -terms.cmx : terms.cmi -pp.cmo : terms.cmi pp.cmi +nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi +nCicProof.cmi : terms.cmi +orderings.cmx : terms.cmx foSubst.cmx orderings.cmi +orderings.cmi : terms.cmi +paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ + foUtils.cmx paramod.cmi +paramod.cmi : terms.cmi orderings.cmi pp.cmx : terms.cmx pp.cmi -foSubst.cmo : terms.cmi foSubst.cmi -foSubst.cmx : terms.cmx foSubst.cmi -orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi -foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi -superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ - foUnif.cmi foSubst.cmi superposition.cmi +pp.cmi : terms.cmi +stats.cmx : terms.cmx stats.cmi +stats.cmi : terms.cmi orderings.cmi superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ foUnif.cmx foSubst.cmx superposition.cmi -stats.cmo : terms.cmi stats.cmi -stats.cmx : terms.cmx stats.cmi -paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ - foUtils.cmi foUnif.cmi paramod.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi -nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi -nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ - nCicBlob.cmi nCicParamod.cmi -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi +superposition.cmi : terms.cmi orderings.cmi index.cmi +terms.cmx : terms.cmi +terms.cmi : diff --git a/matita/components/ng_paramodulation/foUnif.ml b/matita/components/ng_paramodulation/foUnif.ml index 0946873b9..c6d130512 100644 --- a/matita/components/ng_paramodulation/foUnif.ml +++ b/matita/components/ng_paramodulation/foUnif.ml @@ -58,12 +58,12 @@ module Founif (B : Orderings.Blob) = struct Subst.build_subst i t subst | Terms.Var i, t when occurs_check subst i t -> raise (UnificationFailure (lazy "Inference.unification.unif")) - | Terms.Var i, t when (List.mem i locked_vars) -> + | Terms.Var i, _t when (List.mem i locked_vars) -> raise (UnificationFailure (lazy "Inference.unification.unif")) | Terms.Var i, t -> Subst.build_subst i t subst | t, Terms.Var i when occurs_check subst i t -> raise (UnificationFailure (lazy "Inference.unification.unif")) - | t, Terms.Var i when (List.mem i locked_vars) -> + | _t, Terms.Var i when (List.mem i locked_vars) -> raise (UnificationFailure (lazy "Inference.unification.unif")) | t, Terms.Var i -> Subst.build_subst i t subst | Terms.Node l1, Terms.Node l2 -> ( @@ -90,7 +90,7 @@ module Founif (B : Orderings.Blob) = struct in match s, t with | s, t when U.eq_foterm s t -> subst - | Terms.Var i, Terms.Var j + | Terms.Var i, Terms.Var _j when (not (List.exists (fun (_,k) -> k=t) subst)) -> let subst = Subst.build_subst i t subst in subst diff --git a/matita/components/ng_paramodulation/index.ml b/matita/components/ng_paramodulation/index.ml index 49af5e089..c1e12a34d 100644 --- a/matita/components/ng_paramodulation/index.ml +++ b/matita/components/ng_paramodulation/index.ml @@ -13,8 +13,8 @@ module Index(B : Orderings.Blob) = struct module U = FoUtils.Utils(B) - module Unif = FoUnif.Founif(B) - module Pp = Pp.Pp(B) + (*module Unif = FoUnif.Founif(B)*) + (*module Pp = Pp.Pp(B)*) module ClauseOT = struct @@ -44,7 +44,7 @@ module Index(B : Orderings.Blob) = struct let path_string_of = let rec aux arity = function | Terms.Leaf a -> [Constant (a, arity)] - | Terms.Var i -> (* assert (arity = 0); *) [Variable] + | Terms.Var _i -> (* assert (arity = 0); *) [Variable] (* FIXME : should this be allowed or not ? | Terms.Node (Terms.Var _::_) -> assert false *) @@ -87,12 +87,12 @@ module Index(B : Orderings.Blob) = struct op t l (Terms.Left2Right, c) | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> op t r (Terms.Right2Left, c) - | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c -> + | (_,Terms.Equation (l,r,_,Terms.Incomparable),_vl,_) as c -> op (op t l (Terms.Left2Right, c)) r (Terms.Right2Left, c) - | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c -> + | (_,Terms.Equation (l,_r,_,Terms.Invertible),_vl,_) as c -> op t l (Terms.Left2Right, c) - | (_,Terms.Equation (_,r,_,Terms.Eq),_,_) -> assert false + | (_,Terms.Equation (_,_r,_,Terms.Eq),_,_) -> assert false | (_,Terms.Predicate p,_,_) as c -> op t p (Terms.Nodir, c) ;; diff --git a/matita/components/ng_paramodulation/nCicBlob.ml b/matita/components/ng_paramodulation/nCicBlob.ml index be5158452..b1f2cfa6f 100644 --- a/matita/components/ng_paramodulation/nCicBlob.ml +++ b/matita/components/ng_paramodulation/nCicBlob.ml @@ -55,10 +55,10 @@ with type t = NCic.term and type input = NCic.term = struct | NReference.Fix(_,_,h) -> h | _ -> 0 -external old_hash_param : - int -> int -> 'a -> int = "caml_hash_univ_param" "noalloc";; + external old_hash_param : + int -> int -> 'a -> int = "caml_hash_univ_param" (*[@@noalloc]*);; -let old_hash = old_hash_param 10 100;; + let old_hash = old_hash_param 10 100;; let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) = let x = height_of_ref r2 - height_of_ref r1 in diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml index 199e101fa..1827d8098 100644 --- a/matita/components/ng_paramodulation/nCicParamod.ml +++ b/matita/components/ng_paramodulation/nCicParamod.ml @@ -205,7 +205,7 @@ let is_equation status metasenv subst context ty = NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0 in match hty with - | NCic.Appl (eq ::tl) when eq = CB.eqP -> true + | NCic.Appl (eq ::_) when eq = CB.eqP -> true | _ -> false ;; diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index 60f2cbafc..f34b35748 100644 --- a/matita/components/ng_paramodulation/nCicProof.ml +++ b/matita/components/ng_paramodulation/nCicProof.ml @@ -131,7 +131,7 @@ let debug c _ = c;; NCic.Implicit `Term; eq; NCic.Implicit `Term]; ;; - let trans eq p = + let trans eq _p = let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term; @@ -180,7 +180,7 @@ let debug c _ = c;; List.fold_left (fun (i,acc) t -> i+1, - let f = extract status amount vl f in + let _f = extract status amount vl f in if i = n then let imp = NCic.Implicit `Term in NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp:: @@ -201,15 +201,15 @@ let debug c _ = c;; let module Pp = Pp.Pp(NCicBlob) in let module Subst = FoSubst in - let compose subst1 subst2 = + (*let compose subst1 subst2 = let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in let s2 = List.filter (fun (m,_) -> not (List.mem_assoc m s1)) subst2 in s1 @ s2 - in + in*) let position i l = let rec aux = function | [] -> assert false - | (j,_) :: tl when i = j -> 1 + | (j,_) :: _ when i = j -> 1 | _ :: tl -> 1 + aux tl in aux l @@ -287,7 +287,7 @@ let debug c _ = c;; (* prerr_endline (if ongoal then "on goal" else "not on goal"); prerr_endline (Pp.pp_substitution subst); *) (* let subst = if ongoal then res_subst else subst in *) - let id, id1,(lit,vl,proof) = + let id, id1,(lit,vl,_proof) = if ongoal then let lit,vl,proof = get_literal id1 in id1,id,(Subst.apply_subst res_subst lit, diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml index d24a5742e..d5f35a3a3 100644 --- a/matita/components/ng_paramodulation/orderings.ml +++ b/matita/components/ng_paramodulation/orderings.ml @@ -131,8 +131,8 @@ let compare_weights (h1, w1) (h2, w2) = if var1 = var2 then let diffs = (w1 - w2) + diffs in let r = Pervasives.compare w1 w2 in - let lt = lt or (r < 0) in - let gt = gt or (r > 0) in + let lt = lt || (r < 0) in + let gt = gt || (r > 0) in if lt && gt then XINCOMPARABLE else aux hdiff (lt, gt) diffs tl1 tl2 else if var1 < var2 then @@ -208,7 +208,7 @@ module NRKBO (B : Terms.Blob) = struct let name = "nrkbo" include B - module Pp = Pp.Pp(B) + (*module Pp = Pp.Pp(B)*) let eq_foterm = eq_foterm B.eq;; @@ -224,7 +224,7 @@ exception UnificationFailure of string Lazy.t;; in match s, t with | s, t when eq_foterm s t -> subst - | Terms.Var i, Terms.Var j + | Terms.Var i, Terms.Var _j when (not (List.exists (fun (_,k) -> k=t) subst)) -> let subst = FoSubst.build_subst i t subst in subst @@ -290,7 +290,7 @@ module KBO (B : Terms.Blob) = struct let name = "kbo" include B - module Pp = Pp.Pp(B) + (*module Pp = Pp.Pp(B)*) let eq_foterm = eq_foterm B.eq;; @@ -356,7 +356,7 @@ module LPO (B : Terms.Blob) = struct let name = "lpo" include B - module Pp = Pp.Pp(B) + (*module Pp = Pp.Pp(B)*) let eq_foterm = eq_foterm B.eq;; diff --git a/matita/components/ng_paramodulation/paramod.ml b/matita/components/ng_paramodulation/paramod.ml index 66a801187..e38179c77 100644 --- a/matita/components/ng_paramodulation/paramod.ml +++ b/matita/components/ng_paramodulation/paramod.ml @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let print s = prerr_endline (Lazy.force s) ;; -let noprint s = ();; +let noprint _s = ();; let debug = noprint;; let monster = 100;; @@ -65,7 +65,7 @@ module type Paramod = module Paramod (B : Orderings.Blob) = struct module Pp = Pp.Pp (B) - module FU = FoUnif.Founif(B) + (*module FU = FoUnif.Founif(B)*) module IDX = Index.Index(B) module Sup = Superposition.Superposition(B) module Utils = FoUtils.Utils(B) @@ -363,7 +363,7 @@ module Paramod (B : Orderings.Blob) = struct debug (lazy("Last chance " ^ string_of_float (Unix.gettimeofday()))); let actives_l, active_t = actives in - let passive_t,wset,_ = passives in + let passive_t,_wset,_ = passives in let _ = noprint (lazy ("Actives :" ^ (String.concat ";\n" @@ -493,8 +493,8 @@ module Paramod (B : Orderings.Blob) = struct let newstatus = List.fold_left (fun acc g -> - let bag,maxvar,actives,passives,g_actives,g_passives = acc in - let g_passives = + let _bag,_maxvar,_actives,_passives,_g_actives,g_passives = acc in + let _g_passives = remove_passive_goal g_passives g in let current = snd g in let _ = @@ -511,7 +511,7 @@ module Paramod (B : Orderings.Blob) = struct let l = let rec traverse ongoal (accg,acce) i = match Terms.get_from_bag i bag with - | (id,_,_,Terms.Exact _),_,_ -> + | (_id,_,_,Terms.Exact _),_,_ -> if ongoal then [i],acce else if (List.mem i acce) then accg,acce else accg,acce@[i] | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ -> @@ -573,8 +573,8 @@ module Paramod (B : Orderings.Blob) = struct ;; let demod s goal = - let bag,maxvar,actives,passives,g_actives,g_passives = s in - let (bag,maxvar), g = mk_goal (bag,maxvar) goal in + let bag,maxvar,actives,_passives,_g_actives,_g_passives = s in + let (bag,_maxvar), g = mk_goal (bag,maxvar) goal in let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in if g1 = g then GaveUp else compute_result bag i [] (* @@ -584,7 +584,7 @@ let demod s goal = let fast_eq_check s goal = let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in - if is_passive_g_set_empty g_passives then Error "not an equation" + if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology) else try goal_narrowing 0 2 None s @@ -598,7 +598,7 @@ let fast_eq_check s goal = let nparamod ~useage ~max_steps ?timeout s goal = let bag,maxvar,actives,passives,g_actives,g_passives = initialize_goal s goal in - if is_passive_g_set_empty g_passives then Error "not an equation" + if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology) else try given_clause ~useage ~noinfer:false bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives diff --git a/matita/components/ng_paramodulation/pp.ml b/matita/components/ng_paramodulation/pp.ml index 64af9ab17..3f2a5cecc 100644 --- a/matita/components/ng_paramodulation/pp.ml +++ b/matita/components/ng_paramodulation/pp.ml @@ -70,7 +70,7 @@ let pp_proof bag ~formatter:f p = Format.fprintf f "%d: Exact (" eq; pp_foterm f t; Format.fprintf f ")@;"; - | Terms.Step (rule,eq1,eq2,dir,pos,subst) -> + | Terms.Step (rule,eq1,eq2,dir,_pos,_subst) -> Format.fprintf f "%d: %s(" eq (string_of_rule rule); Format.fprintf f "|%d with %d dir %s))" eq1 eq2 diff --git a/matita/components/ng_paramodulation/stats.ml b/matita/components/ng_paramodulation/stats.ml index fd68f0fe7..da00eb551 100644 --- a/matita/components/ng_paramodulation/stats.ml +++ b/matita/components/ng_paramodulation/stats.ml @@ -115,8 +115,8 @@ module Stats (B : Terms.Blob) = else dependencies op tl acc else dependencies op tl acc - | ((Terms.Node (Terms.Leaf op1::t) as x),y) - | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y -> + | ((Terms.Node (Terms.Leaf op1::_t) as x),y) + | (y,(Terms.Node (Terms.Leaf op1::_t) as x)) when leaf_count x > leaf_count y -> let rec term_leaves = function | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l | Terms.Leaf x -> [x] diff --git a/matita/components/ng_paramodulation/superposition.ml b/matita/components/ng_paramodulation/superposition.ml index 13b876bed..801e56b26 100644 --- a/matita/components/ng_paramodulation/superposition.ml +++ b/matita/components/ng_paramodulation/superposition.ml @@ -111,7 +111,7 @@ module Superposition (B : Orderings.Blob) = | Terms.Leaf _ as t -> let bag,subst,t,id = f bag t pos ctx id in assert (subst=[]); bag,t,id - | Terms.Var i as t -> + | Terms.Var _ as t -> let t= Subst.apply_subst subst t in bag,t,id | Terms.Node (hd::l) -> @@ -181,7 +181,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, (id,lit,vl,_)) -> + (fun (dir, (id,lit,_vl,_)) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> @@ -227,7 +227,7 @@ module Superposition (B : Orderings.Blob) = (IDX.DT.retrieve_generalizations table) subterm in list_first - (fun (dir, ((id,lit,vl,_) as c)) -> + (fun (dir, ((id,lit,_vl,_) as c)) -> debug (lazy("candidate: " ^ Pp.pp_unit_clause c)); match lit with @@ -280,7 +280,7 @@ module Superposition (B : Orderings.Blob) = (bag,subst,newside,id) ;; - let rec demodulate bag (id, literal, vl, pr) table = + let demodulate bag (id, literal, vl, _pr) table = debug (lazy ("demodulate " ^ (string_of_int id))); match literal with | Terms.Predicate t -> (* assert false *) @@ -341,7 +341,7 @@ module Superposition (B : Orderings.Blob) = let is_identity_goal = function | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some [] - | _, Terms.Equation (l,r,_,_), vl, proof -> + | _, Terms.Equation (l,r,_,_), _vl, _proof -> (try Some (Unif.unification (* vl *) [] l r) with FoUnif.UnificationFailure _ -> None) | _, Terms.Predicate _, _, _ -> assert false @@ -389,7 +389,7 @@ module Superposition (B : Orderings.Blob) = let f b c = let id, dir, l, r, vl = match c with - | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl + | (d, (id,Terms.Equation (l,r,_ty,_),vl,_))-> id, d, l, r, vl |_ -> assert false in let reverse = (dir = Terms.Left2Right) = b in @@ -508,7 +508,7 @@ module Superposition (B : Orderings.Blob) = let rec orphan_murder bag acc i = match Terms.get_from_bag i bag with | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc) - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc) + | (_,_,_,Terms.Step (_,_i1,_i2,_,_,_)),true,_ -> (true,acc) | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ -> if (List.mem i acc) then (false,acc) else match orphan_murder bag acc i1 with @@ -570,7 +570,7 @@ module Superposition (B : Orderings.Blob) = match simplify ctable maxvar bag c with |bag,None -> (bag,alist,atable) (* an active clause as been discarded *) - |bag,Some c1 -> + |bag,Some _c1 -> bag, c :: alist, IDX.index_unit_clause atable c) (bag,[],IDX.DT.empty) alist in @@ -671,7 +671,7 @@ module Superposition (B : Orderings.Blob) = else match (is_identity_goal clause) with | Some subst -> raise (Success (bag,maxvar,clause,subst)) | None -> - let (id,lit,vl,_) = clause in + let (_id,lit,vl,_) = clause in (* this optimization makes sense only if we demodulated, since in that case the clause should have been turned into an identity *) if (vl = [] && not(no_demod)) @@ -706,10 +706,10 @@ module Superposition (B : Orderings.Blob) = (* =================== inference ===================== *) (* this is OK for both the sup_left and sup_right inference steps *) - let superposition table varlist subterm pos context = + let superposition table _varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map - (fun (dir, (id,lit,vl,_ (*as uc*))) -> + (fun (dir, (id,lit,_vl,_ (*as uc*))) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> diff --git a/matita/components/ng_refiner/Makefile b/matita/components/ng_refiner/Makefile index 79871a567..612078e3e 100644 --- a/matita/components/ng_refiner/Makefile +++ b/matita/components/ng_refiner/Makefile @@ -14,9 +14,6 @@ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -%.cmo: OCAMLOPTIONS += -w Ae -%.cmi: OCAMLOPTIONS += -w Ae -%.cmx: OCAMLOPTIONS += -w Ae include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml index 0207c9231..beeeeeb6b 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.ml +++ b/matita/components/ng_refiner/nCicMetaSubst.ml @@ -53,7 +53,7 @@ let newmeta,maxmeta,pushmaxmeta,popmaxmeta = (fun () -> incr maxmeta; !maxmeta), (fun () -> !maxmeta), (fun () -> pushedmetas := !maxmeta::!pushedmetas; maxmeta := 0), - (fun () -> match !pushedmetas with [] -> assert false | hd::tl -> pushedmetas := tl) + (fun () -> match !pushedmetas with [] -> assert false | _hd::tl -> pushedmetas := tl) ;; exception NotFound of [`NotInTheList | `NotWellTyped];; @@ -525,8 +525,7 @@ let delift status ~unify metasenv subst context n l t = raise (NotFound `NotWellTyped) | TypeNotGood | NCicTypeChecker.AssertFailure _ - | NCicReduction.AssertFailure _ - | NCicTypeChecker.TypeCheckerFailure _ -> + | NCicReduction.AssertFailure _ -> raise (NotFound `NotWellTyped)) with NotFound reason -> (* This is the case where we fail even first order unification. *) diff --git a/matita/components/ng_refiner/nCicRefineUtil.ml b/matita/components/ng_refiner/nCicRefineUtil.ml index 30ae05577..508e891f3 100644 --- a/matita/components/ng_refiner/nCicRefineUtil.ml +++ b/matita/components/ng_refiner/nCicRefineUtil.ml @@ -25,8 +25,8 @@ (* $Id: cicUtil.ml 10153 2009-07-28 15:17:51Z sacerdot $ *) -exception Meta_not_found of int -exception Subst_not_found of int +(*exception Meta_not_found of int +exception Subst_not_found of int*) (* syntactic_equality up to the *) (* distinction between fake dependent products *) diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index 15fcc069a..0523ef8b2 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -608,15 +608,15 @@ and try_coercions status pp (lazy "WWW: trying coercions -- inner check"); match infty, expty, t with (* `XTSort|`XTProd|`XTInd + Match not implemented *) - | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> + | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,_tyno,_leftno)) as r,outty,m,pl) -> (*{{{*) pp (lazy "CASE"); (* {{{ helper functions *) let get_cl_and_left_p refit outty = match refit with - | Ref.Ref (uri, Ref.Ind (_,tyno,leftno)) -> + | Ref.Ref (_uri, Ref.Ind (_,tyno,_leftno)) -> let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in let _, _, ty, cl = List.nth itl tyno in - let constructorsno = List.length cl in + (*let constructorsno = List.length cl in*) let count_pis t = let rec aux ctx t = match NCicReduction.whd status ~subst ~delta:max_int ctx t with @@ -700,7 +700,7 @@ and try_coercions status (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt in C.Prod (name, src, t), k - | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) -> + | C.Const (Ref.Ref (_,Ref.Ind (_,_,_leftno)) as r) -> let k = let k = C.Const(Ref.mk_constructor i r) in NCicUntrusted.mk_appl k par @@ -716,8 +716,8 @@ and try_coercions status (NCicReduction.head_beta_reduce status ~delta:max_int (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k] | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) -> - let left_p,right_p = HExtlib.split_nth leftno pl in - let has_rights = right_p <> [] in + let left_p,_right_p = HExtlib.split_nth leftno pl in + (*let has_rights = right_p <> [] in*) let k = let k = C.Const(Ref.mk_constructor i r) in NCicUntrusted.mk_appl k (left_p@par) @@ -819,7 +819,7 @@ and try_coercions status in (* }}} end helper functions *) (* constructors types with left params already instantiated *) let outty = NCicUntrusted.apply_subst status subst context outty in - let cl, left_p, leftno,rno = + let cl, _left_p, leftno,rno = get_cl_and_left_p r outty in let right_p, mty = @@ -930,7 +930,7 @@ and try_coercions status pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); metasenv, subst, coerced, expty (*}}}*) | _ -> raise exc - with exc2 -> + with _ -> let expty = match expty with `XTSome expty -> expty @@ -1312,7 +1312,7 @@ let typeof_obj let rec aux context (metasenv,subst) = function | C.Meta _ -> metasenv, subst | C.Implicit _ -> metasenv, subst - | C.Appl (C.Rel i :: args) as t + | C.Appl (C.Rel i :: args) when i > List.length context - len -> let lefts, _ = HExtlib.split_nth leftno args in let ctxlen = List.length context in diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml index a0d767c3a..5c7f92f99 100644 --- a/matita/components/ng_refiner/nCicUnifHint.ml +++ b/matita/components/ng_refiner/nCicUnifHint.ml @@ -332,8 +332,8 @@ let look_for_hint (status:#status) metasenv subst context t1 t2 = end ;; -let pp_hint t p = - let context, t = +let pp_hint _t _p = +(* let context, t = let rec aux ctx = function | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest | t -> ctx, t @@ -349,7 +349,6 @@ let pp_hint t p = in let buff = Buffer.create 100 in let fmt = Format.formatter_of_buffer buff in -(* F.fprintf "@[" F.fprintf "@[" (* pp_ctx [] context *) @@ -405,9 +404,9 @@ let generate_dot_file (status:#status) fmt = (HintSet.elements dataset); ); List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes; - List.iter (fun x, y, l, _, _ -> + List.iter (fun x, y, _l, _, _ -> Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt) !edges; edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges; - List.iter (fun x, y, _, p, l -> pp_hint l p) !edges; + List.iter (fun _x, _y, _, p, l -> pp_hint l p) !edges; ;; diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index 582f7353b..5a5c7ba38 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -50,7 +50,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = let p_name = mk_id "Q_" in let params,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in let params = List.rev_map (function name,_ -> mk_id name) params in - let args,sort = NCicReduction.split_prods status ~subst:[] [] (-1) ty in + let args,_sort = NCicReduction.split_prods status ~subst:[] [] (-1) ty in let args = List.rev_map (function name,_ -> mk_id name) args in let rec_arg = mk_id (fresh_name ()) in let mk_prods = @@ -77,7 +77,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = List.map (function (_,name,ty) -> let _,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in - let cargs,ty= my_split_prods status ~subst:[] [] (-1) ty in + let cargs,_ty= my_split_prods status ~subst:[] [] (-1) ty in let cargs_recargs_nih = List.fold_left (fun (acc,nih) -> function @@ -248,7 +248,7 @@ let pp (status: #NCic.status) = in let rec eat_branch n rels ty pat = match (ty, pat) with - | NCic.Prod (name, s, t), _ when n > 0 -> + | NCic.Prod (_name, _s, t), _ when n > 0 -> eat_branch (pred n) rels t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index f03baa656..f25114817 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -130,7 +130,7 @@ let arg_list nleft t = let nargs it nleft consno = pp (lazy (Printf.sprintf "nargs %d %d" nleft consno)); - let _,indname,_,cl = it in + let _,_indname,_,cl = it in let _,_,t_k = List.nth cl consno in List.length (arg_list nleft t_k) ;; @@ -327,14 +327,14 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = NotationPt.Theorem (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs)) in - let uri,height,nmenv,nsubst,nobj = theorem in + let _uri,_height,nmenv,_nsubst,_nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj theorem in let status = status#set_stack ninitial_stack in let status = subst_metasenv_and_fix_names status in (* PHASE 3: we finally prove the discrimination principle *) - let dbranch it ~use_jmeq leftno consno = + let dbranch it ~use_jmeq:__ leftno consno = let refl_id = mk_sym "refl" in pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno)); let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in @@ -482,7 +482,7 @@ let subst_tac ~context ~dir skip cur_eq = else let gen_tac x = (fun s -> - let x' = String.concat " " x in + (*let x' = String.concat " " x in*) let x = List.map mk_id x in (* let s = NTactics.print_tac false ("@generalize " ^ x') s in *) generalize0_tac x s) in @@ -619,7 +619,7 @@ let select_eq ctx acc domain status goal = | _ -> status, `NonEq in match kind with | `Identity -> - let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in + let status, _goalty = term_of_cic_term status (get_goalty status goal) ctx in status, Some (List.length ctx - i), kind | `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *) | _ -> diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index 8267fd877..f1da10cb7 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -71,7 +71,7 @@ let rec jmeqpatt = function let rec mk_arrows ~jmeq xs ys selection target = match selection,xs,ys with [],[],[] -> target - | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target + | false :: l,_x::xs,_y::ys -> mk_arrows ~jmeq xs ys l target | true :: l,x::xs,y::ys when jmeq -> NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_sym "jmsimeq" ; @@ -95,7 +95,7 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o) ;; -let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri = +let mk_inverter ~jmeq name _is_ind it leftno ?selection outsort (status: #NCic.status) baseuri = pp (lazy ("leftno = " ^ string_of_int leftno)); let _,ind_name,ty,cl = it in pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty)); @@ -142,7 +142,7 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st in (hypaux 1 ncons) in - let outsort, suffix = NCicElim.ast_of_sort outsort in + let outsort, _suffix = NCicElim.ast_of_sort outsort in let theorem = mk_prods xs (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), @@ -156,7 +156,7 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st NotationPt.Theorem (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs)) in - let uri,height,nmenv,nsubst,nobj = theorem in + let _uri,_height,nmenv,_nsubst,_nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj theorem in let status = status#set_stack ninitial_stack in @@ -205,6 +205,6 @@ NotationPt.Implicit (`Tagged "end")); let mk_inverter name is_ind it leftno ?selection outsort status baseuri = try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri - with NTacStatus.Error (s,_) -> + with NTacStatus.Error (_s,_) -> mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri ;; diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 2fa02c307..fc525c84a 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -97,24 +97,24 @@ let ctx_of (c,_) = c ;; let mk_cic_term c t = c,t ;; let ppterm (status:#pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppterm ~metasenv ~subst ~context t ;; let ppcontext (status: #pstatus) c = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in status#ppcontext ~metasenv ~subst c ;; let ppterm_and_context (status: #pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ status#ppterm ~metasenv ~subst ~context t ;; -let relocate status destination (source,t as orig) = +let relocate status destination (source,_t as orig) = pp(lazy("relocate:\n" ^ ppterm_and_context status orig)); pp(lazy("relocate in:\n" ^ ppcontext status destination)); let rc = @@ -134,13 +134,13 @@ let relocate status destination (source,t as orig) = compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> + | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> if n1 = n2 && NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> + | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 -> [ `Delift ctx; `Lift (List.rev ex) ] | _::_ as ex, [] -> [ `Lift (List.rev ex) ] | [], _::_ -> [ `Delift ctx ] @@ -369,7 +369,7 @@ let select_term else let _,_,_,subst,_ = status#obj in match t with - | NCic.Meta (i,lc) when List.mem_assoc i subst -> + | NCic.Meta (i,_lc) when List.mem_assoc i subst -> let _,_,t,_ = NCicUtils.lookup_subst i subst in aux ctx (status,already_found) t | NCic.Meta _ -> (status,already_found),t diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 3ef2dbe5b..1aba2be9d 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -312,7 +312,7 @@ let assumption_tac status = distribute_tac (fun status goal -> let find_in_context name context = let rec aux acc = function | [] -> raise Not_found - | (hd,_) :: tl when hd = name -> acc + | (hd,_) :: _ when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context @@ -502,7 +502,7 @@ let analyze_indty_tac ~what indtyref = let goalty = get_goalty status goal in let status, what = disambiguate status (ctx_of goalty) what `XTInd in let status, ty_what = typeof status (ctx_of what) what in - let status, (r,consno,lefts,rights) = analyse_indty status ty_what in + let _status, (r,consno,lefts,rights) = analyse_indty status ty_what in let leftno = List.length lefts in let rightno = List.length rights in indtyref := Some { @@ -675,7 +675,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_) :: s -> + | (g,_,_,_) :: _s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 1937229af..0f11cab74 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -13,7 +13,7 @@ open Printf let print ?(depth=0) s = prerr_endline (String.make (2*depth) ' '^Lazy.force s) -let noprint ?(depth=0) _ = () +let noprint ?depth:(_=0) _ = () let debug_print = noprint open Continuationals.Stack @@ -66,7 +66,7 @@ let is_relevant tbl item = else true with Not_found -> true -let print_stat status tbl = +let print_stat _status tbl = let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in let relevance v = float !(v.uses) /. float !(v.nominations) in let vcompare (_,v1) (_,v2) = @@ -356,7 +356,7 @@ let index_local_equations2 eq_cache status open_goal lemmas nohyps = eq_cache lemmas ;; -let fast_eq_check_tac ~params s = +let fast_eq_check_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in dist_fast_eq_check unit_eq s ;; @@ -367,7 +367,7 @@ let paramod eq_cache status goal = | s::_ -> s ;; -let paramod_tac ~params s = +let paramod_tac ~params:_ s = let unit_eq = index_local_equations s#eq_cache s in NTactics.distribute_tac (paramod unit_eq) s ;; @@ -416,7 +416,7 @@ let close_wrt_context status = (fun ty ctx_entry -> match ctx_entry with | name, NCic.Decl t -> NCic.Prod(name,t,ty) - | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) + | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty) ;; let args_for_context ?(k=1) ctx = @@ -424,8 +424,8 @@ let args_for_context ?(k=1) ctx = List.fold_left (fun (n,l) ctx_entry -> match ctx_entry with - | name, NCic.Decl t -> n+1,NCic.Rel(n)::l - | name, NCic.Def(bo, _) -> n+1,l) + | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l + | _name, NCic.Def(_bo, _) -> n+1,l) (k,[]) ctx in args @@ -444,7 +444,7 @@ let refresh metasenv = List.fold_left (fun (metasenv,subst) (i,(iattr,ctx,ty)) -> let ikind = NCicUntrusted.kind_of_meta iattr in - let metasenv,j,instance,ty = + let metasenv,_j,instance,ty = NCicMetaSubst.mk_meta ~attrs:iattr metasenv ctx ~with_type:ty ikind in let s_entry = i,(iattr, ctx, instance, ty) in @@ -460,12 +460,12 @@ let close_metasenv status metasenv subst = *) let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in List.fold_left - (fun (subst,objs) (i,(iattr,ctx,ty)) -> + (fun (subst,objs) (i,(_iattr,ctx,ty)) -> let ty = NCicUntrusted.apply_subst status subst ctx ty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true subst ctx in - let (uri,_,_,_,obj) as okind = + let (uri,_,_,_,_obj) as okind = constant_for_meta status ctx ty i in try NCicEnvironment.check_and_add_obj status okind; @@ -517,7 +517,7 @@ let replace_meta status i args target = | _ -> let args = List.map (NCicSubstitution.subst_meta status lc) args in NCic.Appl(NCic.Rel k::args)) - | NCic.Meta (j,lc) as m -> + | NCic.Meta (_j,lc) as m -> (match lc with _,NCic.Irl _ -> m | n,NCic.Ctx l -> @@ -532,7 +532,7 @@ let replace_meta status i args target = let close_wrt_metasenv status subst = List.fold_left - (fun ty (i,(iattr,ctx,mty)) -> + (fun ty (i,(_iattr,ctx,mty)) -> let mty = NCicUntrusted.apply_subst status subst ctx mty in let ctx = NCicUntrusted.apply_subst_context status ~fix_projections:true @@ -587,8 +587,8 @@ let saturate_to_ref status metasenv subst ctx nref ty = aux metasenv ty [] let smart_apply t unit_eq status g = - let n,h,metasenv,subst,o = status#obj in - let gname, ctx, gty = List.assoc g metasenv in + let n,h,metasenv,_subst,o = status#obj in + let _gname, ctx, gty = List.assoc g metasenv in (* let ggty = mk_cic_term context gty in *) let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in @@ -629,7 +629,7 @@ let smart_apply t unit_eq status g = debug_print(lazy("ritorno da fast_eq_check")); res with - | NCicEnvironment.ObjectNotFound s as e -> + | NCicEnvironment.ObjectNotFound _s as e -> raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e (* FG: for now we catch TypeCheckerFailure; to be understood *) @@ -952,7 +952,7 @@ let init_cache ?(facts=[]) ?(under_inspection=[],[]) unit_eq = unit_eq; trace = trace} -let only signature _context candidate = true +let only _signature _context _candidate = true (* (* TASSI: nel trie ci mettiamo solo il body, non il ty *) let candidate_ty = @@ -1011,9 +1011,9 @@ let rec stack_goals level gs = let open_goals level status = stack_goals level status#stack ;; -let try_candidate ?(smart=0) flags depth status eq_cache ctx t = +let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t = try - let old_og_no = List.length (open_goals (depth+1) status) in + (*let old_og_no = List.length (open_goals (depth+1) status) in*) debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : " ^ (NotationPp.pp_term status) t)); let status = @@ -1049,7 +1049,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = debug_print ~depth (lazy "strange application"); None) else *) (incr candidate_no; Some ((!candidate_no,t),status)) - with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None + with Error _ -> debug_print ~depth (lazy "failed"); None ;; let sort_of status subst metasenv ctx t = @@ -1087,12 +1087,12 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; -let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty = +let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty = let universe = status#auto_cache in let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in let _, raw_gty = term_of_cic_term status gty context in - let is_prod, is_eq = + let is_prod, _is_eq = let status, t = term_of_cic_term status gty context in let t = NCicReduction.whd status subst context t in match t with @@ -1209,7 +1209,7 @@ let applicative_case ~pfailed depth signature status flags gty cache = flags status tcache signature gty in let sm = if is_eq || is_prod then 0 else 2 in - let sm1 = if flags.last then 2 else 0 in + (*let sm1 = if flags.last then 2 else 0 in *) let maxd = (depth + 1 = flags.maxdepth) in let try_candidates only_one sm acc candidates = List.fold_left @@ -1335,7 +1335,7 @@ let is_prod status = let intro ~depth status facts name = let status = NTactics.intro_tac name status in - let _, ctx, ngty = current_goal status in + let _, ctx, _ngty = current_goal status in let t = mk_cic_term ctx (NCic.Rel 1) in let status, keys = keys_of_term status t in let facts = List.fold_left (add_to_th t) facts keys in @@ -1557,7 +1557,7 @@ match status#stack with List.for_all (fun i -> IntSet.mem i others) (HExtlib.filter_map is_open g) -let top_cache ~depth top status cache = +let top_cache ~depth:_ top status cache = if top then let unit_eq = index_local_equations status#eq_cache status in {cache with unit_eq = unit_eq} @@ -1672,7 +1672,7 @@ auto_main flags signature cache depth status: unit = {cache with under_inspection = tl,tree} in auto_clusters flags signature cache (depth-1) status - | orig::_ -> + | _orig::_ -> if depth > 0 && move_to_side depth status then let status = NTactics.merge_tac status in diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml index 43037aac0..f3309633b 100644 --- a/matita/components/registry/helm_registry.ml +++ b/matita/components/registry/helm_registry.ml @@ -54,7 +54,7 @@ let starts_with prefix = String.sub s 0 prefix_len = prefix with Invalid_argument _ -> false -let hashtbl_keys tbl = Hashtbl.fold (fun k _ acc -> k :: acc) tbl [] +(*let hashtbl_keys tbl = Hashtbl.fold (fun k _ acc -> k :: acc) tbl []*) let hashtbl_pairs tbl = Hashtbl.fold (fun k v acc -> (k,v) :: acc) tbl [] (** *) @@ -85,16 +85,16 @@ let valid_key_rex = Str.regexp ("^" ^ valid_key_rex_raw ^ "$") let interpolated_key_rex = Str.regexp ("\\$(" ^ valid_key_rex_raw ^ ")") let dot_rex = Str.regexp "\\." let spaces_rex = Str.regexp "[ \t\n\r]+" -let heading_spaces_rex = Str.regexp "^[ \t\n\r]+" +(*let heading_spaces_rex = Str.regexp "^[ \t\n\r]+"*) let margin_blanks_rex = Str.regexp "^\\([ \t\n\r]*\\)\\([^ \t\n\r]*\\)\\([ \t\n\r]*\\)$" let strip_blanks s = Str.global_replace margin_blanks_rex "\\2" s -let split s = +(*let split s = (* trailing blanks are removed per default by split *) - Str.split spaces_rex (Str.global_replace heading_spaces_rex "" s) -let merge l = String.concat " " l + Str.split spaces_rex (Str.global_replace heading_spaces_rex "" s)*) +(*let merge l = String.concat " " l*) let handle_type_error f x = try f x with exn -> raise (Type_error (Printexc.to_string exn)) @@ -128,10 +128,10 @@ let quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller v = | _ -> raise (Type_error "not a quad") (* escapes for xml configuration file *) -let (escape, unescape) = +(*let (escape, unescape) = let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in (Netencoding.Html.encode ~in_enc ~out_enc (), - Netencoding.Html.decode ~in_enc ~out_enc ~entity_base:`Xml ()) + Netencoding.Html.decode ~in_enc ~out_enc ~entity_base:`Xml ())*) let key_is_valid key = if not (Str.string_match valid_key_rex key 0) then diff --git a/matita/components/xml/xml.ml b/matita/components/xml/xml.ml index 9696fa4bc..c6bbd66b5 100644 --- a/matita/components/xml/xml.ml +++ b/matita/components/xml/xml.ml @@ -92,7 +92,7 @@ let pp_gen f strm = pp_r m s | [< >] -> () and print_spaces m = - for i = 1 to m do f " " done + for _i = 1 to m do f " " done in pp_r 0 strm ;; diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 35484ddf6..d40a15c7a 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -11,7 +11,7 @@ else ANNOTOPTION = endif -OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w -52 +OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7 OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index df366a9ae..50d7d25bf 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -66,7 +66,7 @@ let ntxt_of_cic_context ~metasenv ~subst = Content2pres.ncontext2pres ((new NCicPp.status)#ppcontext ~metasenv ~subst) -let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst = +let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst = [], "<<>>\n" ^ (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst @@ -75,11 +75,11 @@ class status = object(self) inherit Interpretations.status inherit TermContentPres.status - method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t = + method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t = snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst ~context t) - method ppcontext ?sep ~subst ~metasenv context = + method ppcontext ?sep:(_) ~subst ~metasenv context = snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst context) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index ceb2e1f0d..ec42ee8df 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -25,8 +25,6 @@ open Printf -open GrafiteTypes -open MatitaGtkMisc open MatitaGuiTypes open GtkSourceView3 @@ -197,7 +195,7 @@ object (self) self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START) ~stop:(self#buffer#get_iter `END); ignore(all_tag#connect#event - ~callback:(fun ~origin event pos -> + ~callback:(fun ~origin:_ event _pos -> match GdkEvent.get_type event with | `MOTION_NOTIFY -> Gdk.Window.set_cursor @@ -209,12 +207,12 @@ object (self) | _ -> false)); let hyperlink_tag = self#buffer#create_tag [] in ignore(hyperlink_tag#connect#event - ~callback:(fun ~origin event pos -> + ~callback:(fun ~origin:_ event pos -> let offset = (new GText.iter pos)#offset in let _,_,href = try List.find - (fun (start,stop,href) -> start <= offset && offset <= stop + (fun (start,stop,_href) -> start <= offset && offset <= stop ) hyperlinks with Not_found -> assert false @@ -235,7 +233,7 @@ object (self) false | _ -> false)); List.iter - ( fun (start,stop,(href : string)) -> + ( fun (start,stop,(_href : string)) -> self#buffer#apply_tag hyperlink_tag ~start:(self#buffer#get_iter_at_char start) ~stop:(self#buffer#get_iter_at_char (stop+1)); @@ -690,7 +688,7 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView) -let screenshot status sequents metasenv subst (filename (*as ofn*)) = +let screenshot _status _sequents _metasenv _subst (_filename (*as ofn*)) = () (*MATITA 1.0 let w = GWindow.window ~title:"screenshot" () in let width = 500 in diff --git a/matita/matita/lablGraphviz.ml b/matita/matita/lablGraphviz.ml index b0965e55e..7a30256e3 100644 --- a/matita/matita/lablGraphviz.ml +++ b/matita/matita/lablGraphviz.ml @@ -74,7 +74,7 @@ class graphviz_impl ?packing () = method load_graph_from_file ?(gviz_cmd = "dot") fname = let tmp_png = tempfile () in let rc = Sys.command (mk_gviz_cmd gviz_cmd png_flags fname tmp_png) in - if rc <> 0 || (Unix.stat tmp_png).st_size = 0 then begin + if rc <> 0 || (Unix.stat tmp_png).Unix.st_size = 0 then begin eprintf ("Graphviz command failed (exit code: %d) on the following graph:\n" ^^ "%s\n%!") diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 2bbe85225..2731a5ac7 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -25,11 +25,6 @@ (* $Id$ *) -open Printf - -open MatitaGtkMisc -open GrafiteTypes - (** {2 Initialization} *) let _ = diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index c1c1cd907..2963e71c4 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -25,8 +25,6 @@ (* $Id$ *) -module G = GrafiteAst -open GrafiteTypes open Printf class status baseuri = @@ -163,7 +161,7 @@ let baseuri_of_script ~include_paths fname = (* given a path to a ma file inside the include_paths, returns the new include_paths associated to that file *) -let read_include_paths ~include_paths file = +let read_include_paths ~include_paths:_ file = try let root, _buri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:[] file in diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index 5117b091f..b0a5c7f12 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -124,7 +124,7 @@ let rec to_string exn = | GrafiteTypes.Command_error msg -> None, "Error: " ^ msg | CicNotationParser.Parse_error err -> None, sprintf "Parse error: %s" err - | Unix.Unix_error (code, api, param) -> + | Unix.Unix_error (code, api, _param) -> let err = Unix.error_message code in None, "Unix Error (" ^ api ^ "): " ^ err | HMarshal.Corrupt_file fname -> None, sprintf "file '%s' is corrupt" fname diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml index 52da5b420..1f3caa9c7 100644 --- a/matita/matita/matitaGtkMisc.ml +++ b/matita/matita/matitaGtkMisc.ml @@ -98,7 +98,7 @@ class multiStringListModel ~cols (tree_view: GTree.view) = (fun renderer -> GTree.view_column ~renderer ()) renderers in - object (self) + object val text_columns = text_columns initializer @@ -173,7 +173,7 @@ class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list) let lookup_pixbuf tag = try List.assoc tag tags with Not_found -> assert false in - object (self) + object initializer tree_view#set_model (Some (list_store :> GTree.model)); ignore (tree_view#append_column tag_vcolumn); @@ -227,7 +227,7 @@ class recordModel (tree_view:GTree.view) = ]) in let toggle_vcol = GTree.view_column ~renderer:toggle_rend () in - object (self) + object initializer tree_view#set_model (Some (list_store :> GTree.model)); ignore (tree_view#append_column text_vcol); @@ -267,9 +267,9 @@ let popup_message m#destroy () let popup_message_lowlevel - ~title ~message ?(no_separator=true) ~message_type ~buttons + ~title ~message ?no_separator:(_=true) ~message_type ~buttons ?parent ?(destroy_with_parent=true) - ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint + ?icon ?modal:(_=true) ?(resizable=false) ?screen ?type_hint ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width ?height () = diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index ee268e60a..ad34b7a57 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -31,8 +31,6 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc -exception Found of int - let all_disambiguation_passes = ref false (* this is a shit and should be changed :-{ *) @@ -41,7 +39,7 @@ let interactive_uri_choice ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) ?copy_cb () - ~id uris + ~id:_ uris = if (selection_mode <> `SINGLE) && (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") @@ -180,7 +178,7 @@ class interpErrorModel = (let loc_row = tree_store#append () in begin match lll with - [passes,envs_and_diffs,_,_] -> + [passes,_envs_and_diffs,_,_] -> tree_store#set ~row:loc_row ~column:id_col ("Error location " ^ string_of_int (!idx1+1) ^ ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^ @@ -1011,7 +1009,7 @@ class gui () = console#message ("'"^file^"' loaded."); self#_enableSaveTo file - method private _enableSaveTo file = + method private _enableSaveTo _file = self#main#saveMenuItem#misc#set_sensitive true method private console = console @@ -1133,7 +1131,7 @@ class interpModel = let interactive_string_choice - text prefix_len ?(title = "") ?(msg = "") () ~id locs uris + text prefix_len ?(title = "") ?msg:(_ = "") () ~id:_ locs uris = GtkThread.sync (fun _ -> let dialog = new uriChoiceDialog () in @@ -1258,7 +1256,7 @@ let interactive_interp_choice () text prefix_len choices = let _ = (* disambiguator callbacks *) Disambiguate.set_choose_uris_callback - (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg -> + (fun ~selection_mode ?ok ?enable_button_for_non_vars:(_=false) ~title ~msg -> interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index ef7780f0c..b6c0d209d 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -27,9 +27,7 @@ open Printf -open GrafiteTypes open MatitaGtkMisc -open MatitaGuiTypes open CicMathView module Stack = Continuationals.Stack @@ -91,7 +89,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = GtkSignal.disconnect notebook#as_widget id; switch_page_callback <- None | None -> ()); - for i = 0 to pages do notebook#remove_page 0 done; + for _i = 0 to pages do notebook#remove_page 0 done; notebook#set_show_tabs true; pages <- 0; page2goal <- []; @@ -112,12 +110,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = scrolledWin <- Some w; (match cicMathView#misc#parent with | None -> () - | Some parent -> - let parent = - match cicMathView#misc#parent with - None -> assert false - | Some p -> GContainer.cast_container p - in + | Some p -> + let parent = GContainer.cast_container p in parent#remove cicMathView#coerce); w#add cicMathView#coerce in @@ -158,7 +152,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = in let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in Stack.iter (** populate notebook with tabs *) - ~env:(fun depth tag (pos, sw) -> + ~env:(fun depth _tag (pos, sw) -> let markup = match depth, pos with | 0, 0 -> `Current (render_switch sw) @@ -180,12 +174,12 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = method private render_page: 'status. #ApplyTransformation.status as 'status -> page:int -> goal_switch:Stack.switch -> unit - = fun status ~page ~goal_switch -> + = fun status ~page:_ ~goal_switch -> (match goal_switch with | Stack.Open goal -> let menv,subst = _metasenv in cicMathView#nload_sequent status menv subst goal - | Stack.Closed goal -> + | Stack.Closed _goal -> let root = Lazy.force closed_goal_mathml in cicMathView#load_root ~root); (try @@ -479,7 +473,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_root (Lazy.force empty_mathml) - method private _loadCheck term = + method private _loadCheck _term = failwith "not implemented _loadCheck"; (* self#_showMath *) @@ -504,7 +498,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) "the graph of dependencies amoung objects. Please install it.") ~parent:win#toplevel () - method private dependencies direction uri () = + method private dependencies _direction _uri () = assert false (* MATITA 1.0 let dbd = LibraryDb.instance () in let graph = @@ -728,7 +722,7 @@ let find_selection_owner () = | mv :: tl -> (match mv#get_selections with | [] -> aux tl - | sel :: _ -> mv) + | _sel :: _ -> mv) in aux (get_math_views ()) diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index e612b8803..53d1d1f67 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -38,8 +38,8 @@ let strip_suffix ~suffix s = let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file -let is_proof_script fname = true (** TODO Zack *) -let is_proof_object fname = true (** TODO Zack *) +let is_proof_script _fname = true (** TODO Zack *) +let is_proof_object _fname = true (** TODO Zack *) let append_phrase_sep s = if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then @@ -77,7 +77,7 @@ class shell_history size = let size = size + 1 in let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in let incr x = (x + 1) mod size in - object (self) + object val data = Array.make size "" inherit basic_history (0, -1 , -1) @@ -149,8 +149,8 @@ let list_tl_at ?(equality=(==)) e l = let rec aux = function | [] -> raise Not_found - | hd :: tl as l when equality hd e -> l - | hd :: tl -> aux tl + | hd :: _ as l when equality hd e -> l + | _ :: tl -> aux tl in aux l diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 33296d232..c39e1de40 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -26,7 +26,6 @@ (* $Id$ *) open Printf -open GrafiteTypes module TA = GrafiteAst @@ -84,7 +83,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" - | Some (k,value) -> + | Some (_k,value) -> let newtxt = GrafiteAstPp.pp_alias value in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment @@ -94,7 +93,7 @@ let eval_with_engine include_paths status skipped_txt nonskipped_txt st let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parsed_text script mac = +let eval_nmacro _include_paths (_buffer : GText.buffer) status _unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with | TA.Screenshot (_,name) -> @@ -206,12 +205,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script in match st with | GrafiteAst.Executable (loc, ex) -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in eval_executable include_paths buffer status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> - let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + let _, nonskipped, skipped, _parsed_text_length = text_of_loc loc in eval_executable include_paths buffer status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, _) -> @@ -271,7 +270,7 @@ let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = let status = new MatitaEngine.status baseuri in (match current with - Some current -> NCicLibrary.time_travel status; + Some _current -> NCicLibrary.time_travel status; (* (* MATITA 1.0: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () *) @@ -353,7 +352,7 @@ object (self) false )); ignore(source_view#event#connect#button_release - ~callback:(fun button -> clean_locked := false; false)); + ~callback:(fun _button -> clean_locked := false; false)); ignore(source_view#buffer#connect#after#apply_tag ~callback:( fun tag ~start:_ ~stop:_ -> @@ -375,8 +374,8 @@ object (self) let menuItems = menu#children in let undoMenuItem, redoMenuItem = match menuItems with - [undo;redo;sep1;cut;copy;paste;delete;sep2; - selectall;sep3;inputmethod;insertunicodecharacter] -> + [undo;redo;_sep1;cut;copy;paste;delete;_sep2; + _selectall;_sep3;_inputmethod;_insertunicodecharacter] -> List.iter menu#remove [ copy; cut; delete; paste ]; undo,redo | _ -> assert false in diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index a772ae946..092c79c98 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -25,9 +25,6 @@ (* $Id$ *) -open Printf -open GrafiteTypes - (** user hit the cancel button *) exception Cancel diff --git a/matita/matita/virtuals.ml b/matita/matita/virtuals.ml index 229e780c2..a174ffa21 100644 --- a/matita/matita/virtuals.ml +++ b/matita/matita/virtuals.ml @@ -59,7 +59,7 @@ let similar_symbols symbol = let get_all_eqclass () = let rc = ref [] in Hashtbl.iter - (fun k v -> + (fun _k v -> if not (List.mem v !rc) then rc := v :: !rc) classes;