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
| _ -> dummyres)
| _ -> dummyres
-let more_args_than_expected
- localization_tbl metasenv subst he context hetype' tlbody_and_type exn
+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 (List.length tlbody_and_type) ^
- " arguments that are more than expected")
+ " (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
enrich localization_tbl he ~f:(fun _-> msg) exn
;;
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
-(*
- let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last t ugraph
- in
- try
- let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph coerced
- coercion_tgt
- in
- Some (newt, tty, subst, metasenv, ugraph)
- with
- | RefineFailure _ | Uncertain _ -> None
- in
-*)
let (t',_,_,_,_) as res =
match t with
(* function *)
(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)
| 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.");
+(*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 ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
in
tlbody_and_type,subst,metasenv,ugraph
- and eat_prods
+ and eat_prods
allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
=
(* given he:hety, gives beack all (c he) such that (c e):?->? *)
- let fix_arity exn metasenv context subst he hetype ugraph =
+ 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.NoCoercion -> []
| CoercGraph.NotMetaClosed
- | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotHandled _ ->
+ raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
| CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
HExtlib.filter_map
fo_unif_subst subst context metasenv last he ugraph in
debug_print (lazy ("New head: "^ pp coerc));
try
- let t,tty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context coerc ugraph in
- (*{{{*)debug_print (lazy (" refined: "^ pp t));
- debug_print (lazy (" has type: "^ pp tty));(*}}}*)
- Some (t,tty,subst,metasenv,ugraph)
+ 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 _)
"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 exn = RefineFailure (lazy ("more args than expected")) in
let possible_fixes =
- fix_arity exn metasenv context subst he hetype ugraph in
+ fix_arity (List.length args) metasenv context subst he hetype
+ ugraph in
match
HExtlib.list_findopt
(fun (he,hetype,subst,metasenv,ugraph) ->
try
Some (eat_prods_and_args
metasenv subst context he hetype ugraph [] args)
- with RefineFailure _ | Uncertain _ -> None)
+ with
+ | RefineFailure _ | Uncertain _
+ | HExtlib.Localized (_,RefineFailure _)
+ | HExtlib.Localized (_,Uncertain _) -> None)
possible_fixes
with
| Some x -> x
| None ->
- more_args_than_expected localization_tbl metasenv
- subst he context hetype args_bo_and_ty exn
+ raise
+ (MoreArgsThanExpected
+ (List.length args, RefineFailure (lazy "")))
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 =
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
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
| 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"));
+ debug_print (lazy (string_of_int (List.length candidates) ^
+ " candidates found"));
let uncertain = ref false in
let selected =
let posibilities =
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 =
CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
- 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
- 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
+ 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
- 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 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
- bo
- | Cic.Lambda (name, src, tgt),_ ->
- Cic.Lambda (name, src,
+ (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
+ 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 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
+ 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 =
+ | _ -> 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
+ 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
+ ~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
- debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context
- ~metasenv subst coerced context));
- (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
+ ~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
try
coerce_to_something_aux t infty expty subst metasenv context ugraph
enrich localization_tbl ~f t exn
and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
- match CicReduction.whd ~subst:subst context infty with
+ 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 _ =
merge_coercions ctx t
;;
-let pack_coercion_metasenv conjectures =
+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) ->
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) ->
(name, ind, arity, cl))
indtys
in
- C.InductiveDefinition (indtys, params, leftno, attrs)
+ C.InductiveDefinition (indtys, params, leftno, attrs) *)
;;