From 62f476a05884d451bfb90d845ea2b1c0a1c77f96 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Dec 2008 18:10:04 +0000 Subject: [PATCH] coercions are there, but not heavily tested --- .../disambiguation/multiPassDisambiguator.ml | 1 + .../grafite_parser/grafiteDisambiguate.ml | 5 +- .../ng_disambiguation/nCicDisambiguate.ml | 14 +- .../ng_disambiguation/nCicDisambiguate.mli | 1 + .../components/ng_kernel/nCicUntrusted.ml | 6 + .../components/ng_kernel/nCicUntrusted.mli | 1 + helm/software/components/ng_refiner/.depend | 3 + .../components/ng_refiner/.depend.opt | 3 + helm/software/components/ng_refiner/Makefile | 1 + helm/software/components/ng_refiner/check.ml | 3 +- .../components/ng_refiner/nCicCoercion.ml | 80 +++++++ .../components/ng_refiner/nCicCoercion.mli | 32 +++ .../components/ng_refiner/nCicRefiner.ml | 207 +++++++++++------- .../components/ng_refiner/nCicRefiner.mli | 8 + 14 files changed, 278 insertions(+), 87 deletions(-) create mode 100644 helm/software/components/ng_refiner/nCicCoercion.ml create mode 100644 helm/software/components/ng_refiner/nCicCoercion.mli diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index becf2a412..9415e3a74 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -124,6 +124,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing in let rec aux i errors passes = debug_print (lazy ("Pass: " ^ string_of_int i)); + prerr_endline (("Pass: " ^ string_of_int i)); match passes with [ pass ] -> (try diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index fbbbf6e02..9950b4eb7 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -582,9 +582,10 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice ~mk_implicit + ~coercion_db:(NCicCoercion.db ()) ~context:[] ~metasenv:[] ~subst:[] - ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~aliases:lexicon_status.LexiconEngine.aliases + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) (text,prefix_len,ty) with | [_,metasenv,subst,ty],_ -> diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 6ec2c6507..4092e7ae0 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,7 +27,8 @@ let cic_name_of_name = function | _ -> assert false ;; -let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization_tbl = +let refine_term + metasenv subst context uri ~coercion_db ~use_coercions term _ ~localization_tbl= assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); @@ -39,7 +40,12 @@ let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization assert false in let metasenv, subst, term, _ = - NCicRefiner.typeof metasenv subst context term None ~localise + NCicRefiner.typeof + ~look_for_coercion:( + if use_coercions then + NCicCoercion.look_for_coercion coercion_db + else (fun _ _ _ _ _ -> [])) + metasenv subst context term None ~localise in Disambiguate.Ok (term, metasenv, subst, ()) with @@ -431,7 +437,7 @@ let domain_of_term ~context = let disambiguate_term ~context ~metasenv ~subst ?goal ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~lookup_in_library + ~aliases ~universe ~coercion_db ~lookup_in_library (text,prefix_len,term) = let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in @@ -459,7 +465,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) + ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term) ~mk_localization_tbl ~hint ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 741bd3d0f..55a42a176 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -21,6 +21,7 @@ val disambiguate_term : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> + coercion_db:NCicCoercion.db -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 57a2a4f17..d7635fe88 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -81,3 +81,9 @@ module NCicHash = end) ;; +let mk_appl he args = + if args = [] then he else + match he with + | NCic.Appl l -> NCic.Appl (l@args) + | _ -> NCic.Appl (he::args) +;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index b195760cb..79ac48c38 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -19,3 +19,4 @@ val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list module NCicHash : Hashtbl.S with type key = NCic.term +val mk_appl : NCic.term -> NCic.term list -> NCic.term diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 863921720..c8ccb5d0c 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,7 +1,10 @@ +nCicCoercion.cmi: nDiscriminationTree.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicCoercion.cmo: nDiscriminationTree.cmi nCicCoercion.cmi +nCicCoercion.cmx: nDiscriminationTree.cmx nCicCoercion.cmi nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index 863921720..c8ccb5d0c 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,7 +1,10 @@ +nCicCoercion.cmi: nDiscriminationTree.cmi nDiscriminationTree.cmo: nDiscriminationTree.cmi nDiscriminationTree.cmx: nDiscriminationTree.cmi nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicCoercion.cmo: nDiscriminationTree.cmi nCicCoercion.cmi +nCicCoercion.cmx: nDiscriminationTree.cmx nCicCoercion.cmi nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index e859d3996..f3a7fba40 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -4,6 +4,7 @@ PREDICATES = INTERFACE_FILES = \ nDiscriminationTree.mli \ nCicMetaSubst.mli \ + nCicCoercion.mli \ nCicUnification.mli \ nCicRefiner.mli \ diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index d4a329697..120d3e9cb 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -271,7 +271,8 @@ let _ = let bo = curryfy [] bo in (try let metasenv, subst, bo, infty = - NCicRefiner.typeof [] [] [] bo None + NCicRefiner.typeof + ~look_for_coercion:(fun _ _ _ _ _ -> []) [] [] [] bo None in let metasenv, subst = try diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml new file mode 100644 index 000000000..2fc29d597 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -0,0 +1,80 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) + +module COT : Set.OrderedType with type t = NCic.term * int * int = + struct + type t = NCic.term * int * int + let compare = Pervasives.compare + end + +module CoercionSet = Set.Make(COT) + +module DB = + Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet) + +type db = DB.t * DB.t + +let index_coercion (db_src,db_tgt) c src tgt arity arg = + let data = (c,arity,arg) in + let db_src = DB.index db_src src data in + let db_tgt = DB.index db_tgt tgt data in + db_src, db_tgt +;; + +let db () = + List.fold_left + (fun db (_,tgt,clist) -> + List.fold_left + (fun db (uri,_,arg) -> + let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in + let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in + let src, tgt = + let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in + match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1) + with + | NCic.Prod (_, src, tgt),_,_ -> + src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt + | t,metasenv,_ -> + prerr_endline ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); + assert false + in +(* + prerr_endline (Printf.sprintf "indicizzo %s %d %d" + (UriManager.string_of_uri uri) arity arg); +*) + index_coercion db c src tgt arity arg) + db clist) + (DB.empty,DB.empty) (CoercDb.to_list ()) +;; + +(* XXX saturate takes no subst!!!! *) +let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty = + let set_src = DB.retrieve_unifiables db_src infty in + let set_tgt = DB.retrieve_unifiables db_tgt expty in + let candidates = CoercionSet.inter set_src set_tgt in + prerr_endline "aaaaaaaaaaaaa"; + List.map + (fun (t,arity,arg) -> + let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in + let ty, metasenv, args = + NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity + in + prerr_endline ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ + NCicPp.ppterm ~metasenv ~subst:_subst ~context + (NCicUntrusted.mk_appl t args) ^ " --- " ^ + string_of_int (List.length args) ^ " == " ^ string_of_int arg); + metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) + (CoercionSet.elements candidates) +;; diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli new file mode 100644 index 000000000..d01e30a5a --- /dev/null +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -0,0 +1,32 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) + +type db + +(* index (\x.c ?? x ??): A -> B + index_coercion db c A B \arity_left(c ??x??) \position(x,??x??) +*) +val index_coercion: + db -> NCic.term -> NCic.term -> NCic.term -> int -> int -> db + + (* gets the old imperative coercion DB *) +val db : unit -> db + +val look_for_coercion: + db -> + NCic.metasenv -> NCic.substitution -> NCic.context -> + (* inferred type, expected type *) + NCic.term -> NCic.term -> + (* enriched metasenv, new term, its type, metavriable to + * be unified with the old term *) + (NCic.metasenv * NCic.term * NCic.term * NCic.term) list diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index a0324eab2..e9d0e97fd 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -46,54 +46,6 @@ let exp_implicit metasenv context expty = | _ -> assert false ;; -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 - | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> - metasenv, subst, C.Meta(i,(0,C.Irl 0)) - | C.Meta (i,(_,lc)) -> - let len = match lc with C.Irl len->len | C.Ctx l->List.length l in - let metasenv, subst, newmeta = - if len > 0 then - NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) - else metasenv, subst, i - in - metasenv, subst, C.Meta (newmeta,(0,C.Irl 0)) - | C.Sort _ as t -> metasenv, subst, t - | 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 orig_s localise t1 in - let metasenv, subst, t2 = - 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) -> - metasenv, subst, C.Sort (C.Type (u1@u2)) - | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2 - | C.Meta _, C.Sort _ - | C.Meta _, C.Meta (_,(_,_)) - | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, t2 - | x, (C.Sort _ | C.Meta _) | _, x -> - let y, context, orig = - if x == t1 then s, context, orig_s - else t, ((name,C.Decl s)::context), orig_t - in - raise (RefineFailure (lazy (localise orig,Printf.sprintf - "%s is expected to be a type, but its type is %s that is not a sort" - (NCicPp.ppterm ~subst ~metasenv ~context y) - (NCicPp.ppterm ~subst ~metasenv ~context x)))) -;; let check_allowed_sort_elimination localise r orig = let mkapp he arg = @@ -144,8 +96,10 @@ let check_allowed_sort_elimination localise r orig = ;; let rec typeof - ?(localise=fun _ -> Stdpp.dummy_loc) metasenv subst context term expty + ?(localise=fun _ -> Stdpp.dummy_loc) + ~look_for_coercion metasenv subst context term expty = + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term); let force_ty metasenv subst context orig t infty expty = (*D*)inside 'F'; try let rc = match expty with @@ -157,15 +111,14 @@ let rec typeof pp (lazy ( (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^ (NCicPp.ppterm ~metasenv ~subst ~context expty))); - let metasenv, subst = - try NCicUnification.unify metasenv subst context infty expty - with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf - "The term %s has type %s but is here used with type %s" - (NCicPp.ppterm ~metasenv ~subst ~context t) - (NCicPp.ppterm ~metasenv ~subst ~context infty) - (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) - in - metasenv, subst, t, expty) + try + let metasenv, subst = + NCicUnification.unify metasenv subst context infty expty + in + metasenv, subst, t, expty + with exc -> + try_coercions ~look_for_coercion ~localise + metasenv subst context t orig infty expty true exc) | None -> metasenv, subst, t, infty (*D*)in outside(); rc with exc -> outside (); raise exc in @@ -212,8 +165,8 @@ let rec typeof let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in let context1 = (name,(C.Decl s))::context in let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in - let metasenv, subst, ty = - sort_of_prod localise metasenv subst + let metasenv, subst, s, t, ty = + sort_of_prod ~look_for_coercion localise metasenv subst context orig_s orig_t (name,s) t (s1,s2) in metasenv, subst, NCic.Prod(name,s,t), ty @@ -224,12 +177,13 @@ let rec typeof | Some expty -> match NCicReduction.whd ~subst context expty with | C.Prod (_,s,t) -> Some s, Some t - | _ -> None, None + | _ -> None, None (** XXX FUNCLASS |-> QUALCOSA *) in let metasenv, subst, s, ty_s = typeof_aux metasenv subst context None s in - let metasenv, subst, _ = - force_to_sort metasenv subst context orig_s localise ty_s in + let metasenv, subst, s, _ = + force_to_sort ~look_for_coercion + metasenv subst context s orig_s localise ty_s in let (metasenv,subst), exp_ty_t = match exp_s with | Some exp_s -> @@ -240,7 +194,6 @@ let rec typeof exp_s))) exc)) | None -> (metasenv, subst), None in - (* XXX coerce_to_sort s *) let context = (n,C.Decl s) :: context in let metasenv, subst, t, ty_t = typeof_aux metasenv subst context exp_ty_t t @@ -249,8 +202,9 @@ let rec typeof | 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 orig_ty localise ty_ty in + let metasenv, subst, ty, _ = + force_to_sort ~look_for_coercion + metasenv subst context ty 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 @@ -262,7 +216,8 @@ let rec typeof | C.Appl ((he as orig_he)::(_::_ as args)) -> let metasenv, subst, he, ty_he = typeof_aux metasenv subst context None he in - eat_prods localise metasenv subst context orig_he he ty_he args + eat_prods ~localise ~look_for_coercion + metasenv subst context orig_he he ty_he args | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r, outtype,(term as orig_term),pl) as orig -> @@ -326,21 +281,106 @@ let rec typeof in typeof_aux metasenv subst context expty term -and eat_prods localise metasenv subst context orig_he he ty_he args = +and try_coercions + ~localise ~look_for_coercion + metasenv subst context t orig_t infty expty perform_unification exc += + (* we try with a coercion *) + let rec first exc = function + | [] -> + raise (wrap_exc (lazy (localise orig_t, Printf.sprintf + "The term %s has type %s but is here used with type %s" + (NCicPp.ppterm ~metasenv ~subst ~context t) + (NCicPp.ppterm ~metasenv ~subst ~context infty) + (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) + | (metasenv, newterm, newtype, meta)::tl -> + try + let metasenv, subst = + NCicUnification.unify metasenv subst context meta t + in + let metasenv, subst = + if perform_unification then + NCicUnification.unify metasenv subst context newtype expty + else metasenv, subst + in + metasenv, subst, newterm, newtype + with + | NCicUnification.UnificationFailure _ -> first exc tl + | NCicUnification.Uncertain _ as exc -> first exc tl + in + first exc + (look_for_coercion metasenv subst context infty expty) + +and force_to_sort + ~look_for_coercion metasenv subst context t orig_t localise ty += + match NCicReduction.whd ~subst context ty with + | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> + metasenv, subst, t, ty + | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> + metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) + | C.Meta (i,(_,lc)) -> + let len = match lc with C.Irl len->len | C.Ctx l->List.length l in + let metasenv, subst, newmeta = + if len > 0 then + NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) + else metasenv, subst, i + in + metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0)) + | C.Sort _ as ty -> metasenv, subst, t, ty + | ty -> + try_coercions ~localise ~look_for_coercion metasenv subst context + t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false + (RefineFailure (lazy (localise orig_t, + "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t + ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty))) + +and sort_of_prod ~look_for_coercion + localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) += + let metasenv, subst, s, t1 = + force_to_sort + ~look_for_coercion metasenv subst context s orig_s localise t1 in + let metasenv, subst, t, t2 = + force_to_sort ~look_for_coercion metasenv subst ((name,C.Decl s)::context) + t orig_t localise t2 in + match t1, t2 with + | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2 + | C.Sort (C.Type u1), C.Sort (C.Type u2) -> + metasenv, subst, s, t, C.Sort (C.Type (u1@u2)) + | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2 + | C.Meta _, C.Sort _ + | C.Meta _, C.Meta (_,(_,_)) + | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2 + | x, (C.Sort _ | C.Meta _) | _, x -> + let y, context, orig = + if x == t1 then s, context, orig_s + else t, ((name,C.Decl s)::context), orig_t + in + raise (RefineFailure (lazy (localise orig,Printf.sprintf + "%s is expected to be a type, but its type is %s that is not a sort" + (NCicPp.ppterm ~subst ~metasenv ~context y) + (NCicPp.ppterm ~subst ~metasenv ~context x)))) + +and eat_prods + ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args += (*D*)inside 'E'; try let rc = - let rec aux metasenv subst args_so_far ty_he = function - | [] -> metasenv, subst, NCic.Appl (he :: List.rev args_so_far), ty_he + let rec aux metasenv subst args_so_far he ty_he = function + | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he | arg::tl -> match NCicReduction.whd ~subst context ty_he with | C.Prod (_,s,t) -> let metasenv, subst, arg, _ = - typeof ~localise metasenv subst context arg (Some s) in + typeof ~look_for_coercion ~localise + metasenv subst context arg (Some s) in let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in - aux metasenv subst (arg :: args_so_far) t tl + aux metasenv subst (arg :: args_so_far) he t tl | C.Meta _ | C.Appl (C.Meta _ :: _) as t -> let metasenv, subst, arg, ty_arg = - typeof ~localise metasenv subst context arg None in + typeof ~look_for_coercion ~localise + metasenv subst context arg None in let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv (("_",C.Decl ty_arg) :: context) `Type @@ -363,7 +403,7 @@ and eat_prods localise metasenv subst context orig_he he ty_he args = (* XXX coerce to funclass *) in let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in - aux metasenv subst (arg :: args_so_far) meta tl + aux metasenv subst (arg :: args_so_far) he meta tl | C.Match (_,_,C.Meta _,_) | C.Match (_,_,C.Appl (C.Meta _ :: _),_) | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) -> @@ -371,13 +411,20 @@ and eat_prods localise metasenv subst context orig_he he ty_he args = ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) (List.length args) (List.length args_so_far)))) - | _ -> - raise (RefineFailure (lazy (localise orig_he, Printf.sprintf - ("The term %s is here applied to %d arguments but expects " ^^ - "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) - (List.length args) (List.length args_so_far)))) + | ty -> + let metasenv, subst, newhead, newheadty = + try_coercions ~localise ~look_for_coercion metasenv subst context + (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty + (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) + false + (RefineFailure (lazy (localise orig_he, Printf.sprintf + ("The term %s is here applied to %d arguments but expects " ^^ + "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) + (List.length args) (List.length args_so_far)))) + in + aux metasenv subst [] newhead newheadty (arg :: tl) in - aux metasenv subst [] ty_he args + aux metasenv subst [] he ty_he args (*D*)in outside(); rc with exc -> outside (); raise exc ;; (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index 9b10e3448..741477080 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -17,6 +17,14 @@ exception AssertFailure of string Lazy.t;; val typeof : ?localise:(NCic.term -> Stdpp.location) -> + look_for_coercion:( + NCic.metasenv -> NCic.substitution -> NCic.context -> + (* inferred type, expected type *) + NCic.term -> NCic.term -> + (* enriched metasenv, new term, its type, metavriable to + * be unified with the old term *) + (NCic.metasenv * NCic.term * NCic.term * NCic.term) list + ) -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term option -> (* term, expected type *) NCic.metasenv * NCic.substitution * NCic.term * NCic.term -- 2.39.2