X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b535b9ebe987677505d7d9b40a2c59731a4c2606;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=ad4d0106539f9c207a7e91ebba1d7bf1ebe72f5b;hpb=77aad924b820f7e44b222bfb36afb0a2fb1c91e2;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index ad4d01065..b535b9ebe 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -131,6 +131,20 @@ let exp_impl metasenv subst context = | _ -> assert false ;; +let unvariant newt = + match newt with + | Cic.Appl (hd::args) -> + let uri = CicUtil.uri_of_term hd in + (match + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + with + | Cic.Constant (_,Some t,_,[],attrs),_ + when List.exists ((=) (`Flavour `Variant)) attrs -> + Cic.Appl (t::args) + | _ -> newt) + | _ -> newt +;; + let is_a_double_coercion t = let rec subst_nth n x l = match n,l with @@ -323,8 +337,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t - ugraph +and type_of_aux' ?(clean_dummy_dependent_types=true) + ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph = let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in @@ -491,7 +505,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl s' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(2) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' @@ -617,7 +631,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(3) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type @@ -663,7 +677,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("The term " ^ + lazy ("(4) The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -851,7 +865,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(5) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst instance' @@ -892,7 +906,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(7) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -945,7 +959,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("The term " ^ + lazy ("(8) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -1192,11 +1206,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let selected = HExtlib.list_findopt (fun (metasenv,last,c) _ -> - match c with - | c when not (CoercGraph.is_composite c) -> - debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); - None - | c -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last head ugraph in debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); @@ -1305,7 +1314,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci ugraph in debug_print (lazy (" has type: "^ pp tty)); - Some (coerc,tty,subst,metasenv,ugraph) + + Some (unvariant coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1444,11 +1454,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context c ugraph in let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt expty + avoid_double_coercion context subst metasenv ugraph newt + expty in let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv newhety expty ugraph in - Some ((newt,newty), subst, metasenv, ugraph) + fo_unif_subst subst context metasenv newhety expty ugraph + in + let b, ugraph = + CicReduction.are_convertible + ~subst ~metasenv context infty expty ugraph + in + if b then + Some ((t,infty), subst, metasenv, ugraph) + else + let newt = unvariant newt in + Some ((newt,newty), subst, metasenv, ugraph) with | Uncertain _ -> uncertain := true; None | RefineFailure _ -> None) @@ -1770,7 +1790,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci coerce_to_something_aux t infty expty subst metasenv context ugraph with Uncertain _ | RefineFailure _ as exn -> let f _ = - lazy ("The term " ^ + lazy ("(9) The term " ^ CicMetaSubst.ppterm_in_context metasenv subst t context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst infty context ^ " but is here used with type " ^ @@ -1808,7 +1828,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci (* eat prods ends here! *) let t',ty,subst',metasenv',ugraph1 = - type_of_aux [] metasenv context t ugraph + type_of_aux subst metasenv context t ugraph in let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in @@ -1852,7 +1872,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci else substituted_metasenv in - (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) + (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) +;; + +let type_of metasenv subst context t ug = + type_of_aux' metasenv subst context t ug +;; + +let type_of_aux' + ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug += + let t,ty,m,s,ug = + type_of_aux' ?clean_dummy_dependent_types ?localization_tbl + metasenv [] context t ug + in + t,ty,m,ug ;; let undebrujin uri typesno tys t = @@ -1953,7 +1987,7 @@ let typecheck metasenv uri obj ~localization_tbl = RefineFailure _ | Uncertain _ as exn -> let msg = - lazy ("The term " ^ + lazy ("(1) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ @@ -1973,13 +2007,13 @@ let typecheck metasenv uri obj ~localization_tbl = let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph | Cic.Constant (name,None,ty,args,attrs) -> - let ty',_,metasenv,ugraph = + let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - (match CicReduction.whd [] ty' with + (match CicReduction.whd [] sort with Cic.Sort _ | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph - | _ -> raise (RefineFailure (lazy "")) + | _ -> raise (RefineFailure (lazy ""))) | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> assert (metasenv' = metasenv); (* Here we do not check the metasenv for correctness *)