bugfix: return unshared sequent when applying cic -> mathml transformations so that...

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

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 69c91cdb3eb959d07fa1e8592ddf80adc518de02..81cfaaf099e7290d52a37ddccb2724c4defa92ea 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -23,25 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
-
-let sort_of_string = function
-  | "Prop" -> `Prop
-  | "Set" -> `Set
-  | "Type" -> `Type
-  | "CProp" -> `CProp
-  | _ -> assert false
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
-  | `Type -> "Type"
+  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
   | `CProp -> "CProp"
 
 let sort_of_sort = function
   | Cic.Prop  -> `Prop
   | Cic.Set   -> `Set
-  | Cic.Type _ -> `Type
+  | Cic.Type u -> `Type u
   | Cic.CProp -> `CProp
 
 (* let hashtbl_add_time = ref 0.0;; *)
@@ -134,8 +127,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
        match CicReduction.whd context t with 
           C.Sort C.Prop  -> `Prop
         | C.Sort C.Set   -> `Set
-        | C.Sort (C.Type _)
-        | C.Meta _       -> `Type
+        | C.Sort (C.Type u) -> `Type u
+        | C.Meta _       -> `Type (CicUniv.fresh())
         | C.Sort C.CProp -> `CProp
         | t              ->
             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
@@ -188,7 +181,8 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
         with
          Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
           (* CSC: Type or Set? I can not tell *)
-          None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false 
+          let u = CicUniv.fresh() in
+          None,Cic.Sort (Cic.Type u),`Type u,false 
          (* TASSI non dovrebbe fare danni *)
 (* *)
        in
@@ -388,7 +382,7 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            Hashtbl.add ids_to_hypotheses hid binding ;
            incr hypotheses_seed ;
            match binding with
-               Some (n,Cic.Def (t,None)) ->
+               Some (n,Cic.Def (t,_)) ->
                  let acic = acic_of_cic_context context idrefs t None in
                  (binding::context),
                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
@@ -399,7 +393,6 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
              | None ->
                  (* Invariant: "" is never looked up *)
                   (None::context),((hid,None)::acontext),""::idrefs
-             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) context ([],[],[])
        )
   in 
@@ -415,7 +408,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let ids_to_hypotheses = Hashtbl.create 23 in
     let hypotheses_seed = ref 0 in
     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
-    let sequent =
+    let unsh_sequent =
      let i,canonical_context,term = sequent in
       let canonical_context' =
        List.fold_right
@@ -427,7 +420,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
                Some (n, Cic.Decl (Unshare.unshare t))
             | Some (n, Cic.Def (t,None)) ->
                Some (n, Cic.Def ((Unshare.unshare t),None))
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
           in
            d::canonical_context'
         ) canonical_context []
@@ -438,9 +432,10 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let (metano,acontext,agoal) = 
       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
-      metasenv sequent in
-    ("i0",metano,acontext,agoal), 
-     ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
+      metasenv unsh_sequent in
+    (unsh_sequent,
+     (("i0",metano,acontext,agoal), 
+      ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
 let acic_object_of_cic_object ?(eta_fix=true) obj =