** UNTESTED **

[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 7641ad90e59f9912fad9e098058cbd9ef3817201..815e0caaac8b65ba68f519a2181d238a95786c2a 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -79,8 +79,45 @@ let proof2cic term2cic p =
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | `Joint ho -> 
-            raise TO_DO 
+      | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> 
+            (match target with
+               C.Rel n ->
+                 (match kind with 
+                    `Recursive l ->
+                      let funs = 
+                        List.map2 
+                          (fun n bo ->
+                             match bo with
+                               `Proof bo ->
+                                  (match 
+                                    bo.Con.proof_conclude.Con.conclude_conclusion,
+                                    bo.Con.proof_name
+                                   with
+                                      Some ty, Some name -> 
+                                       (name,n,term2cic ty,proof2cic premise_env bo)
+                                    | _,_ -> assert false)
+                             | _ -> assert false)
+                          l defs in 
+                      C.Fix (n, funs)
+                  | `CoRecursive ->
+                     let funs = 
+                        List.map 
+                          (function bo ->
+                             match bo with
+                              `Proof bo ->
+                                 (match 
+                                    bo.Con.proof_conclude.Con.conclude_conclusion,
+                                    bo.Con.proof_name 
+                                  with
+                                     Some ty, Some name ->
+                                      (name,term2cic ty,proof2cic premise_env bo)
+                                   | _,_ -> assert false)
+                             | _ -> assert false)
+                           defs in 
+                      C.CoFix (n, funs)
+                  | _ -> (* no inductive types in local contexts *)
+                       assert false)
+             | _ -> assert false)
 
   and conclude2cic premise_env conclude =
     let module C = Cic in 
@@ -100,6 +137,10 @@ let proof2cic term2cic p =
     else if conclude.Con.conclude_method = "Exact" then
       (match conclude.Con.conclude_args with
          [Con.Term t] -> term2cic t
+       | [Con.Premise prem] -> 
+           (match prem.Con.premise_n with
+              None -> assert false
+            | Some n -> C.Rel n)
        | _ -> prerr_endline "3"; assert false)
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with