From 7bc72d8afaebb1d2070a26b07f9bf4242b648e2c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Mar 2009 20:16:35 +0000 Subject: [PATCH] - fixed hint generation, more hints are generated - fixpoint refinement added - Appl [Meta _; ... ] handled correctly, no double Appl or Beta redex is generated (both in regular code and interators) --- .../grafite_parser/grafiteDisambiguate.ml | 63 +++++---- .../ng_disambiguation/nCicDisambiguate.ml | 128 ++++++++++++++---- .../ng_disambiguation/nCicDisambiguate.mli | 16 +++ .../components/ng_kernel/nCicReduction.ml | 23 +++- .../components/ng_kernel/nCicReduction.mli | 3 +- .../components/ng_kernel/nCicUntrusted.ml | 14 +- .../components/ng_kernel/nCicUtils.ml | 17 ++- .../components/ng_kernel/nCicUtils.mli | 3 + .../components/ng_refiner/nCicRefiner.ml | 50 +++++-- .../components/ng_refiner/nCicUnifHint.ml | 54 +++++--- .../components/ng_refiner/nCicUnification.ml | 23 ++-- 11 files changed, 285 insertions(+), 109 deletions(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 9f63a5d8f..32d666a38 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -561,21 +561,22 @@ let rec disambiguate_tactic let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let uri = - match obj with - | CicNotationPt.Inductive (_,(name,_,_,_)::_) - | CicNotationPt.Record (_,name,_,_) -> - (match baseuri with - | Some baseuri -> - Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind")) - | None -> raise BaseUriNotSetYet) - | CicNotationPt.Inductive _ -> assert false - | CicNotationPt.Theorem _ -> None in + let baseuri = + match baseuri with Some x -> x | None -> raise BaseUriNotSetYet + in + let name = + match obj with + | CicNotationPt.Inductive (_,(name,_,_,_)::_) + | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" + | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con" + | CicNotationPt.Inductive _ -> assert false + in + UriManager.uri_of_string (baseuri ^ "/" ^ name) + in let try_new cic = (NCicLibrary.clear_cache (); NCicEnvironment.invalidate (); OCic2NCic.clear (); - (match obj with - CicNotationPt.Theorem (_,_,ty,_) -> let graph = match cic with | Cic.CurrentProof (_,metasenv, _, ty,_,_) -> @@ -625,39 +626,45 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = let time = Unix.gettimeofday () in (try (match - NCicDisambiguate.disambiguate_term + NCicDisambiguate.disambiguate_obj ~lookup_in_library:lookup_in_library ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice ~mk_implicit + ~uri:(OCic2NCic.nuri_of_ouri uri) ~coercion_db:(NCicCoercion.db ()) - ~context:[] ~metasenv:[] ~subst:[] ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) - (text,prefix_len,ty) + (text,prefix_len,obj) with - | [_,metasenv,subst,ty],_ -> + | [_,_,_,obj],_ -> let time = Unix.gettimeofday () -. time in +(* NCicTypeChecker.typecheck_obj obj; *) prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty) +(* + let obj = + let u,i,m,_,o = obj in + u,i,m,[],o + in +*) + prerr_endline (NCicPp.ppobj obj) | _ -> prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! ")) with | MultiPassDisambiguator.DisambiguationError (_,s) -> - prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE:\n" ^ + prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE (" + ^UriManager.string_of_uri uri^ + "):\n" ^ String.concat "\n" (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s))) (* | exn -> prerr_endline (Printexc.to_string exn) *) ) - | _ -> ()) ) in -(* try - let time = Unix.gettimeofday () in -*) +(* let time = Unix.gettimeofday () in *) let (diff, metasenv, _, cic, _) = @@ -668,30 +675,26 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~mk_implicit ~description_of_alias:LexiconAst.description_of_alias ~aliases:lexicon_status.LexiconEngine.aliases - ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri + ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) + ~uri:(Some uri) (text,prefix_len,obj)) in (* let time = Unix.gettimeofday () -. time in - prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time); - try_new cic; + prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^ + UriManager.string_of_uri uri ^"): " ^ string_of_float time); *) - +(* try_new cic; *) let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in lexicon_status, metasenv, cic - -(* with | Sys.Break as exn -> raise exn | exn -> - try_new (Cic.InductiveDefinition ([],[],0,[])); raise exn -*) - ;; diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4e3f8cac3..b49af2bbf 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -60,6 +60,41 @@ let refine_term Disambiguate.Ko loc_msg ;; +let refine_obj + ~coercion_db 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 -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); + (*assert false*)HExtlib.dummy_floc + in + try + let obj = + NCicRefiner.typeof_obj + (NCicUnifHint.db ()) + ~look_for_coercion:( + if use_coercions then + NCicCoercion.look_for_coercion coercion_db + else (fun _ _ _ _ _ -> [])) + 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 @@ -362,40 +397,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 + 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, `Regular 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, `Regular in + NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> 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,24 +451,29 @@ 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 in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = - interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo + interpretate_term + ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - NCic.Constant (name,Some bo,ty',attrs)) - | _ -> assert false + let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + NCic.Constant ([],name,Some bo,ty',attrs)) + | _ -> raise (MultiPassDisambiguator.DisambiguationError (0, [])) (* | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in @@ -511,7 +561,6 @@ let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast (tyl,[],List.length params,[`Class (`Record field_names)]) *) ;; -*) let disambiguate_term ~context ~metasenv ~subst ?goal ~mk_implicit ~description_of_alias ~mk_choice @@ -549,6 +598,31 @@ let disambiguate_term ~context ~metasenv ~subst ?goal List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; +let disambiguate_obj + ~mk_implicit ~description_of_alias ~mk_choice + ~aliases ~universe ~coercion_db ~lookup_in_library ~uri + (text,prefix_len,obj) + = + let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in + let hint = (fun x y -> y), (fun x -> x) in + let res,b = + MultiPassDisambiguator.disambiguate_thing + ~freshen_thing:CicNotationUtil.freshen_obj + ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases + ~mk_implicit ~description_of_alias + ~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 ~coercion_db) + (text,prefix_len,obj) + ~mk_localization_tbl ~hint + in + List.map (function (a,b,c,d,_) -> a,b,c,d) res, b +;; let _ = let mk_type n = if n = 0 then diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 3784d5c18..6af6733d8 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -34,3 +34,19 @@ val disambiguate_term : NCic.term) list * bool +val disambiguate_obj : + mk_implicit:(bool -> 'a) -> + description_of_alias:('a -> string) -> + mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) -> + aliases:'a DisambiguateTypes.Environment.t -> + universe:'a list DisambiguateTypes.Environment.t option -> + coercion_db:NCicCoercion.db -> + lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> 'a list) -> + uri:NUri.uri -> + string * int * CicNotationPt.term CicNotationPt.obj -> + ((DisambiguateTypes.Environment.key * 'a) list * NCic.metasenv * + NCic.substitution * NCic.obj) + list * bool + diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 8012f0b75..0393fbcdd 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -363,24 +363,32 @@ let are_convertible ~metasenv ~subst = aux false ;; -let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l = +let rec head_beta_reduce ~delta ~upto ~subst t l = match upto, t, l with | 0, C.Appl l1, _ -> C.Appl (l1 @ l) | 0, t, [] -> t | 0, t, _ -> C.Appl (t::l) - | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l) + | _, C.Meta (n,ctx), _ -> + (try + let _,_, term,_ = NCicUtils.lookup_subst n subst in + head_beta_reduce ~delta ~upto ~subst + (NCicSubstitution.subst_meta ctx term) l + with NCicUtils.Subst_not_found _ -> if l = [] then t else C.Appl (t::l)) + | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto ~subst hd (tl @ l) | _, C.Lambda(_,_,bo), arg::tl -> let bo = NCicSubstitution.subst arg bo in - head_beta_reduce ~delta ~upto:(upto - 1) bo tl + head_beta_reduce ~delta ~upto:(upto - 1) ~subst bo tl | _, C.Const (Ref.Ref (_, Ref.Def height) as re), _ when delta <= height -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in - head_beta_reduce ~upto ~delta bo l + head_beta_reduce ~upto ~delta ~subst bo l | _, t, [] -> t | _, t, _ -> C.Appl (t::l) ;; -let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];; +let head_beta_reduce ?(delta=max_int) ?(upto= -1) ?(subst=[]) t = + head_beta_reduce ~delta ~upto ~subst t [] +;; type stack_item = RS.stack_term type environment_item = RS.env_term @@ -391,4 +399,9 @@ let reduce_machine = R.reduce let from_stack = RS.from_stack let unwind = R.unwind +let _ = + NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t) +;; + + (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 006dba9d4..691d6605d 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -28,7 +28,8 @@ val are_convertible : (* performs head beta/(delta)/cast reduction; the default is to not perform delta reduction; if provided, ~upto is the maximum number of beta redexes reduced *) -val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term +val head_beta_reduce: + ?delta:int -> ?upto:int -> ?subst:NCic.substitution -> NCic.term -> NCic.term type stack_item type environment_item diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index d7635fe88..4dcf01c53 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -22,15 +22,23 @@ let map_term_fold_a g k f a = function | C.Rel _ as t -> a,t | C.Appl [] | C.Appl [_] -> assert false | C.Appl l as orig -> + let fire_beta, upto = + match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 + in let a,l1 = (* sharing fold? *) List.fold_right (fun t (a,l) -> let a,t = f k a t in a, t :: l) l (a,[]) in - a, if l1 == l then orig else (match l1 with - | C.Appl l :: tl -> C.Appl (l@tl) - | _ -> C.Appl l1) + a, if l1 == l then orig else + let t = + match l1 with + | C.Appl l :: tl -> C.Appl (l@tl) + | _ -> C.Appl l1 + in + if fire_beta then NCicReduction.head_beta_reduce ~upto t + else t | C.Prod (n,s,t) as orig -> let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index f4f77a367..a99ae0407 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -17,6 +17,9 @@ module Ref = NReference exception Subst_not_found of int exception Meta_not_found of int +let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);; +let set_head_beta_reduce = (:=) head_beta_reduce;; + let expand_local_context = function | C.Irl len -> let rec aux acc = function @@ -61,10 +64,18 @@ let map g k f = function | C.Rel _ as t -> t | C.Appl [] | C.Appl [_] -> assert false | C.Appl l as orig -> - (match HExtlib.sharing_map (f k) l with + let fire_beta, upto = + match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 + in + let l1 = HExtlib.sharing_map (f k) l in + if l == l1 then orig else + let t = + match l1 with | C.Appl l :: tl -> C.Appl (l@tl) - | l1 when l == l1 -> orig - | l1 -> C.Appl l1) + | l1 -> C.Appl l1 + in + if fire_beta then !head_beta_reduce ~upto t + else t | C.Prod (n,s,t) as orig -> let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index c87dd6638..6baaeda03 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -27,3 +27,6 @@ val fold: val map: (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term + +val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit + diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 6779667d9..1cd2e54b9 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -23,12 +23,9 @@ let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -*) - let pp _ = ();; @@ -111,7 +108,7 @@ let rec typeof hdb | _ -> pp (lazy ( (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^ - (NCicPp.ppterm ~metasenv ~subst ~context expty))); + (NCicPp.ppterm ~metasenv ~subst:[] ~context expty))); try let metasenv, subst = NCicUnification.unify hdb metasenv subst context infty expty @@ -127,7 +124,9 @@ let rec typeof hdb fun t as orig -> (*D*)inside 'R'; try let rc = pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t)); - pp (lazy (NCicPp.ppmetasenv ~subst metasenv)); + pp (lazy (if expty = None then "NONE" else "SOME")); + if (List.exists (fun (i,_) -> i=29) subst) then + pp (lazy (NCicPp.ppsubst ~metasenv subst)); let metasenv, subst, t, infty = match t with | C.Rel n -> @@ -225,10 +224,17 @@ let rec typeof hdb let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty | C.Appl ((he as orig_he)::(_::_ as args)) -> + let upto = + match orig_he with C.Meta _ -> List.length args | _ -> 0 + in let metasenv, subst, he, ty_he = typeof_aux metasenv subst context None he in - eat_prods hdb ~localise ~look_for_coercion - metasenv subst context orig_he he ty_he args + let metasenv, subst, t, ty = + eat_prods hdb ~localise ~look_for_coercion + metasenv subst context orig_he he ty_he args + in + let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in + metasenv, subst, t, ty | 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 -> @@ -240,9 +246,19 @@ let rec typeof hdb let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in let metasenv, subst, term, _ = typeof_aux metasenv subst context (Some ind) term in + let parameters, arguments = HExtlib.split_nth leftno args in + let outtype = + match outtype with + | C.Implicit _ as ot -> + let rec aux = function + | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot) + | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl) + in + aux arguments + | _ -> outtype + in let metasenv, subst, outtype, outsort = typeof_aux metasenv subst context None outtype in - let parameters, arguments = HExtlib.split_nth leftno args in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let ind = if parameters = [] then C.Const r @@ -257,6 +273,14 @@ let rec typeof hdb if List.length pl <> constructorsno then raise (RefineFailure (lazy (localise orig, "Wrong number of cases in a match"))); +(* + let metasenv, subst = + match expty with + | None -> metasenv, subst + | Some expty -> + NCicUnification.unify hdb metasenv subst context resty expty + in +*) let _, metasenv, subst, pl_rev = List.fold_left (fun (j, metasenv, subst, branches) p -> @@ -278,12 +302,10 @@ let rec typeof hdb j+1, metasenv, subst, p :: branches) (1, metasenv, subst, []) pl in - metasenv, subst, - C.Match (r, outtype, term, List.rev pl_rev), - NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term])) - | C.Match _ as orig -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig); - assert false + let resty = C.Appl (outtype::arguments@[term]) in + let resty = NCicReduction.head_beta_reduce ~subst resty in + metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty + | C.Match _ as orig -> assert false in pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ NCicPp.ppterm ~metasenv ~subst ~context infty )); diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 918ada599..1aaecbe77 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -51,9 +51,11 @@ let index_hint hdb context t1 t2 = NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t | _ -> assert false) pair' context in +(* prerr_endline ("INDEXING: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data); +*) DB.index hdb src data ;; @@ -79,13 +81,12 @@ let add_user_provided_hint t = ;; let db () = - let combine f cmp l1 l2 = + let combine f l = List.flatten - (List.map - (fun u1 -> - HExtlib.filter_map - (fun u2 -> if cmp u1 u2 then None else Some (f u1 u2)) l2) - l1) + (let rec aux = function + | u1 :: tl -> List.map (f u1) tl :: aux tl + | [] -> [] + in aux l) in let mk_hint (u1,_,_) (u2,_,_) = let l = OCic2NCic.convert_obj u1 @@ -93,14 +94,14 @@ let db () = let r = OCic2NCic.convert_obj u2 (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in match List.hd l,List.hd r with - | (_,_,_,_,NCic.Constant (_,_,Some l,_,_)), - (_,_,_,_,NCic.Constant (_,_,Some r,_,_)) -> + | (_,h1,_,_,NCic.Constant (_,_,Some l,_,_)), + (_,h2,_,_,NCic.Constant (_,_,Some r,_,_)) -> let rec aux ctx t1 t2 = match t1, t2 with | NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) -> if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2 then aux ((n1, NCic.Decl s1) :: ctx) b1 b2 - else None + else [] | b1,b2 -> if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2 then begin @@ -109,26 +110,36 @@ let db () = ~context:ctx b1 ^ " === " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:ctx b2); *) - Some (ctx,b1,b2) - end else None + let rec mk_rels = + function 0 -> [] | n -> NCic.Rel n :: mk_rels (n-1) + in + let n1 = + NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri + u1 (NReference.Def h1)) :: mk_rels (List.length ctx)) + in + let n2 = + NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri + u2 (NReference.Def h2)) :: mk_rels (List.length ctx)) + in + [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2] + end else [] in aux [] l r - | _ -> None + | _ -> [] in let hints = List.fold_left (fun acc (_,_,l) -> acc @ if List.length l > 1 then - combine mk_hint (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l l + combine mk_hint l else []) [] (CoercDb.to_list ()) in List.fold_left (fun db -> function - | None -> db - | Some (ctx,b1,b2) -> index_hint db ctx b1 b2) - !user_db hints + | (ctx,b1,b2) -> index_hint db ctx b1 b2) + !user_db (List.flatten hints) ;; @@ -155,10 +166,21 @@ let look_for_hint hdb metasenv subst context t1 t2 = false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) (HintSet.elements candidates2) in + let rc = List.map (function | (true,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t1, t2 | (false,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t2, t1 | _ -> assert false) (candidates1 @ candidates2) + in +(* + List.iter + (fun (metasenv, t1, t2) -> + prerr_endline + ("CAND: "^NCicPp.ppterm ~metasenv ~subst ~context t1 ^ + " == "^NCicPp.ppterm ~metasenv ~subst ~context t2)) + rc; +*) + rc ;; diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 838fad9de..54b8218f5 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -29,10 +29,11 @@ let fail_exc metasenv subst context t1 t2 = " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); ;; -let mk_appl hd tl = - match hd with - | NCic.Appl l -> NCic.Appl (l@tl) - | _ -> NCic.Appl (hd :: tl) +let mk_appl ~upto hd tl = + NCicReduction.head_beta_reduce ~upto + (match hd with + | NCic.Appl l -> NCic.Appl (l@tl) + | _ -> NCic.Appl (hd :: tl)) ;; let flexible l = @@ -72,11 +73,9 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -*) let pp _ = ();; @@ -319,7 +318,8 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let term = NCicSubstitution.subst_meta lc term in unify hdb test_eq_only metasenv subst context term t with NCicUtils.Subst_not_found _-> - instantiate hdb test_eq_only metasenv subst context n lc t false) + instantiate hdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) false) | t, C.Meta (n,lc) -> (try @@ -327,17 +327,20 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let term = NCicSubstitution.subst_meta lc term in unify hdb test_eq_only metasenv subst context t term with NCicUtils.Subst_not_found _-> - instantiate hdb test_eq_only metasenv subst context n lc t true) + instantiate hdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) true) | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify hdb test_eq_only metasenv subst context (mk_appl term args) t2 + unify hdb test_eq_only metasenv subst context + (mk_appl ~upto:(List.length args) term args) t2 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify hdb test_eq_only metasenv subst context t1 (mk_appl term args) + unify hdb test_eq_only metasenv subst context t1 + (mk_appl ~upto:(List.length args) term args) | NCic.Appl (NCic.Meta (i,_)::_ as l1), NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> -- 2.39.2