From: Andrea Asperti Date: Fri, 22 Oct 2004 12:05:26 +0000 (+0000) Subject: - ported to typed explicit substitutions X-Git-Tag: V_0_0_10~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1592bfa20a80f2f58fe0593c019689cb32072db6;p=helm.git - ported to typed explicit substitutions (this implies that kernel wrappers which used to handle substitutions are vanished) --- diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index b594e009e..db63ff568 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -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,26 +64,41 @@ 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 @@ -95,7 +111,7 @@ let clean_up_meta subst metasenv t = let cc = (try let (cc,_) = lookup_subst n subst in cc - with SubstNotFound _ -> + with CicUtil.Subst_not_found _ -> try let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc with CicUtil.Meta_not_found _ -> assert false) in @@ -166,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 @@ -316,7 +333,7 @@ let ppcontext' ?(sep = "\n") subst context = let ppsubst_unfolded subst = String.concat "\n" (List.map - (fun (idx, (c, t)) -> + (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)) @@ -329,7 +346,7 @@ let ppsubst_unfolded subst = let ppsubst subst = String.concat "\n" (List.map - (fun (idx, (c, t)) -> + (fun (idx, (c, t, _)) -> let context,name_context = ppcontext' ~sep:"; " [] c in sprintf "%s |- ?%d:= %s" context idx (ppterm_in_context [] t name_context)) @@ -349,67 +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 = clean_up_meta subst metasenv term 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 @@ -552,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' = @@ -600,11 +560,12 @@ let rec restrict subst to_be_restricted metasenv = 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 ([], []) + 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 @@ -619,22 +580,26 @@ 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 -> 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 + 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 ([], []) + subst ([], []) in match more_to_be_restricted @ more_to_be_restricted' with | [] -> (metasenv, subst) @@ -646,6 +611,7 @@ let rec restrict subst to_be_restricted metasenv = 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)))); @@ -695,25 +661,26 @@ let delift n subst context metasenv l t = "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 + 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 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 + end | C.Sort _ as t -> t | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 6ebd5a5b9..9a0bee6ae 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -27,57 +27,38 @@ exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string -exception SubstNotFound of int - (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) -type substitution = (int * (Cic.context * Cic.term)) list +(* type substitution = (int * (Cic.context * Cic.term)) list *) (** @raise SubstNotFound *) -val lookup_subst: int -> substitution -> Cic.context * Cic.term (* apply_subst subst t *) (* applies the substitution [subst] to [t] *) (* [subst] must be already unwinded *) -val apply_subst : substitution -> Cic.term -> Cic.term - -val apply_subst_context : substitution -> Cic.context -> Cic.context -val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv - -(* {2 Kernel wrappers} - * From now on we recreate a kernel abstraction where substitutions are part of - * the calculus *) - -val lift : substitution -> int -> Cic.term -> Cic.term -val subst: substitution -> Cic.term -> Cic.term -> Cic.term -val whd: substitution -> Cic.context -> Cic.term -> Cic.term -val are_convertible: substitution -> Cic.context -> Cic.term -> Cic.term -> bool - -val type_of_aux': - Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term -val tempi_type_of_aux : float ref -val tempi_subst : float ref -val tempi_type_of_aux_subst : float ref +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 -> substitution -> Cic.context -> Cic.metasenv -> + int -> Cic.substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> - Cic.term * Cic.metasenv * substitution + Cic.term * Cic.metasenv * Cic.substitution val restrict : - substitution -> (int * int) list -> Cic.metasenv -> - Cic.metasenv * substitution + Cic.substitution -> (int * int) list -> Cic.metasenv -> + Cic.metasenv * Cic.substitution (** {2 Pretty printers} *) -val ppsubst_unfolded: substitution -> string -val ppsubst: substitution -> string -val ppterm: substitution -> Cic.term -> string -val ppcontext: ?sep: string -> substitution -> Cic.context -> string +val ppsubst_unfolded: Cic.substitution -> string +val ppsubst: Cic.substitution -> string +val ppterm: Cic.substitution -> Cic.term -> string +val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string val ppterm_in_context: - substitution -> Cic.term -> (Cic.name option) list -> string -val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string + Cic.substitution -> Cic.term -> (Cic.name option) list -> string +val ppmetasenv: ?sep: string -> Cic.metasenv -> Cic.substitution -> string (** {2 Format-like pretty printers} * As above with prototypes suitable for toplevel/ocamldebug printers. No @@ -85,7 +66,7 @@ val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string * with only one argument. *) -val fppsubst: Format.formatter -> substitution -> unit +val fppsubst: Format.formatter -> Cic.substitution -> unit val fppterm: Format.formatter -> Cic.term -> unit val fppmetasenv: Format.formatter -> Cic.metasenv -> unit @@ -96,5 +77,5 @@ val reset_counters: unit -> unit *) (* val clean_up_meta : - substitution -> Cic.metasenv -> Cic.term -> Cic.term + Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term *)