-
- (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
-let rev_uniq =
- let module SortedItem =
- struct
- type t = DisambiguateTypes.domain_item
- let compare = Pervasives.compare
- end
- in
- let module Map = Map.Make (SortedItem) in
- fun l ->
- let rev_l = List.rev l in
- let (members, uniq_rev_l) =
- List.fold_left
- (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
- in
- List.rev_map
- (fun e -> try Map.find e members,e with Not_found -> assert false)
- uniq_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.
- *)
-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) ->
- domain_rev_of_term ~loc context term
- | CicNotationPt.Appl terms ->
- List.fold_left
- (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
- | CicNotationPt.Binder (kind, (var, typ), body) ->
- let kind_dom =
- match kind with
- | `Exists -> [ loc, Symbol ("exists", 0) ]
- | _ -> []
+let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
+ | Ast.AttributedTerm (`Loc loc, term) ->
+ domain_of_term ~loc ~context term
+ | Ast.AttributedTerm (_, term) ->
+ domain_of_term ~loc ~context term
+ | Ast.Symbol (symbol, instance) ->
+ [ Node ([loc], Symbol (symbol, instance), []) ]
+ (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
+ | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+ ->
+ let args_dom =
+ List.fold_right
+ (fun term acc -> domain_of_term ~loc ~context term @ acc)
+ args [] in
+ let loc =
+ match hd with
+ Ast.AttributedTerm (`Loc loc,_) -> loc
+ | _ -> loc