X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=8f8bba7d81e2ba69923ca1e92cab72109c988296;hb=1c8e230b1d81491b38126900d76201fb84303ced;hp=2b469ce9d7d4b24585421f5007ff1cc80602c1f4;hpb=93ce01455cfeba6b29e3c8a57e28f56559fb891d;p=helm.git diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 2b469ce9d..8f8bba7d8 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 = []); @@ -341,9 +352,13 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri in let cic_body = aux ~localize loc context' (add_binders `Lambda body) in + let typ = + match typ with + Some typ -> typ + | None-> CicNotationPt.Implicit `JustOne 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 -> @@ -381,8 +396,11 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri 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.NCic _ -> assert false + | CicNotationPt.NRef _ -> assert false + | CicNotationPt.Ident (name,subst) | CicNotationPt.Uri (name, subst) as ast -> let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try @@ -467,7 +485,8 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri with CicEnvironment.CircularDependency _ -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) - | CicNotationPt.Implicit -> Cic.Implicit None + | CicNotationPt.Implicit `Vector -> assert false + | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~mk_choice ~env @@ -484,11 +503,16 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri | 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 ~mk_choice ~env (DisambiguateTypes.Symbol (symbol, instance)) (`Args []) - | _ -> assert false (* god bless Bologna *) + | 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 @@ -519,7 +543,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit + None -> CicNotationPt.Implicit `JustOne | Some t -> t in let name = CicNotationUtil.cic_name_of_name name in name::context,(name, interpretate_term context env None false t)::res @@ -561,7 +585,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit + None -> CicNotationPt.Implicit `JustOne | Some t -> t in let name = CicNotationUtil.cic_name_of_name name in name::context,(name, interpretate_term context env None false t)::res @@ -595,7 +619,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) - | CicNotationPt.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in (match bo,flavour with @@ -623,53 +647,39 @@ 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 +let disambiguate_term ~context ~metasenv ~subst ~expty ?(initial_ugraph = CicUniv.oblivion_ugraph) - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~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 mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst ~initial_ugraph ~aliases ~string_context_of_context ~universe ~lookup_in_library ~mk_implicit ~description_of_alias + ~fix_instance ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) ~refine_thing:refine_term (text,prefix_len,term) ~mk_localization_tbl - ~hint + ~expty ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) -let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice +let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = - let hint = (fun _ x -> x), fun k -> k in let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] ~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 ~mk_implicit ~description_of_alias + ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance ~initial_ugraph:CicUniv.empty_ugraph ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj ~mk_localization_tbl - ~hint + ~expty:None ~passes:(MultiPassDisambiguator.passes ()) ~freshen_thing:CicNotationUtil.freshen_obj (text,prefix_len,obj)