X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=db63ff5685ab23cfe2eec391a304d2caf87c651b;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=512c65d986fa2c48015309faca2a908c7501a654;hpb=fb0f22004d533abca8d157ed89665dbf1041e0e2;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 512c65d98..db63ff568 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,13 +25,147 @@ 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 () = + prerr_endline (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 exception Uncertain of string exception AssertFailure of string let debug_print = prerr_endline -type substitution = (int * Cic.term) list +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.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 ***) @@ -48,9 +182,10 @@ let apply_subst_gen ~appl_fun subst term = C.Var (uri, exp_named_subst') | C.Meta (i, l) -> (try - let t = List.assoc i subst in + let (_, t,_) = lookup_subst i subst in um_aux (S.lift_meta l t) - with Not_found -> (* not constrained 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 @@ -131,10 +266,16 @@ let apply_subst = | _ -> t' end in - apply_subst_gen ~appl_fun + fun s t -> +(* incr apply_subst_counter; *) + apply_subst_gen ~appl_fun s t ;; let rec apply_subst_context subst context = +(* + incr apply_subst_context_counter; + context_length := !context_length + List.length context; +*) List.fold_right (fun item context -> match item with @@ -153,22 +294,19 @@ let rec apply_subst_context subst context = context [] let apply_subst_metasenv subst metasenv = +(* + incr apply_subst_metasenv_counter; + metasenv_length := !metasenv_length + List.length metasenv; +*) List.map (fun (n, context, ty) -> (n, apply_subst_context subst context, apply_subst subst ty)) (List.filter - (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst)) + (fun (i, _, _) -> not (List.mem_assoc i 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 = @@ -192,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 = @@ -202,68 +363,13 @@ let ppmetasenv ?(sep = "\n") metasenv subst = sprintf "%s |- ?%d: %s" context i (ppterm_in_context subst t name_context)) (List.filter - (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) 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 = - 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 = - 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 = - 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 = - 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;; -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 = - List.map - (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t)) - (List.filter - (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) 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_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; - 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 @@ -372,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 @@ -406,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' = @@ -430,9 +536,9 @@ let rec restrict subst to_be_restricted metasenv = with Occur -> more_to_be_restricted, (i :: restricted), None :: tl') in - let (more_to_be_restricted, metasenv, subst) = + let (more_to_be_restricted, metasenv) = (* restrict metasenv *) List.fold_right - (fun (n, context, t) (more, metasenv, subst) -> + (fun (n, context, t) (more, metasenv) -> let to_be_restricted = List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) in @@ -448,37 +554,69 @@ let rec restrict subst to_be_restricted metasenv = force_does_not_occur subst restricted t in let metasenv' = (n, context', t') :: metasenv in - (try - let s = List.assoc n subst in - try - let more_to_be_restricted'', s' = - force_does_not_occur subst restricted s - in - let subst' = (n, s') :: (List.remove_assoc n subst) in - let more = - more @ more_to_be_restricted @ more_to_be_restricted' @ - more_to_be_restricted'' - in - (more, metasenv', subst') - with Occur -> - raise (MetaSubstFailure (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 s))) - with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst)) + (more @ more_to_be_restricted @ more_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 ([], [], subst) + n (names_of_context_indexes context to_be_restricted)))) + metasenv ([], []) in - match more_to_be_restricted with + 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 = 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) + 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) - | _ -> restrict subst more_to_be_restricted metasenv + | 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 @@ -517,28 +655,32 @@ 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 + (* 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))) + 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') + 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) @@ -591,7 +733,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)