X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=8f8bba7d81e2ba69923ca1e92cab72109c988296;hb=5f2a4177ea8f13e2f854cf64e36e1b24e9f001bd;hp=a7e65bcfc8d26edb6c11e16f4d7df35449087955;hpb=ad586dd2ff1080ad6d71587a07772c2596b32a96;p=helm.git diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index a7e65bcfc..8f8bba7d8 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -29,42 +29,71 @@ module Ast = CicNotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () -let refine_term metasenv subst context uri term ugraph ~localization_tbl = +let rec string_context_of_context = + List.map + (function + | Cic.Name n -> Some n + | Cic.Anonymous -> Some "_") +;; + +let refine_term metasenv subst context uri ~use_coercions + term expty ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); - try - let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in - (Disambiguate.Ok (term', metasenv',[],ugraph1)) - with - exn -> - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Disambiguate.Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn + 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)) + with + exn -> + CicRefine.insert_coercions := saved_use_coercions; + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn loc exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Disambiguate.Ko (lazy (loc,Lazy.force msg)) + | exn -> raise exn + in + process_exn Stdpp.dummy_loc exn -let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = +let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph + ~localization_tbl = assert (context = []); assert (metasenv = []); assert (subst = []); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; + let saved_use_coercions = !CicRefine.insert_coercions in try + CicRefine.insert_coercions := use_coercions; let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj ~localization_tbl in - (Disambiguate.Ok (obj', metasenv,[],ugraph)) + CicRefine.insert_coercions := saved_use_coercions; + (Disambiguate.Ok (obj', metasenv,[],ugraph)) with exn -> + CicRefine.insert_coercions := saved_use_coercions; let rec process_exn loc = function HExtlib.Localized (loc,exn) -> process_exn loc exn @@ -81,8 +110,8 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = 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); @@ -94,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) -> @@ -107,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 @@ -134,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 _ -> @@ -151,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 _ -> @@ -321,9 +352,13 @@ 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 `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 -> @@ -361,13 +396,18 @@ 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.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 if is_uri ast then raise Not_found;(* don't search the env for URIs *) - let index = Disambiguate.find_in_context name context in + let index = + Disambiguate.find_in_context name (string_context_of_context context) + in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here"; Cic.Rel index @@ -379,7 +419,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 = @@ -440,9 +485,12 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast 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 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 @@ -455,10 +503,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 @@ -469,14 +523,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 @@ -486,7 +543,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = (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 @@ -495,14 +552,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) -> @@ -511,7 +566,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 @@ -528,7 +585,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = (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 @@ -562,7 +619,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = 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 @@ -576,126 +633,53 @@ 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 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 ~expty + ?(initial_ugraph = CicUniv.oblivion_ugraph) + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice + ~aliases ~universe ~lookup_in_library (text,prefix_len,term) += + 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 + ~expty + ~freshen_thing:CicNotationUtil.freshen_term + ~passes:(MultiPassDisambiguator.passes ()) - -module type CicDisambiguator = -sig - val disambiguate_term : - ?fresh_instances:bool -> - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - ?goal:int -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * - bool - - val disambiguate_obj : - ?fresh_instances:bool -> - aliases:Cic.term DisambiguateTypes.environment -> - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * - Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * - bool -end - -module Make (C: DisambiguateTypes.Callbacks) = - struct - module Disambiguator = Disambiguate.Make(C) - - let mk_implicit = - function true -> Cic.Implicit (Some `Closed) - | _ -> Cic.Implicit None - ;; - - let disambiguate_term ?(fresh_instances=false) ~context ~metasenv - ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) - = - let term = - if fresh_instances then CicNotationUtil.freshen_term term else term - in - 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 - Disambiguator.disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~mk_implicit - ~universe ~lookup_in_library - ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl - ~hint - - let disambiguate_obj - ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library - (text,prefix_len,obj) - = - let obj = - if fresh_instances then CicNotationUtil.freshen_obj obj else obj - in - let hint = - (fun _ x -> x), - fun k -> k - in - let localization_tbl = Cic.CicHash.create 503 in - Disambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~mk_implicit - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) - ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library - ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:interpretate_obj - ~refine_thing:refine_obj - ~localization_tbl - ~hint - (text,prefix_len,obj) -end +let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice + ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) += + 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 ~fix_instance + ~initial_ugraph:CicUniv.empty_ugraph + ~interpretate_thing:(interpretate_obj ~mk_choice) + ~refine_thing:refine_obj + ~mk_localization_tbl + ~expty:None + ~passes:(MultiPassDisambiguator.passes ()) + ~freshen_thing:CicNotationUtil.freshen_obj + (text,prefix_len,obj)