X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=65216f5d6a1677ce8f943150601fce54184e720d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=22f959927335208c2a9bf45c73c8fe7819a11d29;hpb=4a5311d795b19019a675f60c33710301873f646c;p=helm.git diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 22f959927..65216f5d6 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -36,7 +36,7 @@ (* the type cexpr is inspired by OpenMath. A few primitive constructors have been added, in order to take into account some special features of functional expressions. Most notably: case, let in, let rec, and - explicit substitutons *) + explicit substitutions *) type cexpr = Symbol of string option * string * subst option * string option @@ -67,62 +67,63 @@ and let symbol_table = Hashtbl.create 503;; (* eq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic/eq.ind")) + None, Some HelmLibraryObjects.Logic.eq_SURI)) :: List.map acic2cexpr (List.tl args)));; -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_Type/eqT.ind")) - :: List.map acic2cexpr (List.tl args)));; - (* and *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "and", - None, Some "cic:/Coq/Init/Logic/and.ind")) + None, Some HelmLibraryObjects.Logic.and_SURI)) :: List.map acic2cexpr args));; (* or *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "or", - None, Some "cic:/Coq/Init/Logic/or.ind")) + None, Some HelmLibraryObjects.Logic.or_SURI)) :: List.map acic2cexpr args));; (* iff *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "iff", - None, Some "cic:/Coq/Init/Logic/iff.con")) + None, Some HelmLibraryObjects.Logic.iff_SURI)) :: List.map acic2cexpr args));; (* not *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "not", - None, Some "cic:/Coq/Init/Logic/not.con")) + None, Some HelmLibraryObjects.Logic.not_SURI)) :: List.map acic2cexpr args));; -(* exists *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" +(* Rinv *) +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI (fun aid sid args acic2cexpr -> - match (List.tl args) with - [Cic.ALambda (_,Cic.Name n,s,t)] -> - Binder - (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t) - | _ -> raise Not_found);; + Appl + (Some aid, (Symbol (Some sid, "inv", + None, Some HelmLibraryObjects.Reals.rinv_SURI)) + :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" +(* Ropp *) +Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "opp", + None, Some HelmLibraryObjects.Reals.ropp_SURI)) + :: List.map acic2cexpr args));; + +(* exists *) +Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI (fun aid sid args acic2cexpr -> match (List.tl args) with [Cic.ALambda (_,Cic.Name n,s,t)] -> @@ -131,123 +132,148 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" | _ -> raise Not_found);; (* leq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Init/Peano/le.ind")) + None, Some HelmLibraryObjects.Peano.le_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con")) + None, Some HelmLibraryObjects.Reals.rle_SURI)) :: List.map acic2cexpr args));; (* lt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Init/Peano/lt.con")) + None, Some HelmLibraryObjects.Peano.lt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con")) + None, Some HelmLibraryObjects.Reals.rlt_SURI)) :: List.map acic2cexpr args));; (* geq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Init/Peano/ge.con")) + None, Some HelmLibraryObjects.Peano.ge_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con")) + None, Some HelmLibraryObjects.Reals.rge_SURI)) :: List.map acic2cexpr args));; (* gt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Init/Peano/gt.con")) + None, Some HelmLibraryObjects.Peano.gt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con")) + None, Some HelmLibraryObjects.Reals.rgt_SURI)) :: List.map acic2cexpr args));; (* plus *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/Init/Peano/plus.con")) + None, Some HelmLibraryObjects.Peano.plus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con")) + None, Some HelmLibraryObjects.BinInt.zplus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI (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 HelmLibraryObjects.Reals.rplus_SURI)) + :: List.map acic2cexpr args) + in + let rec aux acc = function + | [ Cic.AConst (nid, uri, []); n] when + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> + (match n with + | Cic.AConst (_, uri, []) when + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> + Num (Some aid, string_of_int (acc + 2)) + | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when + UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI -> + aux (acc + 1) args + | _ -> appl ()) + | _ -> appl () + in + aux 0 args) +;; + +(* zero and one *) + +Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI + (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;; + +Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI + (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;; (* times *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "times", - None, Some "cic:/Coq/Init/Peano/mult.con")) + None, Some HelmLibraryObjects.Peano.mult_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "times", - None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con")) + None, Some HelmLibraryObjects.Reals.rmult_SURI)) :: List.map acic2cexpr args));; (* minus *) -Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "minus", - None, Some "cic:/Coq/Arith/Minus/mult.con")) + None, Some HelmLibraryObjects.Peano.minus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "minus", - None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con")) + None, Some HelmLibraryObjects.Reals.rminus_SURI)) :: List.map acic2cexpr args));; (* div *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "div", - None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con")) + None, Some HelmLibraryObjects.Reals.rdiv_SURI)) :: List.map acic2cexpr args));; @@ -258,18 +284,20 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" let string_of_sort = function - Cic.Prop -> "Prop" - | Cic.Set -> "Set" - | Cic.Type -> "Type" + Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type _ -> "Type" (* TASSI *) + | Cic.CProp -> "Type" ;; let get_constructors uri i = 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 + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with + Cic.Constant _ -> assert false + | Cic.Variable _ -> assert false + | Cic.CurrentProof _ -> assert false + | Cic.InductiveDefinition (l,_,_) -> l ) in let (_,_,_,constructors) = List.nth inductive_types i in constructors @@ -338,12 +366,13 @@ 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) -> let inductive_types = - (match CicEnvironment.get_obj uri with + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false @@ -356,17 +385,23 @@ 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 + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false