The Aux argument of conclude is now of type string (used to be int).

Case Fixed.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 2749708d2018ec609e8132f689d02f40ad9e781a..149fd90ec4389dfb47015cbb16dc2803e976fcf3 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -465,46 +465,50 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
+        let inductive_types =
+           (match CicEnvironment.get_obj uri with
+               Cic.Constant _ -> assert false
+             | Cic.Variable _ -> assert false
+             | Cic.CurrentProof _ -> assert false
+             | Cic.InductiveDefinition (l,_,_) -> l 
+           ) in
+        let (_,_,_,constructors) = List.nth inductive_types typeno in 
         let teid = get_id te in
-        let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
-        (match 
-          (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
-           with Not_found -> None)
-         with
-             Some tety -> (* we must lift up the argument *)
+        let pp = List.map2 
+          (fun p (name,_) -> (K.ArgProof (aux ~name p))) 
+           patterns constructors in
+        let apply_context,term =
+          (match 
+            (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
+             with Not_found -> None)
+           with
+             Some tety -> 
                let p = (aux te) in
-               { K.proof_name = Some "name";
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = flat seed p;
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with Not_found -> None  
-                   }
-               }
-           | None ->
-               { K.proof_name = name;
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = [];
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with Not_found -> None 
-                   }
-               }
-         )  
+               (flat seed p, 
+                K.Premise
+                { K.premise_id = gen_id seed; 
+                   K.premise_xref = p.K.proof_id;
+                   K.premise_binder = p.K.proof_name;
+                   K.premise_n = None
+                 })
+           | None -> [],K.Term te) in
+        { K.proof_name = name;
+          K.proof_id   = gen_id seed;
+          K.proof_context = []; 
+          K.proof_apply_context = apply_context;
+          K.proof_conclude = 
+            { K.conclude_id = gen_id seed; 
+              K.conclude_aref = id;
+              K.conclude_method = "Case";
+              K.conclude_args = 
+                (K.Aux (UriManager.string_of_uri uri))::
+                (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+              K.conclude_conclusion = 
+                try Some 
+                  (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+                with Not_found -> None  
+             }
+        }
     | C.AFix (id, no, funs) -> 
         let proofs = 
           List.map 
@@ -696,7 +700,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_aref = id;
                 K.conclude_method = "ByInduction";
                 K.conclude_args =
-                  K.Aux no_constructors 
+                  K.Aux (string_of_int no_constructors) 
                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
                   ::method_args@other_method_args;
                 K.conclude_conclusion = 

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index 2f956d7d11a7aa59a026173900808112c38cc6cc..a09e25cf2b3b46323192d4744e28fcaa95be7d4a 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -121,7 +121,7 @@ and 'term conclude_item =
        }
 
 and 'term arg =
-         Aux of int
+         Aux of string
        | Premise of premise
        | Term of 'term
        | ArgProof of 'term proof

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index 864db1800dc710b97cbe8540d569ff2fae1a03e0..813a31053df36cbccca8dda5f1fbb5633ea86313 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -112,7 +112,7 @@ and 'term conclude_item =
        }
 
 and 'term arg =
-         Aux of int
+         Aux of string
        | Premise of premise
        | Term of 'term
        | ArgProof of 'term proof

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 1d4dcd1ee885bbaac4c9daa0be69f0f18e4a5220..d25d7942595f8b20348b1dc37596516f678f3dfd 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -167,10 +167,29 @@ let proof2cic deannotate p =
            let  cargs = args2cic premise_env args in
            C.Appl (C.Const(uri,subst)::cargs)
        | _ -> prerr_endline "6"; assert false)
+    else if (conclude.Con.conclude_method = "Case") then
+      (match conclude.Con.conclude_args with
+        Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+           C.MutCase
+            (UriManager.uri_of_string uri,
+             int_of_string notype, deannotate ty, 
+             List.assoc prem.Con.premise_xref premise_env,
+             List.map 
+               (function 
+                   Con.ArgProof p -> proof2cic [] p
+                | _ -> prerr_endline "7a"; assert false) patterns)
+      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
+            (UriManager.uri_of_string uri,
+             int_of_string notype, deannotate ty, deannotate te,
+             List.map 
+               (function 
+                   (Con.ArgProof p) -> proof2cic [] p
+                | _ -> prerr_endline "7a"; assert false) patterns) 
+      | _ -> (prerr_endline "7"; assert false))
     else if (conclude.Con.conclude_method = "Apply") then
       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
       C.Appl cargs 
-    else (prerr_endline "7"; assert false)
+    else (prerr_endline "8"; assert false)
 
   and args2cic premise_env l =
     List.map (arg2cic premise_env) l

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index 3bc8bb306ae6cf0896e2d662ab9c516218856751..b51cba99d384c144fdc6861155063fdedb62964a 100644 (file)
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ b/helm/ocaml/cic_omdoc/contentPp.ml
@@ -130,7 +130,7 @@ and pargs args indent =
 and parg indent =
   let module Con = Content in
   function
-       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr
+       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n);flush stderr
     |  Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr
     | Con.Term t -> 
         prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)));