(*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
;;
+let debug_print = prerr_endline
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
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 =
+and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
let module C = Cic in
- let module R = CicReduction in
+ let module R = CicMetaSubst in
let module Un = CicUnification in
- match R.whd context expectedtype with
+ match R.whd subst context expectedtype with
C.MutInd (_,_,_) ->
- (actualtype, [term]), subst, metasenv
+ (n,context,actualtype, [term]), subst, metasenv
| C.Appl (C.MutInd (_,_,_)::tl) ->
let (_,arguments) = split tl left_args_no in
- (actualtype, arguments@[term]), subst, metasenv
+ (n,context,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
+ (match R.whd subst context actualtype with
C.Prod (name',so',de') ->
- let subst,metsaenv =
+ let subst, metasenv =
Un.fo_unif_subst subst context metasenv so so' in
let term' =
(match CicSubstitution.lift 1 term with
| 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
+ 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")
Some (_,C.Decl t) -> S.lift n t,subst,metasenv
| 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
raise
(WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
let rec count_prod t =
- match CicReduction.whd context t with
+ match CicMetaSubst.whd subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0 in
let no_args = count_prod arity 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 =
+ type_of_aux subst metasenv context expected_type
+ in
+ let actual_type = CicMetaSubst.whd subst context actual_type in
let subst,metasenv =
- Un.fo_unif_subst
- subst
- context
- metasenv expected_type (CicReduction.whd context actual_type) in
+ Un.fo_unif_subst subst context metasenv expected_type actual_type
+ in
(* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let (_,outtypeinstances,subst,metasenv) =
List.fold_left
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))
+ (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
type_of_aux subst metasenv context constructor in
let outtypeinstance,subst,metasenv =
check_branch
- context metasenv subst
+ 0 context metasenv subst
no_left_params actual_type constructor expected_type in
(j+1,outtypeinstance::outtypeinstances,subst,metasenv))
(1,[],subst,metasenv) pl in
to a trivial check. Otherwise, we should guess a type from
its instances *)
(* easy case *)
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term]))
+ in
let (subst,metasenv) =
List.fold_left
- (fun (subst,metasenv) (instance,args) ->
- let instance' =
- CicReduction.whd context (C.Appl(outtype::args)) in
+ (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+(*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv) =
+ type_of_aux subst metasenv context appl
+ in
+*)
+ CicMetaSubst.whd subst context appl
+ in
Un.fo_unif_subst subst context metasenv instance instance')
(subst,metasenv) outtypeinstances in
- CicReduction.whd
+ CicMetaSubst.whd subst
context (C.Appl(outtype::right_args@[term])),subst,metasenv
| C.Fix _
| C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
List.fold_left2
(fun (subst,metasenv) t ct ->
match (t,ct) with
- _,None -> subst,metasenv
+ _,None ->
+ subst,metasenv
| Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
type_of_aux subst metasenv context t
in
(try
- CicUnification.fo_unif_subst subst context metasenv inferredty ct
+ CicUnification.fo_unif_subst
+ subst' context metasenv' inferredty ct
with _ -> raise MetasenvInconsistency)
- | _, _ -> raise MetasenvInconsistency
+ | _, _ ->
+ raise MetasenvInconsistency
) (subst,metasenv) l lifted_canonical_context
and check_exp_named_subst metasubst metasenv context =
and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
(* ti could be a metavariable in the domain of the substitution *)
- let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
- let t1' = CicUnification.apply_subst subst' t1 in
- let t2' = CicUnification.apply_subst subst' t2 in
- let t1'' = CicReduction.whd context t1' in
- let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
+ let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
+ let t1' = CicMetaSubst.apply_subst subst' t1 in
+ let t2' = CicMetaSubst.apply_subst subst' t2 in
+ let t1'' = CicMetaSubst.whd subst' context t1' in
+ let t2'' = CicMetaSubst.whd subst' ((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 or s2 = C.CProp) -> (* different from Coq manual!!! *)
| (C.Sort s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
C.Sort C.Type,subst',metasenv'
- | (C.Meta _,_)
- | (_,C.Meta _) ->
+ | (C.Meta _,_) | (_,C.Meta _) ->
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ C.Meta (idx, irl), subst, metasenv'
+(*
raise
(Uncertain
("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
CicPp.ppterm t2''))
+*)
| (_,_) ->
raise
(NotRefinable
function
[] -> hetype,subst,metasenv
| (hete, hety)::tl ->
- (match (CicReduction.whd context hetype) with
+ (match (CicMetaSubst.whd subst context hetype) with
Cic.Prod (n,s,t) ->
let subst',metasenv' =
- try
CicUnification.fo_unif_subst subst context metasenv s hety
- with _ ->
- raise (NotRefinable "Appl: wrong parameter-type")
in
CicReduction.fdebug := -1 ;
eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
in
- let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
+ let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
(* we get rid of the metavariables that have been instantiated *)
let metasenv''' =
List.filter
(function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
metasenv''
in
- CicUnification.apply_subst subst'' t,
- CicUnification.apply_subst subst'' ty,
- subst'', metasenv'''
+ CicMetaSubst.apply_subst subst'' t,
+ CicMetaSubst.apply_subst subst'' ty,
+ subst'', metasenv'''
;;
(* DEBUGGING ONLY *)
let type_of_aux' metasenv context term =
try
- let (t,ty,s,m) =
- type_of_aux' metasenv context term
- in
+ let (t,ty,s,m) = type_of_aux' metasenv context term in
+(*
List.iter
(function (i,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
+ debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
List.iter
(function (i,_,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
- prerr_endline
+ debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
+*)
+ debug_print
("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
(t,ty,s,m)
with
- e ->
+ | CicUnification.AssertFailure msg as e ->
+ debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
+ debug_print msg;
+ raise e
+ | CicUnification.UnificationFailure msg as e ->
+ debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
+ debug_print msg;
+ raise e
+ | e ->
+(*
List.iter
(function (i,_,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
+ debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
metasenv ;
- prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
+*)
+ debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
raise e
;;
-
-
-
-
-
-
-
-
-
projects / helm.git / commitdiff