X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=d18458e2bb711f486e9f5fe557c6390cffb48c3c;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=387c747f6d8c064c3fea82a90802e76946a13e03;hpb=57b385b0d728a06d50d3011473e9afeaf51b674f;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 387c747f6..d18458e2b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2003, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -25,8 +25,9 @@ open Printf -(* (* PROFILING *) -let apply_subst_counter = ref 0 +(* 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 @@ -63,22 +64,108 @@ context length: %d (avg = %.2f) ((float !metasenv_length) /. (float !apply_subst_metasenv_counter)) !context_length ((float !context_length) /. (float !apply_subst_context_counter)) - ) -*) + )*) + + exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string -exception SubstNotFound of int let debug_print = prerr_endline type substitution = (int * (Cic.context * Cic.term)) list -let lookup_subst n subst = - try - List.assoc n subst - with Not_found -> raise (SubstNotFound n) +(* +let rec deref subst = + let third _,_,a = a in + function + Cic.Meta(n,l) as t -> + (try + deref subst + (CicSubstitution.lift_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 ***) @@ -95,9 +182,10 @@ let apply_subst_gen ~appl_fun subst term = C.Var (uri, exp_named_subst') | C.Meta (i, l) -> (try - let (context, t) = lookup_subst i subst in + let (_, t,_) = lookup_subst i subst in um_aux (S.lift_meta l t) - with SubstNotFound _ -> (* unconstrained variable, i.e. free in subst*) + 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 @@ -219,14 +307,6 @@ let apply_subst_metasenv subst metasenv = (***** Pretty printing functions ******) -let ppsubst subst = - String.concat "\n" - (List.map - (fun (idx, (_, term)) -> - Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) - subst) -;; - let ppterm subst term = CicPp.ppterm (apply_subst subst term) let ppterm_in_context subst term name_context = @@ -250,6 +330,29 @@ let ppcontext' ?(sep = "\n") subst context = sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) +let ppsubst_unfolded subst = + String.concat "\n" + (List.map + (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)) + subst) +(* + Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) + subst) *) +;; + +let ppsubst subst = + String.concat "\n" + (List.map + (fun (idx, (c, t, _)) -> + let context,name_context = ppcontext' ~sep:"; " [] c in + sprintf "%s |- ?%d:= %s" context idx + (ppterm_in_context [] t name_context)) + subst) +;; + let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) let ppmetasenv ?(sep = "\n") metasenv subst = @@ -263,66 +366,10 @@ let ppmetasenv ?(sep = "\n") metasenv subst = (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv)) -(* From now on we recreate a kernel abstraction where substitutions are part of - * the calculus *) - -let lift subst n term = -(* incr subst_counter; *) - let term = apply_subst subst term in - try - CicSubstitution.lift n term - with e -> - raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e)) - -let subst subst t1 t2 = -(* incr subst_counter; *) - let t1 = apply_subst subst t1 in - let t2 = apply_subst subst t2 in - try - CicSubstitution.subst t1 t2 - with e -> - raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e)) - -let whd subst context term = -(* incr whd_counter; *) - let term = apply_subst subst term in - let context = apply_subst_context subst context in - try - CicReduction.whd context term - with e -> - raise (MetaSubstFailure ("Weak head reduction failure: " ^ - Printexc.to_string e)) - -let are_convertible subst context t1 t2 = -(* incr are_convertible_counter; *) - let context = apply_subst_context subst context in - let t1 = apply_subst subst t1 in - let t2 = apply_subst subst t2 in - CicReduction.are_convertible context t1 t2 - let tempi_type_of_aux_subst = ref 0.0;; let tempi_subst = ref 0.0;; let tempi_type_of_aux = ref 0.0;; - (* assumption: metasenv is already instantiated wrt subst *) -let type_of_aux' metasenv subst context term = - let time1 = Unix.gettimeofday () in - let term = apply_subst subst term in - let context = apply_subst_context subst context in -(* let metasenv = apply_subst_metasenv subst metasenv in *) - let time2 = Unix.gettimeofday () in - let res = - try - CicTypeChecker.type_of_aux' metasenv context term - with CicTypeChecker.TypeCheckerFailure msg -> - raise (MetaSubstFailure ("Type checker failure: " ^ msg)) - in - let time3 = Unix.gettimeofday () in - tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; - tempi_subst := !tempi_subst +. time2 -. time1 ; - tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; - res - (**** 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 @@ -431,7 +478,7 @@ let rec restrict subst to_be_restricted metasenv = (List.map (fun i -> try - match List.nth context i with + match List.nth context (i-1) with | None -> assert false | Some (n, _) -> CicPp.ppname n with @@ -465,11 +512,11 @@ let rec restrict subst to_be_restricted metasenv = | [] -> [], to_be_restricted, [] | hd::tl -> let more_to_be_restricted,restricted,tl' = - erase (i+1) to_be_restricted n 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' + more_to_be_restricted, restricted, None:: tl' else (try let more_to_be_restricted', hd' = @@ -512,12 +559,13 @@ let rec restrict subst to_be_restricted metasenv = with Occur -> raise (MetaSubstFailure (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 - (fun (n, (context, term)) (more, subst) -> + (* 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 @@ -532,23 +580,43 @@ let rec restrict subst to_be_restricted metasenv = let more_to_be_restricted', term' = force_does_not_occur subst restricted term in - let subst' = (n, (context', term')) :: subst in - let more = more @ more_to_be_restricted @ more_to_be_restricted' 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 -> - raise (MetaSubstFailure (sprintf + let error_msg = 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))))) - subst ([], []) + (ppterm subst term) + in + (* DEBUG + prerr_endline error_msg; + prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst)); + prerr_endline ("subst = \n" ^ (ppsubst subst)); + prerr_endline ("context = \n" ^ (ppcontext subst context)); *) + raise (MetaSubstFailure error_msg))) + subst ([], []) in match more_to_be_restricted @ more_to_be_restricted' with | [] -> (metasenv, subst) | l -> restrict subst l metasenv ;; -(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) +(*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 *) + +(* + prerr_endline ("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, _) = CicUtil.lookup_meta n metasenv in @@ -587,28 +655,36 @@ let delift n subst context metasenv l t = in C.Var (uri,exp_named_subst') | C.Meta (i, l1) as t -> - if i = n then - raise (MetaSubstFailure (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))) - else - (* 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') + (try + let (_,t,_) = CicUtil.lookup_subst i subst in + deliftaux k (CicSubstitution.lift_meta l1 t) + with CicUtil.Subst_not_found _ -> + (* see the top level invariant *) + if (i = n) then + raise (MetaSubstFailure (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))) + 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) @@ -661,7 +737,14 @@ let delift n subst context metasenv l t = (* 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 "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; +(* debug_print "First Order UnificationFailure during delift" ; +prerr_endline(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 + ))); *) raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t)