X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=95e6c7ba6d213ef308592031b32e4e550666d29a;hb=f4f050696e66b8604d9f0ff8173afe03addf74d6;hp=ccf662f185967f799faacbcb4fabf914adc005db;hpb=8d8ac4a42998970114e43c2fb13ff2c98f7c259a;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index ccf662f18..95e6c7ba6 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -29,6 +29,8 @@ exception RefineFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let insert_coercions = ref true + let debug_print = fun _ -> () let profiler = HExtlib.profile "CicRefine.fo_unif" @@ -43,16 +45,20 @@ in profiler.HExtlib.profile foo () | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; -let enrich loc f exn = +let enrich localization_tbl t ?(f = fun msg -> msg) exn = let exn' = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) - | _ -> assert false + | _ -> assert false in + let loc = + try + Cic.CicHash.find localization_tbl t + with Not_found -> + prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + assert false in - match loc with - None -> raise exn' - | Some loc -> raise (HExtlib.Localized (loc,exn')) + raise (HExtlib.Localized (loc,exn')) let relocalize localization_tbl oldt newt = try @@ -86,6 +92,7 @@ let exp_impl metasenv subst context = | _ -> assert false ;; + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -207,7 +214,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - (* this stops on binders, so we have to call it every time *) + let (t',_,_,_,_) as res = match t with (* function *) C.Rel n -> @@ -224,9 +231,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph - | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) + | None -> + enrich localization_tbl t + (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure (lazy "Not a close term"))) + _ -> + enrich localization_tbl t + (RefineFailure (lazy "Not a close term"))) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst @@ -275,47 +286,68 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty' ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + (try + let subst''',metasenv''',ugraph3 = + fo_unif_subst subst'' context metasenv'' + inferredty ty' ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + with + exn -> + enrich localization_tbl te' + ~f:(fun _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst'' te' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst'' inferredty + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst'' ty' context)) exn + ) | C.Prod (name,s,t) -> let carr t subst context = CicMetaSubst.apply_subst subst t in - let coerce_to_sort - in_source tgt_sort t type_to_coerce subst ctx metasenv uragph + let coerce_to_sort in_source tgt_sort t type_to_coerce + subst context metasenv uragph = - let coercion_src = carr type_to_coerce subst ctx in - match coercion_src with - | Cic.Sort _ -> - t,type_to_coerce,subst,metasenv,ugraph -(* - | Cic.Meta _ as meta when not in_source -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in - let subst, metasenv, ugraph = - fo_unif_subst - subst ctx metasenv meta coercion_tgt ugraph - in - t, Cic.Sort tgt_sort, subst, metasenv, ugraph -*) - | Cic.Meta _ as meta -> - t, meta, subst, metasenv, ugraph - | Cic.Cast _ as cast -> - t, cast, subst, metasenv, ugraph - | term -> - let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - (match boh with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - raise - (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) - | CoercGraph.NotMetaClosed -> - raise - (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) + if not !insert_coercions then + t,type_to_coerce,subst,metasenv,ugraph + else + let coercion_src = carr type_to_coerce subst context in + match coercion_src with + | Cic.Sort _ -> + t,type_to_coerce,subst,metasenv,ugraph + | Cic.Meta _ as meta -> + t, meta, subst, metasenv, ugraph + | Cic.Cast _ as cast -> + t, cast, subst, metasenv, ugraph + | term -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + (match boh with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + enrich localization_tbl t + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst t context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl t + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst t context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.SomeCoercion c -> + let newt, tty, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;t]) coercion_tgt + in + newt, tty, subst, metasenv, ugraph) in let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -342,22 +374,41 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let s',sort1 = - match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> s',sort1 - | coercion_src -> - let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in - match boh with - | CoercGraph.SomeCoercion c -> - Cic.Appl [c;s'], coercion_tgt - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ - | CoercGraph.NotMetaClosed -> - raise (RefineFailure (lazy (sprintf - "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1)))) + let s',sort1,subst',metasenv',ugraph1 = + if not !insert_coercions then + s',sort1, subst', metasenv', ugraph1 + else + match CicReduction.whd ~subst:subst' context sort1 with + | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 + | coercion_src -> + let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + match boh with + | CoercGraph.SomeCoercion c -> + let newt, tty, subst', metasenv', ugraph1 = + avoid_double_coercion + subst' metasenv' ugraph1 + (Cic.Appl[c;s']) coercion_tgt + in + newt, tty, subst', metasenv', ugraph1 + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + enrich localization_tbl s' + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst s' context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl s' + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst s' context ^ + " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context + subst coercion_src context ^ " that is not a sort"))) in let context_for_t = ((Some (n,(C.Decl s')))::context) in let t',type2,subst'',metasenv'',ugraph2 = @@ -392,7 +443,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in - relocalize localization_tbl x x'; (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in @@ -400,8 +450,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 in - C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) + avoid_double_coercion + subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty + | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context @@ -443,9 +494,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t C.InductiveDefinition (l,expl_params,parsno,_) -> List.nth l i , expl_params, parsno, u | _ -> - raise - (RefineFailure - (lazy ("Unkown mutual inductive definition " ^ + enrich localization_tbl t + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in let rec count_prod t = @@ -481,8 +532,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv,ugraph3 = + try fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 + with + exn -> + enrich localization_tbl term' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst term' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst expected_type' context)) in let rec instantiate_prod t = function @@ -528,6 +590,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t its instances *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 in (match outtype with | C.Meta (n,l) -> (let candidate,ugraph5,metasenv,subst = @@ -660,9 +724,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) - let outtype,outtypety, subst, metasenv,ugraph4 = - type_of_aux subst metasenv context outtype ugraph4 - in let tlbody_and_type,subst,metasenv,ugraph4 = List.fold_right (fun x (res,subst,metasenv,ugraph) -> @@ -784,6 +845,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fl_ty' fl_bo' fl in C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 + in + relocalize localization_tbl t t'; + res + + and avoid_double_coercion subst metasenv ugraph t ty = + match t with + | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CicMetaSubst.apply_subst subst ty in + (match CoercGraph.look_for_coercion source_carr tgt_carr + with + | CoercGraph.SomeCoercion c -> + Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph + | _ -> assert false) (* the composite coercion must exist *) + | _ -> t, ty, subst, metasenv, ugraph (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -849,7 +926,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = match tl with [] -> [],metasubst,metasenv,ugraph - | ((uri,t) as subst)::tl -> + | (uri,t)::tl -> let ty_uri,ugraph1 = type_of_variable uri ugraph in let typeofvar = CicSubstitution.subst_vars substs ty_uri in @@ -867,8 +944,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t ) ; *) let t',typeoft,metasubst',metasenv',ugraph2 = - type_of_aux metasubst metasenv context t ugraph1 - in + type_of_aux metasubst metasenv context t ugraph1 in + let subst = uri,t' in let metasubst'',metasenv'',ugraph3 = try fo_unif_subst @@ -1000,35 +1077,55 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn when allow_coercions -> + with exn when allow_coercions && !insert_coercions -> (* we search a coercion from hety to s *) - let coer = + let coer, tgt_carr = let carr t subst context = CicMetaSubst.apply_subst subst t in let c_hety = carr hety subst context in let c_s = carr s subst context in - CoercGraph.look_for_coercion c_hety c_s + CoercGraph.look_for_coercion c_hety c_s, c_s in - match coer with + (match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - let msg e = - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)) - in - enrich - (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None) - msg exn + enrich localization_tbl hete + (RefineFailure + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on meta")) + enrich localization_tbl hete + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> - (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph + let newt, _, subst, metasenv, ugraph = + avoid_double_coercion + subst metasenv ugraph + (Cic.Appl[c;hete]) tgt_carr + in + newt, subst, metasenv, ugraph) + | exn -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) exn in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context @@ -1121,7 +1218,6 @@ let map_first_n n start f g l = (*CSC: this is a very rough approximation; to be finished *) let are_all_occurrences_positive metasenv ugraph uri tys leftno = - let number_of_types = List.length tys in let subst,metasenv,ugraph,tys = List.fold_right (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) -> @@ -1235,7 +1331,9 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv,ugraph,cl' = List.fold_right (fun (name,ty) (metasenv,ugraph,res) -> - let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty = + CicTypeChecker.debrujin_constructor + ~cb:(relocalize localization_tbl) uri typesno ty in let ty',_,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv con_context ty ugraph in let ty' = undebrujin uri typesno tys ty' in