X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=e3fca907dd562f494a479333400c33ef069f08b8;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=b85a4a519a01cbd95dc77438cdd0a5a555f2b820;hpb=8c578ae2acfb32b39610aebbd4baab3a31775a9f;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index b85a4a519..e3fca907d 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -28,13 +28,15 @@ 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 ("e" ^ string_of_int !counter) - | _ -> Cic.Anonymous +let debug_print = fun _ -> () +(*let debug_print = prerr_endline *) + +let counter = ref ~-1 ;; + +let fresh_binder () = Cic.Name "matita_dummy" +(* + incr counter; + Cic.Name ("e" ^ string_of_int !counter) *) (** verifies if a given inductive type occurs in a term in target position *) let rec recursive uri typeno = function @@ -101,13 +103,13 @@ let rec delta (uri, typeno) dependent paramsno consno t p args = (CicSubstitution.lift 1 p) [Cic.Rel 1] in let tgt = CicSubstitution.lift 1 tgt in - Cic.Prod (fresh_binder dependent, src, + Cic.Prod (fresh_binder (), src, Cic.Prod (Cic.Anonymous, phi, 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, + Cic.Prod (fresh_binder (), src, delta (uri, typeno) dependent paramsno consno tgt (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1])) | _ -> assert false @@ -134,6 +136,11 @@ let rec add_params binder indno ty eliminator = else match ty with | Cic.Prod (name, src, tgt) -> + let name = + match name with + Cic.Name _ -> name + | Cic.Anonymous -> fresh_binder () + in binder name src (add_params binder (indno - 1) tgt eliminator) | _ -> assert false @@ -151,7 +158,15 @@ let rec count_pi = function let rec type_of_p sort dependent leftno indty = function | Cic.Prod (n, src, tgt) when leftno = 0 -> - Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt) + let n = + if dependent then + match n with + Cic.Name _ -> n + | Cic.Anonymous -> fresh_binder () + else + n + in + Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt) | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt | t -> if dependent then @@ -161,14 +176,14 @@ 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, + Cic.Prod (fresh_binder (), 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 | t -> if dependent then - Cic.Prod (fresh_binder dependent, + Cic.Prod (fresh_binder (), CicSubstitution.lift_from (rightno + 1) liftno indty, Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1))) else @@ -182,15 +197,15 @@ let rec add_right_pi dependent strip liftno liftfrom rightno indty = function 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, + Cic.Lambda (fresh_binder (), CicSubstitution.lift_from liftfrom liftno src, add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty case tgt) | Cic.Prod (_, _, tgt) -> - add_right_lambda dependent (strip - 1) liftno liftfrom rightno indty + add_right_lambda true (strip - 1) liftno liftfrom rightno indty case tgt | t -> - Cic.Lambda (fresh_binder true, + Cic.Lambda (fresh_binder (), CicSubstitution.lift_from (rightno + 1) liftno indty, case) let rec branch (uri, typeno) insource paramsno t fix head args = @@ -224,13 +239,13 @@ let rec branch (uri, typeno) insource paramsno t fix head args = let src = CicSubstitution.lift 1 src in branch (uri, typeno) true paramsno src fix head [Cic.Rel 1] in - Cic.Lambda (fresh_binder true, src, + Cic.Lambda (fresh_binder (), src, 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, + Cic.Lambda (fresh_binder (), src, branch (uri, typeno) insource paramsno tgt (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) (args @ [Cic.Rel 1])) @@ -241,6 +256,7 @@ let branch (uri, typeno) insource liftno paramsno t fix head args = branch (uri, typeno) insource paramsno t fix head args let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = + counter := ~-1; let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, params, leftno, _) -> @@ -305,9 +321,23 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = (shift + 1, b :: branches)) constructors (1, []) in + let shiftno = conslen + rightno + 2 + recshift in + let outtype = + if dependent then + Cic.Rel shiftno + else + let head = + if rightno = 0 then + CicSubstitution.lift 1 (Cic.Rel shiftno) + else + Cic.Appl + ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) :: + mk_rels 1 rightno) + in + add_right_lambda true leftno shiftno 1 rightno indty head ty + in let mutcase = - Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 2 + recshift), - Cic.Rel 1, branches) + Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches) in let body = if is_recursive then @@ -328,7 +358,7 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = (fun (_, constructor) acc -> decr consno; let p = Cic.Rel !consno in - Cic.Lambda (fresh_binder true, + Cic.Lambda (fresh_binder (), (delta (uri, typeno) dependent leftno !consno constructor p [mk_constructor !consno]), acc)) @@ -337,8 +367,16 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic in (* -prerr_endline (CicPp.ppterm eliminator_type); -prerr_endline (CicPp.ppterm eliminator_body); +debug_print (CicPp.ppterm eliminator_type); +debug_print (CicPp.ppterm eliminator_body); +*) + let eliminator_type = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in + let eliminator_body = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +(* +debug_print (CicPp.ppterm eliminator_type); +debug_print (CicPp.ppterm eliminator_body); *) let (computed_type, ugraph) = try @@ -362,8 +400,11 @@ prerr_endline (CicPp.ppterm eliminator_body); | _ -> assert false in let name = UriManager.name_of_uri uri ^ suffix in + let buri = UriManager.buri_of_uri uri in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in let obj_attrs = [`Class (`Elim sort); `Generated] in - Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) + uri, + Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) | _ -> failwith (sprintf "not an inductive definition (%s)" (UriManager.string_of_uri uri))