X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c9e453cf20d6c0b69fd6870b635d27eb29c93c84;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=f0a3fa0eb7386ba9747243c4050d718ed2ffeea7;hpb=f3a40daf813df6d33289d4df64da6c16ea9d3ca4;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index f0a3fa0eb..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 @@ -34,7 +37,7 @@ let rec mk_rels howmany from = ;; let refine_term - metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl= + metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl= assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); @@ -46,12 +49,9 @@ let refine_term (*assert false*) HExtlib.dummy_floc in let metasenv, subst, term, _ = - NCicRefiner.typeof - (NCicUnifHint.db ()) - ~look_for_coercion:( - if use_coercions then - NCicCoercion.look_for_coercion coercion_db - else (fun _ _ _ _ _ -> [])) + NCicRefiner.typeof + (rdb#set_coerc_db + (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db)) metasenv subst context term expty ~localise in Disambiguate.Ok (term, metasenv, subst, ()) @@ -67,7 +67,7 @@ let refine_term ;; let refine_obj - ~coercion_db metasenv subst context _uri + ~rdb metasenv subst _context _uri ~use_coercions obj _ _ugraph ~localization_tbl = assert (metasenv=[]); @@ -75,17 +75,14 @@ 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 let obj = NCicRefiner.typeof_obj - (NCicUnifHint.db ()) - ~look_for_coercion:( - if use_coercions then - NCicCoercion.look_for_coercion coercion_db - else (fun _ _ _ _ _ -> [])) + (rdb#set_coerc_db + (if use_coercions then rdb#coerc_db + else NCicCoercion.empty_db)) obj ~localise in Disambiguate.Ok (obj, [], [], ()) @@ -124,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) @@ -312,22 +315,27 @@ let interpretate_term_and_interpretate_term_option NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed + | CicNotationPt.Uri _ + | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed | CicNotationPt.Ident (name, subst) -> assert (subst = None); (try - NCic.Rel (find_in_context name context) + NCic.Rel (find_in_context name context) with Not_found -> try NCic.Const (List.assoc name obj_context) with Not_found -> - Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) - | CicNotationPt.Uri (name, subst) -> + Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) + | CicNotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (NRef.reference_of_string name) + NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri)) with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") - | CicNotationPt.Implicit -> NCic.Implicit `Term + | 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) @@ -340,13 +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/Type.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 + [`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/CProp.univ"]) + [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) | CicNotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) @@ -363,7 +373,8 @@ let interpretate_term_and_interpretate_term_option res | Some (CicNotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) - | Some CicNotationPt.Implicit -> NCic.Implicit annotation + | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation + | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector | Some term -> aux ~localize loc context term in (fun ~context -> aux ~localize:true HExtlib.dummy_floc context), @@ -405,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 @@ -428,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 @@ -437,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 @@ -478,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 = @@ -494,7 +505,7 @@ let interpretate_obj (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit + None -> CicNotationPt.Implicit `JustOne | Some t -> t in let name = cic_name_of_name name in let t = @@ -508,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 @@ -544,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 = @@ -552,7 +561,7 @@ let interpretate_obj (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit + None -> CicNotationPt.Implicit `JustOne | Some t -> t in let name = cic_name_of_name name in let t = @@ -602,8 +611,8 @@ let interpretate_obj ;; let disambiguate_term ~context ~metasenv ~subst ~expty - ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~coercion_db ~lookup_in_library + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice + ~aliases ~universe ~rdb ~lookup_in_library (text,prefix_len,term) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in @@ -611,21 +620,21 @@ 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 ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) - ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term) + ~refine_thing:(refine_term ~rdb) (text,prefix_len,term) ~mk_localization_tbl ~expty ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; let disambiguate_obj - ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~coercion_db ~lookup_in_library ~uri + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice + ~aliases ~universe ~rdb ~lookup_in_library ~uri (text,prefix_len,obj) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in @@ -633,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) @@ -641,12 +650,13 @@ let disambiguate_obj ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj ~interpretate_thing:(interpretate_obj ~mk_choice) - ~refine_thing:(refine_obj ~coercion_db) + ~refine_thing:(refine_obj ~rdb) (text,prefix_len,obj) ~mk_localization_tbl ~expty:None in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; +(* let _ = let mk_type n = if n = 0 then @@ -685,4 +695,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*)