X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=9695d714b7658940392fc4401af71d3701d7298f;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=a3b27c3e74548e86f2fd9dc712a979e3d9c23094;hpb=04ca589d65bcef6bd46cf4d277a748a12e09234b;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index a3b27c3e7..9695d714b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -1,20 +1,278 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) open Printf -exception AssertFailure of string exception MetaSubstFailure of string - -exception RelToHiddenHypothesis (* TODO remove this exception *) +exception Uncertain of string +exception AssertFailure of string let debug_print = prerr_endline type substitution = (int * Cic.term) list +(*** 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 = List.assoc i subst in + um_aux (S.lift_meta l t) + with Not_found -> (* not constrained 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 _ as t -> t + | C.Implicit _ -> assert false + | 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,t) -> C.LetIn (n, um_aux s, 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 + begin + match um_aux he with + Cic.Appl l -> Cic.Appl (l@tl') + | he' -> Cic.Appl (he'::tl') + end + in + apply_subst_gen ~appl_fun +;; + +(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) +(* performs as (apply_subst subst t) until it finds an application of *) +(* (META [meta_to_reduce]) that, once unwinding is performed, creates *) +(* a new beta-redex; in this case up to [reductions_no] consecutive *) +(* beta-reductions are performed. *) +(* Hint: this function is usually called when [reductions_no] *) +(* eta-expansions have been performed and the head of the new *) +(* application has been unified with (META [meta_to_reduce]): *) +(* during the unwinding the eta-expansions are undone. *) + +let apply_subst_reducing meta_to_reduce = + 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 meta_to_reduce, he with + Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr -> + let rec beta_reduce = + function + (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + beta_reduce (n-1,Cic.Appl(he''::tl')) + | (_,t) -> t + in + beta_reduce (reductions_no,t') + | _,_ -> t' + end + in + apply_subst_gen ~appl_fun + +let rec apply_subst_context subst 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' = + match ty with + | None -> None + | Some ty -> Some (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 = + 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)) + 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 = + CicPp.pp (apply_subst subst term) name_context + +let ppcontext' ?(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_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 + | None -> + sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[]) + +let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) + +let ppmetasenv ?(sep = "\n") metasenv subst = + String.concat sep + (List.map + (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)) + (List.filter + (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = 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_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 @@ -41,30 +299,205 @@ let position n = | _::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,dest) -> C.LetIn (name, aux k so, 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) -(*CSC: this restriction function is utterly wrong, since it does not check *) -(*CSC: that the variable that is going to be restricted does not occur free *) -(*CSC: in a part of the sequent that is not going to be restricted. *) -(*CSC: In particular, the whole approach is wrong; if restriction can fail *) -(*CSC: (as indeed it is the case), we can not collect all the restrictions *) -(*CSC: and restrict everything at the end ;-( *) -let restrict to_be_restricted = - let rec erase i n = - function - [] -> [] - | _::tl when List.mem (n,i) to_be_restricted -> - None::(erase (i+1) n tl) - | he::tl -> he::(erase (i+1) n tl) in - let rec aux = - function - [] -> [] - | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in - aux +let rec restrict subst to_be_restricted metasenv = + let names_of_context_indexes context indexes = + String.concat ", " + (List.map + (fun i -> + try + match List.nth context i 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' = + match ty with + | None -> more_to_be_restricted, None + | Some 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', + Some 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, subst) = + List.fold_right + (fun (n, context, t) (more, metasenv, subst) -> + 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 + (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)) + 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) + in + match more_to_be_restricted with + | [] -> (metasenv, subst) + | _ -> restrict subst more_to_be_restricted metasenv ;; (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) let delift n subst context metasenv l t = let module S = CicSubstitution in + let l = + let (_, canonical_context, _) = CicUtil.lookup_meta n 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 @@ -75,24 +508,19 @@ let delift n subst context metasenv l t = (*CSC: deliftato la regola per il LetIn *) (*CSC: FALSO! La regola per il LetIn non lo fa *) else - (match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> - (*CSC: Hmmm. This bit of reduction is not in the spirit of *) - (*CSC: first order unification. Does it help or does it harm? *) - deliftaux k (S.lift m t) - | Some (_,C.Decl t) -> - (*CSC: The following check seems to be wrong! *) - (*CSC: B:Set |- ?2 : Set *) - (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x *) - (*CSC: Why should I restrict ?2 over B? The instantiation *) - (*CSC: ?1 := A is perfectly reasonable and well-typed. *) - (*CSC: Thus I comment out the following two lines that *) - (*CSC: are the incriminated ones. *) - (*(* It may augment to_be_restricted *) - ignore (deliftaux k (S.lift m t)) ;*) - (*CSC: end of bug commented out *) - C.Rel ((position (m-k) l) + k) - | None -> raise RelToHiddenHypothesis) + (try + match List.nth context (m-k-1) with + Some (_,C.Def (t,_)) -> + (*CSC: Hmmm. This bit of reduction is not in the spirit of *) + (*CSC: first order unification. Does it help or does it harm? *) + deliftaux k (S.lift m t) + | Some (_,C.Decl t) -> + C.Rel ((position (m-k) l) + k) + | None -> raise (MetaSubstFailure "RelToHiddenHypothesis") + with + Failure _ -> + raise (MetaSubstFailure "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 @@ -102,29 +530,27 @@ let delift n subst context metasenv l 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 (CicPp.ppterm t))) + i (ppterm subst t))) else - (try - deliftaux k (S.lift_meta l (List.assoc i subst)) - with Not_found -> - 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 - RelToHiddenHypothesis - | NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l')) + (* 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') | C.Sort _ as t -> t - | C.Implicit 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) @@ -175,344 +601,30 @@ 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 "!!!!!!!!!!! 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 !!!!!!!!!!!!!!!!" ; - raise (MetaSubstFailure (sprintf +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 !!!!!!!!!!!!!!!!" ; + raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (CicPp.ppterm t) + (ppterm subst t) (String.concat "; " (List.map - (function Some t -> CicPp.ppterm t | None -> "_") + (function Some t -> ppterm subst t | None -> "_") l)))) in - res, restrict !to_be_restricted metasenv + let (metasenv, subst) = restrict subst !to_be_restricted metasenv in + res, metasenv, subst ;; (**** END OF DELIFT ****) -let rec unwind metasenv subst unwinded t = - let unwinded = ref unwinded in - let frozen = ref [] in - let rec um_aux metasenv = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t,metasenv - | C.Var _ as t -> t,metasenv - | C.Meta (i,l) -> - (try - S.lift_meta l (List.assoc i !unwinded), metasenv - with Not_found -> - if List.mem i !frozen then - raise (MetaSubstFailure - "Failed to unify due to cyclic constraints (occur check)") - else - let saved_frozen = !frozen in - frozen := i::!frozen ; - let res = - try - let t = List.assoc i subst in - let t',metasenv' = um_aux metasenv t in - let _,metasenv'' = - let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in - delift i subst canonical_context metasenv' l t' - in - unwinded := (i,t')::!unwinded ; - S.lift_meta l t', metasenv' - with Not_found -> - (* not constrained variable, i.e. free in subst*) - let l',metasenv' = - List.fold_right - (fun t (tl,metasenv) -> - match t with - None -> None::tl,metasenv - | Some t -> - let t',metasenv' = um_aux metasenv t in - (Some t')::tl, metasenv' - ) l ([],metasenv) - in - C.Meta (i,l'), metasenv' - in - frozen := saved_frozen ; - res - ) - | C.Sort _ - | C.Implicit as t -> t,metasenv - | C.Cast (te,ty) -> - let te',metasenv' = um_aux metasenv te in - let ty',metasenv'' = um_aux metasenv' ty in - C.Cast (te',ty'),metasenv'' - | C.Prod (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.Prod (n, s', t'), metasenv'' - | C.Lambda (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.Lambda (n, s', t'), metasenv'' - | C.LetIn (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.LetIn (n, s', t'), metasenv'' - | C.Appl (he::tl) -> - let tl',metasenv' = - List.fold_right - (fun t (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - t'::tl, metasenv' - ) tl ([],metasenv) - in - begin - match um_aux metasenv' he with - (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv'' - | (he', metasenv'') -> C.Appl (he'::tl'),metasenv'' - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.Const (uri,exp_named_subst'),metasenv' - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.MutInd (uri,typeno,exp_named_subst'),metasenv' - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv' - | C.MutCase (sp,i,outty,t,pl) -> - let outty',metasenv' = um_aux metasenv outty in - let t',metasenv'' = um_aux metasenv' t in - let pl',metasenv''' = - List.fold_right - (fun p (pl,metasenv) -> - let p',metasenv' = um_aux metasenv p in - p'::pl, metasenv' - ) pl ([],metasenv'') - in - C.MutCase (sp, i, outty', t', pl'),metasenv''' - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl,metasenv' = - List.fold_right - (fun (name, i, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, i, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) - in - C.Fix (i, liftedfl),metasenv' - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl,metasenv' = - List.fold_right - (fun (name, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) - in - C.CoFix (i, liftedfl),metasenv' - in - let t',metasenv' = um_aux metasenv t in - t',metasenv',!unwinded - -let apply_subst subst t = - (* metasenv will not be used nor modified. So, let's use a dummy empty one *) - let metasenv = [] in - let (t',_,_) = unwind metasenv [] subst t in - t' - -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [meta_to_reduce]) that, once unwinding is performed, creates *) -(* a new beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* eta-expansions have been performed and the head of the new *) -(* application has been unified with (META [meta_to_reduce]): *) -(* during the unwinding the eta-expansions are undone. *) - -let rec apply_subst_context subst = - List.map (function - | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t)) - | Some (n, Cic.Def (t, ty)) -> - let ty' = - match ty with - | None -> None - | Some ty -> Some (apply_subst subst ty) - in - Some (n, Cic.Def (apply_subst subst t, ty')) - | None -> None) - -let rec apply_subst_reducing subst meta_to_reduce t = - let rec um_aux = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ - | C.Var _ as t -> t - | C.Meta (i,l) as t -> - (try - S.lift_meta l (List.assoc i subst) - with Not_found -> - C.Meta (i,l)) - | C.Sort _ as t -> t - | 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,t) -> C.LetIn (n, um_aux s, um_aux t) - | C.Appl (he::tl) -> - let tl' = List.map um_aux tl in - let t' = - match um_aux he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - in - begin - match meta_to_reduce,he with - Some (mtr,reductions_no), C.Meta (m,_) when m = mtr -> - let rec beta_reduce = - function - (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - beta_reduce (n-1,C.Appl(he''::tl')) - | (_,t) -> t - in - beta_reduce (reductions_no,t') - | _,_ -> t' - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (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 (function (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 (function (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) -> - C.MutCase (sp, i, um_aux outty, um_aux t, - List.map um_aux pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux 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, um_aux ty, um_aux bo)) - fl - in - C.CoFix (i, liftedfl) - in - um_aux t -let ppcontext ?(sep = "\n") subst context = - String.concat sep - (List.rev_map (function - | Some (n, Cic.Decl t) -> - sprintf "%s : %s" - (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t)) - | Some (n, Cic.Def (t, ty)) -> - sprintf "%s : %s := %s" - (CicPp.ppname n) - (match ty with - | None -> "_" - | Some ty -> CicPp.ppterm (apply_subst subst ty)) - (CicPp.ppterm (apply_subst subst t)) - | None -> "_") - context) - -let ppmetasenv ?(sep = "\n") subst metasenv = - String.concat sep - (List.map - (fun (i, c, t) -> - sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i - (CicPp.ppterm (apply_subst subst t))) - (List.filter - (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst)) - metasenv)) +(** {2 Format-like pretty printers} *) -(* UNWIND THE MGU INSIDE THE MGU *) -let unwind_subst metasenv subst = - List.fold_left - (fun (unwinded,metasenv) (i,_) -> - let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in - let identity_relocation_list = - CicMkImplicit.identity_relocation_list_for_metavariable canonical_context - in - let (_,metasenv',subst') = - unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list)) - in - subst',metasenv' - ) ([],metasenv) subst +let fpp_gen ppf s = + Format.pp_print_string ppf s; + Format.pp_print_newline ppf (); + Format.pp_print_flush ppf () -(* From now on we recreate a kernel abstraction where substitutions are part of - * the calculus *) - -let whd metasenv subst context term = - (* TODO unwind's result is thrown away :-( *) - let (subst, _) = unwind_subst metasenv subst in - 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 metasenv subst context t1 t2 = - (* TODO unwind's result is thrown away :-( *) - let (subst, _) = unwind_subst metasenv subst in - let context = apply_subst_context subst context in - let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in - CicReduction.are_convertible context t1 t2 - -let type_of_aux' metasenv subst context term = - (* TODO unwind's result is thrown away :-( *) - let (subst, _) = unwind_subst metasenv subst 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 - try - CicTypeChecker.type_of_aux' metasenv context term - with CicTypeChecker.TypeCheckerFailure msg -> - raise (MetaSubstFailure ("Type checker failure: " ^ msg)) +let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) +let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) +let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])