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
| _::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 =
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
try
Some (deliftaux k t)::l1'
with
- RelToHiddenHypothesis
- | NotInTheList
+ NotInTheList
| MetaSubstFailure _ ->
to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
in
(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 *)
(* 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,_) ->
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
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 =
projects / helm.git / commitdiff