Cool (but error messages can be bad).
;;
let subst_metasenv_and_fix_names s =
- let u,h,metasenv, subst,o = s.NTacStatus.istatus.NTacStatus.pstatus in
+ let u,h,metasenv, subst,o = s#obj in
let o =
NCicUntrusted.map_obj_kind ~skip_body:true
(NCicUntrusted.apply_subst subst []) o
in
- { s with NTacStatus.istatus =
- { s.NTacStatus.istatus with NTacStatus.pstatus =
- u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o}}
+ s#set_obj (u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
;;
let rec eval_ncommand opts status (text,prefix_len,cmd) =
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NQed loc ->
(match status.GrafiteTypes.ng_status with
- | GrafiteTypes.ProofMode
- { NTacStatus.istatus =
- { NTacStatus.pstatus = pstatus; estatus = estatus } } ->
- let uri,height,menv,subst,obj_kind = pstatus in
- if menv <> [] then
- raise
- (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
- else
- let obj_kind =
- NCicUntrusted.map_obj_kind
- (NCicUntrusted.apply_subst subst []) obj_kind in
- let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
- (* fix the height inside the object *)
- let rec fix () = function
- | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->
- NCic.Const (NReference.reference_of_spec u
- (match spec with
- | NReference.Def _ -> NReference.Def height
- | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
- | NReference.CoFix _ -> NReference.CoFix height
- | NReference.Ind _ | NReference.Con _
- | NReference.Decl as s -> s))
- | t -> NCicUtils.map (fun _ () -> ()) () fix t
- in
- let obj_kind =
- match obj_kind with
- | NCic.Fixpoint _ ->
- NCicUntrusted.map_obj_kind (fix ()) obj_kind
- | _ -> obj_kind
- in
- let obj = uri,height,[],[],obj_kind in
- NCicTypeChecker.typecheck_obj obj;
- let estatus = NCicLibrary.add_obj estatus uri obj in
- let objs = NCicElim.mk_elims obj in
- let timestamp,uris_rev =
- List.fold_left
- (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
- NCicTypeChecker.typecheck_obj obj;
- let estatus = NCicLibrary.add_obj estatus uri obj in
- estatus,uri::uris_rev
- ) (estatus,[]) objs in
- let uris = uri::List.rev uris_rev in
- GrafiteTypes.set_estatus estatus
- {status with
- GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode estatus },`New uris
+ | GrafiteTypes.ProofMode estatus ->
+ let uri,height,menv,subst,obj_kind = estatus#obj in
+ if menv <> [] then
+ raise
+ (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
+ else
+ let obj_kind =
+ NCicUntrusted.map_obj_kind
+ (NCicUntrusted.apply_subst subst []) obj_kind in
+ let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+ (* fix the height inside the object *)
+ let rec fix () = function
+ | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->
+ NCic.Const (NReference.reference_of_spec u
+ (match spec with
+ | NReference.Def _ -> NReference.Def height
+ | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+ | NReference.CoFix _ -> NReference.CoFix height
+ | NReference.Ind _ | NReference.Con _
+ | NReference.Decl as s -> s))
+ | t -> NCicUtils.map (fun _ () -> ()) () fix t
+ in
+ let obj_kind =
+ match obj_kind with
+ | NCic.Fixpoint _ ->
+ NCicUntrusted.map_obj_kind (fix ()) obj_kind
+ | _ -> obj_kind
+ in
+ let obj = uri,height,[],[],obj_kind in
+ NCicTypeChecker.typecheck_obj obj;
+ let estatus = NCicLibrary.add_obj estatus uri obj in
+ let objs = NCicElim.mk_elims obj in
+ let timestamp,uris_rev =
+ List.fold_left
+ (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
+ NCicTypeChecker.typecheck_obj obj;
+ let estatus = NCicLibrary.add_obj estatus uri obj in
+ estatus,uri::uris_rev
+ ) (estatus,[]) objs in
+ let uris = uri::List.rev uris_rev in
+ {status with
+ GrafiteTypes.ng_status =
+ GrafiteTypes.CommandMode (estatus :> NEstatus.status)},`New uris
| _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
| GrafiteAst.NObj (loc,obj) ->
let estatus =
GrafiteTypes.ng_status =
GrafiteTypes.ProofMode
(subst_metasenv_and_fix_names
- { NTacStatus.gstatus = ninitial_stack;
- istatus = { NTacStatus.pstatus = obj; estatus = estatus}})
- }
+ ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus))
+ }
in
(match nmenv with
[] ->
let get_estatus x =
match x.ng_status with
- | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus
+ | ProofMode t -> (t :> NEstatus.status)
| CommandMode e -> e
;;
let set_estatus e x =
{ x with ng_status =
match x.ng_status with
- ProofMode t ->
- ProofMode
- {t with NTacStatus.istatus =
- {t.NTacStatus.istatus with NTacStatus.estatus = e}}
+ ProofMode t -> ProofMode t#set_estatus e
| CommandMode _ -> CommandMode e}
;;
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-class status =
- object
+class type ctstatus =
+ object ('self)
inherit LexiconEngine.status
inherit NRstatus.dumpable_status
+ method set_estatus: ctstatus -> 'self
+ end
+
+class status : ctstatus =
+ object (self)
+ inherit LexiconEngine.status
+ inherit NRstatus.dumpable_status
+ method set_estatus o =
+ (self#set_lexicon_engine_status (o :> LexiconEngine.status))
+ #set_dumpable_status (o :> NRstatus.dumpable_status)
end
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
class status :
- object
+ object ('self)
inherit LexiconEngine.status
inherit NRstatus.dumpable_status
+ method set_estatus: status -> 'self
end
val lstatus = initial_status
method lstatus = lstatus
method set_lstatus v = {< lstatus = v >}
+ method set_lexicon_engine_status (o : status) = {< lstatus = o#lstatus >}
end
let dump_aliases out msg status =
object ('self)
method lstatus: lexicon_status
method set_lstatus: lexicon_status -> 'self
+ method set_lexicon_engine_status: status -> 'self
end
val eval_command : #status as 'status -> LexiconAst.command -> 'status
val timestamp = (time0 : timestamp)
method timestamp = timestamp
method set_timestamp v = {< timestamp = v >}
+ method set_library_status (o : status) = {< timestamp = o#timestamp >}
end
let time_travel status =
object ('self)
method timestamp: timestamp
method set_timestamp: timestamp -> 'self
+ method set_library_status: status -> 'self
end
val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status
val db = empty_db
method coerc_db = db
method set_coerc_db v = {< db = v >}
+ method set_coercion_status (o : status) = {< db = o#coerc_db >}
end
let index_coercion status c src tgt arity arg =
object ('self)
method coerc_db: db
method set_coerc_db: db -> 'self
+ method set_coercion_status: status -> 'self
end
val empty_db: db
val db = DB.empty
method uhint_db = db
method set_uhint_db v = {< db = v >}
+ method set_unifhint_status (o : status) = {< db = o#uhint_db >}
end
let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
object ('self)
method uhint_db: db
method set_uhint_db: db -> 'self
+ method set_unifhint_status: status -> 'self
end
val index_hint:
(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
-class status =
- object
+class type ctstatus =
+ object ('self)
inherit NCicUnifHint.status
inherit NCicCoercion.status
inherit NCicLibrary.status
+ method set_rstatus : ctstatus -> 'self
+ end
+
+class status : ctstatus =
+ object (self)
+ inherit NCicUnifHint.status
+ inherit NCicCoercion.status
+ inherit NCicLibrary.status
+ method set_rstatus o =
+ ((self#set_unifhint_status (o :> NCicUnifHint.status))
+ #set_coercion_status (o :> NCicCoercion.status))
+ #set_library_status (o :> NCicLibrary.status)
end
type sstatus = status
status
end
-class dumpable_status =
+class type ctdumpable_status =
+ object ('self)
+ inherit status
+ method dump: Serializer.obj list
+ method set_dump: Serializer.obj list -> 'self
+ method set_dumpable_status: ctdumpable_status -> 'self
+ end
+
+class dumpable_status : ctdumpable_status =
object
inherit status
val dump = ([] : Serializer.obj list)
method dump = dump
method set_dump v = {< dump = v >}
+ method set_dumpable_status o =
+ {< dump = o#dump >}#set_rstatus (o :> status)
end
(* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
class status :
- object
+ object ('self)
inherit NCicUnifHint.status
inherit NCicCoercion.status
inherit NCicLibrary.status
+ method set_rstatus: status -> 'self
end
module Serializer:
inherit status
method dump: Serializer.obj list
method set_dump: Serializer.obj list -> 'self
+ method set_dumpable_status: dumpable_status -> 'self
end
exception Error of string lazy_t
let fail msg = raise (Error msg)
-type lowtac_status = {
- pstatus : NCic.obj;
- estatus : NEstatus.status;
-}
-
-type lowtactic = lowtac_status -> int -> lowtac_status
-
-type tac_status = {
- gstatus : Continuationals.Stack.t;
- istatus : lowtac_status;
-}
-
-type tactic = tac_status -> tac_status
+class pstatus =
+ fun (o: NCic.obj) ->
+ object
+ inherit NEstatus.status
+ val obj = o
+ method obj = obj
+ method set_obj o = {< obj = o >}
+ end
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
let pp_tac_status status =
- prerr_endline (NCicPp.ppobj status.istatus.pstatus)
+ prerr_endline (NCicPp.ppobj status#obj)
;;
let pp_lowtac_status status =
prerr_endline "--------------------------------------------";
- prerr_endline (NCicPp.ppobj status.pstatus)
+ prerr_endline (NCicPp.ppobj status#obj)
;;
type cic_term = NCic.conjecture (* name, context, term *)
let relocate status destination (name,source,t as orig) =
if source == destination then status, orig else
- let u, d, metasenv, subst, o = status.pstatus in
+ let u, d, metasenv, subst, o = status#obj in
let rec lcp ctx j i = function
| (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
if n1 = n2 &&
let (metasenv, subst), t =
NCicMetaSubst.delift
~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify status.estatus 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
in
- let status = { status with pstatus = u, d, metasenv, subst, o } in
+ let status = status#set_obj (u, d, metasenv, subst, o) in
status, (name, destination, t)
;;
;;
let ppterm status t =
- let uri,height,metasenv,subst,obj = status.pstatus in
+ let uri,height,metasenv,subst,obj = status#obj in
let _,context,t = t in
NCicPp.ppterm ~metasenv ~subst ~context t
;;
| Some ty ->
let status, (_,_,x) = relocate status context ty in status, Some x
in
- let uri,height,metasenv,subst,obj = status.pstatus in
- let metasenv, subst, estatus, t =
- GrafiteDisambiguate.disambiguate_nterm expty
- status.estatus context metasenv subst t
+ let uri,height,metasenv,subst,obj = status#obj in
+ let metasenv, subst, status, t =
+ GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
- { estatus = estatus; pstatus = new_pstatus }, (None, context, t)
+ status#set_obj new_pstatus, (None, context, t)
;;
let typeof status ctx t =
let status, (_,_,t) = relocate status ctx t in
- let _,_,metasenv,subst,_ = status.pstatus in
+ let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
status, (None, ctx, ty)
;;
let whd status ?delta ctx t =
let status, (name,_,t) = relocate status ctx t in
- let _,_,_,subst,_ = status.pstatus in
+ let _,_,_,subst,_ = status#obj in
let t = NCicReduction.whd ~subst ?delta ctx t in
status, (name, ctx, t)
;;
let normalize status ?delta ctx t =
let status, (name,_,t) = relocate status ctx t in
- let _,_,_,subst,_ = status.pstatus in
+ let _,_,_,subst,_ = status#obj in
let t = NCicTacReduction.normalize ~subst ?delta ctx t in
status, (name, ctx, t)
;;
let unify 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.pstatus in
- let metasenv, subst =
- NCicUnification.unify status.estatus metasenv subst ctx a b
- in
- { status with pstatus = n,h,metasenv,subst,o }
+ let n,h,metasenv,subst,o = status#obj in
+ let metasenv, subst = NCicUnification.unify status metasenv subst ctx a b in
+ status#set_obj (n,h,metasenv,subst,o)
;;
let refine status ctx term expty =
| Some e ->
let status, (n,_, e) = relocate status ctx e in status, n, Some e
in
- let name,height,metasenv,subst,obj = status.pstatus in
- let rdb = status.estatus in
- let metasenv, subst, t, ty =
- NCicRefiner.typeof rdb metasenv subst ctx term expty
+ let name,height,metasenv,subst,obj = status#obj in
+ let metasenv,subst,t,ty =
+ NCicRefiner.typeof status metasenv subst ctx term expty
in
- { status with pstatus = name,height,metasenv,subst,obj },
- (nt,ctx,t), (ne,ctx,ty)
+ status#set_obj (name,height,metasenv,subst,obj), (nt,ctx,t), (ne,ctx,ty)
;;
-let get_goalty (status : lowtac_status) (g : int) =
- let _,_,metasenv,_,_ = status.pstatus in
+let get_goalty status g =
+ let _,_,metasenv,_,_ = status#obj in
List.assoc g metasenv
;;
refine status (ctx_of gty) t (Some gty)
in
- let name,height,metasenv,subst,obj = status.pstatus in
+ let name,height,metasenv,subst,obj = status#obj in
let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
let subst = (i, (gname, context, t, ty)) :: subst in
- { status with pstatus = (name,height,metasenv,subst,obj) }
+ status#set_obj (name,height,metasenv,subst,obj)
;;
let mk_meta status ?name ctx bo_or_ty =
match bo_or_ty with
| `Decl ty ->
let status, (_,_,ty) = relocate status ctx ty in
- let n,h,metasenv,subst,o = status.pstatus in
+ let n,h,metasenv,subst,o = status#obj in
let metasenv, _, instance, _ =
NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
status, (None,ctx,instance)
| `Def bo ->
let status, (_,_,bo_ as bo) = relocate status ctx bo in
let status, (_,_,ty) = typeof status ctx bo in
- let n,h,metasenv,subst,o = status.pstatus in
+ let n,h,metasenv,subst,o = status#obj in
let metasenv, metano, instance, _ =
NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
let subst = (metano, (name, ctx, bo_, ty)) :: subst in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
status, (None,ctx,instance)
;;
let status , (_,_,t) = found status (None, ctx, t) in
(status,true),t
else
- let _,_,_,subst,_ = status.pstatus in
+ let _,_,_,subst,_ = status#obj in
match t with
| NCic.Meta (i,lc) when List.mem_assoc i subst ->
let _,_,t,_ = NCicUtils.lookup_subst i subst in
in
aux ctx (status,false) t
in
- let _,_,_,subst,_ = low_status.pstatus in
+ let _,_,_,subst,_ = low_status#obj in
let rec select status ctx pat cic =
match pat, cic with
| _, NCic.Meta (i,lc) when List.mem_assoc i subst ->
let apply_subst status ctx t =
let status, (name,_,t) = relocate status ctx t in
- let _,_,_,subst,_ = status.pstatus in
+ let _,_,_,subst,_ = status#obj in
status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)
;;
+
+class ['stack] status =
+ fun (o: NCic.obj) (s: 'stack) ->
+ object
+ inherit (pstatus o)
+ val stack = s
+ method stack = stack
+ method set_stack s = {< stack = s >}
+ end
+
+class type lowtac_status = [unit] status
+
+type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
+
+class type tac_status = [Continuationals.Stack.t] status
+
+type 'status tactic = #tac_status as 'status -> 'status
exception Error of string lazy_t
val fail: string lazy_t -> 'a
-type lowtac_status = {
- pstatus : NCic.obj;
- estatus : NEstatus.status;
-}
-
-type lowtactic = lowtac_status -> int -> lowtac_status
-
-type tac_status = {
- gstatus : Continuationals.Stack.t;
- istatus : lowtac_status;
-}
-
-type tactic = tac_status -> tac_status
+class pstatus :
+ NCic.obj ->
+ object ('self)
+ inherit NEstatus.status
+ method obj: NCic.obj
+ method set_obj: NCic.obj -> 'self
+ end
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
type cic_term
val ctx_of : cic_term -> NCic.context
val term_of_cic_term :
- lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term
+ #pstatus as 'status -> cic_term -> NCic.context -> 'status * NCic.term
val mk_cic_term : NCic.context -> NCic.term -> cic_term
val disambiguate:
- lowtac_status -> tactic_term -> cic_term option -> NCic.context ->
- lowtac_status * cic_term (* * cic_term XXX *)
+ #pstatus as 'status -> tactic_term -> cic_term option -> NCic.context ->
+ 'status * cic_term (* * cic_term XXX *)
val analyse_indty:
- lowtac_status -> cic_term ->
- lowtac_status *
- (NReference.reference * int * NCic.term list * NCic.term list)
+ #pstatus as 'status -> cic_term ->
+ 'status * (NReference.reference * int * NCic.term list * NCic.term list)
-val ppterm: lowtac_status -> cic_term -> string
+val ppterm: #pstatus -> cic_term -> string
val whd:
- lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
- lowtac_status * cic_term
+ #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term ->
+ 'status * cic_term
val normalize:
- lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
- lowtac_status * cic_term
+ #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term ->
+ 'status * cic_term
val typeof:
- lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
+ #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
val unify:
- lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status
val refine:
- lowtac_status -> NCic.context -> cic_term -> cic_term option ->
- lowtac_status * cic_term * cic_term (* status, term, type *)
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term option ->
+ 'status * cic_term * cic_term (* status, term, type *)
val apply_subst:
- lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
+ #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
-val get_goalty: lowtac_status -> int -> cic_term
+val get_goalty: #pstatus -> int -> cic_term
val mk_meta:
- lowtac_status -> ?name:string -> NCic.context ->
+ #pstatus as 'status -> ?name:string -> NCic.context ->
[ `Decl of cic_term | `Def of cic_term ] ->
- lowtac_status * cic_term
-val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
+ 'status * cic_term
+val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
val select_term:
- lowtac_status ->
- found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
- postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
+ #pstatus as 'status ->
+ found: ('status -> cic_term -> 'status * cic_term) ->
+ postprocess: ('status -> cic_term -> 'status * cic_term) ->
cic_term -> tactic_term option * NCic.term ->
- lowtac_status * cic_term
+ 'status * cic_term
+
+val mk_in_scope: #pstatus as 'status -> cic_term -> 'status * cic_term
+val mk_out_scope:
+ int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term
+
+val pp_tac_status: #pstatus -> unit
+
+class ['stack] status :
+ NCic.obj -> 'stack ->
+ object ('self)
+ inherit pstatus
+ method stack: 'stack
+ method set_stack: 'stack -> 'self
+ end
+
+class type lowtac_status = [unit] status
+
+type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
-val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term
-val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term
+class type tac_status = [Continuationals.Stack.t] status
-val pp_tac_status: tac_status -> unit
+type 'status tactic = #tac_status as 'status -> 'status
(* end *)
;;
let dot_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| ([], _, [], _) :: _ as stack ->
(* backward compatibility: do-nothing-dot *)
(([ loc ], t, k, tag) :: s)
| _ -> fail (lazy "can't use \".\" here")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let branch_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| (g, t, k, tag) :: s ->
match init_pos g with (* TODO *)
| loc :: loc_tl ->
([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let shift_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
(match g' with
| [] -> fail (lazy "no more goals to shift")
:: (loc_tl, t', k', tag) :: s))
| _ -> fail (lazy "can't shift goals here")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let pos_tac i_s status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
when is_fresh loc ->
:: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
| _ -> fail (lazy "can't use relative positioning here")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let wildcard_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
when is_fresh loc ->
(([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
| _ -> fail (lazy "can't use wildcard here")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let merge_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
| _ -> fail (lazy "can't merge goals here")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let focus_tac gs status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| s -> assert(gs <> []);
let stack_locs =
gs;
(zero_pos gs, [], [], `FocusTag) :: deep_close gs s
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let unfocus_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| ([], [], [], `FocusTag) :: s -> s
| _ -> fail (lazy "can't unfocus, some goals are still open")
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let skip_tac status =
- let new_gstatus =
- match status.gstatus with
+ let gstatus =
+ match status#stack with
| [] -> assert false
| (gl, t, k, tag) :: s ->
let gl = List.map switch_of_loc gl in
else
([],t,k,tag) :: s
in
- { status with gstatus = new_gstatus }
+ status#set_stack gstatus
;;
let block_tac l status =
;;
let compare_statuses ~past ~present =
- let _,_,past,_,_ = past.pstatus in
- let _,_,present,_,_ = present.pstatus in
+ let _,_,past,_,_ = past#obj in
+ let _,_,present,_,_ = present#obj in
List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
;;
let exec tac low_status g =
let stack = [ [0,Open g], [], [], `NoTag ] in
- let status = tac { gstatus = stack ; istatus = low_status } in
- status.istatus
+ let status =
+ (new NTacStatus.status low_status#obj stack)#set_estatus
+ (low_status :> NEstatus.status)
+ in
+ let status = tac status in
+ (low_status#set_estatus (status :> NEstatus.status))#set_obj status#obj
;;
let distribute_tac tac status =
- match status.gstatus with
+ match status#stack with
| [] -> assert false
| (g, t, k, tag) :: s ->
debug_print (lazy ("context length " ^string_of_int (List.length g)));
in
aux s go gc loc_tl
in
- let s0, go0, gc0 = status.istatus, [], [] in
+ let s0 =
+ (new NTacStatus.status status#obj ())#set_estatus
+ (status :> NEstatus.status) in
+ let s0, go0, gc0 = s0, [], [] in
let sn, gon, gcn = aux s0 go0 gc0 g in
debug_print (lazy ("opened: "
^ String.concat " " (List.map string_of_int gon)));
let stack =
(zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
in
- { gstatus = stack; istatus = sn }
+ ((status#set_stack stack)#set_obj (sn :> lowtac_status)#obj)#set_estatus (sn :> NEstatus.status)
;;
let atomic_tac htac = distribute_tac (exec htac) ;;
;;
let first_tac tacl status =
- let res = HExtlib.list_findopt
- (fun tac _ ->
- try Some (tac status) with
- NTacStatus.Error _ -> None) tacl
+ let res =
+ HExtlib.list_findopt
+ (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
in
match res with
| None -> raise (NTacStatus.Error (lazy("No tactic left")))
instantiate status goal t)
;;
-let assumption status goal =
+let assumption_tac status = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
let context = ctx_of gty in
- let (htac:NTacStatus.tactic) =
- first_tac (List.map
- (fun (name,_) ->
- exact_tac ("",0,(Ast.Ident (name,None))))
- context)
+ let htac =
+ first_tac
+ (List.map (fun (name,_) -> exact_tac ("",0,(Ast.Ident (name,None))))
+ context)
in
- exec htac status goal
-;;
-
-let assumption_tac =
- distribute_tac assumption
+ exec htac status goal) status
;;
let find_in_context name context =
fail (lazy ("hypothesis '" ^ name ^ "' not found")))
names
in
- let n,h,metasenv,subst,o = status.pstatus in
+ let n,h,metasenv,subst,o = status#obj in
let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
- { status with pstatus = n,h,metasenv,subst,o })
+ status#set_obj (n,h,metasenv,subst,o))
;;
let generalize0_tac args =
let sort = HExtlib.unopt !sort in
let ity = HExtlib.unopt !indtyinfo in
let NReference.Ref (uri, _) = ity.reference in
- let istatus, sort = term_of_cic_term status.istatus sort (ctx_of sort) in
- let status = { status with istatus = istatus } in
+ let status, sort = term_of_cic_term status sort (ctx_of sort) in
let name = NUri.name_of_uri uri ^
match sort with
| NCic.Sort NCic.Prop -> "_ind"
;;
let assert_tac seqs status =
- match status.gstatus with
+ match status#stack with
| [] -> assert false
| (g,_,_,_) :: s ->
assert (List.length g = List.length seqs);
let auto ~params:(l,_) status goal =
let gty = get_goalty status goal in
- let n,h,metasenv,subst,o = status.pstatus in
+ let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in
let status, l =
List.fold_left
(fun (status, l) t ->
let status, t = disambiguate status t None (ctx_of gty) in
let status, ty = typeof status (ctx_of t) t in
- let status, t = term_of_cic_term status t (ctx_of gty) in
+ let status, t = term_of_cic_term status t (ctx_of gty) in
let status, ty = term_of_cic_term status ty (ctx_of ty) in
(status, (t,ty) :: l))
(status,[]) l
in
- let rdb = status.estatus in
let pt, metasenv, subst =
- Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
+ Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
;;
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val dot_tac: NTacStatus.tactic
-val branch_tac: NTacStatus.tactic
-val shift_tac: NTacStatus.tactic
-val pos_tac: int list -> NTacStatus.tactic
-val wildcard_tac: NTacStatus.tactic
-val merge_tac: NTacStatus.tactic
-val focus_tac: int list -> NTacStatus.tactic
-val unfocus_tac: NTacStatus.tactic
-val skip_tac: NTacStatus.tactic
-val try_tac: NTacStatus.tactic -> NTacStatus.tactic
+val dot_tac: 's NTacStatus.tactic
+val branch_tac: 's NTacStatus.tactic
+val shift_tac: 's NTacStatus.tactic
+val pos_tac: int list -> 's NTacStatus.tactic
+val wildcard_tac: 's NTacStatus.tactic
+val merge_tac: 's NTacStatus.tactic
+val focus_tac: int list -> 's NTacStatus.tactic
+val unfocus_tac: 's NTacStatus.tactic
+val skip_tac: 's NTacStatus.tactic
+val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
-val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
-val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
+val distribute_tac:
+ NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
+val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic
-val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
-val assumption_tac: NTacStatus.tactic
+val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
+val assumption_tac: 's NTacStatus.tactic
val change_tac:
where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
- NTacStatus.tactic
+ 's NTacStatus.tactic
val elim_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
- NTacStatus.tactic
-val intro_tac: string -> NTacStatus.tactic
+ 's NTacStatus.tactic
+val intro_tac: string -> 's NTacStatus.tactic
val cases_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
- NTacStatus.tactic
-val case1_tac: string -> NTacStatus.tactic
+ 's NTacStatus.tactic
+val case1_tac: string -> 's NTacStatus.tactic
val rewrite_tac:
dir:[ `LeftToRight | `RightToLeft ] ->
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
- NTacStatus.tactic
-val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
+ 's NTacStatus.tactic
+val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
val reduce_tac:
reduction:[ `Normalize of bool | `Whd of bool ] ->
- where:NTacStatus.tactic_pattern -> NTacStatus.tactic
+ where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
val letin_tac:
where:NTacStatus.tactic_pattern ->
what: NTacStatus.tactic_term ->
- string -> NTacStatus.tactic
+ string -> 's NTacStatus.tactic
val assert_tac:
((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
- NTacStatus.tactic
+ 's NTacStatus.tactic
val auto_tac:
params:(NTacStatus.tactic_term list * (string * string) list) ->
- NTacStatus.tactic
+ 's NTacStatus.tactic
ProofMode nstatus ->
sequents_viewer#nload_sequents nstatus;
(try
- script#setGoal (Some (Continuationals.Stack.find_goal nstatus.NTacStatus.gstatus));
+ script#setGoal
+ (Some (Continuationals.Stack.find_goal nstatus#stack));
let goal =
match script#goal with
None -> assert false
self#script#setGoal (Some (goal_of_switch goal_switch));
self#render_page ~page ~goal_switch))
- method nload_sequents
- { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack }
- =
+ method nload_sequents (status : NTacStatus.tac_status) =
+ let _,_,metasenv,subst,_ = status#obj in
_metasenv <- `New (metasenv,subst);
pages <- 0;
let win goal_switch =
w#coerce
in
assert (
- let stack_goals = Stack.open_goals stack in
+ let stack_goals = Stack.open_goals status#stack in
let proof_goals = List.map fst metasenv in
if
HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
match depth, pos with
| 0, 0 -> `Current (render_switch sw)
| 0, _ -> `Shift (pos, `Current (render_switch sw))
- | 1, pos when Stack.head_tag stack = `BranchTag ->
+ | 1, pos when Stack.head_tag status#stack = `BranchTag ->
`Shift (pos, render_switch sw)
| _ -> render_switch sw
in
add_tab markup sw)
~cont:add_switch ~todo:add_switch
- stack;
+ status#stack;
switch_page_callback <-
Some (notebook#connect#switch_page ~callback:(fun page ->
let goal_switch =
self#_loadObj obj
| _ ->
match self#script#grafite_status.ng_status with
- ProofMode tstatus ->
- let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
- self#_loadNObj nobj
+ ProofMode tstatus -> self#_loadNObj tstatus#obj
| _ -> self#blank ()
(** loads a cic uri from the environment
projects / helm.git / commitdiff