From ff981d975589f8d21a364e7cfe875647f7483cd9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 31 May 2005 22:37:56 +0000 Subject: [PATCH] Changed type of ids_to_inner_sort table used in transformation. It used to be (Cic.id, string) Hashtbl.t, now is (Cic.id, Cic2acic.sort_kind) Hashtbl.t where sort_kind is [ `Type | `Prop | `CProp | `Set ]. String "?", formerly used to denotes meta variable, is not mapped in sort_kind; since it was uniformly treated as "Type", `Type is now used for metas --- helm/ocaml/cic_omdoc/cic2acic.ml | 93 +++++++++++-------- helm/ocaml/cic_omdoc/cic2acic.mli | 13 ++- helm/ocaml/cic_omdoc/cic2content.ml | 49 +++++----- helm/ocaml/cic_omdoc/cic2content.mli | 6 +- helm/ocaml/cic_transformations/acic2Ast.ml | 10 +- helm/ocaml/cic_transformations/acic2Ast.mli | 5 +- .../applyTransformation.mli | 34 +++---- helm/ocaml/cic_transformations/cic2Xml.ml | 53 ++++++----- helm/ocaml/cic_transformations/cic2Xml.mli | 7 +- .../cic_transformations/content2pres.mli | 7 +- .../cic_transformations/sequent2pres.mli | 2 +- 11 files changed, 151 insertions(+), 128 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index c2a832cbe..608f6d7c3 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -23,23 +23,44 @@ * http://cs.unibo.it/helm/. *) -let hashtbl_add_time = ref 0.0;; +type sort_kind = [ `Prop | `Set | `Type | `CProp ] + +let sort_of_string = function + | "Prop" -> `Prop + | "Set" -> `Set + | "Type" -> `Type + | "CProp" -> `CProp + | _ -> assert false + +let string_of_sort = function + | `Prop -> "Prop" + | `Set -> "Set" + | `Type -> "Type" + | `CProp -> "CProp" + +let sort_of_sort = function + | Cic.Prop -> `Prop + | Cic.Set -> `Set + | Cic.Type _ -> `Type + | Cic.CProp -> `CProp + +(* let hashtbl_add_time = ref 0.0;; *) let xxx_add h k v = - let t1 = Sys.time () in +(* let t1 = Sys.time () in *) Hashtbl.add h k v ; - let t2 = Sys.time () in - hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 +(* let t2 = Sys.time () in + hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 *) ;; -let number_new_type_of_aux' = ref 0;; -let type_of_aux'_add_time = ref 0.0;; +(* let number_new_type_of_aux' = ref 0;; +let type_of_aux'_add_time = ref 0.0;; *) let xxx_type_of_aux' m c t = - let t1 = Sys.time () in +(* let t1 = Sys.time () in *) let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in - let t2 = Sys.time () in - type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; +(* let t2 = Sys.time () in + type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *) res ;; @@ -83,8 +104,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in (* let time1 = Sys.time () in *) let terms_to_types = - let time0 = Sys.time () in (* + let time0 = Sys.time () in let prova = CicTypeChecker.type_of_aux' metasenv context t in let time1 = Sys.time () in prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0))); @@ -109,17 +130,15 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (*CSC: This is a very inefficient way of computing inner types *) (*CSC: and inner sorts: very deep terms have their types/sorts *) (*CSC: computed again and again. *) - let string_of_sort t = + let sort_of t = match CicReduction.whd context t with - C.Sort C.Prop -> "Prop" - | C.Sort C.Set -> "Set" - | C.Sort (C.Type _) -> "Type" (* TASSI OK*) - | C.Sort C.CProp -> "CProp" - | C.Meta _ -> -(* prerr_endline "Cic2acic: string_of_sort applied to a meta" ; *) - "?" + C.Sort C.Prop -> `Prop + | C.Sort C.Set -> `Set + | C.Sort (C.Type _) + | C.Meta _ -> `Type + | C.Sort C.CProp -> `CProp | t -> -prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ; + prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ; assert false in let ainnertypes,innertype,innersort,expected_available = @@ -144,7 +163,7 @@ prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ; Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) D.expected = None} in - incr number_new_type_of_aux' ; +(* incr number_new_type_of_aux' ; *) let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in let ainnertypes,expected_available = if computeinnertypes then @@ -164,12 +183,12 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) else None,false in - ainnertypes,synthesized, string_of_sort innersort, expected_available + ainnertypes,synthesized, sort_of innersort, expected_available (*XXXXXXXX *) with Not_found -> (* l'inner-type non e' nella tabella ==> sort <> Prop *) (* CSC: Type or Set? I can not tell *) - None,Cic.Sort (Cic.Type (CicUniv.fresh())),"Type",false + None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false (* TASSI non dovrebbe fare danni *) (* *) in @@ -186,12 +205,12 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) | _ -> "__" ^ string_of_int n in xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then + if innersort = `Prop && expected_available then add_inner_type fresh_id'' ; C.ARel (fresh_id'', List.nth idrefs (n-1), n, id) | C.Var (uri,exp_named_subst) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then + if innersort = `Prop && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = List.map @@ -201,7 +220,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) | C.Meta (n,l) -> let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then + if innersort = `Prop && expected_available then add_inner_type fresh_id'' ; C.AMeta (fresh_id'', n, (List.map2 @@ -215,15 +234,15 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation) | C.Cast (v,t) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t) | C.Prod (n,s,t) -> xxx_add ids_to_inner_sorts fresh_id'' - (string_of_sort innertype) ; + (sort_of innertype) ; let sourcetype = xxx_type_of_aux' metasenv context s in xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; + (sort_of sourcetype) ; let n' = match n with C.Anonymous -> n @@ -240,8 +259,8 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) xxx_add ids_to_inner_sorts fresh_id'' innersort ; let sourcetype = xxx_type_of_aux' metasenv context s in xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - if innersort = "Prop" then + (sort_of sourcetype) ; + if innersort = `Prop then begin let father_is_lambda = match father with @@ -259,19 +278,19 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t) | C.LetIn (n,s,t) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.ALetIn (fresh_id'', n, aux' context idrefs s, aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t) | C.Appl l -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.AAppl (fresh_id'', List.map (aux' context idrefs) l) | C.Const (uri,exp_named_subst) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then + if innersort = `Prop && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = List.map @@ -286,7 +305,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) C.AMutInd (fresh_id'', uri, tyno, exp_named_subst') | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" && expected_available then + if innersort = `Prop && expected_available then add_inner_type fresh_id'' ; let exp_named_subst' = List.map @@ -295,7 +314,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst') | C.MutCase (uri, tyno, outty, term, patterns) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty, aux' context idrefs term, List.map (aux' context idrefs) patterns) @@ -307,7 +326,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.AFix (fresh_id'', funno, List.map2 @@ -324,7 +343,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs in xxx_add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then + if innersort = `Prop then add_inner_type fresh_id'' ; C.ACoFix (fresh_id'', funno, List.map2 diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli index 0288125b9..2dd0a2f31 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.mli +++ b/helm/ocaml/cic_omdoc/cic2acic.mli @@ -31,11 +31,17 @@ type anntypes = {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} ;; +type sort_kind = [ `Prop | `Set | `Type | `CProp ] + +val string_of_sort: sort_kind -> string +val sort_of_string: string -> sort_kind +val sort_of_sort: Cic.sort -> sort_kind + val acic_of_cic_context' : int ref -> (* seed *) (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) - (Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *) + (Cic.id, sort_kind) Hashtbl.t -> (* ids_to_inner_sorts *) (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) Cic.metasenv -> (* metasenv *) Cic.context -> (* context *) @@ -50,7 +56,7 @@ val acic_object_of_cic_object : Cic.annobj * (* annotated object *) (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) - (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) @@ -61,5 +67,6 @@ val asequent_of_sequent : Cic.annconjecture * (* annotated conjecture *) (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) - (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) + diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index c7d59aedc..ff8080983 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -122,7 +122,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= with Not_found -> false) | C.AMeta (id,_,_) -> (try - Hashtbl.find ids_to_inner_sorts id = "Prop" + Hashtbl.find ids_to_inner_sorts id = `Prop with Not_found -> assert false) | C.ASort (id,_) -> false | C.AImplicit _ -> raise NotImplemented @@ -300,7 +300,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts = with Not_found -> None in match sort with - | Some "Prop" -> + | Some `Prop -> `Hypothesis { K.dec_name = name_of n; K.dec_id = gen_id declaration_prefix seed; @@ -343,9 +343,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts (match t with C.ARel (idr,idref,n,b) -> let sort = - (try Hashtbl.find ids_to_inner_sorts idr - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts idr + with Not_found -> `Type) in + if sort = `Prop then K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = idr; @@ -355,9 +356,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts else (K.Term t) | C.AConst(id,uri,[]) -> let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts id + with Not_found -> `Type) in + if sort = `Prop then K.Lemma { K.lemma_id = gen_id lemma_prefix seed; K.lemma_name = UriManager.name_of_uri uri; @@ -366,9 +368,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts else (K.Term t) | C.AMutConstruct(id,uri,tyno,consno,[]) -> let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts id + with Not_found -> `Type) in + if sort = `Prop then let inductive_types = (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri @@ -408,7 +411,7 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then (let p = (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) in @@ -436,17 +439,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = match t with C.ARel (id,idref,n,b) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AVar (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMeta (id,n,l) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.ASort (id,s) -> raise Not_a_proof @@ -455,7 +458,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = | C.ACast (id,v,t) -> aux v | C.ALambda (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -475,7 +478,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.ALetIn (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -530,13 +533,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = }) | C.AConst (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> @@ -728,9 +731,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let idarg = get_id arg in let sortarg = (try (Hashtbl.find ids_to_inner_sorts idarg) - with Not_found -> "Type") in + with Not_found -> `Type) in let hdarg = - if sortarg = "Prop" then + if sortarg = `Prop then let (co,bo) = let rec bc = function @@ -813,8 +816,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = else let aid = get_id a in let asort = (try (Hashtbl.find ids_to_inner_sorts aid) - with Not_found -> "Type") in - if asort = "Prop" then + with Not_found -> `Type) in + if asort = `Prop then K.ArgProof (aux a) else K.Term a in hd::(ma_aux (n-1) tl) in diff --git a/helm/ocaml/cic_omdoc/cic2content.mli b/helm/ocaml/cic_omdoc/cic2content.mli index 10ec4b0d1..e1dfb82de 100644 --- a/helm/ocaml/cic_omdoc/cic2content.mli +++ b/helm/ocaml/cic_omdoc/cic2content.mli @@ -24,10 +24,10 @@ *) val annobj2content : - ids_to_inner_sorts:(string, string) Hashtbl.t -> - ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t -> + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> Cic.annobj -> - Cic.annterm Content.cobj + Cic.annterm Content.cobj val map_sequent : Cic.annconjecture -> Cic.annterm Content.conjecture diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index b60abf258..70036146e 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -29,14 +29,6 @@ module Ast = CicAst let symbol_table = Hashtbl.create 1024 -let sort_of_string = function - | "Prop" -> `Prop - | "Set" -> `Set - | "Type" -> `Type - | "CProp" -> `CProp - | "?" -> `Meta - | _ -> assert false - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -67,7 +59,7 @@ let ast_of_acic ids_to_inner_sorts acic = let register_uri id uri = Hashtbl.add ids_to_uris id uri in let sort_of_id id = try - sort_of_string (Hashtbl.find ids_to_inner_sorts id) + Hashtbl.find ids_to_inner_sorts id with Not_found -> assert false in let idref id t = Ast.AttributedTerm (`IdRef id, t) in diff --git a/helm/ocaml/cic_transformations/acic2Ast.mli b/helm/ocaml/cic_transformations/acic2Ast.mli index c0f1309bf..411057cff 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.mli +++ b/helm/ocaml/cic_transformations/acic2Ast.mli @@ -24,7 +24,7 @@ *) val ast_of_acic : - (Cic.id, string) Hashtbl.t -> (* id -> sort *) + (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> (* id -> sort *) (* (Cic.id, string) Hashtbl.t -> (* id -> uri *) (string, @@ -32,5 +32,6 @@ val ast_of_acic : CicAst.term) Hashtbl.t -> *) - Cic.annterm -> CicAst.term * (Cic.id, string) Hashtbl.t + Cic.annterm -> + CicAst.term * (Cic.id, string) Hashtbl.t (* ast, id -> uri *) diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli index fc5fd547a..4642cc67d 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.mli +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -34,23 +34,23 @@ (***************************************************************************) val mml_of_cic_sequent: - Cic.metasenv -> (* metasenv *) - Cic.conjecture -> (* sequent *) - Gdome.document * (* Math ML *) - (Cic.annconjecture * (* annsequent *) - ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) - (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) - (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) - (Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *) + Cic.metasenv -> (* metasenv *) + Cic.conjecture -> (* sequent *) + Gdome.document * (* Math ML *) + (Cic.annconjecture * (* annsequent *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *) val mml_of_cic_object: - Cic.obj -> (* object *) - Gdome.document * (* Math ML *) - (Cic.annobj * (* annobj *) - ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) - (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) - (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *) - (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) - (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) - (Cic.id, Cic2acic.anntypes) Hashtbl.t))(* ids_to_inner_types *) + Cic.obj -> (* object *) + Gdome.document * (* Math ML *) + (Cic.annobj * (* annobj *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 5d614db05..3be3ba7f1 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -41,24 +41,27 @@ 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) + in let rec aux = let module C = Cic in let module X = Xml in let module U = UriManager in function C.ARel (id,idref,n,b) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_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] | C.AVar (id,uri,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in aux_subst uri (X.xml_empty "VAR" [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) exp_named_subst | C.AMeta (id,n,l) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "META" [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] (List.fold_left @@ -70,12 +73,8 @@ let print_term ~ids_to_inner_sorts = [< i ; X.xml_empty "substitution" [] >] ) [< >] l) | C.ASort (id,s) -> - let string_of_sort = - function - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type _ -> "Type" (* TASSI *) - | C.CProp -> "CProp" + let string_of_sort s = + Cic2acic.string_of_sort (Cic2acic.sort_of_sort s) in X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] | C.AImplicit _ -> raise NotImplemented @@ -88,13 +87,11 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let prods,t = eat_prods prods in - let sort = Hashtbl.find ids_to_inner_sorts last_id in + let sort = find_sort last_id in X.xml_nempty "PROD" [None,"type",sort] [< List.fold_left (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in + let sort = find_sort (Cic2acic.source_id_of_id id) in let attrs = (None,"id",id)::(None,"type",sort):: match binder with @@ -106,7 +103,7 @@ let print_term ~ids_to_inner_sorts = X.xml_nempty "target" [] (aux t) >] | C.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) @@ -120,13 +117,11 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let lambdas,t = eat_lambdas lambdas in - let sort = Hashtbl.find ids_to_inner_sorts last_id in + let sort = find_sort last_id in X.xml_nempty "LAMBDA" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> - let sort = - Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) - in + let sort = find_sort (Cic2acic.source_id_of_id id) in let attrs = (None,"id",id)::(None,"type",sort):: match binder with @@ -148,11 +143,11 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let letins,t = eat_letins letins in - let sort = Hashtbl.find ids_to_inner_sorts last_id in + let sort = find_sort last_id in X.xml_nempty "LETIN" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in let attrs = (None,"id",id)::(None,"sort",sort):: match binder with @@ -164,12 +159,12 @@ let print_term ~ids_to_inner_sorts = X.xml_nempty "target" [] (aux t) >] | C.AAppl (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] | C.AConst (id,uri,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in aux_subst uri (X.xml_empty "CONST" [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] @@ -182,7 +177,7 @@ let print_term ~ids_to_inner_sorts = None, "id", id] ) exp_named_subst | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in aux_subst uri (X.xml_empty "MUTCONSTRUCT" [None,"uri", (U.string_of_uri uri) ; @@ -191,7 +186,7 @@ let print_term ~ids_to_inner_sorts = None,"id",id ; None,"sort",sort] ) exp_named_subst | C.AMutCase (id,uri,typeno,ty,te,patterns) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "MUTCASE" [None,"uriType",(U.string_of_uri uri) ; None,"noType", (string_of_int typeno) ; @@ -203,7 +198,7 @@ let print_term ~ids_to_inner_sorts = patterns [<>] >] | C.AFix (id, no, funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "FIX" [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right @@ -219,7 +214,7 @@ let print_term ~ids_to_inner_sorts = ) funs [<>] >] | C.ACoFix (id,no,funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort id in X.xml_nempty "COFIX" [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right @@ -269,6 +264,9 @@ let print_term ~ids_to_inner_sorts = let xml_of_attrs attributes = [< >] 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 module C = Cic in let module X = Xml in let module U = UriManager in @@ -436,7 +434,8 @@ let [< print_term ids_to_inner_sorts synty >] ; match expty with None -> [<>] - | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >] + | Some expty' -> X.xml_nempty "expected" [] + [< 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 0891d4996..b714469ec 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.mli +++ b/helm/ocaml/cic_transformations/cic2Xml.mli @@ -27,18 +27,19 @@ exception ImpossiblePossible exception NotImplemented val print_term : - ids_to_inner_sorts: (string, string) 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, string) 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 val print_inner_types : UriManager.uri -> - ids_to_inner_sorts: (string, string) Hashtbl.t -> + ids_to_inner_sorts: (string, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types: (string, Cic2acic.anntypes) Hashtbl.t -> ask_dtd_to_the_getter:bool -> Xml.token Stream.t + diff --git a/helm/ocaml/cic_transformations/content2pres.mli b/helm/ocaml/cic_transformations/content2pres.mli index 369b06b3e..90258270b 100644 --- a/helm/ocaml/cic_transformations/content2pres.mli +++ b/helm/ocaml/cic_transformations/content2pres.mli @@ -32,7 +32,8 @@ (* *) (**************************************************************************) -val content2pres : - ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> - Cic.annterm Content.cobj -> Mpresentation.mpres Box.box +val content2pres: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + Cic.annterm Content.cobj -> + Mpresentation.mpres Box.box diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli index 5f4e5cf0c..7a6d8ead3 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.mli +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -33,7 +33,7 @@ (***************************************************************************) val sequent2pres : - ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.annterm Content.conjecture -> Mpresentation.mpres Box.box -- 2.39.2