From c5b3da2ed2b2dafd22cc50edb4ac5f1d402dfa94 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Sep 2008 10:15:31 +0000 Subject: [PATCH] ... --- helm/software/components/ng_refiner/.depend | 4 + .../components/ng_refiner/.depend.opt | 4 + helm/software/components/ng_refiner/Makefile | 4 +- .../components/ng_refiner/nCicMetaSubst.ml | 930 +++++++++++++++++ .../components/ng_refiner/nCicMetaSubst.mli | 90 ++ .../components/ng_refiner/nCicUnification.ml | 951 ++++++++++++++++++ .../components/ng_refiner/nCicUnification.mli | 48 + 7 files changed, 2030 insertions(+), 1 deletion(-) create mode 100644 helm/software/components/ng_refiner/nCicMetaSubst.ml create mode 100644 helm/software/components/ng_refiner/nCicMetaSubst.mli create mode 100644 helm/software/components/ng_refiner/nCicUnification.ml create mode 100644 helm/software/components/ng_refiner/nCicUnification.mli diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 3d4d37787..1bedd90f6 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,2 +1,6 @@ +nCicMetaSubst.cmo: nCicMetaSubst.cmi +nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicUnification.cmo: nCicUnification.cmi +nCicUnification.cmx: nCicUnification.cmi nCicRefiner.cmo: nCicRefiner.cmi nCicRefiner.cmx: nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt index 3d4d37787..1bedd90f6 100644 --- a/helm/software/components/ng_refiner/.depend.opt +++ b/helm/software/components/ng_refiner/.depend.opt @@ -1,2 +1,6 @@ +nCicMetaSubst.cmo: nCicMetaSubst.cmi +nCicMetaSubst.cmx: nCicMetaSubst.cmi +nCicUnification.cmo: nCicUnification.cmi +nCicUnification.cmx: nCicUnification.cmi nCicRefiner.cmo: nCicRefiner.cmi nCicRefiner.cmx: nCicRefiner.cmi diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 099978755..33a66bd8c 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -2,7 +2,9 @@ PACKAGE = ng_refiner PREDICATES = INTERFACE_FILES = \ - nCicRefiner.mli + nCicMetaSubst.mli \ + nCicUnification.mli \ + nCicRefiner.mli \ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml new file mode 100644 index 000000000..4441fa169 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -0,0 +1,930 @@ +(* + ||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$ *) + + +(*open Printf + +(* PROFILING *) +(* +let deref_counter = ref 0 +let apply_subst_context_counter = ref 0 +let apply_subst_metasenv_counter = ref 0 +let lift_counter = ref 0 +let subst_counter = ref 0 +let whd_counter = ref 0 +let are_convertible_counter = ref 0 +let metasenv_length = ref 0 +let context_length = ref 0 +let reset_counters () = + apply_subst_counter := 0; + apply_subst_context_counter := 0; + apply_subst_metasenv_counter := 0; + lift_counter := 0; + subst_counter := 0; + whd_counter := 0; + are_convertible_counter := 0; + metasenv_length := 0; + context_length := 0 +let print_counters () = + debug_print (lazy (Printf.sprintf +"apply_subst: %d +apply_subst_context: %d +apply_subst_metasenv: %d +lift: %d +subst: %d +whd: %d +are_convertible: %d +metasenv length: %d (avg = %.2f) +context length: %d (avg = %.2f) +" + !apply_subst_counter !apply_subst_context_counter + !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter + !are_convertible_counter !metasenv_length + ((float !metasenv_length) /. (float !apply_subst_metasenv_counter)) + !context_length + ((float !context_length) /. (float !apply_subst_context_counter)) + ))*) + + + +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t +exception DeliftingARelWouldCaptureAFreeVariable;; + +let debug_print = fun _ -> () + +type substitution = (int * (Cic.context * Cic.term)) list + +(* +let rec deref subst = + let third _,_,a = a in + function + Cic.Meta(n,l) as t -> + (try + deref subst + (CicSubstitution.subst_meta + l (third (CicUtil.lookup_subst n subst))) + with + CicUtil.Subst_not_found _ -> t) + | t -> t +;; +*) + +let lookup_subst = CicUtil.lookup_subst +;; + +(* clean_up_meta take a metasenv and a term and make every local context +of each occurrence of a metavariable consistent with its canonical context, +with respect to the hidden hipothesis *) + +(* +let clean_up_meta subst metasenv t = + let module C = Cic in + let rec aux t = + match t with + C.Rel _ + | C.Sort _ -> t + | C.Implicit _ -> assert false + | C.Meta (n,l) as t -> + let cc = + (try + let (cc,_) = lookup_subst n subst in cc + with CicUtil.Subst_not_found _ -> + try + let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc + with CicUtil.Meta_not_found _ -> assert false) in + let l' = + (try + List.map2 + (fun t1 t2 -> + match t1,t2 with + None , _ -> None + | _ , t -> t) cc l + with + Invalid_argument _ -> assert false) in + C.Meta (n, l') + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest) + | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest) + | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) + | C.Appl l -> C.Appl (List.map aux l) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst + in + C.Var (uri, exp_named_subst') + | C.Const (uri, exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst + in + C.Const (uri, exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst + in + C.MutInd (uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst + in + C.MutConstruct (uri, tyno, consno, exp_named_subst') + | C.MutCase (uri,tyno,out,te,pl) -> + C.MutCase (uri, tyno, aux out, aux te, List.map aux pl) + | C.Fix (i,fl) -> + let fl' = + List.map + (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl + in + C.Fix (i, fl') + | C.CoFix (i,fl) -> + let fl' = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl + in + C.CoFix (i, fl') + in + aux t *) + +(*** Functions to apply a substitution ***) + +let apply_subst_gen ~appl_fun subst term = + let rec um_aux = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst + in + C.Var (uri, exp_named_subst') + | C.Meta (i, l) -> + (try + let (_, t,_) = lookup_subst i subst in + um_aux (S.subst_meta l t) + with CicUtil.Subst_not_found _ -> + (* unconstrained variable, i.e. free in subst*) + let l' = + List.map (function None -> None | Some t -> Some (um_aux t)) l + in + C.Meta (i,l')) + | C.Sort _ + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) + | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t) + | C.Appl (hd :: tl) -> appl_fun um_aux hd tl + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst + in + C.Const (uri, exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + let pl' = List.map um_aux pl in + C.MutCase (sp, i, um_aux outty, um_aux t, pl') + | C.Fix (i, fl) -> + let fl' = + List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl + in + C.Fix (i, fl') + | C.CoFix (i, fl) -> + let fl' = + List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl + in + C.CoFix (i, fl') + in + um_aux term +;; + +let apply_subst = + let appl_fun um_aux he tl = + let tl' = List.map um_aux tl in + let t' = + match um_aux he with + Cic.Appl l -> Cic.Appl (l@tl') + | he' -> Cic.Appl (he'::tl') + in + begin + match he with + Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' + | _ -> t' + end + in + fun subst t -> +(* incr apply_subst_counter; *) +match subst with + [] -> t + | _ -> apply_subst_gen ~appl_fun subst t +;; + +let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" +let apply_subst s t = + profiler.HExtlib.profile (apply_subst s) t + + +let apply_subst_context subst context = + match subst with + [] -> context + | _ -> +(* + incr apply_subst_context_counter; + context_length := !context_length + List.length context; +*) + List.fold_right + (fun item context -> + match item with + | Some (n, Cic.Decl t) -> + let t' = apply_subst subst t in + Some (n, Cic.Decl t') :: context + | Some (n, Cic.Def (t, ty)) -> + let ty' = apply_subst subst ty in + let t' = apply_subst subst t in + Some (n, Cic.Def (t', ty')) :: context + | None -> None :: context) + context [] + +let apply_subst_metasenv subst metasenv = +(* + incr apply_subst_metasenv_counter; + metasenv_length := !metasenv_length + List.length metasenv; +*) +match subst with + [] -> metasenv + | _ -> + List.map + (fun (n, context, ty) -> + (n, apply_subst_context subst context, apply_subst subst ty)) + (List.filter + (fun (i, _, _) -> not (List.mem_assoc i subst)) + metasenv) + +(***** Pretty printing functions ******) + +let ppterm ~metasenv subst term = + CicPp.ppterm ~metasenv (apply_subst subst term) + +let ppterm_in_name_context ~metasenv subst term name_context = + CicPp.pp ~metasenv (apply_subst subst term) name_context + +let ppterm_in_context ~metasenv subst term context = + let name_context = + List.map (function None -> None | Some (n,_) -> Some n) context + in + ppterm_in_name_context ~metasenv subst term name_context + +let ppterm_in_context_ref = ref ppterm_in_context +let set_ppterm_in_context f = + ppterm_in_context_ref := f +let use_low_level_ppterm_in_context = ref false + +let ppterm_in_context ~metasenv subst term context = + if !use_low_level_ppterm_in_context then + ppterm_in_context ~metasenv subst term context + else + !ppterm_in_context_ref ~metasenv subst term context + +let ppcontext' ~metasenv ?(sep = "\n") subst context = + let separate s = if s = "" then "" else s ^ sep in + List.fold_right + (fun context_entry (i,name_context) -> + match context_entry with + Some (n,Cic.Decl t) -> + sprintf "%s%s : %s" (separate i) (CicPp.ppname n) + (ppterm_in_name_context ~metasenv subst t name_context), + (Some n)::name_context + | Some (n,Cic.Def (bo,ty)) -> + sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) + (ppterm_in_name_context ~metasenv subst ty name_context) + (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context + | None -> + sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[]) + +let ppsubst_unfolded ~metasenv subst = + String.concat "\n" + (List.map + (fun (idx, (c, t,ty)) -> + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in + sprintf "%s |- ?%d : %s := %s" context idx +(ppterm_in_name_context ~metasenv [] ty name_context) + (ppterm_in_name_context ~metasenv subst t name_context)) + subst) +(* + Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) + subst) *) +;; + +let ppsubst ~metasenv subst = + String.concat "\n" + (List.map + (fun (idx, (c, t, ty)) -> + let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in + sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty name_context) + (ppterm_in_name_context ~metasenv [] t name_context)) + subst) +;; + +let ppcontext ~metasenv ?sep subst context = + fst (ppcontext' ~metasenv ?sep subst context) + +let ppmetasenv ?(sep = "\n") subst metasenv = + String.concat sep + (List.map + (fun (i, c, t) -> + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in + sprintf "%s |- ?%d: %s" context i + (ppterm_in_name_context ~metasenv subst t name_context)) + (List.filter + (fun (i, _, _) -> not (List.mem_assoc i subst)) + metasenv)) + +let tempi_type_of_aux_subst = ref 0.0;; +let tempi_subst = ref 0.0;; +let tempi_type_of_aux = ref 0.0;; + +(**** DELIFT ****) +(* the delift function takes in input a metavariable index, an ordered list of + * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some + * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit + * substitution that is applied to a metavariable occurrence and the result of + * the delift function is a term the implicit variable can be substituted with + * to make the term [t] unifiable with the metavariable occurrence. In general, + * the problem is undecidable if we consider equivalence in place of alpha + * convertibility. Our implementation, though, is even weaker than alpha + * convertibility, since it replace the term [tk] if and only if [tk] is a Rel + * (missing all the other cases). Does this matter in practice? + * The metavariable index is the index of the metavariable that must not occur + * in the term (for occur check). + *) + +exception NotInTheList;; + +let position n = + let rec aux k = + function + [] -> raise NotInTheList + | (Some (Cic.Rel m))::_ when m=n -> k + | _::tl -> aux (k+1) tl in + aux 1 +;; + +exception Occur;; + +let rec force_does_not_occur subst to_be_restricted t = + let module C = Cic in + let more_to_be_restricted = ref [] in + let rec aux k = function + C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur + | C.Rel _ + | C.Sort _ as t -> t + | C.Implicit _ -> assert false + | C.Meta (n, l) -> + (* we do not retrieve the term associated to ?n in subst since *) + (* in this way we can restrict if something goes wrong *) + let l' = + let i = ref 0 in + List.map + (function t -> + incr i ; + match t with + None -> None + | Some t -> + try + Some (aux k t) + with Occur -> + more_to_be_restricted := (n,!i) :: !more_to_be_restricted; + None) + l + in + C.Meta (n, l') + | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) + | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest) + | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest) + | C.LetIn (name,so,ty,dest) -> + C.LetIn (name, aux k so, aux k ty, aux (k+1) dest) + | C.Appl l -> C.Appl (List.map (aux k) l) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst + in + C.Var (uri, exp_named_subst') + | C.Const (uri, exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst + in + C.Const (uri, exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst + in + C.MutInd (uri, tyno, exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst + in + C.MutConstruct (uri, tyno, consno, exp_named_subst') + | C.MutCase (uri,tyno,out,te,pl) -> + C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let k_plus_len = k + len in + let fl' = + List.map + (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl + in + C.Fix (i, fl') + | C.CoFix (i,fl) -> + let len = List.length fl in + let k_plus_len = k + len in + let fl' = + List.map + (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl + in + C.CoFix (i, fl') + in + let res = aux 0 t in + (!more_to_be_restricted, res) + +let rec restrict subst to_be_restricted metasenv = + match to_be_restricted with + | [] -> metasenv, subst + | _ -> + let names_of_context_indexes context indexes = + String.concat ", " + (List.map + (fun i -> + try + match List.nth context (i-1) with + | None -> assert false + | Some (n, _) -> CicPp.ppname n + with + Failure _ -> assert false + ) indexes) + in + let force_does_not_occur_in_context to_be_restricted = function + | None -> [], None + | Some (name, Cic.Decl t) -> + let (more_to_be_restricted, t') = + force_does_not_occur subst to_be_restricted t + in + more_to_be_restricted, Some (name, Cic.Decl t') + | Some (name, Cic.Def (bo, ty)) -> + let (more_to_be_restricted, bo') = + force_does_not_occur subst to_be_restricted bo + in + let more_to_be_restricted, ty' = + let more_to_be_restricted', ty' = + force_does_not_occur subst to_be_restricted ty + in + more_to_be_restricted @ more_to_be_restricted', + ty' + in + more_to_be_restricted, Some (name, Cic.Def (bo', ty')) + in + let rec erase i to_be_restricted n = function + | [] -> [], to_be_restricted, [] + | hd::tl -> + let more_to_be_restricted,restricted,tl' = + erase (i+1) to_be_restricted n tl + in + let restrict_me = List.mem i restricted in + if restrict_me then + more_to_be_restricted, restricted, None:: tl' + else + (try + let more_to_be_restricted', hd' = + let delifted_restricted = + let rec aux = + function + [] -> [] + | j::tl when j > i -> (j - i)::aux tl + | _::tl -> aux tl + in + aux restricted + in + force_does_not_occur_in_context delifted_restricted hd + in + more_to_be_restricted @ more_to_be_restricted', + restricted, hd' :: tl' + with Occur -> + more_to_be_restricted, (i :: restricted), None :: tl') + in + let (more_to_be_restricted, metasenv) = (* restrict metasenv *) + List.fold_right + (fun (n, context, t) (more, metasenv) -> + let to_be_restricted = + List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) + in + let (more_to_be_restricted, restricted, context') = + (* just an optimization *) + if to_be_restricted = [] then + [],[],context + else + erase 1 to_be_restricted n context + in + try + let more_to_be_restricted', t' = + force_does_not_occur subst restricted t + in + let metasenv' = (n, context', t') :: metasenv in + (more @ more_to_be_restricted @ more_to_be_restricted', + metasenv') + with Occur -> + raise (MetaSubstFailure (lazy (sprintf + "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" + n (names_of_context_indexes context to_be_restricted))))) + metasenv ([], []) + in + let (more_to_be_restricted', subst) = (* restrict subst *) + List.fold_right + (* TODO: cambiare dopo l'aggiunta del ty *) + (fun (n, (context, term,ty)) (more, subst') -> + let to_be_restricted = + List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) + in + (try + let (more_to_be_restricted, restricted, context') = + (* just an optimization *) + if to_be_restricted = [] then + [], [], context + else + erase 1 to_be_restricted n context + in + let more_to_be_restricted', term' = + force_does_not_occur subst restricted term + in + let more_to_be_restricted'', ty' = + force_does_not_occur subst restricted ty in + let subst' = (n, (context', term',ty')) :: subst' in + let more = + more @ more_to_be_restricted + @ more_to_be_restricted'@more_to_be_restricted'' in + (more, subst') + with Occur -> + let error_msg = lazy (sprintf + "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" + n (names_of_context_indexes context to_be_restricted) n + (ppterm ~metasenv subst term)) + in + (* DEBUG + debug_print (lazy error_msg); + debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); + debug_print (lazy ("subst = \n" ^ (ppsubst subst))); + debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) + raise (MetaSubstFailure error_msg))) + subst ([], []) + in + restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv +;; + +(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*) + +let delift n subst context metasenv l t = +(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), + otherwise the occur check does not make sense *) + +(* + debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto + al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))))); +*) + + let module S = CicSubstitution in + let l = + let (_, canonical_context, _) = + try + CicUtil.lookup_meta n metasenv + with CicUtil.Meta_not_found _ -> + raise (MetaSubstFailure (lazy + ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^ + "declared in the metasenv"))) + in + List.map2 (fun ct lt -> + match (ct, lt) with + | None, _ -> None + | Some _, _ -> lt) + canonical_context l + in + let to_be_restricted = ref [] in + let rec deliftaux k = + let module C = Cic in + function + | C.Rel m as t-> + if m <=k then + t + else + (try + match List.nth context (m-k-1) with + Some (_,C.Def (t,_)) -> + (try + C.Rel ((position (m-k) l) + k) + with + NotInTheList -> + (*CSC: Hmmm. This bit of reduction is not in the spirit of *) + (*CSC: first order unification. Does it help or does it harm? *) + (*CSC: ANSWER: it hurts performances since it is possible to *) + (*CSC: have an exponential explosion of the size of the proof.*) + (*CSC: However, without this bit of reduction some "apply" in *) + (*CSC: the library fail (e.g. nat/nth_prime.ma). *) + deliftaux k (S.lift m t)) + | Some (_,C.Decl t) -> + C.Rel ((position (m-k) l) + k) + | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) + with + Failure _ -> + raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) + ) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i, l1) as t -> + (try + let (_,t,_) = CicUtil.lookup_subst i subst in + deliftaux k (CicSubstitution.subst_meta l1 t) + with CicUtil.Subst_not_found _ -> + (* see the top level invariant *) + if (i = n) then + raise (MetaSubstFailure (lazy (sprintf + "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" + i (ppterm ~metasenv subst t)))) + else + begin + (* I do not consider the term associated to ?i in subst since *) + (* in this way I can restrict if something goes wrong. *) + let rec deliftl j = + function + [] -> [] + | None::tl -> None::(deliftl (j+1) tl) + | (Some t)::tl -> + let l1' = (deliftl (j+1) tl) in + try + Some (deliftaux k t)::l1' + with + NotInTheList + | MetaSubstFailure _ -> + to_be_restricted := + (i,j)::!to_be_restricted ; None::l1' + in + let l' = deliftl 1 l1 in + C.Meta(i,l') + end) + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (deliftaux k) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, deliftaux k outty, deliftaux k t, + List.map (deliftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> + (name, i, deliftaux k ty, deliftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + let res = + try + deliftaux 0 t + with + NotInTheList -> + (* This is the case where we fail even first order unification. *) + (* The reason is that our delift function is weaker than first *) + (* order (in the sense of alpha-conversion). See comment above *) + (* related to the delift function. *) +(* debug_print (lazy "First Order UnificationFailure during delift") ; +debug_print(lazy (sprintf + "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" + (ppterm subst t) + (String.concat "; " + (List.map + (function Some t -> ppterm subst t | None -> "_") l + )))); *) + let msg = (lazy (sprintf + "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" + (ppterm ~metasenv subst t) + (String.concat "; " + (List.map + (function Some t -> ppterm ~metasenv subst t | None -> "_") + l)))) + in + if + List.exists + (function + Some t -> CicUtil.is_meta_closed (apply_subst subst t) + | None -> true) l + then + raise (Uncertain msg) + else + raise (MetaSubstFailure msg) + in + let (metasenv, subst) = restrict subst !to_be_restricted metasenv in + res, metasenv, subst +;; + +(* delifts a term t of n levels strating from k, that is changes (Rel m) + * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails + *) +let delift_rels_from subst metasenv k n = + let rec liftaux subst metasenv k = + let module C = Cic in + function + C.Rel m as t -> + if m < k then + t, subst, metasenv + else if m < k + n then + raise DeliftingARelWouldCaptureAFreeVariable + else + C.Rel (m - n), subst, metasenv + | C.Var (uri,exp_named_subst) -> + let exp_named_subst',subst,metasenv = + List.fold_right + (fun (uri,t) (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) + in + C.Var (uri,exp_named_subst'),subst,metasenv + | C.Meta (i,l) -> + (try + let (_, t,_) = lookup_subst i subst in + liftaux subst metasenv k (CicSubstitution.subst_meta l t) + with CicUtil.Subst_not_found _ -> + let l',to_be_restricted,subst,metasenv = + let rec aux con l subst metasenv = + match l with + [] -> [],[],subst,metasenv + | he::tl -> + let tl',to_be_restricted,subst,metasenv = + aux (con + 1) tl subst metasenv in + let he',more_to_be_restricted,subst,metasenv = + match he with + None -> None,[],subst,metasenv + | Some t -> + try + let t',subst,metasenv = liftaux subst metasenv k t in + Some t',[],subst,metasenv + with + DeliftingARelWouldCaptureAFreeVariable -> + None,[i,con],subst,metasenv + in + he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv + in + aux 1 l subst metasenv in + let metasenv,subst = restrict subst to_be_restricted metasenv in + C.Meta(i,l'),subst,metasenv) + | C.Sort _ as t -> t,subst,metasenv + | C.Implicit _ as t -> t,subst,metasenv + | C.Cast (te,ty) -> + let te',subst,metasenv = liftaux subst metasenv k te in + let ty',subst,metasenv = liftaux subst metasenv k ty in + C.Cast (te',ty'),subst,metasenv + | C.Prod (n,s,t) -> + let s',subst,metasenv = liftaux subst metasenv k s in + let t',subst,metasenv = liftaux subst metasenv (k+1) t in + C.Prod (n,s',t'),subst,metasenv + | C.Lambda (n,s,t) -> + let s',subst,metasenv = liftaux subst metasenv k s in + let t',subst,metasenv = liftaux subst metasenv (k+1) t in + C.Lambda (n,s',t'),subst,metasenv + | C.LetIn (n,s,ty,t) -> + let s',subst,metasenv = liftaux subst metasenv k s in + let ty',subst,metasenv = liftaux subst metasenv k ty in + let t',subst,metasenv = liftaux subst metasenv (k+1) t in + C.LetIn (n,s',ty',t'),subst,metasenv + | C.Appl l -> + let l',subst,metasenv = + List.fold_right + (fun t (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + t'::l,subst,metasenv) l ([],subst,metasenv) in + C.Appl l',subst,metasenv + | C.Const (uri,exp_named_subst) -> + let exp_named_subst',subst,metasenv = + List.fold_right + (fun (uri,t) (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) + in + C.Const (uri,exp_named_subst'),subst,metasenv + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst',subst,metasenv = + List.fold_right + (fun (uri,t) (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) + in + C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst',subst,metasenv = + List.fold_right + (fun (uri,t) (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) + in + C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv + | C.MutCase (sp,i,outty,t,pl) -> + let outty',subst,metasenv = liftaux subst metasenv k outty in + let t',subst,metasenv = liftaux subst metasenv k t in + let pl',subst,metasenv = + List.fold_right + (fun t (l,subst,metasenv) -> + let t',subst,metasenv = liftaux subst metasenv k t in + t'::l,subst,metasenv) pl ([],subst,metasenv) + in + C.MutCase (sp,i,outty',t',pl'),subst,metasenv + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl,subst,metasenv = + List.fold_right + (fun (name, i, ty, bo) (l,subst,metasenv) -> + let ty',subst,metasenv = liftaux subst metasenv k ty in + let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in + (name,i,ty',bo')::l,subst,metasenv + ) fl ([],subst,metasenv) + in + C.Fix (i, liftedfl),subst,metasenv + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl,subst,metasenv = + List.fold_right + (fun (name, ty, bo) (l,subst,metasenv) -> + let ty',subst,metasenv = liftaux subst metasenv k ty in + let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in + (name,ty',bo')::l,subst,metasenv + ) fl ([],subst,metasenv) + in + C.CoFix (i, liftedfl),subst,metasenv + in + liftaux subst metasenv k + +let delift_rels subst metasenv n t = + delift_rels_from subst metasenv 1 n t + + +(**** END OF DELIFT ****) + + +(** {2 Format-like pretty printers} *) + +let fpp_gen ppf s = + Format.pp_print_string ppf s; + Format.pp_print_newline ppf (); + Format.pp_print_flush ppf () + +let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) +let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) +let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) +*) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli new file mode 100644 index 000000000..e03180564 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -0,0 +1,90 @@ +(* + ||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$ *) + +(* + +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t +exception DeliftingARelWouldCaptureAFreeVariable;; + +(* The entry (i,t) in a substitution means that *) +(* (META i) have been instantiated with t. *) +(* type substitution = (int * (Cic.context * Cic.term)) list *) + + (** @raise SubstNotFound *) + +(* apply_subst subst t *) +(* applies the substitution [subst] to [t] *) +(* [subst] must be already unwinded *) + +val apply_subst : Cic.substitution -> Cic.term -> Cic.term +val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context +val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv + +(*** delifting ***) + +val delift : + int -> Cic.substitution -> Cic.context -> Cic.metasenv -> + (Cic.term option) list -> Cic.term -> + Cic.term * Cic.metasenv * Cic.substitution +val restrict : + Cic.substitution -> (int * int) list -> Cic.metasenv -> + Cic.metasenv * Cic.substitution + +(** delifts the Rels in t of n + * @raise DeliftingARelWouldCaptureAFreeVariable + *) +val delift_rels : + Cic.substitution -> Cic.metasenv -> int -> Cic.term -> + Cic.term * Cic.substitution * Cic.metasenv + +(** {2 Pretty printers} *) +val use_low_level_ppterm_in_context : bool ref +val set_ppterm_in_context : + (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> + string) -> unit + +val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string +val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string +val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string +val ppcontext: + metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context -> + string +val ppterm_in_name_context: + metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> + (Cic.name option) list -> string +val ppterm_in_context: + metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string +val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string + +(** {2 Format-like pretty printers} + * As above with prototypes suitable for toplevel/ocamldebug printers. No + * subsitutions are applied here since such printers are required to be invoked + * with only one argument. + *) + +val fppsubst: Format.formatter -> Cic.substitution -> unit +val fppterm: Format.formatter -> Cic.term -> unit +val fppmetasenv: Format.formatter -> Cic.metasenv -> unit + +(* +(* DEBUG *) +val print_counters: unit -> unit +val reset_counters: unit -> unit +*) + +(* val clean_up_meta : + Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term +*) +*) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml new file mode 100644 index 000000000..2643ce843 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -0,0 +1,951 @@ +(* + ||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$ *) +(* + +open Printf + +exception UnificationFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; + +let verbose = false;; +let debug_print = fun _ -> () + +let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" +let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" +let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" +let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" + +let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'" + +let type_of_aux' metasenv subst context term ugraph = +let foo () = + try + profile.HExtlib.profile + (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph + with + CicTypeChecker.TypeCheckerFailure msg -> + let msg = + lazy + (sprintf + "Kernel Type checking error: +%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in + raise (AssertFailure msg) + | CicTypeChecker.AssertFailure msg -> + let msg = lazy + (sprintf + "Kernel Type checking assertion failure: +%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in + raise (AssertFailure msg) +in profiler_toa.HExtlib.profile foo () +;; + +let exists_a_meta l = + List.exists + (function + | Cic.Meta _ + | Cic.Appl (Cic.Meta _::_) -> true + | _ -> false) l + +let rec deref subst t = + let snd (_,a,_) = a in + match t with + Cic.Meta(n,l) -> + (try + deref subst + (CicSubstitution.subst_meta + l (snd (CicUtil.lookup_subst n subst))) + with + CicUtil.Subst_not_found _ -> t) + | Cic.Appl(Cic.Meta(n,l)::args) -> + (match deref subst (Cic.Meta(n,l)) with + | Cic.Lambda _ as t -> + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) + | r -> Cic.Appl(r::args)) + | Cic.Appl(((Cic.Lambda _) as t)::args) -> + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) + | t -> t +;; + +let deref subst t = + let foo () = deref subst t + in profiler_deref.HExtlib.profile foo () + +exception WrongShape;; +let eta_reduce after_beta_expansion after_beta_expansion_body + before_beta_expansion + = + try + match before_beta_expansion,after_beta_expansion_body with + Cic.Appl l, Cic.Appl l' -> + let rec all_but_last check_last = + function + [] -> assert false + | [Cic.Rel 1] -> [] + | [_] -> if check_last then raise WrongShape else [] + | he::tl -> he::(all_but_last check_last tl) + in + let all_but_last check_last l = + match all_but_last check_last l with + [] -> assert false + | [he] -> he + | l -> Cic.Appl l + in + let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in + let all_but_last = all_but_last false l in + (* here we should test alpha-equivalence; however we know by + construction that here alpha_equivalence is equivalent to = *) + if t = all_but_last then + all_but_last + else + after_beta_expansion + | _,_ -> after_beta_expansion + with + WrongShape -> after_beta_expansion + +let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = + let module S = CicSubstitution in + let module C = Cic in +let foo () = + let rec aux metasenv subst n context t' ugraph = + try + + let subst,metasenv,ugraph1 = + fo_unif_subst test_equality_only subst context metasenv + (CicSubstitution.lift n arg) t' ugraph + + in + subst,metasenv,C.Rel (1 + n),ugraph1 + with + Uncertain _ + | UnificationFailure _ -> + match t' with + | C.Rel m -> subst,metasenv, + (if m <= n then C.Rel m else C.Rel (m+1)),ugraph + | C.Var (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 + | C.Meta (i,l) -> + (* andrea: in general, beta_expand can create badly typed + terms. This happens quite seldom in practice, UNLESS we + iterate on the local context. For this reason, we renounce + to iterate and just lift *) + let l = + List.map + (function + Some t -> Some (CicSubstitution.lift 1 t) + | None -> None) l in + subst, metasenv, C.Meta (i,l), ugraph + | C.Sort _ + | C.Implicit _ as t -> subst,metasenv,t,ugraph + | C.Cast (te,ty) -> + let subst,metasenv,te',ugraph1 = + aux metasenv subst n context te ugraph in + let subst,metasenv,ty',ugraph2 = + aux metasenv subst n context ty ugraph1 in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Cast (te', ty')),ugraph2 + | C.Prod (nn,s,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Prod (nn, s', t')),ugraph2 + | C.Lambda (nn,s,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 + | C.LetIn (nn,s,ty,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,ty',ugraph1 = + aux metasenv subst n context ty ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t + ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 + | C.Appl l -> + let subst,metasenv,revl',ugraph1 = + List.fold_left + (fun (subst,metasenv,appl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::appl),ugraph1 + ) (subst,metasenv,[],ugraph) l + in + subst,metasenv,(C.Appl (List.rev revl')),ugraph1 + | C.Const (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 + | C.MutInd (uri,i,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 + | C.MutCase (sp,i,outt,t,pl) -> + let subst,metasenv,outt',ugraph1 = + aux metasenv subst n context outt ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst n context t ugraph1 in + let subst,metasenv,revpl',ugraph3 = + List.fold_left + (fun (subst,metasenv,pl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::pl),ugraph1 + ) (subst,metasenv,[],ugraph2) pl + in + subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 + (* TASSI: not sure this is serial *) + | C.Fix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) +*) + subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph + | C.CoFix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) + +*) + subst,metasenv,(CicSubstitution.lift 1 t'), ugraph + + and aux_exp_named_subst metasenv subst n context ens ugraph = + List.fold_right + (fun (uri,t) (subst,metasenv,l,ugraph) -> + let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in + subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) + in + let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in + let fresh_name = + FreshNamesGenerator.mk_fresh_name ~subst + metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty + in + let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in + let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in + subst, metasenv, t'', ugraph2 +in profiler_beta_expand.HExtlib.profile foo () + + +and beta_expand_many test_equality_only metasenv subst context t args ugraph = + let _,subst,metasenv,hd,ugraph = + List.fold_right + (fun arg (num,subst,metasenv,t,ugraph) -> + let subst,metasenv,t,ugraph1 = + beta_expand num test_equality_only + metasenv subst context t arg ugraph + in + num+1,subst,metasenv,t,ugraph1 + ) args (1,subst,metasenv,t,ugraph) + in + subst,metasenv,hd,ugraph + +and warn_if_not_unique xxx to1 to2 carr car1 car2 = + match xxx with + | [] -> () + | (m2,_,c2,c2')::_ -> + let m1,c1,c1' = carr,to1,to2 in + let unopt = + function Some (_,t) -> CicPp.ppterm t + | None -> "id" + in + HLog.warn + ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^ + CoercDb.string_of_carr car2^": " ^ + CoercDb.string_of_carr m1^" via "^unopt c1^" + "^ + unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^ + unopt c2^" + "^unopt c2') + +(* NUOVA UNIFICAZIONE *) +(* A substitution is a (int * Cic.term) list that associates a + metavariable i with its body. + A metaenv is a (int * Cic.term) list that associate a metavariable + i with is type. + fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back + a new substitution which is _NOT_ unwinded. It must be unwinded before + applying it. *) + +and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let t1 = deref subst t1 in + let t2 = deref subst t2 in + let (&&&) a b = (a && b) || ((not a) && (not b)) in +(* let bef = Sys.time () in *) + let b,ugraph = + if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then + false,ugraph + else +let foo () = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph +in profiler_are_convertible.HExtlib.profile foo () + in +(* let aft = Sys.time () in +if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ +CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ +CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *) + if b then + subst, metasenv, ugraph + else + match (t1, t2) with + | (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> + let _,subst,metasenv,ugraph1 = + (try + List.fold_left2 + (fun (j,subst,metasenv,ugraph) t1 t2 -> + match t1,t2 with + None,_ + | _,None -> j+1,subst,metasenv,ugraph + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + let b, ugraph1 = + R.are_convertible + ~subst ~metasenv context t1' t2' ugraph + in + if b then + j+1,subst,metasenv, ugraph1 + else + (try + let subst,metasenv,ugraph2 = + fo_unif_subst + test_equality_only + subst context metasenv t1' t2' ugraph + in + j+1,subst,metasenv,ugraph2 + with + Uncertain _ + | UnificationFailure _ -> +debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); + let metasenv, subst = + CicMetaSubst.restrict + subst [(n,j)] metasenv in + j+1,subst,metasenv,ugraph1) + ) (1,subst,metasenv,ugraph) ln lm + with + Exit -> + raise + (UnificationFailure (lazy "1")) + (* + (sprintf + "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2))) *) + | Invalid_argument _ -> + raise + (UnificationFailure (lazy "2"))) + (* + (sprintf + "Error trying to unify %s with %s: the lengths of the two local contexts do not match." + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) + in subst,metasenv,ugraph1 + | (C.Meta (n,_), C.Meta (m,_)) when n>m -> + fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph + | (C.Meta (n,l), t) + | (t, C.Meta (n,l)) -> + let swap = + match t1,t2 with + C.Meta (n,_), C.Meta (m,_) when n < m -> false + | _, C.Meta _ -> false + | _,_ -> true + in + let lower = fun x y -> if swap then y else x in + let upper = fun x y -> if swap then x else y in + let fo_unif_subst_ordered + test_equality_only subst context metasenv m1 m2 ugraph = + fo_unif_subst test_equality_only subst context metasenv + (lower m1 m2) (upper m1 m2) ugraph + in + begin + let subst,metasenv,ugraph1 = + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in + (try + let tyt,ugraph1 = + type_of_aux' metasenv subst context t ugraph + in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 + with + UnificationFailure _ as e -> raise e + | Uncertain msg -> raise (UnificationFailure msg) + | AssertFailure _ -> + debug_print (lazy "siamo allo huge hack"); + (* TODO huge hack!!!! + * we keep on unifying/refining in the hope that + * the problem will be eventually solved. + * In the meantime we're breaking a big invariant: + * the terms that we are unifying are no longer well + * typed in the current context (in the worst case + * we could even diverge) *) + (subst, metasenv,ugraph)) in + let t',metasenv,subst = + try + CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> + raise (UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) + in + let t'',ugraph2 = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + (try + let ugraph2 = + CicUniv.add_ge (upper u u') (lower u u') ugraph1 + in + s,ugraph2 + with + CicUniv.UniverseInconsistency msg -> + raise (UnificationFailure msg)) + | _ -> t',ugraph1 + in + (* Unifying the types may have already instantiated n. Let's check *) + try + let (_, oldt,_) = CicUtil.lookup_subst n subst in + let lifted_oldt = S.subst_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt ugraph2 + with + CicUtil.Subst_not_found _ -> + let (_, context, ty) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'',ty)) :: subst in + let metasenv = + List.filter (fun (m,_,_) -> not (n = m)) metasenv in + subst, metasenv, ugraph2 + end + | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) + | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> + if UriManager.eq uri1 uri2 then + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv + exp_named_subst1 exp_named_subst2 ugraph + else + raise (UnificationFailure (lazy + (sprintf + "Can't unify %s with %s due to different constants" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> + if UriManager.eq uri1 uri2 && i1 = i2 then + fo_unif_subst_exp_named_subst + test_equality_only + subst context metasenv exp_named_subst1 exp_named_subst2 ugraph + else + raise (UnificationFailure + (lazy + (sprintf + "Can't unify %s with %s due to different inductive principles" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + | C.MutConstruct (uri1,i1,j1,exp_named_subst1), + C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> + if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then + fo_unif_subst_exp_named_subst + test_equality_only + subst context metasenv exp_named_subst1 exp_named_subst2 ugraph + else + raise (UnificationFailure + (lazy + (sprintf + "Can't unify %s with %s due to different inductive constructors" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only + subst context metasenv te t2 ugraph + | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only + subst context metasenv t1 te ugraph + | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> + let subst',metasenv',ugraph1 = + fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph + in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 + | (C.LetIn (_,s1,ty1,t1), t2) + | (t2, C.LetIn (_,s1,ty1,t1)) -> + fo_unif_subst + test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph + | (C.Appl l1, C.Appl l2) -> + (* andrea: this case should be probably rewritten in the + spirit of deref *) + (match l1,l2 with + | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> + (try + List.fold_left2 + (fun (subst,metasenv,ugraph) t1 t2 -> + fo_unif_subst + test_equality_only subst context metasenv t1 t2 ugraph) + (subst,metasenv,ugraph) l1 l2 + with (Invalid_argument msg) -> + raise (UnificationFailure (lazy msg))) + | C.Meta (i,l)::args, _ when not(exists_a_meta args) -> + (* we verify that none of the args is a Meta, + since beta expanding with respoect to a metavariable + makes no sense *) + (* + (try + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv reduced t2 ugraph + with CicUtil.Subst_not_found _ -> *) + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + test_equality_only metasenv subst context t2 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1 + | _, C.Meta (i,l)::args when not(exists_a_meta args) -> + (* (try + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv t1 reduced ugraph + with CicUtil.Subst_not_found _ -> *) + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + test_equality_only + metasenv subst context t1 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1 + | _,_ -> + let lr1 = List.rev l1 in + let lr2 = List.rev l2 in + let rec + fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = + match (l1,l2) with + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_subst + test_equality_only subst context metasenv h1 h2 ugraph + | ([h],l) + | (l,[h]) -> + fo_unif_subst test_equality_only subst context metasenv + h (C.Appl (List.rev l)) ugraph + | ((h1::l1),(h2::l2)) -> + let subst', metasenv',ugraph1 = + fo_unif_subst + test_equality_only + subst context metasenv h1 h2 ugraph + in + fo_unif_l + test_equality_only subst' metasenv' (l1,l2) ugraph1 + in + (try + fo_unif_l + test_equality_only subst metasenv (lr1, lr2) ugraph + with + | UnificationFailure s + | Uncertain s as exn -> + (match l1, l2 with + (* {{{ pullback *) + | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), + (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when + CoercDb.is_a_coercion cc1 <> None && + CoercDb.is_a_coercion cc2 <> None && + not (UriManager.eq uri1 uri2) -> +(*DEBUGGING ONLY: +prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +*) + let inner_coerced t = + let t = CicMetaSubst.apply_subst subst t in + let rec aux c x t = + match t with + | Cic.Appl l -> + (match CoercGraph.coerced_arg l with + | None -> c, x + | Some (t,_) -> aux (List.hd l) t t) + | _ -> c, x + in + aux (Cic.Implicit None) (Cic.Implicit None) t + in + let c1,last_tl1 = inner_coerced (Cic.Appl l1) in + let c2,last_tl2 = inner_coerced (Cic.Appl l2) in + let car1, car2 = + match + CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 + with + | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 + | _ -> assert false + in + let head1_c, head2_c = + match + CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 + with + | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 + | _ -> assert false + in + let unfold uri ens args = + let o, _ = + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + in + assert (ens = []); + match o with + | Cic.Constant (_,Some bo,_,_,_) -> + CicReduction.head_beta_reduce ~delta:false + (Cic.Appl (bo::args)) + | _ -> assert false + in + let conclude subst metasenv ugraph last_tl1' last_tl2' = + let subst',metasenv,ugraph = +(*DEBUGGING ONLY: +prerr_endline + ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ + " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); +*) + fo_unif_subst test_equality_only subst context + metasenv last_tl1' last_tl2' ugraph + in + if subst = subst' then raise exn + else +(*DEBUGGING ONLY: +let subst,metasenv,ugrph as res = +*) + fo_unif_subst test_equality_only subst' context + metasenv (C.Appl l1) (C.Appl l2) ugraph +(*DEBUGGING ONLY: +in +(prerr_endline + (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ + " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +res) +*) + in + if CoercDb.eq_carr car1 car2 then + match last_tl1,last_tl2 with + | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn + | _, C.Meta _ + | C.Meta _, _ -> + let subst,metasenv,ugraph = + fo_unif_subst test_equality_only subst context + metasenv last_tl1 last_tl2 ugraph + in + fo_unif_subst test_equality_only subst context + metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph + | _ when CoercDb.eq_carr head1_c head2_c -> + (* composite VS composition + metas avoiding + * coercions not only in coerced position *) + if c1 <> cc1 && c2 <> cc2 then + conclude subst metasenv ugraph + last_tl1 last_tl2 + else + let l1, l2 = + if c1 = cc1 then + unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) + else + Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 + in + fo_unif_subst test_equality_only subst context + metasenv l1 l2 ugraph + | _ -> raise exn + else + let grow1 = + match last_tl1 with Cic.Meta _ -> true | _ -> false in + let grow2 = + match last_tl2 with Cic.Meta _ -> true | _ -> false in + if not (grow1 || grow2) then + (* no flexible terminals -> no pullback, but + * we still unify them, in some cases it helps *) + conclude subst metasenv ugraph last_tl1 last_tl2 + else + let meets = + CoercGraph.meets + metasenv subst context (grow1,car1) (grow2,car2) + in + (match meets with + | [] -> raise exn + | (carr,metasenv,to1,to2)::xxx -> + warn_if_not_unique xxx to1 to2 carr car1 car2; + let last_tl1',(subst,metasenv,ugraph) = + match grow1,to1 with + | true,Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl1 ugraph + | _ -> last_tl1,(subst,metasenv,ugraph) + in + let last_tl2',(subst,metasenv,ugraph) = + match grow2,to2 with + | true,Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl2 ugraph + | _ -> last_tl2,(subst,metasenv,ugraph) + in + conclude subst metasenv ugraph last_tl1' last_tl2') + (* }}} pullback *) + (* {{{ CSC: This is necessary because of the "elim H" tactic + where the type of H is only reducible to an + inductive type. This could be extended from inductive + types to any rigid term. However, the code is + duplicated in two places: inside applications and + outside them. Probably it would be better to + work with lambda-bar terms instead. *) + | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn + | (_, Cic.MutInd _::_) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure (lazy "88"))) + | (Cic.MutInd _::_,_) -> + let t2' = R.whd ~subst context t2 in + (match t2' with + C.Appl (C.MutInd _::_) -> + fo_unif_subst test_equality_only + subst context metasenv t1 t2' ugraph + | _ -> raise + (UnificationFailure + (lazy ("not a mutind :"^ + CicMetaSubst.ppterm ~metasenv subst t2 )))) + (* }}} elim H *) + | _ -> raise exn))) + | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> + let subst', metasenv',ugraph1 = + fo_unif_subst test_equality_only subst context metasenv outt1 outt2 + ugraph in + let subst'',metasenv'',ugraph2 = + fo_unif_subst test_equality_only subst' context metasenv' t1' t2' + ugraph1 in + (try + List.fold_left2 + (fun (subst,metasenv,ugraph) t1 t2 -> + fo_unif_subst + test_equality_only subst context metasenv t1 t2 ugraph + ) (subst'',metasenv'',ugraph2) pl1 pl2 + with + Invalid_argument _ -> + raise (UnificationFailure (lazy "6.1"))) + (* (sprintf + "Error trying to unify %s with %s: the number of branches is not the same." + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) + | (C.Rel _, _) | (_, C.Rel _) -> + if t1 = t2 then + subst, metasenv,ugraph + else + raise (UnificationFailure (lazy + (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + test_equality_only metasenv subst context t2 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1 + | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) -> + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + test_equality_only metasenv subst context t1 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + beta_expanded (C.Meta (i,l)) ugraph1 +(* Works iff there are no arguments applied to it; similar to the + case below + | (_, C.MutInd _) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.MutInd _ -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure (lazy "8"))) +*) + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv',ugraph1 = + fo_unif_subst true subst context metasenv s1 s2 ugraph + in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 + | (C.Prod _, _) -> + (match CicReduction.whd ~subst context t2 with + | C.Prod _ as t2 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product")))) + | (_, C.Prod _) -> + (match CicReduction.whd ~subst context t1 with + | C.Prod _ as t1 -> + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product")))) + | (_,_) -> + (* delta-beta reduction should almost never be a problem for + unification since: + 1. long computations require iota reduction + 2. it is extremely rare that a close term t1 (that could be unified + to t2) beta-delta reduces to t1' while t2 does not beta-delta + reduces in the same way. This happens only if one meta of t2 + occurs in head position during beta reduction. In this unluky + case too much reduction will be performed on t1 and unification + will surely fail. *) + let t1' = CicReduction.head_beta_reduce ~delta:true t1 in + let t2' = CicReduction.head_beta_reduce ~delta:true t2 in + if t1 = t1' && t2 = t2' then + raise (UnificationFailure + (lazy + (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + else + try + fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph + with + UnificationFailure _ + | Uncertain _ -> + raise (UnificationFailure + (lazy + (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) + +and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv + exp_named_subst1 exp_named_subst2 ugraph += + try + List.fold_left2 + (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) -> + assert (uri1=uri2) ; + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2 + with + Invalid_argument _ -> + let print_ens ens = + String.concat " ; " + (List.map + (fun (uri,t) -> + UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t) + ) ens) + in + raise (UnificationFailure (lazy (sprintf + "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))) + +(* A substitution is a (int * Cic.term) list that associates a *) +(* metavariable i with its body. *) +(* metasenv is of type Cic.metasenv *) +(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *) +(* a new substitution which is already unwinded and ready to be applied and *) +(* a new metasenv in which some hypothesis in the contexts of the *) +(* metavariables may have been restricted. *) +let fo_unif metasenv context t1 t2 ugraph = + fo_unif_subst false [] context metasenv t1 t2 ugraph ;; + +let enrich_msg msg subst context metasenv t1 t2 ugraph = + lazy ( + if verbose then + sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" + (CicMetaSubst.ppterm ~metasenv subst t1) + (try + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicPp.ppterm ty_t1 + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppterm ~metasenv subst t2) + (try + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicPp.ppterm ty_t2 + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppcontext ~metasenv subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg) + else + sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context) + (try + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context) + (try + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppcontext ~metasenv subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (Lazy.force msg) + ) + +let fo_unif_subst subst context metasenv t1 t2 ugraph = + try + fo_unif_subst false subst context metasenv t1 t2 ugraph + with + | AssertFailure msg -> + raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) + | UnificationFailure msg -> + raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) +;; +*) diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli new file mode 100644 index 000000000..d5a742279 --- /dev/null +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -0,0 +1,48 @@ +(* + ||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$ *) + +(* +exception UnificationFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; + +(* fo_unif metasenv context t1 t2 *) +(* unifies [t1] and [t2] in a context [context]. *) +(* Only the metavariables declared in [metasenv] *) +(* can be used in [t1] and [t2]. *) +(* The returned substitution can be directly *) +(* withouth first unwinding it. *) +val fo_unif : + Cic.metasenv -> Cic.context -> + Cic.term -> Cic.term -> CicUniv.universe_graph -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph + +(* fo_unif_subst metasenv subst context t1 t2 *) +(* unifies [t1] and [t2] in a context [context] *) +(* and with [subst] as the current substitution *) +(* (i.e. unifies ([subst] [t1]) and *) +(* ([subst] [t2]) in a context *) +(* ([subst] [context]) using the metasenv *) +(* ([subst] [metasenv]) *) +(* Only the metavariables declared in [metasenv] *) +(* can be used in [t1] and [t2]. *) +(* [subst] and the substitution returned are not *) +(* unwinded. *) +(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la + cosa all'apply_subst!!!*) +val fo_unif_subst : + Cic.substitution -> Cic.context -> Cic.metasenv -> + Cic.term -> Cic.term -> CicUniv.universe_graph -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph + + *) -- 2.39.2