From: Enrico Tassi Date: Tue, 10 Mar 2009 17:51:12 +0000 (+0000) Subject: unification hints almost ready X-Git-Tag: make_still_working~4165 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4573f1fecaf83f4706f39702555d5319d132477b;p=helm.git unification hints almost ready --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 474294495..d114d9322 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -150,14 +150,14 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 15 +let magic = 16 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) | Coercion of loc * 'term * bool (* add_obj *) * int (* arity *) * int (* saturations *) | PreferCoercion of loc * 'term - | UnificationHint of loc * 'term + | UnificationHint of loc * 'term * int (* term, precedence *) | Default of loc * string * UriManager.uri list | Drop of loc | Include of loc * string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 1fdc87b41..56ac59c7a 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -317,8 +317,8 @@ let pp_command ~term_pp ~obj_pp = function pp_coercion ~term_pp t do_composites i j | PreferCoercion (_,t) -> "prefer coercion " ^ term_pp t - | UnificationHint (_,t) -> - "unification hint " ^ term_pp t + | UnificationHint (_,t, n) -> + "unification hint " ^ string_of_int n ^ " " ^ term_pp t | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\"" diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index c6bebbc39..7f5327b56 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -470,9 +470,9 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = GrafiteAst.Coercion (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) -let eval_unification_hint status t = +let eval_unification_hint status t n = (* XXX no undo *) - NCicUnifHint.add_user_provided_hint t; + NCicUnifHint.add_user_provided_hint t n; status,[] ;; @@ -597,8 +597,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_prefer_coercion status coercion | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> eval_coercion status ~add_composites uri arity saturations - | GrafiteAst.UnificationHint (loc, t) -> - eval_unification_hint status t + | GrafiteAst.UnificationHint (loc, t, n) -> + eval_unification_hint status t n | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 32d666a38..23ec1770e 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -579,12 +579,12 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = OCic2NCic.clear (); let graph = match cic with - | Cic.CurrentProof (_,metasenv, _, ty,_,_) -> + | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) -> let _, ugraph = CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph in ugraph - | Cic.Constant (_,_, ty,_,_) -> + | Some (Cic.Constant (_,_, ty,_,_)) -> let _, ugraph = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in @@ -685,7 +685,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^ UriManager.string_of_uri uri ^"): " ^ string_of_float time); *) -(* try_new cic; *) +(* try_new (Some cic); *) let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in @@ -694,6 +694,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = with | Sys.Break as exn -> raise exn | exn -> +(* try_new None; *) raise exn ;; @@ -725,12 +726,12 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) - | GrafiteAst.UnificationHint (loc, t) -> + | GrafiteAst.UnificationHint (loc, t, n) -> let lexicon_status_ref = ref lexicon_status in let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref [] in let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t) + !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t,n) | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 44dec6d32..28d61d9e5 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -700,8 +700,8 @@ EXTEND (loc, t, composites, arity, saturations) | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> GrafiteAst.PreferCoercion (loc, t) - | IDENT "unification"; IDENT "hint"; t = tactic_term -> - GrafiteAst.UnificationHint (loc, t) + | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> + GrafiteAst.UnificationHint (loc, t, n) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index b49af2bbf..50a0c59da 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -304,7 +304,7 @@ let interpretate_term_and_interpretate_term_option in let cic_body = aux ~localize loc (cic_name :: context) body in NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) - | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false + | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed | CicNotationPt.Ident (name, subst) -> diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 1aaecbe77..dd58fa5c8 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -11,9 +11,9 @@ (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) -module COT : Set.OrderedType with type t = NCic.term = +module COT : Set.OrderedType with type t = int * NCic.term = struct - type t = NCic.term + type t = int * NCic.term let compare = Pervasives.compare end @@ -27,7 +27,7 @@ type db = DB.t let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");; let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;; -let index_hint hdb context t1 t2 = +let index_hint hdb context t1 t2 precedence = assert ( (match t1 with | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true) @@ -41,7 +41,7 @@ let index_hint hdb context t1 t2 = (fun t (n,e) -> match e with | NCic.Decl ty -> NCic.Prod (n,ty,t) - | _ -> assert false) + | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t)) pair' context in let src = List.fold_left @@ -49,21 +49,22 @@ let index_hint hdb context t1 t2 = match e with | NCic.Decl _ -> NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t - | _ -> assert false) + | NCic.Def _ -> + NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t) pair' context in (* prerr_endline ("INDEXING: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data); *) - DB.index hdb src data + DB.index hdb src (precedence, data) ;; let empty_db = DB.empty ;; let user_db = ref empty_db ;; -let add_user_provided_hint t = +let add_user_provided_hint t precedence = let u = UriManager.uri_of_string "cic:/foo/bar.con" in let c, a, b = let rec aux ctx = function @@ -73,11 +74,13 @@ let add_user_provided_hint t = | _ -> assert false) | NCic.Prod (n,s,t) -> aux ((n, NCic.Decl s) :: ctx) t + | NCic.LetIn (n,ty,t,b) -> + aux ((n, NCic.Def (t,ty)) :: ctx) b | _ -> assert false in aux [] (fst (OCic2NCic.convert_term u t)) in - user_db := index_hint !user_db c a b + user_db := index_hint !user_db c a b precedence ;; let db () = @@ -138,7 +141,7 @@ let db () = in List.fold_left (fun db -> function - | (ctx,b1,b2) -> index_hint db ctx b1 b2) + | (ctx,b1,b2) -> index_hint db ctx b1 b2 0) !user_db (List.flatten hints) ;; @@ -157,23 +160,27 @@ let look_for_hint hdb metasenv subst context t1 t2 = let candidates1 = DB.retrieve_unifiables hdb (pair t1 t2) in let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in let candidates1 = - List.map (fun ty -> - true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) + List.map (fun (prec,ty) -> + prec,true,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) (HintSet.elements candidates1) in let candidates2 = - List.map (fun ty -> - false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0) + List.map (fun (prec,ty) -> + prec,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 + | (prec,true,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t1, t2 + | (prec,false,(NCic.Appl [_; t1; t2],metasenv,_)) -> prec,metasenv, t2, t1 | _ -> assert false) (candidates1 @ candidates2) in + let rc = + List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc + in + let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in (* List.iter (fun (metasenv, t1, t2) -> diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 2e94d9c8d..076ac2f62 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -14,11 +14,11 @@ type db val index_hint: - db -> NCic.context -> NCic.term -> NCic.term -> db + db -> NCic.context -> NCic.term -> NCic.term -> int -> db (* gets the old imperative coercion DB *) val db : unit -> db -val add_user_provided_hint : Cic.term -> unit +val add_user_provided_hint : Cic.term -> int -> unit val empty_db : db diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 54b8218f5..79fe81053 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -442,18 +442,32 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = (*D*) in outside(); rc with exn -> outside (); raise exn in let try_hints metasenv subst t1 t2 (* exc*) = +(* + prerr_endline ("\n\n\n looking for hints for : " ^ + NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); +*) let candidates = NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 in let rec cand_iter = function | [] -> None (* raise exc *) | (metasenv,c1,c2)::tl -> +(* + prerr_endline ("\n attempt: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ + NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " AND " ^ + NCicPp.ppterm ~metasenv ~subst ~context c2 ^ " ==?== " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); +*) try - let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in - let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in + let metasenv,subst = unify hdb test_eq_only metasenv subst context t1 c1 in + let metasenv,subst = unify hdb test_eq_only metasenv subst context c2 t2 in Some (metasenv, subst) with - UnificationFailure _ | Uncertain _ -> cand_iter tl + UnificationFailure _ | Uncertain _ -> + prerr_endline (" outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 - with UnificationFailure msg | Uncertain msg as exn -> + with + | UnificationFailure msg as exn -> + (try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn) + | Uncertain msg as exn -> match try_hints metasenv subst t1 t2 with | Some x -> x | None ->