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=da6eb714ad5087544edc87a787395e697fe8f46d;hpb=21bf57e0b7de37faa4991e136cf6f09cfbf4d0a3;p=helm.git diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index da6eb714a..65216f5d6 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -36,13 +36,13 @@ (* 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 (* 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,62 +67,63 @@ and let symbol_table = Hashtbl.create 503;; (* eq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#(/1/0)" +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#(/1/0)")) + None, Some HelmLibraryObjects.Logic.eq_SURI)) :: List.map acic2cexpr (List.tl args)));; -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#(/1/0)" - (fun aid sid args acic2cexpr -> - Appl - (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic/eqT.ind#(/1/0)")) - :: List.map acic2cexpr (List.tl args)));; - (* and *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#(/1/0)" +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#(/1/0)")) + None, Some HelmLibraryObjects.Logic.and_SURI)) :: List.map acic2cexpr args));; (* or *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#(/1/0)" +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#(/1/0)")) + 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#(/1/0)" +(* 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#(/1/0)" +(* 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)] -> @@ -129,108 +132,148 @@ 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 HelmLibraryObjects.Peano.le_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Init/Peano/le.ind#(/1/0)")) + 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 HelmLibraryObjects.Peano.minus_SURI)) + :: List.map acic2cexpr args));; + +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "minus", - None, Some "cic:/Coq/Arith/Minus/mult.con")) + None, Some HelmLibraryObjects.Reals.rminus_SURI)) + :: List.map acic2cexpr args));; + +(* div *) +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI + (fun aid sid args acic2cexpr -> + Appl + (Some aid, (Symbol (Some sid, "div", + None, Some HelmLibraryObjects.Reals.rdiv_SURI)) :: List.map acic2cexpr args));; @@ -241,18 +284,20 @@ Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.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 @@ -275,7 +320,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,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 @@ -326,21 +380,28 @@ 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 -> + with Not_found -> 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) -> - 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 @@ -348,14 +409,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 =