Symbol of string option * string * subst option * string option
(* h:xref, name, subst, definitionURL *)
| LocalVar of (string option) * string (* h:xref, name *)
Symbol of string option * string * subst option * string option
(* h:xref, name, subst, definitionURL *)
| LocalVar of (string option) * string (* h:xref, name *)
| Num of string option * string (* h:xref, value *)
| Appl of string option * cexpr list (* h:xref, args *)
| Binder of string option * string * decl * cexpr
| Num of string option * string (* h:xref, value *)
| Appl of string option * cexpr list (* h:xref, args *)
| Binder of string option * string * decl * cexpr
def = string * cexpr (* name, body *)
and
subst = (UriManager.uri * cexpr) list
def = string * cexpr (* name, body *)
and
subst = (UriManager.uri * cexpr) list
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "and",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "and",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "or",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "or",
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
(Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
| _ -> raise Not_found);;
(Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
| _ -> raise Not_found);;
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
| C.AVar (id,uri,subst) ->
Symbol (Some id, UriManager.name_of_uri uri,
make_subst subst, Some (UriManager.string_of_uri uri))
| 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) ->
| C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
| C.AImplicit _ -> raise NotImplemented
| C.AProd (id,n,s,t) ->
) in
let (name,_,_,_) = List.nth inductive_types i in
let uri_str = UriManager.string_of_uri uri in
) in
let (name,_,_,_) = List.nth inductive_types i in
let uri_str = UriManager.string_of_uri uri 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,
(try
(let f = Hashtbl.find symbol_table puri_str in
f aid sid tl acic2cexpr)
with notfound ->
Appl (Some aid, Symbol (Some sid, name,
| C.AAppl (id,li) ->
Appl (Some id, List.map acic2cexpr li)
| C.AConst (id,uri,subst) ->
| C.AAppl (id,li) ->
Appl (Some id, List.map acic2cexpr li)
| C.AConst (id,uri,subst) ->
) in
let (name,_,_,_) = List.nth inductive_types i in
let uri_str = UriManager.string_of_uri uri in
) 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
| 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 =
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let constructors = get_constructors uri typeno in
let named_patterns =