X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=6bf1c05ba0226ab739812b82d02cd2f95acad3a4;hb=55ef67743ddc33b1b3f86384909fddadbb7d5103;hp=5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da;hpb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 5fa3b8188..6bf1c05ba 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -19,8 +19,8 @@ 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 cic_name_of_name = function | Ast.Ident (n, None) -> n @@ -64,7 +64,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 +72,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 +118,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,7 +321,7 @@ 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 @@ -324,7 +329,8 @@ let interpretate_term_and_interpretate_term_option with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") | CicNotationPt.NRef nref -> NCic.Const nref - | CicNotationPt.Implicit -> NCic.Implicit `Term + | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector + | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) @@ -337,15 +343,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 []) @@ -362,7 +368,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), @@ -493,7 +500,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 = @@ -507,13 +514,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 @@ -543,7 +548,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 = @@ -551,7 +556,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 =