From: Claudio Sacerdoti Coen Date: Wed, 21 Sep 2005 15:34:15 +0000 (+0000) Subject: We do not longer generate inner-types and inner-sorts for XML files generated X-Git-Tag: LAST_BEFORE_NEW~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c8a5bd44cf3de45e2736d45bfb8b9b23835b309b;p=helm.git We do not longer generate inner-types and inner-sorts for XML files generated by matitac. We will have to implement a -export flag to matitac to generate them. This represents yet another important speed-up. --- diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 4b7c940e9..887ed975f 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -349,6 +349,7 @@ let end_element ctxt tag = | "REL" -> push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id; "idref", idref; "value", value] | ["binder", binder; "id", id; "idref", idref; "sort", _; "value", value] -> Cic.ARel (id, idref, int_of_string value, binder) @@ -356,12 +357,14 @@ let end_element ctxt tag = | "VAR" -> push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "uri", uri] | ["id", id; "sort", _; "uri", uri] -> Cic.AVar (id, uri_of_string uri, []) | _ -> attribute_error ())) | "CONST" -> push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "uri", uri] | ["id", id; "sort", _; "uri", uri] -> Cic.AConst (id, uri_of_string uri, []) | _ -> attribute_error ())) @@ -374,22 +377,27 @@ let end_element ctxt tag = let args = pop_cics ctxt in push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id ] | ["id", id; "sort", _] -> Cic.AAppl (id, args) | _ -> attribute_error ())) | "decl" -> let source = pop_cic ctxt in push ctxt (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id ] | ["binder", binder; "id", id; "type", _] -> Decl (id, Cic.Name binder, source) + | ["id", id] | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) | _ -> attribute_error ()) | "def" -> (* same as "decl" above *) let source = pop_cic ctxt in push ctxt (match pop_tag_attrs ctxt with + | ["binder", binder; "id", id] | ["binder", binder; "id", id; "sort", _] -> Def (id, Cic.Name binder, source) + | ["id", id] | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source) | _ -> attribute_error ()) | "arity" (* transparent elements (i.e. which contain a CIC) *) @@ -422,6 +430,7 @@ let end_element ctxt tag = in let term = add_decl target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["type", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -436,6 +445,7 @@ let end_element ctxt tag = in let term = add_decl target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["sort", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -450,6 +460,7 @@ let end_element ctxt tag = in let term = add_def target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["sort", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -458,6 +469,7 @@ let end_element ctxt tag = let term = pop_cic ctxt in push ctxt (Cic_term (match pop_tag_attrs ctxt with + ["id", id] | ["id", id; "sort", _] -> Cic.ACast (id, term, typ) | _ -> attribute_error ())); | "IMPLICIT" -> @@ -478,6 +490,7 @@ let end_element ctxt tag = let meta_substs = pop_meta_substs ctxt in push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "no", no] | ["id", id; "no", no; "sort", _] -> Cic.AMeta (id, int_of_string no, meta_substs) | _ -> attribute_error ())); @@ -490,6 +503,7 @@ let end_element ctxt tag = | "MUTCONSTRUCT" -> push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri] | ["id", id; "noConstr", noConstr; "noType", noType; "sort", _; "uri", uri] -> Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType, @@ -515,6 +529,7 @@ let end_element ctxt tag = let fix_funs = pop_fix_funs ctxt in push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "noFun", noFun] | ["id", id; "noFun", noFun; "sort", _] -> Cic.AFix (id, int_of_string noFun, fix_funs) | _ -> attribute_error ())) @@ -522,6 +537,7 @@ let end_element ctxt tag = let cofix_funs = pop_cofix_funs ctxt in push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "noFun", noFun] | ["id", id; "noFun", noFun; "sort", _] -> Cic.ACoFix (id, int_of_string noFun, cofix_funs) | _ -> attribute_error ())) @@ -530,6 +546,7 @@ let end_element ctxt tag = | patternsType :: inductiveTerm :: patterns -> push ctxt (Cic_term (match pop_tag_attrs ctxt with + | ["id", id; "noType", noType; "uriType", uriType] | ["id", id; "noType", noType; "sort", _; "uriType", uriType] -> Cic.AMutCase (id, uri_of_string uriType, int_of_string noType, patternsType, inductiveTerm, patterns) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 2c3b9fb62..69c91cdb3 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -585,3 +585,137 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, ids_to_conjectures,ids_to_hypotheses ;; + +let plain_acic_term_of_cic_term = + let module C = Cic in + let mk_fresh_id = + let id = ref 0 in + function () -> incr id; "i" ^ string_of_int !id in + let rec aux context t = + let fresh_id = mk_fresh_id () in + match t with + C.Rel n -> + let idref,id = + match get_nth context n with + idref,(Some (C.Name s,_)) -> idref,s + | idref,_ -> idref,"__" ^ string_of_int n + in + C.ARel (fresh_id, idref, n, id) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux context t)) exp_named_subst + in + C.AVar (fresh_id,uri,exp_named_subst') + | C.Implicit _ + | C.Meta _ -> assert false + | C.Sort s -> C.ASort (fresh_id, s) + | C.Cast (v,t) -> + C.ACast (fresh_id, aux context v, aux context t) + | C.Prod (n,s,t) -> + C.AProd + (fresh_id, n, aux context s, + aux ((fresh_id, Some (n, C.Decl s))::context) t) + | C.Lambda (n,s,t) -> + C.ALambda + (fresh_id,n, aux context s, + aux ((fresh_id, Some (n, C.Decl s))::context) t) + | C.LetIn (n,s,t) -> + C.ALetIn + (fresh_id, n, aux context s, + aux ((fresh_id, Some (n, C.Def(s,None)))::context) t) + | C.Appl l -> + C.AAppl (fresh_id, List.map (aux context) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux context t)) exp_named_subst + in + C.AConst (fresh_id, uri, exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux context t)) exp_named_subst + in + C.AMutInd (fresh_id, uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function i,t -> i, (aux context t)) exp_named_subst + in + C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst') + | C.MutCase (uri, tyno, outty, term, patterns) -> + C.AMutCase (fresh_id, uri, tyno, aux context outty, + aux context term, List.map (aux context) patterns) + | C.Fix (funno, funs) -> + let tys = + List.map + (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs + in + C.AFix (fresh_id, funno, + List.map2 + (fun (id,_) (name, indidx, ty, bo) -> + (id, name, indidx, aux context ty, aux (tys@context) bo) + ) tys funs + ) + | C.CoFix (funno, funs) -> + let tys = + List.map (fun (name,ty,_) -> + mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs + in + C.ACoFix (fresh_id, funno, + List.map2 + (fun (id,_) (name, ty, bo) -> + (id, name, aux context ty, aux (tys@context) bo) + ) tys funs + ) + in + aux +;; + +let plain_acic_object_of_cic_object obj = + let module C = Cic in + let mk_fresh_id = + let id = ref 0 in + function () -> incr id; "it" ^ string_of_int !id + in + match obj with + C.Constant (id,Some bo,ty,params,attrs) -> + let abo = plain_acic_term_of_cic_term [] bo in + let aty = plain_acic_term_of_cic_term [] ty in + C.AConstant + ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs) + | C.Constant (id,None,ty,params,attrs) -> + let aty = plain_acic_term_of_cic_term [] ty in + C.AConstant + ("mettereaposto",None,id,None,aty,params,attrs) + | C.Variable (id,bo,ty,params,attrs) -> + let abo = + match bo with + None -> None + | Some bo -> Some (plain_acic_term_of_cic_term [] bo) + in + let aty = plain_acic_term_of_cic_term [] ty in + C.AVariable + ("mettereaposto",id,abo,aty,params,attrs) + | C.CurrentProof _ -> assert false + | C.InductiveDefinition (tys,params,paramsno,attrs) -> + let context = + List.map + (fun (name,_,arity,_) -> + mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in + let atys = + List.map2 + (fun (id,_) (name,inductive,ty,cons) -> + let acons = + List.map + (function (name,ty) -> + (name, + plain_acic_term_of_cic_term context ty) + ) cons + in + (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons) + ) context tys + in + C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs) +;; diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index ff75618f8..abe61f387 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -57,3 +57,4 @@ val asequent_of_sequent : (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) +val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 3ca6a3a50..5bd9fd1c9 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -39,9 +39,12 @@ let param_attribute_of_params params = ;; (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -let print_term ~ids_to_inner_sorts = - let find_sort id = - Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id) +let print_term ?ids_to_inner_sorts = + let find_sort name id = + match ids_to_inner_sorts with + None -> [] + | Some ids_to_inner_sorts -> + [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)] in let rec aux = let module C = Cic in @@ -49,20 +52,21 @@ let print_term ~ids_to_inner_sorts = let module U = UriManager in function C.ARel (id,idref,n,b) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_empty "REL" - [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; - None,"idref",idref ; None,"sort",sort] + (sort @ + [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; + None,"idref",idref]) | C.AVar (id,uri,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "VAR" - [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) + (sort @ [None,"uri",U.string_of_uri uri;None,"id",id])) exp_named_subst | C.AMeta (id,n,l) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "META" - [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"no",(string_of_int n) ; None,"id",id]) (List.fold_left (fun i t -> match t with @@ -86,24 +90,24 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let prods,t = eat_prods prods in - let sort = find_sort last_id in - X.xml_nempty "PROD" [None,"type",sort] + let sort = find_sort "type" last_id in + X.xml_nempty "PROD" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort (Cic2acic.source_id_of_id id) in + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in let attrs = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] prods ; X.xml_nempty "target" [] (aux t) >] | C.ACast (id,v,t) -> - let sort = find_sort id in - X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] + let sort = find_sort "sort" id in + X.xml_nempty "CAST" (sort @ [None,"id",id]) [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) >] @@ -116,16 +120,16 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let lambdas,t = eat_lambdas lambdas in - let sort = find_sort last_id in - X.xml_nempty "LAMBDA" [None,"sort",sort] + let sort = find_sort "sort" last_id in + X.xml_nempty "LAMBDA" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort (Cic2acic.source_id_of_id id) in + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in let attrs = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] lambdas ; @@ -142,31 +146,31 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let letins,t = eat_letins letins in - let sort = find_sort last_id in - X.xml_nempty "LETIN" [None,"sort",sort] + let sort = find_sort "sort" last_id in + X.xml_nempty "LETIN" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort id in + let sort = find_sort "sort" id in let attrs = - (None,"id",id)::(None,"sort",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) in [< i ; X.xml_nempty "def" attrs (aux s) >] ) [< >] letins ; X.xml_nempty "target" [] (aux t) >] | C.AAppl (id,li) -> - let sort = find_sort id in - X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] + let sort = find_sort "sort" id in + X.xml_nempty "APPLY" (sort @ [None,"id",id]) [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] | C.AConst (id,uri,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "CONST" - [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id]) ) exp_named_subst | C.AMutInd (id,uri,i,exp_named_subst) -> aux_subst uri @@ -176,20 +180,22 @@ let print_term ~ids_to_inner_sorts = None, "id", id] ) exp_named_subst | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "MUTCONSTRUCT" - [None,"uri", (U.string_of_uri uri) ; - None,"noType",(string_of_int i) ; - None,"noConstr",(string_of_int j) ; - None,"id",id ; None,"sort",sort] + (sort @ + [None,"uri", (U.string_of_uri uri) ; + None,"noType",(string_of_int i) ; + None,"noConstr",(string_of_int j) ; + None,"id",id]) ) exp_named_subst | C.AMutCase (id,uri,typeno,ty,te,patterns) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "MUTCASE" - [None,"uriType",(U.string_of_uri uri) ; - None,"noType", (string_of_int typeno) ; - None,"id", id ; None,"sort",sort] + (sort @ + [None,"uriType",(U.string_of_uri uri) ; + None,"noType", (string_of_int typeno) ; + None,"id", id]) [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; List.fold_right @@ -197,9 +203,9 @@ let print_term ~ids_to_inner_sorts = patterns [<>] >] | C.AFix (id, no, funs) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "FIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) [< List.fold_right (fun (id,fi,ai,ti,bi) i -> [< X.xml_nempty "FixFunction" @@ -213,9 +219,9 @@ let print_term ~ids_to_inner_sorts = ) funs [<>] >] | C.ACoFix (id,no,funs) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "COFIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) [< List.fold_right (fun (id,fi,ti,bi) i -> [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] @@ -295,10 +301,7 @@ let xml_of_attrs attributes = in Xml.xml_nempty "attributes" [] xml_attrs -let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = - let find_sort id = - Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id) - in +let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj = let module C = Cic in let module X = Xml in let module U = UriManager in @@ -327,30 +330,30 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = C.Name n' -> [None,"id",hid;None,"name",n'] | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) | Some (n,C.ADef t) -> X.xml_nempty "Def" (match n with C.Name n' -> [None,"id",hid;None,"name",n'] | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) | None -> X.xml_empty "Hidden" [None,"id",hid] ) ; i >] ) [< >] canonical_context ; X.xml_nempty "Goal" [] - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) >] >]) [< >] conjectures ; - X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] + X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >] in let xml_for_current_proof_type = X.xml_nempty "ConstantType" [None,"name",n ; None,"params",params' ; None,"id", id] - (print_term ids_to_inner_sorts ty) + (print_term ?ids_to_inner_sorts ty) in let xmlbo = [< X.xml_cdata "\n" ; @@ -379,7 +382,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_nempty "ConstantBody" [None,"for",UriManager.string_of_uri uri ; None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts bo >] + [< print_term ?ids_to_inner_sorts bo >] >] in let xmlty = @@ -387,7 +390,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n"); X.xml_nempty "ConstantType" [None,"name",n ; None,"params",params' ; None,"id", id] - [< xml_attrs; print_term ids_to_inner_sorts ty >] + [< xml_attrs; print_term ?ids_to_inner_sorts ty >] >] in xmlty, xmlbo @@ -398,7 +401,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = match bo with None -> [< >] | Some bo -> - X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >] + X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >] in let aobj = [< X.xml_cdata "\n" ; @@ -406,7 +409,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_nempty "Variable" [None,"name",n ; None,"params",params' ; None,"id", id] [< xml_attrs; xmlbo; - X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) + X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty) >] >] in @@ -430,13 +433,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = None,"inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] - (print_term ids_to_inner_sorts arity) ; + (print_term ?ids_to_inner_sorts arity) ; (List.fold_left (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" [None,"name",name] - (print_term ids_to_inner_sorts lc) + (print_term ?ids_to_inner_sorts lc) >]) [<>] cons ) >] @@ -463,11 +466,11 @@ let [< x ; X.xml_nempty "TYPE" [None,"of",id] [< X.xml_nempty "synthesized" [] - [< print_term ids_to_inner_sorts synty >] ; + [< print_term ~ids_to_inner_sorts synty >] ; match expty with None -> [<>] | Some expty' -> X.xml_nempty "expected" [] - [< print_term ids_to_inner_sorts expty' >] + [< print_term ~ids_to_inner_sorts expty' >] >] >] ) ids_to_inner_types [<>] diff --git a/helm/ocaml/cic_transformations/cic2Xml.mli b/helm/ocaml/cic_transformations/cic2Xml.mli index 47202dd01..22c5669df 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.mli +++ b/helm/ocaml/cic_transformations/cic2Xml.mli @@ -26,13 +26,13 @@ exception NotImplemented val print_term : - ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> + ?ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm -> Xml.token Stream.t val print_object : UriManager.uri -> - ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> + ?ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> ask_dtd_to_the_getter:bool -> Cic.annobj -> Xml.token Stream.t * Xml.token Stream.t option