Cooking discriminated into cooking in types (using Prods) and cooking in bodies

(using Lambdas).

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index cd90fbdf5c0e8327959f3f9bcfacc23f6fb72816..d758c2ca686e99c55d9bde8e86d1cdd737e58fc4 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -245,7 +245,7 @@ let convert_term uri t =
    aux [] [] 0 uri t
 ;;
 
-let cook vars t =
+let cook mode vars t =
  let t = CicSubstitution.lift (List.length vars) t in
  snd (List.fold_right
   (fun uri (n,t) ->
@@ -256,9 +256,10 @@ let cook vars t =
       | _ -> assert false in
     let id = Cic.Name (UriManager.name_of_uri uri) in
     let t =
-     match bo,ty with
-        None,ty -> Cic.Lambda (id,ty,t)
-      | Some bo,ty -> Cic.LetIn (id,bo,ty,t)
+     match bo,ty,mode with
+        None,ty,`Lambda -> Cic.Lambda (id,ty,t)
+      | None,ty,`Pi -> Cic.Prod (id,ty,t)
+      | Some bo,ty,_ -> Cic.LetIn (id,bo,ty,t)
     in
      n+1,t
   ) vars (1,t))
@@ -266,14 +267,14 @@ let cook vars t =
 
 let convert_obj_aux uri = function
  | Cic.Constant (name, None, ty, vars, _) ->
-     let ty = cook vars ty in
+     let ty = cook `Pi vars ty in
      let nty, fixpoints = convert_term uri ty in
      assert(fixpoints = []);
      NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)),
      fixpoints
  | Cic.Constant (name, Some bo, ty, vars, _) ->
-     let bo = cook vars bo in
-     let ty = cook vars ty in
+     let bo = cook `Lambda vars bo in
+     let ty = cook `Pi vars ty in
      let nbo, fixpoints_bo = convert_term uri bo in
      let nty, fixpoints_ty = convert_term uri ty in
      assert(fixpoints_ty = []);
@@ -284,12 +285,12 @@ let convert_obj_aux uri = function
      let itl, fix_itl = 
        List.fold_right
          (fun (name, _, ty, cl) (itl,acc) ->
-            let ty = cook vars ty in
+            let ty = cook `Pi vars ty in
             let ty, fix_ty = convert_term uri ty in
             let cl, fix_cl = 
               List.fold_right
                (fun (name, ty) (cl,acc) -> 
-                 let ty = cook vars ty in
+                 let ty = cook `Pi vars ty in
                  let ty, fix_ty = convert_term uri ty in
                  ([], name, ty)::cl, acc @ fix_ty)
                cl ([],[])