and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
let module C = Cic in
- let module R = CicMetaSubst in
- match R.whd subst context expectedtype with
+ (* 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
| C.Appl (C.MutInd (_,_,_)::tl) ->
| 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
+ (match R.whd ~subst context actualtype with
C.Prod (name',so',de') ->
let subst, metasenv =
fo_unif_subst subst context metasenv so so' in
ty,subst',metasenv'
| C.Meta (n,l) ->
(try
- let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in
+ let (canonical_context, term) = CicUtil.lookup_subst n subst in
let subst,metasenv =
check_metasenv_consistency n subst metasenv context
canonical_context l
in
type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
- with CicMetaSubst.SubstNotFound _ ->
+ with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let subst,metasenv =
check_metasenv_consistency n subst metasenv context
sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
- (match CicMetaSubst.whd subst' context sort1 with
+ (match CicReduction.whd ~subst:subst' context sort1 with
C.Meta _
| C.Sort _ -> ()
| _ ->
(RefineFailure
("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
let rec count_prod t =
- match CicMetaSubst.whd subst context t with
+ match CicReduction.whd ~subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0 in
let no_args = count_prod arity in
let _, subst, metasenv =
type_of_aux subst metasenv context expected_type
in
- let actual_type = CicMetaSubst.whd subst context actual_type in
+ let actual_type = CicReduction.whd ~subst context actual_type in
let subst,metasenv =
fo_unif_subst subst context metasenv expected_type actual_type
in
type_of_aux subst metasenv context appl
in
*)
- CicMetaSubst.whd subst context appl
+ (* 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')
(subst,metasenv) outtypeinstances in
- CicMetaSubst.whd subst
+ CicReduction.whd ~subst
context (C.Appl(outtype::right_args@[term])),subst,metasenv
| C.Fix (i,fl) ->
let subst,metasenv,types =
type_of_aux subst metasenv context' bo
in
fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift subst len ty)
+ ty_of_bo (CicSubstitution.lift len ty)
) (subst,metasenv) fl in
let (_,_,ty,_) = List.nth fl i in
ty,subst,metasenv
type_of_aux subst metasenv context' bo
in
fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift subst len ty)
+ ty_of_bo (CicSubstitution.lift len ty)
) (subst,metasenv) fl in
let (_,ty,_) = List.nth fl i in
C.Def ((S.lift_meta l (S.lift i t)),
Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
- aux 1 canonical_context
+ aux 1 canonical_context
in
try
List.fold_left2
and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
- let t1'' = CicMetaSubst.whd subst context t1 in
- let t2'' = CicMetaSubst.whd subst context_for_t2 t2 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!!! *)
(* 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 =
- FreshNamesGenerator.mk_fresh_name metasenv
+ let name_hint =
+ (* Cic.Name "pippo" *)
+ FreshNamesGenerator.mk_fresh_name metasenv
(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
(CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
- (CicMetaSubst.apply_subst subst argty)
+ (CicMetaSubst.apply_subst subst argty)
in
(* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name
[] context name_hint (Cic.Sort Cic.Prop)
in
let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
in
- metasenv,Cic.Prod (name,meta,target)
+ metasenv,Cic.Prod (name,meta,target)
in
let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
let (subst, metasenv) =
(match hetype with
Cic.Prod (n,s,t) ->
let subst,metasenv =
- fo_unif_subst subst context metasenv hety s
+ fo_unif_subst subst context metasenv hety s
+(*
+ try
+ fo_unif_subst subst context metasenv hety s
+ with _ ->
+ prerr_endline("senza subst fallisce");
+ let hety = CicMetaSubst.apply_subst subst hety in
+ let s = CicMetaSubst.apply_subst subst s in
+ prerr_endline ("unifico = " ^(CicPp.ppterm hety));
+ prerr_endline ("con = " ^(CicPp.ppterm s));
+ fo_unif_subst subst context metasenv hety s *)
in
- eat_prods metasenv subst context
- (CicMetaSubst.subst subst hete t) tl
+ (* DEBUG
+ let t1 = CicMetaSubst.subst subst hete t in
+ let t2 = CicSubstitution.subst hete t in
+ prerr_endline ("con subst = " ^(CicPp.ppterm t1));
+ prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
+ prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
+ (CicMetaSubst.ppmetasenv metasenv subst));
+ prerr_endline("++++++++++subst prima di eat_prods:\n" ^
+ (CicMetaSubst.ppsubst subst));
+ *)
+ eat_prods metasenv subst context
+ (* (CicMetaSubst.subst subst hete t) tl *)
+ (CicSubstitution.subst hete t) tl
| _ -> assert false
)
in
in
aux [] [] (hetype,subst,metasenv) tlbody_and_type
*)
- in
+ in
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
in
let substituted_t = CicMetaSubst.apply_subst subst' t in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
- let substituted_metasenv = metasenv'
-(* CicMetaSubst.apply_subst_metasenv subst' metasenv' *)
- 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 =
(n,context',ty')
) substituted_metasenv
in
- (cleaned_t,cleaned_ty,cleaned_metasenv)
-
+ (cleaned_t,cleaned_ty,cleaned_metasenv)
;;
-(* DEBUGGING ONLY *)
+
+
+(* 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);
-(*
+ 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 m s);
-*)
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
(t,ty,m)
with
| RefineFailure msg as e ->
| Uncertain msg as e ->
debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
raise e
-;;
+;; *)
projects / helm.git / blobdiff