aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/rawterm.mli
blob: 8c93eecd9f145409143b1dbb1fc7b15dfb9e0205 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

(* $Id$ *)

(*i*)
open Names
open Sign
open Type_errors
(*i*)

(* Untyped intermediate terms, after ASTs and before constr. *)

type loc = int * int

(* locs here refers to the ident's location, not whole pat *)
(* the last argument of PatCstr is a possible alias ident for the pattern *)
type pattern =
  | PatVar of loc * name
  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name

type binder_kind = BProd | BLambda
type fix_kind = RFix of int array * int | RCofix of int
type rawsort = RProp of Term.contents | RType

type reference =
  | RConst of section_path * identifier list
  | RInd of inductive_path * identifier list
  | RConstruct of constructor_path * identifier list
  | RAbst of section_path
  | RVar of identifier
  | REVar of int * identifier list
  | RMeta of int

type cases_style = PrintLet | PrintIf | PrintCases

type rawconstr = 
  | RRef of loc * reference
  | RApp of loc * rawconstr * rawconstr list
  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
      (identifier list * pattern list * rawconstr) list
  | ROldCase of loc * bool * rawconstr option * rawconstr * 
      rawconstr array
  | RRec of loc * fix_kind * identifier array * 
      rawconstr array * rawconstr array
  | RSort of loc * rawsort
  | RHole of loc option
  | RCast of loc * rawconstr * rawconstr


(*i - if PRec (_, names, arities, bodies) is in env then arities are
   typed in env too and bodies are typed in env enriched by the
   arities incrementally lifted 

  [On pourrait plutot mettre les arités aves le type qu'elles auront
   dans le contexte servant à typer les body ???]

   - boolean in POldCase means it is recursive
   - option in PHole tell if the "?" was apparent or has been implicitely added
i*)

val dummy_loc : loc
val loc_of_rawconstr : rawconstr -> loc