Cic.CicHash.find localization_tbl t
with Not_found ->
prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
- assert false
+ raise exn'
in
raise (HExtlib.Localized (loc,exn'))
let exp_impl metasenv subst context =
function
| Some `Type ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+ let (metasenv', idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
| Some `Closed ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+ metasenv', Cic.Meta (idx, [])
| None ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
| _ -> assert false
;;
+let is_a_double_coercion t =
+ let last_of l =
+ let rec aux = function
+ | x::[] -> x
+ | x::tl -> aux tl
+ | [] -> assert false
+ in
+ aux l
+ in
+ let dummyres =
+ false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
+ in
+ match t with
+ | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
+ (match last_of tl with
+ | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ let head = last_of tl2 in
+ true, c1, c2, head
+ | _ -> dummyres)
+ | _ -> dummyres
+
+let avoid_double_coercion context subst metasenv ugraph t ty =
+ let arity_of con =
+ try
+ let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+ let rec count_pi = function
+ | Cic.Prod (_,_,t) -> 1 + count_pi t
+ | _ -> 0
+ in
+ count_pi ty
+ with Invalid_argument _ -> assert false (* all coercions have an uri *)
+ in
+ let rec mk_implicits tail = function
+ | 0 -> [tail]
+ | n -> Cic.Implicit None :: mk_implicits tail (n-1)
+ in
+ let b, c1, c2, head = is_a_double_coercion t in
+ if b then
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CicMetaSubst.apply_subst subst ty in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c ->
+ let arity = arity_of c in
+ let args = mk_implicits head (arity - 1) in
+ let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
+ let newt = Cic.Appl (c_bo::args) in
+ (try
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
+ Cic.Appl (c::args), ty, subst, metasenv, ugraph
+ with
+ RefineFailure _ ->
+ prerr_endline ("#### Coercion not packed (Refine_failure): " ^
+ CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
+ assert false
+ | Uncertain _ ->
+ prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
+ CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
+ assert false)
+ | _ -> assert false) (* the composite coercion must exist *)
+ else
+ t, ty, subst, metasenv, ugraph
let rec type_of_constant uri ugraph =
let module C = Cic in
| C.CurrentProof (_,_,_,ty,_,_) -> ty,u
| _ ->
raise
- (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
+ (RefineFailure
+ (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
and type_of_variable uri ugraph =
let module C = Cic in
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion c ->
let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion
+ avoid_double_coercion context
subst metasenv ugraph
(Cic.Appl[c;t]) coercion_tgt
in
match boh with
| CoercGraph.SomeCoercion c ->
let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion
+ avoid_double_coercion context
subst' metasenv' ugraph1
(Cic.Appl[c;s']) coercion_tgt
in
eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
in
- avoid_double_coercion
+ avoid_double_coercion context
subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
| None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
| Some candidate ->
let subst,metasenv,ugraph =
+ try
fo_unif_subst subst context metasenv
candidate outtype ugraph5
+ with
+ exn -> assert false(* unification against a metavariable *)
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
(C.Appl ((outtype :: right_args) @ [term'])) ugraph4
in
let (subst,metasenv,ugraph6) =
- List.fold_left
+ List.fold_left2
(fun (subst,metasenv,ugraph)
- (constructor_args_no,context,instance,args) ->
+ p (constructor_args_no,context,instance,args)
+ ->
let instance' =
let appl =
let outtype' =
in
CicReduction.whd ~subst context appl
in
- fo_unif_subst subst context metasenv
- instance instance' ugraph)
- (subst,metasenv,ugraph5) outtypeinstances
+ try
+ fo_unif_subst subst context metasenv instance instance'
+ ugraph
+ with
+ exn ->
+ enrich localization_tbl p exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst p
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst instance'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst instance
+ context)))
+ (subst,metasenv,ugraph5) pl' outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph
- in
+ type_of_aux subst metasenv context' bo ugraph in
+ let expected_ty = CicSubstitution.lift len ty in
let subst',metasenv',ugraph' =
+ try
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ty_of_bo expected_ty ugraph1
+ with
+ exn ->
+ enrich localization_tbl bo exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_ty
+ context))
in
fl @ [bo'] , subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
List.fold_left
(fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph
- in
+ type_of_aux subst metasenv context' bo ugraph in
+ let expected_ty = CicSubstitution.lift len ty in
let subst',metasenv',ugraph' =
+ try
fo_unif_subst subst context' metasenv
- ty_of_bo (CicSubstitution.lift len ty) ugraph1
+ ty_of_bo expected_ty ugraph1
+ with
+ exn ->
+ enrich localization_tbl bo exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst expected_ty
+ context))
in
fl @ [bo'],subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
relocalize localization_tbl t t';
res
- and avoid_double_coercion subst metasenv ugraph t ty =
- match t with
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
- | _ -> assert false) (* the composite coercion must exist *)
- | _ -> t, ty, subst, metasenv, ugraph
-
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
| (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
- * brake the invariant that refine produce only well typed terms *)
+ * break the invariant that refine produce only well typed terms *)
(* TODO if we check the non meta term and if it is a sort then we
* are likely to know the exact value of the result e.g. if the rhs
* is a Sort (Prop | Set | CProp) then the result is the rhs *)
try
fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ debug_print
+ (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
(CicPp.ppterm hetype')
(CicMetaSubst.ppmetasenv [] metasenv)
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion c ->
let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion
+ avoid_double_coercion context
subst metasenv ugraph
(Cic.Appl[c;hete]) tgt_carr in
try
newhety s ugraph
in
newt, subst, metasenv, ugraph
- with exn ->
+ with _ ->
enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
are_all_occurrences_positive metasenv ugraph uri tys paramsno
in
Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+;;
+
+(* sara' piu' veloce che raffinare da zero? mah.... *)
+let pack_coercion metasenv t =
+ let module C = Cic in
+ let rec merge_coercions ctx =
+ let aux = (fun (u,t) -> u,merge_coercions ctx t) in
+ function
+ | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
+ | C.Meta (n,subst) ->
+ let subst' =
+ List.map
+ (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
+ in
+ C.Meta (n,subst')
+ | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
+ | C.Prod (name,so,dest) ->
+ let ctx' = (Some (name,C.Decl so))::ctx in
+ C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.Lambda (name,so,dest) ->
+ let ctx' = (Some (name,C.Decl so))::ctx in
+ C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,dest) ->
+ let ctx' = Some (name,(C.Def (so,None)))::ctx in
+ C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.Appl l as t ->
+ let b,_,_,_ = is_a_double_coercion t in
+ (* prerr_endline "CANDIDATO!!!!"; *)
+ let newt =
+ if b then
+ let ugraph = CicUniv.empty_ugraph in
+ let old_insert_coercions = !insert_coercions in
+ insert_coercions := false;
+ let newt, _, menv, _ =
+ try
+ type_of_aux' metasenv ctx t ugraph
+ with RefineFailure _ | Uncertain _ ->
+ prerr_endline (CicPp.ppterm t);
+ t, t, [], ugraph
+ in
+ insert_coercions := old_insert_coercions;
+ if metasenv <> [] || menv = [] then
+ newt
+ else
+ (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+ else
+ t
+ in
+ (match newt with
+ | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
+ | _ -> assert false)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Var (uri, exp_named_subst)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Const (uri, exp_named_subst)
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutInd (uri,tyno,exp_named_subst)
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst)
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ let pl = List.map (merge_coercions ctx) pl in
+ C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
+ | C.Fix (fno, fl) ->
+ let ctx =
+ List.fold_left
+ (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,idx,ty,bo) ->
+ (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
+ fl
+ in
+ C.Fix (fno, fl)
+ | C.CoFix (fno, fl) ->
+ let ctx =
+ List.fold_left
+ (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, merge_coercions ctx ty, merge_coercions ctx bo))
+ fl
+ in
+ C.CoFix (fno, fl)
+ in
+ merge_coercions [] t
+;;
+
+let pack_coercion_obj obj =
+ let module C = Cic in
+ match obj with
+ | C.Constant (id, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] body)
+ in
+ let ty = pack_coercion [] ty in
+ C.Constant (id, body, ty, params, attrs)
+ | C.Variable (name, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] body)
+ in
+ let ty = pack_coercion [] ty in
+ C.Variable (name, body, ty, params, attrs)
+ | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
+ let conjectures =
+ List.map
+ (fun (i, ctx, ty) ->
+ let ctx =
+ List.map
+ (function
+ | Some (name, C.Decl t) ->
+ Some (name, C.Decl (pack_coercion conjectures t))
+ | Some (name, C.Def (t,None)) ->
+ Some (name, C.Def (pack_coercion conjectures t, None))
+ | Some (name, C.Def (t,Some ty)) ->
+ Some (name, C.Def (pack_coercion conjectures t,
+ Some (pack_coercion conjectures ty)))
+ | None -> None)
+ ctx
+ in
+ ((i,ctx,pack_coercion conjectures ty)))
+ conjectures
+ in
+ let body = pack_coercion conjectures body in
+ let ty = pack_coercion conjectures ty in
+ C.CurrentProof (name, conjectures, body, ty, params, attrs)
+ | C.InductiveDefinition (indtys, params, leftno, attrs) ->
+ let indtys =
+ List.map
+ (fun (name, ind, arity, cl) ->
+ let arity = pack_coercion [] arity in
+ let cl =
+ List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl
+ in
+ (name, ind, arity, cl))
+ indtys
+ in
+ C.InductiveDefinition (indtys, params, leftno, attrs)
+;;
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =