| 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
+ 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")
(* first, get the inductive type (and noparams)
* in the environment *)
let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj ~trust:true uri
- with Not_found -> assert false
- in
- *)
let obj,u = CicEnvironment.get_obj ugraph uri in
match obj with
C.InductiveDefinition (l,expl_params,parsno,_) ->
(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
- (* 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 *)
-
- (* 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
+ 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
+ (* 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 =
+ match outtypeinstances with
+ | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
+ | (constructor_args_no,_,instance,_)::tl ->
+ try
+ let instance' =
+ CicSubstitution.delift constructor_args_no
+ (CicMetaSubst.apply_subst subst instance)
in
- C.Appl (outtype'::args)
- in
- (*
- (* if appl is not well typed then the type_of below solves the
- * problem *)
- let (_, subst, metasenv,ugraph1) =
- type_of_aux subst metasenv context appl ugraph
- in
- *)
- (* DEBUG
- let prova1 = CicMetaSubst.whd subst context appl in
- let prova2 = CicReduction.whd ~subst context appl in
- if not (prova1 = prova2) then
- begin
- prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
- prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
- end;
- *)
- (* CicMetaSubst.whd subst context appl *)
- 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.whd ~subst context
- (C.Appl(outtype::right_args@[term])),
- subst,metasenv,ugraph6
+ List.fold_left (
+ fun (candidate_oty,ugraph)
+ (constructor_args_no,_,instance,_) ->
+ match candidate_oty with
+ | None -> None,ugraph
+ | Some ty ->
+ try
+ let instance' =
+ CicSubstitution.delift
+ constructor_args_no
+ (CicMetaSubst.apply_subst subst instance)
+ in
+ let b,ugraph1 =
+ CicReduction.are_convertible context
+ instance' ty ugraph
+ in
+ if b then
+ candidate_oty,ugraph1
+ else
+ None,ugraph
+ with Failure s -> None,ugraph
+ ) (Some instance',ugraph4) tl
+ with Failure s ->
+ None,ugraph4
+ in
+ match candidate with
+ | None -> raise (Uncertain "can't solve an higher order unification problem")
+ | Some candidate ->
+ prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
+ let s,m,u =
+ fo_unif_subst subst context metasenv
+ candidate outtype ugraph5
+ in
+ C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
+ | _ -> (* 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.whd ~subst context
+ (C.Appl(outtype::right_args@[term])),
+ subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
let fl_ty',subst,metasenv,types,ugraph1 =
List.fold_left
projects / helm.git / commitdiff