X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=487bceb871377cfb1964e94ad81cccf878e8d733;hb=5780119aea0a20e74f7c153add432f5d491ee2a5;hp=4bfeab669066ad762d7a260515c8a5426ab16a69;hpb=8f785ed7fd5b2674d9fadbe5fac2eb7b2ec1cc4b;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4bfeab669..487bceb87 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -22,6 +22,9 @@ module NRef = NReference let debug_print s = prerr_endline (Lazy.force s);; let debug_print _ = ();; +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; + let cic_name_of_name = function | Ast.Ident (n, None) -> n | _ -> assert false @@ -64,7 +67,7 @@ let refine_term ;; let refine_obj - ~rdb metasenv subst context _uri + ~rdb metasenv subst _context _uri ~use_coercions obj _ _ugraph ~localization_tbl = assert (metasenv=[]); @@ -72,7 +75,6 @@ let refine_obj let localise t = try NCicUntrusted.NCicHash.find localization_tbl t with Not_found -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); (*assert false*)HExtlib.dummy_floc in try @@ -322,16 +324,21 @@ let interpretate_term_and_interpretate_term_option with Not_found -> try NCic.Const (List.assoc name obj_context) with Not_found -> - Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) + Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) | CicNotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri)) + NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri)) with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") | CicNotationPt.NRef nref -> NCic.Const nref + | CicNotationPt.NCic t -> + let context = (* to make metas_of_term happy *) + List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in + assert(NCicUntrusted.metas_of_term [] context t = []); t | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term + | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) @@ -344,15 +351,15 @@ let interpretate_term_and_interpretate_term_option NCic.Meta (index, (0, NCic.Ctx cic_subst)) | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) + [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"]) + [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"]) | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) + [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")]) + [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type - [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"]) + [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) | CicNotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) @@ -412,7 +419,7 @@ let new_flavour_of_flavour = function | `MutualDefinition -> `Definition | `Fact -> `Fact | `Lemma -> `Lemma - | `Remark -> `Corollary + | `Remark -> `Example | `Theorem -> `Theorem | `Variant -> `Corollary | `Axiom -> `Fact @@ -435,7 +442,7 @@ let interpretate_obj interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in let uri = match uri with | None -> assert false | Some u -> u in match obj with - | CicNotationPt.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) -> let ty' = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty @@ -444,11 +451,11 @@ let interpretate_obj uri, height, [], [], (match bo,flavour with | None,`Axiom -> - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,None,ty',attrs) | Some _,`Axiom -> assert false | None,_ -> - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> (match bo with @@ -485,14 +492,14 @@ let interpretate_obj ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in - let attrs = `Provided, new_flavour_of_flavour flavour in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) | CicNotationPt.Inductive (params,tyl) -> let context,params = @@ -607,7 +614,7 @@ let interpretate_obj ;; let disambiguate_term ~context ~metasenv ~subst ~expty - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~rdb ~lookup_in_library (text,prefix_len,term) = @@ -616,7 +623,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_term ~context ~metasenv ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias + ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~passes:(MultiPassDisambiguator.passes ()) @@ -629,7 +636,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty ;; let disambiguate_obj - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~rdb ~lookup_in_library ~uri (text,prefix_len,obj) = @@ -638,7 +645,7 @@ let disambiguate_obj MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_obj ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias + ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:(Some uri)