- (fun (context,res) (name,ty,_coercion) ->
+ (fun (context,res) (name,ty,_coercion,arity) ->
let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
concl fields' in
let con' = add_params con in
let tyl = [name,true,ty',["mk_" ^ name,con']] in
concl fields' in
let con' = add_params con in
let tyl = [name,true,ty',["mk_" ^ name,con']] in
- let field_names = List.map (fun (x,_,y) -> x,y) fields in
+ let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
let bo' = Some (interpretate_term [] env None false bo) in
Cic.Constant (name,bo',ty',[],attrs))
let bo' = Some (interpretate_term [] env None false bo) in
Cic.Constant (name,bo',ty',[],attrs))
- (fun (members, rev_l) elt ->
- if Set.mem elt members then
- (members, rev_l)
- else
- Set.add elt members, elt :: rev_l)
- (Set.empty, []) rev_l
+ (fun (members, rev_l) (loc,elt) ->
+ try
+ let locs = Map.find elt members in
+ if List.mem loc locs then
+ members, rev_l
+ else
+ Map.add elt (loc::locs) members, rev_l
+ with
+ | Not_found -> Map.add elt [loc] members, elt :: rev_l)
+ (Map.empty, []) rev_l
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
| CicNotationPt.Binder (kind, (var, typ), body) ->
let kind_dom =
match kind with
| CicNotationPt.Binder (kind, (var, typ), body) ->
let kind_dom =
match kind with
let outtype_dom = domain_rev_of_term_option loc context outtype in
let get_first_constructor = function
| [] -> []
let outtype_dom = domain_rev_of_term_option loc context outtype in
let get_first_constructor = function
| [] -> []
- | ((head, _, _), _) :: _ -> [ Id head ]
+ | ((head, _, _), _) :: _ -> [ loc, Id head ]
in
let do_branch ((head, _, args), term) =
let (term_context, args_domain) =
in
let do_branch ((head, _, args), term) =
let (term_context, args_domain) =
| CicNotationPt.Cast (term, ty) ->
let term_dom = domain_rev_of_term ~loc context term in
let ty_dom = domain_rev_of_term ~loc context ty in
| CicNotationPt.Cast (term, ty) ->
let term_dom = domain_rev_of_term ~loc context term in
let ty_dom = domain_rev_of_term ~loc context ty in
| CicNotationPt.Meta (index, local_context) ->
List.fold_left
(fun dom term -> domain_rev_of_term_option loc context term @ dom) []
local_context
| CicNotationPt.Sort _ -> []
| CicNotationPt.Meta (index, local_context) ->
List.fold_left
(fun dom term -> domain_rev_of_term_option loc context term @ dom) []
local_context
| CicNotationPt.Sort _ -> []
- | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+ | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ]
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_,_) -> name = Id name') tyl)
) dom
| CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_,_) -> name = Id name') tyl)
) dom
| CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
- (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
+ (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
- || List.exists (fun (name',_,_) -> name = Id name') fields)
+ || List.exists (fun (name',_,_,_) -> name = Id name') fields)
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
?initial_ugraph:CicUniv.universe_graph ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.term*
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.term*
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *
let disambiguate_thing ~dbd ~context ~metasenv
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
let disambiguate_thing ~dbd ~context ~metasenv
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
=
debug_print (lazy "DISAMBIGUATE INPUT");
let disambiguate_context = (* cic context -> disambiguate context *)
=
debug_print (lazy "DISAMBIGUATE INPUT");
let disambiguate_context = (* cic context -> disambiguate context *)
debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
let thing_dom = domain_of_thing ~context:disambiguate_context thing in
debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
let thing_dom = domain_of_thing ~context:disambiguate_context thing in
debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
(*
debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
(DisambiguatePp.pp_environment aliases)));
(*
debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
(DisambiguatePp.pp_environment aliases)));
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
| Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
| Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
- [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
+ [], [Some (List.hd locs),
+ lazy ("No choices for " ^ string_of_domain_item item)]
| [codomain_item] ->
(* just one choice. We perform a one-step look-up and
if the next set of choices is also a singleton we
| [codomain_item] ->
(* just one choice. We perform a one-step look-up and
if the next set of choices is also a singleton we
let choices = lookup_choices he in
Some choices,List.length choices = 1
in
let choices = lookup_choices he in
Some choices,List.length choices = 1
in
debug_print (lazy "SINGLE INTERPRETATION");
[diff,metasenv,t,ugraph], false
| l,_ ->
debug_print (lazy "SINGLE INTERPRETATION");
[diff,metasenv,t,ugraph], false
| l,_ ->
let choices =
List.map
(fun (env, _, _, _, _) ->
List.map
let choices =
List.map
(fun (env, _, _, _, _) ->
List.map
(List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
true
in
(List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
true
in
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj