X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=718951c68a579756e4c4bd1d0994c835d28e2bac;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=614faf6df15f50d6af219ac90ccacf502afd04fb;hpb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 614faf6df..718951c68 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -68,9 +68,9 @@ context length: %d (avg = %.2f) -exception MetaSubstFailure of string -exception Uncertain of string -exception AssertFailure of string +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t exception DeliftingARelWouldCaptureAFreeVariable;; let debug_print = fun _ -> () @@ -191,8 +191,8 @@ let apply_subst_gen ~appl_fun subst term = List.map (function None -> None | Some t -> Some (um_aux t)) l in C.Meta (i,l')) - | C.Sort _ as t -> t - | C.Implicit _ -> assert false + | 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) @@ -288,9 +288,15 @@ let apply_subst_metasenv subst metasenv = let ppterm subst term = CicPp.ppterm (apply_subst subst term) -let ppterm_in_context subst term name_context = +let ppterm_in_name_context subst term name_context = CicPp.pp (apply_subst subst term) name_context +let ppterm_in_context subst term context = + let name_context = + List.map (function None -> None | Some (n,_) -> Some n) context + in + ppterm_in_name_context subst term name_context + let ppcontext' ?(sep = "\n") subst context = let separate s = if s = "" then "" else s ^ sep in List.fold_right @@ -298,13 +304,13 @@ let ppcontext' ?(sep = "\n") subst context = match context_entry with Some (n,Cic.Decl t) -> sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_context subst t name_context), (Some n)::name_context + (ppterm_in_name_context subst t name_context), (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) (match ty with None -> "_" - | Some ty -> ppterm_in_context subst ty name_context) - (ppterm_in_context subst bo name_context), (Some n)::name_context + | Some ty -> ppterm_in_name_context subst ty name_context) + (ppterm_in_name_context subst bo name_context), (Some n)::name_context | None -> sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) @@ -315,7 +321,7 @@ let ppsubst_unfolded subst = (fun (idx, (c, t,_)) -> let context,name_context = ppcontext' ~sep:"; " subst c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_context subst t name_context)) + (ppterm_in_name_context subst t name_context)) subst) (* Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) @@ -328,7 +334,7 @@ let ppsubst subst = (fun (idx, (c, t, _)) -> let context,name_context = ppcontext' ~sep:"; " [] c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_context [] t name_context)) + (ppterm_in_name_context [] t name_context)) subst) ;; @@ -340,7 +346,7 @@ let ppmetasenv ?(sep = "\n") subst metasenv = (fun (i, c, t) -> let context,name_context = ppcontext' ~sep:"; " subst c in sprintf "%s |- ?%d: %s" context i - (ppterm_in_context subst t name_context)) + (ppterm_in_name_context subst t name_context)) (List.filter (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv)) @@ -536,10 +542,10 @@ let rec restrict subst to_be_restricted metasenv = (more @ more_to_be_restricted @ more_to_be_restricted', metasenv') with Occur -> - raise (MetaSubstFailure (sprintf + 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 ([], []) + n (names_of_context_indexes context to_be_restricted))))) + metasenv ([], []) in let (more_to_be_restricted', subst) = (* restrict subst *) List.fold_right @@ -567,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv = @ more_to_be_restricted'@more_to_be_restricted'' in (more, subst') with Occur -> - let error_msg = sprintf + 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 subst term) + (ppterm subst term)) in (* DEBUG debug_print (lazy error_msg); @@ -623,10 +629,10 @@ let delift n subst context metasenv l t = deliftaux k (S.lift m t) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure "RelToHiddenHypothesis") + | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) with Failure _ -> - raise (MetaSubstFailure "Unbound variable found in deliftaux") + raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) ) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = @@ -640,9 +646,9 @@ let delift n subst context metasenv l t = with CicUtil.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then - raise (MetaSubstFailure (sprintf + 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 subst t))) + i (ppterm subst t)))) else begin (* I do not consider the term associated to ?i in subst since *) @@ -724,13 +730,13 @@ debug_print(lazy (sprintf (List.map (function Some t -> ppterm subst t | None -> "_") l )))); *) - raise (Uncertain (sprintf + raise (Uncertain (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)))) + l))))) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst