unused variables removed

diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile
index 8d7fd20844022fb86319db48923340b45ac9e517..f4ef9a8bf8a564878d07fa6c65788b3d402cb306 100644 (file)
--- a/helm/software/components/ng_kernel/Makefile
+++ b/helm/software/components/ng_kernel/Makefile
@@ -18,7 +18,9 @@ IMPLEMENTATION_FILES = \
   nCic.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
-OCAMLOPTIONS += -w Ae
+%.cmo: OCAMLOPTIONS += -w Ae
+%.cmi: OCAMLOPTIONS += -w Ae
+%.cmx: OCAMLOPTIONS += -w Ae
 
 all: rt check
 %: %.ml $(PACKAGE).cma
@@ -49,3 +51,4 @@ depend.png depend.eps: depend.dot
 
 include ../../Makefile.defs
 include ../Makefile.common
+

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 106d92706e8fbe7e46783fb0f0d9cca12353ee21..57f130546d9ed4c5a663e88119fba719d6df2e7f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -152,12 +152,12 @@ let get_checked_indtys = function
 ;;
 
 let get_checked_fixes_or_cofixes = function
-  | Ref.Ref (uri, (Ref.Fix (fixno,_,_)|Ref.CoFix fixno))->
+  | Ref.Ref (uri, (Ref.Fix _|Ref.CoFix _))->
       (match get_checked_obj uri with
       | _,height,_,_, C.Fixpoint (_,funcs,att) ->
          funcs, att, height
       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
-  | r -> prerr_endline ("get_checked_(co)fix on " ^ Ref.string_of_reference r); assert false
+  | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false
 ;;
 
 let get_relevance (Ref.Ref (_, infos) as r) =

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 9f609c85042e166f6c62729255709c58161ab660..00ea9f24e32e5a79b2a71877d6361c9e13cd9a49 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -12,7 +12,8 @@
 (* $Id$ *)
 
 let ppterm = 
-  ref (fun ~context ~subst ~metasenv ?inside_fix t -> "Please, set a pp callback")
+  ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ -> 
+         ignore (inside_fix) ; "Please, set a pp callback")
 ;;
 
 let set_ppterm f = ppterm := f;;
@@ -50,10 +51,10 @@ let r2s pp_fix_name r =
             else 
               NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
         | _ -> assert false)
-  with exn -> R.string_of_reference r
+  with NCicLibrary.ObjectNotFound _ -> R.string_of_reference r
 ;;
 
-let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t = 
+let trivial_pp_term ~context ~subst:_ ~metasenv:_ ?(inside_fix=false) t = 
   let buff = Buffer.create 100 in
   let f = Format.formatter_of_buffer buff in
   let module F = Format in
@@ -159,7 +160,7 @@ let ppobj = function
           ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
   | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) -> 
       "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
-      "inductive "^
+      (if b then "inductive " else "coinductive ")^
       String.concat "\nand "
         (List.map (fun (_,name,ty,cl) ->
           name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 73f78dc3693deab8606a4d5f894a3f27443dba54..c6abbd0e03968529ef960cac19c5cdbe11322181 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -171,7 +171,7 @@ let whd = R.whd
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible whd ?(subst=[])  =
+let are_convertible ?(subst=[])  =
  let rec aux test_eq_only context t1 t2 =
    let rec alpha_eq test_eq_only t1 t2 =
      if t1 === t2 then
@@ -182,8 +182,8 @@ let are_convertible whd ?(subst=[])  =
            NCicEnvironment.universe_leq a b
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
            NCicEnvironment.universe_eq a b
-       | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
-       | (C.Sort s1, C.Sort s2) -> s1 = s2
+       | (C.Sort C.Prop,C.Sort (C.Type _)) -> (not test_eq_only)
+       | (C.Sort C.Prop, C.Sort C.Prop) -> true
 
        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
            aux true context s1 s2 &&
@@ -196,7 +196,7 @@ let are_convertible whd ?(subst=[])  =
           aux test_eq_only context s1 s2 &&
           aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2
 
-       | (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2))) 
+       | (C.Meta (n1,(s1, C.Irl _)), C.Meta (n2,(s2, C.Irl _))) 
           when n1 = n2 && s1 = s2 -> true
        | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 &&
           let l1 = NCicUtils.expand_local_context l1 in
@@ -288,8 +288,6 @@ let are_convertible whd ?(subst=[])  =
   aux false 
 ;;
 
-let are_convertible = are_convertible whd
-
 let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
  match upto, t, l with
   | 0, C.Appl l1, _ -> C.Appl (l1 @ l)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 464aa7c2a539da78633a935b1719fc36ba64a751..efb8386d1e1b787237abc00747b48446ad193108 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -84,7 +84,7 @@ let fixed_args bos j n nn =
       match l1,l2 with
          [],[] -> []
        | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2
-       | he::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *)
+       | _::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *)
        | [],_::_ -> assert false
      in
      let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in
@@ -125,9 +125,9 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    let t1 = R.whd ~subst context t1 in
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
-   | C.Sort s1, C.Sort C.Prop -> t2
+   | C.Sort _, C.Sort C.Prop -> t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
-   | C.Sort _,C.Sort (C.Type _) -> t2
+   | C.Sort C.Prop,C.Sort (C.Type _) -> t2
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
    | C.Sort _, C.Meta  (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
@@ -143,13 +143,7 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   | [] -> ty_he
   | (arg, ty_arg)::tl ->
       match R.whd ~subst context ty_he with 
-      | C.Prod (n,s,t) ->
-(*
-          prerr_endline (PP.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
-            ^ PP.ppterm ~subst ~metasenv ~context ty_arg);
-          prerr_endline (PP.ppterm ~subst ~metasenv ~context
-             (S.subst ~avoid_beta_redexes:true arg t));
-*)
+      | C.Prod (_,s,t) ->
           if R.are_convertible ~subst context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
@@ -184,15 +178,15 @@ let rec instantiate_parameters params c =
   match c, params with
   | c,[] -> c
   | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
-  | t,l -> raise (AssertFailure (lazy "1"))
+  | _,_ -> raise (AssertFailure (lazy "1"))
 ;;
 
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
-  | C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref)  
-  | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as ref) :: _ ) as ty ->
+  | C.Const (Ref.Ref (_,Ref.Ind _) as ref)  
+  | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as ref) :: _ ) as ty ->
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
-      let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
+      let _, leftno, itl, _, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
       let _,_,_,cl = List.nth itl i in
       List.map 
@@ -251,14 +245,14 @@ let rec eat_lambdas ~subst ~metasenv context n te =
         (PP.ppterm ~subst ~metasenv ~context te))))
 ;;
 
-let rec eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
-     (context, recfuns, x as k)
+let rec eat_or_subst_lambdas 
+  ~subst ~metasenv n te to_be_subst args (context,_,_ as k) 
 =
   match n, R.whd ~subst context te, to_be_subst, args with
-  | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
+  | (n, C.Lambda (_,_,ta),true::to_be_subst,arg::args) when n > 0 ->
       eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
        to_be_subst args k
-  | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
+  | (n, C.Lambda (name,so,ta),false::to_be_subst,_::args) when n > 0 ->
       eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
        (shift_k (name,(C.Decl so)) k)
   | (_, te, _, _) -> te, k
@@ -276,7 +270,7 @@ let rec weakly_positive ~subst context n nn uri te =
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
     | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::tl) 
+    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::_) 
         when NUri.eq uri' uri -> dummy
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
@@ -308,7 +302,7 @@ and strictly_positive ~subst context n nn te =
        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.for_all (does_not_occur ~subst context n nn) tl
-   | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i,_)) as r)::tl) -> 
+   | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
       let ok = List.length tyl = 1 in
@@ -333,8 +327,8 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
           if k = 0 then 0
           else
            match R.whd context x with
-           |  C.Rel m when m = n - (indparamsno - k) -> k - 1
-           | y -> raise (TypeCheckerFailure (lazy 
+           | C.Rel m when m = n - (indparamsno - k) -> k - 1
+           | _ -> raise (TypeCheckerFailure (lazy 
               ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
               string_of_int indparamsno ^ " fixed) is not homogeneous in "^
               "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
@@ -437,18 +431,11 @@ let rec typeof ~subst ~metasenv context term =
     | C.Appl (he::(_::_ as args)) ->
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
-(*
-       prerr_endline ("HEAD: " ^ PP.ppterm ~subst ~metasenv ~context ty_he);
-       prerr_endline ("TARGS: " ^ String.concat " | " (List.map (PP.ppterm
-       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
-       prerr_endline ("ARGS: " ^ String.concat " | " (List.map (PP.ppterm
-       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
-*)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
-      let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
+      let _,leftno,itl,_,_ = E.get_checked_indtys r in
       let constructorsno =
         let _,_,_,cl = List.nth itl tyno in List.length cl
       in
@@ -681,7 +668,7 @@ let rec typeof ~subst ~metasenv context term =
             | (C.Sort C.Prop, C.Sort C.Type _) ->
         (* TODO: we should pass all these parameters since we
          * have them already *)
-                let inductive,leftno,itl,_,i = E.get_checked_indtys r in
+                let _,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
                 let _,name,ty,cl = List.nth itl i in
                 let cl_len = List.length cl in
@@ -703,7 +690,7 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
-and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = 
+and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = 
   (* let's check if the arity of the inductive types are well formed *)
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
   (* let's check if the types of the inductive constructors are well formed. *)
@@ -715,7 +702,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
        let context,ty_sort = split_prods ~subst [] ~-1 ty in
        let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
        List.iter
-         (fun (_,name,te) -> 
+         (fun (_,_,te) -> 
            let te = debruijn uri len [] te in
            let context,te = split_prods ~subst tys leftno te in
            let _,chopped_context_rev =
@@ -858,7 +845,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
          ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
-  | C.Match (Ref.Ref (uri,Ref.Ind (true,_,_)),outtype,term,pl) as t ->
+  | C.Match (Ref.Ref (_,Ref.Ind (true,_,_)),outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
          let ty = typeof ~subst ~metasenv context term in
@@ -900,7 +887,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h && List.for_all (does_not_occur ~subst context n nn) tl
    | C.Const (Ref.Ref (_,Ref.Con _)) -> true
-   | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j,paramsno))) :: tl) as t ->
+   | C.Appl (C.Const (Ref.Ref (_, Ref.Con (_,j,paramsno))) :: tl) as t ->
       let ty_t = typeof ~subst ~metasenv context t in
       let dc_ctx, dcl, start, stop = 
         specialize_and_abstract_constrs ~subst indURI indlen context ty_t in
@@ -979,7 +966,7 @@ and is_really_smaller
  | C.Appl [] 
  | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
  | C.Meta _ -> true 
- | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_,_)),outtype,term,pl) ->
+ | C.Match (Ref.Ref (_,Ref.Ind (isinductive,_,_)),_,term,pl) ->
     (match term with
     | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
         if not isinductive then
@@ -1094,7 +1081,8 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let typecheck_obj (uri,height,metasenv,subst,kind) =
+let typecheck_obj (uri,_height,metasenv,subst,kind) =
+ (* height is not checked since it is only used to implement an optimization *)
  typecheck_metasenv metasenv;
  typecheck_subst ~metasenv subst;
  match kind with
@@ -1109,8 +1097,8 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
         (PP.ppterm ~subst ~metasenv ~context:[] ty))))
    | C.Constant (relevance,_,None,ty,_) ->
       ignore (typeof ~subst ~metasenv [] ty)
-   | C.Inductive (is_ind, leftno, tyl, _) -> 
-       check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
+   | C.Inductive (_, leftno, tyl, _) -> 
+       check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
       let types, kl =
         List.fold_left
@@ -1127,7 +1115,7 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
              dbo, Evil rno)
           fl kl)
       in
-      List.iter2 (fun (_,name,x,ty,_) bo ->
+      List.iter2 (fun (_,_,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
        if not (R.are_convertible ~subst types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index ee259877dc63f7cde0ec7ef6bb2a8f6664145ba6..b1b0d321787925a5d7b3c7f8ad6ff0562af57665 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -85,7 +85,7 @@ let restrict octx ctx ot =
    | ((_,objs,None)::tl, Cic.Lambda(name,oso,ota), NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
         (Ce (lazy ((name',NCic.Decl so),objs))::ctx) tl (ota,ta)
-   | ((_,objs,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
+   | ((_,_,Some r)::tl,Cic.Lambda(name,oso,ota),NCic.Lambda(name',so,ta)) ->
        split_lambdas_and_letins ((Some(name,(Cic.Decl oso)))::octx)
         (Fix (lazy (r,name',so))::ctx) tl (ota,ta)
    | ((_,objs,None)::tl,Cic.LetIn(name,obo,oty,ota),NCic.LetIn(nam',bo,ty,ta))->
@@ -170,7 +170,7 @@ let splat_args_for_rel ctx t ?rels n_fix =
 ;;
 
 let splat_args ctx t n_fix rels =
-  let bound, free, _, primo_ce_dopo_fix = context_tassonomy ctx in
+  let bound, _, _, primo_ce_dopo_fix = context_tassonomy ctx in
   if ctx = [] then t
   else
    let rec aux = function
@@ -204,7 +204,7 @@ let fix_outty curi tyno t context outty =
           0, Cic.Sort _ -> 0
         | 0, Cic.Prod (name,so,ty) ->
            1 + count_prods 0 (Some (name, Cic.Decl so)::context) ty
-        | n, Cic.Prod (name,so,ty) ->
+        | _, Cic.Prod (name,so,ty) ->
            count_prods (leftno - 1) (Some (name, Cic.Decl so)::context) ty
         | _,_ -> assert false
       in
@@ -398,15 +398,15 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
   begin
     match obj, ref with 
     | (_,_,_,_,NCic.Fixpoint (true,fl,_)) , 
-      NReference.Ref (y,NReference.Fix _) ->
+      NReference.Ref (_,NReference.Fix _) ->
        ignore(List.fold_left (fun i (_,name,rno,_,_) ->
          let ref = NReference.mk_fix i rno ref in
          Hashtbl.add cache name (ref,obj);
          i+1
        ) 0 fl)
     | (_,_,_,_,NCic.Fixpoint (false,fl,_)) , 
-      NReference.Ref (y,NReference.CoFix _) ->
-       ignore(List.fold_left (fun i (_,name,rno,_,_) ->
+      NReference.Ref (_,NReference.CoFix _) ->
+       ignore(List.fold_left (fun i (_,name,_,_,_) ->
          let ref = NReference.mk_cofix i ref in
          Hashtbl.add cache name (ref,obj);
          i+1
@@ -449,7 +449,7 @@ and height_of_term ?(h=ref 0) t =
  | Cic.MutConstruct (uri,_,_,exp_named_subst) ->
     h := max !h (get_height uri);
     List.iter (function (_,t) -> aux t) exp_named_subst
- | Cic.Meta (i,l) -> List.iter (function None -> () | Some t -> aux t) l
+ | Cic.Meta (_,l) -> List.iter (function None -> () | Some t -> aux t) l
  | Cic.Cast (t1,t2)
  | Cic.Prod (_,t1,t2)
  | Cic.Lambda (_,t1,t2) -> aux t1; aux t2