X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=b3525d3182bcec3737d02c2883cd7402d1acf730;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38;hpb=da11c92be86c24285ef1a4d0ddfe1e074a6b322a;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 06398da9a..b3525d318 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -26,16 +26,8 @@ open Printf exception RefineFailure of string;; - -exception Impossible of int;; -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 WrongArgumentNumber;; +exception AssertFailure of string;; let debug_print = prerr_endline @@ -51,7 +43,7 @@ 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 + | (_,_) -> raise (AssertFailure "split: list too short") ;; let rec type_of_constant uri = @@ -61,7 +53,9 @@ let rec type_of_constant uri = match CicEnvironment.get_cooked_obj uri with C.Constant (_,_,ty,_) -> ty | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) and type_of_variable uri = let module C = Cic in @@ -69,7 +63,10 @@ and type_of_variable uri = let module U = UriManager in match CicEnvironment.get_cooked_obj uri with C.Variable (_,_,ty,_) -> ty - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unknown variable definition " ^ UriManager.string_of_uri uri)) and type_of_mutual_inductive_defs uri i = let module C = Cic in @@ -79,7 +76,10 @@ and type_of_mutual_inductive_defs uri i = C.InductiveDefinition (dl,_,_) -> let (_,_,arity,_) = List.nth dl i in arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) and type_of_mutual_inductive_constr uri i j = let module C = Cic in @@ -90,7 +90,10 @@ and type_of_mutual_inductive_constr uri i j = let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -105,7 +108,6 @@ and type_of_mutual_inductive_constr uri i j = and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in let module R = CicMetaSubst in - let module Un = CicUnification in match R.whd subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv @@ -126,15 +128,14 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* we should also check that the name variable is anonymous in the actual type de' ?? *) check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de - | _ -> raise WrongArgumentNumber) - | _ -> raise (NotRefinable "Prod or MutInd expected") + | _ -> raise (AssertFailure "Wrong number of arguments")) + | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t = let rec type_of_aux subst metasenv context = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - let module Un = CicUnification in function C.Rel n -> (try @@ -143,9 +144,9 @@ and type_of_aux' metasenv context t = | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv | Some (_,C.Def (bo,None)) -> type_of_aux subst metasenv context (S.lift n bo) - | None -> raise RelToHiddenHypothesis + | None -> raise (RefineFailure "Rel to hidden hypothesis") with - _ -> raise (NotRefinable "Not a close term") + _ -> raise (RefineFailure "Not a close term") ) | C.Var (uri,exp_named_subst) -> let subst',metasenv' = @@ -160,10 +161,16 @@ and type_of_aux' metasenv context t = check_metasenv_consistency n subst metasenv context canonical_context l in CicSubstitution.lift_meta l ty, subst', metasenv' - | C.Sort s -> - C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) - subst,metasenv - | C.Implicit _ -> raise (Impossible 21) + (* TASSI: CONSTRAINT *) + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t'),subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv + | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let _,subst',metasenv' = type_of_aux subst metasenv context ty in @@ -176,7 +183,7 @@ and type_of_aux' metasenv context t = in ty,subst''',metasenv''' with - _ -> raise (NotRefinable "Cast")) + _ -> raise (RefineFailure "Cast")) | C.Prod (name,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in let sort2,subst'',metasenv'' = @@ -189,7 +196,7 @@ and type_of_aux' metasenv context t = C.Meta _ | C.Sort _ -> () | _ -> - raise (NotRefinable (sprintf + raise (RefineFailure (sprintf "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))) @@ -219,7 +226,7 @@ and type_of_aux' metasenv context t = ) tl ([],subst',metasenv') in eat_prods subst'' metasenv'' context hetype tlbody_and_type - | C.Appl _ -> raise (NotRefinable "Appl: no arguments") + | C.Appl _ -> raise (RefineFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> let subst',metasenv' = check_exp_named_subst subst metasenv context exp_named_subst in @@ -251,7 +258,8 @@ and type_of_aux' metasenv context t = List.nth l i , expl_params, parsno | _ -> raise - (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in let rec count_prod t = match CicMetaSubst.whd subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) @@ -306,6 +314,7 @@ and type_of_aux' metasenv context t = 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 = type_of_aux subst metasenv context @@ -403,6 +412,7 @@ and type_of_aux' metasenv context t = in aux 1 canonical_context in + try List.fold_left2 (fun (subst,metasenv) t ct -> match (t,ct) with @@ -411,7 +421,7 @@ and type_of_aux' metasenv context t = | Some t,Some (_,C.Def (ct,_)) -> (try fo_unif_subst subst context metasenv t ct - with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -419,13 +429,21 @@ and type_of_aux' metasenv context t = (try fo_unif_subst subst' context metasenv' inferredty ct - with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | None, Some _ -> - raise (NotRefinable (sprintf + raise (RefineFailure (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))) ) (subst,metasenv) l lifted_canonical_context + with + Invalid_argument _ -> + raise + (RefineFailure + (sprintf + "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" + (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext subst canonical_context))) and check_exp_named_subst metasubst metasenv context = let rec check_exp_named_subst_aux metasubst metasenv substs = @@ -437,10 +455,13 @@ and type_of_aux' metasenv context t = (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise - (NotRefinable + (RefineFailure "A variable with a body can not be explicit substituted") | Cic.Variable (_,None,_,_) -> () - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; let typeoft,metasubst',metasenv' = type_of_aux metasubst metasenv context t @@ -451,7 +472,7 @@ and type_of_aux' metasenv context t = in check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl with _ -> - raise (NotRefinable "Wrong Explicit Named Substitution") + raise (RefineFailure "Wrong Explicit Named Substitution") in check_exp_named_subst_aux metasubst metasenv [] @@ -464,9 +485,15 @@ and type_of_aux' metasenv context t = (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) C.Sort s2,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst,metasenv + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t'),subst,metasenv + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + C.Sort (C.Type t1),subst,metasenv | (C.Meta _, C.Sort _) -> t2'',subst,metasenv | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we @@ -481,8 +508,8 @@ and type_of_aux' metasenv context t = in t2'',subst,metasenv | (_,_) -> - raise (NotRefinable (sprintf - "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)" + raise (RefineFailure (sprintf + "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2''))) @@ -525,7 +552,7 @@ and type_of_aux' metasenv context t = in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context metasenv hetype hetype' + fo_unif_subst subst context metasenv hetype hetype' in let rec eat_prods metasenv subst context hetype = function @@ -533,14 +560,11 @@ and type_of_aux' metasenv context t = | (hete, hety)::tl -> (match hetype with Cic.Prod (n,s,t) -> - (try let subst,metasenv = - CicUnification.fo_unif_subst subst context metasenv s hety + fo_unif_subst subst context metasenv hety s in eat_prods metasenv subst context (CicMetaSubst.subst subst hete t) tl - with - e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e))) | _ -> assert false ) in @@ -548,7 +572,6 @@ and type_of_aux' metasenv context t = eat_prods metasenv subst context hetype' tlbody_and_type in t,subst,metasenv - (* let rec aux context' args (resty,subst,metasenv) = function @@ -597,7 +620,6 @@ and type_of_aux' metasenv context t = in aux [] [] (hetype,subst,metasenv) tlbody_and_type *) - in let ty,subst',metasenv' = type_of_aux [] metasenv context t @@ -652,12 +674,10 @@ let type_of_aux' metasenv context term = *) (t,ty,m) with - | CicUnification.AssertFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; - debug_print msg; + | RefineFailure msg as e -> + debug_print ("@@@ REFINE FAILED: " ^ msg); + raise e + | Uncertain msg as e -> + debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e - | e -> - debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; - raise e ;; -