+ *)
+ let obj,u = CicEnvironment.get_obj ugraph uri 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 obj,u = CicEnvironment.get_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_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