with
| MultiPassDisambiguator.DisambiguationError _
| NCicRefiner.RefineFailure _
+ | NCicRefiner.Uncertain _
| NCicUnification.UnificationFailure _
+ | NCicUnification.Uncertain _
| NCicTypeChecker.TypeCheckerFailure _
- | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy fname)
+ | NCicMetaSubst.MetaSubstFailure _
+ | NCicMetaSubst.Uncertain _ as exn -> fail ~exn (lazy fname)
;;
class type g_eq_status =
let mk_cic_term c t = c,t ;;
let ppterm (status:#pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
status#ppterm ~metasenv ~subst ~context t
;;
let ppcontext (status: #pstatus) c =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
status#ppcontext ~metasenv ~subst c
;;
let ppterm_and_context (status: #pstatus) t =
- let uri,height,metasenv,subst,obj = status#obj in
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^
status#ppterm ~metasenv ~subst ~context t
;;
-let relocate status destination (source,t as orig) =
+let relocate status destination (source,_t as orig) =
pp(lazy("relocate:\n" ^ ppterm_and_context status orig));
pp(lazy("relocate in:\n" ^ ppcontext status destination));
let rc =
compute_ops (e::ctx) (cl1,cl2)
else
[ `Delift ctx; `Lift (List.rev ex) ]
- | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+ | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
if n1 = n2 &&
NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then
compute_ops (e::ctx) (cl1,cl2)
else
[ `Delift ctx; `Lift (List.rev ex) ]
- | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 ->
+ | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 ->
[ `Delift ctx; `Lift (List.rev ex) ]
| _::_ as ex, [] -> [ `Lift (List.rev ex) ]
| [], _::_ -> [ `Delift ctx ]
let disambiguate status context t ty =
let status, expty =
match ty with
- | None -> status, None
- | Some ty ->
- let status, (_,x) = relocate status context ty in status, Some x
+ | `XTSome ty ->
+ let status, (_,x) = relocate status context ty in status, `XTSome x
+ | `XTNone -> status, `XTNone
+ | `XTSort -> status, `XTSort
+ | `XTInd -> status, `XTInd
in
let uri,height,metasenv,subst,obj = status#obj in
let metasenv, subst, status, t =
status, (ctx, t)
;;
+let are_convertible status ctx a b =
+ let status, (_,a) = relocate status ctx a in
+ let status, (_,b) = relocate status ctx b in
+ let _n,_h,metasenv,subst,_o = status#obj in
+ let res = NCicReduction.are_convertible status metasenv subst ctx a b in
+ status, res
+;;
+let are_convertible a b c d = wrap "are_convertible" (are_convertible a b c) d;;
+
let unify status ctx a b =
let status, (_,a) = relocate status ctx a in
let status, (_,b) = relocate status ctx b in
let status, (_,term) = relocate status ctx term in
let status, expty =
match expty with
- None -> status, None
- | Some e ->
- let status, (_, e) = relocate status ctx e in status, Some e
+ | `XTSome e ->
+ let status, (_, e) = relocate status ctx e in status, `XTSome e
+ | `XTNone -> status, `XTNone
+ | `XTSort -> status, `XTSort
+ | `XTInd -> status, `XTInd
in
let name,height,metasenv,subst,obj = status#obj in
let metasenv,subst,t,ty =
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
if dorefine then
- let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+ let status, (_,t), (_,ty) = refine status context t (`XTSome (context,gty)) in
to_subst status i (gname,context,t,ty)
else
let status,(_,ty) = typeof status context t in
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
let ggty = mk_cic_term context gty in
- let status, (_,t) = disambiguate status context t (Some ggty) in
+ let status, (_,t) = disambiguate status context t (`XTSome ggty) in
to_subst status i (gname,context,t,gty)
;;
else
let _,_,_,subst,_ = status#obj in
match t with
- | NCic.Meta (i,lc) when List.mem_assoc i subst ->
+ | NCic.Meta (i,_lc) when List.mem_assoc i subst ->
let _,_,t,_ = NCicUtils.lookup_subst i subst in
aux ctx (status,already_found) t
| NCic.Meta _ -> (status,already_found),t
let ctx = (n, NCic.Decl s2) :: ctx in
let status, t = select status ctx t1 t2 in
status, NCic.Prod (n,s,t)
- | NCic.Appl l1, NCic.Appl l2 ->
+ | NCic.Appl l1, NCic.Appl l2 when List.length l1 = List.length l2 ->
let status, l =
List.fold_left2
(fun (status,l) x y ->
(status,[]) l1 l2
in
status, NCic.Appl (List.rev l)
- | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
+ | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2)
+ when List.length pl1 = List.length pl2 ->
let status, t = select status ctx t1 t2 in
let status, ot = select status ctx ot1 ot2 in
let status, pl =
| NCic.Implicit `Hole, t ->
(match wanted with
| Some wanted ->
- let status', wanted = disambiguate status ctx wanted None in
+ let status', wanted = disambiguate status ctx wanted `XTNone in
pp(lazy("wanted: "^ppterm status' wanted));
let (status',found), t' = match_term status' ctx wanted t in
if found then status',t' else status,t
let _,_,_,cl = List.nth tl i in
let consno = List.length cl in
let left, right = HExtlib.split_nth lno args in
- status, (ref, consno, left, right)
+ status, (ref, consno, left, right, cl)
;;
let apply_subst status ctx t =