* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
(DisambiguateTypes.string_of_domain_item item))
(* TODO move it to Cic *)
-let find_in_context name (context: Cic.name list) =
+let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
| Cic.Name hd :: tl when hd = name -> acc
| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term
in
- aux ~localize:true dummy_floc context ast
+ aux ~localize:true HExtlib.dummy_floc context ast
let interpretate_path ~context path =
let localization_tbl = Cic.CicHash.create 23 in
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
*)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
domain_rev_of_term ~loc context term
| CicNotationPt.AttributedTerm (_, term) ->
where_dom @ defs_dom
| CicNotationPt.Ident (name, subst) ->
(try
- let index = find_in_context name context in
+ (* the next line can raise Not_found *)
+ ignore(find_in_context name context);
if subst <> None then
CicNotationPt.fail loc "Explicit substitutions not allowed here"
else
List.flatten
(List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
let dom =
+ List.fold_left
+ (fun dom (_,ty) ->
+ domain_rev_of_term [] ty @ dom
+ ) (dom @ domain_rev_of_term [] ty) params
+ in
List.filter
(fun name->
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_,_) -> name = Id name') fields)
) dom
- in
- List.fold_left
- (fun dom (_,ty) ->
- domain_rev_of_term [] ty @ dom
- ) (dom @ domain_rev_of_term [] ty) params
in
rev_uniq domain_rev