X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=5c031f4733b6806f2da7c1b9ef683d8d589112ec;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=57e4c5e9d6fff45e438c96cc7f4b3f781ee71700;hpb=47c9a0967ce271e551d4cbc8ac388097d774a3ef;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 57e4c5e9d..5c031f473 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -287,7 +287,7 @@ and type_of_aux' metasenv context t ugraph = * Moreover the inferred type is closer to the expected one. *) C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, - subst',metasenv',ugraph2 + subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph @@ -506,9 +506,9 @@ and type_of_aux' metasenv context t ugraph = (Some candidate),ugraph4,metasenv,subst | (constructor_args_no,_,instance,_)::tl -> try - let instance' = - CicSubstitution.delift constructor_args_no - (CicMetaSubst.apply_subst subst instance) + let instance',subst,metasenv = + CicMetaSubst.delift_rels subst metasenv + constructor_args_no instance in let candidate,ugraph,metasenv,subst = List.fold_left ( @@ -518,10 +518,9 @@ and type_of_aux' metasenv context t ugraph = | None -> None,ugraph,metasenv,subst | Some ty -> try - let instance' = - CicSubstitution.delift - constructor_args_no - (CicMetaSubst.apply_subst subst instance) + let instance',subst,metasenv = + CicMetaSubst.delift_rels subst metasenv + constructor_args_no instance in let subst,metasenv,ugraph = fo_unif_subst subst context metasenv @@ -529,7 +528,7 @@ and type_of_aux' metasenv context t ugraph = in candidate_oty,ugraph,metasenv,subst with - CicSubstitution.DeliftingWouldCaptureAFreeVariable + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> None,ugraph,metasenv,subst @@ -549,7 +548,7 @@ and type_of_aux' metasenv context t ugraph = Some (add_lambdas 0 t arity_instantiated_with_left_args), ugraph,metasenv,subst - with CicSubstitution.DeliftingWouldCaptureAFreeVariable -> + with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> None,ugraph4,metasenv,subst in match candidate with @@ -560,7 +559,9 @@ and type_of_aux' metasenv context t ugraph = candidate outtype ugraph5 in C.MutCase (uri, i, outtype, term', pl'), - (Cic.Appl (outtype::right_args@[term'])), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) let _,_, subst, metasenv,ugraph5 = @@ -585,8 +586,9 @@ and type_of_aux' metasenv context t ugraph = (subst,metasenv,ugraph5) outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), - CicReduction.whd ~subst context - (C.Appl(outtype::right_args@[term])), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (C.Appl(outtype::right_args@[term]))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> let fl_ty',subst,metasenv,types,ugraph1 = @@ -962,7 +964,99 @@ let type_of_aux' metasenv context term ugraph = type_of_aux' metasenv context term ugraph with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg) + +(*CSC: this is a very very rough approximation; to be finished *) +let are_all_occurrences_positive uri = + let rec aux = + (*CSC: here we should do a whd; but can we do that? *) + function + Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> () + | Cic.MutInd (uri',_,_) when uri = uri' -> () + | Cic.Prod (_,_,t) -> aux t + | _ -> raise (RefineFailure "not well formed constructor type") + in + aux +let typecheck metasenv uri obj = + let ugraph = CicUniv.empty_ugraph in + match obj with + Cic.Constant (name,Some bo,ty,args,attrs) -> + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph + | Cic.Constant (name,None,ty,args,attrs) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> + assert (metasenv' = metasenv); + (* Here we do not check the metasenv for correctness *) + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + begin + match sort with + Cic.Sort _ + (* instead of raising Uncertain, let's hope that the meta will become + a sort *) + | Cic.Meta _ -> () + | _ -> raise (RefineFailure "The term provided is not a type") + end; + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph + | Cic.Variable _ -> assert false (* not implemented *) + | Cic.InductiveDefinition (tys,args,paramsno,attrs) -> + (*CSC: this code is greately simplified and many many checks are missing *) + (*CSC: e.g. the constructors are not required to build their own types, *) + (*CSC: the arities are not required to have as type a sort, etc. *) + let uri = match uri with Some uri -> uri | None -> assert false in + let typesno = List.length tys in + (* first phase: we fix only the types *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + metasenv,ugraph,(name,b,ty',cl)::res + ) tys (metasenv,ugraph,[]) in + let con_context = + List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in + (* second phase: we fix only the constructors *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let metasenv,ugraph,cl' = + List.fold_right + (fun (name,ty) (metasenv,ugraph,res) -> + let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty',_,metasenv,ugraph = + type_of_aux' metasenv con_context ty ugraph in + let undebrujin t = + snd + (List.fold_right + (fun (name,_,_,_) (i,t) -> + (* here the explicit_named_substituion is assumed to be *) + (* of length 0 *) + let t' = Cic.MutInd (uri,i,[]) in + let t = CicSubstitution.subst t' t in + i - 1,t + ) tys (typesno - 1,t)) in + let ty' = undebrujin ty' in + metasenv,ugraph,(name,ty')::res + ) cl (metasenv,ugraph,[]) + in + metasenv,ugraph,(name,b,ty,cl')::res + ) tys (metasenv,ugraph,[]) in + (* third phase: we check the positivity condition *) + List.iter + (fun (_,_,_,cl) -> + List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl + ) tys ; + Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph (* DEBUGGING ONLY let type_of_aux' metasenv context term =