Initial revision

[helm.git] / helm / ocaml / cic_proof_checking / cicCooking.ml

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 75f594a90542de4f874899b1fe0362a2fa4f9e6e..2c5d0b439ffbaebea810e836fe772828d5c88dba 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -36,7 +36,7 @@ let mem x lol =
 ;;
 
 (* cook var term *)
-let cook curi cookingsno var =
+let cook curi cookingsno var is_letin =
  let rec aux k =
   let module C = Cic in
    function
@@ -66,7 +66,7 @@ let cook curi cookingsno var =
         )
     | C.Appl [] -> raise Impossible
     | C.Const (uri,_) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.Definition (_,_,_,params) when mem var params -> true
          | C.Definition _ -> false
          | C.Axiom (_,_,params) when mem var params -> true
@@ -80,9 +80,8 @@ let cook curi cookingsno var =
           [C.Rel k])
        else
         C.Const (uri,UriManager.relative_depth curi uri cookingsno)
-    | C.Abst _ as t -> t
     | C.MutInd (uri,_,i) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true
          | C.InductiveDefinition _ -> false
          | _ -> raise WrongUriToInductiveDefinition
@@ -91,7 +90,7 @@ let cook curi cookingsno var =
        else
         C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i)
     | C.MutConstruct (uri,_,i,j) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true
          | C.InductiveDefinition _ -> false
          | _ -> raise WrongUriToInductiveDefinition
@@ -139,8 +138,8 @@ let cook_gen add_binder curi cookingsno ty vars =
        let cooked_once =
         add_binder (C.Name varname) varbody vartype
          (match varbody with
-             Some _ -> ty
-           | None -> cook curi cookingsno var ty
+             Some _ -> cook curi cookingsno var true ty
+           | None -> cook curi cookingsno var false ty
          )
        in
         cookrec cooked_once tl
@@ -197,7 +196,18 @@ let cook_one_level obj curi cookingsno vars =
            (name,inductive,cook_prod curi cookingsno arity vars,constructors')
         ) dl
       in
-       C.InductiveDefinition (dl', params, n_ind_params + List.length vars)
+       let number_of_variables_without_a_body =
+        let is_not_letin uri =
+         match CicEnvironment.get_obj uri with
+            C.Variable (_,None,_) -> true
+          | C.Variable (_,Some _,_) -> false
+          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+        in
+         List.fold_left
+          (fun i uri -> if is_not_letin uri then i + 1 else i) 0 vars
+       in
+        C.InductiveDefinition
+         (dl', params, n_ind_params + number_of_variables_without_a_body)
 ;; 
 
 let cook_obj obj uri =