module Loc pour les localisations ; module Ptree pour les arbres de syntaxe...

module Loc pour les localisations ; module Ptree pour les arbres de syntaxe parses (logique uniquement)

Makefile.in

@@ -88,7 +88,7 @@ check: $(BINARY) $(PRELUDE)
 # why
 #####
 
-LIBCMO = lib/pp.cmo
+LIBCMO = lib/pp.cmo lib/loc.cmo
 
 CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo
 CMX = $(CMO:.cmo=.cmx)

lib/loc.ml

+
+let join (b,_) (_,e) = (b,e)
+
+(*s Error locations. *)
+
+let finally ff f x =
+  let y = try f x with e -> ff (); raise e in ff (); y
+
+(***
+let linenum f b =
+  let cin = open_in f in
+  let rec lookup n l cl =
+    if n = b then 
+      (l,cl)
+    else 
+      let c = input_char cin in
+      lookup (succ n) (if c == '\n' then succ l else l) 
+	(if c == '\n' then 0 else succ cl)
+  in
+  try let r = lookup 0 1 0 in close_in cin; r with e -> close_in cin; raise e
+
+let safe_linenum f b = try linenum f b with _ -> (1,1)
+***)
+
+open Format
+open Lexing
+
+(*s Line number *)
+
+let report_line fmt l = fprintf fmt "%s:%d:" l.pos_fname l.pos_lnum
+
+(* Lexing positions *)
+
+type position = Lexing.position * Lexing.position
+
+exception Located of position * exn
+
+let dummy_position = Lexing.dummy_pos, Lexing.dummy_pos
+
+let gen_report_line fmt (f,l,b,e) = 
+  fprintf fmt "File \"%s\", " f;
+  fprintf fmt "line %d, characters %d-%d" l b e
+
+type floc = string * int * int * int
+
+let dummy_floc = ("",0,0,0)
+
+let extract (b,e) = 
+  let f = b.pos_fname in
+  let l = b.pos_lnum in
+  let fc = b.pos_cnum - b.pos_bol in
+  let lc = e.pos_cnum - b.pos_bol in
+  (f,l,fc,lc)
+
+let gen_report_position fmt loc = 
+  gen_report_line fmt (extract loc)
+
+let report_position fmt pos = 
+  fprintf fmt "%a:@\n" gen_report_position pos
+
+let string =
+  let buf = Buffer.create 1024 in
+  fun loc ->
+    let fmt = Format.formatter_of_buffer buf in
+    Format.fprintf fmt "%a@?" gen_report_position loc;
+    let s = Buffer.contents buf in
+    Buffer.reset buf;
+    s
+
+let parse s =
+  Scanf.sscanf s "File %S, line %d, characters %d-%d"
+    (fun f l c1 c2 -> 
+       (*Format.eprintf "Loc.parse %S %d %d %d@." f l c1 c2;*)
+       let p = 
+	 { Lexing.dummy_pos with pos_fname = f; pos_lnum = l; pos_bol = 0 }
+       in
+       { p with pos_cnum = c1 }, { p with pos_cnum = c2 })
+
+let report_obligation_position ?(onlybasename=false) fmt loc =
+  let (f,l,b,e) = loc in
+  let f = if onlybasename then Filename.basename f else f in
+  fprintf fmt "Why obligation from file \"%s\", " f;
+  fprintf fmt "line %d, characters %d-%d:" l b e
+
+let current_offset = ref 0
+let reloc p = { p with pos_cnum = p.pos_cnum + !current_offset }
+
+(* Identifiers localization *)
+
+let ident_t = Hashtbl.create 97
+let add_ident = Hashtbl.add ident_t
+let ident = Hashtbl.find ident_t

lib/loc.mli

+
+open Format
+
+(*s Line number for an absolute position *)
+
+val report_line : formatter -> Lexing.position -> unit
+
+(* Lexing positions *)
+
+type position = Lexing.position * Lexing.position
+
+exception Located of position * exn
+
+val string : position -> string
+val parse : string -> position
+
+val dummy_position : position
+
+type floc = string * int * int * int
+
+val dummy_floc : floc
+
+val extract :  position -> floc
+val gen_report_line : formatter -> floc -> unit
+val gen_report_position : formatter -> position -> unit
+val report_position : formatter -> position -> unit
+val report_obligation_position : ?onlybasename:bool -> formatter -> floc -> unit
+
+
+(* for both type [t] and [position] *)
+
+val join : 'a * 'b -> 'a * 'b -> 'a * 'b
+
+val current_offset : int ref
+val reloc : Lexing.position -> Lexing.position
+
+(* Identifiers localization *)
+
+val add_ident : string -> floc -> unit
+val ident : string -> floc

src/ptree.mli

+
+(*s Parse trees. *)
+
+type loc = Loc.position
+
+(*s Logical expressions (for both terms and predicates) *)
+
+type real_constant = 
+  | RConstDecimal of string * string * string option (* int / frac / exp *)
+  | RConstHexa of string * string * string
+
+type constant =
+  | ConstInt of string
+  | ConstFloat of real_constant
+
+type pp_infix = 
+  PPand | PPor | PPimplies | PPiff |
+  PPlt | PPle | PPgt | PPge | PPeq | PPneq |
+  PPadd | PPsub | PPmul | PPdiv | PPmod
+
+type pp_prefix = 
+  PPneg | PPnot
+
+type ppure_type =
+  | PPTint
+  | PPTbool
+  | PPTreal
+  | PPTunit
+  | PPTvarid of string * Loc.position
+  | PPTexternal of ppure_type list * string * Loc.position
+
+type lexpr = 
+  { pp_loc : loc; pp_desc : pp_desc }
+
+and pp_desc =
+  | PPvar of string
+  | PPapp of string * lexpr list
+  | PPtrue
+  | PPfalse
+  | PPconst of constant
+  | PPinfix of lexpr * pp_infix * lexpr
+  | PPprefix of pp_prefix * lexpr
+  | PPif of lexpr * lexpr * lexpr
+  | PPforall of string * ppure_type * lexpr list list * lexpr
+  | PPexists of string * ppure_type * lexpr
+  | PPnamed of string * lexpr
+  | PPlet of string * lexpr * lexpr
+  | PPmatch of lexpr * ((string * string list * loc) * lexpr) list
+
+(*s Declarations. *)
+
+type external_ = bool
+
+type plogic_type =
+  | PPredicate of ppure_type list
+  | PFunction of ppure_type list * ppure_type
+
+type decl = 
+  | Logic of loc * external_ * string list * plogic_type
+  | Predicate_def of loc * string * (loc * string * ppure_type) list * lexpr
+  | Inductive_def of loc * string * plogic_type * (loc * string * lexpr) list
+  | Function_def 
+      of loc * string * (loc * string * ppure_type) list * ppure_type * lexpr
+  | Axiom of loc * string * lexpr
+  | Goal of loc * string * lexpr
+  | TypeDecl of loc * external_ * string list * string
+  | AlgType of (loc * string list * string
+      * (loc * string * ppure_type list) list) list
+
+type file = decl list