From 8e65e5eb59904848a24506ffe55323fdcc8bf975 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Dec 2008 19:36:50 +0000 Subject: [PATCH] Fixes: - new letin interpretation in nCicDisambiguation fixed to not swap arguments - new refiner raises good exception in case a sort in not such - reference raise good exception instead of assert false Improvements: - new disambiguation attached - constructor -> indty function in reference --- .../grafite_parser/grafiteDisambiguate.ml | 90 +++++++++---------- .../ng_disambiguation/nCicDisambiguate.ml | 65 +++++++++++--- helm/software/components/ng_kernel/nCicPp.ml | 8 +- .../components/ng_kernel/nReference.ml | 11 ++- .../components/ng_kernel/nReference.mli | 2 + .../components/ng_refiner/nCicRefiner.ml | 22 +++-- 6 files changed, 130 insertions(+), 68 deletions(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 58666eed5..b02732543 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -45,21 +45,6 @@ let singleton msg = function in HLog.debug debug; assert false -(* -let cic_codomain_of_uri uri = - (UriManager.string_of_uri uri, - let term = - try - CicUtil.term_of_uri uri - with exn -> - assert false - in - fun _ _ _ -> term) -;; -*) - -(*let cic_num_choices = DisambiguateChoices.lookup_num_choices;;*) - let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" @@ -78,7 +63,38 @@ let cic_mk_choice = function (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri)) ;; -let cic_mk_implicit b = +let ncic_mk_choice = function + | LexiconAst.Symbol_alias (name, _, dsc) -> + if name = __Implicit then + dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) + else if name = __Closed_Implicit then + dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) + else + DisambiguateChoices.lookup_symbol_by_dsc + ~mk_implicit:(function + | true -> NCic.Implicit `Closed + | false -> NCic.Implicit `Term) + ~mk_appl:(function + (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) + ~term_of_uri:(fun uri -> + fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) + name dsc + | LexiconAst.Number_alias (_, dsc) -> + let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in + desc, `Num_interp + (fun num -> + fst (OCic2NCic.convert_term + (UriManager.uri_of_string "cic:/xxx/x.con") + (match f with `Num_interp f -> f num | _ -> assert false))) + | LexiconAst.Ident_alias (name, uri) -> + uri, `Sym_interp + (fun l->assert(l = []); + let uri = UriManager.uri_of_string uri in + fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) +;; + + +let mk_implicit b = match b with | false -> LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit") @@ -86,28 +102,6 @@ let cic_mk_implicit b = LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") ;; -let ncic_codomain_of_uri uri = - (UriManager.string_of_uri uri, - let term = - try - fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) - with exn -> - assert false - in - fun _ _ _ -> term) -;; - -let ncic_num_choices _ = (*assert false*) [];; -let ncic_mk_choice = - DisambiguateChoices.mk_choice - ~mk_implicit:(function - | true -> NCic.Implicit `Closed - | false -> NCic.Implicit `Term) - ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) - ~term_of_uri:(fun uri -> - fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) -;; - let lookup_in_library interactive_user_uri_choice input_or_locate_uri item = @@ -169,7 +163,7 @@ term = ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit:cic_mk_implicit + ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst:[] (text,prefix_len,term)) in @@ -191,7 +185,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = (CicDisambiguate.disambiguate_term ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit:cic_mk_implicit + ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) @@ -576,17 +570,19 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in -(* + (* (match obj with CicNotationPt.Theorem (_,_,ty,_) -> (try (match NCicDisambiguate.disambiguate_term - ~lookup_in_library:(lookup_in_library ncic_codomain_of_uri - ncic_mk_choice ncic_num_choices) + ~lookup_in_library:lookup_in_library + ~description_of_alias:LexiconAst.description_of_alias + ~mk_choice:ncic_mk_choice + ~mk_implicit ~context:[] ~metasenv:[] ~subst:[] - ~aliases:DisambiguateTypes.Environment.empty - ~universe:(Some DisambiguateTypes.Environment.empty) + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) (text,prefix_len,ty) with | [_,metasenv,subst,ty],_ -> @@ -603,13 +599,13 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ) | _ -> () ); -*) + *) let (diff, metasenv, _, cic, _) = singleton "third" (CicDisambiguate.disambiguate_obj ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit:cic_mk_implicit + ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 267b40a20..03579afab 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -34,7 +34,9 @@ let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization try let localise t = try NCicUntrusted.NCicHash.find localization_tbl t - with Not_found -> assert false + with Not_found -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); + assert false in let metasenv, subst, term, _ = NCicRefiner.typeof metasenv subst context term None ~localise @@ -62,12 +64,15 @@ let find_in_context name context = let interpretate_term ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast - ~localization_tbl + ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); let rec aux ~localize loc context = function + t -> + let res = + match t with | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; @@ -128,14 +133,15 @@ let interpretate_term | Some (indty_ident, _) -> (match Disambiguate.resolve ~env ~mk_choice (Id indty_ident) (`Args []) with - | NCic.Const r -> r + | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) - | _ -> + | t -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched "^ - "is not (co)inductive!")))) + "is not (co)inductive: " ^ NCicPp.ppterm + ~metasenv:[] ~subst:[] ~context:[] t)))) | None -> let rec fst_constructor = function @@ -146,16 +152,26 @@ let interpretate_term "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) in - (match Disambiguate.resolve ~env ~mk_choice +(* + DisambiguateTypes.Environment.iter + (fun k v -> + prerr_endline + (DisambiguateTypes.string_of_domain_item k ^ " => " ^ + description_of_alias v)) env; +*) + (match Disambiguate.resolve ~env ~mk_choice (Id (fst_constructor branches)) (`Args []) with - | NCic.Const r -> r + | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> + let b,_,_,_,_ = NCicEnvironment.get_checked_indtys r in + NReference.mk_indty b r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) - | _ -> + | t -> raise (DisambiguateTypes.Invalid_choice (lazy (loc, - "The type of the term to be matched is not (co)inductive!")))) + "The type of the term to be matched is not (co)inductive: " + ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)))) in let _,leftsno,itl,_,indtyp_no = NCicEnvironment.get_checked_indtys indtype_ref in @@ -247,7 +263,7 @@ let interpretate_term | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in - NCic.LetIn (cic_name, cic_def, cic_typ, cic_body) + NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false (* let context' = @@ -372,7 +388,8 @@ patterns not implemented *) in NCic.Meta (index, (0, NCic.Ctx cic_subst)) | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop - | CicNotationPt.Sort `Set -> assert false + | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type + [false,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"]) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type @@ -381,6 +398,11 @@ patterns not implemented *) Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) | _ -> assert false (* god bless Bologna *) + + in + prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] + res); + res and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) -> @@ -442,3 +464,24 @@ let disambiguate_term ~context ~metasenv ~subst ?goal List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; +let _ = +let mk_type n = + if n = 0 then + [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] +in +let mk_cprop n = + if n = 0 then + [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")] +in + NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1); + NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1); + NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1); + NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1); + NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0); + NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0); +;; + diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 2b0787a72..59d6bcf48 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -110,12 +110,16 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = F.fprintf f "@; @[[ "; if pl <> [] then begin - F.fprintf f "@[%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r)); + F.fprintf f "@[%s ⇒@;" + (try r2s inside_fix (R.mk_constructor 1 r) + with R.IllFormedReference _ -> "#ERROR#"); aux ~toplevel:true ctx (List.hd pl); F.fprintf f "@]"; ignore(List.fold_left (fun i t -> - F.fprintf f "@;| @[%s ⇒@;" (r2s inside_fix (R.mk_constructor i r)); + F.fprintf f "@;| @[%s ⇒@;" + (try r2s inside_fix (R.mk_constructor i r) + with R.IllFormedReference _ -> "#ERROR#"); aux ~toplevel:true ctx t; F.fprintf f "@]"; i+1) diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 2892915c3..b5782bd03 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -119,7 +119,16 @@ let string_of_reference (Ref (u,indinfo)) = let mk_constructor j = function | Ref (u, Ind (_,i,l)) -> reference_of_string (string_of_reference (Ref (u, Con (i,j,l)))) - | _ -> assert false + | r -> + raise (IllFormedReference (lazy ("NON INDUCTIVE TYPE REFERENCE: " ^ + string_of_reference r))); +;; +let mk_indty b = function + | Ref (u, Con (i,_,l)) -> + reference_of_string (string_of_reference (Ref (u, Ind (b,i,l)))) + | r -> + raise (IllFormedReference (lazy + ("NON INDUCTIVE TYPE CONSTRUCTOR REFERENCE: " ^ string_of_reference r))); ;; let mk_fix i j = function diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index 703d32d02..1de23ad8b 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -29,5 +29,7 @@ val reference_of_string: string -> reference (* given the reference of an inductive type, returns the i-th contructor *) val mk_constructor: int -> reference -> reference +(* given the reference of an inductive type constructor, returns the indty *) +val mk_indty: bool -> reference -> reference val mk_fix: int -> int -> reference -> reference val mk_cofix: int -> reference -> reference diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 479f95802..a0324eab2 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -46,7 +46,7 @@ let exp_implicit metasenv context expty = | _ -> assert false ;; -let force_to_sort metasenv subst context t = +let force_to_sort metasenv subst context orig localise t = match NCicReduction.whd ~subst context t with | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t -> metasenv, subst, t @@ -61,15 +61,21 @@ let force_to_sort metasenv subst context t = in metasenv, subst, C.Meta (newmeta,(0,C.Irl 0)) | C.Sort _ as t -> metasenv, subst, t - | _ -> assert false + | t -> + raise (RefineFailure (lazy + (localise orig, + "Not a sort: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t))) ;; let sort_of_prod localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) = - let metasenv, subst, t1 = force_to_sort metasenv subst context t1 in + let metasenv, subst, t1 = + force_to_sort metasenv subst context orig_s localise t1 in let metasenv, subst, t2 = - force_to_sort metasenv subst ((name,C.Decl s)::context) t2 in + force_to_sort metasenv subst ((name,C.Decl s)::context) + orig_t localise t2 in match t1, t2 with | C.Sort _, C.Sort C.Prop -> metasenv, subst, t2 | C.Sort (C.Type u1), C.Sort (C.Type u2) -> @@ -222,7 +228,8 @@ let rec typeof in let metasenv, subst, s, ty_s = typeof_aux metasenv subst context None s in - let metasenv, subst, _ = force_to_sort metasenv subst context ty_s in + let metasenv, subst, _ = + force_to_sort metasenv subst context orig_s localise ty_s in let (metasenv,subst), exp_ty_t = match exp_s with | Some exp_s -> @@ -239,10 +246,11 @@ let rec typeof typeof_aux metasenv subst context exp_ty_t t in metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t) - | C.LetIn (n,ty,t,bo) -> + | C.LetIn (n,(ty as orig_ty),t,bo) -> let metasenv, subst, ty, ty_ty = typeof_aux metasenv subst context None ty in - let metasenv, subst, _ = force_to_sort metasenv subst context ty_ty in + let metasenv, subst, _ = + force_to_sort metasenv subst context orig_ty localise ty_ty in let metasenv, subst, t, _ = typeof_aux metasenv subst context (Some ty) t in let context1 = (n, C.Def (t,ty)) :: context in -- 2.39.2