From 1bd6b7d2637d765f11ddbd1218d63474e9d0c63b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 May 2009 16:56:33 +0000 Subject: [PATCH] - pretty printer made robust in face of list_nth - bugfixed in generation of aliases in nCicLibrary: contructor index are 1-based - refinement of indtypes fixed: - missing undebujinate added - index for current indty was in the wrong order - apply_subst moved to nCicUntrusted - new iterator for obj_kind --- .../grafite_engine/grafiteEngine.ml | 6 ++- .../components/ng_kernel/nCicLibrary.ml | 2 +- helm/software/components/ng_kernel/nCicPp.ml | 6 ++- .../components/ng_kernel/nCicTypeChecker.ml | 4 +- .../components/ng_kernel/nCicUntrusted.ml | 49 +++++++++++++++++++ .../components/ng_kernel/nCicUntrusted.mli | 4 ++ .../components/ng_refiner/nCicRefiner.ml | 27 ++++++---- .../components/ng_tactics/nTacStatus.ml | 39 +-------------- .../components/ng_tactics/nTacStatus.mli | 3 -- 9 files changed, 85 insertions(+), 55 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 97af8a06f..4ab7412d8 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -758,7 +758,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status else let obj = prerr_endline "CSC: here we should fix the height!!!"; - uri,height,[],[],NTacStatus.apply_subst_obj subst obj + uri,height,[],[], + NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj in NCicLibrary.add_obj uri obj; {status with @@ -784,7 +785,8 @@ prerr_endline "CSC: here we should fix the height!!!"; (* CSC: cut&paste code from NQed *) let obj = prerr_endline "CSC: here we should fix the height!!!"; - uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj + uri,height,[],[], + NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst nsubst) nobj in NCicLibrary.add_obj uri obj; {status with diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 86822aa74..e2d800157 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -56,7 +56,7 @@ let add_obj u obj = HExtlib.list_mapi (fun (_,cname,_) j-> u,cname, - NReference.reference_of_spec u (NReference.Con (i,j,leftno)) + NReference.reference_of_spec u (NReference.Con (i,j+1,leftno)) ) cl @ [u,iname, NReference.reference_of_spec u diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 6a38873fc..47cdfa3ca 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -43,7 +43,11 @@ let r2s pp_fix_name r = else NUri.name_of_uri u ^"("^ string_of_int i ^ ")" | _ -> assert false) - with NCicLibrary.ObjectNotFound _ -> R.string_of_reference r + with + | NCicLibrary.ObjectNotFound _ + | Failure "nth" + | Invalid_argument "List.nth" -> R.string_of_reference r + ;; let string_of_implicit_annotation = function diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index f459c6024..65f17ee38 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -350,7 +350,9 @@ let type_of_branch ~subst context leftno outty cons tycons = | t -> C.Appl [t ; C.Rel 1] in C.Prod (name,so, aux (liftno+1) ((name,(C.Decl so))::context) cons de) - | _ -> raise (AssertFailure (lazy "type_of_branch")) + | t -> raise (AssertFailure + (lazy ("type_of_branch, the contructor has type: " ^ NCicPp.ppterm + ~metasenv:[] ~context:[] ~subst:[] t))) in aux 0 context cons tycons ;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 4dcf01c53..95f40da53 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -95,3 +95,52 @@ let mk_appl he args = | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (he::args) ;; + +let map_obj_kind f = + function + NCic.Constant (relev,name,bo,ty,attrs) -> + NCic.Constant (relev,name,HExtlib.map_option f bo, f ty,attrs) + | NCic.Fixpoint (ind,fl,attrs) -> + let fl = + List.map + (function (relevance,name,recno,ty,bo) -> relevance,name,recno,f ty,f bo) + fl + in + NCic.Fixpoint (ind,fl,attrs) + | NCic.Inductive (is_ind,lno,itl,attrs) -> + let itl = + List.map + (fun (relevance,name,ty,cl) -> + let cl = + List.map (fun (relevance, name, ty) -> + relevance, name, f ty) + cl + in + relevance, name, f ty, cl) + itl + in + NCic.Inductive (is_ind,lno,itl,attrs) +;; + +let apply_subst subst t = + let rec apply_subst subst () = + 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 () 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 () (NCicSubstitution.lift n t)) l)))) + | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t + in + apply_subst subst () t +;; + diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 79ac48c38..31be9c0d2 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -15,8 +15,12 @@ val map_term_fold_a: (NCic.hypothesis -> 'k -> 'k) -> 'k -> ('k -> 'a -> NCic.term -> 'a * NCic.term) -> 'a -> NCic.term -> 'a * NCic.term +val map_obj_kind: (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind + val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list module NCicHash : Hashtbl.S with type key = NCic.term val mk_appl : NCic.term -> NCic.term list -> NCic.term + +val apply_subst : NCic.substitution -> NCic.term -> NCic.term diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 4807e5271..e38842ac8 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -538,19 +538,19 @@ let typeof_obj hdb ?(localise=fun _ -> Stdpp.dummy_loc) ~look_for_coercion (uri,height,metasenv,subst,obj) = - let check_type metasenv subst (ty as orig_ty) = (* XXX fattorizza *) + let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *) let metasenv, subst, ty, sort = - typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None + typeof hdb ~localise ~look_for_coercion metasenv subst context ty None in let metasenv, subst, ty, sort = force_to_sort hdb ~look_for_coercion - metasenv subst [] ty orig_ty localise sort + metasenv subst context ty orig_ty localise sort in metasenv, subst, ty, sort in match obj with | C.Constant (relevance, name, bo, ty , attr) -> - let metasenv, subst, ty, _ = check_type metasenv subst ty in + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in let metasenv, subst, bo, ty, height = match bo with | Some bo -> @@ -569,7 +569,7 @@ let typeof_obj hdb let types, metasenv, subst, rev_fl = List.fold_left (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) -> - let metasenv, subst, ty, _ = check_type metasenv subst ty in + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in let dbo = NCicTypeChecker.debruijn uri len [] bo in let localise = relocalise localise dbo bo in (name,C.Decl ty)::types, @@ -606,7 +606,7 @@ let typeof_obj hdb let metasenv,subst,rev_itl,tys = List.fold_left (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) -> - let metasenv, subst, ty, _ = check_type metasenv subst ty in + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx ) (metasenv,subst,[],[]) itl in let metasenv,subst,itl,_ = @@ -666,7 +666,9 @@ let typeof_obj hdb ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev with Invalid_argument "List.fold_left2" -> assert false in - let metasenv, subst, te, con_sort = check_type metasenv subst te in + let metasenv, subst, te, con_sort = + check_type metasenv subst context te + in (match NCicReduction.whd ~subst context con_sort, NCicReduction.whd ~subst [] ty_sort @@ -698,11 +700,18 @@ let typeof_obj hdb (lazy (localise te, "Non positive occurence in " ^ NUri.string_of_uri uri))) else + let te = + NCicSubstitution.psubst + (fun i -> NCic.Const (NReference.reference_of_spec uri + (NReference.Ind (ind,i,leftno)))) + (List.rev (HExtlib.list_seq 0 (List.length itl))) + te + in metasenv,subst,(k_relev,n,te)::res ) cl (metasenv,subst,[]) in - metasenv,subst,(it_relev,n,ty,cl)::res,i-1 - ) (metasenv,subst,[],List.length rev_itl) rev_itl + metasenv,subst,(it_relev,n,ty,cl)::res,i+1 + ) (metasenv,subst,[],1) rev_itl in uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr) ;; diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index eeca351c2..323b1e6fc 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -326,45 +326,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 t) ;; diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 59ef35592..0653223af 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -60,9 +60,6 @@ val refine: val apply_subst: lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term -(* CSC: this function must be moved elsewhere *) -val apply_subst_obj: NCic.substitution -> NCic.obj_kind -> NCic.obj_kind - val get_goalty: lowtac_status -> int -> cic_term val mk_meta: lowtac_status -> ?name:string -> NCic.context -> -- 2.39.2