X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=b85a4a519a01cbd95dc77438cdd0a5a555f2b820;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=28a8ed31b378e4e433412c1c44ff375421e30f42;hpb=086099d1a60948454cf0874744ef2222c2edc1b6;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index 28a8ed31b..b85a4a519 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -25,23 +25,34 @@ open Printf +exception Elim_failure of string +exception Can_t_eliminate + let fresh_binder = let counter = ref ~-1 in function | true -> incr counter; - Cic.Name ("elim" ^ string_of_int !counter) + Cic.Name ("e" ^ string_of_int !counter) | _ -> Cic.Anonymous (** verifies if a given inductive type occurs in a term in target position *) -let rec recursive uri typeno subst = function - | Cic.Prod (_, _, target) -> recursive uri typeno subst target - | Cic.MutInd (uri', typeno', subst') - | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: _) -> - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -(* | Cic.Appl args -> List.exists (recursive uri typeno subst) args *) +let rec recursive uri typeno = function + | Cic.Prod (_, _, target) -> recursive uri typeno target + | Cic.MutInd (uri', typeno', []) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: _) -> + UriManager.eq uri uri' && typeno = typeno' | _ -> false + (** given a list of constructor types, return true if at least one of them is + * recursive, false otherwise *) +let recursive_type uri typeno constructors = + let rec aux = function + | Cic.Prod (_, src, tgt) -> recursive uri typeno src || aux tgt + | _ -> false + in + List.exists (fun (_, ty) -> aux ty) constructors + let unfold_appl = function | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl) | t -> t @@ -56,11 +67,10 @@ let rec split l n = * @param paramsno number of Prod to ignore in this constructor (i.e. number of * inductive parameters) * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *) -let rec delta (uri, typeno, subst) dependent paramsno consno t p args = - assert (subst = []); +let rec delta (uri, typeno) dependent paramsno consno t p args = match t with - | Cic.MutInd (uri', typeno', subst') when - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> if dependent then (match args with | [] -> assert false @@ -68,8 +78,8 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args = | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)])) else p - | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> let (lparams, rparams) = split tl paramsno in if dependent then (match args with @@ -83,22 +93,22 @@ let rec delta (uri, typeno, subst) dependent paramsno consno t p args = | [] -> p | _ -> Cic.Appl (p :: rparams)) | Cic.Prod (binder, src, tgt) -> - if recursive uri typeno subst src then + if recursive uri typeno src then let args = List.map (CicSubstitution.lift 2) args in let phi = let src = CicSubstitution.lift 1 src in - delta (uri, typeno, subst) dependent paramsno consno src + delta (uri, typeno) dependent paramsno consno src (CicSubstitution.lift 1 p) [Cic.Rel 1] in let tgt = CicSubstitution.lift 1 tgt in Cic.Prod (fresh_binder dependent, src, Cic.Prod (Cic.Anonymous, phi, - delta (uri, typeno, subst) dependent paramsno consno tgt + delta (uri, typeno) dependent paramsno consno tgt (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2]))) else (* non recursive *) let args = List.map (CicSubstitution.lift 1) args in Cic.Prod (fresh_binder dependent, src, - delta (uri, typeno, subst) dependent paramsno consno tgt + delta (uri, typeno) dependent paramsno consno tgt (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1])) | _ -> assert false @@ -114,17 +124,17 @@ let rec strip_left_params consno leftno = function strip_left_params consno (leftno - 1) tgt | _ -> assert false -let delta (ury, typeno, subst) dependent paramsno consno t p args = +let delta (ury, typeno) dependent paramsno consno t p args = let t = strip_left_params consno paramsno t in - delta (ury, typeno, subst) dependent paramsno consno t p args + delta (ury, typeno) dependent paramsno consno t p args -let rec add_params indno ty eliminator = +let rec add_params binder indno ty eliminator = if indno = 0 then eliminator else match ty with - | Cic.Prod (binder, src, tgt) -> - Cic.Prod (binder, src, add_params (indno - 1) tgt eliminator) + | Cic.Prod (name, src, tgt) -> + binder name src (add_params binder (indno - 1) tgt eliminator) | _ -> assert false let rec mk_rels consno = function @@ -152,7 +162,7 @@ let rec type_of_p sort dependent leftno indty = function let rec add_right_pi dependent strip liftno liftfrom rightno indty = function | Cic.Prod (_, src, tgt) when strip = 0 -> Cic.Prod (fresh_binder true, - CicSubstitution.lift_from (liftfrom + 1) liftno src, + CicSubstitution.lift_from liftfrom liftno src, add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt) | Cic.Prod (_, _, tgt) -> add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt @@ -173,7 +183,7 @@ let rec add_right_lambda dependent strip liftno liftfrom rightno indty case = function | Cic.Prod (_, src, tgt) when strip = 0 -> Cic.Lambda (fresh_binder true, - CicSubstitution.lift_from (liftfrom + 1) liftno src, + CicSubstitution.lift_from liftfrom liftno src, add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty case tgt) | Cic.Prod (_, _, tgt) -> @@ -181,115 +191,59 @@ function case tgt | t -> Cic.Lambda (fresh_binder true, - CicSubstitution.lift_from (rightno + 1) liftno indty, - case) - -exception Failure of string - -let string_of_sort = function - | Cic.Prop -> "Prop" - | Cic.CProp -> "CProp" - | Cic.Set -> "Set" - | Cic.Type _ -> "Type" + CicSubstitution.lift_from (rightno + 1) liftno indty, case) -let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = - let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in - let subst = [] in - match obj with - | Cic.InductiveDefinition (indTypes, params, leftno) -> - let (name, inductive, ty, constructors) = - try - List.nth indTypes typeno - with Failure _ -> assert false - in - let paramsno = count_pi ty in (* number of (left or right) parameters *) - let rightno = paramsno - leftno in - let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in - let conslen = List.length constructors in - let consno = ref (conslen + 1) in - if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then - raise (Failure (sprintf "can't eliminate from Prop to %s" - (string_of_sort sort))); - let indty = - let indty = Cic.MutInd (uri, typeno, subst) in - if paramsno = 0 then - indty - else - Cic.Appl (indty :: mk_rels 0 paramsno) - in - let mk_constructor consno = - let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in - if leftno = 0 then - constructor - else - Cic.Appl (constructor :: mk_rels consno leftno) - in - let eliminator = - let p_ty = type_of_p sort dependent leftno indty ty in - let final_ty = - add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty - in - Cic.Prod (Cic.Name "P", p_ty, - (List.fold_right - (fun (_, constructor) acc -> - decr consno; - let p = Cic.Rel !consno in - Cic.Prod (Cic.Anonymous, - (delta (uri, typeno, subst) dependent leftno !consno - constructor p [mk_constructor !consno]), - acc)) - constructors final_ty)) - in - add_params leftno ty eliminator - | _ -> assert false - -let rec branch (uri, typeno, subst) insource paramsno t fix head args = - assert (subst = []); +let rec branch (uri, typeno) insource paramsno t fix head args = match t with - | Cic.MutInd (uri', typeno', subst') when - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> - let head = if insource then fix else head in - (match args with - | [] -> head - | _ -> Cic.Appl (head :: args)) - | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when - UriManager.eq uri uri' && typeno = typeno' && subst = subst' -> - let (lparams, rparams) = split tl paramsno in - (match args with - | [] when insource && rparams = [] -> fix - | [] when insource -> Cic.Appl (fix :: rparams) - | _ when insource -> Cic.Appl (fix :: rparams @ args) - | _ -> Cic.Appl (head :: rparams @ args)) + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + (match args with + | [arg] -> Cic.Appl (fix :: args) + | _ -> Cic.Appl (head :: [Cic.Appl args])) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + let (lparams, rparams) = split tl paramsno in + match args with + | [arg] -> Cic.Appl (fix :: rparams @ args) + | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args]) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) | Cic.Prod (binder, src, tgt) -> - if recursive uri typeno subst src then + if recursive uri typeno src then let args = List.map (CicSubstitution.lift 1) args in let phi = let fix = CicSubstitution.lift 1 fix in - branch (uri, typeno, subst) true paramsno src fix head - (args @ [Cic.Rel 1]) + let src = CicSubstitution.lift 1 src in + branch (uri, typeno) true paramsno src fix head [Cic.Rel 1] in - let tgt = CicSubstitution.lift 1 tgt in Cic.Lambda (fresh_binder true, src, - branch (uri, typeno, subst) insource paramsno tgt + branch (uri, typeno) insource paramsno tgt (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) (args @ [Cic.Rel 1; phi])) else (* non recursive *) let args = List.map (CicSubstitution.lift 1) args in Cic.Lambda (fresh_binder true, src, - branch (uri, typeno, subst) insource paramsno tgt + branch (uri, typeno) insource paramsno tgt (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) (args @ [Cic.Rel 1])) | _ -> assert false -let branch (uri, typeno, subst) insource liftno paramsno t fix head args = +let branch (uri, typeno) insource liftno paramsno t fix head args = let t = strip_left_params liftno paramsno t in - branch (uri, typeno, subst) insource paramsno t fix head args + branch (uri, typeno) insource paramsno t fix head args -let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = - let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in - let subst = [] in +let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = + let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in match obj with - | Cic.InductiveDefinition (indTypes, params, leftno) -> + | Cic.InductiveDefinition (indTypes, params, leftno, _) -> let (name, inductive, ty, constructors) = try List.nth indTypes typeno @@ -301,59 +255,116 @@ let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = let conslen = List.length constructors in let consno = ref (conslen + 1) in if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then - raise (Failure (sprintf "can't eliminate from Prop to %s" - (string_of_sort sort))); + raise Can_t_eliminate; let indty = - let indty = Cic.MutInd (uri, typeno, subst) in + let indty = Cic.MutInd (uri, typeno, []) in if paramsno = 0 then indty else Cic.Appl (indty :: mk_rels 0 paramsno) in let mk_constructor consno = - let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in + let constructor = Cic.MutConstruct (uri, typeno, consno, []) in if leftno = 0 then constructor else Cic.Appl (constructor :: mk_rels consno leftno) in - let eliminator = - let p_ty = type_of_p sort dependent leftno indty ty in - let final_ty = - add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty + let p_ty = type_of_p sort dependent leftno indty ty in + let final_ty = + add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty + in + let eliminator_type = + let cic = + Cic.Prod (Cic.Name "P", p_ty, + (List.fold_right + (fun (_, constructor) acc -> + decr consno; + let p = Cic.Rel !consno in + Cic.Prod (Cic.Anonymous, + (delta (uri, typeno) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors final_ty)) in + add_params (fun b s t -> Cic.Prod (b, s, t)) leftno ty cic + in + let consno = ref (conslen + 1) in + let eliminator_body = let fix = Cic.Rel (rightno + 2) in + let is_recursive = recursive_type uri typeno constructors in + let recshift = if is_recursive then 1 else 0 in let (_, branches) = List.fold_right (fun (_, ty) (shift, branches) -> - let head = Cic.Rel (rightno + shift + 2) in + let head = Cic.Rel (rightno + shift + 1 + recshift) in let b = - branch (uri, typeno, subst) false (rightno + conslen + 3) leftno - ty fix head [] + branch (uri, typeno) false + (rightno + conslen + 2 + recshift) leftno ty fix head [] in (shift + 1, b :: branches)) constructors (1, []) in - let case = - Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 3), Cic.Rel 1, - branches) + let mutcase = + Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 2 + recshift), + Cic.Rel 1, branches) in - let fix_body = - add_right_lambda dependent leftno (conslen + 1) 1 rightno - indty case ty + let body = + if is_recursive then + let fixfun = + add_right_lambda dependent leftno (conslen + 2) 1 rightno + indty mutcase ty + in + (* rightno is the decreasing argument, i.e. the argument of + * inductive type *) + Cic.Fix (0, ["f", rightno, final_ty, fixfun]) + else + add_right_lambda dependent leftno (conslen + 1) 1 rightno indty + mutcase ty + in + let cic = + Cic.Lambda (Cic.Name "P", p_ty, + (List.fold_right + (fun (_, constructor) acc -> + decr consno; + let p = Cic.Rel !consno in + Cic.Lambda (fresh_binder true, + (delta (uri, typeno) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors body)) in - let fix = Cic.Fix (0, ["f", 0, final_ty, fix_body]) in - Cic.Lambda (Cic.Name "P", p_ty, - (List.fold_right - (fun (_, constructor) acc -> - decr consno; - let p = Cic.Rel !consno in - Cic.Lambda (fresh_binder true, - (delta (uri, typeno, subst) dependent leftno !consno - constructor p [mk_constructor !consno]), - acc)) - constructors fix)) + add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic in - add_params leftno ty eliminator - | _ -> assert false +(* +prerr_endline (CicPp.ppterm eliminator_type); +prerr_endline (CicPp.ppterm eliminator_body); +*) + let (computed_type, ugraph) = + try + CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph + with CicTypeChecker.TypeCheckerFailure msg -> + raise (Elim_failure (sprintf + "type checker failure while type checking:\n%s\nerror:\n%s" + (CicPp.ppterm eliminator_body) msg)) + in + if not (fst (CicReduction.are_convertible [] + eliminator_type computed_type ugraph)) + then + raise (Failure (sprintf + "internal error: type mismatch on eliminator type\n%s\n%s" + (CicPp.ppterm eliminator_type) (CicPp.ppterm computed_type))); + let suffix = + match sort with + | Cic.Prop -> "_ind" + | Cic.Set -> "_rec" + | Cic.Type _ -> "_rect" + | _ -> assert false + in + let name = UriManager.name_of_uri uri ^ suffix in + let obj_attrs = [`Class (`Elim sort); `Generated] in + Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) + | _ -> + failwith (sprintf "not an inductive definition (%s)" + (UriManager.string_of_uri uri))