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
* 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
;;
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)));
(*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 =
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
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
| _ -> "__" ^ 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
| 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
| 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
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
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
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
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)
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
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
{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 *)
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 *)
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 *)
+
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
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;
(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;
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;
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
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
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
| 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
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
})
| 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) ->
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
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
*)
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
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
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
*)
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,
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 *)
(***************************************************************************)
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 *)
(*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
[< 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
| 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
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)
| 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
| 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
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]
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) ;
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) ;
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
) 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
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
[< 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 [<>]
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
+
(* *)
(**************************************************************************)
-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
(***************************************************************************)
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
projects / helm.git / commitdiff