From e603c19e82c160362587cb0bc578287c87122b90 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Jun 2009 16:48:35 +0000 Subject: [PATCH] Objects are now used to represent also the tactic status. Cool (but error messages can be bad). --- .../grafite_engine/grafiteEngine.ml | 100 +++++++-------- .../components/grafite_engine/grafiteTypes.ml | 7 +- .../components/grafite_parser/nEstatus.ml | 14 ++- .../components/grafite_parser/nEstatus.mli | 3 +- .../components/lexicon/lexiconEngine.ml | 1 + .../components/lexicon/lexiconEngine.mli | 1 + .../components/ng_kernel/nCicLibrary.ml | 1 + .../components/ng_kernel/nCicLibrary.mli | 1 + .../components/ng_refiner/nCicCoercion.ml | 1 + .../components/ng_refiner/nCicCoercion.mli | 1 + .../components/ng_refiner/nCicUnifHint.ml | 1 + .../components/ng_refiner/nCicUnifHint.mli | 1 + .../components/ng_refiner/nRstatus.ml | 28 ++++- .../components/ng_refiner/nRstatus.mli | 4 +- .../components/ng_tactics/nTacStatus.ml | 105 ++++++++-------- .../components/ng_tactics/nTacStatus.mli | 90 ++++++++------ .../components/ng_tactics/nTactics.ml | 117 +++++++++--------- .../components/ng_tactics/nTactics.mli | 51 ++++---- helm/software/matita/matita.ml | 3 +- helm/software/matita/matitaMathView.ml | 15 +-- 20 files changed, 297 insertions(+), 248 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index e02bd159f..8edf316f6 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -660,14 +660,12 @@ let rec eval_ng_tac (text, prefix_len, tac) = ;; 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) = @@ -675,52 +673,49 @@ 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 = @@ -738,9 +733,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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 [] -> diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 82dae3d99..5d0ce025d 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -60,17 +60,14 @@ type status = { 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} ;; diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index 1dc05aa51..d7737cde9 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -11,8 +11,18 @@ (* $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 diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index 2c3acc751..e77f4e566 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -12,7 +12,8 @@ (* $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 diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 699af578b..4662ca6bd 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -52,6 +52,7 @@ class status = 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 = diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index 07eb8d298..4e404024d 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -36,6 +36,7 @@ class 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 diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 1cb3a118b..d54002d60 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -28,6 +28,7 @@ class 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 = diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index dfd17f15b..50ebf8f10 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -19,6 +19,7 @@ class 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 diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 29f28ba5c..d7fef8d8f 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -31,6 +31,7 @@ class 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 = diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 1a31172d2..0d96a7407 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -17,6 +17,7 @@ class status : object ('self) method coerc_db: db method set_coerc_db: db -> 'self + method set_coercion_status: status -> 'self end val empty_db: db diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index ccccfca88..6d80fe6ca 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -29,6 +29,7 @@ class status = 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");; diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index f7257d8f8..fa65d5277 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -17,6 +17,7 @@ class status : object ('self) method uhint_db: db method set_uhint_db: db -> 'self + method set_unifhint_status: status -> 'self end val index_hint: diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 736de4aa0..5ef83ec3c 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -11,11 +11,23 @@ (* $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 @@ -32,10 +44,20 @@ module Serializer = 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 diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 522d7e901..7fde1b747 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -12,10 +12,11 @@ (* $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: @@ -29,4 +30,5 @@ class dumpable_status : inherit status method dump: Serializer.obj list method set_dump: Serializer.obj list -> 'self + method set_dumpable_status: dumpable_status -> 'self end diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index cffda3b17..dc3816dab 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -14,30 +14,25 @@ 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 *) @@ -45,7 +40,7 @@ let ctx_of (_,c,_) = c ;; 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 && @@ -83,13 +78,13 @@ let relocate status destination (name,source,t as orig) = 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) ;; @@ -99,7 +94,7 @@ let term_of_cic_term s t c = ;; 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 ;; @@ -111,32 +106,31 @@ let disambiguate status t ty context = | 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) ;; @@ -144,11 +138,9 @@ let normalize status ?delta 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 = @@ -158,17 +150,15 @@ 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 ;; @@ -178,31 +168,31 @@ let instantiate status i t = 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) ;; @@ -241,7 +231,7 @@ let select_term 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 @@ -253,7 +243,7 @@ let select_term 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 -> @@ -336,6 +326,23 @@ 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 + 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 diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 307154127..f32511265 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -14,19 +14,13 @@ 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 @@ -34,52 +28,68 @@ 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 *) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 0be24856e..fe7f176a0 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -28,8 +28,8 @@ let print_tac print_status message status = ;; 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 *) @@ -43,12 +43,12 @@ let dot_tac status = (([ 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 *) @@ -56,12 +56,12 @@ let branch_tac status = | 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") @@ -70,12 +70,12 @@ let shift_tac status = :: (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 -> @@ -84,35 +84,35 @@ let pos_tac i_s status = :: (([ 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 = @@ -126,22 +126,22 @@ let focus_tac gs status = 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 @@ -150,7 +150,7 @@ let skip_tac status = else ([],t,k,tag) :: s in - { status with gstatus = new_gstatus } + status#set_stack gstatus ;; let block_tac l status = @@ -158,8 +158,8 @@ 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) ;; @@ -181,12 +181,16 @@ let compare_statuses ~past ~present = 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))); @@ -210,7 +214,10 @@ let distribute_tac tac status = 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))); @@ -219,7 +226,7 @@ let distribute_tac tac status = 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) ;; @@ -232,10 +239,9 @@ let try_tac tac status = ;; 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"))) @@ -248,20 +254,15 @@ let exact_tac t = distribute_tac (fun status goal -> 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 = @@ -286,9 +287,9 @@ let clear_tac names = 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 = @@ -467,8 +468,7 @@ let elim_tac ~what ~where = 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" @@ -572,7 +572,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> ;; let assert_tac seqs status = - match status.gstatus with + match status#stack with | [] -> assert false | (g,_,_,_) :: s -> assert (List.length g = List.length seqs); @@ -590,23 +590,22 @@ let assert_tac seqs status = 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) ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 95cf5c26f..ab049f1c3 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -11,49 +11,50 @@ (* $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 diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index cc46c7649..4bd7390f9 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -111,7 +111,8 @@ let _ = 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 diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 277dbe8f1..e93ac4f3c 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -798,9 +798,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 = @@ -825,7 +824,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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) @@ -863,13 +862,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 = @@ -1350,9 +1349,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 -- 2.39.2