X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=fcc80369794c375c8bbe0b8d825d8cece1f2b701;hb=afd3b379d4959e4a18c1f26f25e4a9c14997866f;hp=f7392fa3ac34bdfe8c4423902cd54a4c4c15fb06;hpb=ee02781cec1158f51e98ca73a14b63841e5ba545;p=helm.git diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml index f7392fa3a..fcc803697 100644 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -23,7 +23,28 @@ * http://helm.cs.unibo.it/ *) -type location = int * int +(** {2 Parsing related types} *) + +type location = Lexing.position * Lexing.position + + (* maps old style (i.e. <= 3.07) lexer location to new style location, padding + * with dummy values where needed *) +let floc_of_loc (loc_begin, loc_end) = + let floc_begin = + { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; + Lexing.pos_cnum = loc_begin } + in + let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in + (floc_begin, floc_end) + + (* the other way round *) +let loc_of_floc = function + | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> + (loc_begin, loc_end) + +let dummy_floc = floc_of_loc (-1, -1) + +(** {2 Cic Ast} *) type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ]