X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=f1c648e9bdef5bb847bebda860df0b42f1cfd1b2;hb=f15a13bab100064a4da238cede323b8d4568c174;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..f1c648e9b 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 *) @@ -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/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 *) @@ -112,7 +114,7 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.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 +122,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 +131,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" @@ -275,7 +277,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) -> @@ -326,13 +336,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) -> @@ -348,14 +359,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 =