From d016f69818b30b75d186fb14f440b93b0518fc66 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 21 Nov 2019 15:38:39 +0100 Subject: [coq] Untabify the whole ML codebase. We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` --- kernel/constr.ml | 114 +++++++++++++++++++++++++++---------------------------- 1 file changed, 57 insertions(+), 57 deletions(-) (limited to 'kernel/constr.ml') diff --git a/kernel/constr.ml b/kernel/constr.ml index b60b2d6d04..15e5c512ed 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -16,7 +16,7 @@ (* Optimization of substitution functions by Chet Murthy *) (* Optimization of lifting functions by Bruno Barras, Mar 1997 *) (* Hash-consing by Bruno Barras in Feb 1998 *) -(* Restructuration of Coq of the type-checking kernel by Jean-Christophe +(* Restructuration of Coq of the type-checking kernel by Jean-Christophe Filliâtre, 1999 *) (* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *) (* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) @@ -924,7 +924,7 @@ let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true - else + else let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = @@ -933,11 +933,11 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true - else + else let eq_universes _ _ = UGraph.check_eq_instances univs in - let eq_sorts s1 s2 = s1 == s2 || + let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let leq_sorts s1 s2 = s1 == s2 || + let leq_sorts s1 s2 = s1 == s2 || UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -949,17 +949,17 @@ let leq_constr_univs univs m n = let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty - else + else let cstrs = ref Constraint.empty in let eq_universes _ _ = UGraph.check_eq_instances univs in - let eq_sorts s1 s2 = + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else - (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_eq univs u1 u2 then true + else + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -969,23 +969,23 @@ let eq_constr_univs_infer univs m n = let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty - else + else let cstrs = ref Constraint.empty in let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in - let eq_sorts s1 s2 = + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_eq univs u1 u2 then true + else (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in - let leq_sorts s1 s2 = + let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_leq univs u1 u2 then true - else + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_leq univs u1 u2 then true + else (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in cstrs := Univ.Constraint.union c !cstrs; true @@ -1183,54 +1183,54 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let rec hash_term t = match t with | Var i -> - (Var (sh_id i), combinesmall 1 (Id.hash i)) + (Var (sh_id i), combinesmall 1 (Id.hash i)) | Sort s -> - (Sort (sh_sort s), combinesmall 2 (Sorts.hash s)) + (Sort (sh_sort s), combinesmall 2 (Sorts.hash s)) | Cast (c, k, t) -> - let c, hc = sh_rec c in - let t, ht = sh_rec t in - (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht)) + let c, hc = sh_rec c in + let t, ht = sh_rec t in + (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht)) | Prod (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in + let t, ht = sh_rec t + and c, hc = sh_rec c in (Prod (sh_na na, t, c), combinesmall 4 (combine3 (hash_annot Name.hash na) ht hc)) | Lambda (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in + let t, ht = sh_rec t + and c, hc = sh_rec c in (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (hash_annot Name.hash na) ht hc)) | LetIn (na,b,t,c) -> - let b, hb = sh_rec b in - let t, ht = sh_rec t in - let c, hc = sh_rec c in + let b, hb = sh_rec b in + let t, ht = sh_rec t in + let c, hc = sh_rec c in (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc)) | App (c,l) -> - let c, hc = sh_rec c in - let l, hl = hash_term_array l in - (App (c,l), combinesmall 7 (combine hl hc)) + let c, hc = sh_rec c in + let l, hl = hash_term_array l in + (App (c,l), combinesmall 7 (combine hl hc)) | Evar (e,l) -> - let l, hl = hash_term_array l in - (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) + let l, hl = hash_term_array l in + (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Const (c,u) -> - let c' = sh_con c in - let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) + let c' = sh_con c in + let u', hu = sh_instance u in + (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) | Ind (ind,u) -> - let u', hu = sh_instance u in - (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + let u', hu = sh_instance u in + (Ind (sh_ind ind, u'), + combinesmall 10 (combine (ind_syntactic_hash ind) hu)) | Construct (c,u) -> - let u', hu = sh_instance u in - (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + let u', hu = sh_instance u in + (Construct (sh_construct c, u'), + combinesmall 11 (combine (constructor_syntactic_hash c) hu)) | Case (ci,p,c,bl) -> - let p, hp = sh_rec p - and c, hc = sh_rec c in - let bl,hbl = hash_term_array bl in + let p, hp = sh_rec p + and c, hc = sh_rec c in + let bl,hbl = hash_term_array bl in let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) + (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in @@ -1238,16 +1238,16 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (Fix (ln,(lna,tl,bl)), combinesmall 13 h) | CoFix(ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in let h = combine3 hna hbl htl in (CoFix (ln,(lna,tl,bl)), combinesmall 14 h) | Meta n -> - (t, combinesmall 15 n) + (t, combinesmall 15 n) | Rel n -> - (t, combinesmall 16 n) + (t, combinesmall 16 n) | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in -- cgit v1.2.3