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 =
(*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
| _ -> 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
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t,subst,metasenv
- | Some (_,C.Def bo) ->
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+ | Some (_,C.Def (bo,None)) ->
+ prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
type_of_aux subst metasenv context (S.lift n bo)
| None -> raise RelToHiddenHypothesis
with
C.Prod (n,s,type2),subst'''',metasenv''''
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let _,subst',metasenv' = type_of_aux subst metasenv context s in
+ let ty,subst',metasenv' = type_of_aux subst metasenv context s in
let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
+ type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
in
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
(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
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def t))::tl ->
- (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (Some (n,C.Def (t,None)))::tl ->
+ (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
+ | (Some (_,C.Def (_,Some _)))::_ -> assert false
in
aux 1 canonical_context
in
(fun (subst,metasenv) t ct ->
match (t,ct) with
_,None -> subst,metasenv
- | Some t,Some (_,C.Def ct) ->
+ | Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
with _ -> raise MetasenvInconsistency)
let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
C.Sort s2,subst',metasenv'
| (C.Sort s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
raise e
;;
+
+
+
+
+
+
+
+
+
+