X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=6779667d9ca8f4bd4bf83cb6ea2bc9edcc31a688;hb=5338da4d7047b18aacd43447a3261b531895291d;hp=73634e7e0757e2ac3a477cfb0a1b4b092ab4544c;hpb=128b9b9d2a5da45e177f3280cd84a07a1306c86a;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 73634e7e0..6779667d9 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -451,4 +451,193 @@ and eat_prods hdb aux metasenv subst [] he ty_he args (*D*)in outside(); rc with exc -> outside (); raise exc ;; + +let rec first f l1 l2 = + match l1,l2 with + | x1::tl1, x2::tl2 -> + (try f x1 x2 with Not_found -> first f tl1 tl2) + | _ -> raise Not_found +;; + +let rec find add dt t = + if dt == add then t + else + let dl, l = + match dt, t with + | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l)) + | C.Appl dl,C.Appl l -> dl,l + | C.Lambda (_,ds,dt), C.Lambda (_,s,t) + | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t] + | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t] + | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l) + | _ -> raise Not_found + in + first (find add) dl l +;; + +let relocalise old_localise dt t add = + old_localise + (try find add dt t with Not_found -> assert false) +;; + +let undebruijnate inductive ref t rev_fl = + NCicSubstitution.psubst (fun x -> x) + (HExtlib.list_mapi + (fun (_,_,rno,_,_,_) i -> + NCic.Const + (if inductive then NReference.mk_fix i rno ref + else NReference.mk_cofix i ref)) + rev_fl) + t +;; + + +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 metasenv, subst, ty, sort = + typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None + in + let metasenv, subst, ty, _ = + force_to_sort hdb ~look_for_coercion + metasenv subst [] ty orig_ty localise sort + in + metasenv, subst, ty + in + match obj with + | C.Constant (relevance, name, bo, ty , attr) -> + let metasenv, subst, ty = check_type metasenv subst ty in + let metasenv, subst, bo, ty, height = + match bo with + | Some bo -> + let metasenv, subst, bo, ty = + typeof hdb ~localise ~look_for_coercion + metasenv subst [] bo (Some ty) + in + let height = (* XXX recalculate *) height in + metasenv, subst, Some bo, ty, height + | None -> metasenv, subst, None, ty, 0 + in + uri, height, metasenv, subst, + C.Constant (relevance, name, bo, ty, attr) + | C.Fixpoint (inductive, fl, attr) -> + let len = List.length fl in + 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 dbo = NCicTypeChecker.debruijn uri len [] bo in + let localise = relocalise localise dbo bo in + (name,C.Decl ty)::types, + metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl + ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *) + in + let metasenv, subst, fl = + List.fold_left + (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) -> + let metasenv, subst, dbo, ty = + typeof hdb ~localise ~look_for_coercion + metasenv subst types dbo (Some ty) + in + metasenv, subst, (relevance,name,k,ty,dbo)::fl) + (metasenv, subst, []) rev_fl + in + let height = (* XXX recalculate *) height in + let fl = + List.map + (fun (relevance,name,k,ty,dbo) -> + let bo = + undebruijnate inductive + (NReference.reference_of_spec uri + (if inductive then NReference.Fix (0,k,0) + else NReference.CoFix 0)) dbo rev_fl + in + relevance,name,k,ty,bo) + fl + in + uri, height, metasenv, subst, + C.Fixpoint (inductive, fl, attr) + + | C.Inductive (ind, leftno, itl, attr) -> assert false +(* + (* let's check if the arity of the inductive types are well formed *) + List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl; + (* let's check if the types of the inductive constructors are well formed. *) + let len = List.length tyl in + let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in + ignore + (List.fold_right + (fun (it_relev,_,ty,cl) i -> + let context,ty_sort = split_prods ~subst [] ~-1 ty in + let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in + List.iter + (fun (k_relev,_,te) -> + let _,k_relev = HExtlib.split_nth leftno k_relev in + let te = debruijn uri len [] te in + let context,te = split_prods ~subst tys leftno te in + let _,chopped_context_rev = + HExtlib.split_nth (List.length tys) (List.rev context) in + let sx_context_te_rev,_ = + HExtlib.split_nth leftno chopped_context_rev in + (try + ignore (List.fold_left2 + (fun context item1 item2 -> + let convertible = + match item1,item2 with + (n1,C.Decl ty1),(n2,C.Decl ty2) -> + n1 = n2 && + R.are_convertible ~metasenv ~subst context ty1 ty2 + | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> + n1 = n2 + && R.are_convertible ~metasenv ~subst context ty1 ty2 + && R.are_convertible ~metasenv ~subst context bo1 bo2 + | _,_ -> false + in + if not convertible then + raise (TypeCheckerFailure (lazy + ("Mismatch between the left parameters of the constructor " ^ + "and those of its inductive type"))) + else + item1::context + ) [] sx_context_ty_rev sx_context_te_rev) + with Invalid_argument "List.fold_left2" -> assert false); + let con_sort = typeof ~subst ~metasenv context te in + (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with + (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> + if not (E.universe_leq u1 u2) then + raise + (TypeCheckerFailure + (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^ + " of the constructor is not included in the inductive" ^ + " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2))) + | C.Sort _, C.Sort C.Prop + | C.Sort _, C.Sort C.Type _ -> () + | _, _ -> + raise + (TypeCheckerFailure + (lazy ("Wrong constructor or inductive arity shape")))); + (* let's check also the positivity conditions *) + if + not + (are_all_occurrences_positive ~subst context uri leftno + (i+leftno) leftno (len+leftno) te) + then + raise + (TypeCheckerFailure + (lazy ("Non positive occurence in "^NUri.string_of_uri + uri))) + else check_relevance ~subst ~metasenv context k_relev te) + cl; + check_relevance ~subst ~metasenv [] it_relev ty; + i+1) + tyl 1) +*) + + +;; + + + (* vim:set foldmethod=marker: *)