From 4ce27bd72e72474d4d6654898faaa5a583dd6365 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:14:56 +0000 Subject: [PATCH] - removed unwind: every substitution is now _not_ unwinded - removed extra metasenv argument from all kernel proxies - added kernel proxy: subst (for CicSubstitution.subst) - added pretty printer ppterm --- helm/ocaml/cic_unification/cicMetaSubst.ml | 554 +++++++++++--------- helm/ocaml/cic_unification/cicMetaSubst.mli | 29 +- 2 files changed, 307 insertions(+), 276 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 6d8b03ddb..a28b853be 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -4,8 +4,6 @@ open Printf exception AssertFailure of string exception MetaSubstFailure of string -exception RelToHiddenHypothesis (* TODO remove this exception *) - let debug_print = prerr_endline type substitution = (int * Cic.term) list @@ -41,29 +39,194 @@ 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) -> + (try + aux k (CicSubstitution.lift_meta l (List.assoc n subst)) + with Not_found -> + let l' = + let i = ref 0 in + List.map + (function + | None -> None + | Some t -> + incr i; + 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 -> + match List.nth context i with + | None -> assert false + | Some (n, _) -> CicPp.ppname n) + 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 restrict_me = List.mem i to_be_restricted in + if restrict_me then + let more_to_be_restricted, restricted, new_tl = + erase (i+1) (i :: to_be_restricted) n tl + in + more_to_be_restricted, restricted, None :: new_tl + else + (try + let more_to_be_restricted, hd' = + force_does_not_occur_in_context to_be_restricted hd + in + let more_to_be_restricted', restricted, tl' = + erase (i+1) to_be_restricted n tl + in + more_to_be_restricted @ more_to_be_restricted', + restricted, hd' :: tl' + with Occur -> + let more_to_be_restricted, restricted, tl' = + erase (i+1) (i :: to_be_restricted) n tl + in + more_to_be_restricted, 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') = + 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 + (CicPp.ppterm s))) + with Not_found -> (more @ 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 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 module S = CicSubstitution in let to_be_restricted = ref [] in let rec deliftaux k = @@ -92,7 +255,7 @@ let delift n subst context metasenv l t = ignore (deliftaux k (S.lift m t)) ;*) (*CSC: end of bug commented out *) C.Rel ((position (m-k) l) + k) - | None -> raise RelToHiddenHypothesis) + | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst @@ -116,8 +279,7 @@ let delift n subst context metasenv l t = try Some (deliftaux k t)::l1' with - RelToHiddenHypothesis - | NotInTheList + NotInTheList | MetaSubstFailure _ -> to_be_restricted := (i,j)::!to_be_restricted ; None::l1' in @@ -184,158 +346,79 @@ debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have (function Some t -> CicPp.ppterm 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 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,metasenv - | C.Var _ as t -> t,metasenv - | C.Meta (i,l) -> + C.Rel _ as t -> t + | C.Var _ as t -> t + | 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 + 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', 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) + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in - C.Const (uri,exp_named_subst'),metasenv' + C.Const (uri, exp_named_subst') | 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) + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst in - C.MutInd (uri,typeno,exp_named_subst'),metasenv' + C.MutInd (uri,typeno,exp_named_subst') | 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) + 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'),metasenv' + C.MutConstruct (uri,typeno,consno,exp_named_subst') | 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''' + let pl' = List.map um_aux pl in + C.MutCase (sp, i, um_aux outty, um_aux t, pl') | 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) + let fl' = + List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl in - C.Fix (i, liftedfl),metasenv' + C.Fix (i, fl') | 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) + let fl' = + List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl in - C.CoFix (i, liftedfl),metasenv' + C.CoFix (i, fl') in - let t',metasenv' = um_aux metasenv t in - t',metasenv',!unwinded + um_aux term -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' +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 + +let ppterm subst term = CicPp.ppterm (apply_subst subst term) (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) (* performs as (apply_subst subst t) until it finds an application of *) @@ -347,124 +430,78 @@ let apply_subst subst t = (* 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)) +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 - Some (n, Cic.Def (apply_subst subst t, ty')) - | None -> None) + let t' = apply_subst subst t in + Some (n, Cic.Def (t', ty')) :: context + | None -> None :: context) + context [] -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 ppterm subst term = CicPp.ppterm (apply_subst subst term) 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)) + sprintf "%s : %s" (CicPp.ppname n) (ppterm 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)) + (match ty with None -> "_" | Some ty -> ppterm subst ty) + (ppterm subst t) | None -> "_") context) -let ppmetasenv ?(sep = "\n") subst metasenv = +let ppmetasenv ?(sep = "\n") metasenv subst = String.concat sep (List.map (fun (i, c, t) -> sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i - (CicPp.ppterm (apply_subst subst t))) + (ppterm subst t)) (List.filter (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst)) metasenv)) (* UNWIND THE MGU INSIDE THE MGU *) +(* let unwind_subst metasenv subst = List.fold_left (fun (unwinded,metasenv) (i,_) -> @@ -477,23 +514,27 @@ let unwind_subst metasenv subst = in subst',metasenv' ) ([],metasenv) subst +*) (* From now on we recreate a kernel abstraction where substitutions are part of * the calculus *) -let lift metasenv subst n term = - (* TODO unwind's result is thrown away :-( *) - let (subst, _) = unwind_subst metasenv subst in +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)) + 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 metasenv subst context term = - (* TODO unwind's result is thrown away :-( *) - let (subst, _) = unwind_subst metasenv subst in +let whd subst context term = let term = apply_subst subst term in let context = apply_subst_context subst context in try @@ -502,16 +543,13 @@ let whd metasenv subst context term = 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 are_convertible subst context t1 t2 = let context = apply_subst_context subst context in - let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in + let t1 = apply_subst subst t1 in + let t2 = 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 = diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index a81f50c1d..fd770215a 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -31,13 +31,9 @@ exception MetaSubstFailure of string type substitution = (int * Cic.term) list val delift : - int -> substitution -> Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> - Cic.term * Cic.metasenv - -(* unwind_subst metasenv subst *) -(* unwinds [subst] w.r.t. itself. *) -(* It can restrict some metavariable in the [metasenv] *) -val unwind_subst : Cic.metasenv -> substitution -> substitution * Cic.metasenv + int -> substitution -> Cic.context -> Cic.metasenv -> + (Cic.term option) list -> Cic.term -> + Cic.term * Cic.metasenv * substitution (* apply_subst subst t *) (* applies the substitution [subst] to [t] *) @@ -55,29 +51,26 @@ val apply_subst : substitution -> Cic.term -> Cic.term (* during the unwinding the eta-expansions are undone. *) (* [subst] must be already unwinded *) val apply_subst_reducing : - substitution -> (int * int) option -> Cic.term -> Cic.term + (int * int) option -> substitution -> Cic.term -> Cic.term val apply_subst_context : substitution -> Cic.context -> Cic.context (** {2 Pretty printers} *) val ppcontext: ?sep: string -> substitution -> Cic.context -> string -val ppmetasenv: ?sep: string -> substitution -> Cic.metasenv -> string +val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string val ppsubst: substitution -> string +val ppterm: substitution -> Cic.term -> string (* {2 Kernel wrappers} * From now on we recreate a kernel abstraction where substitutions are part of * the calculus *) -val lift : Cic.metasenv -> substitution -> int -> Cic.term -> Cic.term - -val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term - -val are_convertible: - Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term -> - bool +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 + Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term -- 2.39.2