exception AssertFailure of string Lazy.t;;
let insert_coercions = ref true
+let pack_coercions = ref true
let debug_print = fun _ -> ()
+(* let debug_print x = prerr_endline (Lazy.force x);; *)
let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
let is_a_double_coercion t =
let last_of l =
- let rec aux = function
- | x::[] -> x
- | x::tl -> aux tl
+ let rec aux acc = function
+ | x::[] -> acc,x
+ | x::tl -> aux (acc@[x]) tl
| [] -> assert false
in
- aux l
- in
- let dummyres =
- false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
+ aux [] l
in
+ let imp = Cic.Implicit None in
+ let dummyres = false,imp, imp,imp,imp 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
+ | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ let sib2,head = last_of tl2 in
+ true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
+ (c2::sib2@[Cic.Implicit None])])
| _ -> dummyres)
| _ -> dummyres
+
+let more_args_than_expected subst he context hetype' tlbody_and_type =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst he context ^
+ " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
+ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected")
+;;
+
+let mk_prod_of_metas metasenv context' subst args =
+ let rec mk_prod metasenv context' = function
+ | [] ->
+ 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)
+ | (_,argty)::tl ->
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context'
+ in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
+ in
+ let meta = Cic.Meta (idx,irl) in
+ let name =
+ (* The name must be fresh for context. *)
+ (* Nevertheless, argty is well-typed only in context. *)
+ (* 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'. *)
+ let name_hint =
+ (* Cic.Name "pippo" *)
+ FreshNamesGenerator.mk_fresh_name ~subst metasenv
+ (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+ (CicMetaSubst.apply_subst_context subst context')
+ Cic.Anonymous
+ ~typ:(CicMetaSubst.apply_subst subst argty)
+ in
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name ~subst
+ [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
+ in
+ let metasenv,target =
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
+ in
+ metasenv,Cic.Prod (name,meta,target)
+ in
+ mk_prod metasenv context' args
+;;
let rec type_of_constant uri ugraph =
let module C = Cic in
type_of_aux subst metasenv context he ugraph
in
let tlbody_and_type,subst'',metasenv'',ugraph2 =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) tl ([],subst',metasenv',ugraph1)
+ typeof_list subst' metasenv' context ugraph1 tl
in
- let tl',applty,subst''',metasenv''',ugraph3 =
+ let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
eat_prods true subst'' metasenv'' context
he' hetype tlbody_and_type ugraph2
in
- avoid_double_coercion context
- subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
+ let newappl = (C.Appl (coerced_he::coerced_args)) in
+ avoid_double_coercion
+ context subst''' metasenv''' ugraph3 newappl applty
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
subst,metasenv,ugraph)
| _ -> (* easy case *)
let tlbody_and_type,subst,metasenv,ugraph4 =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+ typeof_list subst metasenv context ugraph4 (right_args @ [term'])
in
- let _,_,subst,metasenv,ugraph4 =
+ let _,_,_,subst,metasenv,ugraph4 =
eat_prods false subst metasenv context
outtype outtypety tlbody_and_type ugraph4
in
(CicPp.ppterm t2''))))
and avoid_double_coercion context subst metasenv ugraph t ty =
- let b, c1, c2, head = is_a_double_coercion t in
+ let b, c1, c2, head, c1_c2_implicit = 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
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (fun c ->
+ (function
+ | c when not (CoercGraph.is_composite c) ->
+ debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
+ None
+ | c ->
let newt =
match c with
| Cic.Appl l -> Cic.Appl (l @ [head])
| _ -> Cic.Appl [c;head]
in
+ debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
(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));
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ debug_print (lazy "tipa...");
+ let subst, metasenv, ugraph =
+ (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print (lazy "unifica...");
Some (newt, ty, subst, metasenv, ugraph)
- with RefineFailure _ | Uncertain _ -> None))
+ with
+ | RefineFailure s | Uncertain s when not !pack_coercions->
+ debug_print s; debug_print (lazy "stop\n");None
+ | RefineFailure s | Uncertain s ->
+ debug_print s;debug_print (lazy "goon\n");
+ try
+ pack_coercions := false; (* to avoid diverging *)
+ let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context c1_c2_implicit ugraph
+ in
+ pack_coercions := true;
+ let b, _, _, _, _ =
+ is_a_double_coercion refined_c1_c2_implicit
+ in
+ if b then
+ None
+ else
+ let head' =
+ match refined_c1_c2_implicit with
+ | Cic.Appl l -> HExtlib.list_last l
+ | _ -> assert false
+ in
+ let subst, metasenv, ugraph =
+ try fo_unif_subst subst context metasenv
+ head head' ugraph
+ with RefineFailure s| Uncertain s->
+ debug_print s;assert false
+ in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv
+ refined_c1_c2_implicit t ugraph
+ in
+ Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
+ with
+ | RefineFailure s | Uncertain s ->
+ pack_coercions := true;debug_print s;None
+ | exn -> pack_coercions := true; raise exn))
candidates
in
(match selected with
| Some x -> x
| None ->
- prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
- assert false)
+ debug_print
+ (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
+ t, ty, subst, metasenv, ugraph)
| _ -> assert false) (* the composite coercion must exist *)
else
t, ty, subst, metasenv, ugraph
+ and typeof_list subst metasenv context ugraph l =
+ let tlbody_and_type,subst,metasenv,ugraph =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) l ([],subst,metasenv,ugraph)
+ in
+ tlbody_and_type,subst,metasenv,ugraph
+
and eat_prods
- allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
+ allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
=
- let rec mk_prod metasenv context' =
- function
- [] ->
- 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)
- | (_,argty)::tl ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- let meta = Cic.Meta (idx,irl) in
- let name =
- (* The name must be fresh for context. *)
- (* Nevertheless, argty is well-typed only in context. *)
- (* 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'. *)
- let name_hint =
- (* Cic.Name "pippo" *)
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
- in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name ~subst
- [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
- in
- let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
- in
- metasenv,Cic.Prod (name,meta,target)
- in
- let ((subst,metasenv,ugraph1),hetype') =
- if CicUtil.is_meta_closed hetype then
- (subst,metasenv,ugraph),hetype
- else
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- try
- fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
- with exn ->
- enrich localization_tbl he
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"
- (* "\nReason: " ^ Lazy.force exn*)))) exn
+ (* aux function to add coercions to funclass *)
+ let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+ (* {{{ body *)
+ let pristinemenv = metasenv in
+ let metasenv,hetype' =
+ mk_prod_of_metas metasenv context subst args_bo_and_ty
+ in
+ try
+ let subst,metasenv,ugraph =
+ fo_unif_subst_eat_prods
+ subst context metasenv hetype hetype' ugraph
+ in
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ with RefineFailure s | Uncertain s as exn
+ when allow_coercions && !insert_coercions ->
+ (* {{{ we search a coercion of the head (saturated) to funclass *)
+ let metasenv = pristinemenv in
+ debug_print (lazy
+ ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
+ " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^
+ " cause: " ^ Lazy.force s));
+ let how_many_args_are_needed =
+ let rec aux n = function
+ | Cic.Prod(_,_,t) -> aux (n+1) t
+ | _ -> n
+ in
+ aux 0 (CicMetaSubst.apply_subst subst hetype)
+ in
+ let args, remainder =
+ HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
+ in
+ let args = List.map fst args in
+ let x =
+ if args <> [] then
+ match he with
+ | Cic.Appl l -> Cic.Appl (l@args)
+ | _ -> Cic.Appl (he::args)
+ else
+ he
+ in
+ let x,xty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context x ugraph
+ in
+ let carr_src =
+ CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
+ in
+ let carr_tgt = CoercDb.Fun 0 in
+ match CoercGraph.look_for_coercion' carr_src carr_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotMetaClosed
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ match
+ HExtlib.list_findopt
+ (fun coerc ->
+ let t = Cic.Appl [coerc;x] in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+ try
+ (* we want this to be available in the error handler fo the
+ * following (so it has its own try. *)
+ let t,tty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context t ugraph
+ in
+ try
+ let metasenv, hetype' =
+ mk_prod_of_metas metasenv context subst remainder
+ in
+ debug_print (lazy
+ (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
+ CicMetaSubst.ppterm subst hetype'));
+ let subst,metasenv,ugraph =
+ fo_unif_subst_eat_prods
+ subst context metasenv tty hetype' ugraph
+ in
+ debug_print (lazy " success!");
+ Some (subst,metasenv,ugraph,tty,t,remainder)
+ with
+ | Uncertain _ | RefineFailure _
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ try
+ let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
+ fix_arity
+ metasenv context subst t tty remainder ugraph
+ in
+ Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
+ with exn -> None
+ with exn -> None)
+ candidates
+ with
+ | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ | None ->
+ enrich localization_tbl he
+ ~f:(fun _-> more_args_than_expected subst he context hetype
+ args_bo_and_ty) exn
+ (* }}} end coercion to funclass stuff *)
+ (* }}} end fix_arity *)
in
- let rec eat_prods metasenv subst context hetype ugraph =
+ (* aux function to process the type of the head and the args in parallel *)
+ let rec eat_prods_and_args
+ pristinemenv metasenv subst context he hetype ugraph newargs
+ =
+ (* {{{ body *)
function
- | [] -> [],metasenv,subst,hetype,ugraph
+ | [] -> newargs,subst,metasenv,he,hetype,ugraph
| (hete, hety)::tl ->
- (match (CicReduction.whd ~subst context hetype) with
- Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- try
- let subst,metasenv,ugraph1 =
- fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
- in
- hete,subst,metasenv,ugraph1
- with exn when allow_coercions && !insert_coercions ->
- (* we search a coercion from hety to s *)
- let coer, tgt_carr =
- let carr t subst context =
- 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
- CoercGraph.look_for_coercion c_hety c_s, c_s
- in
- (match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl hete
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (fun c ->
- try
- let t = Cic.Appl[c;hete] in
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- t ugraph
- in
- let newt, _, subst, metasenv, ugraph =
- 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
- Some (newt, subst, metasenv, ugraph)
- with Uncertain _ | RefineFailure _ -> None)
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn))
- | exn ->
+ match (CicReduction.whd ~subst context hetype) with
+ | Cic.Prod (n,s,t) ->
+ let arg,subst,metasenv,ugraph1 =
+ try
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst_eat_prods2
+ subst context metasenv hety s ugraph
+ in
+ (hete,hety),subst,metasenv,ugraph1
+ (* {{{ we search a coercion from hety to s if fails *)
+ with RefineFailure _ | Uncertain _ as exn
+ when allow_coercions && !insert_coercions ->
+ let coer, tgt_carr =
+ let carr t subst context =
+ 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
+ CoercGraph.look_for_coercion c_hety c_s, c_s
+ in
+ (match coer with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
enrich localization_tbl hete
- ~f:(fun _ ->
+ (RefineFailure
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn
- in
- let coerced_args,metasenv',subst',t',ugraph2 =
- eat_prods metasenv subst context
- (CicSubstitution.subst arg t) ugraph1 tl
- in
- arg::coerced_args,metasenv',subst',t',ugraph2
- | _ ->
- raise (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype'
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"))))
+ (* "\nReason: " ^ Lazy.force e*))))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl hete
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))))
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ try
+ let t = Cic.Appl[c;hete] in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ t ugraph
+ in
+ let newt, newty, subst, metasenv, ugraph =
+ 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
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ (match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*)))) exn))
+ | exn ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context ^
+ "\nReason: " ^ Printexc.to_string exn))) exn
+ (* }}} end coercion stuff *)
+ in
+ eat_prods_and_args pristinemenv metasenv subst context he
+ (CicSubstitution.subst (fst arg) t)
+ ugraph1 (newargs@[arg]) tl
+ | _ ->
+ try
+ let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+ fix_arity
+ pristinemenv context subst he hetype
+ (newargs@[hete,hety]@tl) ugraph
+ in
+ eat_prods_and_args metasenv
+ metasenv subst context he hetype' ugraph [] args_bo_and_ty
+ with RefineFailure s | Uncertain s ->
+ (* unable to fix arity *)
+ let msg =
+ more_args_than_expected
+ subst he context hetype args_bo_and_ty
+ in
+ raise (RefineFailure msg)
+ (* }}} *)
+ in
+ (* first we check if we are in the simple case of a meta closed term *)
+ let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+ if CicUtil.is_meta_closed hetype then
+ (* this optimization is to postpone fix_arity (the most common case)*)
+ subst,metasenv,ugraph,hetype,he,args_bo_and_ty
+ else
+ (* this (says CSC) is also useful to infer dependent types *)
+ fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
in
- let coerced_args,metasenv,subst,t,ugraph2 =
- eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
+ let coerced_args,subst,metasenv,he,t,ugraph =
+ eat_prods_and_args
+ metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
in
- coerced_args,t,subst,metasenv,ugraph2
+ he,(List.map fst coerced_args),t,subst,metasenv,ugraph
in
(* eat prods ends here! *)
| 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
+ let b,_,_,_,_ = is_a_double_coercion t in
(* prerr_endline "CANDIDATO!!!!"; *)
if b then
let ugraph = CicUniv.empty_ugraph in
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
+(* vim:set foldmethod=marker: *)
projects / helm.git / blobdiff