(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) open Printf exception RefineFailure of string;; exception Uncertain of string;; exception AssertFailure of string;; let debug_print = fun _ -> () let fo_unif_subst subst context metasenv t1 t2 ugraph = try CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph with (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; 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 (AssertFailure "split: list too short") ;; let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let _ = CicTypeChecker.typecheck uri in let obj,u = try CicEnvironment.get_cooked_obj ugraph uri with Not_found -> assert false in match obj with C.Constant (_,_,ty,_,_) -> ty,u | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) and type_of_variable uri ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let _ = CicTypeChecker.typecheck uri in let obj,u = try CicEnvironment.get_cooked_obj ugraph uri with Not_found -> assert false in match obj with C.Variable (_,_,ty,_,_) -> ty,u | _ -> raise (RefineFailure ("Unknown variable definition " ^ UriManager.string_of_uri uri)) and type_of_mutual_inductive_defs uri i ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let _ = CicTypeChecker.typecheck uri in let obj,u = try CicEnvironment.get_cooked_obj ugraph uri with Not_found -> assert false in match obj with C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity,u | _ -> raise (RefineFailure ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) and type_of_mutual_inductive_constr uri i j ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let _ = CicTypeChecker.typecheck uri in let obj,u = try CicEnvironment.get_cooked_obj ugraph uri with Not_found -> assert false in match obj with C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,u | _ -> 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 *) (* 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 n context metasenv subst left_args_no actualtype term expectedtype ugraph = let module C = Cic in (* let module R = CicMetaSubst in *) let module R = CicReduction in match R.whd ~subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv, ugraph | C.Appl (C.MutInd (_,_,_)::tl) -> let (_,arguments) = split tl left_args_no in (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph | C.Prod (name,so,de) -> (* we expect that the actual type of the branch has the due number of Prod *) (match R.whd ~subst context actualtype with C.Prod (name',so',de') -> let subst, metasenv, ugraph1 = fo_unif_subst subst context metasenv so so' ugraph 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 (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1 | _ -> raise (AssertFailure "Wrong number of arguments")) | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in match t with (* function *) C.Rel n -> (try match List.nth context (n - 1) with Some (_,C.Decl ty) -> t,S.lift n ty,subst,metasenv, ugraph | Some (_,C.Def (_,Some ty)) -> t,S.lift n ty,subst,metasenv, ugraph | Some (_,C.Def (bo,None)) -> type_of_aux subst metasenv context (S.lift n bo) ugraph | None -> raise (RefineFailure "Rel to hidden hypothesis") with _ -> raise (RefineFailure "Not a close term") ) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context exp_named_subst ugraph in let ty_uri,ugraph1 = type_of_variable uri ugraph in let ty = CicSubstitution.subst_vars exp_named_subst' ty_uri in C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1 | C.Meta (n,l) -> (try let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in let l',subst',metasenv',ugraph1 = check_metasenv_consistency n subst metasenv context canonical_context l ugraph in (* trust or check ??? *) C.Meta (n,l'),CicSubstitution.subst_meta l' ty, subst', metasenv', ugraph1 (* type_of_aux subst metasenv context (CicSubstitution.subst_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let l',subst',metasenv', ugraph1 = check_metasenv_consistency n subst metasenv context canonical_context l ugraph in C.Meta (n,l'),CicSubstitution.subst_meta l' ty, subst', metasenv',ugraph1) | C.Sort (C.Type tno) -> let tno' = CicUniv.fresh() in let ugraph1 = CicUniv.add_gt tno' tno ugraph in t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in (try let subst''',metasenv''',ugraph3 = fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2 in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with _ -> raise (RefineFailure "Cast")) | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let t',sort2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' ((Some (name,(C.Decl s')))::context) t ugraph1 in let sop,subst''',metasenv''',ugraph3 = sort_of_prod subst'' metasenv'' context (name,s') (sort1,sort2) ugraph2 in C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 | C.Lambda (n,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in (match CicReduction.whd ~subst:subst' context sort1 with C.Meta _ | C.Sort _ -> () | _ -> 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))) ) ; let t',type2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' ((Some (n,(C.Decl s')))::context) t ugraph1 in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) let s',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in let t',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1 in (* One-step LetIn reduction. * Even faster than the previous solution. * Moreover the inferred type is closer to the expected one. *) C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph in let tlbody_and_type,subst'',metasenv'',ugraph2 = List.fold_right (fun x (res,subst,metasenv,ugraph) -> let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in let tl',applty,subst''',metasenv''',ugraph3 = eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2 in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 | C.Appl _ -> raise (RefineFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context exp_named_subst ugraph in let ty_uri,ugraph2 = type_of_constant uri ugraph1 in let cty = CicSubstitution.subst_vars exp_named_subst' ty_uri in C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2 | C.MutInd (uri,i,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context exp_named_subst ugraph in let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in let cty = CicSubstitution.subst_vars exp_named_subst' ty_uri in C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context exp_named_subst ugraph in let ty_uri,ugraph2 = type_of_mutual_inductive_constr uri i j ugraph1 in let cty = CicSubstitution.subst_vars exp_named_subst' ty_uri in C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst', metasenv',ugraph2 | 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,ugraph = let _ = CicTypeChecker.typecheck uri in let obj,u = CicEnvironment.get_cooked_obj ugraph uri in match obj with C.InductiveDefinition (l,expl_params,parsno,_) -> List.nth l i , expl_params, parsno, u | _ -> raise (RefineFailure ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in let rec count_prod t = match CicReduction.whd ~subst 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 subst 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 subst context no_right_params in let metasenv,exp_named_subst = CicMkImplicit.fresh_subst metasenv subst 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 term',actual_type,subst,metasenv,ugraph1 = type_of_aux subst metasenv context term ugraph in let expected_type',_, subst, metasenv,ugraph2 = type_of_aux subst metasenv context expected_type ugraph1 in let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv,ugraph3 = fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 in let rec instantiate_prod t = function [] -> t | he::tl -> match CicReduction.whd ~subst context t with C.Prod (_,_,t') -> instantiate_prod (CicSubstitution.subst he t') tl | _ -> assert false in let arity_instantiated_with_left_args = instantiate_prod arity left_args in (* TODO: check if the sort elimination * is allowed: [(I q1 ... qr)|B] *) let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = List.fold_left (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) 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 p',actual_type,subst,metasenv,ugraph1 = type_of_aux subst metasenv context p ugraph in let constructor',expected_type, subst, metasenv,ugraph2 = type_of_aux subst metasenv context constructor ugraph1 in let outtypeinstance,subst,metasenv,ugraph3 = check_branch 0 context metasenv subst no_left_params actual_type constructor' expected_type ugraph2 in (pl @ [p'],j+1, outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) ([],1,[],subst,metasenv,ugraph3) 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 *) (match outtype with | C.Meta (n,l) -> (let candidate,ugraph5,metasenv,subst = let exp_name_subst, metasenv = let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in let uris = CicUtil.params_of_obj o in List.fold_right ( fun uri (acc,metasenv) -> let metasenv',new_meta = CicMkImplicit.mk_implicit metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in (uri, Cic.Meta(new_meta,irl))::acc, metasenv' ) uris ([],metasenv) in let ty = match left_args,right_args with [],[] -> Cic.MutInd(uri, i, exp_name_subst) | _,_ -> let rec mk_right_args = function 0 -> [] | n -> (Cic.Rel n)::(mk_right_args (n - 1)) in let right_args_no = List.length right_args in let lifted_left_args = List.map (CicSubstitution.lift right_args_no) left_args in Cic.Appl (Cic.MutInd(uri,i,exp_name_subst):: (lifted_left_args @ mk_right_args right_args_no)) in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:ty in match outtypeinstances with | [] -> let extended_context = let rec add_right_args = function Cic.Prod (name,ty,t) -> Some (name,Cic.Decl ty)::(add_right_args t) | _ -> [] in (Some (fresh_name,Cic.Decl ty)):: (List.rev (add_right_args arity_instantiated_with_left_args))@ context in let metasenv,new_meta = CicMkImplicit.mk_implicit metasenv subst extended_context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable extended_context in let rec add_lambdas b = function Cic.Prod (name,ty,t) -> Cic.Lambda (name,ty,(add_lambdas b t)) | _ -> Cic.Lambda (fresh_name, ty, b) in let candidate = add_lambdas (Cic.Meta (new_meta,irl)) arity_instantiated_with_left_args in (Some candidate),ugraph4,metasenv,subst | (constructor_args_no,_,instance,_)::tl -> try let instance',subst,metasenv = CicMetaSubst.delift_rels subst metasenv constructor_args_no instance in let candidate,ugraph,metasenv,subst = List.fold_left ( fun (candidate_oty,ugraph,metasenv,subst) (constructor_args_no,_,instance,_) -> match candidate_oty with | None -> None,ugraph,metasenv,subst | Some ty -> try let instance',subst,metasenv = CicMetaSubst.delift_rels subst metasenv constructor_args_no instance in let subst,metasenv,ugraph = fo_unif_subst subst context metasenv instance' ty ugraph in candidate_oty,ugraph,metasenv,subst with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> None,ugraph,metasenv,subst ) (Some instance',ugraph4,metasenv,subst) tl in match candidate with | None -> None, ugraph,metasenv,subst | Some t -> let rec add_lambdas n b = function Cic.Prod (name,ty,t) -> Cic.Lambda (name,ty,(add_lambdas (n + 1) b t)) | _ -> Cic.Lambda (fresh_name, ty, CicSubstitution.lift (n + 1) t) in Some (add_lambdas 0 t arity_instantiated_with_left_args), ugraph,metasenv,subst with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> None,ugraph4,metasenv,subst in match candidate with | None -> raise (Uncertain "can't solve an higher order unification problem") | Some candidate -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv candidate outtype ugraph5 in C.MutCase (uri, i, outtype, term', pl'), CicReduction.head_beta_reduce (CicMetaSubst.apply_subst subst (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 in let (subst,metasenv,ugraph6) = List.fold_left (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) -> let instance' = let appl = let outtype' = CicSubstitution.lift constructor_args_no outtype in C.Appl (outtype'::args) in CicReduction.whd ~subst context appl in fo_unif_subst subst context metasenv instance instance' ugraph) (subst,metasenv,ugraph5) outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), 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 = List.fold_left (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', Some (C.Name n,(C.Decl ty')) :: types, ugraph ) ([],subst,metasenv,[],ugraph) fl in let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) -> let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in let subst',metasenv',ugraph' = fo_unif_subst subst context' metasenv ty_of_bo (CicSubstitution.lift len ty) ugraph1 in fl @ [bo'] , subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) fl in let (_,_,ty,_) = List.nth fl i in (* now we have the new ty in fl_ty', the new bo in fl_bo', * and we want the new fl with bo' and ty' injected in the right * place. *) let rec map3 f l1 l2 l3 = match l1,l2,l3 with | [],[],[] -> [] | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) | _ -> assert false in let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') ) fl_ty' fl_bo' fl in C.Fix (i,fl''),ty,subst,metasenv,ugraph2 | C.CoFix (i,fl) -> let fl_ty',subst,metasenv,types,ugraph1 = List.fold_left (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in fl @ [ty'],subst',metasenv', Some (C.Name n,(C.Decl ty')) :: types, ugraph1 ) ([],subst,metasenv,[],ugraph) fl in let len = List.length types in let context' = types@context in let fl_bo',subst,metasenv,ugraph2 = List.fold_left (fun (fl,subst,metasenv,ugraph) (name,ty,bo) -> let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in let subst',metasenv',ugraph' = fo_unif_subst subst context' metasenv ty_of_bo (CicSubstitution.lift len ty) ugraph1 in fl @ [bo'],subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) fl in let (_,ty,_) = List.nth fl i in (* now we have the new ty in fl_ty', the new bo in fl_bo', * and we want the new fl with bo' and ty' injected in the right * place. *) let rec map3 f l1 l2 l3 = match l1,l2,l3 with | [],[],[] -> [] | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) | _ -> assert false in let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') ) fl_ty' fl_bo' fl in C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) and check_metasenv_consistency metano subst metasenv context canonical_context l ugraph = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in let lifted_canonical_context = let rec aux i = function [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (n,C.Def (t,Some ty)))::tl -> (Some (n, C.Def ((S.subst_meta l (S.lift i t)), Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) in aux 1 canonical_context in try List.fold_left2 (fun (l,subst,metasenv,ugraph) t ct -> match (t,ct) with _,None -> l @ [None],subst,metasenv,ugraph | Some t,Some (_,C.Def (ct,_)) -> let subst',metasenv',ugraph' = (try fo_unif_subst subst context metasenv t ct ugraph 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))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> let t',inferredty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context t ugraph in let subst'',metasenv'',ugraph2 = (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 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))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> 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,ugraph) 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 tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = match tl with [] -> [],metasubst,metasenv,ugraph | ((uri,t) as subst)::tl -> let ty_uri,ugraph1 = type_of_variable uri ugraph in let typeofvar = CicSubstitution.subst_vars substs ty_uri in (* CSC: why was this code here? it is wrong (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise (RefineFailure "A variable with a body can not be explicit substituted") | Cic.Variable (_,None,_,_) -> () | _ -> raise (RefineFailure ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; *) let t',typeoft,metasubst',metasenv',ugraph2 = type_of_aux metasubst metasenv context t ugraph1 in let metasubst'',metasenv'',ugraph3 = try fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2 with _ -> raise (RefineFailure ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl ugraph3 in ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4 in check_exp_named_subst_aux metasubst metasenv [] tl ugraph and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph = let module C = Cic in let context_for_t2 = (Some (name,C.Decl s))::context in let t1'' = CicReduction.whd ~subst context t1 in let t2'' = CicReduction.whd ~subst context_for_t2 t2 in match (t1'', t2'') with (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,ugraph | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) let t' = CicUniv.fresh() in let ugraph1 = CicUniv.add_ge t' t1 ugraph in let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in C.Sort (C.Type t'),subst,metasenv,ugraph2 | (C.Sort _,C.Sort (C.Type t1)) -> (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) C.Sort (C.Type t1),subst,metasenv,ugraph | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we * brake the invariant that refine produce only well typed terms *) (* TODO if we check the non meta term and if it is a sort then we are * likely to know the exact value of the result e.g. if the rhs is a * Sort (Prop | Set | CProp) then the result is the rhs *) let (metasenv,idx) = CicMkImplicit.mk_implicit_sort metasenv subst in let (subst, metasenv,ugraph1) = fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph in t2'',subst,metasenv,ugraph1 | (_,_) -> 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''))) and eat_prods subst metasenv context hetype tlbody_and_type ugraph = let rec mk_prod metasenv context = function [] -> let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv,Cic.Meta (idx, irl) | (_,argty)::tl -> let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let meta = Cic.Meta (idx,irl) in let name = (* The name must be fresh for context. *) (* Nevertheless, argty is well-typed only in context. *) (* Thus I generate a name (name_hint) in context and *) (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in (context'@context). *) let name_hint = (* Cic.Name "pippo" *) FreshNamesGenerator.mk_fresh_name ~subst metasenv (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous ~typ:(CicMetaSubst.apply_subst subst argty) in (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name ~subst [] context name_hint ~typ:(Cic.Sort Cic.Prop) in let metasenv,target = mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl in metasenv,Cic.Prod (name,meta,target) in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv,ugraph1) = try fo_unif_subst subst context metasenv hetype hetype' ugraph with exn -> debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" (CicPp.ppterm hetype) (CicPp.ppterm hetype') (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppsubst subst)); raise exn in let rec eat_prods metasenv subst context hetype ugraph = function | [] -> [],metasenv,subst,hetype,ugraph | (hete, hety)::tl -> (match hetype with Cic.Prod (n,s,t) -> let arg,subst,metasenv,ugraph1 = try let subst,metasenv,ugraph1 = fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 with exn -> (* we search a coercion from hety to s *) let coer = CoercGraph.look_for_coercion (CicMetaSubst.apply_subst subst hety) (CicMetaSubst.apply_subst subst s) in match coer with | None -> raise exn | Some c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context (* (CicMetaSubst.subst subst hete t) tl *) (CicSubstitution.subst hete t) ugraph1 tl in arg::coerced_args,metasenv',subst',t',ugraph2 | _ -> assert false ) in let coerced_args,metasenv,subst,t,ugraph2 = eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type in coerced_args,t,subst,metasenv,ugraph2 in (* eat prods ends here! *) let t',ty,subst',metasenv',ugraph1 = type_of_aux [] metasenv context t ugraph in let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in (* Andrea: ho rimesso qui l'applicazione della subst al metasenv dopo che ho droppato l'invariante che il metsaenv e' sempre istanziato *) let substituted_metasenv = CicMetaSubst.apply_subst_metasenv subst' metasenv' in (* metasenv' *) (* substituted_t,substituted_ty,substituted_metasenv *) (* ANDREA: spostare tutta questa robaccia da un altra parte *) let cleaned_t = FreshNamesGenerator.clean_dummy_dependent_types substituted_t in let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in let cleaned_metasenv = List.map (function (n,context,ty) -> let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in let context' = List.map (function None -> None | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) | Some (n, Cic.Def (bo,ty)) -> let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in let ty' = match ty with None -> None | Some ty -> Some (FreshNamesGenerator.clean_dummy_dependent_types ty) in Some (n, Cic.Def (bo',ty')) ) context in (n,context',ty') ) substituted_metasenv in (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) ;; let type_of_aux' metasenv context term ugraph = try 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 = try let (t,ty,m) = type_of_aux' metasenv context term in debug_print ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); debug_print ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []); (t,ty,m) with | RefineFailure msg as e -> debug_print ("@@@ REFINE FAILED: " ^ msg); raise e | Uncertain msg as e -> debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e ;; *)