* 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
i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
let con_env = DisambiguateTypes.env_of_list name_to_uris env in
- let undebrujin t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tyl (List.length tyl - 1,t)) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
let ty' =
add_params (interpretate_term context con_env None false ty)
in
- name,undebrujin ty'
+ name,ty'
) cl
in
name,b,ty',cl'
let fields' =
snd (
List.fold_left
- (fun (context,res) (name,ty) ->
+ (fun (context,res) (name,ty,_coercion) ->
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
- let field_names = List.map fst fields in
+ let field_names = List.map (fun (x,_,y) -> x,y) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
(* "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
| 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
let dom =
- 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
+ List.filter
+ (fun name->
+ not ( List.exists (fun (name',_) -> name = Id name') params
+ || List.exists (fun (name',_,_) -> name = Id name') fields)
+ ) dom
in
rev_uniq domain_rev