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 =
method obj: NCic.obj
end
-class pstatus =
+class virtual pstatus =
fun (o: NCic.obj) ->
object (self)
inherit GrafiteDisambiguate.status
type tactic_term = NotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
-let pp_tac_status status =
- prerr_endline (NCicPp.ppobj status#obj);
- prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
-;;
-
type cic_term = NCic.context * NCic.term
let ctx_of (c,_) = c ;;
let mk_cic_term c t = c,t ;;
-let ppterm status t =
- let uri,height,metasenv,subst,obj = status#obj in
+let ppterm (status:#pstatus) t =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
- NCicPp.ppterm ~metasenv ~subst ~context t
+ status#ppterm ~metasenv ~subst ~context t
;;
-let ppcontext status c =
- let uri,height,metasenv,subst,obj = status#obj in
- NCicPp.ppcontext ~metasenv ~subst c
+let ppcontext (status: #pstatus) c =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
+ status#ppcontext ~metasenv ~subst c
;;
-let ppterm_and_context status t =
- let uri,height,metasenv,subst,obj = status#obj in
+let ppterm_and_context (status: #pstatus) t =
+ let _uri,_height,metasenv,subst,_obj = status#obj in
let context,t = t in
- NCicPp.ppcontext ~metasenv ~subst context ^ "\n ⊢ "^
- NCicPp.ppterm ~metasenv ~subst ~context t
+ 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 =
let rec compute_ops ctx = function (* destination, source *)
| (n1, NCic.Decl t1 as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
if n1 = n2 &&
- NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+ 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.Def (b1,t1) as e)::cl1 as ex, (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
+ NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 &&
+ NCicReduction.are_convertible status ctx ~subst ~metasenv b1 b2 then
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 ctx ~subst ~metasenv t1 t2 then
+ 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 ]
(fun (status, (source,t)) -> function
| `Lift extra_ctx ->
let len = List.length extra_ctx in
- status, (extra_ctx@source, NCicSubstitution.lift len t)
+ status, (extra_ctx@source, NCicSubstitution.lift status len t)
| `Delift ctx ->
let len_ctx = List.length ctx in
let irl = mk_irl 1 (List.length ctx) in
let lc = List.length source - len_ctx, NCic.Ctx irl in
let u, d, metasenv, subst, o = status#obj in
pp(lazy("delifting as " ^
- NCicPp.ppterm ~metasenv ~subst ~context:source
- (NCic.Meta (0,lc))));
+ status#ppterm ~metasenv ~subst ~context:source
+ (NCic.Meta (-1,lc))));
let (metasenv, subst), t =
- NCicMetaSubst.delift
+ NCicMetaSubst.delift status
~unify:(fun m s c t1 t2 ->
try Some (NCicUnification.unify status m s c t1 t2)
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _ -> None)
- metasenv subst source 0 lc t
+ metasenv subst source (-1) lc t
in
let status = status#set_obj (u, d, metasenv, subst, o) in
status, (ctx,t))
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 =
let typeof status ctx t =
let status, (_,t) = relocate status ctx t in
let _,_,metasenv,subst,_ = status#obj in
- let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
+ let ty = NCicTypeChecker.typeof status ~subst ~metasenv ctx t in
status, (ctx, ty)
;;
let typeof a b c = wrap "typeof" (typeof a b) c;;
let saturate status ?delta (ctx,t) =
let n,h,metasenv,subst,k = status#obj in
- let t,metasenv,args = NCicMetaSubst.saturate ?delta metasenv subst ctx t 0 in
+ let t,metasenv,args = NCicMetaSubst.saturate status ?delta metasenv subst ctx t 0 in
let status = status#set_obj (n,h,metasenv,subst,k) in
status, (ctx,t), List.map (fun x -> ctx,x) args
;;
let whd status ?delta ctx t =
let status, (_,t) = relocate status ctx t in
let _,_,_,subst,_ = status#obj in
- let t = NCicReduction.whd ~subst ?delta ctx t in
+ let t = NCicReduction.whd status ~subst ?delta ctx t in
status, (ctx, t)
;;
let normalize status ?delta ctx t =
let status, (_,t) = relocate status ctx t in
let _,_,_,subst,_ = status#obj in
- let t = NCicTacReduction.normalize ~subst ?delta ctx t in
+ let t = NCicTacReduction.normalize status ~subst ?delta ctx t in
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 f () =
let name,height,metasenv,subst,obj = status#obj in
let metasenv, t =
- NCicUnification.fix_sorts metasenv subst t in
+ NCicUnification.fix_sorts status metasenv subst t in
let status = status#set_obj (name,height,metasenv,subst,obj) in
status, (ctx,t)
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
| _ ->
- NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux
+ NCicUntrusted.map_term_fold_a status (fun e c -> e::c) ctx aux
(status,already_found) t
in
aux ctx (status,false) t
| _, NCic.Meta (i,lc) when List.mem_assoc i subst ->
let cic =
let _,_,t,_ = NCicUtils.lookup_subst i subst in
- NCicSubstitution.subst_meta lc t
+ NCicSubstitution.subst_meta status lc t
in
select status ctx pat cic
| NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
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
status,t)
| NCic.Implicit _, t -> status, t
| _,t ->
- fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
+ fail (lazy ("malformed pattern: " ^ status#ppterm ~metasenv:[]
~context:[] ~subst:[] pat ^ " against " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))
in
pp(lazy ("select in: "^ppterm low_status (context,term)));
let status, term = select low_status context path term in
| _,NCic.Appl (NCic.Const (NRef.Ref (_,(NRef.Ind _)) as ref) :: args) ->
ref, args
| _,_ -> fail (lazy ("not an inductive type: " ^ ppterm status ty)) in
- let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys status ref in
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 =
let status, (_,t) = relocate status ctx t in
let _,_,_,subst,_ = status#obj in
- status, (ctx, NCicUntrusted.apply_subst subst ctx t)
+ status, (ctx, NCicUntrusted.apply_subst status subst ctx t)
;;
let apply_subst_context status ~fix_projections ctx =
let _,_,_,subst,_ = status#obj in
- NCicUntrusted.apply_subst_context ~fix_projections subst ctx
+ NCicUntrusted.apply_subst_context status ~fix_projections subst ctx
;;
let metas_of_term status (context,t) =
let _,_,_,subst,_ = status#obj in
- NCicUntrusted.metas_of_term subst context t
+ NCicUntrusted.metas_of_term status subst context t
;;
(* ============= move this elsewhere ====================*)
method stack: 'stack
end
-class ['stack] status =
+class virtual ['stack] status =
fun (o: NCic.obj) (s: 'stack) ->
object (self)
inherit (pstatus o)
= fun o -> (self#set_pstatus o)#set_stack o#stack
end
-class type lowtac_status = [unit] status
+class type virtual lowtac_status = [unit] status
type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
-class type tac_status = [Continuationals.Stack.t] status
+class type virtual tac_status = [Continuationals.Stack.t] status
type 'status tactic = #tac_status as 'status -> 'status
+let pp_tac_status (status: #tac_status) =
+ prerr_endline (status#ppobj status#obj);
+ prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
+;;
+
module NCicInverseRelIndexable : Discrimination_tree.Indexable
with type input = cic_term and type constant_name = NUri.uri = struct
projects / helm.git / blobdiff