From: Enrico Tassi Date: Wed, 11 Feb 2009 16:27:33 +0000 (+0000) Subject: some work to refine objs X-Git-Tag: make_still_working~4205 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46b91f34b693dabbd351ba813f5190051b09a117;p=helm.git some work to refine objs --- diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index bfe12cee7..4e3f8cac3 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -69,9 +69,9 @@ let find_in_context name context = in aux 1 context -let interpretate_term - ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast - ~localization_tbl +let interpretate_term_and_interpretate_term_option + ?(create_dummy_ids=false) + ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -269,103 +269,7 @@ let interpretate_term in let cic_body = aux ~localize loc (cic_name :: context) body in NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) - | CicNotationPt.LetRec (_kind, _defs, _body) -> - assert false (* - let context' = - List.fold_left - (fun acc (_, (name, _), _, _) -> - cic_name_of_name name :: acc) - context defs - in - let cic_body = - let unlocalized_body = aux ~localize:false loc context' body in - match unlocalized_body with - NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n - | NCic.Appl (NCic.Rel n::l) when n <= List.length defs -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] (List.length defs) t - in - assert (subst=[]); - assert (metasenv=[]); - t') l - in - (* We can avoid the LetIn. But maybe we need to recompute l' - so that it is localized *) - if localize then - match body with - CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> - (* since we avoid the letin, the context has no - * recfuns in it *) - let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn (n,l') - | _ -> assert false - else - `AvoidLetIn (n,l') - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body) - | _ -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body - in - let inductiveFuns = - List.map - (fun (params, (name, typ), body, decr_idx) -> - let add_binders kind t = - List.fold_right - (fun var t -> CicNotationPt.Binder (kind, var, t)) params t - in - let cic_body = - aux ~localize loc context' (add_binders `Lambda body) in - let cic_type = - aux_option ~localize loc context (Some `Type) - (HExtlib.map_option (add_binders `Pi) typ) in - let name = - match cic_name_of_name name with - | NCic.Anonymous -> - CicNotationPt.fail loc - "Recursive functions cannot be anonymous" - | NCic.Name name -> name - in - (name, decr_idx, cic_type, cic_body)) - defs - in - let fix_or_cofix n = - match kind with - `Inductive -> NCic.Fix (n,inductiveFuns) - | `CoInductive -> - let coinductiveFuns = - List.map - (fun (name, _, typ, body) -> name, typ, body) - inductiveFuns - in - NCic.CoFix (n,coinductiveFuns) - in - let counter = ref ~-1 in - let build_term _ (var,_,ty,_) t = - incr counter; - NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t) - in - (match cic_body with - `AvoidLetInNoAppl n -> - let n' = List.length inductiveFuns - n in - fix_or_cofix n' - | `AvoidLetIn (n,l) -> - let n' = List.length inductiveFuns - n in - NCic.Appl (fix_or_cofix n'::l) - | `AddLetIn cic_body -> - List.fold_right (build_term inductiveFuns) inductiveFuns - cic_body) -*) + | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed | CicNotationPt.Ident (name, subst) -> @@ -373,7 +277,9 @@ let interpretate_term (try NCic.Rel (find_in_context name context) with Not_found -> - Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) + try NCic.Const (List.assoc name obj_context) + with Not_found -> + Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) | CicNotationPt.Uri (name, subst) -> assert (subst = None); (try @@ -420,16 +326,193 @@ patterns not implemented *) | Some CicNotationPt.Implicit -> NCic.Implicit annotation | Some term -> aux ~localize loc context term in - aux ~localize:true HExtlib.dummy_floc context ast + (fun ~context -> aux ~localize:true HExtlib.dummy_floc context), + (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context) +;; let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl + ~obj_context ~localization_tbl ~mk_choice += + let context = List.map fst context in + fst + (interpretate_term_and_interpretate_term_option + ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl) + ~context ast +;; + +let interpretate_term_option + ?(create_dummy_ids=false) ~context ~env ~uri ~is_path + ~localization_tbl ~mk_choice ~obj_context = let context = List.map fst context in - interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast -~localization_tbl + snd + (interpretate_term_and_interpretate_term_option + ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl) + ~context +;; + +let new_flavour_of_flavour = function + | `Definition -> `Definition + | `MutualDefinition -> `Definition + | `Fact -> `Fact + | `Lemma -> `Lemma + | `Remark -> `Corollary + | `Theorem -> `Theorem + | `Variant -> `Corollary + | `Axiom -> `Fact ;; +(* +let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast + ~localization_tbl += + assert (context = []); + assert (is_path = false); + let interpretate_term ?(obj_context=[]) = + interpretate_term ~mk_choice ~localization_tbl ~obj_context in + let interpretate_term_option ?(obj_context=[]) = + interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in + match obj with + | CicNotationPt.Theorem (flavour, name, ty, bo) -> + let attrs = `Provided, new_flavour_of_flavour flavour in + let ty' = interpretate_term [] env None false ty in + let height = (* XXX calculate *) 0 in + uri, height, [], [], + (match bo,flavour with + None,`Axiom -> + NCic.Constant (name,None,ty',attrs) + | Some bo,`Axiom -> assert false + | None,_ -> + NCic.Constant (name,NCic.Implicit None,ty',attrs) + | Some bo,_ -> + match bo with + | CicNotationPt.LetRec (kind, defs, _) -> + let inductive = kind = `Inductive in + let obj_context = + List.split + (List.fold_left + (fun (i,acc) (_,(name,_),_,k) -> + ((name, NReference.reference_of_spec uri + (if inductive then NReference.Fix (i,k,0) + else NReference.CoFix i)) :: acc) + (0,[]) defs)) + in + let inductiveFuns = + List.map + (fun (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> + CicNotationPt.Binder (kind, var, t)) params t + in + let cic_body = + interpretate_term ~context ~env ~uri:None ~is_path:false + (add_binders `Lambda body) + in + let cic_type = + interpretate_term_option ~context ~env ~uri:None + ~is_path:false `Type + (HExtlib.map_option (add_binders `Pi) typ) + in + (name, decr_idx, cic_type, cic_body)) + defs + in + NCic.Fixpoint (inductive,inductiveFuns,attrs) + | bo -> + let bo = + interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo + in + NCic.Constant (name,Some bo,ty',attrs)) + | _ -> assert false +(* + | CicNotationPt.Inductive (params,tyl) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let obj_context = + snd ( + List.fold_left + (*here the explicit_named_substituion is assumed to be of length 0 *) + (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res) + (0,[]) tyl) in + let tyl = + List.map + (fun (name,b,ty,cl) -> + let ty' = add_params (interpretate_term context env None false ty) in + let cl' = + List.map + (fun (name,ty) -> + let ty' = + add_params + (interpretate_term ~obj_context ~context ~env ~uri:None + ~is_path:false ty) + in + name,ty' + ) cl + in + name,b,ty',cl' + ) tyl + in + Cic.InductiveDefinition (tyl,[],List.length params,[]) + | CicNotationPt.Record (params,name,ty,fields) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right + (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let ty' = add_params (interpretate_term context env None false ty) in + let fields' = + snd ( + List.fold_left + (fun (context,res) (name,ty,_coercion,arity) -> + let context' = Cic.Name name :: context in + context',(name,interpretate_term context env None false ty)::res + ) (context,[]) fields) in + let concl = + (*here the explicit_named_substituion is assumed to be of length 0 *) + let mutind = Cic.MutInd (uri,0,[]) in + if params = [] then mutind + else + Cic.Appl + (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left + (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) + concl fields' in + let con' = add_params con in + let tyl = [name,true,ty',["mk_" ^ name,con']] in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in + Cic.InductiveDefinition + (tyl,[],List.length params,[`Class (`Record field_names)]) +*) +;; +*) + let disambiguate_term ~context ~metasenv ~subst ?goal ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~coercion_db ~lookup_in_library @@ -459,7 +542,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) + ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term) ~mk_localization_tbl ~hint ~subst in diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 55a42a176..3784d5c18 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -33,3 +33,4 @@ val disambiguate_term : NCic.substitution * NCic.term) list * bool + diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index c5ccff2a4..24701683e 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -53,3 +53,5 @@ val check_allowed_sort_elimination : NReference.reference -> NCic.context -> NCic.term -> NCic.term -> NCic.term -> unit +val debruijn: NUri.uri -> int -> NCic.context -> NCic.term -> NCic.term + diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index b5782bd03..be6760bf1 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -142,3 +142,11 @@ let mk_cofix i = function reference_of_string (string_of_reference (Ref (u, CoFix i))) | _ -> assert false ;; + +let reference_of_spec u spec = + reference_of_string (string_of_reference (Ref (u, spec))) +;; + + + + diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index 1de23ad8b..d291b621b 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -23,6 +23,8 @@ type spec = type reference = private Ref of NUri.uri * spec +val reference_of_spec: NUri.uri -> spec -> reference + val eq: reference -> reference -> bool val string_of_reference: reference -> string val reference_of_string: string -> reference 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: *) diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index 2df108697..d43a09f20 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -31,3 +31,16 @@ val typeof : NCic.metasenv * NCic.substitution * NCic.term * NCic.term (* menv, subst,refined term, type *) +val typeof_obj : + NCicUnifHint.db -> + ?localise:(NCic.term -> Stdpp.location) -> + look_for_coercion:( + NCic.metasenv -> NCic.substitution -> NCic.context -> + (* inferred type, expected type *) + NCic.term -> NCic.term -> + (* enriched metasenv, new term, its type, metavriable to + * be unified with the old term *) + (NCic.metasenv * NCic.term * NCic.term * NCic.term) list + ) -> + NCic.obj -> NCic.obj +