X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=cf59ab553c33efc202208ea7d0cea86f7734aa74;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;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..cf59ab553 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -37,15 +37,26 @@ let rec string_context_of_context = ;; let refine_term metasenv subst context uri ~use_coercions - term ugraph ~localization_tbl = + term expty ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); let saved_use_coercions = !CicRefine.insert_coercions in try CicRefine.insert_coercions := use_coercions; + let term = + match expty with + | None -> term + | Some ty -> Cic.Cast(term,ty) + in let term', _, metasenv',ugraph1 = CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl + in + let term' = + match expty, term' with + | None,_ -> term' + | Some _,Cic.Cast (term',_) -> term' + | _ -> assert false in CicRefine.insert_coercions := saved_use_coercions; (Disambiguate.Ok (term', metasenv',[],ugraph1)) @@ -66,7 +77,7 @@ let refine_term metasenv subst context uri ~use_coercions in process_exn Stdpp.dummy_loc exn -let refine_obj metasenv subst context uri ~use_coercions obj ugraph +let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph ~localization_tbl = assert (context = []); assert (metasenv = []); @@ -99,8 +110,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 +123,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 +136,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 +164,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 +181,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 _ -> @@ -339,9 +352,11 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast in let cic_body = aux ~localize loc context' (add_binders `Lambda body) in + let typ = + match typ with Some typ -> typ | None-> CicNotationPt.Implicit in let cic_type = aux_option ~localize loc context (Some `Type) - (HExtlib.map_option (add_binders `Pi) typ) in + (Some (add_binders `Pi typ)) in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> @@ -379,8 +394,10 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast List.fold_right (build_term inductiveFuns) inductiveFuns cic_body) | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed - | CicNotationPt.Ident (name, subst) + | CicNotationPt.Uri _ + | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed + | CicNotationPt.NRef _ -> assert false + | CicNotationPt.Ident (name,subst) | CicNotationPt.Uri (name, subst) as ast -> let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try @@ -399,7 +416,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 +484,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 @@ -475,10 +499,16 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) + | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) + | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ())) | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) () - | _ -> assert false (* god bless Bologna *) + Disambiguate.resolve ~mk_choice ~env + (DisambiguateTypes.Symbol (symbol, instance)) (`Args []) + | CicNotationPt.Variable _ + | CicNotationPt.Magic _ + | CicNotationPt.Layout _ + | CicNotationPt.Literal _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> Cic.Implicit annotation | Some term -> aux ~localize loc context term @@ -489,14 +519,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 +548,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 +562,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,70 +629,52 @@ 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 = List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some (Cic.Anonymous,_) -> Some "_");; -let disambiguate_term ~context ~metasenv ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) +let disambiguate_term ~context ~metasenv ~subst ~expty + ?(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 - | Some i -> - (fun metasenv t -> - let _,c,ty = CicUtil.lookup_meta i metasenv in - assert(c=context); - Cic.Cast(t,ty)), - function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug) - | _ -> assert false) - | k -> k - in - let localization_tbl = Cic.CicHash.create 503 in + let mk_localization_tbl x = Cic.CicHash.create x 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 + ~mk_localization_tbl + ~expty ~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 + let mk_localization_tbl x = Cic.CicHash.create x 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 + ~mk_localization_tbl + ~expty:None ~passes:(MultiPassDisambiguator.passes ()) ~freshen_thing:CicNotationUtil.freshen_obj (text,prefix_len,obj)