X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=2ff989da184439ef060b5344e4dcbbdbf501a89a;hb=5f45c292bf9e99bd746f6ec4c7c268022012e925;hp=b78d1380a603395b6c6d22a00e086375a28acf94;hpb=6104889dac72e3ff37b13ea997dafc4c0ef45ac3;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index b78d1380a..2ff989da1 100644
--- 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 *)
@@ -76,7 +78,7 @@ 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"))
+          None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
      :: List.map acic2cexpr (List.tl args)));;
 
 (* and *)
@@ -111,6 +113,22 @@ 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#xpointer(1/1)" 
   (fun aid sid args acic2cexpr ->
@@ -203,12 +221,41 @@ Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
           None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
      :: List.map acic2cexpr args));;
 
+let rplus_uri =
+  UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
+let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;;
+let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
+
 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" 
   (fun aid sid args acic2cexpr ->
-   Appl 
-    (Some aid, (Symbol (Some sid, "plus",
-          None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
-     :: List.map acic2cexpr args));;
+   let appl () =
+     Appl 
+      (Some aid, (Symbol (Some sid, "plus",
+            None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
+       :: List.map acic2cexpr args)
+   in
+    let rec aux acc = function
+      | [ Cic.AConst (nid, uri, []); n] when
+          UriManager.eq uri r1_uri ->
+            (match n with
+            | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+                Num (Some aid, string_of_int (acc + 2))
+            | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+                UriManager.eq uri rplus_uri ->
+                  aux (acc + 1) args
+            | _ -> appl ())
+      | _ -> appl ()
+    in
+    aux 0 args)
+;;
+
+(* zero and one *)
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" 
+  (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" 
+  (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
 
 (* times *) 
 Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" 
@@ -233,6 +280,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 +337,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) ->
@@ -313,7 +383,7 @@ let acic2cexpr ids_to_inner_sorts t =
         (try 
           (let f = Hashtbl.find symbol_table uri_str in
            f aid sid tl acic2cexpr)
-        with notfound ->
+        with Not_found ->
           Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri, 
           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
@@ -331,14 +401,19 @@ let acic2cexpr ids_to_inner_sorts t =
         (try 
           (let f = Hashtbl.find symbol_table puri_str in
            f aid sid tl acic2cexpr)
-         with notfound ->
+         with Not_found ->
            Appl (Some aid, Symbol (Some sid, name, 
            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) ->
-        Symbol (Some id, UriManager.name_of_uri uri, 
-          make_subst subst, Some (UriManager.string_of_uri uri))
+        let uri_str = UriManager.string_of_uri uri in
+        (try
+          let f = Hashtbl.find symbol_table uri_str in
+          f "dummy" id [] acic2cexpr
+        with Not_found ->
+          Symbol (Some id, UriManager.name_of_uri uri, 
+            make_subst subst, Some (UriManager.string_of_uri uri)))
     | C.AMutInd (id,uri,i,subst) ->
         let inductive_types = 
           (match CicEnvironment.get_obj uri with