X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c34a5731505c0b9b38d10b11ad91ab1ca9387ce7;hb=4112b9f87a555bfc4c3cd06bae652cd2382cad8b;hp=5c2de5caa90ba4e22758637b4feb54478d22ae35;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index 5c2de5caa..c34a57315 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -18,11 +18,11 @@ open DisambiguateTypes module Ast = NotationPt module NRef = NReference -let debug_print s = prerr_endline (Lazy.force s);; +(*let debug_print s = prerr_endline (Lazy.force s);;*) let debug_print _ = ();; let cic_name_of_name = function - | Ast.Ident (n, None) -> n + | Ast.Ident (n,_) -> n | _ -> assert false ;; @@ -104,9 +104,11 @@ let find_in_context name context = aux 1 context let interpretate_term_and_interpretate_term_option (status: #NCic.status) - ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path + ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~universe ~uri ~is_path ~localization_tbl = + let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term + DisambiguateTypes.codomain_item) in (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -123,9 +125,22 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)-> aux ~localize loc context (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args))) - | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) -> + | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) + | NotationPt.Appl + (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) -> + NCic.Implicit `Term + | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args) + | NotationPt.Appl (NotationPt.AttributedTerm + (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) + (try + prerr_endline ("interpr Appl/Sym: " ^ symb); + let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in + Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*)) + interpr (`Args cic_args) + with Failure err -> + prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err); + assert false) | NotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | NotationPt.Binder (binder_kind, (var, typ), body) -> @@ -136,9 +151,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body) | `Pi | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) - | `Exists -> - Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0)) - (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])) + | `Exists -> assert false) + (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None)) + (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])*) | NotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context `Term outtype in @@ -175,23 +190,19 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) else let indtype_ref = match indty_ident with - | Some (indty_ident, _) -> - (match Disambiguate.resolve ~env ~mk_choice - (Id indty_ident) (`Args []) with - | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r - | NCic.Implicit _ -> - raise (Disambiguate.Try_again - (lazy "The type of the term to be matched is still unknown")) - | t -> - raise (DisambiguateTypes.Invalid_choice - (lazy (loc,"The type of the term to be matched "^ - "is not (co)inductive: " ^ status#ppterm - ~metasenv:[] ~subst:[] ~context:[] t)))) + | Some (_,Some r) -> r + | Some (_, None) -> + raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) | None -> - let rec fst_constructor = + let rec fst_constructor concrete_pat_found = function - (Ast.Pattern (head, _, _), _) :: _ -> head - | (Ast.Wildcard, _) :: tl -> fst_constructor tl + | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl + | (Ast.Pattern (head, Some href, _), _) :: _ -> + head, href + | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl + | [] when concrete_pat_found -> raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) | [] -> raise (Invalid_choice (lazy (loc,"The type "^ "of the term to be matched cannot be determined "^ "because it is an inductive type without constructors "^ @@ -204,19 +215,10 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (DisambiguateTypes.string_of_domain_item k ^ " => " ^ description_of_alias v)) env; *) - (match Disambiguate.resolve ~env ~mk_choice - (Id (fst_constructor branches)) (`Args []) with - | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> - let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in - NReference.mk_indty b r - | NCic.Implicit _ -> - raise (Disambiguate.Try_again - (lazy "The type of the term to be matched is still unknown")) - | t -> - raise (DisambiguateTypes.Invalid_choice - (lazy (loc, - "The type of the term to be matched is not (co)inductive: " - ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t)))) + let kname,href = fst_constructor false branches in + let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href + in + NReference.mk_indty b href in let _,leftsno,itl,_,indtyp_no = NCicEnvironment.get_checked_indtys status indtype_ref in @@ -229,7 +231,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) NCic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in - let rec sort branches cl = + let rec sort cno branches cl = match cl with [] -> let rec analyze unused unrecognized useless = @@ -264,6 +266,34 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (lazy (loc, "Missing case: " ^ name))) | ((Ast.Wildcard, _) as branch :: _) as branches -> branch, branches + | (Ast.Pattern (name',Some href,_),_) as branch :: tl -> + prerr_endline + (Printf.sprintf "analysis of %s and %s" name name'); + (match href with + | NReference.Ref (curi, (NReference.Con (n,cno',_))) -> + (* check che la curi corrisponda alla uri del tipo induttivo *) + let this_indty = NReference.mk_indty true href in + if indtype_ref <> this_indty then + (prerr_endline "fail1"; + raise (DisambiguateTypes.Invalid_choice + (lazy (loc, Printf.sprintf + "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s." + (NReference.string_of_reference indtype_ref) + (NReference.string_of_reference href) + (NReference.string_of_reference this_indty))))) + else + if cno = cno' then (prerr_endline "ok";branch, tl) + else + (prerr_endline (Printf.sprintf "skip %d %d" cno cno'); + let found,rest = find_and_remove tl in + found, branch::rest) + | _ -> + (prerr_endline "fail2"; + raise + (DisambiguateTypes.Invalid_choice + (lazy (loc,"Malformed pattern: found " ^ + (NReference.string_of_reference href) ^ + " which is not a type constructor."))))) | (Ast.Pattern (name',_,_),_) as branch :: tl when name = name' -> branch,tl @@ -275,7 +305,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) match branch with Ast.Pattern (name,y,args),term -> if List.length args = count_prod ty - leftsno then - ((name,y,args),term)::sort tl cltl + ((name,y,args),term)::sort (cno+1) tl cltl else raise (DisambiguateTypes.Invalid_choice @@ -286,13 +316,13 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) 0 -> term | n -> NotationPt.Binder - (`Lambda, (NotationPt.Ident ("_", None), None), + (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None), mk_lambdas (n - 1)) in (("wildcard",None,[]), - mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl + mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl in - let branches = sort branches cl in + let branches = sort 1 branches cl in NCic.Match (indtype_ref, cic_outtype, cic_term, (List.map do_branch branches)) | NotationPt.Cast (t1, t2) -> @@ -311,18 +341,17 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term | NotationPt.Ident _ - | NotationPt.Uri _ | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed - | NotationPt.Ident (name, subst) -> - assert (subst = None); - (try - NCic.Rel (find_in_context name context) - with Not_found -> - try NCic.Const (List.assoc name obj_context) - with Not_found -> - Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) - | NotationPt.Uri (uri, subst) -> - assert (subst = None); + | NotationPt.Ident (name, `Rel) -> + (try NCic.Rel (find_in_context name context) + with Not_found -> + (try NCic.Const (List.assoc name obj_context) + with Not_found -> assert false)) (* bug in initialize_ast *) + | NotationPt.Ident (name, `Ambiguous) -> + (try NCic.Const (List.assoc name obj_context) + with Not_found -> NCic.Implicit `Closed) + (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *) + | NotationPt.Ident (name, `Uri uri) -> (try NCic.Const (NReference.reference_of_string uri) with NRef.IllFormedReference _ -> @@ -333,8 +362,10 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | NotationPt.Implicit `JustOne -> NCic.Implicit `Term | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) | NotationPt.UserInput -> NCic.Implicit `Hole - | NotationPt.Num (num, i) -> - Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) + | NotationPt.Num (num, i) -> + let i = HExtlib.map_option + (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in + Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num) | NotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -350,8 +381,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | NotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve ~env ~mk_choice - (Symbol (symbol, instance)) (`Args []) + let instance = HExtlib.map_option + (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc)) + instance + in + Disambiguate.resolve ~env ~universe ~mk_choice + (loc (*,Symbol symbol*)) instance (`Args []) | NotationPt.Variable _ | NotationPt.Magic _ | NotationPt.Layout _ @@ -373,24 +408,24 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context) ;; -let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri +let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri ~is_path ast ~obj_context ~localization_tbl ~mk_choice = let context = List.map fst context in fst (interpretate_term_and_interpretate_term_option status - ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path + ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path ~localization_tbl) ~context ast ;; -let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri - ~is_path ~localization_tbl ~mk_choice ~obj_context +let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env + ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context = let context = List.map fst context in snd (interpretate_term_and_interpretate_term_option status - ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path + ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path ~localization_tbl) ~context ;; @@ -400,18 +435,19 @@ let disambiguate_path status path = fst (interpretate_term_and_interpretate_term_option status ~obj_context:[] ~mk_choice:(fun _ -> assert false) - ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty + ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty + ~universe:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true ~localization_tbl) ~context:[] path ;; let ncic_name_of_ident = function - | Ast.Ident (name, None) -> name + | Ast.Ident (name,_) -> name | _ -> assert false ;; let interpretate_obj status (* ?(create_dummy_ids=false) *) - ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice + ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice = assert (context = []); assert (is_path = false); @@ -424,7 +460,7 @@ let interpretate_obj status | NotationPt.Theorem (flavour, name, ty, bo, pragma) -> let ty' = interpretate_term status - ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty + ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty in let height = (* XXX calculate *) 0 in uri, height, [], [], @@ -459,13 +495,13 @@ let interpretate_obj status in let cic_body = interpretate_term status - ~obj_context ~context ~env ~uri:None ~is_path:false + ~obj_context ~context ~env ~universe ~uri:None ~is_path:false (add_binders `Lambda body) in let cic_type = interpretate_term_option status ~obj_context:[] - ~context ~env ~uri:None ~is_path:false `Type + ~context ~env ~universe ~uri:None ~is_path:false `Type (HExtlib.map_option (add_binders `Pi) typ) in ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) @@ -476,7 +512,7 @@ let interpretate_obj status | bo -> let bo = interpretate_term status - ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo + ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo in let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) @@ -491,7 +527,7 @@ let interpretate_obj status | Some t -> t in let name = cic_name_of_name name in let t = - interpretate_term status ~obj_context:[] ~context ~env ~uri:None + interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false t in (name,NCic.Decl t)::context,(name,t)::res @@ -516,14 +552,14 @@ let interpretate_obj status (fun (name,_,ty,cl) -> let ty' = add_params - (interpretate_term status ~obj_context:[] ~context ~env ~uri:None + (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false ty) in let cl' = List.map (fun (name,ty) -> let ty' = add_params - (interpretate_term status ~obj_context ~context ~env ~uri:None + (interpretate_term status ~obj_context ~context ~env ~universe ~uri:None ~is_path:false ty) in let relevance = [] in relevance,name,ty' @@ -547,7 +583,7 @@ let interpretate_obj status | Some t -> t in let name = cic_name_of_name name in let t = - interpretate_term status ~obj_context:[] ~context ~env ~uri:None + interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false t in (name,NCic.Decl t)::context,(name,t)::res @@ -559,7 +595,7 @@ let interpretate_obj status let leftno = List.length params in let ty' = add_params - (interpretate_term status ~obj_context:[] ~context ~env ~uri:None + (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None ~is_path:false ty) in let nref = NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in @@ -569,7 +605,7 @@ let interpretate_obj status List.fold_left (fun (context,res) (name,ty,_coercion,_arity) -> let ty = - interpretate_term status ~obj_context ~context ~env ~uri:None + interpretate_term status ~obj_context ~context ~env ~universe ~uri:None ~is_path:false ty in let context' = (name,NCic.Decl ty)::context in context',(name,ty)::res @@ -592,25 +628,199 @@ let interpretate_obj status NCic.Inductive (true,leftno,tyl,attrs) ;; +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') +;; + let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = + let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in + let local_names = List.map (fun (n,_) -> n) context in let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let res,b = - MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:NotationUtil.freshen_term - ~context ~metasenv ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias ~fix_instance + Disambiguate.disambiguate_thing + ~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context:(List.map (fun (x,_) -> Some x)) - ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) - ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term + ~initial_ugraph:() ~expty + ~mk_implicit ~description_of_alias ~fix_instance ~aliases + ~universe ~lookup_in_library + ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status) + ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) - ~refine_thing:(refine_term status) (text,prefix_len,term) - ~mk_localization_tbl ~expty ~subst - in - List.map (function (a,b,c,d,_) -> a,b,c,d) res, b + ~refine_thing:(refine_term status) + (text,prefix_len, + (initialize_ast ~universe ~lookup_in_library ~local_names term)) + ~visit:Disambiguate.bfvisit + ~mk_localization_tbl ;; let disambiguate_obj (status: #NCicCoercion.status) @@ -618,23 +828,21 @@ let disambiguate_obj (status: #NCicCoercion.status) ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in - let res,b = - MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:NotationUtil.freshen_obj - ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias ~fix_instance + let obj' = initialize_obj ~universe ~lookup_in_library obj in + Disambiguate.disambiguate_thing + ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true ~string_context_of_context:(List.map (fun (x,_) -> Some x)) - ~universe - ~uri:(Some uri) - ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) - ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj + ~initial_ugraph:() ~expty:None + ~mk_implicit ~description_of_alias ~fix_instance ~aliases + ~universe ~lookup_in_library + ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) + ~pp_term:(NotationPp.pp_term status) + ~domain_of_thing:Disambiguate.domain_of_obj ~interpretate_thing:(interpretate_obj status ~mk_choice) ~refine_thing:(refine_obj status) - (text,prefix_len,obj) - ~mk_localization_tbl ~expty:None - in - List.map (function (a,b,c,d,_) -> a,b,c,d) res, b + (text,prefix_len,obj') + ~visit:Disambiguate.bfvisit_obj + ~mk_localization_tbl ;; (* let _ =