Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: include   Sprache: Isabelle

Original von: Coq©

(* -*-tuareg-*- *)

(* Caml script to include for debugging the checker.
   Usage: from the checker/ directory launch ocaml toplevel and then
   type #use"include";;
   This command loads the relevant modules, defines some pretty
   printers, and provides functions to interactively check modules
   (mainly run_l and norec).
 *)

#cd "..";;
#directory "lib";;
#directory "kernel";;
#directory "checker";;
#directory "+threads";;

#load "unix.cma";;
#load"threads.cma";;
#load "str.cma";;
#load "gramlib.cma";;
(*#load "toplevellib.cma";;

#directory "/usr/lib/ocaml/compiler-libs/utils";;
let _ = Clflags.recursive_types:=true;;
*)
#load "check.cma";;

open Typeops;;
open Check;;

open Pp;;
open CErrors;;
open Util;;
open Names;;
open Term;;
open Environ;;
open Declarations;;
open Mod_checking;;
open Cic;;

let pr_id id = str(string_of_id id)
let pr_na = function Name id -> pr_id id | _ -> str"_";;
let prdp dp = pp(str(string_of_dirpath dp));;
(*
let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
let prcs cs = prc (Declarations.force cs);;
let pru u = pp(str(Univ.string_of_universe u));;*)
let pru u = pp(Univ.pr_uni u);;
let prlab l = pp(str(string_of_label l));;
let prid id = pp(pr_id id);;
let prcon c = pp(Indtypes.prcon c);;
let prkn kn = pp(Indtypes.prkn kn);;


let prus g = pp(Univ.pr_universes g);;

let prcstrs c =
  let g = Univ.merge_constraints c Univ.initial_universes in
  pp(Univ.pr_universes g);;
(*let prcstrs c = pp(Univ.pr_constraints c);; *)
(*
let prenvu e =
  let u = universes e in
  let pu =
  str "UNIVERSES:"++fnl()++str"  "++hov 0 (Univ.pr_universes u) ++fnl() in
  pp pu;;

let prenv e =
  let ctx1 = named_context e in
  let ctx2 = rel_context e in
  let pe =
    hov 1 (str"[" ++
           prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
           str"]") ++ spc() ++
    hov 1 (str"[" ++
           prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
           str"]") in
  pp pe;;
*)

(*
let prsub s =
  let string_of_mp mp =
    let s = string_of_mp mp in
    (match mp with MPbound _ -> "#bound."|_->"")^s in 
  pp (hv 0 
  (fold_subst
    (fun msid mp strm ->
      str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
      str (string_of_mp mp) ++ fnl() ++ strm)
    (fun mbid mp strm ->
      str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
      str (string_of_mp mp) ++ fnl() ++ strm)
    (fun mp1 mp strm ->
      str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
      str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
;;
*)

#install_printer prid;;
#install_printer prcon;;
#install_printer prlab;;
#install_printer prdp;;
#install_printer prkn;;
#install_printer pru;;
(*
#install_printer prc;;
#install_printer prcs;;
*)
#install_printer prcstrs;;
(*#install_printer prus;;*)
(*#install_printer prenv;;*)
(*#install_printer prenvu;;
#install_printer prsub;;*)

Checker.init_with_argv [|"";"-coqlib";"."|];;
Flags.quiet := false;;
Flags.debug := true;;
Sys.catch_break true;;

let module_of_file f =
  let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
  (mb:Cic.module_body)
;;
let deref_mod md s =
  let l = match md.mod_expr with
      Struct(NoFunctor l) -> l 
    | FullStruct ->
      (match md.mod_type with
 NoFunctor l -> l)
 in
  List.assoc (label_of_id(id_of_string s)) l
;;
(*
let mod_access m fld =
  match m.mod_expr with
      Some(SEBstruct l) -> List.assoc fld l
    | _ -> failwith "bad structure type"
;;
*)
let parse_dp s =
  make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s))
;;
let parse_sp s =
  let l = List.rev (Str.split(Str.regexp"\\.") s) in
  {dirpath=List.tl l; basename=List.hd l};;
let parse_kn s =
   let l = List.rev (Str.split(Str.regexp"\\.") s) in
   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
   make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
;;
let parse_con s =
   let l = List.rev (Str.split(Str.regexp"\\.") s) in
   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
   make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
;;
let get_mod dp = 
  lookup_module dp (Safe_typing.get_env())
;;
let get_mod_type dp = 
  lookup_modtype dp (Safe_typing.get_env())
;;
let get_cst kn = 
  lookup_constant kn (Safe_typing.get_env())
;;

let read_mod s f = 
  let lib = intern_from_file (parse_dp s,f) in
  ((Obj.magic lib.library_compiled):
    dir_path *
    module_body *
    (dir_path * Digest.t) list *
    engagement option);;


let expln f x =
  try f x
  with UserError(_,strm) as e ->
    msgnl strm; raise e

let admit_l l =
  let l = List.map parse_sp l in
  Check.recheck_library ~admit:l ~check:l;;
let run_l l =
  Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
let norec q =
  Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;

(*
admit_l["Bool";"OrderedType";"DecidableType"];;
run_l["FSetInterface"];;
*)

¤ Dauer der Verarbeitung: 0.31 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik