From a3ba13b9503a2c0dd89b89b489899362d17b3f3a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Jan 2008 16:26:06 +0000 Subject: [PATCH] stub functions to make all compile --- helm/software/components/ng_kernel/.depend | 15 ++ helm/software/components/ng_kernel/Makefile | 12 + helm/software/components/ng_kernel/nCic.ml | 188 +-------------- .../components/ng_kernel/nCicEnvironment.ml | 8 + .../components/ng_kernel/nCicEnvironment.mli | 4 +- .../components/ng_kernel/nCicTypeChecker.ml | 6 + .../components/ng_kernel/nUriManager.ml | 225 +----------------- .../components/ng_kernel/nUriManager.mli | 3 +- .../components/ng_kernel/oCic2NCic.ml | 2 + .../components/ng_kernel/oCic2NCic.mli | 1 + .../components/ng_kernel/oCicTypeChecker.ml | 8 + 11 files changed, 76 insertions(+), 396 deletions(-) create mode 100644 helm/software/components/ng_kernel/.depend create mode 100644 helm/software/components/ng_kernel/Makefile create mode 100644 helm/software/components/ng_kernel/nCicEnvironment.ml create mode 100644 helm/software/components/ng_kernel/nCicTypeChecker.ml create mode 100644 helm/software/components/ng_kernel/oCic2NCic.ml create mode 100644 helm/software/components/ng_kernel/oCic2NCic.mli create mode 100644 helm/software/components/ng_kernel/oCicTypeChecker.ml diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend new file mode 100644 index 000000000..960471d4e --- /dev/null +++ b/helm/software/components/ng_kernel/.depend @@ -0,0 +1,15 @@ +nCicEnvironment.cmi: nUriManager.cmi nCic.cmo +nCicTypeChecker.cmi: nCic.cmo +oCic2NCic.cmi: nCic.cmo +nCic.cmo: nUriManager.cmi +nCic.cmx: nUriManager.cmx +nCicEnvironment.cmo: oCic2NCic.cmi nCicEnvironment.cmi +nCicEnvironment.cmx: oCic2NCic.cmx nCicEnvironment.cmi +nCicTypeChecker.cmo: nCicTypeChecker.cmi +nCicTypeChecker.cmx: nCicTypeChecker.cmi +nUriManager.cmo: nUriManager.cmi +nUriManager.cmx: nUriManager.cmi +oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi +oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi +oCic2NCic.cmo: oCic2NCic.cmi +oCic2NCic.cmx: oCic2NCic.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile new file mode 100644 index 000000000..143fefa1a --- /dev/null +++ b/helm/software/components/ng_kernel/Makefile @@ -0,0 +1,12 @@ +PACKAGE = ng_kernel +PREDICATES = + +INTERFACE_FILES = \ + nCicEnvironment.mli nCicTypeChecker.mli nUriManager.mli oCicTypeChecker.mli oCic2NCic.mli +IMPLEMENTATION_FILES = \ + nCic.ml $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + +include ../../Makefile.defs +include ../Makefile.common diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 23ba6d084..6466912a1 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -23,207 +23,41 @@ * http://cs.unibo.it/helm/. *) -(*****************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* This module defines the internal representation of the objects (variables,*) -(* blocks of (co)inductive definitions and constants) and the terms of cic *) -(* *) -(*****************************************************************************) - -(* $Id: cic.ml 7190 2007-01-31 18:36:04Z sacerdot $ *) -(* -(* STUFF TO MANAGE IDENTIFIERS *) -type id = string (* the abstract type of the (annotated) node identifiers *) -type 'term explicit_named_substitution = (UriManager.uri * 'term) list - - -(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) - -type object_flavour = - [ `Definition - | `MutualDefinition - | `Fact - | `Lemma - | `Remark - | `Theorem - | `Variant - | `Axiom - ] - -type object_class = - [ `Coercion of int - | `Elim of sort (** elimination principle; if sort is Type, the universe is - * not relevant *) - | `Record of (string * bool * int) list (** - inductive type that encodes a record; the arguments are - the record fields names and if they are coercions and - then the coercion arity *) - | `Projection (** record projection *) - | `InversionPrinciple (** inversion principle *) - ] - -type attribute = - [ `Class of object_class - | `Flavour of object_flavour - | `Generated - ] -*) type sort = | Prop | Set - | Type of CicUniv.universe + | Type of int | CProp type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] type name = Name of string | Anonymous -type local_context = int * (term list) option (* shift, subst (None means id) *) +type local_context = int * (term list) option (* shift (0 -> no shift), + subst (None means id) *) and term = | Rel of int (* DeBruijn index, 1 based *) - | Meta of int * local_context + | Meta of int * string option * local_context | Appl of term list (* arguments *) | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) | LetIn of name * term * term * term (* binder, type, term, body *) - | Const of UriManager.uri (* uri contains indtypeno/constrno *) + | Const of NUriManager.uri (* uri contains indtypeno/constrno *) | Sort of sort (* sort *) | Implicit of implicit_annotation (* ... *) - | MutCase of UriManager.uri * (* ind. uri, *) + | MutCase of NUriManager.uri * (* ind. uri, *) term * term * (* outtype, ind. term *) term list (* patterns *) + and obj = - Constant of string * term option * term * (* id, body, type, *) - UriManager.uri list * attribute list (* parameters *) - | Variable of string * term option * term * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | CurrentProof of string * metasenv * term * (* name, conjectures, body, *) - term * UriManager.uri list * attribute list (* type, parameters *) - | InductiveDefinition of inductiveType list * (* inductive types, *) - UriManager.uri list * int * attribute list (* params, left params no *) + | Constant of term option * term + | InductiveDefinition of inductiveType list (* inductive types, *) + and inductiveType = string * bool * term * (* typename, inductive, arity *) constructor list (* constructors *) + and constructor = string * term (* id, type *) -and inductiveFun = - string * int * term * term (* name, ind. index, type, body *) -and coInductiveFun = - string * term * term (* name, type, body *) - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and conjecture = int * context * term -and metasenv = conjecture list -and substitution = (int * (context * term * term)) list - - - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and annconjecture = id * int * anncontext * annterm -and annmetasenv = annconjecture list - -and annterm = - ARel of id * id * int * (* idref, DeBrujin index, *) - string (* binder *) - | AVar of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMeta of id * int * (annterm option) list (* numeric id, *) - (* local context *) - | ASort of id * sort (* sort *) - | AImplicit of id * implicit_annotation option (* *) - | ACast of id * annterm * annterm (* value, type *) - | AProd of id * name * annterm * annterm (* binder, source, target *) - | ALambda of id * name * annterm * annterm (* binder, source, target *) - | ALetIn of id * name * annterm * annterm (* binder, term, target *) - | AAppl of id * annterm list (* arguments *) - | AConst of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMutInd of id * UriManager.uri * int * (* uri, typeno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - | AMutConstruct of id * UriManager.uri * (* uri, *) - int * int * (* typeno, consno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - (* consno is 1 based *) - | AMutCase of id * UriManager.uri * (* ind. uri, *) - int * (* ind. typeno, *) - annterm * annterm * (* outtype, ind. term *) - annterm list (* patterns *) - | AFix of id * int * anninductiveFun list (* funno, functions *) - | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) -and annobj = - AConstant of id * id option * string * (* name, *) - annterm option * annterm * (* body, type, *) - UriManager.uri list * attribute list (* parameters *) - | AVariable of id * - string * annterm option * annterm * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | ACurrentProof of id * id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm * UriManager.uri list * (* body,type,parameters *) - attribute list - | AInductiveDefinition of id * - anninductiveType list * (* inductive types , *) - UriManager.uri list * int * attribute list (* parameters,n ind. pars*) -and anninductiveType = - id * string * bool * annterm * (* typename, inductive, arity *) - annconstructor list (* constructors *) -and annconstructor = - string * annterm (* id, type *) -and anninductiveFun = - id * string * int * annterm * annterm (* name, ind. index, type, body *) -and anncoInductiveFun = - id * string * annterm * annterm (* name, type, body *) -and annotation = - string - -and context_entry = (* A declaration or definition *) - Decl of term - | Def of term * term option (* body, type (if known) *) - -and hypothesis = - (name * context_entry) option (* None means no more accessible *) - -and context = hypothesis list - -and anncontext_entry = (* A declaration or definition *) - ADecl of annterm - | ADef of annterm - -and annhypothesis = - id * (name * anncontext_entry) option (* None means no more accessible *) - -and anncontext = annhypothesis list -;; - -type lazy_term = - context -> metasenv -> CicUniv.universe_graph -> - term * metasenv * CicUniv.universe_graph - -type anntarget = - Object of annobj (* if annobj is a Constant, this is its type *) - | ConstantBody of annobj - | Term of annterm - | Conjecture of annconjecture - | Hypothesis of annhypothesis - -module CicHash = - Hashtbl.Make - (struct - type t = term - let equal = (==) - let hash = Hashtbl.hash_param 100 1000 - end) -;; diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml new file mode 100644 index 000000000..9f75f147c --- /dev/null +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -0,0 +1,8 @@ + +let get_checked_obj nuri = + let ouri = Obj.magic nuri in + let o,_ = + CicEnvironment.get_cooked_obj ~trust:true CicUniv.oblivion_ugraph + ouri + in + OCic2NCic.convert_obj o diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index ac6654cf9..d8b733dc3 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -26,8 +26,6 @@ (* NG: minimal wrapper on the old cicEnvironment, should provide only the * functions strictly necessary to the typechecking algorithm *) -val get_checked_obj : - NCicUniv.universe_graph -> NUriManager.uri -> - NCic.obj * NCicUniv.universe_graph +val get_checked_obj : NUriManager.uri -> NCic.obj (* EOF *) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml new file mode 100644 index 000000000..ca943a828 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -0,0 +1,6 @@ + +exception TypeCheckerFailure of string Lazy.t +exception AssertFailure of string Lazy.t + +(* typechecks the object, raising an exception if illtyped *) +let typecheck_obj obj = () diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml index c0da8eb4b..de7116cb1 100644 --- a/helm/software/components/ng_kernel/nUriManager.ml +++ b/helm/software/components/ng_kernel/nUriManager.ml @@ -23,223 +23,18 @@ * http://cs.unibo.it/helm/. *) -(* $Id$ *) +exception IllFormedUri of string Lazy.t;; -(* - * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) - * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) - * "cic:/a/b/c.ind#xpointer(1/1/1)" => ("cic:/a/b/c.con#xpointer(1/1/1)", id) - *) - -let fresh_id = - let id = ref 0 in - function () -> - incr id; - !id - -(* (uriwithxpointer, uniqueid) - * where uniqueid is used to build a set of uri *) -type uri = string * int;; - -let eq uri1 uri2 = - uri1 == uri2 -;; +(* order, uri, (type, constructor) *) +type uri = private Uri of int * string * (int * int option ) option -let string_of_uri (uri,_) = - uri +let eq (Uri(_,x1,x2)) (Uri(_,y1,y2)) = x1 = y1 && x2 = y2;; -let name_of_uri (uri, _) = - let xpointer_offset = - try String.rindex uri '#' with Not_found -> String.length uri - 1 - in - let index1 = String.rindex_from uri xpointer_offset '/' + 1 in - let index2 = String.rindex uri '.' in - String.sub uri index1 (index2 - index1) - -let nameext_of_uri (uri, _) = - let xpointer_offset, mah = - try String.rindex uri '#', 0 with Not_found -> String.length uri - 1, 1 - in - let index1 = String.rindex_from uri xpointer_offset '/' + 1 in - String.sub uri index1 (xpointer_offset - index1 + mah) - -let buri_of_uri (uri,_) = - let xpointer_offset = - try String.rindex uri '#' with Not_found -> String.length uri - 1 - in - let index = String.rindex_from uri xpointer_offset '/' in - String.sub uri 0 index - -module OrderedStrings = - struct - type t = string - let compare (s1 : t) (s2 : t) = compare s1 s2 - end +let string_of_uri = function + | Uri (_,s,None) -> s + | Uri (_,s,Some (i,None)) -> + s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ ")" + | Uri (_,s,Some (i, Some k)) -> + s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int k ^ ")" ;; -module MapStringsToUri = Map.Make(OrderedStrings);; - -(* Invariant: the map is the identity function, - * i.e. - * let str' = (MapStringsToUri.find str !set_of_uri) in - * str' == (MapStringsToUri.find str' !set_of_uri) - *) -let set_of_uri = ref MapStringsToUri.empty;; - -exception IllFormedUri of string;; - -let _dottypes = ".types" -let _types = "types",5 -let _dotuniv = ".univ" -let _univ = "univ",4 -let _dotann = ".ann" -let _ann = "ann",3 -let _var = "var",3 -let _dotbody = ".body" -let _con = "con",3 -let _ind = "ind",3 -let _xpointer = "#xpointer(1/" -let _con3 = "con" -let _var3 = "var" -let _ind3 = "ind" -let _ann3 = "ann" -let _univ4 = "univ" -let _types5 = "types" -let _xpointer8 = "xpointer" -let _cic5 = "cic:/" - -let is_malformed suri = - try - if String.sub suri 0 5 <> _cic5 then true - else - let len = String.length suri - 5 in - let last5 = String.sub suri len 5 in - let last4 = String.sub last5 1 4 in - let last3 = String.sub last5 2 3 in - if last3 = _con3 || last3 = _var3 || last3 = _ind3 || - last3 = _ann3 || last5 = _types5 || last5 = _dotbody || - last4 = _univ4 then - false - else - try - let index = String.rindex suri '#' + 1 in - let xptr = String.sub suri index 8 in - if xptr = _xpointer8 then - false - else - true - with Not_found -> true - with Invalid_argument _ -> true - -(* hash conses an uri *) -let uri_of_string suri = - try - MapStringsToUri.find suri !set_of_uri - with Not_found -> - if is_malformed suri then - raise (IllFormedUri suri) - else - let new_uri = suri, fresh_id () in - set_of_uri := MapStringsToUri.add suri new_uri !set_of_uri; - new_uri - - -let strip_xpointer ((uri,_) as olduri) = - try - let index = String.rindex uri '#' in - let no_xpointer = String.sub uri 0 index in - uri_of_string no_xpointer - with - Not_found -> olduri - -let clear_suffix uri ?(pat2="",0) pat1 = - try - let index = String.rindex uri '.' in - let index' = index + 1 in - let suffix = String.sub uri index' (String.length uri - index') in - if fst pat1 = suffix || fst pat2 = suffix then - String.sub uri 0 index - else - uri - with - Not_found -> assert false - -let has_suffix uri (pat,n) = - try - let suffix = String.sub uri (String.length uri - n) n in - pat = suffix - with - Not_found -> assert false - - -let cicuri_of_uri (uri, _) = uri_of_string (clear_suffix uri ~pat2:_types _ann) - -let annuri_of_uri (uri , _) = uri_of_string ((clear_suffix uri _ann) ^ _dotann) - -let uri_is_annuri (uri, _) = has_suffix uri _ann - -let uri_is_var (uri, _) = has_suffix uri _var - -let uri_is_con (uri, _) = has_suffix uri _con - -let uri_is_ind (uri, _) = has_suffix uri _ind - -let bodyuri_of_uri (uri, _) = - if has_suffix uri _con then - Some (uri_of_string (uri ^ _dotbody)) - else - None -;; - -(* these are bugged! - * we should remove _types, _univ, _ann all toghether *) -let innertypesuri_of_uri (uri, _) = - uri_of_string ((clear_suffix uri _types) ^ _dottypes) -;; -let univgraphuri_of_uri (uri,_) = - uri_of_string ((clear_suffix uri _univ) ^ _dotuniv) -;; - - -let uri_of_uriref (uri, _) typeno consno = - let typeno = typeno + 1 in - let suri = - match consno with - | None -> Printf.sprintf "%s%s%d)" uri _xpointer typeno - | Some n -> Printf.sprintf "%s%s%d/%d)" uri _xpointer typeno n - in - uri_of_string suri - -let compare (_,id1) (_,id2) = id1 - id2 - -module OrderedUri = -struct - type t = uri - let compare = compare (* the one above, not Pervasives.compare *) -end - -module UriSet = Set.Make (OrderedUri) - -(* -module OrderedUriPair = -struct - type t = uri * uri - let compare (u11, u12) (u21, u22) = - match compare u11 u21 with - | 0 -> compare u12 u22 - | x -> x -end - -module UriPairSet = Set.Make (OrderedUriPair) -*) - -module HashedUri = -struct - type t = uri - let equal = eq - let hash = snd -end - -module UriHashtbl = Hashtbl.Make (HashedUri) - - diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli index 5dd69e9d9..b05ae502c 100644 --- a/helm/software/components/ng_kernel/nUriManager.mli +++ b/helm/software/components/ng_kernel/nUriManager.mli @@ -25,7 +25,8 @@ exception IllFormedUri of string Lazy.t;; -type uri +(* order, uri, (type, constructor) *) +type uri = private Uri of int * string * (int * int option ) option val eq: uri -> uri -> bool diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml new file mode 100644 index 000000000..c815358a5 --- /dev/null +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -0,0 +1,2 @@ + +let convert_obj obj = Obj.magic obj diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli new file mode 100644 index 000000000..86637b67a --- /dev/null +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -0,0 +1 @@ +val convert_obj: Cic.obj -> NCic.obj diff --git a/helm/software/components/ng_kernel/oCicTypeChecker.ml b/helm/software/components/ng_kernel/oCicTypeChecker.ml new file mode 100644 index 000000000..100e572af --- /dev/null +++ b/helm/software/components/ng_kernel/oCicTypeChecker.ml @@ -0,0 +1,8 @@ + +let typecheck_obj obj = + try + NCicTypeChecker.typecheck_obj (OCic2NCic.convert_obj obj); true + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> false + -- 2.39.2