matita/components/binaries/matex/meta.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 module L = List
  13
  14 module C = NCic
  15
  16 module X = Ground
  17 module G = Options
  18 module K = Kernel
  19
  20 type term = Meta
  21           | Sort of C.sort
  22           | GRef of string * string
  23           | LRef of int
  24           | Appl of term list
  25           | Prod of string * term * term
  26           | Abst of string * term * term
  27           | Abbr of string * term * term * term
  28           | Case of term * term * term * term list
  29           | Sigs of string list * term list * term list
  30
  31 (* internal functions *******************************************************)
  32
  33 let get_sigs s =
  34    let rec aux = function
  35       | []              -> G.nan, G.nan
  36       | (n, i, j) :: tl ->
  37          if n = s then i, j else aux tl
  38    in
  39    aux !G.sigs_gref
  40
  41 let rec get_names ss j t =
  42    if j <= 0 then ss else match t with
  43       | Abst (s, _, t) -> get_names (s :: ss) (pred j) t
  44       | _              -> assert false
  45
  46 let rec trim_absts j t =
  47    if j <= 0 then t else match t with
  48       | Abst (_, _, t) -> trim_absts (pred j) t
  49       | _              -> assert false
  50
  51 let proc_appl ts = match ts with
  52    | GRef (s, _) :: vs ->
  53       let i, j = get_sigs s in
  54       if L.length vs <> i + j || i = 0 || j = 0 then Appl ts else
  55       let types, preds = X.split_at j vs in
  56       let names = get_names [] j (L.hd preds) in
  57       let preds = L.rev_map (trim_absts j) preds in
  58       Sigs (names, types, preds)
  59    | ts                -> Appl ts
  60
  61 let rec proc_term = function
  62    | C.Meta _
  63    | C.Implicit _          -> Meta
  64    | C.Sort s              -> Sort s
  65    | C.Const c             ->
  66       let s, name = K.resolve_reference c in
  67       GRef (s, name)
  68    | C.Rel m               -> LRef m
  69    | C.Appl ts             -> proc_appl (proc_terms ts)
  70    | C.Prod (s, w, t)      -> Prod (s, proc_term w, proc_term t)
  71    | C.Lambda (s, w, t)    -> Abst (s, proc_term w, proc_term t)
  72    | C.LetIn (s, w, v, t)  -> Abbr (s, proc_term w, proc_term v, proc_term t)
  73    | C.Match (c, u, v, ts) -> Case (proc_term (C.Const c), proc_term u, proc_term v, proc_terms ts)
  74
  75 and proc_terms ts =
  76    L.rev (L.rev_map proc_term ts)
  77
  78 (* interface functions ******************************************************)
  79
  80 let process = proc_term