matita/components/binaries/xoa/engine.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 P = Printf
  13 module A = Ast
  14
  15 let string_iter sep f n =
  16    let rec aux = function
  17       | n when n < 1 -> ""
  18       | 1            -> f 1
  19       | n            -> f n ^ sep ^ aux (pred n)
  20    in
  21    aux n
  22
  23 let void_iter f n =
  24    let rec aux = function
  25       | n when n < 1 -> ()
  26       | 1            -> f 1
  27       | n            -> f n; aux (pred n)
  28    in
  29    aux n
  30
  31 let mk_exists ooch noch c v =
  32    let description = "multiple existental quantifier" in
  33    let prec = "non associative with precedence 20\n" in
  34    let name s =
  35       if v = 1 then P.sprintf "%s%u" s c else P.sprintf "%s%u_%u" s c v
  36    in
  37    let o_name = name "ex" in
  38    let i_name =
  39       if v = 1 then "'Ex" else P.sprintf "'Ex%u" v
  40    in
  41    let set n      = P.sprintf "A%u" (v - n) in
  42    let set_list   = string_iter "," set v in
  43    let set_type   = string_iter "→" set v in
  44
  45    let ele n      = P.sprintf "x%u" (v - n) in
  46    let ele_list   = string_iter "," ele v in
  47    let ele_seq    = string_iter " " ele v in
  48
  49    let pre n      = P.sprintf "P%u" (c - n) in
  50    let pre_list   = string_iter "," pre c in
  51    let pre_seq    = string_iter " " pre c in
  52    let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in
  53    let pre_type   = string_iter " → " pre_appl c in
  54
  55    let qm n       = "?" in
  56    let qm_set     = string_iter " " qm v in
  57    let qm_pre     = string_iter " " qm c in
  58
  59    let id n       = P.sprintf "ident x%u" (v - n) in
  60    let id_list    = string_iter " , " id v in
  61
  62    let term n     = P.sprintf "term 19 P%u" (c - n) in
  63    let term_conj  = string_iter " break & " term c in
  64
  65    let abst b n   = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in
  66                     P.sprintf "λ${ident x%u}%s" (v - n) xty in
  67
  68    let abst_clo b = string_iter "." (abst b) v in
  69
  70    let full b n   = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in
  71    let full_seq b = string_iter " " (full b) c in
  72
  73    P.fprintf ooch "(* %s (%u, %u) *)\n\n" description c v;
  74
  75    P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n"
  76       o_name set_list pre_list set_type;
  77    P.fprintf ooch "   | %s_intro: ∀%s. %s → %s %s %s\n.\n\n"
  78       o_name ele_list pre_type o_name qm_set qm_pre;
  79
  80    P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n"
  81       description c v i_name pre_seq o_name qm_set pre_seq;
  82
  83    P.fprintf noch "(* %s (%u, %u) *)\n\n" description c v;
  84
  85    P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n"
  86       id_list term_conj prec i_name (full_seq false);
  87
  88    P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n"
  89       id_list term_conj prec i_name (full_seq true)
  90
  91 let mk_or ooch noch c =
  92    let description = "multiple disjunction connective" in
  93    let prec = "non associative with precedence 30\n" in
  94    let name s = P.sprintf "%s%u" s c in
  95    let o_name = name "or" in
  96    let i_name = "'Or" in
  97
  98    let pre n      = P.sprintf "P%u" (c - n) in
  99    let pre_list   = string_iter "," pre c in
 100    let pre_seq    = string_iter " " pre c in
 101
 102    let qm n       = "?" in
 103    let qm_pre     = string_iter " " qm c in
 104
 105    let term n     = P.sprintf "term 29 P%u" (c - n) in
 106    let term_disj  = string_iter " break | " term c in
 107
 108    let par n     = P.sprintf "$P%u" (c - n) in
 109    let par_seq   = string_iter " " par c in
 110
 111    let mk_con n   = P.fprintf ooch "   | %s_intro%u: %s → %s %s\n"
 112                        o_name (c - n) (pre n) o_name qm_pre
 113    in
 114
 115    P.fprintf ooch "(* %s (%u) *)\n\n" description c;
 116
 117    P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
 118       o_name pre_list;
 119    void_iter mk_con c;
 120    P.fprintf ooch ".\n\n";
 121
 122    P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
 123       description c i_name pre_seq o_name pre_seq;
 124
 125    P.fprintf noch "(* %s (%u) *)\n\n" description c;
 126
 127    P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n"
 128       term_disj prec i_name par_seq
 129
 130 let mk_and ooch noch c =
 131    let description = "multiple conjunction connective" in
 132    let prec = "non associative with precedence 35\n" in
 133    let name s = P.sprintf "%s%u" s c in
 134    let o_name = name "and" in
 135    let i_name = "'And" in
 136
 137    let pre n      = P.sprintf "P%u" (c - n) in
 138    let pre_list   = string_iter "," pre c in
 139    let pre_type   = string_iter " → " pre c in
 140    let pre_seq    = string_iter " " pre c in
 141
 142    let qm n       = "?" in
 143    let qm_pre     = string_iter " " qm c in
 144
 145    let term n     = P.sprintf "term 34 P%u" (c - n) in
 146    let term_conj  = string_iter " break & " term c in
 147
 148    let par n     = P.sprintf "$P%u" (c - n) in
 149    let par_seq   = string_iter " " par c in
 150
 151    P.fprintf ooch "(* %s (%u) *)\n\n" description c;
 152
 153    P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n"
 154       o_name pre_list;
 155    P.fprintf ooch "   | %s_intro: %s → %s %s\n.\n\n"
 156       o_name pre_type o_name qm_pre;
 157
 158    P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
 159       description c i_name pre_seq o_name pre_seq;
 160
 161    P.fprintf noch "(* %s (%u) *)\n\n" description c;
 162
 163    P.fprintf noch "notation \"hvbox(∧∧ %s)\"\n %s for @{ %s %s }.\n\n"
 164       term_conj prec i_name par_seq
 165
 166 let generate ooch noch = function
 167    | A.Exists (c, v) ->
 168       if c > 0 && v > 0 then mk_exists ooch noch c v
 169    | A.Or c          ->
 170       if c > 1 then mk_or ooch noch c
 171    | A.And c         ->
 172       if c > 1 then mk_and ooch noch c