From: Enrico Tassi Date: Tue, 25 Oct 2005 15:49:18 +0000 (+0000) Subject: moved the expansion of implicits inside the refiner in a lazy way X-Git-Tag: V_0_7_2_3~188 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8523a35427aa3fdf40a0e14b8aac3428c8aa13f0;p=helm.git moved the expansion of implicits inside the refiner in a lazy way --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 7e0996f4f..f203e6d79 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -62,8 +62,6 @@ type 'a test_result = let refine_term metasenv context uri term ugraph = (* if benchmark then incr actual_refinements; *) assert (uri=None); - let metasenv, term = - CicMkImplicit.expand_implicits metasenv [] context term in debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = @@ -80,7 +78,6 @@ let refine_term metasenv context uri term ugraph = let refine_obj metasenv context uri obj ugraph = assert (context = []); - let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 0229f2338..39133ac92 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -1006,8 +1006,7 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = else false,ugraph | (C.Cast _, _) | (_, C.Cast _) - | (C.Implicit _, _) | (_, C.Implicit _) -> - assert false + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false,ugraph end in diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 605b9676e..2f7075dac 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -460,7 +460,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = C.Rel m when m = n - (indparamsno - k) -> k - 1 | _ -> raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + (lazy + ("Non-positive occurence in mutual inductive definition(s) [1]" ^ UriManager.string_of_uri uri))) ) indparamsno tl in @@ -468,14 +469,14 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true else raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ UriManager.string_of_uri uri))) | C.Rel m when m = i -> if indparamsno = 0 then true else raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ UriManager.string_of_uri uri))) | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn source && diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index a2d0a73d5..bc60a188d 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -118,196 +118,3 @@ let fresh_subst metasenv subst context uris = (uri,Cic.Meta(newmeta+2,irl))::l in aux newmeta uris -let expand_implicits 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) = mk_implicit_type metasenv subst context in - let irl = identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) - | Cic.Implicit (Some `Closed) -> - let (metasenv', idx) = mk_implicit metasenv subst [] in - metasenv', Cic.Meta (idx, []) - | Cic.Implicit None -> - let (metasenv', idx) = mk_implicit metasenv subst context in - let irl = 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 - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Decl s') :: context) t - in - metasenv'', Cic.Prod (name, s', t') - | Cic.Lambda (name, s, t) -> - let metasenv', s' = aux metasenv context s in - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Decl s') :: context) t - in - metasenv'', Cic.Lambda (name, s', t') - | Cic.LetIn (name, s, t) -> - let metasenv', s' = aux metasenv context s in - let metasenv'', t' = - aux metasenv' (Some (name, Cic.Def (s', None)) :: context) t - 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 context' = - (List.rev_map - (fun (name, t) -> Some (Cic.Name name, Cic.Decl t)) - types) - @ context - in - let metasenv'', bodies = - List.fold_right - (fun (_, _, _, body) (metasenv, bodies) -> - let new_metasenv, new_body = aux metasenv context' body in - (new_metasenv, new_body :: bodies)) - funs (metasenv', []) - in - let rec combine = function - | ((name, index, _, _) :: funs_tl), - ((_, typ) :: typ_tl), - (body :: body_tl) -> - (name, index, typ, body) :: combine (funs_tl, typ_tl, body_tl) - | [], [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types, bodies) 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 context' = - (List.rev_map - (fun (name, t) -> Some (Cic.Name name, Cic.Decl t)) - types) - @ context - in - let metasenv'', bodies = - List.fold_right - (fun (_, _, body) (metasenv, bodies) -> - let new_metasenv, new_body = aux metasenv context' body in - (new_metasenv, new_body :: bodies)) - funs (metasenv', []) - in - let rec combine = function - | ((name, _, _) :: funs_tl), - ((_, typ) :: typ_tl), - (body :: body_tl) -> - (name, typ, body) :: combine (funs_tl, typ_tl, body_tl) - | [], [], [] -> [] - | _ -> assert false - in - let funs' = combine (funs, types, bodies) 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 expand_implicits_in_obj metasenv subst = - function - Cic.Constant (name,bo,ty,params,attrs) -> - let metasenv,bo' = - match bo with - None -> metasenv,None - | Some bo -> - let metasenv,bo' = expand_implicits metasenv subst [] bo in - metasenv,Some bo' in - let metasenv,ty' = expand_implicits metasenv subst [] ty in - metasenv,Cic.Constant (name,bo',ty',params,attrs) - | Cic.CurrentProof (name,metasenv',bo,ty,params,attrs) -> - assert (metasenv' = []); - let metasenv,bo' = expand_implicits metasenv subst [] bo in - let metasenv,ty' = expand_implicits metasenv subst [] ty in - metasenv,Cic.CurrentProof (name,metasenv,bo',ty',params,attrs) - | Cic.InductiveDefinition (tyl,params,paramsno,attrs) -> - let metasenv,tyl = - List.fold_right - (fun (name,b,ty,cl) (metasenv,res) -> - let metasenv,ty' = expand_implicits metasenv subst [] ty in - let metasenv,cl' = - List.fold_right - (fun (name,ty) (metasenv,res) -> - let metasenv,ty' = expand_implicits metasenv subst [] ty in - metasenv,(name,ty')::res - ) cl (metasenv,[]) - in - metasenv,(name,b,ty',cl')::res - ) tyl (metasenv,[]) - in - metasenv,Cic.InductiveDefinition (tyl,params,paramsno,attrs) - | Cic.Variable _ -> assert false (* Not implemented *) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 4f6fcee2e..476270144 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -58,9 +58,3 @@ val fresh_subst: UriManager.uri list -> Cic.metasenv * (Cic.term Cic.explicit_named_substitution) -val expand_implicits: - Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term -> - Cic.metasenv * Cic.term - -val expand_implicits_in_obj: - Cic.metasenv -> Cic.substitution -> Cic.obj -> Cic.metasenv * Cic.obj diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 120fdceaa..03acb40cb 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -50,6 +50,131 @@ let rec split l n = | (_,_) -> 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') + | term -> metasenv,term + 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 = let module C = Cic in let module R = CicReduction in @@ -97,7 +222,7 @@ 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 @@ -114,14 +239,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 - (lazy ("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 *) @@ -139,307 +265,309 @@ 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 (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 (lazy "Rel to hidden hypothesis")) + | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure (lazy "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 (lazy "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 + in (try - let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' + let subst''',metasenv''',ugraph3 = + fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with - _ -> raise (RefineFailure (lazy "Cast"))) - | C.Prod (name,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = + | _ -> raise (RefineFailure (lazy "Cast"))) + | 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 -> + raise (RefineFailure (lazy "no coercion")) + | CoercGraph.NotHandled _ -> + raise (RefineFailure (lazy "not a sort in PI")) + | CoercGraph.NotMetaClosed -> + raise (Uncertain (lazy "Coercions on metas 1")) + | 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 - (try + 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 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 - with - | RefineFailure _ as exn -> - (* given [t] of type [type_to_coerce] returns - * a term that has type [tgt_sort] eventually - * derived from (coercion [t]) *) - let refined_target = t' in - let sort_of_refined_target = sort2 in - let carr t subst context = CicMetaSubst.apply_subst subst t in - let coerce_to_sort tgt_sort t type_to_coerce subst ctx = - match type_to_coerce with - | Cic.Sort _ -> t - | term -> - let coercion_src = carr type_to_coerce subst ctx in - let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in - let search = CoercGraph.look_for_coercion in - (match search coercion_src coercion_tgt with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> raise exn - | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on metas")) - | CoercGraph.SomeCoercion c -> Cic.Appl [c;t]) - in - (* this is probably not the best... *) - let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in - let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in - let new_src = - coerce_to_sort tgt_sort_for_pi_source s sort1 subst context - in - let context_with_new_src = - ((Some (name,(C.Decl new_src)))::context) - in - let new_tgt = - coerce_to_sort - tgt_sort_for_pi_target - refined_target sort_of_refined_target - subst context_with_new_src - in - let newprod = C.Prod (name,new_src,new_tgt) in - let _,sort_of_refined_prod,subst,metasenv,ugraph3 = - type_of_aux subst metasenv context newprod ugraph2 - in - (* this if for a coercion on the tail of the arrow *) - let new_target = - match sort_of_refined_target with - | Cic.Sort _ -> refined_target - | _ -> new_tgt - in - C.Prod(name,new_src,new_target), - sort_of_refined_prod,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 (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)))) - ) ; - 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. + | 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 (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)))) + ) ; + 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 + eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2 in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | 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 + | 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 - (lazy ("Unkown mutual inductive definition " ^ + 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 @@ -451,37 +579,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 outtypeinstance,subst,metasenv,ugraph3 = - check_branch 0 context metasenv subst no_left_params + 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 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 @@ -541,7 +669,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 @@ -642,33 +770,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. @@ -683,33 +812,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. @@ -736,92 +866,88 @@ 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 (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)))))) + (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 (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 | _ -> (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 (lazy (sprintf - "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context)))) - ) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with - Invalid_argument _ -> - raise - (RefineFailure + 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)))) + "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 (Reason - "A variable with a body can not be explicit substituted")) - | Cic.Variable (_,None,_,_) -> () - | _ -> - raise - (RefineFailure (Reason - ("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 (lazy - ("Wrong Explicit Named Substitution: " ^ + raise (RefineFailure (lazy + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ - " not unifiable with " ^ + " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) @@ -840,19 +966,19 @@ 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) + (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)) -> - 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 _) -> + | (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 @@ -878,71 +1004,71 @@ and type_of_aux' metasenv context t ugraph = and eat_prods 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 (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" - (CicPp.ppterm hetype) - (CicPp.ppterm hetype') + 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 + (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 -> (* we search a coercion from hety to s *) let coer = let carr t subst context = @@ -959,9 +1085,9 @@ and type_of_aux' metasenv context t ugraph = 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 + eat_prods metasenv subst context (* (CicMetaSubst.subst subst hete t) tl *) (CicSubstitution.subst hete t) ugraph1 tl in @@ -1001,18 +1127,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 @@ -1028,17 +1154,80 @@ let type_of_aux' metasenv context term ugraph = with 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 (lazy "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 @@ -1098,27 +1287,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