added notation for Ropp and Rinv

[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index bb062f9cc2cce1337e038ce6cb33dc4df687c930..52318d1c010d7e25818c8a4b6d6180e995e1fe54 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -42,7 +42,7 @@ type cexpr =
     Symbol of string option * string * subst option * string option
                              (* h:xref, name, subst, definitionURL *)
   | LocalVar of (string option) * string        (* h:xref, name *)
-  | Meta of string option * string            (* h:xref, name *)
+  | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
   | Num of string option * string             (* h:xref, value *)
   | Appl of string option * cexpr list        (* h:xref, args *)
   | Binder of string option * string * decl * cexpr   
@@ -58,6 +58,8 @@ and
   def = string * cexpr               (* name, body *)
 and
   subst = (UriManager.uri * cexpr) list
+and
+  meta_subst = cexpr option list
 ;;
 
 (* NOTATION *)
@@ -65,34 +67,34 @@ and
 let symbol_table = Hashtbl.create 503;;
 
 (* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "eq",
-          None, Some "cic:/Coq/Init/Logic/eq.ind#(/1/0)"))
+          None, Some "cic:/Coq/Init/Logic/eq.ind"))
      :: List.map acic2cexpr (List.tl args)));;   
 
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "eq",
-          None, Some "cic:/Coq/Init/Logic/eqT.ind#(/1/0)"))
+          None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
      :: List.map acic2cexpr (List.tl args)));;
 
 (* and *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "and",
-          None, Some "cic:/Coq/Init/Logic/and.ind#(/1/0)"))
+          None, Some "cic:/Coq/Init/Logic/and.ind"))
      :: List.map acic2cexpr args));;
 
 (* or *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    Appl 
     (Some aid, (Symbol (Some sid, "or",
-          None, Some "cic:/Coq/Init/Logic/or.ind#(/1/0)"))
+          None, Some "cic:/Coq/Init/Logic/or.ind"))
      :: List.map acic2cexpr args));;
 
 (* iff *)
@@ -111,8 +113,24 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
           None, Some "cic:/Coq/Init/Logic/not.con"))
      :: List.map acic2cexpr args));;
 
+(* Rinv *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "inv",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+     :: List.map acic2cexpr args));;
+
+(* Ropp *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "opp",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+     :: List.map acic2cexpr args));;
+
 (* exists *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    match (List.tl args) with
      [Cic.ALambda (_,Cic.Name n,s,t)] ->
@@ -120,7 +138,7 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#(/1/0)"
         (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
   | _ -> raise Not_found);;
 
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    match (List.tl args) with
      [Cic.ALambda (_,Cic.Name n,s,t)] ->
@@ -129,11 +147,11 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#(/1/0)"
   | _ -> raise Not_found);;
 
 (* leq *) 
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#(/1/0)" 
+Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
    Appl
     (Some aid, (Symbol (Some sid, "leq",
-          None, Some "cic:/Coq/Init/Peano/le.ind#(/1/0)"))
+          None, Some "cic:/Coq/Init/Peano/le.ind"))
      :: List.map acic2cexpr args));;
 
 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" 
@@ -233,6 +251,21 @@ Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
           None, Some "cic:/Coq/Arith/Minus/mult.con"))
      :: List.map acic2cexpr args));;
 
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" 
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "minus",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+     :: List.map acic2cexpr args));;
+
+(* div *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" 
+  (fun aid sid args acic2cexpr ->
+   Appl 
+    (Some aid, (Symbol (Some sid, "div",
+          None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+     :: List.map acic2cexpr args));;
+
 
 
 
@@ -275,7 +308,15 @@ let acic2cexpr ids_to_inner_sorts t =
     | C.AVar (id,uri,subst) ->
         Symbol (Some id, UriManager.name_of_uri uri, 
           make_subst subst, Some (UriManager.string_of_uri uri))
-    | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
+    | C.AMeta (id,n,l) ->
+       let l' =
+        List.rev_map
+         (function
+             None -> None
+           | Some t -> Some (acic2cexpr t)
+         ) l
+       in
+        Meta (Some id,("?" ^ (string_of_int n)),l')
     | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (id,n,s,t) ->
@@ -296,11 +337,12 @@ let acic2cexpr ids_to_inner_sorts t =
              Binder (Some id,binder,decl,acic2cexpr t)) 
     | C.ACast (id,v,t) -> acic2cexpr v
     | C.ALambda (id,n,s,t) ->
-        (match n with
-           Cic.Anonymous -> assert false
-         | Cic.Name name ->
-             let decl = (name, acic2cexpr s) in 
-             Binder (Some id,"Lambda",decl,acic2cexpr t))
+        let name =
+          (match n with
+             Cic.Anonymous -> "_"
+           | Cic.Name name -> name) in
+        let decl = (name, acic2cexpr s) in 
+        Binder (Some id,"Lambda",decl,acic2cexpr t)
     | C.ALetIn (id,n,s,t) ->
         (match n with
            Cic.Anonymous -> assert false
@@ -325,13 +367,14 @@ let acic2cexpr ids_to_inner_sorts t =
           ) in
         let (name,_,_,_) = List.nth inductive_types i in
         let uri_str = UriManager.string_of_uri uri in
-        let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ ")") in
+        let puri_str =
+         uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
         (try 
           (let f = Hashtbl.find symbol_table puri_str in
            f aid sid tl acic2cexpr)
          with notfound ->
            Appl (Some aid, Symbol (Some sid, name, 
-           make_subst subst, Some puri_str)::List.map acic2cexpr tl)) 
+           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
     | C.AAppl (id,li) ->
         Appl (Some id, List.map acic2cexpr li)
     | C.AConst (id,uri,subst) ->
@@ -347,14 +390,12 @@ let acic2cexpr ids_to_inner_sorts t =
           ) in
         let (name,_,_,_) = List.nth inductive_types i in
         let uri_str = UriManager.string_of_uri uri in
-        let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ ")") in 
-        Symbol (Some id, name, make_subst subst, Some puri_str)
+        Symbol (Some id, name, make_subst subst, Some uri_str)
     | C.AMutConstruct (id,uri,i,j,subst) ->
         let constructors = get_constructors uri i in
         let (name,_) = List.nth constructors (j-1) in
         let uri_str = UriManager.string_of_uri uri in
-        let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ "/" ^ (string_of_int j) ^ ")") in
-        Symbol (Some id, name, make_subst subst, Some puri_str)
+        Symbol (Some id, name, make_subst subst, Some uri_str)
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let constructors = get_constructors uri typeno in
         let named_patterns =