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 =
| 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)
(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) *)
| 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)
| 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
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
| 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
| _ -> []
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
| 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
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
| _ -> 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 =
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)
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
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
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
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) ->
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
(* $Id$ *)
-open Printf
-
module Ast = NotationPt
module Mpres = Mpresentation
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)
| 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
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)
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
(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
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 =
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"
| 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 =
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"
| 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
| 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"]
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 -> []
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([],"(");
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");
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) ->
(* $Id$ *)
-open Printf
-
module Ast = NotationPt
module Env = NotationEnv
-module Pp = NotationPp
module Util = NotationUtil
let get_tag term0 =
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
*)
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
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
| 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)
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
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 ->
| 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 ]
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)
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
| 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
| _ -> 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
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
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 *)
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: " ^
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
| _ :: 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) ->
| 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
(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
(match elt with
Symbol (symb',_) when symb = symb' -> true
| _ -> false)
- | Num i ->
+ | Num _i ->
(match elt with
Num _ -> true
| _ -> false)
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 *)
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
(* $Id$ *)
-open Printf
-
let debug = ref false;;
let debug_print s =
if !debug then prerr_endline (Lazy.force s) else ();;
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
(* 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
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 ->
(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)
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 ->
in
aux
-let rec list_findopt f l =
+let list_findopt f l =
let rec aux k = function
| [] -> None
| x::tl ->
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
(* $Id$ *)
-open Printf
-
type log_tag = [ `Debug | `Error | `Message | `Warning ]
type log_callback = log_tag -> string -> unit
(* $Id$ *)
-open Printf
-
type pattern_kind = Variable | Constructor
type tag_t = int
| _ -> 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)
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
(* Remote interface: getter methods implemented using a remote getter *)
(* <TODO> *)
-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"
(* </TODO> *)
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
| 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
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
| (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
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
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 "/"
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
(******************************* 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://)"
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))
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)
"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 " ^
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
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
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
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 =
;;
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
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
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
;;
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
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
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
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
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
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
~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
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
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")
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
| _ -> 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 =
(* 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 =
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
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
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) ->
[] -> 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
"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,_,_) =
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
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
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
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)
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
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
depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
# </cross>
#
-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
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 =
(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 "@[<v>";
(match name with
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
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 ());
(* $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;;
(*
;;
*)
-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
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
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
| 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
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
) 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
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
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
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
;;
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 ->
(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
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
open Coq
open OcamlExtractionTable
-open Miniml
+(*open Miniml*)
open Mlutil
(*s Some pretty-print utility functions. *)
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
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
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
(*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
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;
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))
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;*)
(* 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"
(* [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
(*s Extraction from Coq terms to Miniml. *)
-open Coq
open Miniml
-open OcamlExtractionTable
val extract:
#OcamlExtractionTable.status as 'status -> NCic.obj ->
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
(*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]. *)
(*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. *)
| 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
(*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
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
| _ ->
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.
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)
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
(* 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
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 *)
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.
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
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 *)
restriction for the moment.
*)
-let inline_test _r _t =
+(*let inline_test _r _t =
(*CSC:if not (auto_inline ()) then*) false
(*
else
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 =
]
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}
(*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))
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
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
(* $Id$ *)
module C = NCic
-module Ref = NReference
let lift_from status ?(no_implicit=true) k n =
let rec liftaux k = function
let indent = ref 0;;
let debug = true;;
-let logger =
+let _logger =
let do_indent () = String.make !indent ' ' in
(function
| `Start_type_checking s ->
$(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
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
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
-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 :
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 -> (
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
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
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 *)
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)
;;
| 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
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
;;
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;
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::
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
(* 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,
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
let name = "nrkbo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
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
let name = "kbo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
let name = "lpo"
include B
- module Pp = Pp.Pp(B)
+ (*module Pp = Pp.Pp(B)*)
let eq_foterm = eq_foterm B.eq;;
(* $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;;
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)
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"
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 _ =
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,_,_,_)),_,_ ->
;;
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 []
(*
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
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
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
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]
| 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) ->
(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) ->
(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
(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 *)
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
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
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
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
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))
(* =================== 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) ->
$(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
(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];;
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. *)
(* $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 *)
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
(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
(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)
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 =
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
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
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
in
let buff = Buffer.create 100 in
let fmt = Format.formatter_of_buffer buff in
-(*
F.fprintf "@[<hov>"
F.fprintf "@[<hov>"
(* pp_ctx [] context *)
(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;
;;
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 =
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
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
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) ;;
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
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
| _ -> 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 *)
| _ ->
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" ;
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));
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)))),
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
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
;;
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 =
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 ]
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
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
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 {
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
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
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) =
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
;;
| 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
;;
(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 =
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
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
*)
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;
| _ -> 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 ->
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
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
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 *)
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 =
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 =
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 =
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
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
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
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}
{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
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 []
(** </helpers> *)
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))
| _ -> 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
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
;;
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)"
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 =
[],
"<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
(new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
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)
open Printf
-open GrafiteTypes
-open MatitaGtkMisc
open MatitaGuiTypes
open GtkSourceView3
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
| _ -> 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
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));
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
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%!")
(* $Id$ *)
-open Printf
-
-open MatitaGtkMisc
-open GrafiteTypes
-
(** {2 Initialization} *)
let _ =
(* $Id$ *)
-module G = GrafiteAst
-open GrafiteTypes
open Printf
class status baseuri =
(* 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
| 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
(fun renderer -> GTree.view_column ~renderer ())
renderers
in
- object (self)
+ object
val text_columns = text_columns
initializer
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);
])
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);
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 ()
=
open MatitaGtkMisc
open MatitaMisc
-exception Found of int
-
let all_disambiguation_passes = ref false
(* this is a shit and should be changed :-{ *)
?(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")
(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" ^
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
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
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 *)
open Printf
-open GrafiteTypes
open MatitaGtkMisc
-open MatitaGuiTypes
open CicMathView
module Stack = Continuationals.Stack
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 <- [];
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
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)
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
self#_showMath;
mathView#load_root (Lazy.force empty_mathml)
- method private _loadCheck term =
+ method private _loadCheck _term =
failwith "not implemented _loadCheck";
(* self#_showMath *)
"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 =
| mv :: tl ->
(match mv#get_selections with
| [] -> aux tl
- | sel :: _ -> mv)
+ | _sel :: _ -> mv)
in
aux (get_math_views ())
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
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)
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
(* $Id$ *)
open Printf
-open GrafiteTypes
module TA = GrafiteAst
(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
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) ->
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, _) ->
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 () *)
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:_ ->
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
(* $Id$ *)
-open Printf
-open GrafiteTypes
-
(** user hit the cancel button *)
exception Cancel
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;
projects / helm.git / commitdiff