let nargs it nleft consno =
pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
- let _,indname,_,cl = it in
+ let _,_indname,_,cl = it in
let _,_,t_k = List.nth cl consno in
List.length (arg_list nleft t_k) ;;
let default_pattern = "",0,(None,[],Some NotationPt.UserInput);;
let prod_pattern =
- "",0,(None,[],Some NotationPt.Binder
+ "",0,(None,[],Some (NotationPt.Binder
(`Pi, (mk_id "_",Some (NotationPt.Appl
[ NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne
; NotationPt.UserInput
; NotationPt.Implicit `JustOne ])),
- NotationPt.Implicit `JustOne));;
+ NotationPt.Implicit `JustOne)));;
let prod_pattern_jm =
- "",0,(None,[],Some NotationPt.Binder
+ "",0,(None,[],Some (NotationPt.Binder
(`Pi, (mk_id "_",Some (NotationPt.Appl
[ NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne
; NotationPt.UserInput
; NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne ])),
- NotationPt.Implicit `JustOne));;
+ NotationPt.Implicit `JustOne)));;
let hp_pattern n =
"",0,(None,[n, NotationPt.Appl
(* PHASE 1: derive the type of the discriminator (we'll name it "principle") *)
- let mk_eq tys ts us es n deps =
+ let mk_eq tys ts us es n =
if use_jmeq then
mk_appl [mk_id "jmeq";
NotationPt.Implicit `JustOne; List.nth ts n;
NotationPt.Implicit `JustOne; List.nth us n]
else
- (* we use deps in an attempt to remove unnecessary rewritings when the type
- is not maximally dependent *)
(* eqty = Tn u0 e0...un-1 en-1 *)
let eqty = mk_appl
- (List.nth tys n :: iter
- (fun i acc ->
- if (List.mem (List.nth ts i) deps)
- then List.nth us i::
- List.nth es i::acc
- else acc)
- (n-1) []) in
-
- (* params = [T0;t0;...;Tn;tn;u0;e0;...;un-1;en-1] *)
+ (List.nth tys n :: iter (fun i acc ->
+ List.nth us i::
+ List.nth es i:: acc)
+ (n-1) []) in
+
+ (* params = [T0;t0;...;Tn;tn;u0;e0;un-1;en-1] *)
let params = iter (fun i acc ->
- if (List.mem (List.nth ts i) deps)
- then List.nth tys i ::
- List.nth ts i :: acc
- else acc) (n-1)
- (List.nth tys n::List.nth ts n::
- iter (fun i acc ->
- if (List.mem (List.nth ts i) deps)
- then List.nth us i::
- List.nth es i::acc
- else acc) (n-1) []) in
- let nrewrites = List.length deps in
+ List.nth tys i ::
+ List.nth ts i :: acc) n
+ (iter (fun i acc ->
+ List.nth us i::
+ List.nth es i:: acc) (n-1) []) in
mk_appl [mk_id "eq"; eqty;
- mk_appl (mk_id ("R" ^ string_of_int nrewrites) :: params);
- List.nth us n]
+ mk_appl (mk_id ("R" ^ string_of_int n) :: params);
+ List.nth us n]
in
name
in
- let branch i j ts us deps =
+ let branch i j ts us =
let nargs = nargs it leftno i in
let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in
- let ndepargs k =
- let tk = List.nth ts k in
- List.length (List.assoc tk deps)
- in
let tys = List.map
- (fun x ->
- iter
+ (fun x -> iter
(fun i acc ->
NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None),
NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None),
- acc))) ((ndepargs x) - 1)
+ acc))) (x-1)
(NotationPt.Implicit (`Tagged ("T" ^ (string_of_int x)))))
(HExtlib.list_seq 0 nargs) in
let tys = tys @
if i = j then
NotationPt.Binder (`Forall, (mk_id "_",
Some (iter (fun i acc ->
- NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i (List.assoc (List.nth ts i) deps))), acc))
+ NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc))
(nargs-1)
(** (NotationPt.Binder (`Forall, (mk_id "_",
Some (mk_eq tys ts us es nargs)),*)
else mk_id "P")
in
- let inner i ts deps =
- NotationPt.Case
+ let inner i ts = NotationPt.Case
(mk_id "y",None,
(*Some (NotationPt.Binder (`Lambda, (mk_id "y",None),
NotationPt.Binder (`Forall, (mk_id "_", Some
NotationPt.Pattern (kname j,
None,
List.combine us nones),
- branch i j ts us deps)
+ branch i j ts us)
(HExtlib.list_seq 0 (List.length cl)))
in
let outer = NotationPt.Case
(mk_id "x",None,
None ,
List.map
- (fun i ->
- let _,_,kty = List.nth cl i in
+ (fun i ->
let nargs_kty = nargs it leftno i in
- let ts = iter (fun m acc -> ("t" ^ (string_of_int m))::acc)
+ if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i));
+ let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
(nargs_kty - 1) [] in
- (* this context is used to compute dependencies between constructor arguments *)
- let kctx = List.map2 (fun t ty -> t, NCic.Decl ty) (List.rev ts) (List.rev (arg_list leftno kty)) in
- let ts = List.map mk_id ts in
- (* compute graph of dependencies *)
- let deps,_ = List.fold_left
- (fun (acc,i) (t,_) ->
- let name,_ = List.nth kctx (i-1) in
- (name,fst (cascade_select_in_ctx status ~subst:[] kctx [] i))::acc,i+1) ([],1) kctx
- in
- (* transpose graph *)
- let deps = List.fold_left
- (fun acc (t,_) ->
- let t_deps = List.map fst (List.filter (fun (name,rev_deps) -> List.mem t rev_deps) deps) in
- (t,t_deps)::acc) [] deps
- in
- let deps = List.map (fun (x,xs) -> mk_id x, (List.map mk_id) xs) deps in
- let max_dep = List.fold_left max 0 (List.map (fun (_,xs) -> List.length xs) deps) in
- if (max_dep > 4 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i));
-
- let nones =
+ let nones =
iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in
NotationPt.Pattern (kname i,
None,
List.combine ts nones),
- inner i ts deps)
+ inner i ts)
(HExtlib.list_seq 0 (List.length cl))) in
let principle =
mk_prods params (NotationPt.Binder (`Forall, (mk_id "x",
(* PHASE 2: create the object for the proof of the principle: we'll name it
* "theorem" *)
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,principle,
- Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+ (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
- let uri,height,nmenv,nsubst,nobj = theorem in
+ let _uri,_height,nmenv,_nsubst,_nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
(* PHASE 3: we finally prove the discrimination principle *)
- let dbranch it ~use_jmeq leftno consno =
+ let dbranch it ~use_jmeq:__ leftno consno =
let refl_id = mk_sym "refl" in
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
;;
let subst_tac ~context ~dir skip cur_eq =
- fun status as oldstatus ->
+ fun (status as oldstatus) ->
let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
let _,ctx' = HExtlib.split_nth cur_eq context in
let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in
else
let gen_tac x =
(fun s ->
- let x' = String.concat " " x in
+ (*let x' = String.concat " " x in*)
let x = List.map mk_id x in
(* let s = NTactics.print_tac false ("@generalize " ^ x') s in *)
generalize0_tac x s) in
| _ -> status, `NonEq
in match kind with
| `Identity ->
- let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+ let status, _goalty = term_of_cic_term status (get_goalty status goal) ctx in
status, Some (List.length ctx - i), kind
| `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
| _ ->
projects / helm.git / blobdiff