let relocate status destination (name,source,t as orig) =
if source == destination then status, orig else
- let rec lcp j i = function
- | (n1, t1)::cl1, (n2, t2)::cl2 ->
- if n1 = n2 && t1 = t2 then
- NCic.Rel i :: lcp (j-1) (i-1) (cl1,cl2)
+ let u, d, metasenv, subst, o = status.pstatus in
+ let rec lcp ctx j i = function
+ | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+ NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
+ else
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
+ | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
+ NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
+ else
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
+ | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+ NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
else
HExtlib.mk_list (NCic.Appl
[NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
+ | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false
| _::_, [] ->
HExtlib.mk_list (NCic.Appl
[NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
| _ -> []
in
let lc =
- lcp (List.length destination) (List.length source)
+ lcp [] (List.length destination) (List.length source)
(List.rev destination, List.rev source)
in
let lc = (0,NCic.Ctx (List.rev lc)) in
- let u, d, metasenv, subst, o = status.pstatus in
let db = NCicUnifHint.db () in (* XXX fixme *)
let (metasenv, subst), t =
NCicMetaSubst.delift
s, t
;;
-type ast_term = string * int * CicNotationPt.term
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let _,context,t = t in
+ NCicPp.ppterm ~metasenv ~subst ~context t
+;;
-let disambiguate (status : lowtac_status) (t : ast_term)
- (ty : cic_term option) context =
+let disambiguate status t ty context =
let status, expty =
match ty with
| None -> status, None
;;
let mk_cic_term c t = None,c,t ;;
+
+let apply_subst status ctx t =
+ let status, (name,_,t) = relocate status ctx t in
+ let _,_,_,subst,_ = status.pstatus in
+ status, (name, ctx, NCicUntrusted.apply_subst subst t)
+;;