resolve env (Symbol (symb, i)) ~args:cic_args ()
| CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
| CicAst.Binder (binder_kind, (var, typ), body) ->
- let cic_type = aux_option loc context typ in
+ let cic_type = aux_option loc context (Some `Type) typ in
let cic_body = aux loc (var :: context) body in
(match binder_kind with
| `Lambda -> Cic.Lambda (var, cic_type, cic_body)
~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
| CicAst.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux loc context term in
- let cic_outtype = aux_option loc context outtype in
+ let cic_outtype = aux_option loc context None outtype in
let do_branch ((head, args), term) =
let rec do_branch' context = function
| [] -> aux loc context term
List.map
(fun ((name, typ), body, decr_idx) ->
let cic_body = aux loc context' body in
- let cic_type = aux_option loc context typ in
+ let cic_type = aux_option loc context (Some `Type) typ in
let name =
match name with
| Cic.Anonymous ->
let cic =
if is_uri ast then (* we have the URI, build the term out of it *)
try
- CicUtil.term_of_uri name
+ CicUtil.term_of_uri (UriManager.uri_of_string name)
with UriManager.IllFormedUri _ ->
CicTextualParser2.fail loc "Ill formed URI"
else
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
- and aux_option loc context = function
- | None -> Cic.Implicit (Some `Type)
+ and aux_option loc context annotation = function
+ | None -> Cic.Implicit annotation
| Some term -> aux loc context term
in
match ast with
(UriManager.string_of_uri uri,
let term =
try
- CicUtil.term_of_uri (UriManager.string_of_uri uri)
+ CicUtil.term_of_uri uri
with exn ->
debug_print (UriManager.string_of_uri uri);
debug_print (Printexc.to_string exn);