From 044618edc33fa1cf00ec345e84c2a62939746751 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 20 Jan 2004 10:25:10 +0000 Subject: [PATCH] First version of refine for MutCase, still largely incomplete. --- helm/ocaml/cic_unification/cicMkImplicit.ml | 28 ++++ helm/ocaml/cic_unification/cicMkImplicit.mli | 12 ++ helm/ocaml/cic_unification/cicRefine.ml | 128 ++++++++++++++++++- helm/ocaml/cic_unification/cicUnification.ml | 4 +- 4 files changed, 170 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 24a94514e..0ee364053 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -33,6 +33,34 @@ let mk_implicit metasenv context = newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) +let n_fresh_metas metasenv context n = + if n = 0 then metasenv, [] + else + let irl = identity_relocation_list_for_metavariable context in + let newmeta = new_meta metasenv in + let rec aux newmeta n = + if n = 0 then metasenv, [] + else + let metasenv', l = aux (newmeta + 3) (n-1) in + (newmeta, context, Cic.Sort Cic.Type):: + (newmeta + 1, context, Cic.Meta (newmeta, irl)):: + (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', + Cic.Meta(newmeta+2,irl)::l in + aux newmeta n + +let fresh_subst metasenv context uris = + let irl = identity_relocation_list_for_metavariable context in + let newmeta = new_meta metasenv in + let rec aux newmeta = function + [] -> metasenv, [] + | uri::tl -> + let metasenv', l = aux (newmeta + 3) tl in + (newmeta, context, Cic.Sort Cic.Type):: + (newmeta + 1, context, Cic.Meta (newmeta, irl)):: + (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', + (uri,Cic.Meta(newmeta+2,irl))::l in + aux newmeta uris + let mk_implicit' metasenv context = let (metasenv, index) = mk_implicit metasenv context in (metasenv, index - 1, index) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 919027b02..a698386b5 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -14,6 +14,18 @@ val new_meta : Cic.metasenv -> int * @return the new metasenv and the index of the added conjecture *) val mk_implicit: Cic.metasenv -> Cic.context -> Cic.metasenv * int +(** [mk_implicit metasenv context] create n fresh metavariables *) +val n_fresh_metas: + Cic.metasenv -> Cic.context -> int -> Cic.metasenv * Cic.term list + +(** [mk_implicit metasenv context] takes in input a list of uri and +creates a fresh explicit substitution *) +val fresh_subst: + Cic.metasenv -> + Cic.context -> + UriManager.uri list -> + Cic.metasenv * (Cic.term Cic.explicit_named_substitution) + (** as above but return both the index of the added conjecture (2nd index) and * the index of its type (1st index) *) val mk_implicit': Cic.metasenv -> Cic.context -> Cic.metasenv * int * int diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index ba79ce922..d822ec341 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -28,11 +28,13 @@ exception NotRefinable of string;; exception Uncertain of string;; exception WrongUriToConstant of string;; exception WrongUriToVariable of string;; +exception ListTooShort;; exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; exception MetasenvInconsistency;; exception MutCaseFixAndCofixRefineNotImplemented;; exception FreeMetaFound of int;; +exception WrongArgumentNumber;; let fdebug = ref 0;; let debug t context = @@ -46,6 +48,13 @@ let debug t context = (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) ;; +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> raise ListTooShort +;; + let rec type_of_constant uri = let module C = Cic in let module R = CicReduction in @@ -85,6 +94,42 @@ and type_of_mutual_inductive_constr uri i j = | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) + +(* the check_branch function checks if a branch of a case is refinable. + It returns a pair (outype_instance,args), a subst and a metasenv. + outype_instance is the expected result of applying the case outtype + to args. + The problem is that outype is in general unknown, and we should + try to synthesize it from the above information, that is in general + a second order unification problem. *) + +and check_branch context metasenv subst left_args_no actualtype term expectedtype = + let module C = Cic in + let module R = CicReduction in + let module Un = CicUnification in + match R.whd context expectedtype with + C.MutInd (_,_,_) -> + (actualtype, [term]), subst, metasenv + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl left_args_no in + (actualtype, arguments@[term]), subst, metasenv + | C.Prod (name,so,de) -> + (* we expect that the actual type of the branch has the due + number of Prod *) + (match R.whd context actualtype with + C.Prod (name',so',de') -> + let subst,metsaenv = + Un.fo_unif_subst subst context metasenv so so' in + let term' = + (match CicSubstitution.lift 1 term with + C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1]) in + (* we should also check that the name variable is anonymous in + the actual type de' ?? *) + check_branch ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de + | _ -> raise WrongArgumentNumber) + | _ -> raise (NotRefinable "Prod or MutInd expected") + and type_of_aux' metasenv context t = let rec type_of_aux subst metasenv context = let module C = Cic in @@ -209,7 +254,78 @@ and type_of_aux' metasenv context t = (type_of_mutual_inductive_constr uri i j) in cty,subst',metasenv' - | C.MutCase _ + | C.MutCase (uri, i, outtype, term, pl) -> + (* first, get the inductive type (and noparams) in the environment *) + let (_,b,arity,constructors), expl_params, no_left_params = + match CicEnvironment.get_cooked_obj ~trust:true uri with + C.InductiveDefinition (l,expl_params,parsno) -> + List.nth l i , expl_params, parsno + | _ -> + raise + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in + let rec count_prod t = + match CicReduction.whd context t with + C.Prod (_, _, t) -> 1 + (count_prod t) + | _ -> 0 in + let no_args = count_prod arity in + (* now, create a "generic" MutInd *) + let metasenv,left_args = + CicMkImplicit.n_fresh_metas metasenv context no_left_params in + let metasenv,right_args = + let no_right_params = no_args - no_left_params in + if no_right_params < 0 then assert false + else CicMkImplicit.n_fresh_metas metasenv context no_right_params in + let metasenv,exp_named_subst = + CicMkImplicit.fresh_subst metasenv context expl_params in + let expected_type = + if no_args = 0 then + C.MutInd (uri,i,exp_named_subst) + else + C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args)) + in + (* check consistency with the actual type of term *) + let actual_type,subst,metasenv = + type_of_aux subst metasenv context term in + let subst,metasenv = + Un.fo_unif_subst + subst + context + metasenv expected_type (CicReduction.whd context actual_type) in + (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *) + let (_,outtypeinstances,subst,metasenv) = + List.fold_left + (fun (j,outtypeinstances,subst,metasenv) p -> + let constructor = + if left_args = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl + (C.MutConstruct (uri,i,j,exp_named_subst)::left_args)) + in + let actual_type,subst,metasenv = + type_of_aux subst metasenv context p in + let expected_type, subst, metasenv = + type_of_aux subst metasenv context constructor in + let outtypeinstance,subst,metasenv = + check_branch + context metasenv subst + no_left_params actual_type constructor expected_type in + (j+1,outtypeinstance::outtypeinstances,subst,metasenv)) + (1,[],subst,metasenv) pl in + (* we are left to check that the outype matches his instances. + The easy case is when the outype is specified, that amount + to a trivial check. Otherwise, we should guess a type from + its instances *) + (* easy case *) + let (subst,metasenv) = + List.fold_left + (fun (subst,metasenv) (instance,args) -> + let instance' = + CicReduction.whd context (C.Appl(outtype::args)) in + Un.fo_unif_subst subst context metasenv instance instance') + (subst,metasenv) outtypeinstances in + CicReduction.whd + context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix _ | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented @@ -366,3 +482,13 @@ let type_of_aux' metasenv context term = prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; raise e ;; + + + + + + + + + + diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index dd33f3e44..164a9cdce 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -33,7 +33,8 @@ exception OpenTerm;; (* the delift function takes in input an ordered list of optional terms *) (* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *) -(* rel(k). Typically, the list of optional terms is the explicit substitution *)(* that is applied to a metavariable occurrence and the result of the delift *) +(* rel(k). Typically, the list of optional terms is the explicit substitution *) +(* that is applied to a metavariable occurrence and the result of the delift *) (* function is a term the implicit variable can be substituted with to make *) (* the term [t] unifiable with the metavariable occurrence. *) (* In general, the problem is undecidable if we consider equivalence in place *) @@ -498,6 +499,7 @@ let unwind metasenv subst unwinded t = (* during the unwinding the eta-expansions are undone. *) let apply_subst_reducing subst meta_to_reduce t = + (* andrea: che senso ha questo ref ?? *) let unwinded = ref subst in let rec um_aux = let module C = Cic in -- 2.39.2