exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;
+(* for internal use only; the integer is the number of surplus arguments *)
+exception MoreArgsThanExpected of int * exn;;
+
let insert_coercions = ref true
+let pack_coercions = ref true
+
+let debug = false;;
+
+let debug_print =
+ if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
-let debug_print = fun _ -> ()
+let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
+
+let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
+ try
+let foo () =
+ CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods2.HExtlib.profile foo ()
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
+let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
+
+let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
+ try
+let foo () =
+ CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods.HExtlib.profile foo ()
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
let profiler = HExtlib.profile "CicRefine.fo_unif"
match exn with
RefineFailure msg -> RefineFailure (f msg)
| Uncertain msg -> Uncertain (f msg)
- | _ -> assert false in
+ | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
+ | Sys.Break -> raise exn
+ | _ -> prerr_endline (Printexc.to_string exn); assert false
+ in
let loc =
try
Cic.CicHash.find localization_tbl t
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 ->
+ | Cic.Appl (c1::tl) when CoercDb.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 CoercDb.is_a_coercion' c2 ->
+ let sib2,head = last_of tl2 in
+ true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
+ (c2::sib2@[imp])])
| _ -> 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)
+
+let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
+=
+ let len = List.length tlbody_and_type in
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
+ " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
+ ") is here applied to " ^ string_of_int len ^
+ " arguments but here it can handle only up to " ^
+ string_of_int (len - residuals) ^ " arguments")
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
- let subst, metasenv, ugraph =
- CicUnification.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
- | _ -> assert false) (* the composite coercion must exist *)
- else
- t, ty, subst, metasenv, ugraph
+ enrich localization_tbl he ~f:(fun _-> msg) exn
+;;
+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
let module R = CicReduction in
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
with
- _ ->
+ Failure _ ->
enrich localization_tbl t
- (RefineFailure (lazy "Not a close term")))
+ (RefineFailure (lazy "Not a closed term")))
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
check_exp_named_subst
subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ (try
+ let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+ t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| C.Sort _ ->
t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
| C.Implicit infos ->
let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
- (try
- let subst''',metasenv''',ugraph3 =
- fo_unif_subst subst'' context metasenv''
- inferredty ty' ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- exn ->
- enrich localization_tbl te'
- ~f:(fun _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst'' te'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst'' inferredty
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst'' ty' context)) exn
- )
- | C.Prod (name,s,t) ->
- let carr t subst context = CicMetaSubst.apply_subst subst t in
- let coerce_to_sort in_source tgt_sort t type_to_coerce
- subst context metasenv uragph
- =
- if not !insert_coercions then
- t,type_to_coerce,subst,metasenv,ugraph
- else
- let coercion_src = carr type_to_coerce subst context in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- 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
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl t
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst t context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion c ->
- let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context
- subst metasenv ugraph
- (Cic.Appl[c;t]) coercion_tgt
- in
- newt, tty, subst, metasenv, ugraph)
+ let (te', ty'), subst''',metasenv''',ugraph3 =
+ coerce_to_something true localization_tbl te' inferredty ty'
+ subst'' metasenv'' context ugraph2
in
+ C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
+ | C.Prod (name,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
in
let s',sort1,subst', metasenv',ugraph1 =
- coerce_to_sort true (Cic.Type(CicUniv.fresh()))
+ coerce_to_sort localization_tbl
s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (name,(C.Decl s')))::context) in
context_for_t t ugraph1
in
let t',sort2,subst'',metasenv'',ugraph2 =
- coerce_to_sort false (Cic.Type(CicUniv.fresh()))
+ coerce_to_sort localization_tbl
t' sort2 subst'' context_for_t metasenv'' ugraph2
in
let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
+ sort_of_prod localization_tbl subst'' metasenv''
+ context (name,s') t' (sort1,sort2) ugraph2
in
C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
| C.Lambda (n,s,t) ->
-
let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
+ type_of_aux subst metasenv context s ugraph
+ in
let s',sort1,subst',metasenv',ugraph1 =
- if not !insert_coercions then
- s',sort1, subst', metasenv', ugraph1
- else
- match CicReduction.whd ~subst:subst' context sort1 with
- | 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
- match boh with
- | CoercGraph.SomeCoercion c ->
- let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion context
- subst' metasenv' ugraph1
- (Cic.Appl[c;s']) coercion_tgt
- in
- newt, tty, subst', metasenv', ugraph1
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl s'
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
- subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl s'
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst s' context ^
- " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context
- subst coercion_src context ^ " that is not a sort")))
+ coerce_to_sort localization_tbl
+ s' sort1 subst' context metasenv' ugraph1
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst'',metasenv'',ugraph2
+ C.LetIn (n,s',t'),
+ CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
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
- hetype tlbody_and_type ugraph2
+ 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 =
(lazy ("Unkown mutual inductive definition " ^
U.string_of_uri uri)))
in
+ if List.length constructors <> List.length pl then
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy "Wrong number of cases")) ;
let rec count_prod t =
match CicReduction.whd ~subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst term'
+ lazy ("(10)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst actual_type
+ CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst expected_type' context))
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
in
let rec instantiate_prod t =
function
(* TODO: check if the sort elimination
* is allowed: [(I q1 ... qr)|B] *)
let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- List.fold_left
- (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+ List.fold_right
+ (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
let constructor =
if left_args = [] then
(C.MutConstruct (uri,i,j,exp_named_subst))
type_of_aux subst metasenv context constructor ugraph1
in
let outtypeinstance,subst,metasenv,ugraph3 =
- check_branch 0 context metasenv subst no_left_params
- actual_type constructor' expected_type ugraph2
+ try
+ check_branch 0 context metasenv subst
+ no_left_params actual_type constructor' expected_type
+ ugraph2
+ with
+ exn ->
+ enrich localization_tbl constructor'
+ ~f:(fun _ ->
+ lazy ("(11)The term " ^
+ CicMetaSubst.ppterm_in_context metasenv subst p'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context metasenv subst actual_type
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context metasenv subst expected_type
+ context)) exn
in
- (pl @ [p'],j+1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- ([],1,[],subst,metasenv,ugraph3) pl
+ (p'::pl,j-1,
+ outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+ pl ([],List.length pl,[],subst,metasenv,ugraph3)
in
(* we are left to check that the outype matches his instances.
candidate_oty,ugraph,metasenv,subst
with
CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
+ | RefineFailure _ | Uncertain _ ->
None,ugraph,metasenv,subst
) (Some instance',ugraph4,metasenv,subst) tl
in
| 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
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
- outtypety tlbody_and_type ugraph4
+ outtype outtypety tlbody_and_type ugraph4
in
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(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 ("(12)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst p
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst instance
+ context)))
+ (subst,metasenv,ugraph5) pl' outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
(C.Appl(outtype::right_args@[term]))),
subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1,len =
List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
+ (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
in
fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl ty')) :: types, ugraph
- ) ([],subst,metasenv,[],ugraph) fl
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
+ :: types, ugraph, len+1
+ ) ([],subst,metasenv,[],ugraph,0) fl
in
- let len = List.length types in
let context' = types@context in
let fl_bo',subst,metasenv,ugraph2 =
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 ("(13)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
+ context))
in
fl @ [bo'] , subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
in
C.Fix (i,fl''),ty,subst,metasenv,ugraph2
| C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1 =
+ let fl_ty',subst,metasenv,types,ugraph1,len =
List.fold_left
- (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
+ (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
let ty',_,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context ty ugraph
in
fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl ty')) :: types, ugraph1
- ) ([],subst,metasenv,[],ugraph) fl
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
+ types, ugraph1, len+1
+ ) ([],subst,metasenv,[],ugraph,0) fl
in
- let len = List.length types in
let context' = types@context in
let fl_bo',subst,metasenv,ugraph2 =
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 ("(14)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst bo
+ context' ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
+ context' ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
+ context))
in
fl @ [bo'],subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
| Some t,Some (_,C.Def (ct,_)) ->
let subst',metasenv',ugraph' =
(try
+(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
+ * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
fo_unif_subst subst context metasenv t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
(try
fo_unif_subst
subst' context metasenv' inferredty ct ugraph1
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t'], subst'',metasenv'',ugraph2
| None, Some _ ->
- raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
+ raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
with
Invalid_argument _ ->
raise
(RefineFailure
(lazy (sprintf
"Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext subst canonical_context))))
+ (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
and check_exp_named_subst metasubst metasenv context tl ugraph =
let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
with _ ->
raise (RefineFailure (lazy
("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasubst' typeoft ^
+ CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
" not unifiable with " ^
- CicMetaSubst.ppterm metasubst' typeofvar)))
+ CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
in
(* FIXME: no mere tail recursive! *)
let exp_name_subst, metasubst''', metasenv''', ugraph4 =
check_exp_named_subst_aux metasubst metasenv [] tl ugraph
- and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
+ and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
+ ugraph
+ =
let module C = Cic in
let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicReduction.whd ~subst context t1 in
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
C.Sort (C.Type t1),subst,metasenv,ugraph
| (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 *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv,ugraph1) =
+ try
fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2'' ugraph
+ with _ -> assert false (* unification against a metavariable *)
in
t2'',subst,metasenv,ugraph1
+ | (C.Sort _,_)
+ | (C.Meta _,_) ->
+ enrich localization_tbl s
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
| _,_ ->
- raise
- (RefineFailure
- (lazy
- (sprintf
- ("Two sorts were expected, found %s " ^^
- "(that reduces to %s) and %s (that reduces to %s)")
- (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
- (CicPp.ppterm t2''))))
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
+
+ and avoid_double_coercion context subst metasenv ugraph t ty =
+ if not !pack_coercions then
+ t,ty,subst,metasenv,ugraph
+ else
+ 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
+ (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (function (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));
+ (try
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context c 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 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
+ let old_pack_coercions = !pack_coercions in
+ 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 := old_pack_coercions;
+ 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 ->
+ debug_print
+ (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
+ t, ty, subst, metasenv, ugraph)
+ | _ -> t, ty, subst, metasenv, ugraph)
+ else
+ t, ty, subst, metasenv, ugraph
- and eat_prods
- allow_coercions subst metasenv context hetype tlbody_and_type 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 args_bo_and_ty ugraph
=
- let rec mk_prod metasenv context' =
+ (* given he:hety, gives beack all (c he) such that (c e):?->? *)
+ let fix_arity n metasenv context subst he hetype ugraph =
+ let hetype = CicMetaSubst.apply_subst subst hetype in
+ let src = CoercDb.coerc_carr_of_term hetype in
+ let tgt = CoercDb.Fun 0 in
+ match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+ | CoercGraph.NoCoercion -> []
+ | CoercGraph.NotMetaClosed
+ | CoercGraph.NotHandled _ ->
+ raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
+ | CoercGraph.SomeCoercionToTgt candidates
+ | CoercGraph.SomeCoercion candidates ->
+ HExtlib.filter_map
+ (fun (metasenv,last,coerc) ->
+ let pp t =
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context in
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last he ugraph in
+ debug_print (lazy ("New head: "^ pp coerc));
+ try
+ let tty,ugraph =
+ CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
+ debug_print (lazy (" has type: "^ pp tty));
+ Some (coerc,tty,subst,metasenv,ugraph)
+ with
+ | Uncertain _ | RefineFailure _
+ | HExtlib.Localized (_,Uncertain _)
+ | HExtlib.Localized (_,RefineFailure _) -> None
+ | exn -> assert false)
+ candidates
+ in
+ (* aux function to process the type of the head and the args in parallel *)
+ let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
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)
+ | [] -> newargs,subst,metasenv,he,hetype,ugraph
+ | (hete, hety)::tl as args ->
+ match (CicReduction.whd ~subst context hetype) with
+ | Cic.Prod (n,s,t) ->
+ let arg,subst,metasenv,ugraph =
+ coerce_to_something allow_coercions localization_tbl
+ hete hety s subst metasenv context ugraph in
+ eat_prods_and_args
+ metasenv subst context he (CicSubstitution.subst (fst arg) t)
+ ugraph (newargs@[arg]) tl
+ | _ ->
+ let he =
+ match he, newargs with
+ | _, [] -> he
+ | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
+ | _ -> Cic.Appl (he::List.map fst newargs)
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)
+ (*{{{*) debug_print (lazy
+ let pp x =
+ CicMetaSubst.ppterm_in_context ~metasenv subst x context in
+ "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
+ "\n but is applyed to: " ^ String.concat ";"
+ (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+ let possible_fixes =
+ fix_arity (List.length args) metasenv context subst he hetype
+ ugraph in
+ match
+ HExtlib.list_findopt
+ (fun (he,hetype,subst,metasenv,ugraph) ->
+ (* {{{ *)debug_print (lazy ("Try fix: "^
+ CicMetaSubst.ppterm_in_context ~metasenv subst he context));
+ debug_print (lazy (" of type: "^
+ CicMetaSubst.ppterm_in_context
+ ~metasenv subst hetype context)); (* }}} *)
+ try
+ Some (eat_prods_and_args
+ metasenv subst context he hetype ugraph [] args)
+ with
+ | RefineFailure _ | Uncertain _
+ | HExtlib.Localized (_,RefineFailure _)
+ | HExtlib.Localized (_,Uncertain _) -> None)
+ possible_fixes
+ with
+ | Some x -> x
+ | None ->
+ raise
+ (MoreArgsThanExpected
+ (List.length args, RefineFailure (lazy "")))
in
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv,ugraph1) =
- 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"
- (CicPp.ppterm hetype)
- (CicPp.ppterm hetype')
- (CicMetaSubst.ppmetasenv [] metasenv)
- (CicMetaSubst.ppsubst subst)));
- raise exn
+ (* 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 (CicMetaSubst.apply_subst subst 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 *)
+ 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 _ | Uncertain _ ->
+ subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
+ in
+ let coerced_args,subst,metasenv,he,t,ugraph =
+ try
+ eat_prods_and_args
+ metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
+ with
+ MoreArgsThanExpected (residuals,exn) ->
+ more_args_than_expected localization_tbl metasenv
+ subst he context hetype' residuals args_bo_and_ty exn
+ in
+ he,(List.map fst coerced_args),t,subst,metasenv,ugraph
+ and coerce_to_something
+ allow_coercions localization_tbl t infty expty subst metasenv context ugraph
+ =
+ let module CS = CicSubstitution in
+ let module CR = CicReduction in
+ let cs_subst = CS.subst ~avoid_beta_redexes:true in
+ let coerce_atom_to_something t infty expty subst metasenv context ugraph =
+ debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
+ let coer =
+ CoercGraph.look_for_coercion metasenv subst context infty expty
+ in
+ match coer with
+ | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
+ "coerce_atom_to_something fails since not meta closed"))
+ | CoercGraph.NoCoercion
+ | CoercGraph.SomeCoercionToTgt _
+ | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+ "coerce_atom_to_something fails since no coercions found"))
+ | CoercGraph.SomeCoercion candidates ->
+ debug_print (lazy (string_of_int (List.length candidates) ^
+ " candidates found"));
+ let uncertain = ref false in
+ let selected =
+ let posibilities =
+ HExtlib.filter_map
+ (fun (metasenv,last,c) ->
+ try
+ (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
+ " <==> " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
+ "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+ context));
+ debug_print (lazy ("FO_UNIF_SUBST: " ^
+ CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last t ugraph
+ in
+ 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
+ in
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv newhety expty ugraph in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with
+ | Uncertain _ -> uncertain := true; None
+ | RefineFailure _ -> None)
+ candidates
+ in
+ match
+ List.fast_sort
+ (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
+ posibilities
+ with
+ | [] -> None
+ | x::_ -> Some x
+ in
+ match selected with
+ | Some x -> x
+ | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
+ | None -> raise (RefineFailure (lazy "coerce_atom fails"))
in
- let rec eat_prods metasenv subst context hetype ugraph =
- function
- | [] -> [],metasenv,subst,hetype,ugraph
- | (hete, hety)::tl ->
- (match hetype with
- Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- try
- let subst,metasenv,ugraph1 =
- fo_unif_subst 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 =
- 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
+ let rec coerce_to_something_aux
+ t infty expty subst metasenv context ugraph
+ =
+ try
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv infty expty ugraph
+ in
+ (t, expty), subst, metasenv, ugraph
+ with Uncertain _ | RefineFailure _ as exn ->
+ if not allow_coercions || not !insert_coercions then
+ enrich localization_tbl t exn
+ else
+ let whd = CicReduction.whd ~delta:false in
+ let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
+ let infty = clean infty subst context in
+ let expty = clean expty subst context in
+ let t = clean t subst context in
+ (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
+ CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
+ let (coerced,_),subst,metasenv,_ as result =
+ match infty, expty, t with
+ | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
+ (*{{{*) debug_print (lazy "FIX");
+ (match fl with
+ [name,i,_(* infty *),bo] ->
+ let context_bo =
+ Some (Cic.Name name,Cic.Decl expty)::context in
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux (Cic.Rel 1)
+ (CS.lift 1 expty) (CS.lift 1 infty) subst
+ metasenv context_bo ugraph in
+ let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
+ let (bo,_), subst, metasenv, ugraph =
+ coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
+ expty) subst
+ metasenv context_bo ugraph
+ in
+ (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
+ | _ -> assert false (* not implemented yet *)) (*}}}*)
+ | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
+ (*{{{*) debug_print (lazy "CASE");
+ (* {{{ helper functions *)
+ let get_cl_and_left_p uri tyno outty ugraph =
+ match CicEnvironment.get_obj ugraph uri with
+ | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
+ let count_pis t =
+ let rec aux ctx t =
+ match CicReduction.whd ~delta:false ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ let ctx = Some (name, Cic.Decl src) :: ctx in
+ 1 + aux ctx tgt
+ | _ -> 0
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 c ->
- 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
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- newt, subst, metasenv, ugraph
- with _ ->
- 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: " ^ Lazy.force e*)))) exn
+ aux [] t
+ in
+ let rec skip_lambda_delifting t n =
+ match t,n with
+ | _,0 -> t
+ | Cic.Lambda (_,_,t),n ->
+ skip_lambda_delifting
+ (CS.subst (Cic.Implicit None) t) (n - 1)
+ | _ -> assert false
+ in
+ let get_l_r_p n = function
+ | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
+ | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
+ HExtlib.split_nth n args
+ | _ -> assert false
+ in
+ let _, _, ty, cl = List.nth tl tyno in
+ let pis = count_pis ty in
+ let rno = pis - leftno in
+ let t = skip_lambda_delifting outty rno in
+ let left_p, _ = get_l_r_p leftno t in
+ let instantiale_with_left cl =
+ List.map
+ (fun ty ->
+ List.fold_left
+ (fun t p -> match t with
+ | Cic.Prod (_,_,t) ->
+ cs_subst p t
+ | _-> assert false)
+ ty left_p)
+ cl
+ in
+ let cl = instantiale_with_left (List.map snd cl) in
+ cl, left_p, leftno, rno, ugraph
+ | _ -> raise exn
+ in
+ let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+ match t,n with
+ | _,0 ->
+ let rec mkr n = function
+ | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
in
- let coerced_args,metasenv',subst',t',ugraph2 =
- eat_prods metasenv subst context
- (CicSubstitution.subst arg t) ugraph1 tl
+ let bo =
+ CicReplace.replace_lifting
+ ~equality:(fun _ -> CicUtil.alpha_equivalence)
+ ~context:ctx
+ ~what:(matched::right_p)
+ ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
+ ~where:bo
in
- arg::coerced_args,metasenv',subst',t',ugraph2
- | _ -> assert false
- )
- in
- let coerced_args,metasenv,subst,t,ugraph2 =
- eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
+ bo
+ | Cic.Lambda (name, src, tgt),_ ->
+ Cic.Lambda (name, src,
+ keep_lambdas_and_put_expty
+ (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
+ (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
+ | _ -> assert false
+ in
+ let eq_uri, eq, eq_refl =
+ match LibraryObjects.eq_URI () with
+ | None -> HLog.warn "no default equality"; raise exn
+ | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
+ in
+ let add_params
+ metasenv subst context uri tyno cty outty mty m leftno i
+ =
+ let rec aux context outty par k mty m = function
+ | Cic.Prod (name, src, tgt) ->
+ let t,k =
+ aux
+ (Some (name, Cic.Decl src) :: context)
+ (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
+ (CS.lift 1 mty) (CS.lift 1 m) tgt
+ in
+ Cic.Prod (name, src, t), k
+ | Cic.MutInd _ ->
+ let k =
+ let k = Cic.MutConstruct (uri,tyno,i,[]) in
+ if par <> [] then Cic.Appl (k::par) else k
+ in
+ Cic.Prod (Cic.Name "p",
+ Cic.Appl [eq; mty; m; k],
+ (CS.lift 1
+ (CR.head_beta_reduce ~delta:false
+ (Cic.Appl [outty;k])))),k
+ | Cic.Appl (Cic.MutInd _::pl) ->
+ let left_p,right_p = HExtlib.split_nth leftno pl in
+ let has_rights = right_p <> [] in
+ let k =
+ let k = Cic.MutConstruct (uri,tyno,i,[]) in
+ Cic.Appl (k::left_p@par)
+ in
+ let right_p =
+ try match
+ CicTypeChecker.type_of_aux' ~subst metasenv context k
+ CicUniv.oblivion_ugraph
+ with
+ | Cic.Appl (Cic.MutInd _::args),_ ->
+ snd (HExtlib.split_nth leftno args)
+ | _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _-> assert false
+ in
+ if has_rights then
+ CR.head_beta_reduce ~delta:false
+ (Cic.Appl (outty ::right_p @ [k])),k
+ else
+ Cic.Prod (Cic.Name "p",
+ Cic.Appl [eq; mty; m; k],
+ (CS.lift 1
+ (CR.head_beta_reduce ~delta:false
+ (Cic.Appl (outty ::right_p @ [k]))))),k
+ | _ -> assert false
+ in
+ aux context outty [] 1 mty m cty
+ in
+ let add_lambda_for_refl_m pbo rno mty m k cty =
+ (* k lives in the right context *)
+ if rno <> 0 then pbo else
+ let rec aux mty m = function
+ | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
+ Cic.Lambda (name,src,
+ (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
+ | t,_ ->
+ Cic.Lambda (Cic.Name "p",
+ Cic.Appl [eq; mty; m; k],CS.lift 1 t)
+ in
+ aux mty m (pbo,cty)
+ in
+ let add_pi_for_refl_m new_outty mty m rno =
+ if rno <> 0 then new_outty else
+ let rec aux m mty = function
+ | Cic.Lambda (name, src, tgt) ->
+ Cic.Lambda (name, src,
+ aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
+ | t ->
+ Cic.Prod
+ (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
+ CS.lift 1 t)
+ in
+ aux m mty new_outty
+ in (* }}} end helper functions *)
+ (* constructors types with left params already instantiated *)
+ let outty = CicMetaSubst.apply_subst subst outty in
+ let cl, left_p, leftno,rno,ugraph =
+ get_cl_and_left_p uri tyno outty ugraph
+ in
+ let right_p, mty =
+ try
+ match
+ CicTypeChecker.type_of_aux' ~subst metasenv context m
+ CicUniv.oblivion_ugraph
+ with
+ | Cic.MutInd _ as mty,_ -> [], mty
+ | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+ snd (HExtlib.split_nth leftno args), mty
+ | _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ let new_outty =
+ keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+ in
+ debug_print
+ (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst new_outty context));
+ let _,pl,subst,metasenv,ugraph =
+ List.fold_right2
+ (fun cty pbo (i, acc, s, menv, ugraph) ->
+ (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
+ * (new_)outty right_par (K_i left_par k_par) *)
+ let infty_pbo, _ =
+ add_params menv s context uri tyno
+ cty outty mty m leftno i in
+ debug_print
+ (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst infty_pbo context));
+ let expty_pbo, k = (* k is (K_i left_par k_par) *)
+ add_params menv s context uri tyno
+ cty new_outty mty m leftno i in
+ debug_print
+ (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst expty_pbo context));
+ let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
+ debug_print
+ (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst pbo context));
+ let (pbo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux pbo infty_pbo expty_pbo
+ s menv context ugraph
+ in
+ debug_print
+ (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst pbo context));
+ (i-1, pbo::acc, subst, metasenv, ugraph))
+ cl pl (List.length pl, [], subst, metasenv, ugraph)
+ in
+ let new_outty = add_pi_for_refl_m new_outty mty m rno in
+ debug_print
+ (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst new_outty context));
+ let t =
+ if rno = 0 then
+ let refl_m=Cic.Appl[eq_refl;mty;m]in
+ Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
+ else
+ Cic.MutCase(uri,tyno,new_outty,m,pl)
+ in
+ (t, expty), subst, metasenv, ugraph (*}}}*)
+ | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
+ (*{{{*) debug_print (lazy "LAM");
+ let name_con =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst metasenv context ~typ:src2 Cic.Anonymous
+ in
+ let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
+ (* contravariant part: the argument of f:src->ty *)
+ let (rel1, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ (Cic.Rel 1) (CS.lift 1 src2)
+ (CS.lift 1 src) subst metasenv context_src2 ugraph
+ in
+ (* covariant part: the result of f(c x); x:src2; (c x):src *)
+ let name_t, bo =
+ match t with
+ | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
+ | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
+ in
+ (* we fix the possible dependency problem in the source ty *)
+ let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
+ let (bo, _), subst, metasenv, ugraph =
+ coerce_to_something_aux
+ bo ty ty2 subst metasenv context_src2 ugraph
+ in
+ let coerced = Cic.Lambda (name_t,src2, bo) in
+ (coerced, expty), subst, metasenv, ugraph (*}}}*)
+ | _ ->
+ (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst infty context ^ " ==> " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
+ coerce_atom_to_something
+ t infty expty subst metasenv context ugraph (*}}}*)
+ in
+ debug_print (lazy ("COERCE TO SOMETHING END: "^
+ CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
+ result
in
- coerced_args,t,subst,metasenv,ugraph2
+ try
+ coerce_to_something_aux t infty expty subst metasenv context ugraph
+ with Uncertain _ | RefineFailure _ as exn ->
+ let f _ =
+ lazy ("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 " ^
+ CicMetaSubst.ppterm_in_context metasenv subst expty context)
+ in
+ enrich localization_tbl ~f t exn
+
+ and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
+ match CicReduction.whd ~delta:false ~subst context infty with
+ | Cic.Meta _ | Cic.Sort _ ->
+ t,infty, subst, metasenv, ugraph
+ | src ->
+ debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst src context));
+ let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ try
+ let (t, ty_t), subst, metasenv, ugraph =
+ coerce_to_something true
+ localization_tbl t src tgt subst metasenv context ugraph
+ in
+ debug_print (lazy ("COERCE TO SORT END: "^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+ t, ty_t, subst, metasenv, ugraph
+ with HExtlib.Localized (_, exn) ->
+ let f _ =
+ lazy ("(7)The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context
+ ^ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv subst src context
+ ^ " that is not a sort")
+ in
+ enrich localization_tbl ~f t exn
in
(* eat prods ends here! *)
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
-let type_of_aux' ?localization_tbl metasenv context term ugraph =
- try
- type_of_aux' ?localization_tbl metasenv context term ugraph
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
-
let undebrujin uri typesno tys t =
snd
(List.fold_right
let con_context =
List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
(* second phase: we fix only the constructors *)
+ let saved_menv = metasenv in
let metasenv,ugraph,tys =
List.fold_right
(fun (name,b,ty,cl) (metasenv,ugraph,res) ->
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
- metasenv,ugraph,(name,ty')::res
+ metasenv@saved_menv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in
metasenv,ugraph,(name,b,ty,cl')::res
;;
(* 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
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
+ let _,ty,metasenv,ugraph =
+ pack_coercions := false;
+ type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
+ pack_coercions := true;
+ let ctx' = Some (name,(C.Def (so,Some ty)))::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.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
+ if b then
+ let ugraph = CicUniv.oblivion_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 _ ->
+ 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_metasenv conjectures = conjectures (*
+
+ TASSI: this code war written when coercions were a toy,
+ now packing coercions involves unification thus
+ the metasenv may change, and this pack coercion
+ does not handle that.
+
+ let module C = Cic in
+ List.map
+ (fun (i, ctx, ty) ->
+ let 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 ctx ty))
+ ) conjectures
+ *)
;;
-let pack_coercion_obj obj =
+let pack_coercion_obj obj = obj (*
+
+ TASSI: this code war written when coercions were a toy,
+ now packing coercions involves unification thus
+ the metasenv may change, and this pack coercion
+ does not handle that.
+
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)
+ | 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
- in
- ((i,ctx,pack_coercion conjectures ty)))
- conjectures
- in
- let body = pack_coercion conjectures body in
- let ty = pack_coercion conjectures ty in
+ let conjectures = pack_coercion_metasenv 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 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
in
- C.InductiveDefinition (indtys, params, leftno, attrs)
+ C.InductiveDefinition (indtys, params, leftno, attrs) *)
;;
let typecheck ~localization_tbl metasenv uri obj =
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
+
+let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
+(* vim:set foldmethod=marker: *)
projects / helm.git / blobdiff