X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=288be5fa2d5b06fc11a51d4cd682a1b33c1f068c;hb=9a9c5b863f68367119450ae7b806d454ba1265e3;hp=97f24c1907c6050620f3c74d5812c42a31f07065;hpb=3323758b99384afb5c7a70aa31bc006a78af64dd;p=helm.git diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 97f24c190..288be5fa2 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -99,8 +99,8 @@ let refine_obj metasenv subst context uri ~use_coercions obj ugraph process_exn Stdpp.dummy_loc exn ;; -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri + ~is_path ast ~localization_tbl ~obj_context = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -112,8 +112,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve env - (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args) | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> @@ -125,8 +125,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | `Pi | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) | `Exists -> - Disambiguate.resolve env (DisambiguateTypes.Symbol ("exists", 0)) - ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol ("exists", 0)) + (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ])) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context None outtype in @@ -152,8 +153,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast match indty_ident with | Some (indty_ident, _) -> (match - Disambiguate.resolve env - (DisambiguateTypes.Id indty_ident) () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id indty_ident) (`Args []) with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> @@ -169,8 +170,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | (Ast.Wildcard, _) :: tl -> fst_constructor tl | [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))) in - (match Disambiguate.resolve env - (DisambiguateTypes.Id (fst_constructor branches)) () with + (match Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id (fst_constructor branches)) + (`Args []) with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) | Cic.Implicit _ -> @@ -399,7 +401,12 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast with UriManager.IllFormedUri _ -> CicNotationPt.fail loc "Ill formed URI" else - Disambiguate.resolve env (DisambiguateTypes.Id name) () + try + List.assoc name obj_context + with + Not_found -> + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Id name) (`Args []) in let mk_subst uris = let ids_to_uris = @@ -462,7 +469,9 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) - | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num () + | CicNotationPt.Num (num, i) -> + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Num i) (`Num_arg num) | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -477,7 +486,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) () + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol (symbol, instance)) (`Args []) | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> Cic.Implicit annotation @@ -489,14 +499,17 @@ let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in (* here we are throwing away useful localization informations!!! *) fst ( - interpretate_term ~create_dummy_ids:true + interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true - path ~localization_tbl, localization_tbl) + path ~localization_tbl ~obj_context:[], localization_tbl) -let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = +let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj + ~localization_tbl += assert (context = []); assert (is_path = false); - let interpretate_term = interpretate_term ~localization_tbl in + let interpretate_term ?(obj_context=[]) = + interpretate_term ~mk_choice ~localization_tbl ~obj_context in match obj with | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in @@ -515,14 +528,12 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = context,List.rev res in let add_params = List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let name_to_uris = + let obj_context = snd ( List.fold_left (*here the explicit_named_substituion is assumed to be of length 0 *) - (fun (i,res) (name,_,_,_) -> - i + 1,(name,name,Cic.MutInd (uri,i,[]))::res - ) (0,[]) tyl) in - let con_env = DisambiguateTypes.env_of_list name_to_uris env in + (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res) + (0,[]) tyl) in let tyl = List.map (fun (name,b,ty,cl) -> @@ -531,7 +542,9 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = List.map (fun (name,ty) -> let ty' = - add_params (interpretate_term context con_env None false ty) + add_params + (interpretate_term ~obj_context ~context ~env ~uri:None + ~is_path:false ty) in name,ty' ) cl @@ -596,17 +609,14 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = Cic.Constant (name,bo',ty',[],attrs)) ;; -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri + ~is_path ast ~localization_tbl = - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in -interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast -~localization_tbl -;; - -let mk_implicit = - function true -> Cic.Implicit (Some `Closed) - | _ -> Cic.Implicit None + let context = + List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context + in + interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path + ast ~localization_tbl ~obj_context:[] ;; let string_context_of_context = @@ -614,9 +624,9 @@ let string_context_of_context = (Cic.Anonymous,_) -> Some "_");; let disambiguate_term ~context ~metasenv ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) + ?(initial_ugraph = CicUniv.oblivion_ugraph) + ~mk_implicit ~description_of_alias ~mk_choice + ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = let hint = match goal with | None -> (fun _ x -> x), fun k -> k @@ -634,29 +644,29 @@ let disambiguate_term ~context ~metasenv ~subst ?goal in let localization_tbl = Cic.CicHash.create 503 in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context - ~universe ~lookup_in_library + ~initial_ugraph ~aliases ~string_context_of_context + ~universe ~lookup_in_library ~mk_implicit ~description_of_alias ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ~hint ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) -let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library - (text,prefix_len,obj) +let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice + ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let hint = (fun _ x -> x), fun k -> k in let localization_tbl = Cic.CicHash.create 503 in MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~aliases ~universe ~uri ~string_context_of_context + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library + ~lookup_in_library ~mk_implicit ~description_of_alias ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:interpretate_obj + ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj ~localization_tbl ~hint