| _ -> 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
let module R = CicReduction in
t, cast, subst, metasenv, ugraph
| term ->
let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
+ let boh =
+ CoercGraph.look_for_coercion coercion_src coercion_tgt
+ in
(match boh with
| CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
CicMetaSubst.ppterm_in_context
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion c ->
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context (Cic.Appl[c;t])
+ ugraph in
let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context
- subst metasenv ugraph
- (Cic.Appl[c;t]) coercion_tgt
+ avoid_double_coercion context subst metasenv ugraph
+ newt coercion_tgt
in
newt, tty, subst, metasenv, ugraph)
in
| C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
| coercion_src ->
let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
+ let boh =
+ CoercGraph.look_for_coercion coercion_src coercion_tgt
+ in
match boh with
| CoercGraph.SomeCoercion c ->
+ let newt,_,subst',metasenv',ugraph1 =
+ type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
+ ugraph1 in
let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion context
- subst' metasenv' ugraph1
- (Cic.Appl[c;s']) coercion_tgt
+ avoid_double_coercion context subst' metasenv'
+ ugraph1 newt coercion_tgt
in
newt, tty, subst', metasenv', ugraph1
| CoercGraph.NoCoercion
in
let tl',applty,subst''',metasenv''',ugraph3 =
eat_prods true subst'' metasenv'' context
- he hetype tlbody_and_type ugraph2
+ he' hetype tlbody_and_type ugraph2
in
avoid_double_coercion context
subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2''))))
+ and avoid_double_coercion context subst metasenv ugraph t ty =
+ 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 newt =
+ match c with
+ Cic.Appl l -> Cic.Appl (l @ [head])
+ | _ -> Cic.Appl [c;head]
+ in
+ (try
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ newt, ty, subst, metasenv, ugraph
+ with
+ RefineFailure _ ->
+ prerr_endline ("#### Coercion not packed (Refine_failure): " ^
+ CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+ assert false
+ | Uncertain _ ->
+ prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
+ CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+ assert false)
+ | _ -> assert false) (* the composite coercion must exist *)
+ else
+ t, ty, subst, metasenv, ugraph
+
and eat_prods
allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
=
~f:(fun _ ->
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst he
- context ^ "(that has type " ^
+ context ^ " (that has type " ^
CicMetaSubst.ppterm_in_context subst hetype
context ^ ") is here applied to " ^
string_of_int (List.length tlbody_and_type) ^
(* we search a coercion from hety to s *)
let coer, tgt_carr =
let carr t subst context =
- CicMetaSubst.apply_subst subst t
+ CicReduction.whd ~delta:false
+ context (CicMetaSubst.apply_subst subst t )
in
let c_hety = carr hety subst context in
let c_s = carr s subst context in
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion c ->
+ try
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ (Cic.Appl[c;hete]) ugraph in
let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion context
- subst metasenv ugraph
- (Cic.Appl[c;hete]) tgt_carr in
- try
- let newty,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
+ avoid_double_coercion context subst metasenv
+ ugraph newt tgt_carr in
let subst,metasenv,ugraph1 =
fo_unif_subst subst context metasenv
newhety s ugraph
in
newt, subst, metasenv, ugraph
- with _ ->
- enrich localization_tbl hete
+ with _ ->
+ enrich localization_tbl hete
~f:(fun _ ->
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
;;
(* sara' piu' veloce che raffinare da zero? mah.... *)
-let pack_coercion metasenv t =
+let pack_coercion metasenv ctx t =
let module C = Cic in
let rec merge_coercions ctx =
let aux = (fun (u,t) -> u,merge_coercions ctx t) in
| 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 ->
+ | C.Appl l ->
+ let l = List.map (merge_coercions ctx) l in
+ let t = C.Appl l in
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)
+ 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
| C.Var (uri,exp_named_subst) ->
let exp_named_subst = List.map aux exp_named_subst in
C.Var (uri, exp_named_subst)
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 =
+ let ctx' =
List.fold_left
(fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
ctx fl
let fl =
List.map
(fun (name,idx,ty,bo) ->
- (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
+ (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
fl
in
C.Fix (fno, fl)
| C.CoFix (fno, fl) ->
- let ctx =
+ let ctx' =
List.fold_left
(fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
ctx fl
let fl =
List.map
(fun (name,ty,bo) ->
- (name, merge_coercions ctx ty, merge_coercions ctx bo))
+ (name, merge_coercions ctx ty, merge_coercions ctx' bo))
fl
in
C.CoFix (fno, fl)
in
- merge_coercions [] t
+ merge_coercions ctx t
;;
let pack_coercion_obj obj =
let body =
match body with
| None -> None
- | Some body -> Some (pack_coercion [] body)
+ | Some body -> Some (pack_coercion [] [] body)
in
- let ty = pack_coercion [] ty 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)
+ | Some body -> Some (pack_coercion [] [] body)
in
- let ty = pack_coercion [] ty 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
+ List.fold_right
+ (fun item ctx ->
+ let item' =
+ match item with
+ Some (name, C.Decl t) ->
+ Some (name, C.Decl (pack_coercion conjectures ctx t))
+ | Some (name, C.Def (t,None)) ->
+ Some (name,C.Def (pack_coercion conjectures ctx t,None))
+ | Some (name, C.Def (t,Some ty)) ->
+ Some (name, C.Def (pack_coercion conjectures ctx t,
+ Some (pack_coercion conjectures ctx ty)))
+ | None -> None
+ in
+ item'::ctx
+ ) ctx []
in
- ((i,ctx,pack_coercion conjectures ty)))
- conjectures
+ ((i,ctx,pack_coercion conjectures ctx ty))
+ ) conjectures
in
- let body = pack_coercion conjectures body in
- let ty = pack_coercion conjectures ty 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 arity = pack_coercion [] [] arity in
let cl =
- List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl
+ List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
in
(name, ind, arity, cl))
indtys
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
projects / helm.git / blobdiff