X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=eecb0fae6a97826e037e8c150b14d3493a0d7c67;hb=f263e4ec717d5ec2e7f9c057855f8223f81baae8;hp=707a7b2b2ed522886791f670aacb7d21af1787fb;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index 707a7b2b2..eecb0fae6 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -30,13 +30,11 @@ exception Can_t_eliminate
 
 let debug_print = fun _ -> ()
 
-let fresh_binder =
-  let counter = ref ~-1 in
-  function
-    | true ->
-        incr counter;
-        Cic.Name ("e" ^ string_of_int !counter)
-    | _ -> Cic.Anonymous
+let counter = ref ~-1 ;;
+
+let fresh_binder () =
+ incr counter;
+ Cic.Name ("e" ^ string_of_int !counter)
 
   (** verifies if a given inductive type occurs in a term in target position *)
 let rec recursive uri typeno = function
@@ -103,13 +101,13 @@ let rec delta (uri, typeno) dependent paramsno consno t p args =
             (CicSubstitution.lift 1 p) [Cic.Rel 1]
         in
         let tgt = CicSubstitution.lift 1 tgt in
-        Cic.Prod (fresh_binder dependent, src,
+        Cic.Prod (fresh_binder (), src,
           Cic.Prod (Cic.Anonymous, phi,
             delta (uri, typeno) dependent paramsno consno tgt
               (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2])))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
-        Cic.Prod (fresh_binder dependent, src,
+        Cic.Prod (fresh_binder (), src,
           delta (uri, typeno) dependent paramsno consno tgt
             (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1]))
   | _ -> assert false
@@ -136,6 +134,11 @@ let rec add_params binder indno ty eliminator =
   else
     match ty with
     | Cic.Prod (name, src, tgt) ->
+       let name =
+        match name with
+           Cic.Name _ -> name
+         | Cic.Anonymous -> fresh_binder ()
+       in
         binder name src (add_params binder (indno - 1) tgt eliminator)
     | _ -> assert false
 
@@ -153,7 +156,15 @@ let rec count_pi = function
 
 let rec type_of_p sort dependent leftno indty = function
   | Cic.Prod (n, src, tgt) when leftno = 0 ->
-      Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
+      let n =
+       if dependent then 
+        match n with
+           Cic.Name _ -> n
+         | Cic.Anonymous -> fresh_binder ()
+       else
+        n
+      in
+       Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt)
   | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt
   | t ->
       if dependent then
@@ -163,14 +174,14 @@ let rec type_of_p sort dependent leftno indty = function
 
 let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
-      Cic.Prod (fresh_binder true,
+      Cic.Prod (fresh_binder (),
         CicSubstitution.lift_from liftfrom liftno src,
         add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt)
   | Cic.Prod (_, _, tgt) ->
       add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt
   | t ->
       if dependent then
-        Cic.Prod (fresh_binder dependent,
+        Cic.Prod (fresh_binder (),
           CicSubstitution.lift_from (rightno + 1) liftno indty,
           Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1)))
       else
@@ -184,15 +195,15 @@ let rec add_right_pi dependent strip liftno liftfrom rightno indty = function
 let rec add_right_lambda dependent strip liftno liftfrom rightno indty case =
 function
   | Cic.Prod (_, src, tgt) when strip = 0 ->
-      Cic.Lambda (fresh_binder true,
+      Cic.Lambda (fresh_binder (),
         CicSubstitution.lift_from liftfrom liftno src,
         add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty
           case tgt)
   | Cic.Prod (_, _, tgt) ->
-      add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty
+      add_right_lambda true (strip - 1) liftno liftfrom rightno indty
         case tgt
   | t ->
-      Cic.Lambda (fresh_binder true,
+      Cic.Lambda (fresh_binder (),
         CicSubstitution.lift_from (rightno + 1) liftno indty, case)
 
 let rec branch (uri, typeno) insource paramsno t fix head args =
@@ -226,13 +237,13 @@ let rec branch (uri, typeno) insource paramsno t fix head args =
           let src = CicSubstitution.lift 1 src in
           branch (uri, typeno) true paramsno src fix head [Cic.Rel 1]
         in
-        Cic.Lambda (fresh_binder true, src,
+        Cic.Lambda (fresh_binder (), src,
           branch (uri, typeno) insource paramsno tgt
             (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1; phi]))
       else  (* non recursive *)
         let args = List.map (CicSubstitution.lift 1) args in
-        Cic.Lambda (fresh_binder true, src,
+        Cic.Lambda (fresh_binder (), src,
           branch (uri, typeno) insource paramsno tgt
           (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
             (args @ [Cic.Rel 1]))
@@ -243,6 +254,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args =
   branch (uri, typeno) insource paramsno t fix head args
 
 let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
+  counter := ~-1;
   let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
   match obj with
   | Cic.InductiveDefinition (indTypes, params, leftno, _) ->
@@ -330,7 +342,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
               (fun (_, constructor) acc ->
                 decr consno;
                 let p = Cic.Rel !consno in
-                Cic.Lambda (fresh_binder true,
+                Cic.Lambda (fresh_binder (),
                   (delta (uri, typeno) dependent leftno !consno
                     constructor p [mk_constructor !consno]),
                   acc))