X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=ba030806827beab9fd2c7f21b4ecb762139444d8;hb=f6c887944d48d718f372a57f1609f3d059908aa8;hp=eeca351c228f01462ce591e70569109d7c2642c4;hpb=dc83d986afedb519551b2509faa9f58e5baf022c;p=helm.git diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index eeca351c2..ba0308068 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -16,7 +16,7 @@ let fail msg = raise (Error msg) type lowtac_status = { pstatus : NCic.obj; - lstatus : LexiconEngine.status + estatus : NEstatus.extra_status; } type lowtactic = lowtac_status -> int -> lowtac_status @@ -80,11 +80,11 @@ let relocate status destination (name,source,t as orig) = (List.rev destination, List.rev source) in let lc = (0,NCic.Ctx (List.rev lc)) in - let db = NCicUnifHint.db () in (* XXX fixme *) let (metasenv, subst), t = NCicMetaSubst.delift ~unify:(fun m s c t1 t2 -> - try Some (NCicUnification.unify db m s c t1 t2) + try Some (NCicUnification.unify + status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2) with | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) @@ -113,12 +113,12 @@ let disambiguate status t ty context = let status, (_,_,x) = relocate status context ty in status, Some x in let uri,height,metasenv,subst,obj = status.pstatus in - let metasenv, subst, lexicon_status, t = + let metasenv, subst, estatus, t = GrafiteDisambiguate.disambiguate_nterm expty - status.lstatus context metasenv subst t + status.estatus context metasenv subst t in let new_pstatus = uri,height,metasenv,subst,obj in - { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) + { estatus = estatus; pstatus = new_pstatus }, (None, context, t) ;; let typeof status ctx t = @@ -135,12 +135,19 @@ let whd status ?delta ctx t = 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 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 (NCicUnifHint.db ()) metasenv subst ctx a b + NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b in { status with pstatus = n,h,metasenv,subst,o } ;; @@ -153,11 +160,9 @@ let refine status ctx term expty = let status, (n,_, e) = relocate status ctx e in status, n, Some e in let name,height,metasenv,subst,obj = status.pstatus in - let db = NCicUnifHint.db () in (* XXX fixme *) - let coercion_db = NCicCoercion.db () in - let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in + let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in let metasenv, subst, t, ty = - NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term expty + NCicRefiner.typeof rdb metasenv subst ctx term expty in { status with pstatus = name,height,metasenv,subst,obj }, (nt,ctx,t), (ne,ctx,ty) @@ -231,22 +236,23 @@ let select_term | NCicUnification.Uncertain _ -> false, status in let match_term status ctx (wanted : cic_term) t = - let rec aux ctx status t = + let rec aux ctx (status,already_found) t = let b, status = is_found status ctx t wanted in if b then let status , (_,_,t) = found status (None, ctx, t) in - status, t + (status,true),t else let _,_,_,subst,_ = status.pstatus in match t with | NCic.Meta (i,lc) when List.mem_assoc i subst -> let _,_,t,_ = NCicUtils.lookup_subst i subst in - aux ctx status t - | NCic.Meta _ -> status, t - | _ -> - NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t + aux ctx (status,already_found) t + | NCic.Meta _ -> (status,already_found),t + | _ -> + NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux + (status,already_found) t in - aux ctx status t + aux ctx (status,false) t in let _,_,_,subst,_ = low_status.pstatus in let rec select status ctx pat cic = @@ -296,9 +302,12 @@ let select_term | NCic.Implicit `Hole, t -> (match wanted with | Some wanted -> - let status, wanted = disambiguate status wanted None ctx in - match_term status ctx wanted t - | None -> match_term status ctx (None,ctx,t) t) + let status', wanted = disambiguate status wanted None ctx in + let (status',found), t' = match_term status' ctx wanted t in + if found then status',t' else status,t + | None -> + let (status,_),t = match_term status ctx (None,ctx,t) t in + status,t) | NCic.Implicit _, t -> status, t | _,t -> fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[] @@ -326,45 +335,8 @@ let analyse_indty status ty = let mk_cic_term c t = None,c,t ;; -(* CSC: next two functions to be moved elsewhere *) -let rec apply_subst subst ctx = - function - NCic.Meta (i,lc) -> - (try - let _,_,t,_ = NCicUtils.lookup_subst i subst in - let t = NCicSubstitution.subst_meta lc t in - apply_subst subst ctx t - with - Not_found -> - match lc with - _,NCic.Irl _ -> NCic.Meta (i,lc) - | n,NCic.Ctx l -> - NCic.Meta - (i,(0,NCic.Ctx - (List.map (fun t -> - apply_subst subst ctx (NCicSubstitution.lift n t)) l)))) - | t -> NCicUtils.map (fun item ctx -> item::ctx) ctx (apply_subst subst) t -;; - -let apply_subst_obj subst = - function - NCic.Constant (relev,name,bo,ty,attrs) -> - NCic.Constant - (relev,name,HExtlib.map_option (apply_subst subst []) bo, - apply_subst subst [] ty,attrs) - | NCic.Fixpoint (ind,fl,attrs) -> - let fl = - List.map - (function (relevance,name,recno,ty,bo) -> - relevance,name,recno,apply_subst subst [] ty,apply_subst subst [] bo - ) fl - in - NCic.Fixpoint (ind,fl,attrs) - | _ -> assert false (* not implemented yet *) -;; - let apply_subst status ctx t = let status, (name,_,t) = relocate status ctx t in let _,_,_,subst,_ = status.pstatus in - status, (name, ctx, apply_subst subst ctx t) + status, (name, ctx, NCicUntrusted.apply_subst subst ctx t) ;;