X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f216b3c5c03429324561f49e8a89e770246063e1;hpb=990de61eb594f86798348c1ff53a8caed2e0e6f2;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index f216b3c5c..d3a297d43 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,25 +25,159 @@ open Printf -exception RefineFailure of string;; -exception Uncertain of string;; -exception AssertFailure of string;; +exception RefineFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; let debug_print = fun _ -> () +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 f = + function + RefineFailure msg -> raise (RefineFailure (f msg)) + | Uncertain msg -> raise (Uncertain (f msg)) + | _ -> assert false + 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 "split: list too short") + | (_,_) -> raise (AssertFailure (lazy "split: list too short")) +;; + +let exp_impl metasenv subst context term = + let rec aux metasenv context = function + | (Cic.Rel _) as t -> metasenv, t + | (Cic.Sort _) as t -> metasenv, t + | Cic.Const (uri, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.Const (uri, subst') + | Cic.Var (uri, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.Var (uri, subst') + | Cic.MutInd (uri, i, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.MutInd (uri, i, subst') + | Cic.MutConstruct (uri, i, j, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.MutConstruct (uri, i, j, subst') + | Cic.Meta (n,l) -> + let metasenv', l' = do_local_context metasenv context l in + metasenv', Cic.Meta (n, l') + | Cic.Implicit (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) + | Cic.Implicit (Some `Closed) -> + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) + | Cic.Implicit 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) + | Cic.Implicit _ -> assert false + | Cic.Cast (te, ty) -> + let metasenv', ty' = aux metasenv context ty in + let metasenv'', te' = aux metasenv' context te in + metasenv'', Cic.Cast (te', ty') + | Cic.Prod (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.Prod (name, s', t) + | Cic.Lambda (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.Lambda (name, s', t) + | Cic.LetIn (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.LetIn (name, s', t) + | Cic.Appl l when List.length l > 1 -> + let metasenv', l' = + List.fold_right + (fun term (metasenv, terms) -> + let new_metasenv, term = aux metasenv context term in + new_metasenv, term :: terms) + l (metasenv, []) + in + metasenv', Cic.Appl l' + | Cic.Appl _ -> assert false + | Cic.MutCase (uri, i, outtype, term, patterns) -> + let metasenv', l' = + List.fold_right + (fun term (metasenv, terms) -> + let new_metasenv, term = aux metasenv context term in + new_metasenv, term :: terms) + (outtype :: term :: patterns) (metasenv, []) + in + let outtype', term', patterns' = + match l' with + | outtype' :: term' :: patterns' -> outtype', term', patterns' + | _ -> assert false + in + metasenv', Cic.MutCase (uri, i, outtype', term', patterns') + | Cic.Fix (i, funs) -> + let metasenv', types = + List.fold_right + (fun (name, _, typ, _) (metasenv, types) -> + let new_metasenv, new_type = aux metasenv context typ in + (new_metasenv, (name, new_type) :: types)) + funs (metasenv, []) + in + let rec combine = function + | ((name, index, _, body) :: funs_tl), + ((_, typ) :: typ_tl) -> + (name, index, typ, body) :: combine (funs_tl, typ_tl) + | [], [] -> [] + | _ -> assert false + in + let funs' = combine (funs, types) in + metasenv', Cic.Fix (i, funs') + | Cic.CoFix (i, funs) -> + let metasenv', types = + List.fold_right + (fun (name, typ, _) (metasenv, types) -> + let new_metasenv, new_type = aux metasenv context typ in + (new_metasenv, (name, new_type) :: types)) + funs (metasenv, []) + in + let rec combine = function + | ((name, _, body) :: funs_tl), + ((_, typ) :: typ_tl) -> + (name, typ, body) :: combine (funs_tl, typ_tl) + | [], [] -> [] + | _ -> assert false + in + let funs' = combine (funs, types) in + metasenv', Cic.CoFix (i, funs') + and do_subst metasenv context subst = + List.fold_right + (fun (uri, term) (metasenv, substs) -> + let metasenv', term' = aux metasenv context term in + (metasenv', (uri, term') :: substs)) + subst (metasenv, []) + and do_local_context metasenv context local_context = + List.fold_right + (fun term (metasenv, local_context) -> + let metasenv', term' = + match term with + | None -> metasenv, None + | Some term -> + let metasenv', term' = aux metasenv context term in + metasenv', Some term' + in + metasenv', term' :: local_context) + local_context (metasenv, []) + in + aux metasenv context term ;; let rec type_of_constant uri ugraph = @@ -61,7 +195,7 @@ let rec type_of_constant uri ugraph = | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise - (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) + (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) and type_of_variable uri ugraph = let module C = Cic in @@ -78,7 +212,7 @@ and type_of_variable uri ugraph = | _ -> raise (RefineFailure - ("Unknown variable definition " ^ UriManager.string_of_uri uri)) + (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs uri i ugraph = let module C = Cic in @@ -93,11 +227,11 @@ and type_of_mutual_inductive_defs uri i ugraph = match obj with C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in - arity,u + arity,u | _ -> raise (RefineFailure - ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) + (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 @@ -110,14 +244,15 @@ and type_of_mutual_inductive_constr uri i j ugraph = with Not_found -> assert false in match obj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,u - | _ -> - raise - (RefineFailure - ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) + | _ -> + 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 *) @@ -135,257 +270,321 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* let module R = CicMetaSubst in *) let module R = CicReduction in match R.whd ~subst context expectedtype with - C.MutInd (_,_,_) -> - (n,context,actualtype, [term]), subst, metasenv, ugraph + 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 + let (_,arguments) = split tl left_args_no in + (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph | C.Prod (name,so,de) -> - (* we expect that the actual type of the branch has the due + (* we expect that the actual type of the branch has the due number of Prod *) - (match R.whd ~subst context actualtype with + (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]) + 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) + (* 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 "Wrong number of arguments")) - | _ -> raise (AssertFailure "Prod or MutInd expected") + | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) + | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) and type_of_aux' metasenv context t ugraph = + let metasenv, t = exp_impl metasenv [] context t in 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 + (* this stops on binders, so we have to call it every time *) match t with - (* function *) - C.Rel n -> - (try + (* function *) + C.Rel n -> + (try match List.nth context (n - 1) with - Some (_,C.Decl ty) -> + Some (_,C.Decl ty) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (_,Some ty)) -> + | Some (_,C.Def (_,Some ty)) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (bo,None)) -> + | Some (_,C.Def (bo,None)) -> let ty,ugraph = (* if it is in the context it must be already well-typed*) - CicTypeChecker.type_of_aux' ~subst metasenv context + CicTypeChecker.type_of_aux' ~subst metasenv context (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph - | None -> raise (RefineFailure "Rel to hidden hypothesis") + | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure "Not a close term") - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst + _ -> raise (RefineFailure (lazy "Not a close 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) -> + 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 + check_metasenv_consistency n subst metasenv context + canonical_context l ugraph in - (* trust or check ??? *) - C.Meta (n,l'),CicSubstitution.subst_meta l' ty, + (* 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) *) + (* 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 + check_metasenv_consistency n subst metasenv context + canonical_context l ugraph in - C.Meta (n,l'),CicSubstitution.subst_meta l' ty, + C.Meta (n,l'),CicSubstitution.subst_meta l' ty, subst', metasenv',ugraph1) - | C.Sort (C.Type tno) -> + | C.Sort (C.Type tno) -> let tno' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt tno' tno ugraph in - t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 - | C.Sort _ -> + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph - | C.Implicit _ -> raise (AssertFailure "21") - | C.Cast (te,ty) -> - let ty',_,subst',metasenv',ugraph1 = + | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Cast (te,ty) -> + let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in - let te',inferredty,subst'',metasenv'',ugraph2 = + let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 - in - (try - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' - inferredty ty ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - _ -> raise (RefineFailure "Cast")) - | C.Prod (name,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = + in + let subst''',metasenv''',ugraph3 = + fo_unif_subst subst'' context metasenv'' + inferredty ty' ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + | C.Prod (name,s,t) -> + let carr t subst context = CicMetaSubst.apply_subst subst t in + let coerce_to_sort + in_source tgt_sort t type_to_coerce subst ctx metasenv uragph + = + let coercion_src = carr type_to_coerce subst ctx in + match coercion_src with + | Cic.Sort _ -> + t,type_to_coerce,subst,metasenv,ugraph +(* + | Cic.Meta _ as meta when not in_source -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let subst, metasenv, ugraph = + fo_unif_subst + subst ctx metasenv meta coercion_tgt ugraph + in + t, Cic.Sort tgt_sort, subst, metasenv, ugraph +*) + | Cic.Meta _ as meta -> + t, meta, subst, metasenv, ugraph + | Cic.Cast _ as cast -> + t, cast, subst, metasenv, ugraph + | term -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + (match boh with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + raise + (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) + | CoercGraph.NotMetaClosed -> + raise + (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) + | CoercGraph.SomeCoercion c -> + Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) + in + let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let t',sort2,subst'',metasenv'',ugraph2 = + let s',sort1,subst', metasenv',ugraph1 = + coerce_to_sort true (Cic.Type(CicUniv.fresh())) + s' sort1 subst' context metasenv' ugraph1 + in + let context_for_t = ((Some (name,(C.Decl s')))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t in + let t',sort2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' - ((Some (name,(C.Decl s')))::context) t ugraph1 - in - let sop,subst''',metasenv''',ugraph3 = - sort_of_prod subst'' metasenv'' - context (name,s') (sort1,sort2) ugraph2 + context_for_t t ugraph1 + in + let t',sort2,subst'',metasenv'',ugraph2 = + coerce_to_sort false (Cic.Type(CicUniv.fresh())) + t' sort2 subst'' context_for_t metasenv'' 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 - (match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> () - | _ -> - raise (RefineFailure (sprintf - "Not well-typed lambda-abstraction: the source %s should be a type; - instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1))) - ) ; - let t',type2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - ((Some (n,(C.Decl s')))::context) t ugraph1 - in - C.Lambda (n,s',t'),C.Prod (n,s',type2), - subst'',metasenv'',ugraph2 - | C.LetIn (n,s,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 t',inferredty,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1 - in - (* One-step LetIn reduction. + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod subst'' metasenv'' + context (name,s') (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 = + match CicReduction.whd ~subst:subst' context sort1 with + C.Meta _ + | C.Sort _ -> s',sort1 + | coercion_src -> + let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + match boh with + | CoercGraph.SomeCoercion c -> + Cic.Appl [c;s'], coercion_tgt + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ + | CoercGraph.NotMetaClosed -> + raise (RefineFailure (lazy (sprintf + "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1)))) + in + let context_for_t = ((Some (n,(C.Decl s')))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t 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,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 context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t 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. + * Moreover the inferred type is closer to the expected one. *) - C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, + C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, subst'',metasenv'',ugraph2 - | C.Appl (he::((_::_) as tl)) -> - let he',hetype,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context he ugraph - in - let tlbody_and_type,subst'',metasenv'',ugraph2 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) tl ([],subst',metasenv',ugraph1) - in + | C.Appl (he::((_::_) as tl)) -> + let he',hetype,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context he ugraph + in + let tlbody_and_type,subst'',metasenv'',ugraph2 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) tl ([],subst',metasenv',ugraph1) + in let tl',applty,subst''',metasenv''',ugraph3 = - eat_prods subst'' metasenv'' context + try + eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 + with + exn -> + enrich + (fun msg -> + lazy ("The application " ^ + CicMetaSubst.ppterm_in_context subst'' t context ^ + " is not well typed:\n" ^ Lazy.force msg)) exn in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | C.Appl _ -> raise (RefineFailure "Appl: no arguments") - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context + | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) + | 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 + 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 + 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 = + let ty_uri,ugraph2 = type_of_mutual_inductive_constr uri i j ugraph1 in - let cty = - CicSubstitution.subst_vars exp_named_subst' ty_uri + let cty = + CicSubstitution.subst_vars exp_named_subst' ty_uri in - C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst', + 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) + | 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 (_,b,arity,constructors), expl_params, no_left_params,ugraph = let _ = CicTypeChecker.typecheck uri in - let obj,u = CicEnvironment.get_cooked_obj ugraph 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 - | _ -> - raise - (RefineFailure - ("Unkown mutual inductive definition " ^ - U.string_of_uri uri)) + C.InductiveDefinition (l,expl_params,parsno,_) -> + List.nth l i , expl_params, parsno, u + | _ -> + raise + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ + U.string_of_uri uri))) in - let rec count_prod t = + let rec count_prod t = match CicReduction.whd ~subst context t with - C.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 + 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 = + 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 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 + 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 = + let metasenv,exp_named_subst = CicMkImplicit.fresh_subst metasenv subst context expl_params in - let expected_type = + let expected_type = if no_args = 0 then - C.MutInd (uri,i,exp_named_subst) + C.MutInd (uri,i,exp_named_subst) else - C.Appl + 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 = + 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 = + 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 = + in + let actual_type = CicReduction.whd ~subst context actual_type in + let subst,metasenv,ugraph3 = fo_unif_subst subst context metasenv expected_type' actual_type ugraph2 - in + in let rec instantiate_prod t = function [] -> t @@ -397,37 +596,37 @@ and type_of_aux' metasenv context t ugraph = in let arity_instantiated_with_left_args = instantiate_prod arity left_args in - (* TODO: check if the sort elimination + (* TODO: check if the sort elimination * is allowed: [(I q1 ... qr)|B] *) - let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = + let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = List.fold_left - (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p -> - let constructor = - if left_args = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl + (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p -> + 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 + 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 = - check_branch 0 context metasenv subst no_left_params + let outtypeinstance,subst,metasenv,ugraph3 = + check_branch 0 context metasenv subst no_left_params actual_type constructor' expected_type ugraph2 in - (pl @ [p'],j+1, + (pl @ [p'],j+1, outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) - ([],1,[],subst,metasenv,ugraph3) pl + ([],1,[],subst,metasenv,ugraph3) pl 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 + The easy case is when the outype is specified, that amount + to a trivial check. Otherwise, we should guess a type from + its instances *) (match outtype with @@ -487,7 +686,7 @@ and type_of_aux' metasenv context t ugraph = let metasenv,new_meta = CicMkImplicit.mk_implicit metasenv subst extended_context in - let irl = + let irl = CicMkImplicit.identity_relocation_list_for_metavariable extended_context in @@ -550,7 +749,7 @@ and type_of_aux' metasenv context t ugraph = None,ugraph4,metasenv,subst in match candidate with - | None -> raise (Uncertain "can't solve an higher order unification problem") + | None -> raise (Uncertain (lazy "can't solve an higher order unification problem")) | Some candidate -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv @@ -562,6 +761,22 @@ and type_of_aux' metasenv context t ugraph = (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 + in + let tlbody_and_type,subst,metasenv,ugraph4 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + in + let _,_,subst,metasenv,ugraph4 = + eat_prods false subst metasenv context + outtypety tlbody_and_type ugraph4 + in let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 @@ -588,33 +803,34 @@ and type_of_aux' metasenv context t ugraph = (CicMetaSubst.apply_subst subst (C.Appl(outtype::right_args@[term]))), subst,metasenv,ugraph6) - | C.Fix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1 = - List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> - let ty',_,subst',metasenv',ugraph1 = + | C.Fix (i,fl) -> + let fl_ty',subst,metasenv,types,ugraph1 = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> + let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in - fl @ [ty'],subst',metasenv', + fl @ [ty'],subst',metasenv', Some (C.Name n,(C.Decl ty')) :: types, ugraph - ) ([],subst,metasenv,[],ugraph) fl - in - let len = List.length types in - let context' = types@context in - let fl_bo',subst,metasenv,ugraph2 = + ) ([],subst,metasenv,[],ugraph) fl + in + let len = List.length types in + let context' = types@context in + let fl_bo',subst,metasenv,ugraph2 = List.fold_left - (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) -> - let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph - in + (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> + let metasenv, bo = exp_impl metasenv subst context' bo in + let bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph + in let subst',metasenv',ugraph' = - fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) ugraph1 + fo_unif_subst subst context' metasenv + ty_of_bo (CicSubstitution.lift len ty) ugraph1 in fl @ [bo'] , subst',metasenv',ugraph' - ) ([],subst,metasenv,ugraph1) fl + ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') in - let (_,_,ty,_) = List.nth fl i 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. @@ -629,33 +845,34 @@ and type_of_aux' metasenv context t ugraph = 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 = - List.fold_left - (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> - let ty',_,subst',metasenv',ugraph1 = + | C.CoFix (i,fl) -> + let fl_ty',subst,metasenv,types,ugraph1 = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> + let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in - fl @ [ty'],subst',metasenv', + fl @ [ty'],subst',metasenv', Some (C.Name n,(C.Decl ty')) :: types, ugraph1 - ) ([],subst,metasenv,[],ugraph) fl - in - let len = List.length types in - let context' = types@context in - let fl_bo',subst,metasenv,ugraph2 = + ) ([],subst,metasenv,[],ugraph) fl + in + let len = List.length types in + let context' = types@context in + let fl_bo',subst,metasenv,ugraph2 = List.fold_left - (fun (fl,subst,metasenv,ugraph) (name,ty,bo) -> - let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph - in + (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> + let metasenv, bo = exp_impl metasenv subst context' bo in + let bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph + in let subst',metasenv',ugraph' = - fo_unif_subst subst context' metasenv + fo_unif_subst subst context' metasenv ty_of_bo (CicSubstitution.lift len ty) ugraph1 in fl @ [bo'],subst',metasenv',ugraph' - ) ([],subst,metasenv,ugraph1) fl + ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') in - let (_,ty,_) = List.nth fl i 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. @@ -682,93 +899,89 @@ and type_of_aux' metasenv context t ugraph = let module S = CicSubstitution in let lifted_canonical_context = let rec aux i = - function + function [] -> [] - | (Some (n,C.Decl t))::tl -> + | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> + | (Some (n,C.Def (t,None)))::tl -> (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) - | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> + | None::tl -> None::(aux (i+1) tl) + | (Some (n,C.Def (t,Some ty)))::tl -> (Some (n, - C.Def ((S.subst_meta l (S.lift i t)), - Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) + C.Def ((S.subst_meta l (S.lift i t)), + Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) in - aux 1 canonical_context + aux 1 canonical_context in try - List.fold_left2 - (fun (l,subst,metasenv,ugraph) t ct -> + List.fold_left2 + (fun (l,subst,metasenv,ugraph) t ct -> match (t,ct) with - _,None -> - l @ [None],subst,metasenv,ugraph + _,None -> + l @ [None],subst,metasenv,ugraph | Some t,Some (_,C.Def (ct,_)) -> let subst',metasenv',ugraph' = - (try - fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + (try + fo_unif_subst subst context metasenv t ct ugraph + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) 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 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 (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + (try + fo_unif_subst + subst' context metasenv' inferredty ct ugraph1 + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (sprintf - "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context))) - ) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with - Invalid_argument _ -> - raise - (RefineFailure - (sprintf - "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context))) + Invalid_argument _ -> + raise + (RefineFailure + (lazy (sprintf + "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" + (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext subst canonical_context)))) 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) as subst)::tl -> - let ty_uri,ugraph1 = type_of_variable uri ugraph in - let typeofvar = + [] -> [],metasubst,metasenv,ugraph + | ((uri,t) as subst)::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 - "A variable with a body can not be explicit substituted") - | Cic.Variable (_,None,_,_) -> () - | _ -> - raise - (RefineFailure - ("Unkown variable definition " ^ UriManager.string_of_uri uri)) - ) ; - *) - let t',typeoft,metasubst',metasenv',ugraph2 = + (* 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 + in let metasubst'',metasenv'',ugraph3 = try - fo_unif_subst + fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2 with _ -> - raise (RefineFailure - ("Wrong Explicit Named Substitution: " ^ + raise (RefineFailure (lazy + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ - " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar)) + " not unifiable with " ^ + CicMetaSubst.ppterm metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -786,119 +999,141 @@ and type_of_aux' metasenv context t ugraph = 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 or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + (* different than Coq manual!!! *) C.Sort s2,subst,metasenv,ugraph - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) - let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),subst,metasenv,ugraph2 - | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) - C.Sort (C.Type t1),subst,metasenv,ugraph - | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph - | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),subst,metasenv,ugraph2 + | (C.Sort _,C.Sort (C.Type t1)) -> + C.Sort (C.Type t1),subst,metasenv,ugraph + | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph + | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> (* TODO how can we force the meta to become a sort? If we don't we * brake the invariant that refine produce only well typed terms *) - (* 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 *) + (* 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) = - fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph + fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' ugraph in t2'',subst,metasenv,ugraph1 - | (_,_) -> - raise (RefineFailure (sprintf - "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" - (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2''))) + | _,_ -> + raise + (RefineFailure + (lazy + (sprintf + ("Two sorts were expected, found %s " ^^ + "(that reduces to %s) and %s (that reduces to %s)") + (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) + (CicPp.ppterm t2'')))) - and eat_prods subst metasenv context hetype tlbody_and_type ugraph = + and eat_prods + allow_coercions subst metasenv context hetype tlbody_and_type ugraph + = let rec mk_prod metasenv context = function - [] -> - let (metasenv, idx) = + [] -> + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in - let irl = + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context - in + in metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = + | (_,argty)::tl -> + let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let meta = Cic.Meta (idx,irl) in - let name = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let meta = Cic.Meta (idx,irl) in + let name = (* The name must be fresh for context. *) (* Nevertheless, argty is well-typed only in context. *) (* Thus I generate a name (name_hint) in context and *) (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in (context'@context). *) let name_hint = - (* Cic.Name "pippo" *) - FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - ~typ:(CicMetaSubst.apply_subst subst argty) + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name ~subst - [] context name_hint ~typ:(Cic.Sort Cic.Prop) - in - let metasenv,target = + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl - in + in metasenv,Cic.Prod (name,meta,target) in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv,ugraph1) = try - fo_unif_subst subst context metasenv hetype hetype' ugraph + fo_unif_subst subst context metasenv hetype hetype' ugraph with exn -> - debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" - (CicPp.ppterm hetype) - (CicPp.ppterm hetype') - (CicMetaSubst.ppmetasenv metasenv []) - (CicMetaSubst.ppsubst subst)); - raise exn + debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" + (CicPp.ppterm hetype) + (CicPp.ppterm hetype') + (CicMetaSubst.ppmetasenv [] metasenv) + (CicMetaSubst.ppsubst subst))); + raise exn in let rec eat_prods metasenv subst context hetype ugraph = function | [] -> [],metasenv,subst,hetype,ugraph - | (hete, hety)::tl -> + | (hete, hety)::tl -> (match hetype with - Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph1 = - try + Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph1 = + try let subst,metasenv,ugraph1 = fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn -> + with exn when allow_coercions -> (* we search a coercion from hety to s *) - let coer = CoercGraph.look_for_coercion - (CicMetaSubst.apply_subst subst hety) - (CicMetaSubst.apply_subst subst s) + let coer = + let carr t subst context = + CicMetaSubst.apply_subst subst t + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s in match coer with - | None -> raise exn - | Some c -> + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + let msg e = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)) + in + enrich msg exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain (lazy "Coercions on meta")) + | CoercGraph.SomeCoercion c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph - in + in let coerced_args,metasenv',subst',t',ugraph2 = - eat_prods metasenv subst context - (* (CicMetaSubst.subst subst hete t) tl *) - (CicSubstitution.subst hete t) ugraph1 tl + eat_prods metasenv subst context + (CicSubstitution.subst arg t) ugraph1 tl in arg::coerced_args,metasenv',subst',t',ugraph2 | _ -> assert false @@ -936,18 +1171,18 @@ and type_of_aux' metasenv context t ugraph = 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' = + 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' = match ty with - None -> None - | Some ty -> - Some (FreshNamesGenerator.clean_dummy_dependent_types ty) - in + None -> None + | Some ty -> + Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + in Some (n, Cic.Def (bo',ty')) ) context in @@ -961,19 +1196,82 @@ let type_of_aux' metasenv context term ugraph = try type_of_aux' metasenv context term ugraph with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg) + CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) -(*CSC: this is a very very rough approximation; to be finished *) -let are_all_occurrences_positive uri = - let rec aux = - (*CSC: here we should do a whd; but can we do that? *) - function - Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> () - | Cic.MutInd (uri',_,_) when uri = uri' -> () - | Cic.Prod (_,_,t) -> aux t - | _ -> raise (RefineFailure "not well formed constructor type") - in - aux +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 number_of_types = List.length tys in + 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 = let ugraph = CicUniv.empty_ugraph in @@ -1000,7 +1298,7 @@ let typecheck metasenv uri obj = (* instead of raising Uncertain, let's hope that the meta will become a sort *) | Cic.Meta _ -> () - | _ -> raise (RefineFailure "The term provided is not a type") + | _ -> 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 @@ -1033,27 +1331,16 @@ let typecheck metasenv uri obj = let ty = CicTypeChecker.debrujin_constructor uri typesno ty in let ty',_,metasenv,ugraph = type_of_aux' metasenv con_context ty ugraph in - let undebrujin 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)) in - let ty' = undebrujin ty' in + let ty' = undebrujin uri typesno tys ty' in metasenv,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 *) - List.iter - (fun (_,_,_,cl) -> - List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl - ) tys ; + let metasenv,ugraph,tys = + are_all_occurrences_positive metasenv ugraph uri tys paramsno + in Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph (* DEBUGGING ONLY @@ -1061,16 +1348,24 @@ let type_of_aux' metasenv context term = try let (t,ty,m) = type_of_aux' metasenv context term in - debug_print - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty); - debug_print - ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []); + 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 ("@@@ REFINE FAILED: " ^ msg); + debug_print (lazy ("@@@ REFINE FAILED: " ^ msg)); raise e | Uncertain msg as e -> - debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); + debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); raise e ;; *) + +let profiler2 = HExtlib.profile "CicRefine" + +let type_of_aux' metasenv context term ugraph = + profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph + +let typecheck metasenv uri obj = + profiler2.HExtlib.profile (typecheck metasenv uri) obj