+let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
+ (* ast_of_alias_spec is duplicate in Disambiguate *)
+ let ast_of_alias_spec t alias = match (t,alias) with
+ | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try
+ let res = Environment.find item universe in
+ let id = match item with
+ | DisambiguateTypes.Id id -> id
+ | DisambiguateTypes.Symbol _ -> "SYM"
+ | DisambiguateTypes.Num _ -> "NUM"
+ in
+ debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
+ (List.length res)));
+ res
+ with Not_found -> [])
+ in
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ (*
+ List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])
+ *)
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ in
+ let init_pattern ~local_names = function
+ | Ast.Wildcard as t -> local_names,t
+ | Ast.Pattern (c,uri,vars) ->
+ let ln',vars' = init_vars ~local_names vars in
+ let uri' = match uri with
+ | Some _ -> uri
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id c) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ in
+ ln',Ast.Pattern (c,uri',vars')
+ in
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id id
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
+ | Ast.Num _ -> DisambiguateTypes.Num
+ | _ -> assert false
+ in
+ match t with
+ | Ast.Ident (id,(`Ambiguous|`Rel))
+ when List.mem id local_names -> Ast.Ident (id,`Rel)
+ | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else ast_of_alias_spec t (List.hd choices)
+ | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
+ | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
+ | Ast.Binder (k,(n,ty),body) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let body' = init ~local_names:(n'::local_names) body in
+ Ast.Binder (k,(n,ty'),body')
+ | Ast.Case (t,ity,oty,pl) ->
+ let t' = init ~local_names t in
+ let oty' = HExtlib.map_option (init ~local_names) oty in
+ let pl' =
+ List.map (fun (p,u) ->
+ let ns,p' = init_pattern ~local_names p in
+ p',init ~local_names:ns u) pl in
+ let ity' = HExtlib.map_option
+ (fun (ity_id,href) ->
+ let href' = match href with
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id ity_id) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ | Some _ -> href
+ in (ity_id,href')) ity
+ in Ast.Case (t',ity',oty',pl')
+ | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
+ | Ast.LetIn ((n,ty),u,v) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let u' = init ~local_names u in
+ let v' = init ~local_names:(n'::local_names) v in
+ Ast.LetIn ((n,ty'),u',v')
+ | Ast.LetRec (ik,l,t) ->
+ let recfuns =
+ List.fold_right (fun (_,(n,_),_,_) acc ->
+ cic_name_of_name n::acc) l [] in
+ let l' = List.map (fun (vl,(n,ty),u,m) ->
+ let ln',vl' = init_vars ~local_names vl in
+ let ty' = HExtlib.map_option (init ~local_names:ln') ty in
+ let ln'' = recfuns@ln' in
+ let u' = init ~local_names:ln'' u in
+ vl',(n,ty'),u',m) l in
+ let t' = init ~local_names:(recfuns@local_names) t in
+ Ast.LetRec (ik,l',t') (* XXX: t??? *)
+ | t -> t
+;;
+
+let initialize_obj ~universe ~lookup_in_library o =
+ let init = initialize_ast ~universe ~lookup_in_library in
+ let init_var ~local_names (n,ty) =
+ (n,HExtlib.map_option (init ~local_names) ty)
+ in
+ let init_vars ~local_names vars =
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])*)
+ in
+
+ match o with
+ | Ast.Inductive (ls,itl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let indtys =
+ List.fold_right
+ (fun (name,_,_,_) acc -> name::acc) itl [] in
+ let itl' = List.map
+ (fun (name,isind,ty,cl) ->
+ let ty' = init ~local_names:ln ty in
+ let cl' =
+ List.map (fun (cname,cty) ->
+ cname, init ~local_names:(indtys@ln) cty) cl
+ in
+ name,isind,ty',cl') itl
+ in
+ Ast.Inductive (ls',itl')
+ | Ast.Theorem (flav,n,ty,bo,p) ->
+ let ty' = init ~local_names:[] ty in
+ let bo' = HExtlib.map_option (init ~local_names:[]) bo in
+ Ast.Theorem (flav,n,ty',bo',p)
+ | Ast.Record (ls,n,ty,fl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let ty' = init ~local_names:ln ty in
+ let _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) ->
+ (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl
+ in
+ let fl' = List.rev fl' in
+ Ast.Record (ls',n,ty',fl')
+;;
+