1 files changed, 231 insertions, 0 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
new file mode 100644
index 00000000..e87ba70c
--- /dev/null
+++ b/contrib/correctness/pcic.ml
@@ -0,0 +1,231 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
+
+(* $Id: pcic.ml,v 1.23.2.1 2004/07/16 19:30:00 herbelin Exp $ *)
+
+open Util
+open Names
+open Nameops
+open Libnames
+open Term
+open Termops
+open Nametab
+open Declarations
+open Indtypes
+open Sign
+open Rawterm
+open Typeops
+open Entries
+open Topconstr
+
+open Pmisc
+open Past
+
+
+(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *)
+
+let make_hole c = mkCast (isevar, c)
+
+(* Tuples are defined in file Tuples.v 
+ * and their constructors are called Build_tuple_n or exists_n,
+ * wether they are dependant (last element only) or not. 
+ * If necessary, tuples are generated ``on the fly''. *)
+
+let tuple_exists id = 
+  try let _ = Nametab.locate (make_short_qualid id) in true
+  with Not_found -> false
+
+let ast_set = CSort (dummy_loc,RProp Pos)
+
+let tuple_n n =
+  let id = make_ident "tuple_" (Some n) in
+  let l1n = Util.interval 1 n in
+  let params =
+    List.map (fun i ->
+      (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set)))
+      l1n in
+  let fields = 
+    List.map
+      (fun i -> 
+	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
+	 let id' = make_ident "T" (Some i) in
+	 (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id')))
+      l1n 
+  in
+  let cons = make_ident "Build_tuple_" (Some n) in
+  Record.definition_structure
+    ((false, (dummy_loc,id)), params, fields, cons, mk_Set)
+
+(*s [(sig_n n)] generates the inductive
+    \begin{verbatim}
+    Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set :=
+      exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P).
+    \end{verbatim} *)
+
+let sig_n n =
+  let id = make_ident "sig_" (Some n) in
+  let l1n = Util.interval 1 n in
+  let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in
+  let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in
+  let idp = make_ident "P" None in
+  let params =
+    let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in
+    (idp, LocalAssum typ) :: 
+    (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT)
+  in
+  let lc = 
+    let app_sig = mkApp(mkRel (2*n+3),
+                        Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in
+    let app_p = mkApp(mkRel (n+1),
+                      Array.init n (fun i -> mkRel (n-i))) in
+    let c = mkArrow app_p app_sig in
+    List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
+  in
+  let cname = make_ident "exist_" (Some n) in
+  Declare.declare_mind 
+    { mind_entry_finite = true;
+      mind_entry_inds = 
+	[ { mind_entry_params = params;
+	    mind_entry_typename = id;
+	    mind_entry_arity = mkSet;
+	    mind_entry_consnames = [ cname ];
+	    mind_entry_lc = [ lc ] } ] }
+
+(*s On the fly generation of needed (possibly dependent) tuples. *)
+
+let check_product_n n =
+  if n > 2 then
+    let s = Printf.sprintf "tuple_%d" n in
+    if not (tuple_exists (id_of_string s)) then tuple_n n
+
+let check_dep_product_n n =
+  if n > 1 then
+    let s = Printf.sprintf "sig_%d" n in
+    if not (tuple_exists (id_of_string s)) then ignore (sig_n n)
+
+(*s Constructors for the tuples. *)
+	
+let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
+let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
+
+let tuple_ref dep n =
+  if n = 2 & not dep then
+    pair
+  else
+    let n = n - (if dep then 1 else 0) in
+    if dep then
+      if n = 1 then 
+	exist
+      else begin
+	let id = make_ident "exist_" (Some n) in
+	if not (tuple_exists id) then ignore (sig_n n);
+	Nametab.locate (make_short_qualid id)
+      end
+    else begin
+      let id = make_ident "Build_tuple_" (Some n) in
+      if not (tuple_exists id) then tuple_n n;
+      Nametab.locate (make_short_qualid id)
+    end
+
+(* Binders. *)
+
+let trad_binder avoid nenv id = function
+  | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
+  | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
+
+let rec push_vars avoid nenv = function
+  | [] -> ([],avoid,nenv)
+  | (id,b) :: bl -> 
+      let b' = trad_binder avoid nenv id b in
+      let bl',avoid',nenv' = 
+	push_vars (id :: avoid) (add_name (Name id) nenv) bl 
+      in
+      ((id,b') :: bl', avoid', nenv')
+
+let rec raw_lambda bl v = match bl with
+  | [] -> 
+      v
+  | (id,ty) :: bl' -> 
+      RLambda (dummy_loc, Name id, ty, raw_lambda bl' v)
+
+(* The translation itself is quite easy.
+   letin are translated into Cases constructions *)
+
+let rawconstr_of_prog p =
+  let rec trad avoid nenv = function
+    | CC_var id -> 
+	RVar (dummy_loc, id)
+
+    (*i optimisation : let x = <constr> in e2  =>  e2[x<-constr] 
+    | CC_letin (_,_,[id,_],CC_expr c,e2) ->
+	real_subst_in_constr [id,c] (trad e2)
+    | CC_letin (_,_,([_] as b),CC_expr e1,e2) ->
+	let (b',avoid',nenv') = push_vars avoid nenv b in
+      	let c1 = Detyping.detype avoid nenv e1 
+	and c2 = trad avoid' nenv' e2 in
+	let id = Name (fst (List.hd b')) in
+	RLetIn (dummy_loc, id, c1, c2)
+    i*)
+
+    | CC_letin (_,_,([_] as b),e1,e2) ->
+	let (b',avoid',nenv') = push_vars avoid nenv b in
+      	let c1 = trad avoid nenv e1 
+	and c2 = trad avoid' nenv' e2 in
+	RApp (dummy_loc, raw_lambda b' c2, [c1])
+
+    | CC_letin (dep,ty,bl,e1,e2) ->
+	let (bl',avoid',nenv') = push_vars avoid nenv bl in
+	let c1 = trad avoid nenv e1
+	and c2 = trad avoid' nenv' e2 in
+	ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None)
+
+    | CC_lam (bl,e) ->
+	let bl',avoid',nenv' = push_vars avoid nenv bl in
+	let c = trad avoid' nenv' e in 
+	raw_lambda bl' c
+
+    | CC_app (f,args) ->
+	let c = trad avoid nenv f
+	and cargs = List.map (trad avoid nenv) args in
+	RApp (dummy_loc, c, cargs)
+
+    | CC_tuple (_,_,[e]) -> 
+	trad avoid nenv e
+	
+    | CC_tuple (false,_,[e1;e2]) ->
+	let c1 = trad avoid nenv e1 
+	and c2 = trad avoid nenv e2 in
+	RApp (dummy_loc, RRef (dummy_loc,pair),
+	      [RHole (dummy_loc,ImplicitArg (pair,1));
+	       RHole (dummy_loc,ImplicitArg (pair,2));c1;c2])
+
+    | CC_tuple (dep,tyl,l) ->
+      	let n = List.length l in
+      	let cl = List.map (trad avoid nenv) l in
+      	let tuple = tuple_ref dep n in
+	let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
+      	let args = tyl @ cl in
+	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
+
+    | CC_case (ty,b,el) ->
+	let c = trad avoid nenv b in
+	let cl = List.map (trad avoid nenv) el in
+	let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
+	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
+
+    | CC_expr c -> 
+	Detyping.detype (false,Global.env()) avoid nenv c
+
+    | CC_hole c -> 
+	RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
+               Detyping.detype (false,Global.env()) avoid nenv c)
+
+  in
+  trad [] empty_names_context p