(* $Id$ *)
-(*
-open Printf
-
-exception RefineFailure of string Lazy.t;;
-exception Uncertain of string Lazy.t;;
+exception RefineFailure of (Stdpp.location * string) Lazy.t;;
+exception Uncertain of (Stdpp.location * 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;;
+module C = NCic
+module Ref = NReference
-let insert_coercions = ref true
-let pack_coercions = ref true
+let indent = ref "";;
+let inside c = indent := !indent ^ String.make 1 c;;
+let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-let debug = false;;
-let debug_print =
- if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
+let pp s =
+ prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+;;
-let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
+let pp _ = ();;
-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 wrap_exc msg = function
+ | NCicUnification.Uncertain _ -> Uncertain msg
+ | NCicUnification.UnificationFailure _ -> RefineFailure msg
+ | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
+ | e -> raise e
;;
-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"
-
-let fo_unif_subst subst context metasenv t1 t2 ugraph =
- try
-let foo () =
- CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
-in profiler.HExtlib.profile foo ()
- with
- (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
- | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
-;;
-
-let enrich localization_tbl t ?(f = fun msg -> msg) exn =
- let exn' =
- match exn with
- RefineFailure msg -> RefineFailure (f msg)
- | Uncertain msg -> Uncertain (f msg)
- | 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
- with Not_found ->
- HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
- raise exn'
- in
- raise (HExtlib.Localized (loc,exn'))
-
-let relocalize localization_tbl oldt newt =
- try
- let infos = Cic.CicHash.find localization_tbl oldt in
- Cic.CicHash.remove localization_tbl oldt;
- Cic.CicHash.add localization_tbl newt infos;
- with
- Not_found -> ()
-;;
-
-let rec split l n =
- match (l,n) with
- (l,0) -> ([], l)
- | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
- | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
-;;
-
-let exp_impl metasenv subst context =
- function
- | Some `Type ->
- let (metasenv', idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
- | Some `Closed ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
- | None ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+let exp_implicit metasenv context expty =
+ let foo x = match expty with Some t -> `WithType t | None -> x in
+ function
+ | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
+ | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
+ | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
| _ -> assert false
;;
-let is_a_double_coercion t =
- let rec subst_nth n x l =
- match n,l with
- | _, [] -> []
- | 0, _::tl -> x :: tl
- | n, hd::tl -> hd :: subst_nth (n-1) x tl
- in
- let imp = Cic.Implicit None in
- let dummyres = false,imp, imp,imp,imp in
- match t with
- | Cic.Appl l1 ->
- (match CoercGraph.coerced_arg l1 with
- | Some (Cic.Appl l2, pos1) ->
- (match CoercGraph.coerced_arg l2 with
- | Some (x, pos2) ->
- true, List.hd l1, List.hd l2, x,
- Cic.Appl (subst_nth (pos1 + 1)
- (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
- | _ -> dummyres)
- | _ -> dummyres)
- | _ -> dummyres
-;;
-
-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
- 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'
+let check_allowed_sort_elimination rdb localise r orig =
+ let mkapp he arg =
+ match he with
+ | C.Appl l -> C.Appl (l @ [arg])
+ | t -> C.Appl [t;arg] in
+ (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
+ let rec aux metasenv subst context ind arity1 arity2 =
+ (*D*)inside 'S'; try let rc =
+ let arity1 = NCicReduction.whd ~subst context arity1 in
+ pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " elimsto " ^
+ NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
+ NCicPp.ppmetasenv ~subst metasenv));
+ match arity1 with
+ | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
+ let metasenv, _, meta, _ =
+ NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type
in
- metasenv,Cic.Meta (idx, irl)
- | (_,argty)::tl ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
+ let metasenv, subst =
+ try NCicUnification.unify rdb metasenv subst context
+ arity2 (C.Prod (name, so1, meta))
+ with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
+ "expected %s, found %s" (* XXX localizzare meglio *)
+ (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta)))
+ (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
+ aux metasenv subst ((name, C.Decl so1)::context)
+ (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
+ | C.Sort _ (* , t ==?== C.Prod _ *) ->
+ let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
+ let metasenv, subst =
+ try NCicUnification.unify rdb metasenv subst context
+ arity2 (C.Prod ("_", ind, meta))
+ with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
+ "expected %s, found %s" (* XXX localizzare meglio *)
+ (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta)))
+ (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
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 =
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
- in
- 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
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.Constant (_,_,ty,_,_) -> ty,u
- | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
-
-and type_of_variable uri ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.Variable (_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
-
-and type_of_mutual_inductive_defs uri i ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
-
-and type_of_mutual_inductive_constr uri i j ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
+ (try NCicTypeChecker.check_allowed_sort_elimination
+ ~metasenv ~subst r context ind arity1 arity2;
+ metasenv, subst
+ with exc -> raise (wrap_exc (lazy (localise orig,
+ "Sort elimination not allowed ")) exc))
+ | _ -> assert false
+ (*D*)in outside(); rc with exc -> outside (); raise exc
in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,_,cl) = List.nth dl i in
- let (_,ty) = List.nth cl (j-1) in
- ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
-
-
-(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-
-(* the check_branch function checks if a branch of a case is refinable.
- It returns a pair (outype_instance,args), a subst and a metasenv.
- outype_instance is the expected result of applying the case outtype
- to args.
- The problem is that outype is in general unknown, and we should
- try to synthesize it from the above information, that is in general
- a second order unification problem. *)
-
-and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
- let module C = Cic in
- let module R = CicReduction in
- match R.whd ~subst context expectedtype with
- C.MutInd (_,_,_) ->
- (n,context,actualtype, [term]), subst, metasenv, ugraph
- | C.Appl (C.MutInd (_,_,_)::tl) ->
- let (_,arguments) = split tl left_args_no in
- (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
- | C.Prod (_,so,de) ->
- (* we expect that the actual type of the branch has the due
- number of Prod *)
- (match R.whd ~subst context actualtype with
- C.Prod (name',so',de') ->
- let subst, metasenv, ugraph1 =
- fo_unif_subst subst context metasenv so so' ugraph in
- let term' =
- (match CicSubstitution.lift 1 term with
- C.Appl l -> C.Appl (l@[C.Rel 1])
- | t -> C.Appl [t ; C.Rel 1]) in
- (* we should also check that the name variable is anonymous in
- the actual type de' ?? *)
- check_branch (n+1)
- ((Some (name',(C.Decl so)))::context)
- metasenv subst left_args_no de' term' de ugraph1
- | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
- | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
+ aux
+;;
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
- ugraph
+let rec typeof rdb
+ ?(localise=fun _ -> Stdpp.dummy_loc)
+ metasenv subst context term expty
=
- let rec type_of_aux subst metasenv context t ugraph =
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
- let (t',_,_,_,_) as res =
- match t with
- (* function *)
- C.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Decl ty) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,ty)) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | None ->
- enrich localization_tbl t
- (RefineFailure (lazy "Rel to hidden hypothesis"))
- with
- Failure _ ->
- enrich localization_tbl t
- (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 context exp_named_subst ugraph
- in
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let ty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
- | C.Meta (n,l) ->
- (try
- let (canonical_context, term,ty) =
- CicUtil.lookup_subst n subst
- in
- let l',subst',metasenv',ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- (* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv', ugraph1
- (* type_of_aux subst metasenv
- context (CicSubstitution.subst_meta l term) *)
- with CicUtil.Subst_not_found _ ->
- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let l',subst',metasenv', ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv',ugraph1)
- | C.Sort (C.Type tno) ->
- let tno' = CicUniv.fresh() in
- (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 (C.CProp tno) ->
- let tno' = CicUniv.fresh() in
- (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 (C.Prop|C.Set) ->
- t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
- | C.Implicit infos ->
- let metasenv',t' = exp_impl metasenv subst context infos in
- type_of_aux subst metasenv' context t' ugraph
- | C.Cast (te,ty) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- let te',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' context te ugraph1
- in
- 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 localization_tbl
- s' sort1 subst' context metasenv' ugraph1
- in
- let context_for_t = ((Some (name,(C.Decl s')))::context) in
- let t',sort2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- let t',sort2,subst'',metasenv'',ugraph2 =
- coerce_to_sort localization_tbl
- t' sort2 subst'' context_for_t metasenv'' ugraph2
- in
- let sop,subst''',metasenv''',ugraph3 =
- 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
- let s',sort1,subst',metasenv',ugraph1 =
- 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 =
- type_of_aux subst' metasenv' context_for_t t ugraph1
- in
- C.Lambda (n,s',t'),C.Prod (n,s',type2),
- subst'',metasenv'',ugraph2
- | C.LetIn (n,s,ty,t) ->
- (* only to check if s is well-typed *)
- let s',ty',subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
- let ty,_,subst',metasenv',ugraph1 =
- type_of_aux subst' metasenv' context ty ugraph1 in
- let subst',metasenv',ugraph1 =
- try
- fo_unif_subst subst' context metasenv'
- ty ty' ugraph1
- with
- exn ->
- enrich localization_tbl s' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
- context))
- in
- let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
-
- let t',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- (* One-step LetIn reduction.
- * Even faster than the previous solution.
- * Moreover the inferred type is closer to the expected one.
- *)
- C.LetIn (n,s',ty,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 =
- typeof_list subst' metasenv' context ugraph1 tl
- in
- let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
- eat_prods true subst'' metasenv'' context
- he' hetype tlbody_and_type ugraph2
- in
- 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 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph in
- let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutInd (uri,i,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri in
- C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 =
- type_of_mutual_inductive_constr uri i j ugraph1
- in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
- metasenv',ugraph2
- | C.MutCase (uri, i, outtype, term, pl) ->
- (* first, get the inductive type (and noparams)
- * in the environment *)
- let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
- let _ = CicTypeChecker.typecheck uri in
- let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
- match obj with
- C.InductiveDefinition (l,expl_params,parsno,_) ->
- List.nth l i , expl_params, parsno, u
- | _ ->
- enrich localization_tbl t
- (RefineFailure
- (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)
- | _ -> 0
- in
- let no_args = count_prod arity in
- (* now, create a "generic" MutInd *)
- let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
- in
- let metasenv,right_args =
- let no_right_params = no_args - no_left_params in
- if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas
- metasenv subst context no_right_params
- in
- let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv subst context expl_params in
- let expected_type =
- if no_args = 0 then
- C.MutInd (uri,i,exp_named_subst)
- else
- C.Appl
- (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
- in
- (* check consistency with the actual type of term *)
- let term',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context term ugraph in
- let expected_type',_, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context expected_type ugraph1
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv,ugraph3 =
- try
- fo_unif_subst subst context metasenv
- expected_type' actual_type ugraph2
- with
- exn ->
- enrich localization_tbl term' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst term'
- 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))
- in
- let rec instantiate_prod t =
- function
- [] -> t
- | he::tl ->
- match CicReduction.whd ~subst context t with
- C.Prod (_,_,t') ->
- instantiate_prod (CicSubstitution.subst he t') tl
- | _ -> assert false
- in
- let arity_instantiated_with_left_args =
- instantiate_prod arity left_args in
- (* TODO: check if the sort elimination
- * is allowed: [(I q1 ... qr)|B] *)
- let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- 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))
- else
- (C.Appl
- (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
- in
- let p',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context p ugraph
- in
- let constructor',expected_type, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context constructor ugraph1
- in
- let outtypeinstance,subst,metasenv,ugraph3 =
- 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 ("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
- (p'::pl,j-1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- pl ([],List.length pl,[],subst,metasenv,ugraph3)
- in
-
- (* we are left to check that the outype matches his instances.
- The easy case is when the outype is specified, that amount
- to a trivial check. Otherwise, we should guess a type from
- its instances
- *)
-
- let outtype,outtypety, subst, metasenv,ugraph4 =
- type_of_aux subst metasenv context outtype ugraph4 in
- (match outtype with
- | C.Meta (n,l) ->
- (let candidate,ugraph5,metasenv,subst =
- let exp_name_subst, metasenv =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
- in
- let uris = CicUtil.params_of_obj o in
- List.fold_right (
- fun uri (acc,metasenv) ->
- let metasenv',new_meta =
- CicMkImplicit.mk_implicit metasenv subst context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- context
- in
- (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
- ) uris ([],metasenv)
- in
- let ty =
- match left_args,right_args with
- [],[] -> Cic.MutInd(uri, i, exp_name_subst)
- | _,_ ->
- let rec mk_right_args =
- function
- 0 -> []
- | n -> (Cic.Rel n)::(mk_right_args (n - 1))
- in
- let right_args_no = List.length right_args in
- let lifted_left_args =
- List.map (CicSubstitution.lift right_args_no) left_args
- in
- Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
- (lifted_left_args @ mk_right_args right_args_no))
- in
- let fresh_name =
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- context Cic.Anonymous ~typ:ty
- in
- match outtypeinstances with
- | [] ->
- let extended_context =
- let rec add_right_args =
- function
- Cic.Prod (name,ty,t) ->
- Some (name,Cic.Decl ty)::(add_right_args t)
- | _ -> []
- in
- (Some (fresh_name,Cic.Decl ty))::
- (List.rev
- (add_right_args arity_instantiated_with_left_args))@
- context
- in
- let metasenv,new_meta =
- CicMkImplicit.mk_implicit metasenv subst extended_context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- extended_context
- in
- let rec add_lambdas b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas b t))
- | _ -> Cic.Lambda (fresh_name, ty, b)
- in
- let candidate =
- add_lambdas (Cic.Meta (new_meta,irl))
- arity_instantiated_with_left_args
- in
- (Some candidate),ugraph4,metasenv,subst
- | (constructor_args_no,_,instance,_)::tl ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let candidate,ugraph,metasenv,subst =
- List.fold_left (
- fun (candidate_oty,ugraph,metasenv,subst)
- (constructor_args_no,_,instance,_) ->
- match candidate_oty with
- | None -> None,ugraph,metasenv,subst
- | Some ty ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv
- instance' ty ugraph
- in
- candidate_oty,ugraph,metasenv,subst
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | RefineFailure _ | Uncertain _ ->
- None,ugraph,metasenv,subst
- ) (Some instance',ugraph4,metasenv,subst) tl
- in
- match candidate with
- | None -> None, ugraph,metasenv,subst
- | Some t ->
- let rec add_lambdas n b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
- | _ ->
- Cic.Lambda (fresh_name, ty,
- CicSubstitution.lift (n + 1) t)
- in
- Some
- (add_lambdas 0 t arity_instantiated_with_left_args),
- ugraph,metasenv,subst
- with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- None,ugraph4,metasenv,subst
- in
- match candidate with
- | 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
- (CicMetaSubst.apply_subst subst
- (Cic.Appl (outtype::right_args@[term']))),
- subst,metasenv,ugraph)
- | _ -> (* easy case *)
- let tlbody_and_type,subst,metasenv,ugraph4 =
- typeof_list subst metasenv context ugraph4 (right_args @ [term'])
- in
- let _,_,_,subst,metasenv,ugraph4 =
- eat_prods false subst metasenv context
- outtype outtypety tlbody_and_type ugraph4
- in
- let _,_, subst, metasenv,ugraph5 =
- type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
+ let force_ty skip_lambda metasenv subst context orig t infty expty =
+ (*D*)inside 'F'; try let rc =
+ match expty with
+ | Some expty ->
+ (match t with
+ | C.Implicit _ -> assert false
+ | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
+ | _ ->
+ pp (lazy (
+ (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
+ try
+ let metasenv, subst =
+ NCicUnification.unify rdb metasenv subst context infty expty
in
- let (subst,metasenv,ugraph6) =
- List.fold_left2
- (fun (subst,metasenv,ugraph)
- p (constructor_args_no,context,instance,args)
- ->
- let instance' =
- let appl =
- let outtype' =
- CicSubstitution.lift constructor_args_no outtype
- in
- C.Appl (outtype'::args)
- in
- CicReduction.head_beta_reduce ~delta:false
- ~upto:(List.length args) appl
- in
- try
- fo_unif_subst subst context metasenv instance instance'
- ugraph
- with
- exn ->
- enrich localization_tbl p exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~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
+ metasenv, subst, t, expty
+ with exc ->
+ try_coercions rdb ~localise
+ metasenv subst context t orig infty expty true exc)
+ | None -> metasenv, subst, t, infty
+ (*D*)in outside(); rc with exc -> outside (); raise exc
+ in
+ let rec typeof_aux metasenv subst context expty =
+ fun t as orig ->
+ (*D*)inside 'R'; try let rc =
+ pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
+ pp (lazy (if expty = None then "NONE" else "SOME"));
+ if (List.exists (fun (i,_) -> i=29) subst) then
+ pp (lazy (NCicPp.ppsubst ~metasenv subst));
+ let metasenv, subst, t, infty =
+ match t with
+ | C.Rel n ->
+ let infty =
+ (try
+ match List.nth context (n - 1) with
+ | (_,C.Decl ty) -> NCicSubstitution.lift n ty
+ | (_,C.Def (_,ty)) -> NCicSubstitution.lift n ty
+ with Failure _ ->
+ raise (RefineFailure (lazy (localise t,"unbound variable"))))
+ in
+ metasenv, subst, t, infty
+ | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
+ | C.Sort (C.Type _) ->
+ raise (AssertFailure (lazy ("Cannot type an inferred type: "^
+ NCicPp.ppterm ~subst ~metasenv ~context t)))
+ | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
+ | C.Implicit infos ->
+ let metasenv,_,t,ty = exp_implicit metasenv context expty infos in
+ metasenv, subst, t, ty
+ | C.Meta (n,l) as t ->
+ let ty =
+ try
+ let _,_,_,ty = NCicUtils.lookup_subst n subst in ty
+ with NCicUtils.Subst_not_found _ -> try
+ let _,_,ty = NCicUtils.lookup_meta n metasenv in
+ match ty with C.Implicit _ ->
+ prerr_endline (string_of_int n);
+ prerr_endline (NCicPp.ppmetasenv ~subst metasenv);
+ prerr_endline (NCicPp.ppsubst ~metasenv subst);
+ assert false | _ -> ty
+ with NCicUtils.Meta_not_found _ ->
+ raise (AssertFailure (lazy (Printf.sprintf
+ "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
+ in
+ metasenv, subst, t, NCicSubstitution.subst_meta l ty
+ | C.Const _ ->
+ metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
+ | C.Prod (name,(s as orig_s),(t as orig_t)) ->
+ let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+ let metasenv, subst, s, s1 =
+ force_to_sort rdb
+ metasenv subst context s orig_s localise s1 in
+ let context1 = (name,(C.Decl s))::context in
+ let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+ let metasenv, subst, t, s2 =
+ force_to_sort rdb
+ metasenv subst context1 t orig_t localise s2 in
+ let metasenv, subst, s, t, ty =
+ sort_of_prod localise metasenv subst
+ context orig_s orig_t (name,s) t (s1,s2)
+ in
+ metasenv, subst, NCic.Prod(name,s,t), ty
+ | C.Lambda (n,(s as orig_s),t) as orig ->
+ let exp_s, exp_ty_t, force_after =
+ match expty with
+ | None -> None, None, false
+ | Some expty ->
+ match NCicReduction.whd ~subst context expty with
+ | C.Prod (_,s,t) -> Some s, Some t, false
+ | _ -> None, None, true
+ in
+ let metasenv, subst, s, ty_s =
+ typeof_aux metasenv subst context None s in
+ let metasenv, subst, s, _ =
+ force_to_sort rdb
+ metasenv subst context s orig_s localise ty_s in
+ let (metasenv,subst), exp_ty_t =
+ match exp_s with
+ | Some exp_s ->
+ (try NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t
+ with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
+ "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
+ ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
+ exp_s))) exc))
+ | None -> (metasenv, subst), None
+ in
+ let context_for_t = (n,C.Decl s) :: context in
+ let metasenv, subst, t, ty_t =
+ typeof_aux metasenv subst context_for_t exp_ty_t t
+ in
+ if force_after then
+ force_ty false metasenv subst context orig
+ (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
+ else
+ metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
+ | C.LetIn (n,(ty as orig_ty),t,bo) ->
+ let metasenv, subst, ty, ty_ty =
+ typeof_aux metasenv subst context None ty in
+ let metasenv, subst, ty, _ =
+ force_to_sort rdb
+ metasenv subst context ty orig_ty localise ty_ty in
+ let metasenv, subst, t, _ =
+ typeof_aux metasenv subst context (Some ty) t in
+ let context1 = (n, C.Def (t,ty)) :: context in
+ let metasenv, subst, bo, bo_ty =
+ typeof_aux metasenv subst context1 None bo
+ in
+ let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
+ metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
+ | C.Appl ((he as orig_he)::(_::_ as args)) ->
+ let upto =
+ match orig_he with C.Meta _ -> List.length args | _ -> 0
+ in
+ let metasenv, subst, he, ty_he =
+ typeof_aux metasenv subst context None he in
+ let metasenv, subst, t, ty =
+ eat_prods rdb ~localise
+ metasenv subst context orig_he he ty_he args
+ in
+ let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
+ metasenv, subst, t, ty
+ | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
+ | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
+ outtype,(term as orig_term),pl) as orig ->
+ let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
+ let _, _, arity, cl = List.nth itl tyno in
+ let constructorsno = List.length cl in
+ let _, metasenv, args =
+ NCicMetaSubst.saturate metasenv subst context arity 0 in
+ let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
+ let metasenv, subst, term, _ =
+ typeof_aux metasenv subst context (Some ind) term in
+ let parameters, arguments = HExtlib.split_nth leftno args in
+ let outtype =
+ match outtype with
+ | C.Implicit _ as ot ->
+ let rec aux = function
+ | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
+ | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (C.Appl(outtype::right_args@[term']))),
- subst,metasenv,ugraph6)
- | C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (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 (CicSubstitution.lift len ty')))
- :: types, ugraph, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- 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
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("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
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.Fix (i,fl''),ty,subst,metasenv,ugraph2
- | C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (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 (CicSubstitution.lift len ty'))) ::
- types, ugraph1, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- 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
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("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
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
- in
- relocalize localization_tbl t t';
- res
-
- (* check_metasenv_consistency checks that the "canonical" context of a
- metavariable is consitent - up to relocation via the relocation list l -
- with the actual context *)
- and check_metasenv_consistency
- metano subst metasenv context canonical_context l ugraph
- =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let lifted_canonical_context =
- let rec aux i =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,ty)))::tl ->
- (Some
- (n,
- C.Def
- (S.subst_meta l (S.lift i t),
- S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
+ aux arguments
+ | _ -> outtype
+ in
+ let metasenv, subst, outtype, outsort =
+ typeof_aux metasenv subst context None outtype in
+
+ (* next lines are to do a subst-expansion of the outtype, so
+ that when it becomes a beta-abstraction, the beta-redex is
+ fired during substitution *)
+ (*CSC: this is instantiate! should we move it from tactics to the
+ refiner? I think so! *)
+ let metasenv,metanoouttype,newouttype,metaoutsort =
+ NCicMetaSubst.mk_meta metasenv context `Term in
+ let metasenv,subst =
+ NCicUnification.unify rdb metasenv subst context outsort metaoutsort in
+ let metasenv =
+ List.filter (function (j,_) -> j <> metanoouttype) metasenv in
+ let subst =
+ (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+ let outtype = newouttype in
+
+ (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+ let ind =
+ if parameters = [] then C.Const r
+ else C.Appl ((C.Const r)::parameters) in
+ let metasenv, subst, ind, ind_ty =
+ typeof_aux metasenv subst context None ind in
+ let metasenv, subst =
+ check_allowed_sort_elimination rdb localise r orig_term metasenv subst
+ context ind ind_ty outsort
in
- aux 1 canonical_context
- in
- try
- List.fold_left2
- (fun (l,subst,metasenv,ugraph) t ct ->
- match (t,ct) with
- _,None ->
- l @ [None],subst,metasenv,ugraph
- | Some t,Some (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly
- expensive reduction that can be easily avoided and
- that is quite frequent. However, this is better
- handled using levels to control reduction *)
- let optimized_t =
- match t with
- Cic.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with
- Failure _ -> t)
- | _ -> t
- in
- 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 optimized_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 optimized_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) ->
- let t',inferredty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context t ugraph
- in
- let subst'',metasenv'',ugraph2 =
- (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 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 ~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 ~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 =
- match tl with
- [] -> [],metasubst,metasenv,ugraph
- | (uri,t)::tl ->
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let typeofvar =
- CicSubstitution.subst_vars substs ty_uri in
- (* CSC: why was this code here? it is wrong
- (match CicEnvironment.get_cooked_obj ~trust:false uri with
- Cic.Variable (_,Some bo,_,_) ->
- raise
- (RefineFailure (lazy
- "A variable with a body can not be explicit substituted"))
- | Cic.Variable (_,None,_,_) -> ()
- | _ ->
- raise
- (RefineFailure (lazy
- ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
- ) ;
- *)
- let t',typeoft,metasubst',metasenv',ugraph2 =
- type_of_aux metasubst metasenv context t ugraph1 in
- let subst = uri,t' in
- let metasubst'',metasenv'',ugraph3 =
- try
- fo_unif_subst
- metasubst' context metasenv' typeoft typeofvar ugraph2
- with _ ->
- raise (RefineFailure (lazy
- ("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
- " not unifiable with " ^
- 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'' (substs@[subst]) tl ugraph3
- in
- ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
- in
- check_exp_named_subst_aux metasubst metasenv [] tl 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
- let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
- match (t1'', t2'') with
- | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
- (* different than Coq manual!!! *)
- C.Sort s2,subst,metasenv,ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (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.CProp t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (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.Sort _,C.Sort (C.CProp t1)) ->
- C.Sort (C.CProp 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
- * 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))))
- | _,_ ->
- 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 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
- =
- (* 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
- (* instead of a dummy functional type we may create the real product
- * using args_bo_and_ty, but since coercions lookup ignores the
- * actual ariety we opt for the simple solution *)
- let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
- match CoercGraph.look_for_coercion metasenv subst context hetype fty with
- | CoercGraph.NoCoercion -> []
- | 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
- try
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last he ugraph in
- debug_print (lazy ("New head: "^ pp coerc));
- 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
- | [] -> 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)
+ (* let's check if the type of branches are right *)
+ if List.length pl <> constructorsno then
+ raise (RefineFailure (lazy (localise orig,
+ "Wrong number of cases in a match")));
+(*
+ let metasenv, subst =
+ match expty with
+ | None -> metasenv, subst
+ | Some expty ->
+ NCicUnification.unify rdb metasenv subst context resty expty
+ in
+*)
+ let _, metasenv, subst, pl =
+ List.fold_right
+ (fun p (j, metasenv, subst, branches) ->
+ let cons =
+ let cons = Ref.mk_constructor j r in
+ if parameters = [] then C.Const cons
+ else C.Appl (C.Const cons::parameters)
in
- (*{{{*) 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
- (* 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
+ let metasenv, subst, cons, ty_cons =
+ typeof_aux metasenv subst context None cons in
+ let ty_branch =
+ NCicTypeChecker.type_of_branch
+ ~subst context leftno outtype cons ty_cons in
+ pp (lazy ("TYPEOFBRANCH: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ty_branch ));
+ let metasenv, subst, p, _ =
+ typeof_aux metasenv subst context (Some ty_branch) p in
+ j-1, metasenv, subst, p :: branches)
+ pl (List.length pl, metasenv, subst, [])
+ in
+ let resty = C.Appl (outtype::arguments@[term]) in
+ let resty = NCicReduction.head_beta_reduce ~subst resty in
+ metasenv, subst, C.Match (r, outtype, term, pl),resty
+ | C.Match _ -> assert false
in
- he,(List.map fst coerced_args),t,subst,metasenv,ugraph
+ pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+ NCicPp.ppterm ~metasenv ~subst ~context infty ));
+ force_ty true metasenv subst context orig t infty expty
+ (*D*)in outside(); rc with exc -> outside (); raise exc
+ in
+ typeof_aux metasenv subst context expty term
- 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
+and try_coercions rdb
+ ~localise
+ metasenv subst context t orig_t infty expty perform_unification exc
+=
+ (* we try with a coercion *)
+ let rec first exc = function
+ | [] ->
+ raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
+ "The term %s has type %s but is here used with type %s"
+ (NCicPp.ppterm ~metasenv ~subst ~context t)
+ (NCicPp.ppterm ~metasenv ~subst ~context infty)
+ (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
+ | (metasenv, newterm, newtype, meta)::tl ->
+ try
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
+ let metasenv, subst =
+ NCicUnification.unify rdb metasenv subst context meta t
+ in
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context newtype ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
+ let metasenv, subst =
+ if perform_unification then
+ NCicUnification.unify rdb metasenv subst context newtype expty
+ else metasenv, subst
+ in
+ metasenv, subst, newterm, newtype
+ with
+ | NCicUnification.UnificationFailure _ -> first exc tl
+ | NCicUnification.Uncertain _ as exc -> first exc tl
+ in
+ first exc
+ (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
+
+and force_to_sort rdb metasenv subst context t orig_t localise ty =
+ match NCicReduction.whd ~subst context ty with
+ | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty ->
+ metasenv, subst, t, ty
+ | C.Meta (_i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ???
+ metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *)
+ | C.Meta (i,(_,lc)) ->
+ let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
+ let metasenv, subst, newmeta =
+ if len > 0 then
+ NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
+ else metasenv, subst, i
+ in
+ metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
+ | C.Sort _ as ty -> metasenv, subst, t, ty
+ | ty ->
+ try_coercions rdb ~localise metasenv subst context
+ t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false
+ (Uncertain (lazy (localise orig_t,
+ "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
+ ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
+
+and sort_of_prod
+ localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)
+=
+ (* force to sort is done in the Prod case in typeof *)
+ match t1, t2 with
+ | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
+ | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
+ metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2))
+ | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
+ | C.Meta _, C.Sort _
+ | C.Meta _, C.Meta (_,(_,_))
+ | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2
+ | x, (C.Sort _ | C.Meta _) | _, x ->
+ let y, context, orig =
+ if x == t1 then s, context, orig_s
+ else t, ((name,C.Decl s)::context), orig_t
in
- match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
- "coerce_atom_to_something fails since no coercions found"))
- | CoercGraph.NotHandled when
- not (CicUtil.is_meta_closed infty) ||
- not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
- "coerce_atom_to_something fails since carriers have metas"))
- | 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
+ raise (RefineFailure (lazy (localise orig,Printf.sprintf
+ "%s is expected to be a type, but its type is %s that is not a sort"
+ (NCicPp.ppterm ~subst ~metasenv ~context y)
+ (NCicPp.ppterm ~subst ~metasenv ~context x))))
+
+and guess_name subst ctx ty =
+ let aux initial = "#" ^ String.make 1 initial in
+ match ty with
+ | C.Const (NReference.Ref (u,_))
+ | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
+ aux (String.sub (NUri.name_of_uri u) 0 1).[0]
+ | C.Prod _ -> aux 'f'
+ | C.Meta (n,lc) ->
+ (try
+ let _,_,t,_ = NCicUtils.lookup_subst n subst in
+ guess_name subst ctx (NCicSubstitution.subst_meta lc t)
+ with NCicUtils.Subst_not_found _ -> aux 'M')
+ | _ -> aux 'H'
+
+and eat_prods rdb
+ ~localise metasenv subst context orig_he he ty_he args
+=
+ (*D*)inside 'E'; try let rc =
+ let rec aux metasenv subst args_so_far he ty_he = function
+ | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he
+ | arg::tl ->
+ match NCicReduction.whd ~subst context ty_he with
+ | C.Prod (_,s,t) ->
+ let metasenv, subst, arg, _ =
+ typeof rdb ~localise
+ metasenv subst context arg (Some s) in
+ let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
+ aux metasenv subst (arg :: args_so_far) he t tl
+ | C.Meta _
+ | C.Appl (C.Meta _ :: _) as t ->
+ let metasenv, subst, arg, ty_arg =
+ typeof rdb ~localise
+ metasenv subst context arg None in
+ let name = guess_name subst context ty_arg in
+ let metasenv, _, meta, _ =
+ NCicMetaSubst.mk_meta metasenv
+ ((name,C.Decl ty_arg) :: context) `Type
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 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)
- when allow_coercions && !insert_coercions ->
- 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
- 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 _ | Cic.Meta _) as mty,_ -> [], mty
- | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
- snd (HExtlib.split_nth leftno args), mty
- | _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _ ->
- raise (AssertFailure(lazy "already ill-typed matched term"))
- 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 (*}}}*)
+ let flex_prod = C.Prod (name, ty_arg, meta) in
+ (* next line grants that ty_args is a type *)
+ let metasenv,subst, flex_prod, _ =
+ typeof rdb ~localise metasenv subst
+ context flex_prod None in
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
+ let metasenv, subst =
+ try NCicUnification.unify rdb metasenv subst context t flex_prod
+ with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
+ ("The term %s has an inferred type %s, but is applied to the" ^^
+ " argument %s of type %s")
+ (NCicPp.ppterm ~metasenv ~subst ~context he)
+ (NCicPp.ppterm ~metasenv ~subst ~context t)
+ (NCicPp.ppterm ~metasenv ~subst ~context arg)
+ (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
+ (* XXX coerce to funclass *)
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
- 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! *)
-
- let t',ty,subst',metasenv',ugraph1 =
- type_of_aux [] metasenv context t ugraph
- in
- let substituted_t = CicMetaSubst.apply_subst subst' t' in
- let substituted_ty = CicMetaSubst.apply_subst subst' ty in
- (* Andrea: ho rimesso qui l'applicazione della subst al
- metasenv dopo che ho droppato l'invariante che il metsaenv
- e' sempre istanziato *)
- let substituted_metasenv =
- CicMetaSubst.apply_subst_metasenv subst' metasenv' in
- (* metasenv' *)
- (* substituted_t,substituted_ty,substituted_metasenv *)
- (* ANDREA: spostare tutta questa robaccia da un altra parte *)
- let cleaned_t =
- if clean_dummy_dependent_types then
- FreshNamesGenerator.clean_dummy_dependent_types substituted_t
- else substituted_t in
- let cleaned_ty =
- if clean_dummy_dependent_types then
- FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
- else substituted_ty in
- let cleaned_metasenv =
- if clean_dummy_dependent_types then
- List.map
- (function (n,context,ty) ->
- let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
- let context' =
- List.map
- (function
- None -> None
- | Some (n, Cic.Decl t) ->
- Some (n,
- Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
- | Some (n, Cic.Def (bo,ty)) ->
- let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
- in
- Some (n, Cic.Def (bo',ty'))
- ) context
- in
- (n,context',ty')
- ) substituted_metasenv
- else
- substituted_metasenv
+ let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
+ aux metasenv subst (arg :: args_so_far) he meta tl
+ | C.Match (_,_,C.Meta _,_)
+ | C.Match (_,_,C.Appl (C.Meta _ :: _),_)
+ | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+ raise (Uncertain (lazy (localise orig_he, Printf.sprintf
+ ("The term %s is here applied to %d arguments but expects " ^^
+ "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+ (List.length args) (List.length args_so_far))))
+ | ty ->
+ let metasenv, subst, newhead, newheadty =
+ try_coercions rdb ~localise metasenv subst context
+ (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
+ (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
+ false
+ (RefineFailure (lazy (localise orig_he, Printf.sprintf
+ ("The term %s is here applied to %d arguments but expects " ^^
+ "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+ (List.length args) (List.length args_so_far))))
+ in
+ aux metasenv subst [] newhead newheadty (arg :: tl)
in
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
+ (* We need to reverse the order of the new created metas since they
+ are pushed on top of the metasenv in the wrong order *)
+ let highest_meta = NCicMetaSubst.maxmeta () in
+ let metasenv, subst, newhead, newheadty =
+ aux metasenv subst [] he ty_he args in
+ let metasenv_old,metasenv_new =
+ List.partition (fun (i,_) -> i <= highest_meta) metasenv
+ in
+ (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
+ (*D*)in outside(); rc with exc -> outside (); raise exc
;;
-let undebrujin uri typesno tys t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (* here the explicit_named_substituion is assumed to be *)
- (* of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tys (typesno - 1,t))
-
-let map_first_n n start f g l =
- let rec aux acc k l =
- if k < n then
- match l with
- | [] -> raise (Invalid_argument "map_first_n")
- | hd :: tl -> f hd k (aux acc (k+1) tl)
- else
- g acc l
- in
- aux start 0 l
-
-(*CSC: this is a very rough approximation; to be finished *)
-let are_all_occurrences_positive metasenv ugraph uri tys leftno =
- let subst,metasenv,ugraph,tys =
- List.fold_right
- (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
- let subst,metasenv,ugraph,cl =
- List.fold_right
- (fun (name,ty) (subst,metasenv,ugraph,acc) ->
- let rec aux ctx k subst = function
- | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
- let subst,metasenv,ugraph,tl =
- map_first_n leftno
- (subst,metasenv,ugraph,[])
- (fun t n (subst,metasenv,ugraph,acc) ->
- let subst,metasenv,ugraph =
- fo_unif_subst
- subst ctx metasenv t (Cic.Rel (k-n)) ugraph
- in
- subst,metasenv,ugraph,(t::acc))
- (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
- tl
- in
- subst,metasenv,ugraph,(Cic.Appl (hd::tl))
- | Cic.MutInd(uri',_,_) as t when uri = uri'->
- subst,metasenv,ugraph,t
- | Cic.Prod (name,s,t) ->
- let ctx = (Some (name,Cic.Decl s))::ctx in
- let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
- subst,metasenv,ugraph,Cic.Prod (name,s,t)
- | _ ->
- raise
- (RefineFailure
- (lazy "not well formed constructor type"))
- in
- let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
- subst,metasenv,ugraph,(name,ty) :: acc)
- cl (subst,metasenv,ugraph,[])
- in
- subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
- tys ([],metasenv,ugraph,[])
- in
- let substituted_tys =
- List.map
- (fun (name,ind,arity,cl) ->
- let cl =
- List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
- in
- name,ind,CicMetaSubst.apply_subst subst arity,cl)
- tys
- in
- metasenv,ugraph,substituted_tys
-
-let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.oblivion_ugraph in
- match obj with
- Cic.Constant (name,Some bo,ty,args,attrs) ->
- (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
- since type_of_aux' destroys localization information (which are
- preserved by type_of_aux *)
- let loc exn' =
- try
- Cic.CicHash.find localization_tbl bo
- with Not_found ->
- HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
- raise exn' in
- let bo',boty,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] bo ugraph in
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- let subst,metasenv,ugraph =
- try
- fo_unif_subst [] [] metasenv boty ty' ugraph
- with
- RefineFailure _
- | Uncertain _ as exn ->
- let msg =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
- " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
- " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
- in
- let exn' =
- match exn with
- RefineFailure _ -> RefineFailure msg
- | Uncertain _ -> Uncertain msg
- | _ -> assert false
- in
- raise (HExtlib.Localized (loc exn',exn'))
- in
- let bo' = CicMetaSubst.apply_subst subst bo' in
- let ty' = CicMetaSubst.apply_subst subst ty' in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
- | Cic.Constant (name,None,ty,args,attrs) ->
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph
- in
- Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
- | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
- assert (metasenv' = metasenv);
- (* Here we do not check the metasenv for correctness *)
- let bo',boty,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] bo ugraph in
- let ty',sort,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- begin
- match sort with
- Cic.Sort _
- (* instead of raising Uncertain, let's hope that the meta will become
- a sort *)
- | Cic.Meta _ -> ()
- | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
- end;
- let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
- let bo' = CicMetaSubst.apply_subst subst bo' in
- let ty' = CicMetaSubst.apply_subst subst ty' in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
- | Cic.Variable _ -> assert false (* not implemented *)
- | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
- (*CSC: this code is greately simplified and many many checks are missing *)
- (*CSC: e.g. the constructors are not required to build their own types, *)
- (*CSC: the arities are not required to have as type a sort, etc. *)
- let uri = match uri with Some uri -> uri | None -> assert false in
- let typesno = List.length tys in
- (* first phase: we fix only the types *)
- let metasenv,ugraph,tys =
- List.fold_right
- (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
- let ty',_,metasenv,ugraph =
- (* clean_dummy_dependent_types: false to avoid cleaning the names
- of the left products, that must be identical to those of the
- constructors; however, non-left products should probably be
- cleaned *)
- type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
- metasenv [] ty ugraph
- in
- metasenv,ugraph,(name,b,ty',cl)::res
- ) tys (metasenv,ugraph,[]) in
- 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 metasenv,ugraph,cl' =
- List.fold_right
- (fun (name,ty) (metasenv,ugraph,res) ->
- let ty =
- CicTypeChecker.debrujin_constructor
- ~cb:(relocalize localization_tbl) uri typesno [] ty in
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
- let ty' = undebrujin uri typesno tys ty' in
- metasenv@saved_menv,ugraph,(name,ty')::res
- ) cl (metasenv,ugraph,[])
- in
- metasenv,ugraph,(name,b,ty,cl')::res
- ) tys (metasenv,ugraph,[]) in
- (* third phase: we check the positivity condition *)
- let metasenv,ugraph,tys =
- are_all_occurrences_positive metasenv ugraph uri tys paramsno
- in
- Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+let rec first f l1 l2 =
+ match l1,l2 with
+ | x1::tl1, x2::tl2 ->
+ (try f x1 x2 with Not_found -> first f tl1 tl2)
+ | _ -> raise Not_found
;;
-(* sara' piu' veloce che raffinare da zero? mah.... *)
-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
- function
- | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
- | C.Meta (n,subst) ->
- let subst' =
- List.map
- (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
- in
- C.Meta (n,subst')
- | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
- | C.Prod (name,so,dest) ->
- let ctx' = (Some (name,C.Decl so))::ctx in
- C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.Lambda (name,so,dest) ->
- let ctx' = (Some (name,C.Decl so))::ctx in
- C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,ty,dest) ->
- let ctx' = Some (name,(C.Def (so,ty)))::ctx in
- C.LetIn
- (name, merge_coercions ctx so, merge_coercions ctx ty,
- merge_coercions ctx' dest)
- | 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)
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Const (uri, exp_named_subst)
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutInd (uri,tyno,exp_named_subst)
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutConstruct (uri,tyno,consno,exp_named_subst)
- | C.MutCase (uri,tyno,out,te,pl) ->
- let pl = List.map (merge_coercions ctx) pl in
- C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
- | C.Fix (fno, fl) ->
- let ctx' =
- List.fold_left
- (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
- ctx fl
- in
- let fl =
- List.map
- (fun (name,idx,ty,bo) ->
- (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
- fl
- in
- C.Fix (fno, fl)
- | C.CoFix (fno, fl) ->
- let ctx' =
- List.fold_left
- (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
- ctx fl
- in
- let fl =
- List.map
- (fun (name,ty,bo) ->
- (name, merge_coercions ctx ty, merge_coercions ctx' bo))
- fl
- in
- C.CoFix (fno, fl)
- in
- merge_coercions ctx t
+let rec find add dt t =
+ if dt == add then t
+ else
+ let dl, l =
+ match dt, t with
+ | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
+ | C.Appl dl,C.Appl l -> dl,l
+ | C.Lambda (_,ds,dt), C.Lambda (_,s,t)
+ | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
+ | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t]
+ | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
+ | _ -> raise Not_found
+ in
+ first (find add) dl l
;;
-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 relocalise old_localise dt t add =
+ old_localise
+ (try find add dt t with Not_found -> assert false)
;;
-let pack_coercion_obj obj = obj (*
+let undebruijnate inductive ref t rev_fl =
+ NCicSubstitution.psubst (fun x -> x)
+ (List.rev (HExtlib.list_mapi
+ (fun (_,_,rno,_,_,_) i ->
+ NCic.Const
+ (if inductive then NReference.mk_fix i rno ref
+ else NReference.mk_cofix i ref))
+ rev_fl))
+ t
+;;
- 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)
+let typeof_obj
+ rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
+=
+ let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *)
+ let metasenv, subst, ty, sort =
+ typeof rdb ~localise metasenv subst context ty None
+ in
+ let metasenv, subst, ty, sort =
+ force_to_sort rdb metasenv subst context ty orig_ty localise sort
+ in
+ metasenv, subst, ty, sort
+ in
+ match obj with
+ | C.Constant (relevance, name, bo, ty , attr) ->
+ let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+ let metasenv, subst, bo, ty, height =
+ match bo with
+ | Some bo ->
+ let metasenv, subst, bo, ty =
+ typeof rdb ~localise metasenv subst [] bo (Some ty) in
+ let height = (* XXX recalculate *) height in
+ metasenv, subst, Some bo, ty, height
+ | None -> metasenv, subst, None, ty, 0
+ in
+ uri, height, metasenv, subst,
+ C.Constant (relevance, name, bo, ty, attr)
+ | C.Fixpoint (inductive, fl, attr) ->
+ let len = List.length fl in
+ let types, metasenv, subst, rev_fl =
+ List.fold_left
+ (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
+ let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+ let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in
+ let localise = relocalise localise dbo bo in
+ (name,C.Decl ty)::types,
+ metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
+ ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
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)
+ let metasenv, subst, fl =
+ List.fold_left
+ (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
+ let metasenv, subst, dbo, ty =
+ typeof rdb ~localise metasenv subst types dbo (Some ty)
+ in
+ metasenv, subst, (relevance,name,k,ty,dbo)::fl)
+ (metasenv, subst, []) rev_fl
in
- let ty = pack_coercion [] [] ty in
- C.Variable (name, body, ty, params, attrs)
- | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
- 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 =
+ let height = (* XXX recalculate *) height in
+ let fl =
List.map
- (fun (name, ind, arity, cl) ->
- let arity = pack_coercion [] [] arity in
- let cl =
- List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
- in
- (name, ind, arity, cl))
- indtys
+ (fun (relevance,name,k,ty,dbo) ->
+ let bo =
+ undebruijnate inductive
+ (NReference.reference_of_spec uri
+ (if inductive then NReference.Fix (0,k,0)
+ else NReference.CoFix 0)) dbo rev_fl
+ in
+ relevance,name,k,ty,bo)
+ fl
in
- C.InductiveDefinition (indtys, params, leftno, attrs) *)
+ uri, height, metasenv, subst,
+ C.Fixpoint (inductive, fl, attr)
+ | C.Inductive (ind, leftno, itl, attr) ->
+ let len = List.length itl in
+ let metasenv,subst,rev_itl,tys =
+ List.fold_left
+ (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
+ let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+ metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
+ ) (metasenv,subst,[],[]) itl in
+ let metasenv,subst,itl,_ =
+ List.fold_left
+ (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
+ let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
+ let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
+ let metasenv,subst,cl =
+ List.fold_right
+ (fun (k_relev,n,te) (metasenv,subst,res) ->
+ let k_relev =
+ try snd (HExtlib.split_nth leftno k_relev)
+ with Failure _ -> k_relev in
+ let te = NCicTypeChecker.debruijn uri len [] ~subst te in
+ let metasenv, subst, te, _ = check_type metasenv subst tys te in
+ let context,te = NCicReduction.split_prods ~subst tys leftno te in
+ let _,chopped_context_rev =
+ HExtlib.split_nth (List.length tys) (List.rev context) in
+ let sx_context_te_rev,_ =
+ HExtlib.split_nth leftno chopped_context_rev in
+ let metasenv,subst,_ =
+ try
+ List.fold_left2
+ (fun (metasenv,subst,context) item1 item2 ->
+ let (metasenv,subst),convertible =
+ try
+ match item1,item2 with
+ (n1,C.Decl ty1),(n2,C.Decl ty2) ->
+ if n1 = n2 then
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
+ subst context ty1 ty2,true
+ else
+ (metasenv,subst),false
+ | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
+ if n1 = n2 then
+ let metasenv,subst =
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
+ subst context ty1 ty2
+ in
+ NCicUnification.unify rdb ~test_eq_only:true metasenv
+ subst context bo1 bo2,true
+ else
+ (metasenv,subst),false
+ | _,_ -> (metasenv,subst),false
+ with
+ | NCicUnification.Uncertain _
+ | NCicUnification.UnificationFailure _ ->
+ (metasenv,subst),false
+ in
+ let term2 =
+ match item2 with
+ _,C.Decl t -> t
+ | _,C.Def (b,_) -> b in
+ if not convertible then
+ raise (RefineFailure (lazy (localise term2,
+ ("Mismatch between the left parameters of the constructor " ^
+ "and those of its inductive type"))))
+ else
+ metasenv,subst,item1::context
+ ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+ with Invalid_argument "List.fold_left2" -> assert false in
+ let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
+ (match
+ NCicReduction.whd ~subst context con_sort,
+ NCicReduction.whd ~subst [] ty_sort
+ with
+ (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
+ if not (NCicEnvironment.universe_leq u1 u2) then
+ raise
+ (RefineFailure
+ (lazy(localise te, "The type " ^
+ NCicPp.ppterm ~metasenv ~subst ~context s1 ^
+ " of the constructor is not included in the inductive"^
+ " type sort " ^
+ NCicPp.ppterm ~metasenv ~subst ~context s2)))
+ | C.Sort _, C.Sort C.Prop
+ | C.Sort _, C.Sort C.Type _ -> ()
+ | _, _ ->
+ raise
+ (RefineFailure
+ (lazy (localise te,
+ "Wrong constructor or inductive arity shape"))));
+ (* let's check also the positivity conditions *)
+ if
+ not
+ (NCicTypeChecker.are_all_occurrences_positive
+ ~subst context uri leftno (i+leftno) leftno (len+leftno) te)
+ then
+ raise
+ (RefineFailure
+ (lazy (localise te,
+ "Non positive occurence in " ^ NUri.string_of_uri uri)))
+ else
+ let relsno = List.length itl + leftno in
+ let te =
+ NCicSubstitution.psubst
+ (fun i ->
+ if i <= leftno then
+ NCic.Rel i
+ else
+ NCic.Const (NReference.reference_of_spec uri
+ (NReference.Ind (ind,relsno - i,leftno))))
+ (HExtlib.list_seq 1 (relsno+1))
+ te in
+ let te =
+ List.fold_right
+ (fun (name,decl) te ->
+ match decl with
+ NCic.Decl ty -> NCic.Prod (name,ty,te)
+ | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te)
+ ) sx_context_te_rev te
+ in
+ metasenv,subst,(k_relev,n,te)::res
+ ) cl (metasenv,subst,[])
+ in
+ metasenv,subst,(it_relev,n,ty,cl)::res,i+1
+ ) (metasenv,subst,[],1) rev_itl
+ in
+ uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
;;
-
-(* DEBUGGING ONLY
-let type_of_aux' metasenv context term =
- try
- let (t,ty,m) =
- type_of_aux' metasenv context term in
- debug_print (lazy
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
- debug_print (lazy
- ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
- (t,ty,m)
- with
- | RefineFailure msg as e ->
- debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
- raise e
- | Uncertain msg as e ->
- debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
- raise e
-;; *)
-
-let profiler2 = HExtlib.profile "CicRefine"
-
-let type_of_aux' ?localization_tbl metasenv context term ugraph =
- profiler2.HExtlib.profile
- (type_of_aux' ?localization_tbl metasenv context term) ugraph
-
-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