X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMkImplicit.ml;h=a2d0a73d54bbf09ecf10da7b08a2512f9c42dbbf;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=0fa33047f3e2adeab1b2f931746155cb3786cd2c;hpb=bcab6f64ea13c1d4124c7ff53412033df1803918;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 0fa33047f..a2d0a73d5 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -28,7 +28,6 @@ (* where n = List.length [canonical_context] *) (*CSC: ma mi basta la lunghezza del contesto canonico!!!*) let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = - let canonical_context_length = List.length canonical_context in let rec aux = function (_,[]) -> [] @@ -39,63 +38,87 @@ let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = (* Returns the first meta whose number is above the *) (* number of the higher meta. *) -let new_meta metasenv = +let new_meta metasenv subst = let rec aux = function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + None, [] -> 1 + | Some n, [] -> n + | None, n::tl -> aux (Some n,tl) + | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) in - 1 + aux (None,metasenv) + let indexes = + (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst) + in + 1 + aux (None, indexes) + +(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *) +(* questa o la precedente sembrano essere equivalenti come tempi *) +let apply_subst_context _ context = context ;; -let mk_implicit metasenv context = - let newmeta = new_meta metasenv in +let mk_implicit metasenv subst context = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let irl = identity_relocation_list_for_metavariable context in - ([ newmeta, [], Cic.Sort Cic.Type ; + (* in the following mk_* functions we apply substitution to canonical + * context since we have the invariant that the metasenv has already been + * instantiated with subst *) + let context = apply_subst_context subst context in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ; + (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []); newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, newmeta + 2) -let mk_implicit_type metasenv context = - let newmeta = new_meta metasenv in - ([ newmeta, [], Cic.Sort Cic.Type ; +let mk_implicit_type metasenv subst context = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in + let context = apply_subst_context subst context in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv); + (* TASSI: ?? *) newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, newmeta + 1) -let mk_implicit_sort metasenv = - let newmeta = new_meta metasenv in - ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta) +let mk_implicit_sort metasenv subst = + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in + ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta) + (* TASSI: ?? *) -let n_fresh_metas metasenv context n = +let n_fresh_metas metasenv subst context n = if n = 0 then metasenv, [] else let irl = identity_relocation_list_for_metavariable context in - let newmeta = new_meta metasenv in + let context = apply_subst_context subst context in + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let rec aux newmeta n = if n = 0 then metasenv, [] else let metasenv', l = aux (newmeta + 3) (n-1) in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', Cic.Meta(newmeta+2,irl)::l in aux newmeta n -let fresh_subst metasenv context uris = +let fresh_subst metasenv subst context uris = let irl = identity_relocation_list_for_metavariable context in - let newmeta = new_meta metasenv in + let context = apply_subst_context subst context in + let newmeta = new_meta metasenv subst in + let newuniv = CicUniv.fresh () in let rec aux newmeta = function [] -> metasenv, [] | uri::tl -> let metasenv', l = aux (newmeta + 3) tl in - (newmeta, context, Cic.Sort Cic.Type):: + (* TASSI: ?? *) + (newmeta, context, Cic.Sort (Cic.Type newuniv)):: (newmeta + 1, context, Cic.Meta (newmeta, irl)):: (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', (uri,Cic.Meta(newmeta+2,irl))::l in aux newmeta uris -let expand_implicits metasenv context term = +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 @@ -115,16 +138,17 @@ let expand_implicits metasenv context term = 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 context in + 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 [] in + let (metasenv', idx) = mk_implicit metasenv subst [] in metasenv', Cic.Meta (idx, []) | Cic.Implicit None -> - let (metasenv', idx) = mk_implicit metasenv context in + 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 @@ -254,3 +278,36 @@ let expand_implicits metasenv context term = 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 *)