From ef72426636bf3f920118df4cf0124010d0125533 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Jul 2008 17:54:23 +0000
Subject: [PATCH] cic2acic: new function acic_term_of_cic_term matita/Makefile:
 LAMBDA-TYPES tested only in opt mode

---
 helm/software/components/cic_acic/cic2acic.ml | 23 +++++++++++++++++--
 .../software/components/cic_acic/cic2acic.mli |  7 ++++++
 helm/software/matita/Makefile                 |  4 ++--
 3 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 01a4bb144..563beaa1c 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -490,7 +490,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=false) obj =
+let acic_term_or_object_of_cic_term_or_object ?(eta_fix=false) () =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
@@ -512,6 +512,19 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
    let eta_fix_and_unshare metasenv context t =
     let t = if eta_fix then E.eta_fix metasenv context t else t in
      Unshare.unshare t in
+   (fun context t ->
+     let map = function
+        | None                     -> None
+	| Some (n, C.Decl ty)      -> Some (n, C.Decl (Unshare.unshare ty))
+        | Some (n, C.Def (bo, ty)) ->
+	    Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty))
+     in
+     let t = Unshare.unshare t in
+     let context = List.map map context in
+     let idrefs = List.map (function _ -> gen_id seed) context in
+     let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in
+     t, ids_to_inner_sorts, ids_to_inner_types
+   ),(function obj ->
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
@@ -633,7 +646,10 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
    in
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses
-;;
+);;
+
+let acic_object_of_cic_object ?eta_fix =
+   snd (acic_term_or_object_of_cic_term_or_object ?eta_fix ()) 
 
 let plain_acic_term_of_cic_term =
  let module C = Cic in
@@ -774,3 +790,6 @@ let plain_acic_object_of_cic_object obj =
      in
       C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
 ;;
+
+let acic_term_of_cic_term ?eta_fix =
+   fst (acic_term_or_object_of_cic_term_or_object ?eta_fix ()) 
diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index c3cf56e88..4526521fb 100644
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -59,3 +59,10 @@ val asequent_of_sequent :
     (Cic.id, Cic.hypothesis) Hashtbl.t)    (* ids_to_hypotheses *)
 
 val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj
+
+val acic_term_of_cic_term :
+  ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
+  Cic.context -> Cic.term ->               (* term and context *)
+   Cic.annterm *                            (* annotated term *)
+    (Cic.id, sort_kind) Hashtbl.t *         (* ids_to_inner_sorts *)
+    (Cic.id, anntypes) Hashtbl.t            (* ids_to_inner_types *)
diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index eae880741..e350c80b6 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -188,13 +188,13 @@ TEST_DIRS = 				\
 	contribs/CoRN	 	        \
 	contribs/RELATIONAL	 	\
 	contribs/LOGIC	       	 	\
-	contribs/LAMBDA-TYPES 		\
 	contribs/PREDICATIVE-TOPOLOGY 	\
 	$(NULL)
 
 #	library_auto 			
 TEST_DIRS_OPT = 			\
-	$(TEST_DIRS)        \
+	$(TEST_DIRS)                    \
+	contribs/LAMBDA-TYPES 		\
 	$(NULL)
 
 .PHONY: tests tests.opt cleantests cleantests.opt
-- 
2.39.2