X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c9e453cf20d6c0b69fd6870b635d27eb29c93c84;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=357f9e53977aa10be34f8df4b805304d5cd92041;hpb=0369aa83a42ed4730ed1946b02365760817f6ea2;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 357f9e539..c9e453cf2 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -19,8 +19,11 @@ open UriManager module Ast = CicNotationPt module NRef = NReference +let debug_print s = prerr_endline (Lazy.force s);; let debug_print _ = ();; -(* let debug_print s = prerr_endline (Lazy.force s);; *) + +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 @@ -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 @@ -119,6 +121,12 @@ let interpretate_term_and_interpretate_term_option NCicUntrusted.NCicHash.add localization_tbl res loc; res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term + | CicNotationPt.Appl (CicNotationPt.Appl inner :: args) -> + aux ~localize loc context (CicNotationPt.Appl (inner @ args)) + | CicNotationPt.Appl + (CicNotationPt.AttributedTerm (att,(CicNotationPt.Appl inner))::args)-> + aux ~localize loc context + (CicNotationPt.AttributedTerm (att,CicNotationPt.Appl (inner @ args))) | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) @@ -316,16 +324,18 @@ 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 -> 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) @@ -338,15 +348,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 []) @@ -406,7 +416,7 @@ let new_flavour_of_flavour = function | `MutualDefinition -> `Definition | `Fact -> `Fact | `Lemma -> `Lemma - | `Remark -> `Corollary + | `Remark -> `Example | `Theorem -> `Theorem | `Variant -> `Corollary | `Axiom -> `Fact @@ -429,7 +439,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 @@ -438,11 +448,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 @@ -479,14 +489,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 = @@ -509,13 +519,11 @@ let interpretate_obj let add_params = List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in let leftno = List.length params in + let _,inductive,_,_ = try List.hd tyl with Failure _ -> assert false in let obj_context = snd ( List.fold_left (fun (i,res) (name,_,_,_) -> - let _,inductive,_,_ = - (* ??? *) - try List.hd tyl with Failure _ -> assert false in let nref = NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno)) in @@ -545,7 +553,7 @@ let interpretate_obj let height = (* XXX calculate *) 0 in let attrs = `Provided, `Regular in uri, height, [], [], - NCic.Inductive (true,leftno,tyl,attrs) + NCic.Inductive (inductive,leftno,tyl,attrs) | CicNotationPt.Record (params,name,ty,fields) -> let context,params = let context,res = @@ -603,7 +611,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) = @@ -612,7 +620,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 ()) @@ -625,7 +633,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) = @@ -634,7 +642,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)