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
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 = \
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 $@ $<
--- /dev/null
+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
+;;
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)
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)
+
?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
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
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 =
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
"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
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
;;
projects / helm.git / commitdiff