From 5f45c292bf9e99bd746f6ec4c7c268022012e925 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sat, 13 Sep 2003 23:56:42 +0000 Subject: [PATCH] added notation for reals 0, 1, n --- .../content_expressions.ml | 50 ++++++++++++++++--- 1 file changed, 42 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 52318d1c0..2ff989da1 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -221,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" @@ -354,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) -> @@ -372,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 -- 2.39.2