From: Enrico Tassi Date: Fri, 4 Apr 2008 11:46:57 +0000 (+0000) Subject: debugging started X-Git-Tag: make_still_working~5452 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=79501fecaa51e1afff2ac940706b4490b368dc27;p=helm.git debugging started --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 12dc298e7..0485befbe 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -2,7 +2,7 @@ nReference.cmi: nUri.cmi nCicPp.cmi: nCic.cmo oCic2NCic.cmi: nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicTypeChecker.cmi: nCic.cmo +nCicTypeChecker.cmi: nUri.cmi nCic.cmo nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo nCicReduction.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index f00a5e38a..1401a16a6 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -6,12 +6,12 @@ INTERFACE_FILES = \ nReference.mli \ nCicPp.mli \ oCic2NCic.mli \ - nCicEnvironment.mli \ - nCicTypeChecker.mli \ - oCicTypeChecker.mli \ nCicUtils.mli \ nCicSubstitution.mli \ + nCicEnvironment.mli \ nCicReduction.mli \ + nCicTypeChecker.mli \ + oCicTypeChecker.mli \ nCic2OCic.mli IMPLEMENTATION_FILES = \ @@ -20,8 +20,8 @@ EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = OCAMLOPTIONS += -w Ae -all: rt -rt: rt.ml $(PACKAGE).cma +all: rt check +%: %.ml $(PACKAGE).cma $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml new file mode 100644 index 000000000..39e80cca2 --- /dev/null +++ b/helm/software/components/ng_kernel/check.ml @@ -0,0 +1,20 @@ +let _ = + NCicTypeChecker.set_logger + (function + | `Start_type_checking s -> + prerr_endline ("Start: " ^ NUri.string_of_uri s) + | `Type_checking_completed s -> + prerr_endline ("End: " ^ NUri.string_of_uri s)); + NCicPp.set_ppterm NCicPp.trivial_pp_term; + Helm_registry.load_from "conf.xml"; + let u = UriManager.uri_of_string Sys.argv.(1) in + let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in + let l = OCic2NCic.convert_obj u o in + List.iter + (fun o -> + try NCicTypeChecker.typecheck_obj o + with + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)) + l +;; diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index ff54e0232..fbbf71025 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -18,8 +18,9 @@ let get_obj u = with Not_found -> (* in th final implementation should get it from disk *) let ouri = NUri.ouri_of_nuri u in + prerr_endline (UriManager.string_of_uri ouri); let o,_ = - CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri + CicEnvironment.get_cooked_obj ~trust:true CicUniv.oblivion_ugraph ouri in (* here we should freeze it *) false, HExtlib.list_last (OCic2NCic.convert_obj ouri o) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 6f9a70d50..27c7fc97e 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -7,3 +7,29 @@ let set_ppterm f = ppterm := f;; let ppterm ?(context=[]) ?(subst=[]) ?(metasenv=[]) t = !ppterm ~context ~subst ~metasenv t ;; + +module C = NCic +module R = NReference + +let trivial_pp_term ~context ~subst ~metasenv = + let rec aux ctx = function + | C.Rel m -> + (try List.nth ctx m + with Not_found -> " -" ^ string_of_int (m - List.length context)) + | C.Const r -> R.string_of_reference r + | C.Prod (name,s,t) -> " \Pi "^name^":"^aux ctx s^"."^aux (name::ctx) t + | C.Lambda (name,s,t) -> " \lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t + | C.LetIn (name,ty,t,b) -> + " let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b + | C.Match (_,oty,t,pl) -> + " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^ + String.concat "|" (List.map (aux ctx) pl) ^ "]" + | C.Appl l -> "("^String.concat " " (List.map (aux ctx) l) ^")" + | C.Implicit _ -> "?" + | C.Meta (n,_) -> "?"^string_of_int n + | C.Sort C.Prop -> "Prop" + | C.Sort C.CProp -> "CProp" + | C.Sort (C.Type n) -> "Type"^string_of_int n + in + aux (List.map fst context) + diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index 7a88824c0..ef535cee8 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -9,3 +9,9 @@ val ppterm: ?subst:NCic.substitution -> ?metasenv:NCic.metasenv -> NCic.term -> string + +val trivial_pp_term: + context:NCic.context -> + subst:NCic.substitution -> + metasenv:NCic.metasenv -> + NCic.term -> string diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 7ba5ab152..e0f6bbaed 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -765,9 +765,9 @@ let rec typeof ~subst ~metasenv context term = in if List.length pl <> constructorsno then raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match"))); - let j,branches_ok = + let j,branches_ok,p_ty, exp_p_ty = List.fold_left - (fun (j,b) p -> + (fun (j,b,old_p_ty,old_exp_p_ty) p -> if b then let cons = let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in @@ -778,19 +778,21 @@ let rec typeof ~subst ~metasenv context term = let ty_cons = typeof_aux context cons in let ty_branch = type_of_branch ~subst context leftno outtype cons ty_cons 0 in - j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch + j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch, + ty_p, ty_branch else - j,false - ) (1,true) pl - in - if not branches_ok then - raise - (TypeCheckerFailure - (lazy (Printf.sprintf "Branch for constructor %s has wrong type" - (NCicPp.ppterm (C.Const - (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))))); - let res = outtype::arguments@[term] in - R.head_beta_reduce (C.Appl res) + j,false,old_p_ty,old_exp_p_ty + ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl + in + if not branches_ok then + raise + (TypeCheckerFailure + (lazy (Printf.sprintf "Branch for constructor %s has type %s != %s" + (NCicPp.ppterm (C.Const + (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j))))) + (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); + let res = outtype::arguments@[term] in + R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false and type_of_branch ~subst context leftno outty cons tycons liftno = @@ -953,7 +955,7 @@ let rec typeof ~subst ~metasenv context term = in typeof_aux context term -and check_mutual_inductive_defs _ = assert false +and check_mutual_inductive_defs _ = () and eat_lambdas ~subst context n te = match (n, R.whd ~subst context te) with @@ -1170,7 +1172,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = "the type of the body is not the one expected:\n%s\nvs\n%s" (NCicPp.ppterm ty_te) (NCicPp.ppterm ty)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) - | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj + | C.Inductive _ as obj -> check_mutual_inductive_defs obj | C.Fixpoint (inductive,fl,_) -> let types,kl,len = List.fold_left diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b2591b361..2b59549d6 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -233,16 +233,24 @@ let convert_obj_aux uri = function assert(fixpoints_ty = []); NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)), fixpoints_bo @ fixpoints_ty - | Cic.InductiveDefinition (_,_,_,_) -> assert false (* + | Cic.InductiveDefinition (itl,_,leftno,_) -> let ind = let _,x,_,_ = List.hd itl in x in - let itl = - List.map - (fun name, _, ty, cl -> - [], name, convert_term ty, - List.map (fun name, ty -> [], name, convert_term ty) cl) - itl + let itl, fix_itl = + List.fold_right + (fun (name, _, ty, cl) (itl,acc) -> + let ty, fix_ty = convert_term uri ty in + let cl, fix_cl = + List.fold_right + (fun (name, ty) (cl,acc) -> + let ty, fix_ty = convert_term uri ty in + ([], name, ty)::cl, acc @ fix_ty) + cl ([],[]) + in + ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc) + itl ([],[]) in - NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)) *) + NCic.Inductive (ind, leftno, itl, (`Provided, `Regular)), + fix_itl | Cic.Variable _ | Cic.CurrentProof _ -> assert false ;;