X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=7ebca20d763f41043577fd1ed953f38fd987c10e;hb=bca340f9c590e6530f8346fddd61c9fa0ae7f411;hp=4e3f8cac3e265aa362253b2dd47e440bfa97705e;hpb=46b91f34b693dabbd351ba813f5190051b09a117;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4e3f8cac3..7ebca20d7 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -19,16 +19,25 @@ 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 | _ -> assert false ;; +let rec mk_rels howmany from = + match howmany with + | 0 -> [] + | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from) +;; + let refine_term - metasenv subst context uri ~coercion_db ~use_coercions term _ ~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))); @@ -36,17 +45,14 @@ let refine_term let localise t = try NCicUntrusted.NCicHash.find localization_tbl t with Not_found -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - assert false + prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t); + (*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 _ _ _ _ _ -> [])) - metasenv subst context term None ~localise + 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, ()) with @@ -60,6 +66,38 @@ let refine_term Disambiguate.Ko loc_msg ;; +let refine_obj + ~rdb metasenv subst _context _uri + ~use_coercions obj _ _ugraph ~localization_tbl += + assert (metasenv=[]); + assert (subst=[]); + let localise t = + try NCicUntrusted.NCicHash.find localization_tbl t + with Not_found -> + (*assert false*)HExtlib.dummy_floc + in + try + let obj = + NCicRefiner.typeof_obj + (rdb#set_coerc_db + (if use_coercions then rdb#coerc_db + else NCicCoercion.empty_db)) + obj ~localise + in + Disambiguate.Ok (obj, [], [], ()) + with + | NCicRefiner.Uncertain loc_msg -> + debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ + NCicPp.ppobj obj)) ; + Disambiguate.Uncertain loc_msg + | NCicRefiner.RefineFailure loc_msg -> + debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s" + (NCicPp.ppobj obj) (snd(Lazy.force loc_msg)))); + Disambiguate.Ko loc_msg +;; + + (* TODO move it to Cic *) let find_in_context name context = let rec aux acc = function @@ -83,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) @@ -269,26 +313,33 @@ let interpretate_term_and_interpretate_term_option in let cic_body = aux ~localize loc (cic_name :: context) body in NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) - | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false + | 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.UserInput -> assert false (*NCic.Implicit (Some `Hole) -patterns not implemented *) + | 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) | CicNotationPt.Meta (index, subst) -> @@ -300,13 +351,15 @@ patterns not implemented *) 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 []) @@ -323,7 +376,8 @@ patterns not implemented *) 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), @@ -351,6 +405,15 @@ let interpretate_term_option ~context ;; +let disambiguate_path path = + let localization_tbl = NCicUntrusted.NCicHash.create 23 in + fst + (interpretate_term_and_interpretate_term_option + ~obj_context:[] ~mk_choice:(fun _ -> assert false) + ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty + ~uri:None ~is_path:true ~localization_tbl) ~context:[] path +;; + let new_flavour_of_flavour = function | `Definition -> `Definition | `MutualDefinition -> `Definition @@ -362,40 +425,50 @@ let new_flavour_of_flavour = function | `Axiom -> `Fact ;; -(* -let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl +let ncic_name_of_ident = function + | Ast.Ident (name, None) -> name + | _ -> assert false +;; + +let interpretate_obj +(* ?(create_dummy_ids=false) *) + ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice = assert (context = []); assert (is_path = false); - let interpretate_term ?(obj_context=[]) = + let interpretate_term ~obj_context = interpretate_term ~mk_choice ~localization_tbl ~obj_context in - let interpretate_term_option ?(obj_context=[]) = + let interpretate_term_option ~obj_context = 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) -> - let attrs = `Provided, new_flavour_of_flavour flavour in - let ty' = interpretate_term [] env None false ty in + | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) -> + let ty' = + interpretate_term + ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty + in let height = (* XXX calculate *) 0 in uri, height, [], [], (match bo,flavour with - None,`Axiom -> - NCic.Constant (name,None,ty',attrs) - | Some bo,`Axiom -> assert false + | None,`Axiom -> + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + NCic.Constant ([],name,None,ty',attrs) + | Some _,`Axiom -> assert false | None,_ -> - NCic.Constant (name,NCic.Implicit None,ty',attrs) + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> - match bo with + (match bo with | CicNotationPt.LetRec (kind, defs, _) -> let inductive = kind = `Inductive in - let obj_context = - List.split - (List.fold_left - (fun (i,acc) (_,(name,_),_,k) -> - ((name, NReference.reference_of_spec uri - (if inductive then NReference.Fix (i,k,0) - else NReference.CoFix i)) :: acc) - (0,[]) defs)) + let _,obj_context = + List.fold_left + (fun (i,acc) (_,(name,_),_,k) -> + (i+1, + (ncic_name_of_ident name, NReference.reference_of_spec uri + (if inductive then NReference.Fix (i,k,0) + else NReference.CoFix i)) :: acc)) + (0,[]) defs in let inductiveFuns = List.map @@ -406,149 +479,187 @@ let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast CicNotationPt.Binder (kind, var, t)) params t in let cic_body = - interpretate_term ~context ~env ~uri:None ~is_path:false + interpretate_term + ~obj_context ~context ~env ~uri:None ~is_path:false (add_binders `Lambda body) in let cic_type = - interpretate_term_option ~context ~env ~uri:None - ~is_path:false `Type + interpretate_term_option + ~obj_context:[] + ~context ~env ~uri:None ~is_path:false `Type (HExtlib.map_option (add_binders `Pi) typ) in - (name, decr_idx, cic_type, cic_body)) + ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = - interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo - in - NCic.Constant (name,Some bo,ty',attrs)) - | _ -> assert false -(* - | CicNotationPt.Inductive (params,tyl) -> - let uri = match uri with Some uri -> uri | None -> assert false in - let context,params = - let context,res = - List.fold_left - (fun (context,res) (name,t) -> - let t = - match t with - None -> CicNotationPt.Implicit - | Some t -> t in - let name = CicNotationUtil.cic_name_of_name name in - name::context,(name, interpretate_term context env None false t)::res - ) ([],[]) params - in - context,List.rev res in - let add_params = - List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - 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,Cic.MutInd (uri,i,[]))::res) - (0,[]) tyl) in - let tyl = - List.map - (fun (name,b,ty,cl) -> - let ty' = add_params (interpretate_term context env None false ty) in - let cl' = - List.map - (fun (name,ty) -> - let ty' = - add_params - (interpretate_term ~obj_context ~context ~env ~uri:None - ~is_path:false ty) + interpretate_term + ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - name,ty' - ) cl + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + NCic.Constant ([],name,Some bo,ty',attrs))) + | CicNotationPt.Inductive (params,tyl) -> + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit `JustOne + | Some t -> t in + let name = cic_name_of_name name in + let t = + interpretate_term ~obj_context:[] ~context ~env ~uri:None + ~is_path:false t in - name,b,ty',cl' - ) tyl + (name,NCic.Decl t)::context,(name,t)::res + ) ([],[]) params in - Cic.InductiveDefinition (tyl,[],List.length params,[]) - | CicNotationPt.Record (params,name,ty,fields) -> - let uri = match uri with Some uri -> uri | None -> assert false in - let context,params = - let context,res = - List.fold_left - (fun (context,res) (name,t) -> - let t = - match t with - None -> CicNotationPt.Implicit - | Some t -> t in - let name = CicNotationUtil.cic_name_of_name name in - name::context,(name, interpretate_term context env None false t)::res - ) ([],[]) params - in - context,List.rev res in - let add_params = - List.fold_right - (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let ty' = add_params (interpretate_term context env None false ty) in - let fields' = - snd ( - List.fold_left - (fun (context,res) (name,ty,_coercion,arity) -> - let context' = Cic.Name name :: context in - context',(name,interpretate_term context env None false ty)::res - ) (context,[]) fields) in - let concl = - (*here the explicit_named_substituion is assumed to be of length 0 *) - let mutind = Cic.MutInd (uri,0,[]) in - if params = [] then mutind - else - Cic.Appl - (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in - let con = + context,List.rev res in + 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 t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) - concl fields' in - let con' = add_params con in - let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in - Cic.InductiveDefinition - (tyl,[],List.length params,[`Class (`Record field_names)]) -*) + (fun (i,res) (name,_,_,_) -> + let nref = + NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno)) + in + i+1,(name,nref)::res) + (0,[]) tyl) in + let tyl = + List.map + (fun (name,_,ty,cl) -> + let ty' = + add_params + (interpretate_term ~obj_context:[] ~context ~env ~uri:None + ~is_path:false ty) in + let cl' = + List.map + (fun (name,ty) -> + let ty' = + add_params + (interpretate_term ~obj_context ~context ~env ~uri:None + ~is_path:false ty) in + let relevance = [] in + relevance,name,ty' + ) cl in + let relevance = [] in + relevance,name,ty',cl' + ) tyl + in + let height = (* XXX calculate *) 0 in + let attrs = `Provided, `Regular in + uri, height, [], [], + NCic.Inductive (inductive,leftno,tyl,attrs) + | CicNotationPt.Record (params,name,ty,fields) -> + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit `JustOne + | Some t -> t in + let name = cic_name_of_name name in + let t = + interpretate_term ~obj_context:[] ~context ~env ~uri:None + ~is_path:false t + in + (name,NCic.Decl t)::context,(name,t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in + let leftno = List.length params in + let ty' = + add_params + (interpretate_term ~obj_context:[] ~context ~env ~uri:None + ~is_path:false ty) in + let nref = + NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in + let obj_context = [name,nref] in + let fields' = + snd ( + List.fold_left + (fun (context,res) (name,ty,_coercion,_arity) -> + let ty = + interpretate_term ~obj_context ~context ~env ~uri:None + ~is_path:false ty in + let context' = (name,NCic.Decl ty)::context in + context',(name,ty)::res + ) (context,[]) fields) in + let concl = + let mutind = NCic.Const nref in + if params = [] then mutind + else + NCic.Appl + (mutind::mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in + let con' = add_params con in + let relevance = [] in + let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in + let height = (* XXX calculate *) 0 in + let attrs = `Provided, `Record field_names in + uri, height, [], [], + NCic.Inductive (true,leftno,tyl,attrs) ;; -*) -let disambiguate_term ~context ~metasenv ~subst ?goal - ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~coercion_db ~lookup_in_library +let disambiguate_term ~context ~metasenv ~subst ~expty + ~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 - let hint = - match goal with - None -> (fun _ y -> y),(fun x -> x) - | Some n -> - (fun metasenv y -> - let _,_,ty = NCicUtils.lookup_meta n metasenv in - NCic.LetIn ("_",ty,y,NCic.Rel 1)), - (function - | Disambiguate.Ok (t,m,s,ug) -> - (match t with - | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug) - | _ -> assert false) - | k -> k) - in let res,b = 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) - ~mk_localization_tbl ~hint ~subst + ~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 ~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 + let res,b = + MultiPassDisambiguator.disambiguate_thing + ~freshen_thing:CicNotationUtil.freshen_obj + ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases + ~mk_implicit ~description_of_alias ~fix_instance + ~string_context_of_context:(List.map (fun (x,_) -> Some x)) + ~universe + ~uri:(Some uri) + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~passes:(MultiPassDisambiguator.passes ()) + ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj + ~interpretate_thing:(interpretate_obj ~mk_choice) + ~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 @@ -587,4 +698,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*)